awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
⊢ TendstoCofinite (α := α →₀ ℕ) (mapDomain f)
have refine : ∀ (x : β →₀ ℕ), Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
Tactic: classical
  refine (tendstoCofinite_iff_finite_preimage_singleton _).mpr fun x ↦ ?_
  let s := Finset.sup x.support (fun t ↦ (TendstoCofinite.finite_preimage_singleton f t).toFinset)
  let e : s ↪ α := Function.Embedding.subtype (fun u ↦ u ∈ s)
  refine Set.Finite.subset (Set.Finite.image (embDomain e) <| finite_of_degree_le (degree x)) ?_
  simp only [Set.subset_def, Set.mem_preimage, Set.mem_singleton_iff, Set.mem_image,
    Set.mem_setOf_eq]
  refine fun y hy ↦ ⟨y.comapDomain e e.injective.injOn, ?_, embDomain_comapDomain ?_⟩
  · rw [← hy, degree_mapDomain]
    exact degree_comapDomain_le_of_canonicallyOrderedAdd ..
  · suffices y.support ⊆ s by simpa [e]
    simpa [← hy, mapDomain, sum, Finset.subset_iff, single_apply, s] using
      fun i hi ↦ ⟨i, by simp [hi]⟩
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
refine : ∀ (x : β →₀ ℕ), Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
refine₁ refine₂ : ∀ (x : β →₀ ℕ), Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
⊢ TendstoCofinite (α := α →₀ ℕ) (mapDomain f)
have refine₃ : ∀ (x : β →₀ ℕ),
  let s : Finset α := x.support.sup fun (t : β) ↦ sorry.toFinset (s := f ⁻¹' {t});
  let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
  Subset (α := Set (α →₀ ℕ)) (mapDomain f ⁻¹' {x})
    (embDomain e ''
      {f : ↥s →₀ ℕ | LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) f : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)})
Tactic: classical
  refine (tendstoCofinite_iff_finite_preimage_singleton _).mpr fun x ↦ ?_
  let s := Finset.sup x.support (fun t ↦ (TendstoCofinite.finite_preimage_singleton f t).toFinset)
  let e : s ↪ α := Function.Embedding.subtype (fun u ↦ u ∈ s)
  refine Set.Finite.subset (Set.Finite.image (embDomain e) <| finite_of_degree_le (degree x)) ?_
  simp only [Set.subset_def, Set.mem_preimage, Set.mem_singleton_iff, Set.mem_image,
    Set.mem_setOf_eq]
  refine fun y hy ↦ ⟨y.comapDomain e e.injective.injOn, ?_, embDomain_comapDomain ?_⟩
  · rw [← hy, degree_mapDomain]
    exact degree_comapDomain_le_of_canonicallyOrderedAdd ..
  · suffices y.support ⊆ s by simpa [e]
    simpa [← hy, mapDomain, sum, Finset.subset_iff, single_apply, s] using
      fun i hi ↦ ⟨i, by simp [hi]⟩
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
refine : ∀ (x : β →₀ ℕ), Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
refine₁ refine₂ : ∀ (x : β →₀ ℕ), Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
refine₃ :
  ∀ (x : β →₀ ℕ),
    let s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t});
    let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
    Subset (α := Set (α →₀ ℕ)) (mapDomain f ⁻¹' {x})
      (embDomain e ''
        {f : ↥s →₀ ℕ | LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) f : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)})
⊢ TendstoCofinite (α := α →₀ ℕ) (mapDomain f)
have refine₄ : ∀ (x : β →₀ ℕ),
  let s : Finset α := x.support.sup fun (t : β) ↦ sorry.toFinset (s := f ⁻¹' {t});
  let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
  ∀ (x_1 : α →₀ ℕ),
    mapDomain f x_1 = x →
      ∃ (x_2 : ↥s →₀ ℕ),
        LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) x_2 : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ) ∧
          embDomain e x_2 = x_1
Tactic: classical
  refine (tendstoCofinite_iff_finite_preimage_singleton _).mpr fun x ↦ ?_
  let s := Finset.sup x.support (fun t ↦ (TendstoCofinite.finite_preimage_singleton f t).toFinset)
  let e : s ↪ α := Function.Embedding.subtype (fun u ↦ u ∈ s)
  refine Set.Finite.subset (Set.Finite.image (embDomain e) <| finite_of_degree_le (degree x)) ?_
  simp only [Set.subset_def, Set.mem_preimage, Set.mem_singleton_iff, Set.mem_image,
    Set.mem_setOf_eq]
  refine fun y hy ↦ ⟨y.comapDomain e e.injective.injOn, ?_, embDomain_comapDomain ?_⟩
  · rw [← hy, degree_mapDomain]
    exact degree_comapDomain_le_of_canonicallyOrderedAdd ..
  · suffices y.support ⊆ s by simpa [e]
    simpa [← hy, mapDomain, sum, Finset.subset_iff, single_apply, s] using
      fun i hi ↦ ⟨i, by simp [hi]⟩
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
refine : ∀ (x : β →₀ ℕ), Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
refine₁ refine₂ : ∀ (x : β →₀ ℕ), Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
refine₃ :
  ∀ (x : β →₀ ℕ),
    let s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t});
    let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
    Subset (α := Set (α →₀ ℕ)) (mapDomain f ⁻¹' {x})
      (embDomain e ''
        {f : ↥s →₀ ℕ | LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) f : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)})
refine₄ :
  ∀ (x : β →₀ ℕ),
    let s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t});
    let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
    ∀ (x_1 : α →₀ ℕ),
      mapDomain f x_1 = x →
        ∃ (x_2 : ↥s →₀ ℕ),
          LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) x_2 : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ) ∧
            embDomain e x_2 = x_1
⊢ TendstoCofinite (α := α →₀ ℕ) (mapDomain f)
have refine_1 : ∀ (x : β →₀ ℕ),
  let s : Finset α := x.support.sup fun (t : β) ↦ sorry.toFinset (s := f ⁻¹' {t});
  let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
  ∀ (y : α →₀ ℕ) (hy : mapDomain f y = x),
    LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) (comapDomain (⇑e : (a : ↥s) → α) y sorry) : ℕ)
      ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)
Tactic: classical
  refine (tendstoCofinite_iff_finite_preimage_singleton _).mpr fun x ↦ ?_
  let s := Finset.sup x.support (fun t ↦ (TendstoCofinite.finite_preimage_singleton f t).toFinset)
  let e : s ↪ α := Function.Embedding.subtype (fun u ↦ u ∈ s)
  refine Set.Finite.subset (Set.Finite.image (embDomain e) <| finite_of_degree_le (degree x)) ?_
  simp only [Set.subset_def, Set.mem_preimage, Set.mem_singleton_iff, Set.mem_image,
    Set.mem_setOf_eq]
  refine fun y hy ↦ ⟨y.comapDomain e e.injective.injOn, ?_, embDomain_comapDomain ?_⟩
  · rw [← hy, degree_mapDomain]
    exact degree_comapDomain_le_of_canonicallyOrderedAdd ..
  · suffices y.support ⊆ s by simpa [e]
    simpa [← hy, mapDomain, sum, Finset.subset_iff, single_apply, s] using
      fun i hi ↦ ⟨i, by simp [hi]⟩
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
refine : ∀ (x : β →₀ ℕ), Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
refine₁ refine₂ : ∀ (x : β →₀ ℕ), Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
refine₃ :
  ∀ (x : β →₀ ℕ),
    let s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t});
    let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
    Subset (α := Set (α →₀ ℕ)) (mapDomain f ⁻¹' {x})
      (embDomain e ''
        {f : ↥s →₀ ℕ | LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) f : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)})
refine₄ :
  ∀ (x : β →₀ ℕ),
    let s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t});
    let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
    ∀ (x_1 : α →₀ ℕ),
      mapDomain f x_1 = x →
        ∃ (x_2 : ↥s →₀ ℕ),
          LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) x_2 : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ) ∧
            embDomain e x_2 = x_1
refine_1 :
  ∀ (x : β →₀ ℕ),
    let s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t});
    let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
    ∀ (y : α →₀ ℕ) (hy : mapDomain f y = x),
      LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) (comapDomain (⇑e : (a : ↥s) → α) y ⋯) : ℕ)
        ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)
⊢ TendstoCofinite (α := α →₀ ℕ) (mapDomain f)
have refine_2 : ∀ (x : β →₀ ℕ),
  let s : Finset α := x.support.sup fun (t : β) ↦ sorry.toFinset (s := f ⁻¹' {t});
  let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
  ∀ (y : α →₀ ℕ) (hy : mapDomain f y = x), (↑y.support : Set α) ⊆ range (ι := ↥s) (⇑e : (a : ↥s) → α)
Tactic: classical
  refine (tendstoCofinite_iff_finite_preimage_singleton _).mpr fun x ↦ ?_
  let s := Finset.sup x.support (fun t ↦ (TendstoCofinite.finite_preimage_singleton f t).toFinset)
  let e : s ↪ α := Function.Embedding.subtype (fun u ↦ u ∈ s)
  refine Set.Finite.subset (Set.Finite.image (embDomain e) <| finite_of_degree_le (degree x)) ?_
  simp only [Set.subset_def, Set.mem_preimage, Set.mem_singleton_iff, Set.mem_image,
    Set.mem_setOf_eq]
  refine fun y hy ↦ ⟨y.comapDomain e e.injective.injOn, ?_, embDomain_comapDomain ?_⟩
  · rw [← hy, degree_mapDomain]
    exact degree_comapDomain_le_of_canonicallyOrderedAdd ..
  · suffices y.support ⊆ s by simpa [e]
    simpa [← hy, mapDomain, sum, Finset.subset_iff, single_apply, s] using
      fun i hi ↦ ⟨i, by simp [hi]⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Basic (goal)
Goal:
α : Type u
f : Ultrafilter α
s : Set (Set α)
hs : s.Finite
⊢ ⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f
have empty : ⋃₀ ∅ ∈ f ↔ ∃ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t ∧ t ∈ f
Tactic: induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ his => simp [union_mem_iff, his, or_and_right, exists_or]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Basic (goal)
Goal:
α : Type u
f : Ultrafilter α
s : Set (Set α)
hs : s.Finite
empty : ⋃₀ ∅ ∈ f ↔ ∃ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t ∧ t ∈ f
⊢ ⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f
have insert : ∀ {a : Set α} {s : Set (Set α)},
  a ∉ s → s.Finite → ∀ (his : ⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f), ⋃₀ insert a s ∈ f ↔ ∃ t ∈ insert a s, t ∈ f
Tactic: induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ his => simp [union_mem_iff, his, or_and_right, exists_or]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Basic (goal)
Goal:
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
⊢ (∀ᶠ (i : α) in (↑f : Filter α), ∃ a ∈ is, P a i) ↔ ∃ a ∈ is, ∀ᶠ (i : α) in (↑f : Filter α), P a i
have simp : {x : α | ∃ a ∈ is, P a x} ∈ f ↔ ∃ a ∈ is, {x : α | P a x} ∈ f
Tactic: simp only [Filter.Eventually, Ultrafilter.mem_coe]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Basic (goal)
Goal:
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
⊢ {x : α | ∃ a ∈ is, P a x} ∈ f ↔ ∃ a ∈ is, {x : α | P a x} ∈ f
have h : Eq.{u + 1} (α := Set α) {x : α | ∃ a ∈ is, P a x} (⋃ i ∈ is, P i)
Tactic: convert! f.finite_biUnion_mem_iff his (s := P) with i
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Basic (hypothesis)
Goal:
α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : s ∈ f
⊢ ∃ x ∈ s, f = pure x
have h'₁ : ⋃ x ∈ s, {x} ∈ f
Tactic: rw [← biUnion_of_singleton s] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Basic (goal)
Goal:
α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : ⋃ x ∈ s, {x} ∈ f
⊢ ∃ x ∈ s, f = pure x
have rcases : ∀ (a : α) (has : a ∈ s) (haf : {a} ∈ f), ∃ x ∈ s, f = pure x
Tactic: rcases (Ultrafilter.finite_biUnion_mem_iff h).mp h' with ⟨a, has, haf⟩
-- Lean 4 proof step from Mathlib.Order.Filter.ZeroAndBoundedAtFilter (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedRing β
l : Filter α
f g : α → β
hf : l.ZeroAtFilter f
hg : l.BoundedAtFilter g
⊢ l.ZeroAtFilter (f * g)
have rw : ∀ (hf : Asymptotics.IsLittleO (F := ℝ) l f fun (_x : α) ↦ 1) (hg : l.BoundedAtFilter g),
  Asymptotics.IsLittleO (F := ℝ) l (f * g) fun (_x : α) ↦ 1
Tactic: rw [ZeroAtFilter, ← Asymptotics.isLittleO_one_iff (F := ℝ)] at hf ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Order.Filter.ZeroAndBoundedAtFilter (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedRing β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.ZeroAtFilter g
⊢ l.ZeroAtFilter (f * g)
have rw : ∀ (hg : Asymptotics.IsLittleO (F := ℝ) l g fun (_x : α) ↦ 1), Asymptotics.IsLittleO (F := ℝ) l (f * g) fun (_x : α) ↦ 1
Tactic: rw [ZeroAtFilter, ← Asymptotics.isLittleO_one_iff (F := ℝ)] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
⊢ (last n).rev = ⊥
have rw : Eq (α := Fin (n + 1)) 0 ⊥
Tactic: rw [rev_last, bot_eq_zero]
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
rw : Eq (α := Fin (n + 1)) 0 ⊥
⊢ (last n).rev = ⊥
have rw₁ : Eq (α := Fin (n + 1)) 0 0
Tactic: rw [rev_last, bot_eq_zero]
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin (n + 1)) (succ ⊤) ⊤
have rw : Eq (α := Fin (n + 1)) (succ (rev 0)) ⊤
Tactic: rw [← rev_zero_eq_top, ← rev_zero_eq_top, ← rev_castSucc, castSucc_zero']
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
rw : Eq (α := Fin (n + 1)) (succ (rev 0)) ⊤
⊢ Eq (α := Fin (n + 1)) (succ ⊤) ⊤
have rw₁ : Eq (α := Fin (n + 1)) (succ (rev 0)) (rev 0)
Tactic: rw [← rev_zero_eq_top, ← rev_zero_eq_top, ← rev_castSucc, castSucc_zero']
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
rw : Eq (α := Fin (n + 1)) (succ (rev 0)) ⊤
rw₁ : Eq (α := Fin (n + 1)) (succ (rev 0)) (rev 0)
⊢ Eq (α := Fin (n + 1)) (succ ⊤) ⊤
have rw₂ : Eq (α := Fin (n + 1)) (rev (castSucc 0)) (rev 0)
Tactic: rw [← rev_zero_eq_top, ← rev_zero_eq_top, ← rev_castSucc, castSucc_zero']
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
rw : Eq (α := Fin (n + 1)) (succ (rev 0)) ⊤
rw₁ : Eq (α := Fin (n + 1)) (succ (rev 0)) (rev 0)
rw₂ : Eq (α := Fin (n + 1)) (rev (castSucc 0)) (rev 0)
⊢ Eq (α := Fin (n + 1)) (succ ⊤) ⊤
have rw₃ : Eq (α := Fin (n + 1)) (rev 0) (rev 0)
Tactic: rw [← rev_zero_eq_top, ← rev_zero_eq_top, ← rev_castSucc, castSucc_zero']
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin n) 0 ⊤ ↔ n = 1
have rw : Eq (α := Fin n) ⊥ ⊤ ↔ n = 1
Tactic: rw [← bot_eq_zero, subsingleton_iff_bot_eq_top, subsingleton_iff_le_one,
    le_one_iff_eq_zero_or_eq_one, or_iff_right (NeZero.ne n)]
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
rw : Eq (α := Fin n) ⊥ ⊤ ↔ n = 1
⊢ Eq (α := Fin n) 0 ⊤ ↔ n = 1
have rw₁ : Subsingleton (Fin n) ↔ n = 1
Tactic: rw [← bot_eq_zero, subsingleton_iff_bot_eq_top, subsingleton_iff_le_one,
    le_one_iff_eq_zero_or_eq_one, or_iff_right (NeZero.ne n)]
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
rw : Eq (α := Fin n) ⊥ ⊤ ↔ n = 1
rw₁ : Subsingleton (Fin n) ↔ n = 1
⊢ Eq (α := Fin n) 0 ⊤ ↔ n = 1
have rw₂ : n ≤ 1 ↔ n = 1
Tactic: rw [← bot_eq_zero, subsingleton_iff_bot_eq_top, subsingleton_iff_le_one,
    le_one_iff_eq_zero_or_eq_one, or_iff_right (NeZero.ne n)]
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
rw : Eq (α := Fin n) ⊥ ⊤ ↔ n = 1
rw₁ : Subsingleton (Fin n) ↔ n = 1
rw₂ : n ≤ 1 ↔ n = 1
⊢ Eq (α := Fin n) 0 ⊤ ↔ n = 1
have rw₃ : n = 0 ∨ n = 1 ↔ n = 1
Tactic: rw [← bot_eq_zero, subsingleton_iff_bot_eq_top, subsingleton_iff_le_one,
    le_one_iff_eq_zero_or_eq_one, or_iff_right (NeZero.ne n)]
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
rw : Eq (α := Fin n) ⊥ ⊤ ↔ n = 1
rw₁ : Subsingleton (Fin n) ↔ n = 1
rw₂ : n ≤ 1 ↔ n = 1
rw₃ : n = 0 ∨ n = 1 ↔ n = 1
⊢ Eq (α := Fin n) 0 ⊤ ↔ n = 1
have rw₄ : n = 1 ↔ n = 1
Tactic: rw [← bot_eq_zero, subsingleton_iff_bot_eq_top, subsingleton_iff_le_one,
    le_one_iff_eq_zero_or_eq_one, or_iff_right (NeZero.ne n)]
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α) ↔
    ∀ (i : Fin n), Ne (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
have mp : Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α) →
  ∀ (i : Fin n), Ne (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
mp :
  Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α) →
    ∀ (i : Fin n), Ne (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
⊢ Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α) ↔
    ∀ (i : Fin n), Ne (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
have mpr : (∀ (i : Fin n), Ne (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)) →
  Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (hypothesis)
Goal:
α : Type u_2
inst : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α)
i : Fin n
hi : Eq (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
⊢ False
have this : i.castSucc = i.succ
Tactic: have := hf hi
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : ∀ (i : Fin n), Ne (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
⊢ Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α)
have mpr : ∀ (i : Fin n), LT.lt (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
Tactic: refine (strictMono_iff_lt_succ (f := f).2 fun i ↦ ?_).injective
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
⊢ LE.le (α := Fin n) (if h : p.castSucc < a then a.pred ⋯ else a.castPred ⋯)
    (if h : p.castSucc < b then b.pred ⋯ else b.castPred ⋯)
have pos : ∀ (ha : p.castSucc < a) (hb : p.castSucc < b), a.pred sorry ≤ b.pred sorry
Tactic: split_ifs with ha hb hb
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
pos : ∀ (ha : p.castSucc < a) (hb : p.castSucc < b), a.pred ⋯ ≤ b.pred ⋯
⊢ LE.le (α := Fin n) (if h : p.castSucc < a then a.pred ⋯ else a.castPred ⋯)
    (if h : p.castSucc < b then b.pred ⋯ else b.castPred ⋯)
have neg : ∀ (ha : p.castSucc < a) (hb : ¬p.castSucc < b), a.pred sorry ≤ b.castPred sorry
Tactic: split_ifs with ha hb hb
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
pos : ∀ (ha : p.castSucc < a) (hb : p.castSucc < b), a.pred ⋯ ≤ b.pred ⋯
neg : ∀ (ha : p.castSucc < a) (hb : ¬p.castSucc < b), a.pred ⋯ ≤ b.castPred ⋯
⊢ LE.le (α := Fin n) (if h : p.castSucc < a then a.pred ⋯ else a.castPred ⋯)
    (if h : p.castSucc < b then b.pred ⋯ else b.castPred ⋯)
have pos₁ : ∀ (ha : ¬p.castSucc < a) (hb : p.castSucc < b), a.castPred sorry ≤ b.pred sorry
Tactic: split_ifs with ha hb hb
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
pos : ∀ (ha : p.castSucc < a) (hb : p.castSucc < b), a.pred ⋯ ≤ b.pred ⋯
neg : ∀ (ha : p.castSucc < a) (hb : ¬p.castSucc < b), a.pred ⋯ ≤ b.castPred ⋯
pos₁ : ∀ (ha : ¬p.castSucc < a) (hb : p.castSucc < b), a.castPred ⋯ ≤ b.pred ⋯
⊢ LE.le (α := Fin n) (if h : p.castSucc < a then a.pred ⋯ else a.castPred ⋯)
    (if h : p.castSucc < b then b.pred ⋯ else b.castPred ⋯)
have neg₁ : ∀ (ha : ¬p.castSucc < a) (hb : ¬p.castSucc < b), a.castPred sorry ≤ b.castPred sorry
Tactic: split_ifs with ha hb hb
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ LE.le (α := Fin n) (if h : a.castSucc < i then i.pred ⋯ else i.castPred ⋯)
    (if h : b.castSucc < i then i.pred ⋯ else i.castPred ⋯)
have pos : ∀ (ha : a.castSucc < i) (hb : b.castSucc < i), i.pred sorry ≤ i.pred sorry
Tactic: split_ifs with ha hb hb
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
pos : ∀ (ha : a.castSucc < i) (hb : b.castSucc < i), i.pred ⋯ ≤ i.pred ⋯
⊢ LE.le (α := Fin n) (if h : a.castSucc < i then i.pred ⋯ else i.castPred ⋯)
    (if h : b.castSucc < i then i.pred ⋯ else i.castPred ⋯)
have neg : ∀ (ha : a.castSucc < i) (hb : ¬b.castSucc < i), i.pred sorry ≤ i.castPred sorry
Tactic: split_ifs with ha hb hb
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
pos : ∀ (ha : a.castSucc < i) (hb : b.castSucc < i), i.pred ⋯ ≤ i.pred ⋯
neg : ∀ (ha : a.castSucc < i) (hb : ¬b.castSucc < i), i.pred ⋯ ≤ i.castPred ⋯
⊢ LE.le (α := Fin n) (if h : a.castSucc < i then i.pred ⋯ else i.castPred ⋯)
    (if h : b.castSucc < i then i.pred ⋯ else i.castPred ⋯)
have pos₁ : ∀ (ha : ¬a.castSucc < i) (hb : b.castSucc < i), i.castPred sorry ≤ i.pred sorry
Tactic: split_ifs with ha hb hb
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
pos : ∀ (ha : a.castSucc < i) (hb : b.castSucc < i), i.pred ⋯ ≤ i.pred ⋯
neg : ∀ (ha : a.castSucc < i) (hb : ¬b.castSucc < i), i.pred ⋯ ≤ i.castPred ⋯
pos₁ : ∀ (ha : ¬a.castSucc < i) (hb : b.castSucc < i), i.castPred ⋯ ≤ i.pred ⋯
⊢ LE.le (α := Fin n) (if h : a.castSucc < i then i.pred ⋯ else i.castPred ⋯)
    (if h : b.castSucc < i then i.pred ⋯ else i.castPred ⋯)
have neg₁ : ∀ (ha : ¬a.castSucc < i) (hb : ¬b.castSucc < i), i.castPred sorry ≤ i.castPred sorry
Tactic: split_ifs with ha hb hb
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (hypothesis)
Goal:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
⊢ i.castPred ⋯ ≤ i.pred ⋯
have this : b < a
Tactic: have : b < a := castSucc_lt_castSucc_iff.mpr (hb.trans_le (le_of_not_gt ha))
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
i j : Fin n
hij : i.predAbove = j.predAbove
⊢ i = j
have obtain : ∀ (n : ℕ) ⦃i j : Fin (n + 1)⦄ (hij : i.predAbove = j.predAbove), i = j
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_add_one_eq.2 i.size_positive
Cleared hypotheses: n, i, j, hij
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
⊢ i = j
have inr : ∀ (this : ∀ ⦃i j : Fin (n + 1)⦄ (hij : i.predAbove = j.predAbove) (h : i < j), i = j) (h : j ≤ i), i = j
Tactic: wlog! h : i < j generalizing i j
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
inr : ∀ (this : ∀ ⦃i j : Fin (n + 1)⦄ (hij : i.predAbove = j.predAbove) (h : i < j), i = j) (h : j ≤ i), i = j
⊢ i = j
have wlog! : ∀ ⦃i j : Fin (n + 1)⦄ (hij : i.predAbove = j.predAbove) (h : i < j), i = j
Tactic: wlog! h : i < j generalizing i j
Cleared hypotheses: i, j, hij
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄ (hij : i.predAbove = j.predAbove) (h : i < j), i = j
h : j ≤ i
⊢ i = j
have inr : ∀ (h : j < i), i = j
Tactic: obtain h | rfl := h.lt_or_eq
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄ (hij : i.predAbove = j.predAbove) (h : i < j), i = j
h : j ≤ i
inr : ∀ (h : j < i), i = j
⊢ i = j
have inr₁ : ∀ (hij : j.predAbove = j.predAbove) (h : j ≤ j), j = j
Tactic: obtain h | rfl := h.lt_or_eq
Cleared hypotheses: i, hij, h
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (hypothesis)
Goal:
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
h : i < j
⊢ i = j
have hij₁ : i.predAbove i.succ = j.predAbove i.succ
Tactic: replace hij := congr_fun hij i.succ
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Order.Fin.Basic (hypothesis)
Goal:
n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i.predAbove i.succ = j.predAbove i.succ
⊢ i = j
have hij₁ : i.castSucc = i.succ
Tactic: rw [predAbove_succ_self, Fin.predAbove_of_le_castSucc _ _ (by simpa),
    ← Fin.castSucc_inj, castSucc_castPred] at hij
Cleared hypotheses: hij