awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
a : R
ha : SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ HAdd.hAdd (α := ℕ) 0 1) ⊤) (c (HAdd.hAdd (α := ℕ) 0 1)) a
⊢ a - a₀ ∈ I
have ha₁ : SModEq (R := R) I (c 0 + -(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ)) a
Tactic: rw [hc, pow_one, ← Ideal.one_eq_top, Ideal.smul_eq_mul, mul_one, sub_eq_add_neg] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
a : R
ha : SModEq (R := R) I (c 0 + -(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ)) a
⊢ a - a₀ ∈ I
have refine_2 : SModEq (R := R) I a (a₀ + 0)
Tactic: rw [← SModEq.sub_mem, ← add_zero a₀]
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
a : R
ha : SModEq (R := R) I (c 0 + -(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ)) a
⊢ SModEq (R := R) I a (a₀ + 0)
have refine_2 : SModEq (R := R) I (-(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ)) 0
Tactic: refine ha.symm.trans (SModEq.rfl.add ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
a : R
ha : SModEq (R := R) I (c 0 + -(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ)) a
⊢ SModEq (R := R) I (-(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ)) 0
have refine_2 : Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ ∈ I
Tactic: rw [SModEq.zero, Ideal.neg_mem_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f))
⊢ a = b
have obtain : ∀ (c : R),
  c * HPow.hPow (β := ℕ) (b - a) 2 + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f) * (b - a) +
        Polynomial.eval a f =
      Polynomial.eval (a + (b - a)) f →
    a = b
Tactic: obtain ⟨c, _⟩ := exists_mul_sq_add_linear_part_eq_eval_add f a (b - a)
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f))
c : R
h_1 :
  c * HPow.hPow (β := ℕ) (b - a) 2 + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f) * (b - a) +
      Polynomial.eval a f =
    Polynomial.eval (a + (b - a)) f
⊢ a = b
have hc : (c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f)) * (b - a) = 0
Tactic: have hc : (c * (b - a) + eval a (derivative f)) * (b - a) = 0 := by grind
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f))
c : R
h_1 :
  c * HPow.hPow (β := ℕ) (b - a) 2 + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f) * (b - a) +
      Polynomial.eval a f =
    Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f)) * (b - a) = 0
this : c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f) ∉ maximalIdeal R
⊢ a = b
have this₁ : ∃ (b_1 : R),
  (c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f)) * b_1 = 1 ∧
    b_1 * (c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f)) = 1
Tactic: rw [notMem_maximalIdeal, isUnit_iff_exists] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f))
c : R
h_1 :
  c * HPow.hPow (β := ℕ) (b - a) 2 + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f) * (b - a) +
      Polynomial.eval a f =
    Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f)) * (b - a) = 0
⊢ a = b
have suffices : c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f) ∉ maximalIdeal R
Tactic: suffices (c * (b - a) + eval a (derivative f)) ∉ maximalIdeal R by
    rw [notMem_maximalIdeal, isUnit_iff_exists] at this
    grind
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f))
c : R
h_1 :
  c * HPow.hPow (β := ℕ) (b - a) 2 + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f) * (b - a) +
      Polynomial.eval a f =
    Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f)) * (b - a) = 0
this :
  Membership.mem (γ := Ideal R) (maximalIdeal R) (c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f))
⊢ False
have this₁ : Membership.mem (γ := Ideal R) (maximalIdeal R)
  (c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f) + c * (a - b))
Tactic: replace this := (maximalIdeal R).add_mem this ((maximalIdeal R).mul_mem_left c h)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f))
c : R
h_1 :
  c * HPow.hPow (β := ℕ) (b - a) 2 + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f) * (b - a) +
      Polynomial.eval a f =
    Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f)) * (b - a) = 0
this :
  Membership.mem (γ := Ideal R) (maximalIdeal R)
    (c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f) + c * (a - b))
⊢ False
have this₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) (Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f))
Tactic: ring_nf at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
repr : Coalgebra.Repr.{u, v, u_1} R a
⊢ ∑ i ∈ repr.index, HMul.hMul (α := A) ((antipode R : (a : A) → A) (repr.left i) : A) (repr.right i) =
    HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) a : R) 1
have rw : (algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) =
  HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) a : R) 1
Tactic: rw [sum_antipode_mul_eq_algebraMap_counit, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
repr : Coalgebra.Repr.{u, v, u_1} R a
rw :
  (algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) =
    HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) a : R) 1
⊢ ∑ i ∈ repr.index, HMul.hMul (α := A) ((antipode R : (a : A) → A) (repr.left i) : A) (repr.right i) =
    HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) a : R) 1
have rw₁ : (algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) =
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) : A) (1 : A)
Tactic: rw [sum_antipode_mul_eq_algebraMap_counit, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
repr : Coalgebra.Repr.{u, v, u_1} R a
rw :
  (algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) =
    HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) a : R) 1
rw₁ :
  (algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) =
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) : A) (1 : A)
⊢ ∑ i ∈ repr.index, HMul.hMul (α := A) ((antipode R : (a : A) → A) (repr.left i) : A) (repr.right i) =
    HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) a : R) 1
have rw₂ : Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) : A)
  ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) : A)
Tactic: rw [sum_antipode_mul_eq_algebraMap_counit, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
repr : Coalgebra.Repr.{u, v, u_1} R a
⊢ ∑ i ∈ repr.index, HMul.hMul (β := A) (repr.left i) ((antipode R : (a : A) → A) (repr.right i) : A) =
    HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) a : R) 1
have rw : (algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) =
  HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) a : R) 1
Tactic: rw [sum_mul_antipode_eq_algebraMap_counit, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
repr : Coalgebra.Repr.{u, v, u_1} R a
rw :
  (algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) =
    HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) a : R) 1
⊢ ∑ i ∈ repr.index, HMul.hMul (β := A) (repr.left i) ((antipode R : (a : A) → A) (repr.right i) : A) =
    HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) a : R) 1
have rw₁ : (algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) =
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) : A) (1 : A)
Tactic: rw [sum_mul_antipode_eq_algebraMap_counit, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
repr : Coalgebra.Repr.{u, v, u_1} R a
rw :
  (algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) =
    HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) a : R) 1
rw₁ :
  (algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) =
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) : A) (1 : A)
⊢ ∑ i ∈ repr.index, HMul.hMul (β := A) (repr.left i) ((antipode R : (a : A) → A) (repr.right i) : A) =
    HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) a : R) 1
have rw₂ : Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) : A)
  ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) : A)
Tactic: rw [sum_mul_antipode_eq_algebraMap_counit, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
⊢ Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    ((counit : (a : A) → R)
        (∑ i ∈ Repr.index (ℛ R a),
          HMul.hMul (β := A) (Repr.left (ℛ R a) i) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) i) : A)) :
      R)
have simp_rw : Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
  (∑ x ∈ Repr.index (ℛ R a),
      (counit : (a : A) → R)
        (HMul.hMul (β := A) (Repr.left (ℛ R a) x) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) x) : A)) :
    R)
Tactic: simp_rw [map_sum, counit_mul, ← smul_eq_mul, ← map_smul, ← map_sum, sum_counit_smul]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
simp_rw :
  Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    (∑ x ∈ Repr.index (ℛ R a),
        (counit : (a : A) → R)
          (HMul.hMul (β := A) (Repr.left (ℛ R a) x) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) x) : A)) :
      R)
⊢ Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    ((counit : (a : A) → R)
        (∑ i ∈ Repr.index (ℛ R a),
          HMul.hMul (β := A) (Repr.left (ℛ R a) i) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) i) : A)) :
      R)
have simp_rw₁ : Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
  (∑ x ∈ Repr.index (ℛ R a),
      HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) (Repr.left (ℛ R a) x) : R)
        ((counit : (a : A) → R) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) x) : A) : R) :
    R)
Tactic: simp_rw [map_sum, counit_mul, ← smul_eq_mul, ← map_smul, ← map_sum, sum_counit_smul]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
simp_rw :
  Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    (∑ x ∈ Repr.index (ℛ R a),
        (counit : (a : A) → R)
          (HMul.hMul (β := A) (Repr.left (ℛ R a) x) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) x) : A)) :
      R)
simp_rw₁ :
  Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    (∑ x ∈ Repr.index (ℛ R a),
        HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) (Repr.left (ℛ R a) x) : R)
          ((counit : (a : A) → R) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) x) : A) : R) :
      R)
⊢ Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    ((counit : (a : A) → R)
        (∑ i ∈ Repr.index (ℛ R a),
          HMul.hMul (β := A) (Repr.left (ℛ R a) i) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) i) : A)) :
      R)
have simp_rw₂ : Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
  (∑ x ∈ Repr.index (ℛ R a),
      HSMul.hSMul (α := R) (β := R) ((counit : (a : A) → R) (Repr.left (ℛ R a) x) : R)
        ((counit : (a : A) → R) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) x) : A) : R) :
    R)
Tactic: simp_rw [map_sum, counit_mul, ← smul_eq_mul, ← map_smul, ← map_sum, sum_counit_smul]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
simp_rw :
  Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    (∑ x ∈ Repr.index (ℛ R a),
        (counit : (a : A) → R)
          (HMul.hMul (β := A) (Repr.left (ℛ R a) x) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) x) : A)) :
      R)
simp_rw₁ :
  Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    (∑ x ∈ Repr.index (ℛ R a),
        HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) (Repr.left (ℛ R a) x) : R)
          ((counit : (a : A) → R) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) x) : A) : R) :
      R)
simp_rw₂ :
  Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    (∑ x ∈ Repr.index (ℛ R a),
        HSMul.hSMul (α := R) (β := R) ((counit : (a : A) → R) (Repr.left (ℛ R a) x) : R)
          ((counit : (a : A) → R) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) x) : A) : R) :
      R)
⊢ Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    ((counit : (a : A) → R)
        (∑ i ∈ Repr.index (ℛ R a),
          HMul.hMul (β := A) (Repr.left (ℛ R a) i) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) i) : A)) :
      R)
have simp_rw₃ : Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
  (∑ x ∈ Repr.index (ℛ R a),
      (counit : (a : A) → R)
        ((antipode R : (a : A) → A)
            (HSMul.hSMul.{u, v, v} (α := R) ((counit : (a : A) → R) (Repr.left (ℛ R a) x) : R) (Repr.right (ℛ R a) x)) :
          A) :
    R)
Tactic: simp_rw [map_sum, counit_mul, ← smul_eq_mul, ← map_smul, ← map_sum, sum_counit_smul]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
simp_rw :
  Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    (∑ x ∈ Repr.index (ℛ R a),
        (counit : (a : A) → R)
          (HMul.hMul (β := A) (Repr.left (ℛ R a) x) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) x) : A)) :
      R)
simp_rw₁ :
  Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    (∑ x ∈ Repr.index (ℛ R a),
        HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) (Repr.left (ℛ R a) x) : R)
          ((counit : (a : A) → R) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) x) : A) : R) :
      R)
simp_rw₂ :
  Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    (∑ x ∈ Repr.index (ℛ R a),
        HSMul.hSMul (α := R) (β := R) ((counit : (a : A) → R) (Repr.left (ℛ R a) x) : R)
          ((counit : (a : A) → R) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) x) : A) : R) :
      R)
simp_rw₃ :
  Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    (∑ x ∈ Repr.index (ℛ R a),
        (counit : (a : A) → R)
          ((antipode R : (a : A) → A)
              (HSMul.hSMul.{u, v, v} (α := R) ((counit : (a : A) → R) (Repr.left (ℛ R a) x) : R)
                (Repr.right (ℛ R a) x)) :
            A) :
      R)
⊢ Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    ((counit : (a : A) → R)
        (∑ i ∈ Repr.index (ℛ R a),
          HMul.hMul (β := A) (Repr.left (ℛ R a) i) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) i) : A)) :
      R)
have simp_rw₄ : Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
  ((counit : (a : A) → R)
      ((antipode R : (a : A) → A)
          (∑ x ∈ Repr.index (ℛ R a),
            HSMul.hSMul.{u, v, v} (α := R) ((counit : (a : A) → R) (Repr.left (ℛ R a) x) : R) (Repr.right (ℛ R a) x)) :
        A) :
    R)
Tactic: simp_rw [map_sum, counit_mul, ← smul_eq_mul, ← map_smul, ← map_sum, sum_counit_smul]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
⊢ Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R) ((counit : (a : A) → R) a : R)
have counit : Eq.{u + 1} (α := R) ((counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
  ((counit : (a : A) → R)
      (∑ i ∈ Repr.index (ℛ R a),
        HMul.hMul (β := A) (Repr.left (ℛ R a) i) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) i) : A)) :
    R)
Tactic: calc
        counit (antipode R a)
    _ = counit (∑ i ∈ (ℛ R a).index, (ℛ R a).left i * antipode R ((ℛ R a).right i)) := by
      simp_rw [map_sum, counit_mul, ← smul_eq_mul, ← map_smul, ← map_sum, sum_counit_smul]
    _ = counit a := by simpa using congr(counit (R := R) $(sum_mul_antipode_eq_smul (ℛ R a)))
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
counit :
  Eq.{u + 1} (α := R) ((CoalgebraStruct.counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    ((CoalgebraStruct.counit : (a : A) → R)
        (∑ i ∈ Repr.index (ℛ R a),
          HMul.hMul (β := A) (Repr.left (ℛ R a) i) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) i) : A)) :
      R)
⊢ Eq.{u + 1} (α := R) ((CoalgebraStruct.counit : (a : A) → R) ((antipode R : (a : A) → A) a : A) : R)
    ((CoalgebraStruct.counit : (a : A) → R) a : R)
have counit₁ : Eq.{u + 1} (α := R)
  ((CoalgebraStruct.counit : (a : A) → R)
      (∑ i ∈ Repr.index (ℛ R a),
        HMul.hMul (β := A) (Repr.left (ℛ R a) i) ((antipode R : (a : A) → A) (Repr.right (ℛ R a) i) : A)) :
    R)
  ((CoalgebraStruct.counit : (a : A) → R) a : R)
Tactic: calc
        counit (antipode R a)
    _ = counit (∑ i ∈ (ℛ R a).index, (ℛ R a).left i * antipode R ((ℛ R a).right i)) := by
      simp_rw [map_sum, counit_mul, ← smul_eq_mul, ← map_smul, ← map_sum, sum_counit_smul]
    _ = counit a := by simpa using congr(counit (R := R) $(sum_mul_antipode_eq_smul (ℛ R a)))
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
⊢ Eq (α := A →ₗ[R] R) (counit ∘ₗ antipode R) counit
have h : ∀ (x : A), Eq.{u + 1} (α := R) ((counit ∘ₗ antipode R : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)
Tactic: ext