awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Henselian
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
refine_2 : SModEq (R := R) I a (a₀ + 0)
⊢ a - a₀ ∈ I

Tactic:
rw [← SModEq.sub_mem, ← add_zero a₀]

Premises used: SModEq.sub_mem, add_zero
-- Module: Mathlib.RingTheory.Henselian
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)

Tactic:
ha.symm.trans (SModEq.rfl.add ?_)

Premises used: SModEq.add, SModEq.symm, SModEq.trans, SModEq.rfl
-- Module: Mathlib.RingTheory.Henselian
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
refine_2 : SModEq (R := R) I (-(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ)) 0
⊢ SModEq (R := R) I a (a₀ + 0)

Tactic:
refine ha.symm.trans (SModEq.rfl.add ?_)

Premises used: SModEq.add, SModEq.symm, SModEq.trans, SModEq.rfl
-- Module: Mathlib.RingTheory.Henselian
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
refine_2 : Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ ∈ I
⊢ SModEq (R := R) I (-(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ)) 0

Tactic:
rw [SModEq.zero, Ideal.neg_mem_iff]

Premises used: SModEq.zero, Ideal.neg_mem_iff
-- Module: Mathlib.RingTheory.Henselian
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
⊢ Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ ∈ I

Tactic:
Ideal.mul_mem_right _ _ h₁

Premises used: Set.Mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Henselian
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
⊢ Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ ∈ I

Tactic:
exact Ideal.mul_mem_right _ _ h₁

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Henselian
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))
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
⊢ a = b

Tactic:
obtain ⟨c, _⟩ := exists_mul_sq_add_linear_part_eq_eval_add f a (b - a)

Premises used: HSub.hSub, Polynomial.exists_mul_sq_add_linear_part_eq_eval_add
-- Module: Mathlib.RingTheory.Henselian
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
⊢ (c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f)) * (b - a) = 0

Tactic:
grind
-- Module: Mathlib.RingTheory.Henselian
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
⊢ (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
-- Module: Mathlib.RingTheory.Henselian
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
⊢ ∃ (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

Premises used: isUnit_iff_exists, IsLocalRing.notMem_maximalIdeal
-- Module: Mathlib.RingTheory.Henselian
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 :
  ∃ (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
⊢ a = b

Tactic:
grind
-- Module: Mathlib.RingTheory.Henselian
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
suffices : c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f) ∉ maximalIdeal R
⊢ a = b

Tactic:
suffices (c * (b - a) + eval a (derivative f)) ∉ maximalIdeal R by
    rw [notMem_maximalIdeal, isUnit_iff_exists] at this
    grind
-- Module: Mathlib.RingTheory.Henselian
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
by_contra! :
  ∀
    (this :
      Membership.mem (γ := Ideal R) (maximalIdeal R)
        (c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f))),
    False
⊢ c * (b - a) + Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f) ∉ maximalIdeal R

Tactic:
by_contra!
-- Module: Mathlib.RingTheory.Henselian
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))
⊢ 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)
-- Module: Mathlib.RingTheory.Henselian
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))
⊢ Membership.mem (γ := Ideal R) (maximalIdeal R) (Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f))

Tactic:
ring_nf at this
-- Module: Mathlib.RingTheory.Henselian
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) (Polynomial.eval a ((derivative : (a : R[X]) → R[X]) f))
⊢ False

Tactic:
contradiction
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
⊢ Eq (α := A)
    ((LinearMap.mul' R A : (a : TensorProduct R A A) → A)
        ((LinearMap.rTensor A (antipode R) : (a : TensorProduct R A A) → TensorProduct R A A)
            ((CoalgebraStruct.comul : (a : A) → TensorProduct R A A) a) :
          TensorProduct R A A) :
      A)
    ((algebraMap R A : (a : R) → A) ((CoalgebraStruct.counit : (a : A) → R) a : R) : A)

Tactic:
LinearMap.congr_fun mul_antipode_rTensor_comul a

Premises used: Quotient.liftOn', AddCon.liftOn, HopfAlgebra.mul_antipode_rTensor_comul, LinearMap.congr_fun
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
⊢ Eq (α := A)
    ((LinearMap.mul' R A : (a : TensorProduct R A A) → A)
        ((LinearMap.lTensor A (antipode R) : (a : TensorProduct R A A) → TensorProduct R A A)
            ((CoalgebraStruct.comul : (a : A) → TensorProduct R A A) a) :
          TensorProduct R A A) :
      A)
    ((algebraMap R A : (a : R) → A) ((CoalgebraStruct.counit : (a : A) → R) a : R) : A)

Tactic:
LinearMap.congr_fun mul_antipode_lTensor_comul a

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.congr_fun, HopfAlgebra.mul_antipode_lTensor_comul
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
⊢ Eq.{v + 1} (α := A) ((antipode R : (a : A) → A) 1 : A) (1 : A)

Tactic:
simpa [Algebra.TensorProduct.one_def] using mul_antipode_rTensor_comul_apply (R := R) (1 : A)

Premises used: HopfAlgebra.mul_antipode_rTensor_comul_apply, OfNat.ofNat, Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
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
⊢ Eq.{v + 1} (α := A)
    (∑ i ∈ repr.index, HMul.hMul (α := A) ((antipode R : (a : A) → A) (repr.left i) : A) (repr.right i) : A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) : A)

Tactic:
simpa [← repr.eq, map_sum] using congr($(mul_antipode_rTensor_comul (R := R)) a)

Premises used: map_sum, Coalgebra.Repr.eq
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
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
⊢ Eq.{v + 1} (α := A)
    (∑ i ∈ repr.index, HMul.hMul (β := A) (repr.left i) ((antipode R : (a : A) → A) (repr.right i) : A) : A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) a : R) : A)

Tactic:
simpa [← repr.eq, map_sum] using congr($(mul_antipode_lTensor_comul (R := R)) a)

Premises used: map_sum, Coalgebra.Repr.eq
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
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)
rw₂ 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)
⊢ ∑ 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

Tactic:
rw [sum_antipode_mul_eq_algebraMap_counit, Algebra.smul_def, mul_one]

Premises used: Algebra.smul_def, HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit, mul_one
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
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)
rw₂ 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)
⊢ ∑ 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

Tactic:
rw [sum_mul_antipode_eq_algebraMap_counit, Algebra.smul_def, mul_one]

Premises used: HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit, Algebra.smul_def, mul_one
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
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)
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)
⊢ 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:
simp_rw [map_sum, counit_mul, ← smul_eq_mul, ← map_smul, ← map_sum, sum_counit_smul]

Premises used: Coalgebra.sum_counit_smul, map_sum, Bialgebra.counit_mul, smul_eq_mul, map_smul
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
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)
        (∑ 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)
    ((counit : (a : A) → R) a : R)

Tactic:
simpa using congr(counit (R := R) $(sum_mul_antipode_eq_smul (ℛ R a)))
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
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)
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)
⊢ Eq.{u + 1} (α := R) ((CoalgebraStruct.counit : (a : A) → R) ((antipode R : (a : A) → A) a : 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)))

Premises used: HMul.hMul, CoalgebraStruct.counit, Coalgebra.Repr.index, Coalgebra.Repr.left, Coalgebra.Repr.arbitrary, Coalgebra.Repr.right, DFunLike.coe, HopfAlgebraStruct.antipode, Finset.sum
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
h : ∀ (x : A), Eq.{u + 1} (α := R) ((counit ∘ₗ antipode R : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)
⊢ Eq (α := A →ₗ[R] R) (counit ∘ₗ antipode R) counit

Tactic:
ext
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
x : A
⊢ Eq.{u + 1} (α := R) ((counit ∘ₗ antipode R : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)

Tactic:
counit_antipode _

Premises used: HopfAlgebra.counit_antipode
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
x : A
⊢ Eq.{u + 1} (α := R) ((counit ∘ₗ antipode R : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)

Tactic:
exact counit_antipode _

Premises used: HopfAlgebra.counit_antipode