mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : Subsingleton m
A : Matrix m n R
i : m
b : n → R
⊢ A.updateRow i b = (replicateRow (Fin 1) b).submatrix (Function.const m 0) id

Tactic:
ext x y

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : Subsingleton m
A : Matrix m n R
i : m
b : n → R
x : m
y : n
⊢ A.updateRow i b x y = (replicateRow (Fin 1) b).submatrix (Function.const m 0) id x y
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (diagonal d).blockDiag k i j = diagonal (fun i ↦ d (i, k)) i j

Tactic:
· rw [blockDiag_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt _ hij)]
      exact Prod.fst_eq_iff.mpr

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
⊢ x ∈ N → x = 0

Tactic:
hx

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
⊢ x = 0
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
⊢ x ∈ N → x = 0

Tactic:
hx

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
⊢ x = 0
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
x : O
⊢ x ∈ N' → x ∈ M'

Tactic:
hx

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
x : O
hx : x ∈ N'
⊢ x ∈ M'
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
c : Rᵐᵒᵖ
f : (m → R) →ₗ[R] n → R
⊢ (fun i j ↦ (c • f) ((single R (fun x ↦ R) i) 1) j) = (RingHom.id Rᵐᵒᵖ) c • fun i j ↦ f ((single R (fun x ↦ R) i) 1) j

Tactic:
ext i j
    simp only [Pi.smul_apply, LinearMap.smul_apply, RingHom.id_apply, Matrix.smul_apply]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
ms : M × ↥S
eq : 0 * f ↑ms.2 = f ms.1
⊢ f 0 = 0

Tactic:
← zero_mul,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
ms : M × ↥S
eq : 0 * f ↑ms.2 = f ms.1
⊢ f (0 * ?m.37) = 0

M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
ms : M × ↥S
eq : 0 * f ↑ms.2 = f ms.1
⊢ M
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
f : S.LocalizationMap N
ms : M × ↥S
eq : 0 * f ↑ms.2 = f ms.1
⊢ f 0 = 0

Tactic:
← zero_mul,

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
f : S.LocalizationMap N
ms : M × ↥S
eq : 0 * f ↑ms.2 = f ms.1
⊢ f (0 * ?m.42) = 0

M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
f : S.LocalizationMap N
ms : M × ↥S
eq : 0 * f ↑ms.2 = f ms.1
⊢ M
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
⊢ (toMatrix b b) 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
⊢ 0 = 0
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
z₁ z₂ : S
⊢ mk' S x y + z₁ = z₂ ↔ (algebraMap R S) x + z₁ * (algebraMap R S) ↑y = z₂ * (algebraMap R S) ↑y

Tactic:
rw [← mk'_spec S x y, ← IsUnit.mul_left_inj (IsLocalization.map_units S y), right_distrib]

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * w + 1 * z₁ = z₂ ↔ w + g ↑y * (1 * z₁) = g ↑y * z₂

Tactic:
← Units.inv_mul (IsUnit.liftRight (g.toMonoidHom.domRestrict M) h y),

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * w +
        ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y) * z₁ =
      z₂ ↔
    w +
        g ↑y *
          (↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y) * z₁) =
      g ↑y * z₂
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
⊢ ∀ (y : ↥ℤ⁰), IsUnit ((algebraMap ℤ ℚ) ↑y)

Tactic:
rintro ⟨x, hx⟩
    rw [mem_nonZeroDivisors_iff_ne_zero] at hx
    simpa only [eq_intCast, isUnit_iff_ne_zero, Int.cast_eq_zero, Ne, Subtype.coe_mk] using hx

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ inst✝¹ = (algebraMap R S).toAlgebra

Tactic:
apply Algebra.algebra_ext

Goal state after:
case e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := ⋯
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ ∀ (r : R), (algebraMap R S) r = (algebraMap R S) r
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : Subsingleton R
a : Localization M
x✝ : R × ↥M
⊢ mk x✝.1 x✝.2 = mk 1 1

Tactic:
congr <;> apply Subsingleton.elim

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : x = 0
⊢ (algebraMap R S) 0 = 0

Tactic:
map_zero

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : x = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: case inr
R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
left✝ : Subsingleton R
right✝ : Nontrivial S
⊢ (algebraMap R S) 0 = 0

Tactic:
map_zero

Goal state after:
case inr
R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
left✝ : Subsingleton R
right✝ : Nontrivial S
⊢ 0 = 0
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : ↥J₂ ⊗[R] M
⊢ (rTensor M J₁.subtype) y₁ + (rTensor M J₂.subtype) y₂ =
    (rTensor M (J₁ ⊔ J₂).subtype) ((rTensor M (inclusion ⋯)) y₁) +
      (rTensor M (J₁ ⊔ J₂).subtype) ((rTensor M (inclusion ⋯)) y₂)

Tactic:
← rTensor_comp_apply,

Goal state after:
case add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
J₂ : Submodule R N
fg₂ : J₂.FG
y₂ : ↥J₂ ⊗[R] M
⊢ (rTensor M J₁.subtype) y₁ + (rTensor M J₂.subtype) y₂ =
    (rTensor M ((J₁ ⊔ J₂).subtype ∘ₗ inclusion ⋯)) y₁ + (rTensor M (J₁ ⊔ J₂).subtype) ((rTensor M (inclusion ⋯)) y₂)
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
⊢ Algebra.IsEpi R A

Tactic:
refine (isEpi_iff_forall_one_tmul_eq R A).mpr fun x ↦ ?_

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
x : A
⊢ 1 ⊗ₜ[R] x = x ⊗ₜ[R] 1
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = R ∙ x
⊢ R ∙ x = ⊤

Tactic:
hx

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = R ∙ x
⊢ R ∙ x = R ∙ x
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
nsmul : SMul ℕ α := ⋯
⊢ e 0 = 0

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
nsmul : SMul ℕ α := ⋯
⊢ e 0 = 0

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
⊢ e 0 = 0

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
⊢ e 1 = 1

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
n✝ : ℕ
⊢ e ↑n✝ = ↑n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 0 = 0

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 1 = 1

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case npow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n✝ : ℕ
⊢ e ↑n✝ = ↑n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
⊢ NonUnitalCommSemiring α

Tactic:
apply e.injective.nonUnitalCommSemiring _ <;> intros

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
nsmul : SMul ℕ α := ⋯
⊢ e 0 = 0

case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝

case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
nsmul : SMul ℕ α := ⋯
⊢ e 0 = 0

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 0 = 0

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 1 = 1

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case npow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n✝ : ℕ
⊢ e ↑n✝ = ↑n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ e 0 = 0

Tactic:
exact e.apply_symm_apply _

Goal state after: