chore(Order): process misc porting notes

Author: jcommelin

Mathlib/Order/Defs/LinearOrder.lean

@@ -130,8 +130,6 @@ theorem le_imp_le_of_lt_imp_lt {α β} [Preorder α] [LinearOrder β] {a b : α}
 lemma min_def (a b : α) : min a b = if a ≤ b then a else b := by rw [LinearOrder.min_def a]
 lemma max_def (a b : α) : max a b = if a ≤ b then b else a := by rw [LinearOrder.max_def a]
 
--- Porting note: no `min_tac` tactic in the following series of lemmas
-
 lemma min_le_left (a b : α) : min a b ≤ a := by
   if h : a ≤ b
   then simp [min_def, if_pos h, le_refl]

Mathlib/Order/Extension/Well.lean

@@ -22,11 +22,11 @@ We can map our order into two well-orders:
 
 Then their lexicographic product is a well-founded linear order which our original order injects in.
 
-## Porting notes
+## Implementation note
 
-The definition in `mathlib` 3 used an auxiliary well-founded order on `α` lifted from `Cardinal`
-instead of `Cardinal`. The new definition is definitionally equal to the `mathlib` 3 version but
-avoids non-standard instances.
+The definition in `mathlib` 3 used an auxiliary well-founded order on `α` lifted from `Cardinal`,
+instead of using `Cardinal` directly. The new definition is definitionally equal
+to the `mathlib` 3 version but avoids non-standard instances.
 
 ## Tags
 

Mathlib/Order/Filter/AtTopBot/Basic.lean

@@ -441,7 +441,6 @@ theorem tendsto_add_atTop_iff_nat {f : ℕ → α} {l : Filter α} (k : ℕ) :
 
 theorem map_div_atTop_eq_nat (k : ℕ) (hk : 0 < k) : map (fun a => a / k) atTop = atTop :=
   map_atTop_eq_of_gc (fun b => k * b + (k - 1)) 1 (fun _ _ h => Nat.div_le_div_right h)
-    -- Porting note: there was a parse error in `calc`, use `simp` instead
     (fun a b _ => by rw [Nat.div_le_iff_le_mul_add_pred hk])
     fun b _ => by rw [Nat.mul_add_div hk, Nat.div_eq_of_lt, Nat.add_zero]; omega
 

Mathlib/Order/GameAdd.lean

@@ -200,19 +200,16 @@ attribute [local instance] Sym2.Rel.setoid
 /-- Recursion on the well-founded `Sym2.GameAdd` relation. -/
 def GameAdd.fix {C : α → α → Sort*} (hr : WellFounded rα)
     (IH : ∀ a₁ b₁, (∀ a₂ b₂, Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) (a b : α) :
-    C a b := by
-  -- Porting note: this was refactored for https://github.com/leanprover-community/mathlib4/pull/3414 (reenableeta), and could perhaps be cleaned up.
-  have := hr.sym2_gameAdd
-  dsimp only [GameAdd, lift₂, DFunLike.coe, EquivLike.coe] at this
-  exact @WellFounded.fix (α × α) (fun x => C x.1 x.2) _ this.of_quotient_lift₂
+    C a b :=
+  @WellFounded.fix (α × α) (fun x => C x.1 x.2)
+    (fun x y ↦ Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα x.swap y)
+    (by simpa [← Sym2.gameAdd_iff] using hr.sym2_gameAdd.onFun)
     (fun ⟨x₁, x₂⟩ IH' => IH x₁ x₂ fun a' b' => IH' ⟨a', b'⟩) (a, b)
 
 theorem GameAdd.fix_eq {C : α → α → Sort*} (hr : WellFounded rα)
     (IH : ∀ a₁ b₁, (∀ a₂ b₂, Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) (a b : α) :
-    GameAdd.fix hr IH a b = IH a b fun a' b' _ => GameAdd.fix hr IH a' b' := by
-  -- Porting note: this was refactored for https://github.com/leanprover-community/mathlib4/pull/3414 (reenableeta), and could perhaps be cleaned up.
-  dsimp [GameAdd.fix]
-  exact WellFounded.fix_eq _ _ _
+    GameAdd.fix hr IH a b = IH a b fun a' b' _ => GameAdd.fix hr IH a' b' :=
+  WellFounded.fix_eq ..
 
 /-- Induction on the well-founded `Sym2.GameAdd` relation. -/
 theorem GameAdd.induction {C : α → α → Prop} :

Mathlib/Order/Height.lean

@@ -271,14 +271,8 @@ theorem chainHeight_insert_of_forall_gt (a : α) (hx : ∀ b ∈ s, a < b) :
     refine ⟨a::l, ⟨?_, ?_⟩, by simp⟩
     · rw [chain'_cons']
       exact ⟨fun y hy ↦ hx _ (hl.2 _ (mem_of_mem_head? hy)), hl.1⟩
-    · -- Porting note: originally this was
-        -- rintro x (rfl | hx)
-        -- exacts [Or.inl (Set.mem_singleton x), Or.inr (hl.2 x hx)]
-      -- but this fails because `List.Mem` is now an inductive prop.
-      -- I couldn't work out how to drive `rcases` here but asked at
-      -- https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/rcases.3F/near/347976083
-      rintro x (_ | _)
-      exacts [Or.inl (Set.mem_singleton a), Or.inr (hl.2 x ‹_›)]
+    · rintro x (_ | _)
+      exacts [Or.inl (Set.mem_singleton a), Or.inr (hl.2 x ‹x ∈ l›)]
 
 theorem chainHeight_insert_of_forall_lt (a : α) (ha : ∀ b ∈ s, b < a) :
     (insert a s).chainHeight = s.chainHeight + 1 := by

Mathlib/Order/Heyting/Hom.lean

@@ -248,7 +248,6 @@ instance instHeytingHomClass : HeytingHomClass (HeytingHom α β) α β where
   map_bot f := f.map_bot'
   map_himp := HeytingHom.map_himp'
 
--- @[simp] -- Porting note: not in simp-nf, simp can simplify lhs. Added aux simp lemma
 theorem toFun_eq_coe {f : HeytingHom α β} : f.toFun = ⇑f :=
   rfl
 
@@ -354,7 +353,6 @@ instance : CoheytingHomClass (CoheytingHom α β) α β where
   map_top f := f.map_top'
   map_sdiff := CoheytingHom.map_sdiff'
 
--- @[simp] -- Porting note: not in simp-nf, simp can simplify lhs. Added aux simp lemma
 theorem toFun_eq_coe {f : CoheytingHom α β} : f.toFun = (f : α → β) :=
   rfl
 
@@ -460,7 +458,6 @@ instance : BiheytingHomClass (BiheytingHom α β) α β where
   map_himp f := f.map_himp'
   map_sdiff f := f.map_sdiff'
 
--- @[simp] -- Porting note: not in simp-nf, simp can simplify lhs. Added aux simp lemma
 theorem toFun_eq_coe {f : BiheytingHom α β} : f.toFun = (f : α → β) :=
   rfl
 

Mathlib/Order/PropInstances.lean

@@ -92,7 +92,6 @@ theorem Prop.isCompl_iff {P Q : Prop} : IsCompl P Q ↔ ¬(P ↔ Q) := by
   rw [_root_.isCompl_iff, Prop.disjoint_iff, Prop.codisjoint_iff, not_iff]
   by_cases P <;> by_cases Q <;> simp [*]
 
--- Porting note: Lean 3 would unfold these for us, but we need to do it manually now
 section decidable_instances
 
 universe u