awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α ↪ γ
f : β ↪ γ
h :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ)) ↔
    Subset.{u_3} (α := Set γ) (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ))
      (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))ᶜ
h₁ :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ)) ↔
    Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ))
      (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))
⊢ Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ)) ↔
    ∀ (a_1 : β),
      Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))ᶜ
        ((f : (a : β) → γ) a_1 : γ)
have h₂ : Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ))
    (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ)) ↔
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ))
    (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))
Tactic: rw [← Set.range_subset_iff, Set.subset_compl_iff_disjoint_right, disjoint_comm]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Unique α
x : α ↪ β
⊢ (fun (x : β) ↦ ({ toFun := fun (x_1 : α) ↦ x, inj' := ⋯ } : α ↪ β))
      ((fun (f : α ↪ β) ↦ ((f : (a : α) → β) default : β)) x) =
    x
have h : ∀ (x_1 : α),
  Eq.{u_2 + 1} (α := β)
    (((fun (x : β) ↦ ({ toFun := fun (x_2 : α) ↦ x, inj' := sorry } : α ↪ β))
            ((fun (f : α ↪ β) ↦ ((f : (a : α) → β) default : β)) x) :
          (a : α) → β)
        x_1 :
      β)
    ((x : (a : α) → β) x_1 : β)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Unique α
x_1 : α ↪ β
x : α
⊢ Eq.{u_2 + 1} (α := β)
    (((fun (x : β) ↦ ({ toFun := fun (x_2 : α) ↦ x, inj' := ⋯ } : α ↪ β))
            ((fun (f : α ↪ β) ↦ ((f : (a : α) → β) default : β)) x_1) :
          (a : α) → β)
        x :
      β)
    ((x_1 : (a : α) → β) x : β)
have h : Eq.{u_2 + 1} (α := β) ((x_1 : (a : α) → β) default : β) ((x_1 : (a : α) → β) x : β)
Tactic: simp_rw [Function.Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Unique α
x_1 : α ↪ β
x : α
⊢ Eq.{u_2 + 1} (α := β) ((x_1 : (a : α) → β) default : β) ((x_1 : (a : α) → β) x : β)
have h : default = x
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
α : Fin 2 → Type u
s : Set (α 0)
t : Set (α 1)
⊢ 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))))))
have 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
Tactic: ext f
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n : ℕ
i : Fin (n + 1)
x : 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) x) =
    x
have none : 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: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
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 some
        ((fun (x : Option (Fin n)) ↦ x.casesOn' i i.succAbove) Option.none) :
      Option (Fin n))
    Option.none
⊢ i.insertNth (α := fun (a : Fin (n + 1)) ↦ Option (Fin n)) Option.none some
      ((fun (x : Option (Fin n)) ↦ x.casesOn' i i.succAbove) x) =
    x
have some : ∀ (val : Fin n),
  i.insertNth (α := fun (a : Fin (n + 1)) ↦ Option (Fin n)) Option.none some
      ((fun (x : Option (Fin n)) ↦ x.casesOn' i i.succAbove) (some val)) =
    some val
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : m.castSucc < i
⊢ (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) m.castSucc = some m
have rw : (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) (i.succAbove m) = some m
Tactic: rw [← Fin.succAbove_of_castSucc_lt _ _ h, finSuccEquiv'_succAbove]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
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
⊢ (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) m.castSucc = some m
have rw₁ : some m = some m
Tactic: rw [← Fin.succAbove_of_castSucc_lt _ _ h, finSuccEquiv'_succAbove]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : i ≤ m.castSucc
⊢ (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) m.succ = some m
have rw : (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) (i.succAbove m) = some m
Tactic: rw [← Fin.succAbove_of_le_castSucc _ _ h, finSuccEquiv'_succAbove]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
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
⊢ (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) m.succ = some m
have rw₁ : some m = some m
Tactic: rw [← Fin.succAbove_of_le_castSucc _ _ h, finSuccEquiv'_succAbove]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin n
⊢ (finSuccEquiv' (Fin.last n) : (a : Fin (n + 1)) → Option (Fin n)) i.castSucc = some i
have rw : (finSuccEquiv' (Fin.last n) : (a : Fin (n + 1)) → Option (Fin n)) ((Fin.last n).succAbove i) = some i
Tactic: rw [← Fin.succAbove_last, finSuccEquiv'_succAbove]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin n
rw : (finSuccEquiv' (Fin.last n) : (a : Fin (n + 1)) → Option (Fin n)) ((Fin.last n).succAbove i) = some i
⊢ (finSuccEquiv' (Fin.last n) : (a : Fin (n + 1)) → Option (Fin n)) i.castSucc = some i
have rw₁ : some i = some i
Tactic: rw [← Fin.succAbove_last, finSuccEquiv'_succAbove]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hi : i ≠ Fin.last n
hj : j ≠ i
⊢ (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) j = some ((i.castLT ⋯).predAbove j)
have rcases : ∀ (j : Fin n) (hj : i.succAbove j ≠ i),
  (finSuccEquiv' i : (a : Fin (n + 1)) → Option (Fin n)) (i.succAbove j) = some ((i.castLT sorry).predAbove (i.succAbove j))
Tactic: rcases Fin.exists_succAbove_eq hj with ⟨j, rfl⟩
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
hi : i ≠ Fin.last n
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))
have 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 sorry).predAbove (i.castSucc.succAbove j))
Tactic: rcases Fin.exists_castSucc_eq.2 hi with ⟨i, rfl⟩
Cleared hypotheses: i, hi, hj
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n : ℕ
x : { x : Fin (n + 1) // x ≠ Fin.last n }
⊢ ((finSuccAboveEquiv (Fin.last n)).symm : (a : { x : Fin (n + 1) // x ≠ Fin.last n }) → Fin n) x =
    (↑x : Fin (n + 1)).castLT ⋯
have 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 sorry)
Tactic: rw [← Option.some_inj]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x : Fin (n + 1) // x ≠ p }
⊢ ((finSuccAboveEquiv p).symm : (a : { x : Fin (n + 1) // x ≠ p }) → Fin n) x =
    (p.castLT ⋯).predAbove (↑x : Fin (n + 1))
have rw : some (((finSuccAboveEquiv p).symm : (a : { x : Fin (n + 1) // x ≠ p }) → Fin n) x) =
  some ((p.castLT sorry).predAbove (↑x : Fin (n + 1)))
Tactic: rw [← Option.some_inj]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n : ℕ
ι : Type u_1
f : (e : Fin n ↪ ι) × { i : ι // ¬Membership.mem (γ := Set ι) (Set.range (ι := Fin n) (⇑e : (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) → ι))
have 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 :
      ι)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n : ℕ
x : 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) x) =
    x
have 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)
Tactic: rcases x with y | y
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
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)
⊢ (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
have 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)
Tactic: rcases x with y | y
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
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
have 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
Tactic: refine Fin.addCases (fun i => ?_) (fun i => ?_) x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
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
⊢ 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
have 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
Tactic: refine Fin.addCases (fun i => ?_) (fun i => ?_) x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n i : ℕ
⊢ Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)
have inl : ∀ (hi : i < n), Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)
Tactic: rcases i.lt_or_ge n with hi | hi
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n i : ℕ
inl :
  ∀ (hi : i < n), Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)
⊢ Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)
have inr : ∀ (hi : i ≥ n), Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)
Tactic: rcases i.lt_or_ge n with hi | hi
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n i : ℕ
hi : i < n
⊢ Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)
have inl : Sum.isLeft (β := ℕ) (Sum.inl (⟨i, hi⟩ : Fin n)) = decide (i < n)
Tactic: simp_rw [finSumNatEquiv_symm_apply_of_lt hi, hi, Sum.isLeft_inl, decide_true]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n i : ℕ
hi : i < n
inl : Sum.isLeft (β := ℕ) (Sum.inl (⟨i, hi⟩ : Fin n)) = decide (i < n)
⊢ Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)
have inl₁ : Sum.isLeft (β := ℕ) (Sum.inl (⟨i, hi⟩ : Fin n)) = decide True
Tactic: simp_rw [finSumNatEquiv_symm_apply_of_lt hi, hi, Sum.isLeft_inl, decide_true]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n i : ℕ
hi : i < n
inl : Sum.isLeft (β := ℕ) (Sum.inl (⟨i, hi⟩ : Fin n)) = decide (i < n)
inl₁ : Sum.isLeft (β := ℕ) (Sum.inl (⟨i, hi⟩ : Fin n)) = decide True
⊢ Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)
have inl₂ : true = decide True
Tactic: simp_rw [finSumNatEquiv_symm_apply_of_lt hi, hi, Sum.isLeft_inl, decide_true]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n i : ℕ
hi : i ≥ n
⊢ Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)
have inr : Sum.isLeft (α := Fin n) (Sum.inr (i - n)) = decide (i < n)
Tactic: simp_rw [finSumNatEquiv_symm_apply_of_ge hi, hi.not_gt, Sum.isLeft_inr, decide_false]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n i : ℕ
hi : i ≥ n
inr : Sum.isLeft (α := Fin n) (Sum.inr (i - n)) = decide (i < n)
⊢ Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)
have inr₁ : Sum.isLeft (α := Fin n) (Sum.inr (i - n)) = decide False
Tactic: simp_rw [finSumNatEquiv_symm_apply_of_ge hi, hi.not_gt, Sum.isLeft_inr, decide_false]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n i : ℕ
hi : i ≥ n
inr : Sum.isLeft (α := Fin n) (Sum.inr (i - n)) = decide (i < n)
inr₁ : Sum.isLeft (α := Fin n) (Sum.inr (i - n)) = decide False
⊢ Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)
have inr₂ : false = decide False
Tactic: simp_rw [finSumNatEquiv_symm_apply_of_ge hi, hi.not_gt, Sum.isLeft_inr, decide_false]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n i : ℕ
⊢ Sum.isRight (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (n ≤ i)
have simp_rw : Sum.isRight (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) =
  !Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i)
Tactic: simp_rw [← not_lt, decide_not, ← isLeft_finSumNatEquiv_symm_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n i : ℕ
⊢ Sum.isRight (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) =
    !Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i)
have inl : ∀ (val : Fin n), Sum.isRight (β := ℕ) (Sum.inl val) = !Sum.isLeft (β := ℕ) (Sum.inl val)
Tactic: cases (finSumNatEquiv n).symm i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
n i : ℕ
inl : ∀ (val : Fin n), Sum.isRight (β := ℕ) (Sum.inl val) = !Sum.isLeft (β := ℕ) (Sum.inl val)
⊢ Sum.isRight (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) =
    !Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i)
have inr : ∀ (val : ℕ), Sum.isRight (α := Fin n) (Sum.inr val) = !Sum.isLeft (α := Fin n) (Sum.inr val)
Tactic: cases (finSumNatEquiv n).symm i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ (finAddFlip : (a : Fin (m + n)) → Fin (n + m)) ⟨k, h₂⟩ = (⟨k - m, ⋯⟩ : Fin (n + m))
have h : k = (↑(Fin.natAdd m (⟨k - m, sorry⟩ : Fin n)) : ℕ)
Tactic: convert! @finAddFlip_apply_natAdd n ⟨k - m, by lia⟩ m
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n : ℕ
x_1 : Fin m × Fin n
x : Fin m
y : Fin n
H : 0 < n
⊢ (↑y : ℕ) / n + (↑x : ℕ) = 0 + (↑x : ℕ)
have rw : 0 + (↑x : ℕ) = 0 + (↑x : ℕ)
Tactic: rw [Nat.div_eq_of_lt y.2]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n_1 n : ℕ
inst : NeZero n
p : ℕ × Fin n
⊢ (fun (a : ℕ) ↦ (a / n, Fin.ofNat n a)) ((fun (p : ℕ × Fin n) ↦ p.1 * n + (↑p.2 : ℕ)) p) = p
have refine : ((fun (a : ℕ) ↦ (a / n, Fin.ofNat n a)) ((fun (p : ℕ × Fin n) ↦ p.1 * n + (↑p.2 : ℕ)) p)).1 = p.1
Tactic: refine Prod.ext ?_ (Fin.ext <| Nat.mul_add_mod_of_lt p.2.is_lt)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n_1 n : ℕ
inst : NeZero n
p : ℕ × Fin n
⊢ (p.1 * n + (↑p.2 : ℕ)) / n = p.1
have rw : ((↑p.2 : ℕ) + p.1 * n) / n = p.1
Tactic: rw [Nat.add_comm, Nat.add_mul_div_right _ _ n.pos_of_neZero, Nat.div_eq_of_lt p.2.is_lt,
      Nat.zero_add]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n_1 n : ℕ
inst : NeZero n
p : ℕ × Fin n
rw : ((↑p.2 : ℕ) + p.1 * n) / n = p.1
⊢ (p.1 * n + (↑p.2 : ℕ)) / n = p.1
have rw₁ : (↑p.2 : ℕ) / n + p.1 = p.1
Tactic: rw [Nat.add_comm, Nat.add_mul_div_right _ _ n.pos_of_neZero, Nat.div_eq_of_lt p.2.is_lt,
      Nat.zero_add]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n_1 n : ℕ
inst : NeZero n
p : ℕ × Fin n
rw : ((↑p.2 : ℕ) + p.1 * n) / n = p.1
rw₁ : (↑p.2 : ℕ) / n + p.1 = p.1
⊢ (p.1 * n + (↑p.2 : ℕ)) / n = p.1
have rw₂ : 0 + p.1 = p.1
Tactic: rw [Nat.add_comm, Nat.add_mul_div_right _ _ n.pos_of_neZero, Nat.div_eq_of_lt p.2.is_lt,
      Nat.zero_add]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n_1 n : ℕ
inst : NeZero n
p : ℕ × Fin n
rw : ((↑p.2 : ℕ) + p.1 * n) / n = p.1
rw₁ : (↑p.2 : ℕ) / n + p.1 = p.1
rw₂ : 0 + p.1 = p.1
⊢ (p.1 * n + (↑p.2 : ℕ)) / n = p.1
have rw₃ : p.1 = p.1
Tactic: rw [Nat.add_comm, Nat.add_mul_div_right _ _ n.pos_of_neZero, Nat.div_eq_of_lt p.2.is_lt,
      Nat.zero_add]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n_1 n : ℕ
inst : NeZero n
a : ℤ
⊢ (fun (p : ℤ × Fin n) ↦ p.1 * (↑n : ℤ) + (↑(↑p.2 : ℕ) : ℤ))
      ((fun (a : ℤ) ↦ (a / (↑n : ℤ), Fin.ofNat n (a.natMod (↑n : ℤ)))) a) =
    a
have simp_rw : a / (↑n : ℤ) * (↑n : ℤ) + (↑(↑(Fin.ofNat n (a.natMod (↑n : ℤ))) : ℕ) : ℤ) = a
Tactic: simp_rw [Fin.val_ofNat, natCast_mod, natMod,
      toNat_of_nonneg (emod_nonneg _ <| natCast_eq_zero.not.2 (NeZero.ne n)), emod_emod,
      ediv_mul_add_emod]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n_1 n : ℕ
inst : NeZero n
a : ℤ
simp_rw simp_rw₁ : a / (↑n : ℤ) * (↑n : ℤ) + (↑(↑(Fin.ofNat n (a.natMod (↑n : ℤ))) : ℕ) : ℤ) = a
⊢ (fun (p : ℤ × Fin n) ↦ p.1 * (↑n : ℤ) + (↑(↑p.2 : ℕ) : ℤ))
      ((fun (a : ℤ) ↦ (a / (↑n : ℤ), Fin.ofNat n (a.natMod (↑n : ℤ)))) a) =
    a
have simp_rw₂ : a / (↑n : ℤ) * (↑n : ℤ) + (↑(a.natMod (↑n : ℤ) % n) : ℤ) = a
Tactic: simp_rw [Fin.val_ofNat, natCast_mod, natMod,
      toNat_of_nonneg (emod_nonneg _ <| natCast_eq_zero.not.2 (NeZero.ne n)), emod_emod,
      ediv_mul_add_emod]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n_1 n : ℕ
inst : NeZero n
a : ℤ
simp_rw simp_rw₁ : a / (↑n : ℤ) * (↑n : ℤ) + (↑(↑(Fin.ofNat n (a.natMod (↑n : ℤ))) : ℕ) : ℤ) = a
simp_rw₂ : a / (↑n : ℤ) * (↑n : ℤ) + (↑(a.natMod (↑n : ℤ) % n) : ℤ) = a
⊢ (fun (p : ℤ × Fin n) ↦ p.1 * (↑n : ℤ) + (↑(↑p.2 : ℕ) : ℤ))
      ((fun (a : ℤ) ↦ (a / (↑n : ℤ), Fin.ofNat n (a.natMod (↑n : ℤ)))) a) =
    a
have simp_rw₃ : a / (↑n : ℤ) * (↑n : ℤ) + HMod.hMod (α := ℤ) (↑(a.natMod (↑n : ℤ)) : ℤ) (↑n : ℤ) = a
Tactic: simp_rw [Fin.val_ofNat, natCast_mod, natMod,
      toNat_of_nonneg (emod_nonneg _ <| natCast_eq_zero.not.2 (NeZero.ne n)), emod_emod,
      ediv_mul_add_emod]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n_1 n : ℕ
inst : NeZero n
a : ℤ
simp_rw simp_rw₁ : a / (↑n : ℤ) * (↑n : ℤ) + (↑(↑(Fin.ofNat n (a.natMod (↑n : ℤ))) : ℕ) : ℤ) = a
simp_rw₂ : a / (↑n : ℤ) * (↑n : ℤ) + (↑(a.natMod (↑n : ℤ) % n) : ℤ) = a
simp_rw₃ : a / (↑n : ℤ) * (↑n : ℤ) + HMod.hMod (α := ℤ) (↑(a.natMod (↑n : ℤ)) : ℤ) (↑n : ℤ) = a
⊢ (fun (p : ℤ × Fin n) ↦ p.1 * (↑n : ℤ) + (↑(↑p.2 : ℕ) : ℤ))
      ((fun (a : ℤ) ↦ (a / (↑n : ℤ), Fin.ofNat n (a.natMod (↑n : ℤ)))) a) =
    a
have simp_rw₄ : a / (↑n : ℤ) * (↑n : ℤ) + HMod.hMod (α := ℤ) (↑(a % (↑n : ℤ)).toNat : ℤ) (↑n : ℤ) = a
Tactic: simp_rw [Fin.val_ofNat, natCast_mod, natMod,
      toNat_of_nonneg (emod_nonneg _ <| natCast_eq_zero.not.2 (NeZero.ne n)), emod_emod,
      ediv_mul_add_emod]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Basic (goal)
Goal:
m n_1 n : ℕ
inst : NeZero n
a : ℤ
simp_rw simp_rw₁ : a / (↑n : ℤ) * (↑n : ℤ) + (↑(↑(Fin.ofNat n (a.natMod (↑n : ℤ))) : ℕ) : ℤ) = a
simp_rw₂ : a / (↑n : ℤ) * (↑n : ℤ) + (↑(a.natMod (↑n : ℤ) % n) : ℤ) = a
simp_rw₃ : a / (↑n : ℤ) * (↑n : ℤ) + HMod.hMod (α := ℤ) (↑(a.natMod (↑n : ℤ)) : ℤ) (↑n : ℤ) = a
simp_rw₄ : a / (↑n : ℤ) * (↑n : ℤ) + HMod.hMod (α := ℤ) (↑(a % (↑n : ℤ)).toNat : ℤ) (↑n : ℤ) = a
⊢ (fun (p : ℤ × Fin n) ↦ p.1 * (↑n : ℤ) + (↑(↑p.2 : ℕ) : ℤ))
      ((fun (a : ℤ) ↦ (a / (↑n : ℤ), Fin.ofNat n (a.natMod (↑n : ℤ)))) a) =
    a
have simp_rw₅ : a / (↑n : ℤ) * (↑n : ℤ) + a % (↑n : ℤ) % (↑n : ℤ) = a
Tactic: simp_rw [Fin.val_ofNat, natCast_mod, natMod,
      toNat_of_nonneg (emod_nonneg _ <| natCast_eq_zero.not.2 (NeZero.ne n)), emod_emod,
      ediv_mul_add_emod]