Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ e 0 = 0

pp: case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ e 1 = 1

pp: case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x y : α), e (x + y) = e x + e y

pp: case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

pp: case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x : α), e (-x) = -e x

pp: case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x y : α), e (x - y) = e x - e y

pp: case inv
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x : α), e x⁻¹ = (e x)⁻¹

pp: case div
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x y : α), e (x / y) = e x / e y

pp: case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (n : ℕ) (x : α), e (n • x) = n • e x

pp: case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (n : ℤ) (x : α), e (n • x) = n • e x

pp: case nnqsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (q : ℚ≥0) (x : α), e (q • x) = q • e x

pp: case qsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (q : ℚ) (x : α), e (q • x) = q • e x

pp: case npow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

pp: case zpow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x : α) (n : ℤ), e (x ^ n) = e x ^ n

pp: case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (n : ℕ), e ↑n = ↑n

pp: case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (n : ℤ), e ↑n = ↑n

pp: case nnratCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (q : ℚ≥0), e ↑q = ↑q

pp: case ratCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (q : ℚ), e ↑q = ↑q

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ e 0 = 0

case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ e 1 = 1

case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x y : α), e (x + y) = e x + e y

case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x : α), e (-x) = -e x

case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x y : α), e (x - y) = e x - e y

case inv
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x : α), e x⁻¹ = (e x)⁻¹

case div
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x y : α), e (x / y) = e x / e y

case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (n : ℕ) (x : α), e (n • x) = n • e x

case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (n : ℤ) (x : α), e (n • x) = n • e x

case nnqsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (q : ℚ≥0) (x : α), e (q • x) = q • e x

case qsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (q : ℚ) (x : α), e (q • x) = q • e x

case npow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

case zpow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (x : α) (n : ℤ), e (x ^ n) = e x ^ n

case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (n : ℕ), e ↑n = ↑n

case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (n : ℤ), e ↑n = ↑n

case nnratCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (q : ℚ≥0), e ↑q = ↑q

case ratCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ ∀ (q : ℚ), e ↑q = ↑q