awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
q : ℚ
rw : (↑q : β) < inducedMap α β a ↔ (↑q : γ) < inducedMap α γ a
⊢ (↑q : γ) < inducedMap β γ (inducedMap α β a) ↔ (↑q : γ) < inducedMap α γ a
have rw₁ : (↑q : α) < a ↔ (↑q : γ) < inducedMap α γ a
Tactic: rw [coe_lt_inducedMap_iff, coe_lt_inducedMap_iff, Iff.comm, coe_lt_inducedMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
q : ℚ
rw : (↑q : β) < inducedMap α β a ↔ (↑q : γ) < inducedMap α γ a
rw₁ : (↑q : α) < a ↔ (↑q : γ) < inducedMap α γ a
⊢ (↑q : γ) < inducedMap β γ (inducedMap α β a) ↔ (↑q : γ) < inducedMap α γ a
have rw₂ : (↑q : γ) < inducedMap α γ a ↔ (↑q : α) < a
Tactic: rw [coe_lt_inducedMap_iff, coe_lt_inducedMap_iff, Iff.comm, coe_lt_inducedMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
q : ℚ
rw : (↑q : β) < inducedMap α β a ↔ (↑q : γ) < inducedMap α γ a
rw₁ : (↑q : α) < a ↔ (↑q : γ) < inducedMap α γ a
rw₂ : (↑q : γ) < inducedMap α γ a ↔ (↑q : α) < a
⊢ (↑q : γ) < inducedMap β γ (inducedMap α β a) ↔ (↑q : γ) < inducedMap α γ a
have rw₃ : (↑q : α) < a ↔ (↑q : α) < a
Tactic: rw [coe_lt_inducedMap_iff, coe_lt_inducedMap_iff, Iff.comm, coe_lt_inducedMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
β : Type u_3
γ : Type u_4
inst : Field β
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : Field γ
inst_4 : ConditionallyCompleteLinearOrder γ
inst_5 : IsStrictOrderedRing γ
b : β
⊢ inducedMap γ β (inducedMap β γ b) = b
have rw : inducedMap β β b = b
Tactic: rw [inducedMap_inducedMap, inducedMap_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
β : Type u_3
γ : Type u_4
inst : Field β
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : Field γ
inst_4 : ConditionallyCompleteLinearOrder γ
inst_5 : IsStrictOrderedRing γ
b : β
rw : inducedMap β β b = b
⊢ inducedMap γ β (inducedMap β γ b) = b
have rw₁ : b = b
Tactic: rw [inducedMap_inducedMap, inducedMap_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
x y : α
⊢ inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y
have rw : sSup (cutMap β x + cutMap β y) = inducedMap α β x + inducedMap α β y
Tactic: rw [inducedMap, cutMap_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hb : b ∈ cutMap β (a * a)
⊢ b ≤ inducedMap α β a * inducedMap α β a
have obtain : ∀ (q : ℚ) (hb : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a * a} q),
  (↑q : β) ≤ inducedMap α β a * inducedMap α β a
Tactic: obtain ⟨q, hb, rfl⟩ := hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
q : ℚ
hb : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a * a} q
⊢ (↑q : β) ≤ inducedMap α β a * inducedMap α β a
have obtain : ∀ (q' : ℚ) (hq' : 0 < q') (hqq' : (↑q : α) < HPow.hPow (α := α) (β := ℕ) (↑q' : α) 2)
  (hqa : HPow.hPow (α := α) (β := ℕ) (↑q' : α) 2 < a * a), (↑q : β) ≤ inducedMap α β a * inducedMap α β a
Tactic: obtain ⟨q', hq', hqq', hqa⟩ := exists_rat_pow_btwn two_ne_zero hb (mul_self_pos.2 ha.ne')
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
q : ℚ
hb : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a * a} q
q' : ℚ
hq' : 0 < q'
hqq' : (↑q : α) < HPow.hPow (α := α) (β := ℕ) (↑q' : α) 2
hqa : HPow.hPow (α := α) (β := ℕ) (↑q' : α) 2 < a * a
⊢ (↑q : β) ≤ inducedMap α β a * inducedMap α β a
have trans : (↑q : β) ≤ HPow.hPow (α := β) (β := ℕ) (↑q' : β) 2
Tactic: trans (q' : β) ^ 2
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
q : ℚ
hb : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a * a} q
q' : ℚ
hq' : 0 < q'
hqq' : (↑q : α) < HPow.hPow (α := α) (β := ℕ) (↑q' : α) 2
hqa : HPow.hPow (α := α) (β := ℕ) (↑q' : α) 2 < a * a
trans : (↑q : β) ≤ HPow.hPow (α := β) (β := ℕ) (↑q' : β) 2
⊢ (↑q : β) ≤ inducedMap α β a * inducedMap α β a
have trans₁ : HPow.hPow (α := β) (β := ℕ) (↑q' : β) 2 ≤ inducedMap α β a * inducedMap α β a
Tactic: trans (q' : β) ^ 2
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
q : ℚ
hb : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a * a} q
q' : ℚ
hq' : 0 < q'
hqq' : (↑q : α) < HPow.hPow (α := α) (β := ℕ) (↑q' : α) 2
hqa : HPow.hPow (α := α) (β := ℕ) (↑q' : α) 2 < a * a
⊢ HPow.hPow (α := β) (β := ℕ) (↑q' : β) 2 ≤ inducedMap α β a * inducedMap α β a
have rw : ∀ (hqa : HMul.hMul (α := α) (↑q' : α) (↑q' : α) < a * a),
  HMul.hMul (α := β) (↑q' : β) (↑q' : β) ≤ inducedMap α β a * inducedMap α β a
Tactic: rw [pow_two] at hqa ⊢
Cleared hypotheses: hqa
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c
have inl : ∀ (hb : b < 0), ∃ c ∈ cutMap β (a * a), b < c
Tactic: obtain hb | hb := lt_or_ge b 0
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
inl : ∀ (hb : b < 0), ∃ c ∈ cutMap β (a * a), b < c
⊢ ∃ c ∈ cutMap β (a * a), b < c
have inr : ∀ (hb : 0 ≤ b), ∃ c ∈ cutMap β (a * a), b < c
Tactic: obtain hb | hb := lt_or_ge b 0
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ ∃ c ∈ cutMap β (a * a), b < c
have inl : 0 ∈ cutMap β (a * a)
Tactic: refine ⟨0, ?_, hb⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ 0 ∈ cutMap β (a * a)
have inl : 0 < a * a
Tactic: rw [← Rat.cast_zero, coe_mem_cutMap_iff, Rat.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
⊢ ∃ c ∈ cutMap β (a * a), b < c
have inr : ∀ (q : ℚ) (hq : 0 < q) (hbq : b < HPow.hPow (α := β) (β := ℕ) (↑q : β) 2)
  (hqa : HPow.hPow (α := β) (β := ℕ) (↑q : β) 2 < inducedMap α β a * inducedMap α β a), ∃ c ∈ cutMap β (a * a), b < c
Tactic: obtain ⟨q, hq, hbq, hqa⟩ := exists_rat_pow_btwn two_ne_zero hba (hb.trans_lt hba)
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < HPow.hPow (α := β) (β := ℕ) (↑q : β) 2
hqa : HPow.hPow (α := β) (β := ℕ) (↑q : β) 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c
have hbq₁ : b < (↑(HPow.hPow (β := ℕ) q 2) : β)
Tactic: rw [← cast_pow] at hbq
Cleared hypotheses: hbq, hqa
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < (↑(HPow.hPow (β := ℕ) q 2) : β)
hqa : HPow.hPow (α := β) (β := ℕ) (↑q : β) 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c
have inr : (↑(HPow.hPow (β := ℕ) q 2) : α) < a * a
Tactic: refine ⟨(q ^ 2 : ℚ), coe_mem_cutMap_iff.2 ?_, hbq⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < (↑(HPow.hPow (β := ℕ) q 2) : β)
hqa : HPow.hPow (α := β) (β := ℕ) (↑q : β) 2 < inducedMap α β a * inducedMap α β a
⊢ (↑(HPow.hPow (β := ℕ) q 2) : α) < a * a
have inr : ∀ (hqa : HMul.hMul (α := β) (↑q : β) (↑q : β) < inducedMap α β a * inducedMap α β a), (↑(q * q) : α) < a * a
Tactic: rw [pow_two] at hqa ⊢
Cleared hypotheses: hqa
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < (↑(HPow.hPow (β := ℕ) q 2) : β)
hqa : HMul.hMul (α := β) (↑q : β) (↑q : β) < inducedMap α β a * inducedMap α β a
⊢ (↑(q * q) : α) < a * a
have inr : HMul.hMul (α := α) (↑q : α) (↑q : α) < a * a
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < (↑(HPow.hPow (β := ℕ) q 2) : β)
hqa : HMul.hMul (α := β) (↑q : β) (↑q : β) < inducedMap α β a * inducedMap α β a
⊢ HMul.hMul (α := α) (↑q : α) (↑q : α) < a * a
have inr : ∀ (q' : ℚ) (hq' : LT.lt.{u_3} (α := β) (↑q : β) (↑q' : β)) (hqa' : (↑q' : α) < a),
  HMul.hMul (α := α) (↑q : α) (↑q : α) < a * a
Tactic: obtain ⟨q', hq', hqa'⟩ := lt_inducedMap_iff.1 (lt_of_mul_self_lt_mul_self₀
    (inducedMap_nonneg ha.le) hqa)
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < (↑(HPow.hPow (β := ℕ) q 2) : β)
hqa : HMul.hMul (α := β) (↑q : β) (↑q : β) < inducedMap α β a * inducedMap α β a
q' : ℚ
hq' : LT.lt.{u_3} (α := β) (↑q : β) (↑q' : β)
hqa' : (↑q' : α) < a
⊢ LT.lt.{u_2} (α := α) (↑q : α) (↑q' : α)
have assumption_mod_cast : ∀ (ha : 0 < a) (hb : 0 ≤ b) (hq : 0 < q) (hqa : (↑(q * q) : β) < inducedMap α β a * inducedMap α β a) (hq' : q < q'),
  q < q'
Tactic: assumption_mod_cast
Cleared hypotheses: ha, hb, hq, hqa, hq'
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
⊢ (inducedAddHom α β : (a : α) → β) (x * x) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
have inl : ∀ (h : x < 0),
  (inducedAddHom α β : (a : α) → β) (x * x) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
Tactic: obtain h | rfl | h := lt_trichotomy x 0
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
inl :
  ∀ (h : x < 0),
    (inducedAddHom α β : (a : α) → β) (x * x) =
      HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
⊢ (inducedAddHom α β : (a : α) → β) (x * x) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
have inr : (inducedAddHom α β : (a : α) → β) (HMul.hMul (α := α) 0 0) =
  HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) 0 : β) ((inducedAddHom α β : (a : α) → β) 0 : β)
Tactic: obtain h | rfl | h := lt_trichotomy x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
inl :
  ∀ (h : x < 0),
    (inducedAddHom α β : (a : α) → β) (x * x) =
      HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
inr :
  (inducedAddHom α β : (a : α) → β) (HMul.hMul (α := α) 0 0) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) 0 : β) ((inducedAddHom α β : (a : α) → β) 0 : β)
⊢ (inducedAddHom α β : (a : α) → β) (x * x) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
have inr₁ : ∀ (h : 0 < x),
  (inducedAddHom α β : (a : α) → β) (x * x) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
Tactic: obtain h | rfl | h := lt_trichotomy x 0
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : x < 0
⊢ (inducedAddHom α β : (a : α) → β) (x * x) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
have h₁ : Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β) ((inducedAddHom α β : (a : α) → β) (-x * -x) : β)
Tactic: convert! this (-x) (neg_pos.2 h) using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : x < 0
h₁ :
  Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
    ((inducedAddHom α β : (a : α) → β) (-x * -x) : β)
⊢ (inducedAddHom α β : (a : α) → β) (x * x) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
have h₂ : HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
  HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) (-x) : β) ((inducedAddHom α β : (a : α) → β) (-x) : β)
Tactic: convert! this (-x) (neg_pos.2 h) using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : x < 0
⊢ Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
    ((inducedAddHom α β : (a : α) → β) (-x * -x) : β)
have h₁ : Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
  ((inducedAddHom α β : (a : α) → β) (-(x * -x)) : β)
Tactic: rw [neg_mul, mul_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : x < 0
h₁ :
  Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
    ((inducedAddHom α β : (a : α) → β) (-(x * -x)) : β)
⊢ Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
    ((inducedAddHom α β : (a : α) → β) (-x * -x) : β)
have h₂ : Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
  ((inducedAddHom α β : (a : α) → β) (- -(x * x)) : β)
Tactic: rw [neg_mul, mul_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : x < 0
h₁ :
  Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
    ((inducedAddHom α β : (a : α) → β) (-(x * -x)) : β)
h₂ :
  Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
    ((inducedAddHom α β : (a : α) → β) (- -(x * x)) : β)
⊢ Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
    ((inducedAddHom α β : (a : α) → β) (-x * -x) : β)
have h₃ : Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
Tactic: rw [neg_mul, mul_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : x < 0
⊢ HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) (-x) : β)
      ((inducedAddHom α β : (a : α) → β) (-x) : β)
have h₁ : HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
  HMul.hMul (α := β) (β := β) (-(inducedAddHom α β : (a : α) → β) x : β) (-(inducedAddHom α β : (a : α) → β) x : β)
Tactic: simp_rw [map_neg, neg_mul, mul_neg, neg_neg]