mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
⊢ (toLinearMapRight' M') ((toLinearMapRight' M) x) = x

Tactic:
rw [← Matrix.toLinearMapRight'_mul_apply, hMM', Matrix.toLinearMapRight'_one, id_apply]

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
z : OreLocalization S R
y : OreLocalization S X
r₁ : X
s₁ : ↥S
⊢ z • (r₁ /ₒ s₁ + y) = z • (r₁ /ₒ s₁) + z • y

Tactic:
induction y with | _ r₂ s₂

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ z • (r₁ /ₒ s₁ + r₂ /ₒ s₂) = z • (r₁ /ₒ s₁) + z • (r₂ /ₒ s₂)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ i ∉ Finset.univ → M j i * (Finsupp.single i 1) i = 0

Tactic:
intros

Goal state after:
case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
a✝ : i ∉ Finset.univ
⊢ M j i * (Finsupp.single i 1) i = 0
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
y z : OreLocalization S R
r₁ : X
s₁ : ↥S
⊢ (y + z) • (r₁ /ₒ s₁) = y • (r₁ /ₒ s₁) + z • (r₁ /ₒ s₁)

Tactic:
induction y with | _ r₂ s₂

Goal state after:
case c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (r₂ /ₒ s₂ + z) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + z • (r₁ /ₒ s₁)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
y : OreLocalization S R
r₁ : R
s₁ : ↥S
⊢ (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁ + y) = (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁) + (universalMulHom (↑f) fS ⋯) y

Tactic:
induction y with | _ r₂ s₂

Goal state after:
case c.c
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁ + r₂ /ₒ s₂) =
    (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁) + (universalMulHom (↑f) fS ⋯) (r₂ /ₒ s₂)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : Matrix ι ι (End A M)
⊢ ∀ (x y : ι → M), (fun i ↦ ∑ j, (m i j) ((x + y) j)) = (fun i ↦ ∑ j, (m i j) (x j)) + fun i ↦ ∑ j, (m i j) (y j)

Tactic:
intros

Goal state after:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : Matrix ι ι (End A M)
x✝ y✝ : ι → M
⊢ (fun i ↦ ∑ j, (m i j) ((x✝ + y✝) j)) = (fun i ↦ ∑ j, (m i j) (x✝ j)) + fun i ↦ ∑ j, (m i j) (y✝ j)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : Matrix ι ι (End A M)
⊢ ∀ (m_1 : A) (x : ι → M), (fun i ↦ ∑ j, (m i j) ((m_1 • x) j)) = (RingHom.id A) m_1 • fun i ↦ ∑ j, (m i j) (x j)

Tactic:
intros

Goal state after:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : Matrix ι ι (End A M)
m✝ : A
x✝ : ι → M
⊢ (fun i ↦ ∑ j, (m i j) ((m✝ • x✝) j)) = (RingHom.id A) m✝ • fun i ↦ ∑ j, (m i j) (x✝ j)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case refine_1
A : Type u_3
inst✝ : Semiring A
h : ∀ (n : ℕ) {a b : End A (Fin n → A)}, a * b = 1 → b * a = 1
n : ℕ
f : End A (Fin n → A)
surj : Surjective ⇑f
g : (Fin n → A) →ₗ[A] Fin n → A
eq : f ∘ₗ g = LinearMap.id
⊢ Injective ⇑f

Tactic:
exact injective_of_comp_eq_id _ _ (h _ eq)

Goal state after:
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✝³ : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
⊢ (map Q g hy) (z • x) = g z • (map Q g hy) x

Tactic:
by
  rw [Algebra.smul_def, Algebra.smul_def, map_mul, map_eq]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : FaithfulSMul R K
surj : ∀ (z : K), ∃ x y, z = (algebraMap R K) x / (algebraMap R K) y
inj : Function.Injective ⇑(algebraMap R K)
this✝ : NoZeroDivisors R
this : Nontrivial R
z : K
x : R
eq : z = (algebraMap R K) x / (algebraMap R K) 0
⊢ ∃ x, z * (algebraMap R K) ↑x.2 = (algebraMap R K) x.1

pp: case inr
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : FaithfulSMul R K
surj : ∀ (z : K), ∃ x y, z = (algebraMap R K) x / (algebraMap R K) y
inj : Function.Injective ⇑(algebraMap R K)
this✝ : NoZeroDivisors R
this : Nontrivial R
z : K
x y : R
eq : z = (algebraMap R K) x / (algebraMap R K) y
hy : y ≠ 0
⊢ ∃ x, z * (algebraMap R K) ↑x.2 = (algebraMap R K) x.1

Tactic:
· obtain rfl : z = 0 := by simpa using eq
      exact ⟨(0, 1), by simp⟩

Goal state after:
case inr
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : FaithfulSMul R K
surj : ∀ (z : K), ∃ x y, z = (algebraMap R K) x / (algebraMap R K) y
inj : Function.Injective ⇑(algebraMap R K)
this✝ : NoZeroDivisors R
this : Nontrivial R
z : K
x y : R
eq : z = (algebraMap R K) x / (algebraMap R K) y
hy : y ≠ 0
⊢ ∃ x, z * (algebraMap R K) ↑x.2 = (algebraMap R K) x.1
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: F : Type u_4
inst✝² : CommSemiring F
E : Type u_5
inst✝¹ : CommSemiring E
inst✝ : Algebra F E
K : Subalgebra F E
S : Set E
⊢ Subalgebra.restrictScalars F (adjoin (↥K) S) = adjoin F (↑K ∪ S)

Tactic:
conv_lhs => rw [← Algebra.adjoin_eq K, ← Algebra.adjoin_union_eq_adjoin_adjoin]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_4
inst✝⁴ : CommSemiring S
K : Type u_5
inst✝³ : CommSemiring K
inst✝² : Algebra R K
e : R ≃+* S
inst✝¹ : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h : ∀ (x : R), (algebraMap R K) x = (algebraMap S K) (e x)
inst✝ : IsLocalization M₁ K
⊢ IsLocalization M₂ K

Tactic:
by
  rw [IsLocalization.isLocalization_iff_of_base_ringEquiv _ _ e, hM]
  convert! (inferInstance : IsLocalization M₁ K)
  exact Algebra.algebra_ext _ _ (by simp [RingHom.algebraMap_toAlgebra, h])

Goal state after:
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
inst✝ : Nontrivial R
hM : M ≤ nonZeroDivisors R
x : R
hx : x ∈ nonZeroDivisors R
⊢ (algebraMap R S) x ≠ 0

Tactic:
rw [Ne, to_map_eq_zero_iff S hM]

Goal state after:
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
inst✝ : Nontrivial R
hM : M ≤ nonZeroDivisors R
x : R
hx : x ∈ nonZeroDivisors R
⊢ ¬x = 0
Module: Mathlib.RingTheory.Localization.Basic

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
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
⊢ (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x) = (algebraMap S Sₘ) ((algebraMap R S) x)

Tactic:
← IsScalarTower.algebraMap_apply R S Sₘ,

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
⊢ (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x) = (algebraMap R Sₘ) x
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : Surjective ⇑(algebraMap R A)
r : R
⊢ 1 ⊗ₜ[R] (r • 1) = (r • 1) ⊗ₜ[R] 1

Tactic:
smul_tmul

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : Surjective ⇑(algebraMap R A)
r : R
⊢ 1 ⊗ₜ[R] (r • 1) = 1 ⊗ₜ[R] (r • 1)
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
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : f b ≠ 0
⊢ (b • (f a / f b)) ⊗ₜ[R] (1 / f b) = (f a / f b) ⊗ₜ[R] (b • (1 / f b))

Tactic:
smul_tmul

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
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : f b ≠ 0
⊢ (f a / f b) ⊗ₜ[R] (b • (1 / f b)) = (f a / f b) ⊗ₜ[R] (b • (1 / f b))
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
⊢ ∀ (x y : A),
    { toFun := fun y_1 ↦ (x + y) ⊗ₜ[R] (y_1 • m), map_add' := ⋯, map_smul' := ⋯ } =
      { toFun := fun y ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun y_1 ↦ y ⊗ₜ[R] (y_1 • m), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
intros

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
x✝ y✝ : A
⊢ { toFun := fun y ↦ (x✝ + y✝) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun y ↦ x✝ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun y ↦ y✝ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ }
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
⊢ ∀ (m_1 : R) (x : A),
    { toFun := fun y ↦ (m_1 • x) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } =
      (RingHom.id R) m_1 • { toFun := fun y ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
intros

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
m✝ : R
x✝ : A
⊢ { toFun := fun y ↦ (m✝ • x✝) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) m✝ • { toFun := fun y ↦ x✝ ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ }
Module: Mathlib.Algebra.Algebra.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
⊢ let semiring := e.semiring;
  let algebra := Equiv.algebra R e;
  α ≃ₐ[R] β

Tactic:
intros

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
semiring✝ : Semiring α := e.semiring
algebra✝ : Algebra R α := Equiv.algebra R e
⊢ α ≃ₐ[R] β
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
⊢ let add := e.add;
  let mul := e.mul;
  α ≃+* β

Tactic:
intros

Goal state after:
α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
add✝ : Add α := e.add
mul✝ : Mul α := e.mul
⊢ α ≃+* β
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:
intros

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
nsmul : SMul ℕ α := ⋯
⊢ e 0 = 0
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
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✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
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✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
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✝
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:
intros

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
nsmul : SMul ℕ α := ⋯
⊢ e 0 = 0
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
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✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
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✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
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✝
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:
intros

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
⊢ e 0 = 0
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:
intros

Goal state after:
case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
⊢ e 1 = 1
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
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✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
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✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
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✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
⊢ ∀ (n : ℕ), e ↑n = ↑n

Tactic:
intros

Goal state after:
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✝
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:
intros

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 0 = 0
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:
intros

Goal state after:
case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 1 = 1
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
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✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
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✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
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✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
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✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℕ), e ↑n = ↑n

Tactic:
intros

Goal state after:
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✝