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
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
rwa₁ rwa₂ rwa₃ 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
⊢ x = a

Tactic:
rwa [hcxa, smul_right_inj hcx] at hc

Premises used: smul_right_inj
-- 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
hcxa : d = c x
⊢ x ∉ s

Tactic:
obtain rfl : x = a := by rwa [hcxa, smul_right_inj hcx] at hc

Premises used: rfl
-- 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
hcxa : d = c x
has₁ : x ∉ s
⊢ IsGroupLikeElem R x

Tactic:
obtain rfl : x = a := by rwa [hcxa, smul_right_inj hcx] at hc

Premises used: rfl
-- 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
hcxa : d = c x
has₁ : x ∉ s
ha₁ : IsGroupLikeElem R x
⊢ c x • x = d • x

Tactic:
obtain rfl : x = a := by rwa [hcxa, smul_right_inj hcx] at hc

Premises used: rfl
-- 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
s : Finset 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
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
hc : c x • x = d • x
⊢ False

Tactic:
contradiction
-- 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), 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
-- 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 : ∀ (x : A) (hx : x ∈ s), c x = 0
⊢ d = 0

Tactic:
simp_all [ha.ne_zero, eq_comm]

Premises used: eq_comm, IsGroupLikeElem.ne_zero
-- 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
⊢ LinearIndependent.{u_3, u_2, u_3} (ι := GroupLike R A) R GroupLike.val

Tactic:
simpa using (linearIndependent_equiv GroupLike.valEquiv).2 linearIndepOn_isGroupLikeElem

Premises used: Iff.mpr, GroupLike.valEquiv, linearIndependent_equiv, linearIndepOn_isGroupLikeElem
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
F : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
inst_7 : FunLike F A B
inst_8 : CoalgHomClass F R A B
f : F
x : A
⊢ Eq.{u_1 + 1} (α := R) ((counit : (a : B) → R) ((f : (a : A) → B) x : B) : R) ((counit : (a : A) → R) x : R)

Tactic:
LinearMap.congr_fun (counit_comp f) _

Premises used: LinearMap.congr_fun, CoalgHomClass.counit_comp
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
F : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
inst_7 : FunLike F A B
inst_8 : CoalgHomClass F R A B
f : F
x : A
⊢ Eq (α := B ⊗[R] B)
    (((map (↑f : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
              (↑f : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
            LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (A ⊗[R] A) (B ⊗[R] B)) :
          (a : A ⊗[R] A) → B ⊗[R] B)
        ((comul : (a : A) → A ⊗[R] A) x) :
      B ⊗[R] B)
    ((comul : (a : B) → B ⊗[R] B) ((f : (a : A) → B) x) : B ⊗[R] B)

Tactic:
LinearMap.congr_fun (map_comp_comul f) _

Premises used: Quotient.liftOn', AddCon.liftOn, CoalgHomClass.map_comp_comul, LinearMap.congr_fun
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : AddCommMonoid D
inst_8 : Module R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
f g : A →ₗc[R] B
h : Eq (α := (a : A) → B) ((fun (f : A →ₗc[R] B) ↦ f.toFun) f) ((fun (f : A →ₗc[R] B) ↦ f.toFun) g)
rcases :
  ∀ (toFun : A → B) (map_add' : ∀ (x y : A), toFun (x + y) = toFun x + toFun y)
    (map_smul' :
      ∀ (m : R) (x : A),
        { toFun := toFun, map_add' := map_add' : A →ₙ+ B }.toFun (m • x) =
          HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
            ({ toFun := toFun, map_add' := map_add' : A →ₙ+ B }.toFun x))
    (counit_comp : counit ∘ₗ { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B } = counit)
    (map_comp_comul :
      map { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B }
            { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B } ∘ₗ
          comul =
        comul ∘ₗ { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B })
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : A →ₗc[R] B) ↦ f.toFun)
          { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
            map_comp_comul := map_comp_comul })
        ((fun (f : A →ₗc[R] B) ↦ f.toFun) g)),
    { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
        map_comp_comul := map_comp_comul : A →ₗc[R] B } =
      g
⊢ f = g

Tactic:
rcases f with ⟨⟨⟨_, _⟩, _⟩, _, _⟩
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : AddCommMonoid D
inst_8 : Module R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
g : A →ₗc[R] B
toFun : A → B
map_add' : ∀ (x y : A), toFun (x + y) = toFun x + toFun y
map_smul' :
  ∀ (m : R) (x : A),
    { toFun := toFun, map_add' := map_add' : A →ₙ+ B }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        ({ toFun := toFun, map_add' := map_add' : A →ₙ+ B }.toFun x)
counit_comp : counit ∘ₗ { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B } = counit
map_comp_comul :
  map { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B }
        { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B } ∘ₗ
      comul =
    comul ∘ₗ { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B }
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →ₗc[R] B) ↦ f.toFun)
      { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
        map_comp_comul := map_comp_comul })
    ((fun (f : A →ₗc[R] B) ↦ f.toFun) g)
rcases :
  ∀ (toFun_1 : A → B) (map_add'_1 : ∀ (x y : A), toFun_1 (x + y) = toFun_1 x + toFun_1 y)
    (map_smul'_1 :
      ∀ (m : R) (x : A),
        { toFun := toFun_1, map_add' := map_add'_1 : A →ₙ+ B }.toFun (m • x) =
          HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
            ({ toFun := toFun_1, map_add' := map_add'_1 : A →ₙ+ B }.toFun x))
    (counit_comp_1 :
      counit ∘ₗ { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : A →ₗ[R] B } = counit)
    (map_comp_comul_1 :
      map { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : A →ₗ[R] B }
            { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : A →ₗ[R] B } ∘ₗ
          comul =
        comul ∘ₗ { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : A →ₗ[R] B })
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : A →ₗc[R] B) ↦ f.toFun)
          { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
            map_comp_comul := map_comp_comul })
        ((fun (f : A →ₗc[R] B) ↦ f.toFun)
          { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1, counit_comp := counit_comp_1,
            map_comp_comul := map_comp_comul_1 })),
    { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
        map_comp_comul := map_comp_comul : A →ₗc[R] B } =
      { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1, counit_comp := counit_comp_1,
        map_comp_comul := map_comp_comul_1 }
⊢ { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
      map_comp_comul := map_comp_comul : A →ₗc[R] B } =
    g

Tactic:
rcases g with ⟨⟨⟨_, _⟩, _⟩, _, _⟩
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : AddCommMonoid D
inst_8 : Module R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
toFun : A → B
map_add' : ∀ (x y : A), toFun (x + y) = toFun x + toFun y
map_smul' :
  ∀ (m : R) (x : A),
    { toFun := toFun, map_add' := map_add' : A →ₙ+ B }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        ({ toFun := toFun, map_add' := map_add' : A →ₙ+ B }.toFun x)
counit_comp : counit ∘ₗ { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B } = counit
map_comp_comul :
  map { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B }
        { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B } ∘ₗ
      comul =
    comul ∘ₗ { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B }
toFun_1 : A → B
map_add'_1 : ∀ (x y : A), toFun_1 (x + y) = toFun_1 x + toFun_1 y
map_smul'_1 :
  ∀ (m : R) (x : A),
    { toFun := toFun_1, map_add' := map_add'_1 : A →ₙ+ B }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        ({ toFun := toFun_1, map_add' := map_add'_1 : A →ₙ+ B }.toFun x)
counit_comp_1 : counit ∘ₗ { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : A →ₗ[R] B } = counit
map_comp_comul_1 :
  map { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : A →ₗ[R] B }
        { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : A →ₗ[R] B } ∘ₗ
      comul =
    comul ∘ₗ { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : A →ₗ[R] B }
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →ₗc[R] B) ↦ f.toFun)
      { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
        map_comp_comul := map_comp_comul })
    ((fun (f : A →ₗc[R] B) ↦ f.toFun)
      { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1, counit_comp := counit_comp_1,
        map_comp_comul := map_comp_comul_1 })
⊢ { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
      map_comp_comul := map_comp_comul : A →ₗc[R] B } =
    { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1, counit_comp := counit_comp_1,
      map_comp_comul := map_comp_comul_1 }

Tactic:
congr
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
F : Type u_6
inst_7 : FunLike F A B
inst_8 : CoalgHomClass F R A B
f : F
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →ₗc[R] B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A →ₗ[R] B
h : counit ∘ₗ f = counit
h₁ : map f f ∘ₗ comul = comul ∘ₗ f
⊢ Eq (α := (a : A) → B) (⇑{ toLinearMap := f, counit_comp := h, map_comp_comul := h₁ : A →ₗc[R] B } : (a : A) → B)
    (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A → B
h₁ : ∀ (x y : A), f (x + y) = f x + f y
h₂ :
  ∀ (m : R) (x : A),
    { toFun := f, map_add' := h₁ : A →ₙ+ B }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) ({ toFun := f, map_add' := h₁ : A →ₙ+ B }.toFun x)
h₃ : counit ∘ₗ { toFun := f, map_add' := h₁, map_smul' := h₂ : A →ₗ[R] B } = counit
h₄ :
  map { toFun := f, map_add' := h₁, map_smul' := h₂ : A →ₗ[R] B }
        { toFun := f, map_add' := h₁, map_smul' := h₂ : A →ₗ[R] B } ∘ₗ
      comul =
    comul ∘ₗ { toFun := f, map_add' := h₁, map_smul' := h₂ : A →ₗ[R] B }
⊢ (⇑{ toFun := f, map_add' := h₁, map_smul' := h₂, counit_comp := h₃, map_comp_comul := h₄ : A →ₗc[R] B } :
      (a : A) → B) =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A →ₗ[R] B
h : counit ∘ₗ f = counit
h₁ : map f f ∘ₗ comul = comul ∘ₗ f
⊢ (↑{ toLinearMap := f, counit_comp := h, map_comp_comul := h₁ : A →ₗc[R] B } :
      [inst_7 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B) =
    f

Tactic:
rfl

Premises used: SemilinearMapClass.semilinearMap, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A →ₗc[R] B
⊢ f.toLinearMap =
    (↑f : [inst_7 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B)

Tactic:
rfl

Premises used: SemilinearMapClass.semilinearMap, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A →ₗc[R] B
⊢ Eq (α := (a : A) → B)
    (⇑(↑f : [inst_7 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
      (a : A) → B)
    (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A →ₗc[R] B
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →+ B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
⊢ Function.Injective (α := A →ₗc[R] B) (β := A → B) (DFunLike.coe (β := fun (x : A) ↦ B))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ₁ φ₂ : A →ₗc[R] B
⊢ Eq (α := (a : A) → B) (⇑φ₁ : (a : A) → B) (⇑φ₂ : (a : A) → B) ↔ φ₁ = φ₂

Tactic:
DFunLike.coe_fn_eq

Premises used: DFunLike.coe_fn_eq
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
⊢ Function.Injective (β := A →ₗ[R] B) fun (x : A →ₗc[R] B) ↦
    (↑x : [inst_7 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B)

Tactic:
fun φ₁ φ₂ H => coe_fn_injective <|
    show ((φ₁ : A →ₗ[R] B) : A → B) = ((φ₂ : A →ₗ[R] B) : A → B) from congr_arg _ H

Premises used: congr_arg, CoalgHom.coe_fn_injective, Function.Injective, DFunLike.coe
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
⊢ Function.Injective (α := A →ₗc[R] B) (β := A →+ B) AddMonoidHomClass.toAddMonoidHom

Tactic:
LinearMap.toAddMonoidHom_injective.comp coe_linearMap_injective

Premises used: LinearMap.toAddMonoidHom, AddMonoidHomClass.toAddMonoidHom, LinearMap.toAddMonoidHom_injective, CoalgHom.coe_linearMap_injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ₁ φ₂ : A →ₗc[R] B
H : φ₁ = φ₂
x : A
⊢ Eq.{u_3 + 1} (α := B) ((φ₁ : (a : A) → B) x : B) ((φ₂ : (a : A) → B) x : B)

Tactic:
DFunLike.congr_fun H x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ : A →ₗc[R] B
x y : A
h : x = y
⊢ Eq.{u_3 + 1} (α := B) ((φ : (a : A) → B) x : B) ((φ : (a : A) → B) y : B)

Tactic:
DFunLike.congr_arg φ h

Premises used: DFunLike.congr_arg
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ₁ φ₂ : A →ₗc[R] B
H : ∀ (x : A), Eq.{u_3 + 1} (α := B) ((φ₁ : (a : A) → B) x : B) ((φ₂ : (a : A) → B) x : B)
⊢ φ₁ = φ₂

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.ext