Module: Mathlib.Algebra.Field.TransferInstance

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

Tactic:
apply e.injective.field _

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