mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: case fst
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → Semiring (A₁ i)
inst✝⁶ : (i : ι) → Semiring (A₂ i)
inst✝⁵ : (i : ι) → Semiring (A₃ i)
inst✝⁴ : (i : ι) → Algebra R (A₁ i)
inst✝³ : (i : ι) → Algebra R (A₂ i)
inst✝² : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
x✝¹ : R
x✝ : α
⊢ ((RingEquiv.sumArrowEquivProdArrow α β S) ((algebraMap R (α ⊕ β → S)) x✝¹)).1 x✝ =
    ((algebraMap R ((α → S) × (β → S))) x✝¹).1 x✝

pp: case snd
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → Semiring (A₁ i)
inst✝⁶ : (i : ι) → Semiring (A₂ i)
inst✝⁵ : (i : ι) → Semiring (A₃ i)
inst✝⁴ : (i : ι) → Algebra R (A₁ i)
inst✝³ : (i : ι) → Algebra R (A₂ i)
inst✝² : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
x✝¹ : R
x✝ : β
⊢ ((RingEquiv.sumArrowEquivProdArrow α β S) ((algebraMap R (α ⊕ β → S)) x✝¹)).2 x✝ =
    ((algebraMap R ((α → S) × (β → S))) x✝¹).2 x✝

Tactic:
<;>

Goal state after:
case fst
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → Semiring (A₁ i)
inst✝⁶ : (i : ι) → Semiring (A₂ i)
inst✝⁵ : (i : ι) → Semiring (A₃ i)
inst✝⁴ : (i : ι) → Algebra R (A₁ i)
inst✝³ : (i : ι) → Algebra R (A₂ i)
inst✝² : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
x✝¹ : R
x✝ : α
⊢ ((RingEquiv.sumArrowEquivProdArrow α β S) ((algebraMap R (α ⊕ β → S)) x✝¹)).1 x✝ =
    ((algebraMap R ((α → S) × (β → S))) x✝¹).1 x✝

case snd
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → Semiring (A₁ i)
inst✝⁶ : (i : ι) → Semiring (A₂ i)
inst✝⁵ : (i : ι) → Semiring (A₃ i)
inst✝⁴ : (i : ι) → Algebra R (A₁ i)
inst✝³ : (i : ι) → Algebra R (A₂ i)
inst✝² : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
x✝¹ : R
x✝ : β
⊢ ((RingEquiv.sumArrowEquivProdArrow α β S) ((algebraMap R (α ⊕ β → S)) x✝¹)).2 x✝ =
    ((algebraMap R ((α → S) × (β → S))) x✝¹).2 x✝
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case «0»
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ ![(a * d - b * c) • x, (a * d - b * c) • y] ((fun i ↦ i) ⟨0, ⋯⟩) =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)] ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ ![(a * d - b * c) • x, (a * d - b * c) • y] ((fun i ↦ i) ⟨1, ⋯⟩) =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ ![(a * d - b * c) • x, (a * d - b * c) • y] ((fun i ↦ i) ⟨0, ⋯⟩) =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ ![(a * d - b * c) • x, (a * d - b * c) • y] ((fun i ↦ i) ⟨1, ⋯⟩) =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case «0»
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ (a * d - b * c) • x = d • a • x + d • b • y + (-(b • c • x) + -(b • d • y))

pp: case «1»
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ (a * d - b * c) • y = -(c • a • x) + -(c • b • y) + (a • c • x + a • d • y)

Tactic:
<;>

Goal state after:
case «0»
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ (a * d - b * c) • x = d • a • x + d • b • y + (-(b • c • x) + -(b • d • y))

case «1»
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ (a * d - b * c) • y = -(c • a • x) + -(c • b • y) + (a • c • x + a • d • y)
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∉ a.support ↔ (coeff x) a = 0

Tactic:
rw [support, Finsupp.notMem_support_iff]
  exact Iff.rfl

Goal state after:
Module: Mathlib.Algebra.Module.BigOperators

Goal state before:
pp: case h₀
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ ∀ b ∈ univ, b ≠ i₀ → Pi.single i₀ r b • f b = 0

pp: case h₁
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ i₀ ∉ univ → Pi.single i₀ r i₀ • f i₀ = 0

Tactic:
<;>

Goal state after:
case h₀
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ ∀ b ∈ univ, b ≠ i₀ → Pi.single i₀ r b • f b = 0

case h₁
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ i₀ ∉ univ → Pi.single i₀ r i₀ • f i₀ = 0
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case empty
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
⊢ ⇑(∏ i ∈ ∅, ψ i) = ∏ i ∈ ∅, ⇑(ψ i)

pp: case cons
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ⇑(∏ i ∈ s✝, ψ i) = ∏ i ∈ s✝, ⇑(ψ i)
⊢ ⇑(∏ i ∈ cons a✝¹ s✝ h✝, ψ i) = ∏ i ∈ cons a✝¹ s✝ h✝, ⇑(ψ i)

Tactic:
<;>

Goal state after:
case empty
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
⊢ ⇑(∏ i ∈ ∅, ψ i) = ∏ i ∈ ∅, ⇑(ψ i)

case cons
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ⇑(∏ i ∈ s✝, ψ i) = ∏ i ∈ s✝, ⇑(ψ i)
⊢ ⇑(∏ i ∈ cons a✝¹ s✝ h✝, ψ i) = ∏ i ∈ cons a✝¹ s✝ h✝, ⇑(ψ i)
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case empty
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
⊢ ⇑(∑ i ∈ ∅, ψ i) = ∏ i ∈ ∅, ⇑(ψ i)

pp: case cons
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ⇑(∑ i ∈ s✝, ψ i) = ∏ i ∈ s✝, ⇑(ψ i)
⊢ ⇑(∑ i ∈ cons a✝¹ s✝ h✝, ψ i) = ∏ i ∈ cons a✝¹ s✝ h✝, ⇑(ψ i)

Tactic:
<;>

Goal state after:
case empty
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
⊢ ⇑(∑ i ∈ ∅, ψ i) = ∏ i ∈ ∅, ⇑(ψ i)

case cons
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ⇑(∑ i ∈ s✝, ψ i) = ∏ i ∈ s✝, ⇑(ψ i)
⊢ ⇑(∑ i ∈ cons a✝¹ s✝ h✝, ψ i) = ∏ i ∈ cons a✝¹ s✝ h✝, ⇑(ψ i)
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
x✝¹ x✝ : A
⊢ { toFun := fun ψ ↦ ψ (x✝¹ + x✝), map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } =
    { toFun := fun ψ ↦ ψ x✝¹, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } +
      { toFun := fun ψ ↦ ψ x✝, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }

Tactic:
ext; simp [map_add_eq_mul]

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case ofNat
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ : AddChar A M
a : A
a✝ : ℕ
⊢ (Int.ofNat a✝ • ψ) a = ψ a ^ Int.ofNat a✝

pp: case negSucc
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ : AddChar A M
a : A
a✝ : ℕ
⊢ (Int.negSucc a✝ • ψ) a = ψ a ^ Int.negSucc a✝

Tactic:
<;>

Goal state after:
case ofNat
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ : AddChar A M
a : A
a✝ : ℕ
⊢ (Int.ofNat a✝ • ψ) a = ψ a ^ Int.ofNat a✝

case negSucc
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ : AddChar A M
a : A
a✝ : ℕ
⊢ (Int.negSucc a✝ • ψ) a = ψ a ^ Int.negSucc a✝
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ ψ⁻¹ x✝ = (ψ.mulShift (-1)) x✝

Tactic:
rw [inv_apply, mulShift_apply, neg_mul, one_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
a0 : a ≠ 0
⊢ 1 = a⁻¹ * (a * 1)

pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
a0 : a ≠ 0
⊢ 0 = a⁻¹ * 1 + -a⁻¹ * 1

Tactic:
<;>

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
a0 : a ≠ 0
⊢ 1 = a⁻¹ * (a * 1)

K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
a0 : a ≠ 0
⊢ 0 = a⁻¹ * 1 + -a⁻¹ * 1
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
s : Set M
h : of' R M m ∈ Submodule.span R ↑(Submonoid.closure (of' R M '' s))
⊢ m ∈ AddSubmonoid.closure s

Tactic:
suffices Multiplicative.ofAdd m ∈ Submonoid.closure (Multiplicative.toAdd ⁻¹' s) by
    simpa [← AddSubmonoid.toSubmonoid_closure]

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
s : Set M
h : of' R M m ∈ Submodule.span R ↑(Submonoid.closure (of' R M '' s))
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' s)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case e'_3
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
x✝ : Set V
⊢ t = id '' t

pp: case e'_4
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
x✝ : Set V
⊢ x✝ = id '' x✝

Tactic:
<;>

Goal state after:
case e'_3
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
x✝ : Set V
⊢ t = id '' t

case e'_4
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
x✝ : Set V
⊢ x✝ = id '' x✝
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case e'_3
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ t = id '' t

pp: case e'_4
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ hs.extend hst = id '' hs.extend hst

Tactic:
<;>

Goal state after:
case e'_3
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ t = id '' t

case e'_4
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ hs.extend hst = id '' hs.extend hst
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: case h₁
R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
r✝ : R
a✝ : M
⊢ ((mapDomainRingHom R (MonoidHom.id M)) (single 1 r✝)).coeff a✝ = ((RingHom.id R[M]) (single 1 r✝)).coeff a✝

pp: case h_of
R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
m✝ a✝ : M
⊢ ((mapDomainRingHom R (MonoidHom.id M)) (single m✝ 1)).coeff a✝ = ((RingHom.id R[M]) (single m✝ 1)).coeff a✝

Tactic:
<;>

Goal state after:
case h₁
R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
r✝ : R
a✝ : M
⊢ ((mapDomainRingHom R (MonoidHom.id M)) (single 1 r✝)).coeff a✝ = ((RingHom.id R[M]) (single 1 r✝)).coeff a✝

case h_of
R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
m✝ a✝ : M
⊢ ((mapDomainRingHom R (MonoidHom.id M)) (single m✝ 1)).coeff a✝ = ((RingHom.id R[M]) (single m✝ 1)).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: case h₁
R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst✝³ : Semiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : N →* O
g : M →* N
r✝ : R
a✝ : O
⊢ ((mapDomainRingHom R (f.comp g)) (single 1 r✝)).coeff a✝ =
    (((mapDomainRingHom R f).comp (mapDomainRingHom R g)) (single 1 r✝)).coeff a✝

pp: case h_of
R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst✝³ : Semiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : N →* O
g : M →* N
m✝ : M
a✝ : O
⊢ ((mapDomainRingHom R (f.comp g)) (single m✝ 1)).coeff a✝ =
    (((mapDomainRingHom R f).comp (mapDomainRingHom R g)) (single m✝ 1)).coeff a✝

Tactic:
<;>

Goal state after:
case h₁
R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst✝³ : Semiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : N →* O
g : M →* N
r✝ : R
a✝ : O
⊢ ((mapDomainRingHom R (f.comp g)) (single 1 r✝)).coeff a✝ =
    (((mapDomainRingHom R f).comp (mapDomainRingHom R g)) (single 1 r✝)).coeff a✝

case h_of
R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst✝³ : Semiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : N →* O
g : M →* N
m✝ : M
a✝ : O
⊢ ((mapDomainRingHom R (f.comp g)) (single m✝ 1)).coeff a✝ =
    (((mapDomainRingHom R f).comp (mapDomainRingHom R g)) (single m✝ 1)).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: case h₁
R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
r✝ : R
a✝ : M
⊢ ((mapRingHom M (RingHom.id R)) (single 1 r✝)).coeff a✝ = ((RingHom.id R[M]) (single 1 r✝)).coeff a✝

pp: case h_of
R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
m✝ a✝ : M
⊢ ((mapRingHom M (RingHom.id R)) (single m✝ 1)).coeff a✝ = ((RingHom.id R[M]) (single m✝ 1)).coeff a✝

Tactic:
<;>

Goal state after:
case h₁
R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
r✝ : R
a✝ : M
⊢ ((mapRingHom M (RingHom.id R)) (single 1 r✝)).coeff a✝ = ((RingHom.id R[M]) (single 1 r✝)).coeff a✝

case h_of
R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
m✝ a✝ : M
⊢ ((mapRingHom M (RingHom.id R)) (single m✝ 1)).coeff a✝ = ((RingHom.id R[M]) (single m✝ 1)).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: case h₁
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Semiring T
inst✝ : Monoid M
f : S →+* T
g : R →+* S
r✝ : R
a✝ : M
⊢ ((mapRingHom M (f.comp g)) (single 1 r✝)).coeff a✝ = (((mapRingHom M f).comp (mapRingHom M g)) (single 1 r✝)).coeff a✝

pp: case h_of
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Semiring T
inst✝ : Monoid M
f : S →+* T
g : R →+* S
m✝ a✝ : M
⊢ ((mapRingHom M (f.comp g)) (single m✝ 1)).coeff a✝ = (((mapRingHom M f).comp (mapRingHom M g)) (single m✝ 1)).coeff a✝

Tactic:
<;>

Goal state after:
case h₁
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Semiring T
inst✝ : Monoid M
f : S →+* T
g : R →+* S
r✝ : R
a✝ : M
⊢ ((mapRingHom M (f.comp g)) (single 1 r✝)).coeff a✝ = (((mapRingHom M f).comp (mapRingHom M g)) (single 1 r✝)).coeff a✝

case h_of
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Semiring T
inst✝ : Monoid M
f : S →+* T
g : R →+* S
m✝ a✝ : M
⊢ ((mapRingHom M (f.comp g)) (single m✝ 1)).coeff a✝ = (((mapRingHom M f).comp (mapRingHom M g)) (single m✝ 1)).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: case h₁
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (r : R), ((mapDomainRingHom R ↑e).comp (mapDomainRingHom R ↑e.symm)) (single 1 r) = (RingHom.id R[N]) (single 1 r)

pp: case h_of
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (m : N), ((mapDomainRingHom R ↑e).comp (mapDomainRingHom R ↑e.symm)) (single m 1) = (RingHom.id R[N]) (single m 1)

Tactic:
<;>

Goal state after:
case h₁
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (r : R), ((mapDomainRingHom R ↑e).comp (mapDomainRingHom R ↑e.symm)) (single 1 r) = (RingHom.id R[N]) (single 1 r)

case h_of
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (m : N), ((mapDomainRingHom R ↑e).comp (mapDomainRingHom R ↑e.symm)) (single m 1) = (RingHom.id R[N]) (single m 1)
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: case h₁
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (r : R), ((mapDomainRingHom R ↑e.symm).comp (mapDomainRingHom R ↑e)) (single 1 r) = (RingHom.id R[M]) (single 1 r)

pp: case h_of
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (m : M), ((mapDomainRingHom R ↑e.symm).comp (mapDomainRingHom R ↑e)) (single m 1) = (RingHom.id R[M]) (single m 1)

Tactic:
<;>

Goal state after:
case h₁
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (r : R), ((mapDomainRingHom R ↑e.symm).comp (mapDomainRingHom R ↑e)) (single 1 r) = (RingHom.id R[M]) (single 1 r)

case h_of
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (m : M), ((mapDomainRingHom R ↑e.symm).comp (mapDomainRingHom R ↑e)) (single m 1) = (RingHom.id R[M]) (single m 1)
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: case h₁
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ ∀ (r : S), ((mapRingHom M ↑e).comp (mapRingHom M ↑e.symm)) (single 1 r) = (RingHom.id S[M]) (single 1 r)

pp: case h_of
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ ∀ (m : M), ((mapRingHom M ↑e).comp (mapRingHom M ↑e.symm)) (single m 1) = (RingHom.id S[M]) (single m 1)

Tactic:
<;>

Goal state after:
case h₁
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ ∀ (r : S), ((mapRingHom M ↑e).comp (mapRingHom M ↑e.symm)) (single 1 r) = (RingHom.id S[M]) (single 1 r)

case h_of
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ ∀ (m : M), ((mapRingHom M ↑e).comp (mapRingHom M ↑e.symm)) (single m 1) = (RingHom.id S[M]) (single m 1)