awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
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

Tactic:
le_ciSup bddAbove_of_small (⟨_, ho.succ_lt ?_⟩ : Set.Iio o)

Premises used: Order.succ, Set.Mem, Order.IsSuccLimit.succ_lt, Subtype.mk, le_ciSup, Cardinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
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
limit : ord (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card) < o
⊢ (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:
refine le_ciSup bddAbove_of_small (⟨_, ho.succ_lt ?_⟩ : Set.Iio o)

Premises used: Order.IsSuccLimit.succ_lt, Subtype.mk, le_ciSup, Cardinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
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
⊢ ord (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card) < o

Tactic:
(ord_card_le _).trans_lt' (ord_strictMono h)

Premises used: LE.le.trans_lt', Cardinal.ord_strictMono, Cardinal.ord_card_le
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
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
⊢ ord (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card) < o

Tactic:
exact (ord_card_le _).trans_lt' (ord_strictMono h)

Premises used: LE.le.trans_lt', Cardinal.ord_strictMono, Cardinal.ord_card_le
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
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)
limit : ∀ (o : Ordinal.{u}) (ho : IsSuccLimit o) (ih : ∀ o' < o, (V_ o').card = preBeth 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)

Premises used: Cardinal.lift_lift, LE.le.antisymm', iSup, Cardinal.sum_eq_lift_iSup_of_lift_mk_le_lift_iSup, Eq.le, ZFSet.vonNeumann, Cardinal.mk_Iio_ordinal, ZFSet.lift_card_iUnion_le_sum_card, Ordinal.aleph0_le_card, Cardinal.cantor, LT.lt.trans_le, Cardinal.card_ord, Ordinal.card_le_card_vonNeumann, Eq.not_lt, ZFSet.card, ZFSet.card_powerset, LE.le.trans, Subtype.val, LE.le.trans_lt, ZFSet.vonNeumann_succ, ZFSet.iSup_card_le_card_iUnion, Cardinal.lift_le
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommMonoid α
k : α
n : ℕ
x a a' : α
h : k + a = a'
⊢ k + term n x a = term n x a'

Tactic:
simp [h.symm, term, add_comm, add_assoc]

Premises used: add_assoc, Mathlib.Tactic.Abel.term, add_comm, Eq.symm
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
k : α
n : ℤ
x a a' : α
h : k + a = a'
⊢ k + termg n x a = termg n x a'

Tactic:
simp [h.symm, termg, add_comm, add_assoc]

Premises used: add_assoc, add_comm, Mathlib.Tactic.Abel.termg, Eq.symm
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommMonoid α
n : ℕ
x a k a' : α
h : a + k = a'
⊢ term n x a + k = term n x a'

Tactic:
simp [h.symm, term, add_assoc]

Premises used: add_assoc, Mathlib.Tactic.Abel.term, Eq.symm
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
n : ℤ
x a k a' : α
h : a + k = a'
⊢ termg n x a + k = termg n x a'

Tactic:
simp [h.symm, termg, add_assoc]

Premises used: add_assoc, Mathlib.Tactic.Abel.termg, Eq.symm
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommMonoid α
n₁ : ℕ
x a₁ : α
n₂ : ℕ
a₂ : α
n' : ℕ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ term n₁ x a₁ + term n₂ x a₂ = term n' x a'

Tactic:
simp [h₁.symm, h₂.symm, term, add_nsmul, add_assoc, add_left_comm]

Premises used: add_left_comm, add_assoc, Mathlib.Tactic.Abel.term, Eq.symm, add_nsmul
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
simp : n₁ • x + a₁ + (n₂ • x + a₂) = n₁ • x + n₂ • x + (a₁ + a₂)
⊢ termg n₁ x a₁ + termg n₂ x a₂ = termg n' x a'

Tactic:
simp only [termg, h₁.symm, add_zsmul, h₂.symm]

Premises used: add_zsmul, Mathlib.Tactic.Abel.termg, Eq.symm
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ n₁ • x + a₁ + (n₂ • x + a₂) = n₁ • x + n₂ • x + (a₁ + a₂)

Tactic:
add_add_add_comm (n₁ • x) a₁ (n₂ • x) a₂

Premises used: HSMul.hSMul, add_add_add_comm
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ n₁ • x + a₁ + (n₂ • x + a₂) = n₁ • x + n₂ • x + (a₁ + a₂)

Tactic:
exact add_add_add_comm (n₁ • x) a₁ (n₂ • x) a₂

Premises used: HSMul.hSMul, add_add_add_comm
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommMonoid α
x a : α
⊢ term 0 x a = a

Tactic:
simp [term, zero_nsmul]

Premises used: Mathlib.Tactic.Abel.term, zero_nsmul
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
x a : α
⊢ termg 0 x a = a

Tactic:
simp [termg, zero_zsmul]

Premises used: zero_zsmul, Mathlib.Tactic.Abel.termg
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : -n = n'
h₂ : -a = a'
⊢ -termg n x a = termg n' x a'

Tactic:
simpa [h₂.symm, h₁.symm, termg] using add_comm _ _

Premises used: add_comm, Mathlib.Tactic.Abel.termg, Eq.symm
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommMonoid α
c : ℕ
⊢ Eq.{u_1 + 1} (α := α) (smul c 0) 0

Tactic:
simp [smul, nsmul_zero]

Premises used: nsmul_zero, Mathlib.Tactic.Abel.smul
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
c : ℤ
⊢ Eq.{u_1 + 1} (α := α) (smulg c 0) 0

Tactic:
simp [smulg, zsmul_zero]

Premises used: zsmul_zero, Mathlib.Tactic.Abel.smulg
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommMonoid α
c n : ℕ
x a : α
n' : ℕ
a' : α
h₁ : c * n = n'
h₂ : smul c a = a'
⊢ smul c (term n x a) = term n' x a'

Tactic:
simp [h₂.symm, h₁.symm, term, smul, nsmul_add, mul_nsmul']

Premises used: Mathlib.Tactic.Abel.term, mul_nsmul', nsmul_add, Mathlib.Tactic.Abel.smul, Eq.symm
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
c n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : c * n = n'
h₂ : smulg c a = a'
⊢ smulg c (termg n x a) = termg n' x a'

Tactic:
simp [h₂.symm, h₁.symm, termg, smulg, zsmul_add, mul_zsmul]

Premises used: zsmul_add, mul_zsmul, Mathlib.Tactic.Abel.termg, Eq.symm, Mathlib.Tactic.Abel.smulg
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommMonoid α
x : α
⊢ x = term 1 x 0

Tactic:
simp [term, one_nsmul]

Premises used: Mathlib.Tactic.Abel.term, one_nsmul
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
x : α
⊢ x = termg 1 x 0

Tactic:
simp [termg]

Premises used: Mathlib.Tactic.Abel.termg
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommMonoid α
x x' : α
h : x = x'
⊢ x = term 1 x' 0

Tactic:
simp [term, h, one_nsmul]

Premises used: Mathlib.Tactic.Abel.term, one_nsmul
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
x x' : α
h : x = x'
⊢ x = termg 1 x' 0

Tactic:
simp [termg, h]

Premises used: Mathlib.Tactic.Abel.termg
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : SubtractionMonoid α
a b c : α
h : a + -b = c
rw : a + -b = c
rw₁ rw₂ : c = c
⊢ a - b = c

Tactic:
rw [sub_eq_add_neg, h]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommMonoid α
n : ℕ
x y : α
h : smul n x = y
⊢ n • x = y

Tactic:
h

Premises used: Mathlib.Tactic.Abel.smul
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
n : ℕ
x y : α
h : smulg (Int.ofNat n) x = y
⊢ HSMul.hSMul (α := ℤ) (↑n : ℤ) x = y

Tactic:
h

Premises used: Mathlib.Tactic.Abel.smulg
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
n : ℤ
x y : α
h : smulg n x = y
⊢ n • x = y

Tactic:
h

Premises used: Mathlib.Tactic.Abel.smulg
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommMonoid α
l : ℕ
r : α
tl : ℕ
tr t : α
prl : l = tl
prr : r = tr
prt : smul tl tr = t
⊢ smul l r = t

Tactic:
simp [prl, prr, prt]
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
l : ℤ
r : α
tl : ℤ
tr t : α
prl : l = tl
prr : r = tr
prt : smulg tl tr = t
⊢ smulg l r = t

Tactic:
simp [prl, prr, prt]
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
l : ℕ
r : α
tl : ℕ
zl : ℤ
tr t : α
prl₁ : l = tl
prl₂ : (↑tl : ℤ) = zl
prr : r = tr
prt : smulg zl tr = t
⊢ smul l r = t

Tactic:
simp [← prt, prl₁, ← prl₂, prr, smul, smulg, natCast_zsmul]

Premises used: Mathlib.Tactic.Abel.smul, natCast_zsmul, Mathlib.Tactic.Abel.smulg
-- Module: Mathlib.Tactic.Abel
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
rw₂ rw₃ : t = t
⊢ l + r = t

Tactic:
rw [prl, prr, prt]
-- Module: Mathlib.Tactic.Abel
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
rw₂ rw₃ : t = t
⊢ l + r = t

Tactic:
rw [prl, prr, prt]
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
a ta t : α
pra : a = ta
prt : -ta = t
⊢ -a = t

Tactic:
simp [pra, prt]
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommMonoid α
n : ℕ
x a : α
⊢ term n x a = n • x + a

Tactic:
(rfl)

Premises used: Mathlib.Tactic.Abel.term, rfl
-- Module: Mathlib.Tactic.Abel
Goal:
α : Type u_1
inst : AddCommGroup α
n : ℤ
x a : α
⊢ termg n x a = n • x + a

Tactic:
(rfl)

Premises used: Mathlib.Tactic.Abel.termg, rfl
-- Module: Mathlib.Tactic.AdaptationNote
Goal:
⊢ True

Tactic:
trivial
-- Module: Mathlib.Tactic.AdaptationNote
Goal:
⊢ True

Tactic:
#adaptation_note /-- This is a test -/
  trivial

Premises used: trivial
-- Module: Mathlib.Tactic.Algebra.Basic
Goal:
«$u» «$v» : Level
«$R» : Type u
«$A» : Type v
«$sR» : CommSemiring «$R»
«$sA» : CommSemiring «$A»
«$sAlg» : Algebra «$R» «$A»
«$a_1» «$b_1» «$a» «$b» : «$A»
«$r» «$s» «$t» : «$R»
«$pt» : «$r» * «$s» = «$t»
⊢ HMul.hMul (α := «$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»

Tactic:
simp [← $pt, map_mul]

Premises used: map_mul
-- Module: Mathlib.Tactic.Algebra.Basic
Goal:
«$u» «$v» : Level
«$R» : Type u
«$A» : Type v
«$sR» : CommSemiring «$R»
«$sA» : CommSemiring «$A»
«$sAlg» : Algebra «$R» «$A»
«$a» «$b» : «$A»
«$r» : «$R» := Nat.rawCast 1
⊢ Eq.{v + 1} (α := «$A») (Nat.rawCast 1 : «$A») ((algebraMap «$R» «$A» : (a : «$R») → «$A») («$r» + 0) : «$A»)

Tactic:
simp +zetaDelta
-- Module: Mathlib.Tactic.Algebra.Basic
Goal:
A : Type u_1
inst : CommSemiring A
n : ℕ
⊢ Eq (α := A) ((↑n : A) : A) ((algebraMap ℕ A : (a : ℕ) → A) n : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Tactic.Algebra.Basic
Goal:
A : Type u_1
inst : CommSemiring A
n : ℕ
⊢ Eq (α := A) ((algebraMap ℕ A : (a : ℕ) → A) n : A) ((↑n : A) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Tactic.Algebra.Basic
Goal:
A : Type u_1
inst : CommRing A
n : ℤ
⊢ Eq (α := A) ((↑n : A) : A) ((algebraMap ℤ A : (a : ℤ) → A) n : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Tactic.Algebra.Basic
Goal:
A : Type u_1
inst : CommRing A
n : ℤ
⊢ Eq (α := A) ((algebraMap ℤ A : (a : ℤ) → A) n : A) ((↑n : A) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
a : A
lit : ℕ
h : IsInt a (Int.negOfNat lit)
⊢ a =
    HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) (HAdd.hAdd (α := R) (Int.negOfNat lit).rawCast 0) : A)
      (0 : A)

Tactic:
simp [h.out]

Premises used: Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : Semifield R
inst_1 : Semifield A
inst_2 : Algebra R A
a : A
n d : ℕ
h : IsNNRat a n d
⊢ a =
    HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) (HAdd.hAdd (α := R) (NNRat.rawCast n d) 0) : A) (0 : A)

Tactic:
simp [Mathlib.Tactic.Ring.cast_nnrat h]

Premises used: Mathlib.Tactic.Ring.cast_nnrat
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : Field R
inst_1 : Field A
inst_2 : Algebra R A
a : A
n d : ℕ
h : IsRat a (Int.negOfNat n) d
⊢ a =
    HAdd.hAdd (α := A) (β := A)
      ((algebraMap R A : (a : R) → A) (HAdd.hAdd (α := R) (Rat.rawCast (Int.negOfNat n) d) 0) : A) (0 : A)

Tactic:
simp [Mathlib.Tactic.Ring.cast_rat h]

Premises used: Mathlib.Tactic.Ring.cast_rat
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
A : Type u_2
sA : CommSemiring A
a : A
h : IsNat a 0
⊢ a = (↑0 : A)

Tactic:
have := h.out
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
A : Type u_2
sA : CommSemiring A
a : A
h : IsNat a 0
this : a = (↑0 : A)
⊢ a = 0

Tactic:
simp [this]
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
a : A
lit : ℕ
h : IsNat a lit
⊢ a = HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) (HAdd.hAdd (α := R) (↑lit : R) 0) : A) (0 : A)

Tactic:
simp [h.out]

Premises used: Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
sR : CommSemiring R
a b c : R
⊢ a + (b + c) = a + b + c

Tactic:
(add_assoc ..).symm

Premises used: add_assoc, Eq.symm
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
sR : CommSemiring R
a b c : R
⊢ a * (b * c) = a * b * c

Tactic:
(mul_assoc ..).symm

Premises used: mul_assoc, Eq.symm
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_3
inst : Ring R
a b : R
⊢ a * -b = -(a * b)

Tactic:
simp
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_3
inst : Ring R
a b : R
⊢ a + -b = a - b

Tactic:
(sub_eq_add_neg ..).symm

Premises used: sub_eq_add_neg, Eq.symm
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
sR : CommSemiring R
⊢ Eq.{u_1 + 1} (α := R) (Nat.rawCast 0) 0

Tactic:
simp
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
sR : CommSemiring R
⊢ Eq.{u_1 + 1} (α := R) (Nat.rawCast 1) 1

Tactic:
simp
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
sR : CommSemiring R
n : ℕ
inst : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := R) n.rawCast (OfNat.ofNat n)

Tactic:
rfl

Premises used: Nat.rawCast, rfl
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
n : ℕ
R : Type u_3
inst : Ring R
⊢ Eq.{u_3 + 1} (α := R) (Int.negOfNat n).rawCast (-n.rawCast)

Tactic:
simp
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
n d : ℕ
R : Type u_3
inst : DivisionSemiring R
⊢ NNRat.rawCast n d = HDiv.hDiv (α := R) n.rawCast d.rawCast

Tactic:
simp
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
n d : ℕ
R : Type u_3
inst : DivisionRing R
⊢ Rat.rawCast (Int.negOfNat n) d = HDiv.hDiv (α := R) (Int.negOfNat n).rawCast d.rawCast

Tactic:
simp
-- Module: Mathlib.Tactic.Algebra.Lemmas
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
simp_rw : HSMul.hSMul.{u_3, u_4, u_4} (α := R) n.rawCast a = n.rawCast * a
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) (OfNat.ofNat n) a = OfNat.ofNat n * a

Tactic:
simp_rw [← nat_rawCast_2]

Premises used: Mathlib.Tactic.Algebra.nat_rawCast_2
-- Module: Mathlib.Tactic.Algebra.Lemmas
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) n.rawCast a = n.rawCast * a

Tactic:
simp [Nat.cast_smul_eq_nsmul]

Premises used: Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
n : ℕ
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
a : A
inst_3 : n.AtLeastTwo
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-OfNat.ofNat n) a = -OfNat.ofNat n * a

Tactic:
simpa [← nat_rawCast_2] using ofNat_smul

Premises used: Mathlib.Tactic.Algebra.nat_rawCast_2, Mathlib.Tactic.Algebra.ofNat_smul
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
a : A
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) (-1) a = -a

Tactic:
simp
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
d : ℕ
R : Type u_3
A : Type u_4
inst : Semifield R
inst_1 : Semifield A
inst_2 : Algebra R A
a : A
inst_3 : d.AtLeastTwo
⊢ HDiv.hDiv (α := R) 1 (OfNat.ofNat d) • a = HDiv.hDiv (α := A) 1 (OfNat.ofNat d) * a

Tactic:
simp [Algebra.smul_def, ← nat_rawCast_2]

Premises used: Mathlib.Tactic.Algebra.nat_rawCast_2, Algebra.smul_def
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
n d : ℕ
R : Type u_3
A : Type u_4
inst : Semifield R
inst_1 : Semifield A
inst_2 : Algebra R A
a : A
inst_3 : n.AtLeastTwo
inst_4 : d.AtLeastTwo
⊢ HDiv.hDiv (α := R) (OfNat.ofNat n) (OfNat.ofNat d) • a = HDiv.hDiv (α := A) (OfNat.ofNat n) (OfNat.ofNat d) * a

Tactic:
simp [Algebra.smul_def, ← nat_rawCast_2]

Premises used: Mathlib.Tactic.Algebra.nat_rawCast_2, Algebra.smul_def
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
d : ℕ
R : Type u_3
A : Type u_4
inst : Field R
inst_1 : Field A
inst_2 : Algebra R A
a : A
inst_3 : d.AtLeastTwo
⊢ HDiv.hDiv (α := R) (-1) (OfNat.ofNat d) • a = HDiv.hDiv (α := A) (-1) (OfNat.ofNat d) * a

Tactic:
simp [Algebra.smul_def, ← nat_rawCast_2]

Premises used: Mathlib.Tactic.Algebra.nat_rawCast_2, Algebra.smul_def
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
n d : ℕ
R : Type u_3
A : Type u_4
inst : Field R
inst_1 : Field A
inst_2 : Algebra R A
a : A
inst_3 : n.AtLeastTwo
inst_4 : d.AtLeastTwo
⊢ HDiv.hDiv (α := R) (-OfNat.ofNat n) (OfNat.ofNat d) • a = HDiv.hDiv (α := A) (-OfNat.ofNat n) (OfNat.ofNat d) * a

Tactic:
simp [Algebra.smul_def, ← nat_rawCast_2]

Premises used: Mathlib.Tactic.Algebra.nat_rawCast_2, Algebra.smul_def
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r : R
h : r = 0
⊢ HSMul.hSMul (β := A) r 1 = 0

Tactic:
simp [h]
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
A : Type u_2
sA : CommSemiring A
a b : A
ha : a = 0
hb : b = 0
⊢ a + b = 0

Tactic:
simp [ha, hb]
-- Module: Mathlib.Tactic.Algebra.Lemmas
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
⊢ HSMul.hSMul (β := A) r 1 = HSMul.hSMul (β := A) s 1

Tactic:
simp [h]
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
A : Type u_2
sA : CommSemiring A
a₁ a₂ b₁ b₂ : A
ha₁ : a₁ = 0
ha₂ : a₂ = b₁ + b₂
subst_vars : 0 + (b₁ + b₂) = b₁ + b₂
⊢ a₁ + a₂ = b₁ + b₂

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
A : Type u_2
sA : CommSemiring A
b₁ b₂ : A
⊢ 0 + (b₁ + b₂) = b₁ + b₂

Tactic:
simp
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
A : Type u_2
sA : CommSemiring A
a₁ a₂ b₁ b₂ : A
hb₁ : b₁ = 0
ha : a₁ + a₂ = b₂
subst_vars : a₁ + a₂ = 0 + (a₁ + a₂)
⊢ a₁ + a₂ = b₁ + b₂

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
A : Type u_2
sA : CommSemiring A
a₁ a₂ : A
⊢ a₁ + a₂ = 0 + (a₁ + a₂)

Tactic:
simp
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
A : Type u_2
sA : CommSemiring A
a₁ a₂ b₁ b₂ : A
ha : a₁ = b₁
hb : a₂ = b₂
subst_vars : b₁ + b₂ = b₁ + b₂
⊢ a₁ + a₂ = b₁ + b₂

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
A : Type u_2
sA : CommSemiring A
b₁ b₂ : A
⊢ b₁ + b₂ = b₁ + b₂

Tactic:
rfl
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
A : Type u_2
e₁ e₂ a b : A
ha : e₁ = a
hb : e₂ = b
hab : a = b
subst_vars : b = b
⊢ e₁ = e₂

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
A : Type u_2
b : A
⊢ b = b

Tactic:
rfl
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
A : Type u_2
sA : CommSemiring A
c a b : A
h : a = b
⊢ c * a = c * b

Tactic:
simp [h]
-- Module: Mathlib.Tactic.Algebra.Lemmas
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)
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) t : 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

Tactic:
rw [← map_add, h]

Premises used: map_add
-- Module: Mathlib.Tactic.Algebra.Lemmas
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
rw : IsNat.{u_2} (α := A) 0 0
⊢ IsNat (HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) s : A)) 0

Tactic:
rw [← map_add, h, map_zero]

Premises used: map_zero, map_add
-- Module: Mathlib.Tactic.Algebra.Lemmas
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
⊢ Eq.{u_2 + 1} (α := A) 0 (↑0 : A)

Tactic:
simp
-- Module: Mathlib.Tactic.Algebra.Lemmas
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.{u_2} (α := A) 0 0

Tactic:
exact ⟨by simp⟩
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
R' : Type u_3
inst : HSMul R' A A
r' : R'
r : R
hr : r = 0
h_smul : ∀ (a : A), r • a = r' • a
a : A
⊢ r' • a = 0 * a

Tactic:
simp [← h_smul, hr]
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
R' : Type u_3
inst : HSMul R' A A
r' : R'
r r'' : R
hr : r = r''
h_smul : ∀ (a : A), r • a = r' • a
a : A
⊢ r' • a = HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) r'' : A) (0 : A) * a

Tactic:
simp [← h_smul, ← hr, Algebra.smul_def r a]

Premises used: Algebra.smul_def
-- Module: Mathlib.Tactic.Algebra.Lemmas
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)
rw₁ rw₂ : Eq.{u_4 + 1} (α := A) ((algebraMap R A : (a : R) → A) t : 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)

Tactic:
rw [← map_neg, h]

Premises used: map_neg
-- Module: Mathlib.Tactic.Algebra.Lemmas
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)
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) ((algebraMap R A : (a : R) → A) s : 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

Tactic:
rw [← map_pow, h]

Premises used: map_pow