awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x_1 x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) y
h : Ordinal.{u + 1}
⊢ h < lift.{u + 1, u} x.rank → h < ⨆ (i : ↥x), succ (lift.{u + 1, u} (↑i : ZFSet.{u}).rank)
have rw : (∃ a' < x.rank, lift.{u + 1, u} a' = h) → h < ⨆ (i : ↥x), succ (lift.{u + 1, u} (↑i : ZFSet.{u}).rank)
Tactic: rw [lt_lift_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ V_ o ↔ ∃ a < o, x ⊆ V_ a
have rw : x ∈ ⋃ (a : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑a : Ordinal.{u})).powerset ↔ ∃ a < o, x ⊆ V_ a
Tactic: rw [vonNeumann]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u_1}
⊢ IsTransitive.{u_1} (V_ o)
have rw : IsTransitive.{u_1} (⋃ (a : (↑(Set.Iio o) : Type (u_1 + 1))), (V_ (↑a : Ordinal.{u_1})).powerset)
Tactic: rw [vonNeumann]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
a b : Ordinal.{u}
h : a < b
⊢ V_ a ∈ V_ b
have rw : V_ a ∈ ⋃ (a : (↑(Set.Iio b) : Type (u + 1))), (V_ (↑a : Ordinal.{u})).powerset
Tactic: rw [vonNeumann]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ⊆ V_ o ↔ x.rank ≤ o
have rw : x ⊆ V_ o ↔ ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
Tactic: rw [rank_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ⊆ V_ o ↔ ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
have mp : x ⊆ V_ o → ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
mp : x ⊆ V_ o → ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
⊢ x ⊆ V_ o ↔ ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
have mpr : (∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o) → x ⊆ V_ o
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y.rank < o
have mp : (V_ o).rank ≤ o
Tactic: apply (rank_lt_of_mem (hx hy)).trans_le
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ (V_ o).rank ≤ o
have mp : ∀ ⦃y : ZFSet.{u_1}⦄, (∃ a < o, y ⊆ V_ a) → y.rank < o
Tactic: simp_rw [rank_le_iff, mem_vonNeumann']
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y ∈ V_ o
have mpr : ∃ a < o, y ⊆ V_ a
Tactic: rw [mem_vonNeumann']
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (hypothesis)
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ ∃ a < o, y ⊆ V_ a
have this : y.rank < o
Tactic: have := hx hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ V_ o ↔ x.rank < o
have simp_rw : (∃ a < o, x.rank ≤ a) ↔ x.rank < o
Tactic: simp_rw [mem_vonNeumann', subset_vonNeumann]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u_1}
⊢ (V_ o).rank ≤ o
have rw : V_ o ⊆ V_ o
Tactic: rw [← subset_vonNeumann]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
x y : ZFSet.{u}
h : x ⊆ y
hy : y ∈ V_ o
⊢ x ∈ V_ o
have rw : ∀ (hy : y.rank < o), x.rank < o
Tactic: rw [mem_vonNeumann] at *
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u_1}
z : ZFSet.{u_1}
⊢ z ∈ V_ (o + 1) ↔ z ∈ (V_ o).powerset
have rw : z.rank < o + 1 ↔ z ∈ (V_ o).powerset
Tactic: rw [mem_vonNeumann, mem_powerset, subset_vonNeumann, lt_add_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u_1}
z : ZFSet.{u_1}
rw : z.rank < o + 1 ↔ z ∈ (V_ o).powerset
⊢ z ∈ V_ (o + 1) ↔ z ∈ (V_ o).powerset
have rw₁ : z.rank < o + 1 ↔ z ⊆ V_ o
Tactic: rw [mem_vonNeumann, mem_powerset, subset_vonNeumann, lt_add_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u_1}
z : ZFSet.{u_1}
rw : z.rank < o + 1 ↔ z ∈ (V_ o).powerset
rw₁ : z.rank < o + 1 ↔ z ⊆ V_ o
⊢ z ∈ V_ (o + 1) ↔ z ∈ (V_ o).powerset
have rw₂ : z.rank < o + 1 ↔ z.rank ≤ o
Tactic: rw [mem_vonNeumann, mem_powerset, subset_vonNeumann, lt_add_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u_1}
z : ZFSet.{u_1}
rw : z.rank < o + 1 ↔ z ∈ (V_ o).powerset
rw₁ : z.rank < o + 1 ↔ z ⊆ V_ o
rw₂ : z.rank < o + 1 ↔ z.rank ≤ o
⊢ z ∈ V_ (o + 1) ↔ z ∈ (V_ o).powerset
have rw₃ : z.rank ≤ o ↔ z.rank ≤ o
Tactic: rw [mem_vonNeumann, mem_powerset, subset_vonNeumann, lt_add_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ (V_ o).card = preBeth o
have limit : (⋃ (a : (↑(Set.Iio o) : Type (u + 1))), V_ (↑a : Ordinal.{u})).card =
  ⨆ (a : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑a : Ordinal.{u})).card
Tactic: simp_rw [preBeth_limit ho.isSuccPrelimit, ← fun i : Set.Iio o => ih i i.2,
      vonNeumann_of_isSuccPrelimit ho.isSuccPrelimit]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ (⋃ (a : (↑(Set.Iio o) : Type (u + 1))), V_ (↑a : Ordinal.{u})).card =
    ⨆ (a : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑a : Ordinal.{u})).card
have limit : (⋃ (i : (↑(Set.Iio o) : Type (u + 1))), V_ (↑i : Ordinal.{u})).card ≤
  ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card
Tactic: apply iSup_card_le_card_iUnion.antisymm'
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ (⋃ (i : (↑(Set.Iio o) : Type (u + 1))), V_ (↑i : Ordinal.{u})).card ≤
    ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card
have limit : lift.{u + 1, u} (⋃ (i : (↑(Set.Iio o) : Type (u + 1))), V_ (↑i : Ordinal.{u})).card ≤
  lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)
Tactic: rw [← lift_le.{u + 1}]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ lift.{u + 1, u} (⋃ (i : (↑(Set.Iio o) : Type (u + 1))), V_ (↑i : Ordinal.{u})).card ≤
    lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)
have limit : (sum fun (i : (↑(Set.Iio o) : Type (u + 1))) ↦ (V_ (↑i : Ordinal.{u})).card) ≤
  lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)
Tactic: apply lift_card_iUnion_le_sum_card.trans
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ (sum fun (i : (↑(Set.Iio o) : Type (u + 1))) ↦ (V_ (↑i : Ordinal.{u})).card) ≤
    lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)
have limit : ℵ₀ ≤ #(↑(Set.Iio o) : Type (u + 1))
Tactic: refine (sum_eq_lift_iSup_of_lift_mk_le_lift_iSup ?_ ?_).le
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
limit : ℵ₀ ≤ #(↑(Set.Iio o) : Type (u + 1))
⊢ (sum fun (i : (↑(Set.Iio o) : Type (u + 1))) ↦ (V_ (↑i : Ordinal.{u})).card) ≤
    lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)
have limit₁ : lift.{u, u + 1} #(↑(Set.Iio o) : Type (u + 1)) ≤
  lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)
Tactic: refine (sum_eq_lift_iSup_of_lift_mk_le_lift_iSup ?_ ?_).le
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ ℵ₀ ≤ #(↑(Set.Iio o) : Type (u + 1))
have limit : Ordinal.omega0 ≤ o
Tactic: rw [mk_Iio_ordinal, ← lift_aleph0.{u + 1, u}, lift_le, Ordinal.aleph0_le_card]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ lift.{u, u + 1} #(↑(Set.Iio o) : Type (u + 1)) ≤
    lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)
have limit : o.card ≤ ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card
Tactic: rw [mk_Iio_ordinal, lift_lift, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ o.card ≤ ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card
have limit : ∀ (h : ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card < o.card), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card < o.card
⊢ False
have limit : HPow.hPow (α := Cardinal.{u}) 2 (V_ (ord (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card))).card ≤
  ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card
Tactic: refine (⨆ i : Set.Iio o, (V_ ↑i).card).card_ord.not_lt <|
        (Ordinal.card_le_card_vonNeumann _).trans_lt <| (cantor _).trans_le ?_
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card < o.card
⊢ HPow.hPow (α := Cardinal.{u}) 2
      (V_ (ord (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card))).card ≤
    ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card
have limit : (V_ (succ (ord (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)))).card ≤
  ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card
Tactic: rw [← card_powerset, ← vonNeumann_succ]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card < o.card
⊢ (V_ (succ (ord (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)))).card ≤
    ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card
have limit : ord (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card) < o
Tactic: refine le_ciSup bddAbove_of_small (⟨_, ho.succ_lt ?_⟩ : Set.Iio o)
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
⊢ (V_ o).card = preBeth o
have zero : (V_ 0).card = preBeth 0
Tactic: induction o using Ordinal.limitRecOn with
  | zero => simp
  | add_one o ih => simp [ih]
  | limit o ho ih =>
    simp_rw [preBeth_limit ho.isSuccPrelimit, ← fun i : Set.Iio o => ih i i.2,
      vonNeumann_of_isSuccPrelimit ho.isSuccPrelimit]
    apply iSup_card_le_card_iUnion.antisymm'
    rw [← lift_le.{u + 1}]
    apply lift_card_iUnion_le_sum_card.trans
    refine (sum_eq_lift_iSup_of_lift_mk_le_lift_iSup ?_ ?_).le
    · rw [mk_Iio_ordinal, ← lift_aleph0.{u + 1, u}, lift_le, Ordinal.aleph0_le_card]
      exact Ordinal.omega0_le_of_isSuccLimit ho
    · rw [mk_Iio_ordinal, lift_lift, lift_le]
      by_contra! h
      refine (⨆ i : Set.Iio o, (V_ ↑i).card).card_ord.not_lt <|
        (Ordinal.card_le_card_vonNeumann _).trans_lt <| (cantor _).trans_le ?_
      rw [← card_powerset, ← vonNeumann_succ]
      refine le_ciSup bddAbove_of_small (⟨_, ho.succ_lt ?_⟩ : Set.Iio o)
      exact (ord_card_le _).trans_lt' (ord_strictMono h)
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
zero : (V_ 0).card = preBeth 0
⊢ (V_ o).card = preBeth o
have add_one : ∀ (o : Ordinal.{u}) (ih : (V_ o).card = preBeth o), (V_ (o + 1)).card = preBeth (o + 1)
Tactic: induction o using Ordinal.limitRecOn with
  | zero => simp
  | add_one o ih => simp [ih]
  | limit o ho ih =>
    simp_rw [preBeth_limit ho.isSuccPrelimit, ← fun i : Set.Iio o => ih i i.2,
      vonNeumann_of_isSuccPrelimit ho.isSuccPrelimit]
    apply iSup_card_le_card_iUnion.antisymm'
    rw [← lift_le.{u + 1}]
    apply lift_card_iUnion_le_sum_card.trans
    refine (sum_eq_lift_iSup_of_lift_mk_le_lift_iSup ?_ ?_).le
    · rw [mk_Iio_ordinal, ← lift_aleph0.{u + 1, u}, lift_le, Ordinal.aleph0_le_card]
      exact Ordinal.omega0_le_of_isSuccLimit ho
    · rw [mk_Iio_ordinal, lift_lift, lift_le]
      by_contra! h
      refine (⨆ i : Set.Iio o, (V_ ↑i).card).card_ord.not_lt <|
        (Ordinal.card_le_card_vonNeumann _).trans_lt <| (cantor _).trans_le ?_
      rw [← card_powerset, ← vonNeumann_succ]
      refine le_ciSup bddAbove_of_small (⟨_, ho.succ_lt ?_⟩ : Set.Iio o)
      exact (ord_card_le _).trans_lt' (ord_strictMono h)
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.VonNeumann (goal)
Goal:
o : Ordinal.{u}
zero : (V_ 0).card = preBeth 0
add_one : ∀ (o : Ordinal.{u}) (ih : (V_ o).card = preBeth o), (V_ (o + 1)).card = preBeth (o + 1)
⊢ (V_ o).card = preBeth o
have limit : ∀ (o : Ordinal.{u}) (ho : IsSuccLimit o) (ih : ∀ o' < o, (V_ o').card = preBeth o'), (V_ o).card = preBeth o
Tactic: induction o using Ordinal.limitRecOn with
  | zero => simp
  | add_one o ih => simp [ih]
  | limit o ho ih =>
    simp_rw [preBeth_limit ho.isSuccPrelimit, ← fun i : Set.Iio o => ih i i.2,
      vonNeumann_of_isSuccPrelimit ho.isSuccPrelimit]
    apply iSup_card_le_card_iUnion.antisymm'
    rw [← lift_le.{u + 1}]
    apply lift_card_iUnion_le_sum_card.trans
    refine (sum_eq_lift_iSup_of_lift_mk_le_lift_iSup ?_ ?_).le
    · rw [mk_Iio_ordinal, ← lift_aleph0.{u + 1, u}, lift_le, Ordinal.aleph0_le_card]
      exact Ordinal.omega0_le_of_isSuccLimit ho
    · rw [mk_Iio_ordinal, lift_lift, lift_le]
      by_contra! h
      refine (⨆ i : Set.Iio o, (V_ ↑i).card).card_ord.not_lt <|
        (Ordinal.card_le_card_vonNeumann _).trans_lt <| (cantor _).trans_le ?_
      rw [← card_powerset, ← vonNeumann_succ]
      refine le_ciSup bddAbove_of_small (⟨_, ho.succ_lt ?_⟩ : Set.Iio o)
      exact (ord_card_le _).trans_lt' (ord_strictMono h)
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Tactic.Abel (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ termg n₁ x a₁ + termg n₂ x a₂ = termg n' x a'
have simp : n₁ • x + a₁ + (n₂ • x + a₂) = n₁ • x + n₂ • x + (a₁ + a₂)
Tactic: simp only [termg, h₁.symm, add_zsmul, h₂.symm]
-- Lean 4 proof step from Mathlib.Tactic.Abel (goal)
Goal:
α : Type u_1
inst : SubtractionMonoid α
a b c : α
h : a + -b = c
rw : a + -b = c
⊢ a - b = c
have rw₁ : c = c
Tactic: rw [sub_eq_add_neg, h]
-- Lean 4 proof step from Mathlib.Tactic.Abel (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t
have rw : tl + r = t
Tactic: rw [prl, prr, prt]
-- Lean 4 proof step from Mathlib.Tactic.Abel (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
rw : tl + r = t
rw₁ : tl + tr = t
⊢ l + r = t
have rw₂ : t = t
Tactic: rw [prl, prr, prt]
-- Lean 4 proof step from Mathlib.Tactic.Abel (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t
have rw : tl + r = t
Tactic: rw [prl, prr, prt]
-- Lean 4 proof step from Mathlib.Tactic.Abel (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
rw : tl + r = t
rw₁ : tl + tr = t
⊢ l + r = t
have rw₂ : t = t
Tactic: rw [prl, prr, prt]
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (hypothesis)
Goal:
A : Type u_2
sA : CommSemiring A
a : A
h : IsNat a 0
⊢ a = 0
have this : a = (↑0 : A)
Tactic: have := h.out
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
n : ℕ
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : n.AtLeastTwo
a : A
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) (OfNat.ofNat n) a = OfNat.ofNat n * a
have simp_rw : HSMul.hSMul.{u_3, u_4, u_4} (α := R) n.rawCast a = n.rawCast * a
Tactic: simp_rw [← nat_rawCast_2]
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
A : Type u_2
sA : CommSemiring A
a₁ a₂ b₁ b₂ : A
ha₁ : a₁ = 0
ha₂ : a₂ = b₁ + b₂
⊢ a₁ + a₂ = b₁ + b₂
have subst_vars : 0 + (b₁ + b₂) = b₁ + b₂
Tactic: subst_vars
Cleared hypotheses: a₁, a₂, ha₁, ha₂
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
A : Type u_2
sA : CommSemiring A
a₁ a₂ b₁ b₂ : A
hb₁ : b₁ = 0
ha : a₁ + a₂ = b₂
⊢ a₁ + a₂ = b₁ + b₂
have subst_vars : a₁ + a₂ = 0 + (a₁ + a₂)
Tactic: subst_vars
Cleared hypotheses: b₁, b₂, hb₁, ha
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
A : Type u_2
sA : CommSemiring A
a₁ a₂ b₁ b₂ : A
ha : a₁ = b₁
hb : a₂ = b₂
⊢ a₁ + a₂ = b₁ + b₂
have subst_vars : b₁ + b₂ = b₁ + b₂
Tactic: subst_vars
Cleared hypotheses: a₁, a₂, ha, hb
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
A : Type u_2
e₁ e₂ a b : A
ha : e₁ = a
hb : e₂ = b
hab : a = b
⊢ e₁ = e₂
have subst_vars : b = b
Tactic: subst_vars
Cleared hypotheses: e₁, e₂, a, ha, hb, hab
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s t : R
h : r + s = t
⊢ HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) s : A) =
    (algebraMap R A : (a : R) → A) t
have rw : Eq.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) (r + s) : A) ((algebraMap R A : (a : R) → A) t : A)
Tactic: rw [← map_add, h]
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s t : R
h : r + s = t
rw : Eq.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) (r + s) : A) ((algebraMap R A : (a : R) → A) t : A)
⊢ HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) s : A) =
    (algebraMap R A : (a : R) → A) t
have rw₁ : Eq.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) t : A) ((algebraMap R A : (a : R) → A) t : A)
Tactic: rw [← map_add, h]
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
h : r + s = 0
⊢ IsNat (HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) s : A)) 0
have rw : IsNat.{u_2} (α := A) 0 0
Tactic: rw [← map_add, h, map_zero]
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
r t : R
h : -r = t
⊢ Eq.{u_4 + 1} (α := A) (-(algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) t : A)
have rw : Eq.{u_4 + 1} (α := A) ((algebraMap R A : (a : R) → A) (-r) : A) ((algebraMap R A : (a : R) → A) t : A)
Tactic: rw [← map_neg, h]
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
r t : R
h : -r = t
rw : Eq.{u_4 + 1} (α := A) ((algebraMap R A : (a : R) → A) (-r) : A) ((algebraMap R A : (a : R) → A) t : A)
⊢ Eq.{u_4 + 1} (α := A) (-(algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) t : A)
have rw₁ : Eq.{u_4 + 1} (α := A) ((algebraMap R A : (a : R) → A) t : A) ((algebraMap R A : (a : R) → A) t : A)
Tactic: rw [← map_neg, h]
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
b : ℕ
h : r ^ b = s
⊢ HPow.hPow (α := A) ((algebraMap R A : (a : R) → A) r : A) b = (algebraMap R A : (a : R) → A) s
have rw : Eq.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) (r ^ b) : A) ((algebraMap R A : (a : R) → A) s : A)
Tactic: rw [← map_pow, h]
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
b : ℕ
h : r ^ b = s
rw : Eq.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) (r ^ b) : A) ((algebraMap R A : (a : R) → A) s : A)
⊢ HPow.hPow (α := A) ((algebraMap R A : (a : R) → A) r : A) b = (algebraMap R A : (a : R) → A) s
have rw₁ : Eq.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) s : A) ((algebraMap R A : (a : R) → A) s : A)
Tactic: rw [← map_pow, h]
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
R : Type u_3
A : Type u_4
inst : Semifield R
inst_1 : Semifield A
inst_2 : Algebra R A
r s : R
h : r⁻¹ = s
⊢ Eq.{u_4 + 1} (α := A) (((algebraMap R A : (a : R) → A) r)⁻¹ : A) ((algebraMap R A : (a : R) → A) s : A)
have rw : Eq.{u_4 + 1} (α := A) ((algebraMap R A : (a : R) → A) r⁻¹ : A) ((algebraMap R A : (a : R) → A) s : A)
Tactic: rw [← map_inv₀, h]
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
R : Type u_3
A : Type u_4
inst : Semifield R
inst_1 : Semifield A
inst_2 : Algebra R A
r s : R
h : r⁻¹ = s
rw : Eq.{u_4 + 1} (α := A) ((algebraMap R A : (a : R) → A) r⁻¹ : A) ((algebraMap R A : (a : R) → A) s : A)
⊢ Eq.{u_4 + 1} (α := A) (((algebraMap R A : (a : R) → A) r)⁻¹ : A) ((algebraMap R A : (a : R) → A) s : A)
have rw₁ : Eq.{u_4 + 1} (α := A) ((algebraMap R A : (a : R) → A) s : A) ((algebraMap R A : (a : R) → A) s : A)
Tactic: rw [← map_inv₀, h]
-- Lean 4 proof step from Mathlib.Tactic.Algebra.Lemmas (goal)
Goal:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r : R
h : IsNat r 1
⊢ IsNat.{u_2} (α := A) ((algebraMap R A : (a : R) → A) (r + 0) : A) 1
have simp : IsNat.{u_2} (α := A) 1 1
Tactic: simp only [h.out, Nat.cast_one, add_zero, map_one]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
Goal:
α : Type u_1
inst : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ k * (e1 * e2) = t1 * t2
have rw : n1 * n2 * (e1 * e2) = t1 * t2
Tactic: rw [← h3, mul_comm n1, mul_assoc n2, ← mul_assoc n1, h1,
      ← mul_assoc n2, mul_comm n2, mul_assoc, h2]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
Goal:
α : Type u_1
inst : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
rw : n1 * n2 * (e1 * e2) = t1 * t2
⊢ k * (e1 * e2) = t1 * t2
have rw₁ : n2 * n1 * (e1 * e2) = t1 * t2
Tactic: rw [← h3, mul_comm n1, mul_assoc n2, ← mul_assoc n1, h1,
      ← mul_assoc n2, mul_comm n2, mul_assoc, h2]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
Goal:
α : Type u_1
inst : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
rw : n1 * n2 * (e1 * e2) = t1 * t2
rw₁ : n2 * n1 * (e1 * e2) = t1 * t2
⊢ k * (e1 * e2) = t1 * t2
have rw₂ : n2 * (n1 * (e1 * e2)) = t1 * t2
Tactic: rw [← h3, mul_comm n1, mul_assoc n2, ← mul_assoc n1, h1,
      ← mul_assoc n2, mul_comm n2, mul_assoc, h2]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
Goal:
α : Type u_1
inst : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
rw : n1 * n2 * (e1 * e2) = t1 * t2
rw₁ : n2 * n1 * (e1 * e2) = t1 * t2
rw₂ : n2 * (n1 * (e1 * e2)) = t1 * t2
⊢ k * (e1 * e2) = t1 * t2
have rw₃ : n2 * (n1 * e1 * e2) = t1 * t2
Tactic: rw [← h3, mul_comm n1, mul_assoc n2, ← mul_assoc n1, h1,
      ← mul_assoc n2, mul_comm n2, mul_assoc, h2]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
Goal:
α : Type u_1
inst : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
rw : n1 * n2 * (e1 * e2) = t1 * t2
rw₁ : n2 * n1 * (e1 * e2) = t1 * t2
rw₂ : n2 * (n1 * (e1 * e2)) = t1 * t2
rw₃ : n2 * (n1 * e1 * e2) = t1 * t2
⊢ k * (e1 * e2) = t1 * t2
have rw₄ : n2 * (t1 * e2) = t1 * t2
Tactic: rw [← h3, mul_comm n1, mul_assoc n2, ← mul_assoc n1, h1,
      ← mul_assoc n2, mul_comm n2, mul_assoc, h2]