awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
α : Fin 2 → Type u
s : Set (α 0)
t : Set (α 1)
h :
  ∀ (f : (i : Fin 2) → α i),
    Membership.mem (γ := Set ((i : Fin 2) → α i)) ((fun (f : (i : Fin 2) → α i) ↦ (f 0, f 1)) ⁻¹' s ×ˢ t) f ↔
      Membership.mem (γ := Set ((i : Fin 2) → α i))
        (Set.pi (α := α) Set.univ
          (cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ Set (α i)) s
            (cons (α := fun (i : Fin 1) ↦ Set (α i.succ)) t
              (finZeroElim (α := fun (i : Fin 0) ↦ Set (α i.succ.succ))))))
        f
⊢ Eq (α := Set ((i : Fin 2) → α i)) ((fun (f : (i : Fin 2) → α i) ↦ (f 0, f 1)) ⁻¹' s ×ˢ t)
    (Set.pi (α := α) Set.univ
      (cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ Set (α i)) s
        (cons (α := fun (i : Fin 1) ↦ Set (α i.succ)) t (finZeroElim (α := fun (i : Fin 0) ↦ Set (α i.succ.succ))))))

Tactic:
ext f
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
α : Fin 2 → Type u
s : Set (α 0)
t : Set (α 1)
f : (i : Fin 2) → α i
⊢ Membership.mem (γ := Set ((i : Fin 2) → α i)) ((fun (f : (i : Fin 2) → α i) ↦ (f 0, f 1)) ⁻¹' s ×ˢ t) f ↔
    Membership.mem (γ := Set ((i : Fin 2) → α i))
      (Set.pi (α := α) Set.univ
        (cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ Set (α i)) s
          (cons (α := fun (i : Fin 1) ↦ Set (α i.succ)) t (finZeroElim (α := fun (i : Fin 0) ↦ Set (α i.succ.succ))))))
      f

Tactic:
simp [Fin.forall_fin_two]

Premises used: Fin.forall_fin_two
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
α : Type u
s t : Set α
⊢ (fun (f : Fin 2 → α) ↦ (f 0, f 1)) ⁻¹' s ×ˢ t = Set.pi (α := fun (a : Fin (Nat.succ 0).succ) ↦ α) Set.univ ![s, t]

Tactic:
@Fin.preimage_apply_01_prod (fun _ => α) s t

Premises used: Fin.preimage_apply_01_prod, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
i x : Fin (n + 1)
⊢ (fun (x : Option (Fin n)) ↦ x.casesOn' i i.succAbove)
      (i.insertNth (α := fun (a : Fin (n + 1)) ↦ Option (Fin n)) none some i) =
    i

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
i x : Fin (n + 1)
j : Fin n
⊢ (fun (x : Option (Fin n)) ↦ x.casesOn' i i.succAbove)
      (i.insertNth (α := fun (a : Fin (n + 1)) ↦ Option (Fin n)) none some (i.succAbove j)) =
    i.succAbove j

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
i : Fin (n + 1)
x : Option (Fin n)
none :
  Eq (α := Option (Fin n))
    (i.insertNth (α := fun (a : Fin (n + 1)) ↦ Option (Fin n)) Option.none Option.some
        ((fun (x : Option (Fin n)) ↦ x.casesOn' i i.succAbove) Option.none) :
      Option (Fin n))
    Option.none
some :
  ∀ (val : Fin n),
    i.insertNth (α := fun (a : Fin (n + 1)) ↦ Option (Fin n)) Option.none Option.some
        ((fun (x : Option (Fin n)) ↦ x.casesOn' i i.succAbove) (Option.some val)) =
      Option.some val
⊢ i.insertNth (α := fun (a : Fin (n + 1)) ↦ Option (Fin n)) Option.none Option.some
      ((fun (x : Option (Fin n)) ↦ x.casesOn' i i.succAbove) x) =
    x

Tactic:
cases x
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
i : Fin (n + 1)
⊢ Eq (α := Option (Fin n))
    (i.insertNth (α := fun (a : Fin (n + 1)) ↦ Option (Fin n)) none some
        ((fun (x : Option (Fin n)) ↦ x.casesOn' i i.succAbove) none) :
      Option (Fin n))
    none

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
i : Fin (n + 1)
val : Fin n
⊢ i.insertNth (α := fun (a : Fin (n + 1)) ↦ Option (Fin n)) none some
      ((fun (x : Option (Fin n)) ↦ x.casesOn' i i.succAbove) (some val)) =
    some val

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Eq (α := Option (Fin n)) ((finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) i : Option (Fin n)) none

Tactic:
simp [finSuccEquiv']

Premises used: finSuccEquiv'
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) (i.succAbove j) = some j

Tactic:
@Fin.insertNth_apply_succAbove n (fun _ => Option (Fin n)) i _ _ _

Premises used: Fin.succAboveCases, Fin.insertNth_apply_succAbove, Fin.insertNth, dite
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : m.castSucc < i
rw : (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) (i.succAbove m) = some m
rw₁ rw₂ : some m = some m
⊢ (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) m.castSucc = some m

Tactic:
rw [← Fin.succAbove_of_castSucc_lt _ _ h, finSuccEquiv'_succAbove]

Premises used: Fin.succAbove_of_castSucc_lt, finSuccEquiv'_succAbove
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : i ≤ m.castSucc
rw : (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) (i.succAbove m) = some m
rw₁ rw₂ : some m = some m
⊢ (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) m.succ = some m

Tactic:
rw [← Fin.succAbove_of_le_castSucc _ _ h, finSuccEquiv'_succAbove]

Premises used: Fin.succAbove_of_le_castSucc, finSuccEquiv'_succAbove
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ ((finSuccEquiv' i).symm : (a : Option (Fin n)) → Fin (n + 1)) none = i

Tactic:
rfl

Premises used: Option.casesOn', rfl
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ ((finSuccEquiv' i).symm : (a : Option (Fin n)) → Fin (n + 1)) (some j) = i.succAbove j

Tactic:
rfl

Premises used: Fin.succAbove, Option.casesOn', rfl, ite
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
k : Fin n
⊢ (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) j = some k ↔ j = i.succAbove k

Tactic:
(finSuccEquiv' i).apply_eq_iff_eq_symm_apply

Premises used: Fin.succAbove, Option.casesOn', finSuccEquiv', ite, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
⊢ Eq (α := Option (Fin n)) ((finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) j : Option (Fin n)) none ↔ i = j

Tactic:
(finSuccEquiv' i).apply_eq_iff_eq_symm_apply.trans eq_comm

Premises used: eq_comm, Iff.trans, finSuccEquiv', Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : m.castSucc < i
⊢ ((finSuccEquiv' i).symm : (a : Option (Fin n)) → Fin (n + 1)) (some m) = m.castSucc

Tactic:
Fin.succAbove_of_castSucc_lt i m h

Premises used: Fin.succAbove, Option.casesOn', Fin.succAbove_of_castSucc_lt, ite
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : i ≤ m.castSucc
⊢ ((finSuccEquiv' i).symm : (a : Option (Fin n)) → Fin (n + 1)) (some m) = m.succ

Tactic:
Fin.succAbove_of_le_castSucc i m h

Premises used: Fin.succAbove_of_le_castSucc, Fin.succAbove, Option.casesOn', ite
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : m.castSucc < i
⊢ ((finSuccEquiv' i).symm : (a : Option (Fin n)) → Fin (n + 1)) (some m) = m.castSucc

Tactic:
finSuccEquiv'_symm_some_below h

Premises used: finSuccEquiv'_symm_some_below
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : i ≤ m.castSucc
⊢ ((finSuccEquiv' i).symm : (a : Option (Fin n)) → Fin (n + 1)) (some m) = m.succ

Tactic:
finSuccEquiv'_symm_some_above h

Premises used: finSuccEquiv'_symm_some_above
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
⊢ Eq (α := Option (Fin n)) ((finSuccEquiv n : (a : Fin (n + 1)) → Option (Fin n)) 0 : Option (Fin n))
    (none : Option (Fin n))

Tactic:
rfl

Premises used: Fin.succAboveCases, Fin.insertNth, dite, rfl
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
m : Fin n
⊢ (finSuccEquiv n : (a : Fin (n + 1)) → Option (Fin n)) m.succ = some m

Tactic:
finSuccEquiv'_above (Fin.zero_le _)

Premises used: Fin.zero_le, finSuccEquiv'_above
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
⊢ Eq (α := Fin (n + 1)) (((finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) none : Fin (n + 1))
    (0 : Fin (n + 1))

Tactic:
finSuccEquiv'_symm_none _

Premises used: finSuccEquiv'_symm_none
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
m : Fin n
⊢ ((finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) (some m) = m.succ

Tactic:
congr_fun Fin.succAbove_zero m

Premises used: Fin.succAbove, Fin.succ, Option.casesOn', congr_fun, Fin.succAbove_zero, ite
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ (finSuccEquiv n : (a : Fin (n + 1)) → Option (Fin n)) i = some j ↔ i = j.succ

Tactic:
(finSuccEquiv n).apply_eq_iff_eq_symm_apply

Premises used: Fin.succAbove, Fin.succ, Option.casesOn', finSuccEquiv, ite, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Eq (α := Option (Fin n)) ((finSuccEquiv n : (a : Fin (n + 1)) → Option (Fin n)) i : Option (Fin n)) none ↔ i = 0

Tactic:
(finSuccEquiv n).apply_eq_iff_eq_symm_apply

Premises used: Option.casesOn', Fin.ofNat, finSuccEquiv, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
⊢ finSuccEquiv' 0 = finSuccEquiv n

Tactic:
rfl

Premises used: finSuccEquiv, rfl
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin n
rw : (finSuccEquiv' (Fin.last n) : (a : Fin (n + 1)) → Option (Fin n)) ((Fin.last n).succAbove i) = some i
rw₁ rw₂ : some i = some i
⊢ (finSuccEquiv' (Fin.last n) : (a : Fin (n + 1)) → Option (Fin n)) i.castSucc = some i

Tactic:
rw [← Fin.succAbove_last, finSuccEquiv'_succAbove]

Premises used: Fin.succAbove_last, finSuccEquiv'_succAbove
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
h : i ≠ Fin.last n
⊢ (finSuccEquiv' (Fin.last n) : (a : Fin (n + 1)) → Option (Fin n)) i = some (i.castLT ⋯)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
hi : i ≠ Fin.last n
hj : j ≠ i
rcases :
  ∀ (j : Fin n) (hj : i.succAbove j ≠ i),
    (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) (i.succAbove j) =
      some ((i.castLT ⋯).predAbove (i.succAbove j))
⊢ (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) j = some ((i.castLT ⋯).predAbove j)

Tactic:
rcases Fin.exists_succAbove_eq hj with ⟨j, rfl⟩

Premises used: Fin.exists_succAbove_eq, rfl
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
hi : i ≠ Fin.last n
j : Fin n
hj : i.succAbove j ≠ i
rcases :
  ∀ (i : Fin n) (hi : i.castSucc ≠ Fin.last n) (hj : i.castSucc.succAbove j ≠ i.castSucc),
    (finSuccEquiv' i.castSucc : (a : Fin (n + 1)) → Option (Fin n)) (i.castSucc.succAbove j) =
      some ((i.castSucc.castLT ⋯).predAbove (i.castSucc.succAbove j))
⊢ (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) (i.succAbove j) = some ((i.castLT ⋯).predAbove (i.succAbove j))

Tactic:
rcases Fin.exists_castSucc_eq.2 hi with ⟨i, rfl⟩

Premises used: Iff.mpr, Fin.exists_castSucc_eq, rfl
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
j i : Fin n
hi : i.castSucc ≠ Fin.last n
hj : i.castSucc.succAbove j ≠ i.castSucc
⊢ (finSuccEquiv' i.castSucc : (a : Fin (n + 1)) → Option (Fin n)) (i.castSucc.succAbove j) =
    some ((i.castSucc.castLT ⋯).predAbove (i.castSucc.succAbove j))

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ Eq (α := { x : Fin (n + 1) // x ≠ p })
    ((finSuccAboveEquiv p : (a : Fin n) → { x : Fin (n + 1) // x ≠ p }) i : { x : Fin (n + 1) // x ≠ p })
    (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ≠ p) (p.succAbove i) ⋯ : { x : Fin (n + 1) // x ≠ p })

Tactic:
rfl

Premises used: Fin.succAbove, Option.casesOn', rfl, ite
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
x : { x : Fin (n + 1) // x ≠ Fin.last n }
rw :
  some (((finSuccAboveEquiv (Fin.last n)).symm : (a : { x : Fin (n + 1) // x ≠ Fin.last n }) → Fin n) x) =
    some ((↑x : Fin (n + 1)).castLT ⋯)
⊢ ((finSuccAboveEquiv (Fin.last n)).symm : (a : { x : Fin (n + 1) // x ≠ Fin.last n }) → Fin n) x =
    (↑x : Fin (n + 1)).castLT ⋯

Tactic:
rw [← Option.some_inj]

Premises used: Option.some_inj
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
x : { x : Fin (n + 1) // x ≠ Fin.last n }
⊢ some (((finSuccAboveEquiv (Fin.last n)).symm : (a : { x : Fin (n + 1) // x ≠ Fin.last n }) → Fin n) x) =
    some ((↑x : Fin (n + 1)).castLT ⋯)

Tactic:
simp [finSuccAboveEquiv]

Premises used: finSuccAboveEquiv
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x : Fin (n + 1) // x ≠ p }
rw :
  some (((finSuccAboveEquiv p).symm : (a : { x : Fin (n + 1) // x ≠ p }) → Fin n) x) =
    some ((p.castLT ⋯).predAbove (↑x : Fin (n + 1)))
⊢ ((finSuccAboveEquiv p).symm : (a : { x : Fin (n + 1) // x ≠ p }) → Fin n) x =
    (p.castLT ⋯).predAbove (↑x : Fin (n + 1))

Tactic:
rw [← Option.some_inj]

Premises used: Option.some_inj
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x : Fin (n + 1) // x ≠ p }
⊢ some (((finSuccAboveEquiv p).symm : (a : { x : Fin (n + 1) // x ≠ p }) → Fin n) x) =
    some ((p.castLT ⋯).predAbove (↑x : Fin (n + 1)))

Tactic:
simpa [finSuccAboveEquiv] using finSuccEquiv'_ne_last_apply h x.property

Premises used: finSuccEquiv'_ne_last_apply, finSuccAboveEquiv, Subtype.property
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin n
⊢ (finSuccEquivLast : (a : Fin (n + 1)) → Option (Fin n)) i.castSucc = some i

Tactic:
finSuccEquiv'_below i.2

Premises used: Fin.isLt, finSuccEquiv'_below
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
⊢ Eq (α := Option (Fin n)) ((finSuccEquivLast : (a : Fin (n + 1)) → Option (Fin n)) (Fin.last n) : Option (Fin n)) none

Tactic:
simp [finSuccEquivLast]

Premises used: finSuccEquivLast
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin n
⊢ (Equiv.symm finSuccEquivLast : (a : Option (Fin n)) → Fin (n + 1)) (some i) = i.castSucc

Tactic:
finSuccEquiv'_symm_some_below i.2

Premises used: Fin.isLt, finSuccEquiv'_symm_some_below
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
⊢ (Equiv.symm finSuccEquivLast : (a : Option (Fin n)) → Fin (n + 1)) none = Fin.last n

Tactic:
finSuccEquiv'_symm_none _

Premises used: finSuccEquiv'_symm_none
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
ι : Type u_1
e : Fin (n + 1) ↪ ι
⊢ Eq (α := (a : Fin n) → ι)
    (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦
          { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i })
          ((embeddingFinSucc n ι :
              (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // ¬i ∈ Set.range (⇑e : (a : Fin n) → ι) })
            e)) :
      (a : Fin n) → ι)
    ((⇑e : (a : Fin (n + 1)) → ι) ∘ Fin.succ)

Tactic:
rfl

Premises used: Fin.succAbove, Fin.succ, Option.casesOn', rfl, ite
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
ι : Type u_1
e : Fin (n + 1) ↪ ι
⊢ Eq (α := ι)
    ((↑(Sigma.snd (β := fun (e : Fin n ↪ ι) ↦
              { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i })
              ((embeddingFinSucc n ι :
                  (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // ¬i ∈ Set.range (⇑e : (a : Fin n) → ι) })
                e) :
            { i : ι //
              ¬Membership.mem (γ := Set ι)
                  (Set.range (ι := Fin n)
                    (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦
                          { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i })
                          ((embeddingFinSucc n ι :
                              (a : Fin (n + 1) ↪ ι) →
                                (e : Fin n ↪ ι) × { i : ι // ¬i ∈ Set.range (⇑e : (a : Fin n) → ι) })
                            e)) :
                      (a : Fin n) → ι))
                  i }) :
        ι) :
      ι)
    ((e : (a : Fin (n + 1)) → ι) 0 : ι)

Tactic:
rfl

Premises used: Option.casesOn', Fin.ofNat, rfl
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
ι : Type u_1
f : (e : Fin n ↪ ι) × { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i }
h :
  ∀ (i : Fin (n + 1)),
    Eq (α := ι)
      (((((embeddingFinSucc n ι).symm :
                  (a : (e : Fin n ↪ ι) × { i : ι // ¬i ∈ Set.range (⇑e : (a : Fin n) → ι) }) → Fin (n + 1) ↪ ι)
                f :
              Fin (n + 1) ↪ ι) :
            (a : Fin (n + 1)) → ι)
          i :
        ι)
      (Fin.cons (α := fun (i : Fin (n + 1)) ↦ ι)
          (↑(f.snd (β := fun (e : Fin n ↪ ι) ↦
                { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i })) :
            ι)
          (⇑(f.fst (β := fun (e : Fin n ↪ ι) ↦
                { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i })) :
            (a : Fin n) → ι)
          i :
        ι)
⊢ Eq (α := (a : Fin (n + 1)) → ι)
    (⇑(((embeddingFinSucc n ι).symm :
              (a : (e : Fin n ↪ ι) × { i : ι // ¬i ∈ Set.range (⇑e : (a : Fin n) → ι) }) → Fin (n + 1) ↪ ι)
            f :
          Fin (n + 1) ↪ ι) :
      (a : Fin (n + 1)) → ι)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ ι)
      (↑(f.snd (β := fun (e : Fin n ↪ ι) ↦
            { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i })) :
        ι)
      (⇑(f.fst (β := fun (e : Fin n ↪ ι) ↦
            { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i })) :
        (a : Fin n) → ι))

Tactic:
ext i
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
ι : Type u_1
f : (e : Fin n ↪ ι) × { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i }
i : Fin (n + 1)
⊢ Eq (α := ι)
    (((((embeddingFinSucc n ι).symm :
                (a : (e : Fin n ↪ ι) × { i : ι // ¬i ∈ Set.range (⇑e : (a : Fin n) → ι) }) → Fin (n + 1) ↪ ι)
              f :
            Fin (n + 1) ↪ ι) :
          (a : Fin (n + 1)) → ι)
        i :
      ι)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ ι)
        (↑(f.snd (β := fun (e : Fin n ↪ ι) ↦
              { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i })) :
          ι)
        (⇑(f.fst (β := fun (e : Fin n ↪ ι) ↦
              { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i })) :
          (a : Fin n) → ι)
        i :
      ι)

Tactic:
Fin.cases rfl (fun j ↦ rfl) i

Premises used: Fin.cases
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
ι : Type u_1
f : (e : Fin n ↪ ι) × { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i }
i : Fin (n + 1)
⊢ Eq (α := ι)
    (((((embeddingFinSucc n ι).symm :
                (a : (e : Fin n ↪ ι) × { i : ι // ¬i ∈ Set.range (⇑e : (a : Fin n) → ι) }) → Fin (n + 1) ↪ ι)
              f :
            Fin (n + 1) ↪ ι) :
          (a : Fin (n + 1)) → ι)
        i :
      ι)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ ι)
        (↑(f.snd (β := fun (e : Fin n ↪ ι) ↦
              { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i })) :
          ι)
        (⇑(f.fst (β := fun (e : Fin n ↪ ι) ↦
              { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (a : Fin n) → ι)) i })) :
          (a : Fin n) → ι)
        i :
      ι)

Tactic:
exact Fin.cases rfl (fun j ↦ rfl) i
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
x : Fin m ⊕ Fin n
inl :
  ∀ (y : Fin m),
    Eq (α := Fin m ⊕ Fin n)
      ((fun (i : Fin (m + n)) ↦
          (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
        (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inl y)))
      (Sum.inl y)
inr :
  ∀ (y : Fin n),
    Eq (α := Fin m ⊕ Fin n)
      ((fun (i : Fin (m + n)) ↦
          (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
        (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inr y)))
      (Sum.inr y)
⊢ (fun (i : Fin (m + n)) ↦
        (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
      (Sum.elim (Fin.castAdd n) (Fin.natAdd m) x) =
    x

Tactic:
rcases x with y | y
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
y : Fin m
⊢ Eq (α := Fin m ⊕ Fin n)
    ((fun (i : Fin (m + n)) ↦
        (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
      (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inl y)))
    (Sum.inl y)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
y : Fin n
⊢ Eq (α := Fin m ⊕ Fin n)
    ((fun (i : Fin (m + n)) ↦
        (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
      (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inr y)))
    (Sum.inr y)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
x : Fin (m + n)
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m)
      ((fun (i : Fin (m + n)) ↦
          (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
        x) =
    x

Tactic:
Fin.addCases (fun i => ?_) (fun i => ?_) x

Premises used: Fin.addCases
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
x : Fin (m + n)
refine_1 :
  ∀ (i : Fin m),
    Sum.elim (Fin.castAdd n) (Fin.natAdd m)
        ((fun (i : Fin (m + n)) ↦
            (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
          (Fin.castAdd n i)) =
      Fin.castAdd n i
refine_2 :
  ∀ (i : Fin n),
    Sum.elim (Fin.castAdd n) (Fin.natAdd m)
        ((fun (i : Fin (m + n)) ↦
            (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
          (Fin.natAdd m i)) =
      Fin.natAdd m i
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m)
      ((fun (i : Fin (m + n)) ↦
          (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
        x) =
    x

Tactic:
refine Fin.addCases (fun i => ?_) (fun i => ?_) x
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
x : Fin (m + n)
i : Fin m
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m)
      ((fun (i : Fin (m + n)) ↦
          (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
        (Fin.castAdd n i)) =
    Fin.castAdd n i

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
x : Fin (m + n)
i : Fin n
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m)
      ((fun (i : Fin (m + n)) ↦
          (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ Fin m ⊕ Fin n) Sum.inl Sum.inr i : Fin m ⊕ Fin n))
        (Fin.natAdd m i)) =
    Fin.natAdd m i

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
i : Fin m
⊢ (finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n)) (Sum.inl i) = Fin.castAdd n i

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
i : Fin n
⊢ (finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n)) (Sum.inr i) = Fin.natAdd m i

Tactic:
rfl

Premises used: Fin.natAdd, rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
x : Fin m
⊢ Eq (α := Fin m ⊕ Fin n)
    ((Equiv.symm finSumFinEquiv : (a : Fin (m + n)) → Fin m ⊕ Fin n) (Fin.castAdd n x) : Fin m ⊕ Fin n)
    (Sum.inl x : Fin m ⊕ Fin n)

Tactic:
finSumFinEquiv.symm_apply_apply (Sum.inl x)

Premises used: Equiv.symm_apply_apply, Sum.inl, finSumFinEquiv, Sum.elim
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m : ℕ
x : Fin m
⊢ Eq (α := Fin m ⊕ Fin 1) ((Equiv.symm finSumFinEquiv : (a : Fin (m + 1)) → Fin m ⊕ Fin 1) x.castSucc : Fin m ⊕ Fin 1)
    (Sum.inl x : Fin m ⊕ Fin 1)

Tactic:
finSumFinEquiv_symm_apply_castAdd x

Premises used: finSumFinEquiv_symm_apply_castAdd
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
x : Fin n
⊢ Eq (α := Fin m ⊕ Fin n)
    ((Equiv.symm finSumFinEquiv : (a : Fin (m + n)) → Fin m ⊕ Fin n) (Fin.natAdd m x) : Fin m ⊕ Fin n)
    (Sum.inr x : Fin m ⊕ Fin n)

Tactic:
finSumFinEquiv.symm_apply_apply (Sum.inr x)

Premises used: Fin.natAdd, Equiv.symm_apply_apply, Sum.inr, finSumFinEquiv, Sum.elim
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
⊢ Eq (α := Fin n ⊕ Fin 1) ((Equiv.symm finSumFinEquiv : (a : Fin (n + 1)) → Fin n ⊕ Fin 1) (Fin.last n) : Fin n ⊕ Fin 1)
    (Sum.inr 0 : Fin n ⊕ Fin 1)

Tactic:
finSumFinEquiv_symm_apply_natAdd 0

Premises used: finSumFinEquiv_symm_apply_natAdd, OfNat.ofNat
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin n
⊢ (finSumNatEquiv n : (a : Fin n ⊕ ℕ) → ℕ) (Sum.inl i) = (↑i : ℕ)

Tactic:
rfl

Premises used: rfl, Sum.elim