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✝ : NonUnitalCommSemiring β
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✝ : NonUnitalCommSemiring β
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✝ : NonUnitalCommSemiring β
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✝ : 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✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
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

Tactic:
intros

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

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

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

Tactic:
intros

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

Goal state after:
case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
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✝ : CommSemiring β
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✝ : 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✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
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

Tactic:
intros

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

Goal state before:
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

Tactic:
intros

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

Goal state before:
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

Tactic:
intros

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

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

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

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

Goal state before:
pp: case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : 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✝ : NonUnitalNonAssocRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : 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✝ : NonUnitalNonAssocRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : 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✝ : NonUnitalNonAssocRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x✝ : α
⊢ e (-x✝) = -e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : 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✝ : NonUnitalNonAssocRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (n : ℕ) (x : α), e (n • x) = n • e x

Tactic:
intros

Goal state after:
case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : 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✝ : NonUnitalRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ e 0 = 0

Tactic:
intros

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

Goal state before:
pp: case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : 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✝ : NonUnitalRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : 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✝ : NonUnitalRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : 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✝ : NonUnitalRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x : α), e (-x) = -e x

Tactic:
intros

Goal state after:
case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x✝ : α
⊢ e (-x✝) = -e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x y : α), e (x - y) = e x - e y

Tactic:
intros

Goal state after:
case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : 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✝ : NonUnitalRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (n : ℕ) (x : α), e (n • x) = n • e x

Tactic:
intros

Goal state after:
case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : 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✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

Tactic:
intros

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

Tactic:
intros

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

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

Tactic:
intros

Goal state after:
case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
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✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := ⋯
mul : Mul α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

Tactic:
intros

Goal state after:
case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := ⋯
mul : Mul α := ⋯
⊢ ∀ (x : α), e (-x) = -e x

Tactic:
intros

Goal state after:
case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
x✝ : α
⊢ e (-x✝) = -e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := ⋯
mul : Mul α := ⋯
⊢ ∀ (x y : α), e (x - y) = e x - e y

Tactic:
intros

Goal state after:
case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
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✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := ⋯
mul : Mul α := ⋯
⊢ ∀ (n : ℕ) (x : α), e (n • x) = n • e x

Tactic:
intros

Goal state after:
case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := ⋯
mul : Mul α := ⋯
⊢ ∀ (n : ℤ) (x : α), e (n • x) = n • e x

Tactic:
intros

Goal state after:
case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
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✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := ⋯
mul : Mul α := ⋯
⊢ ∀ (n : ℕ), e ↑n = ↑n

Tactic:
intros

Goal state after:
case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
n✝ : ℕ
⊢ e ↑n✝ = ↑n✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := ⋯
mul : Mul α := ⋯
⊢ ∀ (n : ℤ), e ↑n = ↑n

Tactic:
intros

Goal state after:
case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
n✝ : ℤ
⊢ e ↑n✝ = ↑n✝
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 0 = 0
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
intros

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

Goal state before:
pp: case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
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✝ : Ring β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
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✝ : Ring β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x : α), e (-x) = -e x

Tactic:
intros

Goal state after:
case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
⊢ e (-x✝) = -e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x - y) = e x - e y

Tactic:
intros

Goal state after:
case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
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✝ : Ring β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℤ) (x : α), e (n • x) = n • e x

Tactic:
intros

Goal state after:
case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
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✝ : Ring β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℕ), e ↑n = ↑n

Tactic:
intros

Goal state after:
case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n✝ : ℕ
⊢ e ↑n✝ = ↑n✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℤ), e ↑n = ↑n

Tactic:
intros

Goal state after:
case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
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✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ e 0 = 0

Tactic:
intros

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