gistfile1.txt

Mathport suggests:
```
structure Finset (α : Type _) where
  val : Multiset α
  Nodup : Nodup val
```  
amended to:
```
structure Finset (α : Type _) where
  val : Multiset α
  nodup : Nodup val
```

Changes:
* propositional fields of structures should start lowercase

---

Mathport suggests:
```
theorem mem_split {a : α} {l : List α} (h : a ∈ l) : ∃ s t : List α, l = s ++ a :: t := by
  induction' l with b l ih
  · cases h
    
  rcases h with (rfl | h)
  · exact ⟨[], l, rfl⟩
    
  · rcases ih h with ⟨s, t, rfl⟩
    exact ⟨b :: s, t, rfl⟩
```
amended to:
```
theorem mem_split {a : α} {l : List α} (h : a ∈ l) : ∃ s t : List α, l = s ++ a :: t := by
  induction l with
  | nil => cases h
  | cons b l ih =>
    cases h with
    | head => exact ⟨[], l, rfl⟩
    | tail _ h =>
      rcases ih h with ⟨s, t, rfl⟩
      exact ⟨b :: s, t, rfl⟩
```          

Changes:
* There's no `induction'` tactic that just takes a big list of new identifiers and greedily uses them in the different cases.
* I couldn't get `rcases h with (rfl | h)`, or any variant, to work.
  Using `rfl` generates an error, but replacing it with `_` gives the desired behaviour.
  I couldn't get `rcases` to introduce a new hypothesis named `h` in the 2nd branch.

---

Mathport suggests:
```
theorem pairwise_append {l₁ l₂ : List α} :
    Pairwiseₓ R (l₁ ++ l₂) ↔ Pairwiseₓ R l₁ ∧ Pairwiseₓ R l₂ ∧ ∀ x ∈ l₁, ∀ y ∈ l₂, R x y := by
  induction' l₁ with x l₁ IH <;>
    [simp only [List.Pairwiseₓ.nil, forall_prop_of_false (not_mem_nil _), forall_true_iff, and_trueₓ, true_andₓ,
      nil_append],
    simp only [cons_append, pairwise_cons, forall_mem_append, IH, forall_mem_cons, forall_and_distrib, and_assocₓ,
      And.left_comm]]
```
amended to:
```
theorem pairwise_append {l₁ l₂ : List α} :
    Pairwise R (l₁ ++ l₂) ↔ Pairwise R l₁ ∧ Pairwise R l₂ ∧ (∀ x, x ∈ l₁ → ∀ y, y ∈ l₂ → R x y) :=
by
  induction l₁ with
  | nil => simp [Pairwise.nil]
  | cons a l₁ ih =>
    simp only [cons_append, Pairwise_cons, forall_mem_append, ih, forall_mem_cons,
      forall_and_distrib, and_assoc, And.left_comm]
    rfl
```

Changes:
* Remove the `ₓ` from each appearance of `Pairwiseₓ`. (Also in `List.Pairwiseₓ.nil`, `and_trueₓ`, `true_andₓ`, `and_assocₓ`.)
* Binders of the form `∀ x ∈ l₁` not yet supported.
* Replace `induction'` with structured `induction` tactic.
* In the first branch, `List.Pairwiseₓ.nil` doesn't need the `List.` prefix, as we're in that namespace.
* In the first branch, the lemma `forall_prop_of_false (not_mem_nil _)` is not successfully used by `simp`. Worked around by using `simp` rather than `simp only`.
* In the second branch, change `pairwise_cons` to `Pairwise_cons`.
* In the second branch, need to add `rfl` after `simp only`.

---

Mathport suggests:
```
theorem pairwise_append_comm (s : Symmetric R) {l₁ l₂ : List α} : Pairwiseₓ R (l₁ ++ l₂) ↔ Pairwiseₓ R (l₂ ++ l₁) := by
  have : ∀ l₁ l₂ : List α, (∀ x : α, x ∈ l₁ → ∀ y : α, y ∈ l₂ → R x y) → ∀ x : α, x ∈ l₂ → ∀ y : α, y ∈ l₁ → R x y :=
    fun l₁ l₂ a x xm y ym => s (a y ym x xm)
  simp only [pairwise_append, And.left_comm] <;> rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]
```
amended to:
```
theorem pairwise_append_comm (s : symmetric R) {l₁ l₂ : List α} :
  Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁) := by
  have : ∀ l₁ l₂ : List α, (∀ x : α, x ∈ l₁ → ∀ y : α, y ∈ l₂ → R x y) →
    ∀ x : α, x ∈ l₂ → ∀ y : α, y ∈ l₁ → R x y := fun l₁ l₂ a x xm y ym => s (a y ym x xm)
  simp only [pairwise_append, And.left_comm] <;> rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]
```

Changes:
* `Symmetric` to `symmetric`

---

Mathport suggests:
```
theorem Perm.pairwise_iff {R : α → α → Prop} (S : Symmetric R) :
    ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), Pairwiseₓ R l₁ ↔ Pairwiseₓ R l₂ :=
  suffices ∀ {l₁ l₂}, l₁ ~ l₂ → Pairwiseₓ R l₁ → Pairwiseₓ R l₂ from fun l₁ l₂ p => ⟨this p, this p.symm⟩
  fun l₁ l₂ p d => by
  induction' d with a l₁ h d IH generalizing l₂
  · rw [← p.nil_eq]
    constructor
    
  · have : a ∈ l₂ := p.subset (mem_cons_self _ _)
    rcases mem_split this with ⟨s₂, t₂, rfl⟩
    have p' := (p.trans perm_middle).cons_inv
    refine' (pairwise_middle S).2 (pairwise_cons.2 ⟨fun b m => _, IH _ p'⟩)
    exact h _ (p'.symm.subset m)
```
amended to:
```
theorem Perm.pairwise_iff {R : α → α → Prop} (S : symmetric R) :
  ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → (Pairwise R l₁ ↔ Pairwise R l₂) := by
  suffices ∀ {l₁ l₂}, l₁ ~ l₂ → Pairwise R l₁ → Pairwise R l₂ from
    fun l₁ l₂ p => ⟨this p, this p.symm⟩
  intros l₁ l₂ p d
  induction d generalizing l₂ with
  | nil =>
    rw [←p.nil_eq]
    constructor
  | @cons a h d _ ih =>
    have : a ∈ l₂ := p.subset (mem_cons_self _ _)
    rcases mem_split this with ⟨s₂, t₂, rfl⟩
    have p' := (p.trans perm_middle).cons_inv
    refine' (pairwise_middle S).2 (Pairwise_cons.2 ⟨_, ih p'⟩)
    intro b m
    exact d _ (p'.symm.subset m)
```

Changes:
* `refine'` doesn't behave as it used to in Lean3 with `fun b m => _`: we get the goal `∀ (b : α), b ∈ s₂ ++ t₂ → R a b`,
  whereas we might hope that `intro b m` has already been achieved.

---

Mathport suggests:
```
def Multiset.{u} (α : Type u) : Type u :=
  Quotientₓ (List.isSetoid α)
```
amended to:
```
def Multiset.{u} (α : Type u) : Type u :=
  Quotient (List.instSetoidList α)
```
 
Changes:
* Incorrect instance name.

---

Mathport suggests:
```
def Nodup (s : Multiset α) : Prop :=
  Quot.liftOn s Nodupₓ fun s t p => propext p.nodup_iff
```
amended to:
```
def Nodup (s : Multiset α) : Prop :=
  Quot.liftOn s List.Nodup fun _ _ p => propext p.nodup_iff
```

Changes:
* `Nodupₓ` to `List.Nodup`, to avoid self-reference.
* Replace `fun s t p` with `fun _ _ p` to satisfy the unused variable linter.