awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
ih : ∀ (hs : (↑s : Set A) ⊆ {a : A | IsGroupLikeElem R a}), LinearIndepOn R id (↑s : Set A)
hs : IsGroupLikeElem R a ∧ ∀ a ∈ s, IsGroupLikeElem R a
ha : IsGroupLikeElem R a
⊢ ∀ a ∈ s, IsGroupLikeElem R a

Tactic:
obtain ⟨ha, hs⟩ := hs
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
ih : ∀ (hs : (↑s : Set A) ⊆ {a : A | IsGroupLikeElem R a}), LinearIndepOn R id (↑s : Set A)
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
⊢ LinearIndepOn R id (↑s : Set A)

Tactic:
specialize ih hs
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
ih : LinearIndepOn R id (↑s : Set A)
cons : LinearIndepOn R id (insert a (↑s : Set A))
⊢ LinearIndepOn R id (↑(Finset.cons a s has) : Set A)

Tactic:
rw [Finset.coe_cons]

Premises used: Finset.coe_cons
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
ih : LinearIndepOn R id (↑s : Set A)
⊢ LinearIndepOn R id (insert a (↑s : Set A))

Tactic:
ih.id_insert' ?_

Premises used: LinearIndepOn.id_insert'
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
ih : LinearIndepOn R id (↑s : Set A)
cons : ∀ (r : R), Membership.mem (γ := Submodule R A) (span R (↑s : Set A)) (r • a) → r = 0
⊢ LinearIndepOn R id (insert a (↑s : Set A))

Tactic:
refine ih.id_insert' ?_

Premises used: LinearIndepOn.id_insert'
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
ih : LinearIndepOn R id (↑s : Set A)
cons : ∀ (r : R) (x : A → R), support x ⊆ (↑s : Set A) → ∑ a ∈ s, x a • a = r • a → r = 0
⊢ ∀ (r : R), Membership.mem (γ := Submodule R A) (span R (↑s : Set A)) (r • a) → r = 0

Tactic:
simp only [mem_span_finset, forall_exists_index, and_imp]

Premises used: and_imp, Submodule.mem_span_finset, forall_exists_index
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
ih : LinearIndepOn R id (↑s : Set A)
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
⊢ LinearIndepOn R (M := A ⊗[R] A) (fun (i : A × A) ↦ id i.1 ⊗ₜ[R] id i.2) ((↑s : Set A) ×ˢ (↑s : Set A))

Tactic:
replace ih := ih.tmul_of_isDomain ih
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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 : LinearIndepOn R (M := A ⊗[R] A) (fun (i : A × A) ↦ id i.1 ⊗ₜ[R] id i.2) ((↑s : Set A) ×ˢ (↑s : Set A))
⊢ ∀ (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

Tactic:
simp_rw [← Finset.coe_product, linearIndepOn_finset_iffₛ, id] at ih

Premises used: id, linearIndepOn_finset_iffₛ, Finset.coe_product
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
⊢ ∑ x ∈ s, ∑ y ∈ s, HSMul.hSMul (β := A ⊗[R] A) (if x = y then d * c x else 0) (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := A ⊗[R] A) d (∑ x ∈ s, HSMul.hSMul (β := A ⊗[R] A) (c x) (x ⊗ₜ[R] x))

Tactic:
simp [Finset.smul_sum, mul_smul]

Premises used: Finset.smul_sum, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
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))
⊢ 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)

Tactic:
rw [← hc]
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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) (∑ a ∈ s, c a • a))

Tactic:
simp +contextual [(hs _ _).comul_eq_tmul_self]

Premises used: IsGroupLikeElem.comul_eq_tmul_self
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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 ((comul : (a : A) → A ⊗[R] A) (d • a) : A ⊗[R] A) = (d • a) ⊗ₜ[R] (d • a)

Tactic:
simp [ha.comul_eq_tmul_self, smul_tmul, tmul_smul, -neg_smul]

Premises used: IsGroupLikeElem.comul_eq_tmul_self, neg_smul, TensorProduct.smul_tmul, TensorProduct.tmul_smul
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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))
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))
⊢ 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))

Tactic:
simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]

Premises used: TensorProduct.smul_tmul, TensorProduct.tmul_smul, TensorProduct.sum_tmul, TensorProduct.tmul_sum, Finset.smul_sum, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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) (∑ 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]
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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))
⊢ 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

Premises used: Finset.sum_product'
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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))
⊢ ∀ 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
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
by_contra! : ∀ (hcx : c x ≠ 0), False
⊢ c x = 0

Tactic:
by_contra! hcx
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
y : A
hys : y ∈ s
hyx : y ≠ x
⊢ (y, x) ∈ s ×ˢ s

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
y : A
hys : y ∈ s
hyx : y ≠ x
⊢ c y = 0

Tactic:
simpa [*] using (key (y, x) (by simp [*])).symm

Premises used: Prod.mk, Eq.symm
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
⊢ ∀ (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
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
⊢ ∀ b ∈ s, b ≠ x → c b • b = 0

Tactic:
simp +contextual [hcy]
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
⊢ x ∉ s → c x • x = 0

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
⊢ c x • x = d • a

Tactic:
rw [Finset.sum_eq_single x (by simp +contextual [hcy]) (by simp [hx])] at hc

Premises used: Finset.sum_eq_single
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
hc₁ : c x • x = d • a
⊢ x ∈ s

Tactic:
rw [Finset.sum_eq_single x (by simp +contextual [hcy]) (by simp [hx])] at hc

Premises used: Finset.sum_eq_single
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
hc₁ : c x • x = d • a
hx₁ : x ∈ s
⊢ c x ≠ 0

Tactic:
rw [Finset.sum_eq_single x (by simp +contextual [hcy]) (by simp [hx])] at hc

Premises used: Finset.sum_eq_single
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
hc₁ : c x • x = d • a
hx₁ : x ∈ s
hcx₁ : c x ≠ 0
⊢ ∀ (y : A) (hys : y ∈ s) (hyx : y ≠ x), c y = 0

Tactic:
rw [Finset.sum_eq_single x (by simp +contextual [hcy]) (by simp [hx])] at hc

Premises used: Finset.sum_eq_single
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
⊢ (x, x) ∈ s ×ˢ s

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
⊢ Eq.{u_2 + 1} (α := R) ((fun (a : R) ↦ a * c x) d) ((fun (a : R) ↦ a * c x) (c x))

Tactic:
simpa using (key (x, x) (by simp [*]))

Premises used: Prod.mk
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
⊢ d = c x

Tactic:
have hcxa : d = c x := mul_left_injective₀ hcx (by simpa using (key (x, x) (by simp [*])))