mathlib-initiative/mathlib-tactics huggingface dataset:
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

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

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

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:
<;>

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

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

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

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
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

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✝

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✝

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:
<;>

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

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✝

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✝

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

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

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

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

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

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

Tactic:
<;>

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

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

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

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

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

case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
⊢ ∀ (n : ℕ), e ↑n = ↑n
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

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

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✝

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✝

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✝

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:
<;>

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

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

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✝

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✝

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✝

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

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

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

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

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

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

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:
<;>

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

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

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

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

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

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

case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (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

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

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✝

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✝

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✝

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✝

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:
<;>

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

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

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✝

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✝

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✝

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✝

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✝
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

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

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

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

Tactic:
<;>

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 α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
nsmul : SMul ℕ α := ⋯
⊢ ∀ (x y : α), e (x + y) = e x + e y

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

case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
nsmul : SMul ℕ α := ⋯
⊢ ∀ (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

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✝

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✝

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:
<;>

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✝ : CommSemiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 0 = 0

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

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

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

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

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

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

Tactic:
<;>

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

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

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

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

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

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

case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℕ), e ↑n = ↑n
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

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

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✝

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✝

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✝

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✝

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:
<;>

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

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

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✝

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✝

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✝

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✝

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✝
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_1
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ (mul (1 ⊗ₜ[R] 1)) 0 = 0

pp: case refine_2
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ ∀ (x : A) (y : B), (mul (1 ⊗ₜ[R] 1)) (x ⊗ₜ[R] y) = x ⊗ₜ[R] y

pp: case refine_3
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ ∀ (x y : A ⊗[R] B), (mul (1 ⊗ₜ[R] 1)) x = x → (mul (1 ⊗ₜ[R] 1)) y = y → (mul (1 ⊗ₜ[R] 1)) (x + y) = x + y

Tactic:
<;>

Goal state after:
case refine_1
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ (mul (1 ⊗ₜ[R] 1)) 0 = 0

case refine_2
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ ∀ (x : A) (y : B), (mul (1 ⊗ₜ[R] 1)) (x ⊗ₜ[R] y) = x ⊗ₜ[R] y

case refine_3
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ ∀ (x y : A ⊗[R] B), (mul (1 ⊗ₜ[R] 1)) x = x → (mul (1 ⊗ₜ[R] 1)) y = y → (mul (1 ⊗ₜ[R] 1)) (x + y) = x + y