[GOAL]
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ DivisionSemiring (ULift α)
[PROOFSTEP]
refine' down_injective.divisionSemiring down ..
[GOAL]
case refine'_1
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ 0.down = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ 1.down = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x y : ULift α), (x + y).down = x.down + y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x y : ULift α), (x * y).down = x.down * y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_5
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x : ULift α), x⁻¹.down = x.down⁻¹
[PROOFSTEP]
intros
[GOAL]
case refine'_6
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x y : ULift α), (x / y).down = x.down / y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_7
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x : ULift α) (n : ℕ), (n • x).down = n • x.down
[PROOFSTEP]
intros
[GOAL]
case refine'_8
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x : ULift α) (n : ℕ), (x ^ n).down = x.down ^ n
[PROOFSTEP]
intros
[GOAL]
case refine'_9
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (x : ULift α) (n : ℤ), (x ^ n).down = x.down ^ n
[PROOFSTEP]
intros
[GOAL]
case refine'_10
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ ∀ (n : ℕ), (↑n).down = ↑n
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ 0.down = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
⊢ 1.down = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ y✝ : ULift α
⊢ (x✝ + y✝).down = x✝.down + y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ y✝ : ULift α
⊢ (x✝ * y✝).down = x✝.down * y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_5
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ : ULift α
⊢ x✝⁻¹.down = x✝.down⁻¹
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ y✝ : ULift α
⊢ (x✝ / y✝).down = x✝.down / y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_7
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ : ULift α
n✝ : ℕ
⊢ (n✝ • x✝).down = n✝ • x✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_8
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ : ULift α
n✝ : ℕ
⊢ (x✝ ^ n✝).down = x✝.down ^ n✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_9
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
x✝ : ULift α
n✝ : ℤ
⊢ (x✝ ^ n✝).down = x✝.down ^ n✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_10
α : Type u
x y : ULift α
inst✝ : DivisionSemiring α
n✝ : ℕ
⊢ (↑n✝).down = ↑n✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ DivisionRing (ULift α)
[PROOFSTEP]
refine' down_injective.divisionRing down ..
[GOAL]
case refine'_1
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ 0.down = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ 1.down = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x y : ULift α), (x + y).down = x.down + y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x y : ULift α), (x * y).down = x.down * y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_5
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α), (-x).down = -x.down
[PROOFSTEP]
intros
[GOAL]
case refine'_6
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x y : ULift α), (x - y).down = x.down - y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_7
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α), x⁻¹.down = x.down⁻¹
[PROOFSTEP]
intros
[GOAL]
case refine'_8
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x y : ULift α), (x / y).down = x.down / y.down
[PROOFSTEP]
intros
[GOAL]
case refine'_9
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α) (n : ℕ), (n • x).down = n • x.down
[PROOFSTEP]
intros
[GOAL]
case refine'_10
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α) (n : ℤ), (n • x).down = n • x.down
[PROOFSTEP]
intros
[GOAL]
case refine'_11
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α) (n : ℚ), (n • x).down = n • x.down
[PROOFSTEP]
intros
[GOAL]
case refine'_12
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α) (n : ℕ), (x ^ n).down = x.down ^ n
[PROOFSTEP]
intros
[GOAL]
case refine'_13
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (x : ULift α) (n : ℤ), (x ^ n).down = x.down ^ n
[PROOFSTEP]
intros
[GOAL]
case refine'_14
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (n : ℕ), (↑n).down = ↑n
[PROOFSTEP]
intros
[GOAL]
case refine'_15
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (n : ℤ), (↑n).down = ↑n
[PROOFSTEP]
intros
[GOAL]
case refine'_16
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ ∀ (n : ℚ), (↑n).down = ↑n
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ 0.down = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u
x y : ULift α
inst✝ : DivisionRing α
⊢ 1.down = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ y✝ : ULift α
⊢ (x✝ + y✝).down = x✝.down + y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ y✝ : ULift α
⊢ (x✝ * y✝).down = x✝.down * y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_5
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
⊢ (-x✝).down = -x✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ y✝ : ULift α
⊢ (x✝ - y✝).down = x✝.down - y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_7
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
⊢ x✝⁻¹.down = x✝.down⁻¹
[PROOFSTEP]
rfl
[GOAL]
case refine'_8
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ y✝ : ULift α
⊢ (x✝ / y✝).down = x✝.down / y✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_9
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
n✝ : ℕ
⊢ (n✝ • x✝).down = n✝ • x✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_10
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
n✝ : ℤ
⊢ (n✝ • x✝).down = n✝ • x✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_11
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
n✝ : ℚ
⊢ (n✝ • x✝).down = n✝ • x✝.down
[PROOFSTEP]
rfl
[GOAL]
case refine'_12
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
n✝ : ℕ
⊢ (x✝ ^ n✝).down = x✝.down ^ n✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_13
α : Type u
x y : ULift α
inst✝ : DivisionRing α
x✝ : ULift α
n✝ : ℤ
⊢ (x✝ ^ n✝).down = x✝.down ^ n✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_14
α : Type u
x y : ULift α
inst✝ : DivisionRing α
n✝ : ℕ
⊢ (↑n✝).down = ↑n✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_15
α : Type u
x y : ULift α
inst✝ : DivisionRing α
n✝ : ℤ
⊢ (↑n✝).down = ↑n✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_16
α : Type u
x y : ULift α
inst✝ : DivisionRing α
n✝ : ℚ
⊢ (↑n✝).down = ↑n✝
[PROOFSTEP]
rfl
