awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
⊢ HSMul.hSMul (β := A ⊗[R] A) d (∑ x ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x) (x ⊗ₜ[R] x)) =
    HSMul.hSMul (β := A ⊗[R] A) d ((comul : (a : A) → A ⊗[R] A) (d • a) : A ⊗[R] A)
have rw : HSMul.hSMul (β := A ⊗[R] A) d (∑ x ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x) (x ⊗ₜ[R] x)) =
  HSMul.hSMul (β := A ⊗[R] A) d ((comul : (a : A) → A ⊗[R] A) (∑ a ∈ s, c a • a))
Tactic: rw [← hc]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
⊢ Eq (α := A ⊗[R] A) ((d • a) ⊗ₜ[R] (d • a)) (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
have simp_rw : Eq (α := A ⊗[R] A) ((∑ a ∈ s, c a • a) ⊗ₜ[R] ∑ a ∈ s, c a • a)
  (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
Tactic: simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
simp_rw :
  Eq (α := A ⊗[R] A) ((∑ a ∈ s, c a • a) ⊗ₜ[R] ∑ a ∈ s, c a • a)
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
⊢ Eq (α := A ⊗[R] A) ((d • a) ⊗ₜ[R] (d • a)) (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
have simp_rw₁ : Eq (α := A ⊗[R] A) (∑ a ∈ s, (c a • a) ⊗ₜ[R] ∑ a ∈ s, c a • a)
  (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
Tactic: simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
simp_rw :
  Eq (α := A ⊗[R] A) ((∑ a ∈ s, c a • a) ⊗ₜ[R] ∑ a ∈ s, c a • a)
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
simp_rw₁ :
  Eq (α := A ⊗[R] A) (∑ a ∈ s, (c a • a) ⊗ₜ[R] ∑ a ∈ s, c a • a)
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
⊢ Eq (α := A ⊗[R] A) ((d • a) ⊗ₜ[R] (d • a)) (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
have simp_rw₂ : Eq (α := A ⊗[R] A) (∑ x ∈ s, x ⊗ₜ[R] HSMul.hSMul (β := A) (c x) (∑ a ∈ s, c a • a))
  (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
Tactic: simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
simp_rw :
  Eq (α := A ⊗[R] A) ((∑ a ∈ s, c a • a) ⊗ₜ[R] ∑ a ∈ s, c a • a)
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
simp_rw₁ :
  Eq (α := A ⊗[R] A) (∑ a ∈ s, (c a • a) ⊗ₜ[R] ∑ a ∈ s, c a • a)
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
simp_rw₂ :
  Eq (α := A ⊗[R] A) (∑ x ∈ s, x ⊗ₜ[R] HSMul.hSMul (β := A) (c x) (∑ a ∈ s, c a • a))
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
⊢ Eq (α := A ⊗[R] A) ((d • a) ⊗ₜ[R] (d • a)) (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
have simp_rw₃ : Eq (α := A ⊗[R] A) (∑ x ∈ s, x ⊗ₜ[R] ∑ x_1 ∈ s, c x • c x_1 • x_1)
  (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
Tactic: simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
simp_rw :
  Eq (α := A ⊗[R] A) ((∑ a ∈ s, c a • a) ⊗ₜ[R] ∑ a ∈ s, c a • a)
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
simp_rw₁ :
  Eq (α := A ⊗[R] A) (∑ a ∈ s, (c a • a) ⊗ₜ[R] ∑ a ∈ s, c a • a)
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
simp_rw₂ :
  Eq (α := A ⊗[R] A) (∑ x ∈ s, x ⊗ₜ[R] HSMul.hSMul (β := A) (c x) (∑ a ∈ s, c a • a))
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
simp_rw₃ :
  Eq (α := A ⊗[R] A) (∑ x ∈ s, x ⊗ₜ[R] ∑ x_1 ∈ s, c x • c x_1 • x_1)
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
⊢ Eq (α := A ⊗[R] A) ((d • a) ⊗ₜ[R] (d • a)) (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
have simp_rw₄ : Eq (α := A ⊗[R] A) (∑ x ∈ s, ∑ a ∈ s, x ⊗ₜ[R] (c x • c a • a))
  (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
Tactic: simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
simp_rw :
  Eq (α := A ⊗[R] A) ((∑ a ∈ s, c a • a) ⊗ₜ[R] ∑ a ∈ s, c a • a)
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
simp_rw₁ :
  Eq (α := A ⊗[R] A) (∑ a ∈ s, (c a • a) ⊗ₜ[R] ∑ a ∈ s, c a • a)
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
simp_rw₂ :
  Eq (α := A ⊗[R] A) (∑ x ∈ s, x ⊗ₜ[R] HSMul.hSMul (β := A) (c x) (∑ a ∈ s, c a • a))
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
simp_rw₃ :
  Eq (α := A ⊗[R] A) (∑ x ∈ s, x ⊗ₜ[R] ∑ x_1 ∈ s, c x • c x_1 • x_1)
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
simp_rw₄ :
  Eq (α := A ⊗[R] A) (∑ x ∈ s, ∑ a ∈ s, x ⊗ₜ[R] (c x • c a • a))
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
⊢ Eq (α := A ⊗[R] A) ((d • a) ⊗ₜ[R] (d • a)) (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
have simp_rw₅ : Eq (α := A ⊗[R] A) (∑ x ∈ s, ∑ x_1 ∈ s, c x • HSMul.hSMul (β := A ⊗[R] A) (c x_1) (x ⊗ₜ[R] x_1))
  (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
Tactic: simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
⊢ d = 0
have key : Eq (α := A ⊗[R] A) (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (if x = y then d * c x else 0) (x ⊗ₜ[R] y))
  (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
Tactic: have key := calc
        ∑ x ∈ s, ∑ y ∈ s, (if x = y then d * c x else 0) • x ⊗ₜ[R] y
    _ = d • ∑ x ∈ s, c x • x ⊗ₜ[R] x := by simp [Finset.smul_sum, mul_smul]
    _ = d • comul (d • a) := by rw [← hc]; simp +contextual [(hs _ _).comul_eq_tmul_self]
    _ = (d • a) ⊗ₜ (d • a) := by simp [ha.comul_eq_tmul_self, smul_tmul, tmul_smul, -neg_smul]
    _ = ∑ x ∈ s, ∑ y ∈ s, (c x * c y) • x ⊗ₜ[R] y := by
      simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
key :
  Eq (α := A ⊗[R] A) (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (if x = y then d * c x else 0) (x ⊗ₜ[R] y))
    (∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x * c y) (x ⊗ₜ[R] y))
⊢ d = 0
have key₁ : Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (if x.1 = x.2 then d * c x.1 else 0) (x.1 ⊗ₜ[R] x.2))
  (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (c x.1 * c x.2) (x.1 ⊗ₜ[R] x.2))
Tactic: simp_rw [← Finset.sum_product'] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
key :
  Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (if x.1 = x.2 then d * c x.1 else 0) (x.1 ⊗ₜ[R] x.2))
    (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (c x.1 * c x.2) (x.1 ⊗ₜ[R] x.2))
⊢ d = 0
have key₁ : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
Tactic: apply ih at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hx : x ∈ s
⊢ c x = 0
have by_contra! : ∀ (hcx : c x ≠ 0), False
Tactic: by_contra! hcx
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hx : x ∈ s
hcx : c x ≠ 0
⊢ False
have hcy : ∀ (y : A) (hys : y ∈ s) (hyx : y ≠ x), c y = 0
Tactic: have hcy (y) (hys : y ∈ s) (hyx : y ≠ x) : c y = 0 := by
      simpa [*] using (key (y, x) (by simp [*])).symm
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ (y : A) (hys : y ∈ s) (hyx : y ≠ x), c y = 0
⊢ False
have hc₁ : c x • x = d • a
Tactic: rw [Finset.sum_eq_single x (by simp +contextual [hcy]) (by simp [hx])] at hc
Cleared hypotheses: hc, hx, hcx, hcy
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ (y : A) (hys : y ∈ s) (hyx : y ≠ x), c y = 0
⊢ False
have hcxa : d = c x
Tactic: have hcxa : d = c x := mul_left_injective₀ hcx (by simpa using (key (x, x) (by simp [*])))
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ (y : A) (hys : y ∈ s) (hyx : y ≠ x), c y = 0
hcxa : d = c x
⊢ x = a
have rwa : ∀ (hc : c x • x = c x • a) (hx : x ∈ s) (hcx : c x ≠ 0) (hcy : ∀ (y : A) (hys : y ∈ s) (hyx : y ≠ x), c y = 0)
  (hcxa : d = c x), x = a
Tactic: rwa [hcxa, smul_right_inj hcx] at hc
Cleared hypotheses: hc, hx, hcx, hcy, hcxa
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ (y : A) (hys : y ∈ s) (hyx : y ≠ x), c y = 0
hcxa : d = c x
rwa :
  ∀ (hc : c x • x = c x • a) (hx : x ∈ s) (hcx : c x ≠ 0) (hcy : ∀ (y : A) (hys : y ∈ s) (hyx : y ≠ x), c y = 0)
    (hcxa : d = c x), x = a
⊢ x = a
have rwa₁ : ∀ (hc : x = a) (hx : x ∈ s) (hcx : c x ≠ 0) (hcy : ∀ (y : A) (hys : y ∈ s) (hyx : y ≠ x), c y = 0) (hcxa : d = c x),
  x = a
Tactic: rwa [hcxa, smul_right_inj hcx] at hc
Cleared hypotheses: hc, hx, hcx, hcy, hcxa
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ (y : A) (hys : y ∈ s) (hyx : y ≠ x), c y = 0
hcxa : d = c x
⊢ False
have has₁ : x ∉ s
Tactic: obtain rfl : x = a := by rwa [hcxa, smul_right_inj hcx] at hc
Cleared hypotheses: a, has, ha, hc
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ (y : A) (hys : y ∈ s) (hyx : y ≠ x), c y = 0
hcxa : d = c x
has₁ : x ∉ s
⊢ False
have ha₁ : IsGroupLikeElem R x
Tactic: obtain rfl : x = a := by rwa [hcxa, smul_right_inj hcx] at hc
Cleared hypotheses: a, has, ha, hc
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ (y : A) (hys : y ∈ s) (hyx : y ≠ x), c y = 0
hcxa : d = c x
has₁ : x ∉ s
ha₁ : IsGroupLikeElem R x
⊢ False
have hc₁ : c x • x = d • x
Tactic: obtain rfl : x = a := by rwa [hcxa, smul_right_inj hcx] at hc
Cleared hypotheses: a, has, ha, hc
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R),
    Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
        (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
      ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
⊢ d = 0
have key₁ : ∀ (x : A) (hx : x ∈ s), c x = 0
Tactic: replace key x (hx : x ∈ s) : c x = 0 := by
    -- Otherwise, we deduce from `key` that `c y = 0` for any `y ≠ x` with `y ∈ s`.
    by_contra! hcx
    have hcy (y) (hys : y ∈ s) (hyx : y ≠ x) : c y = 0 := by
      simpa [*] using (key (y, x) (by simp [*])).symm
    -- Then substitute this into `hc` to get `c x • x = d • a`.
    rw [Finset.sum_eq_single x (by simp +contextual [hcy]) (by simp [hx])] at hc
    -- But `key` also says that `c x = d`.
    have hcxa : d = c x := mul_left_injective₀ hcx (by simpa using (key (x, x) (by simp [*])))
    -- So `x = a`...
    obtain rfl : x = a := by rwa [hcxa, smul_right_inj hcx] at hc
    -- ... which contradicts `x ∈ s` and `a ∉ s`.
    contradiction
Cleared hypotheses: key