awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.CompleteField
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 α
⊢ inducedMap α β 1 = 1

Tactic:
mod_cast inducedMap_rat α β 1

Premises used: congrArg, ConditionallyCompleteLinearOrderedField.inducedMap_rat, cast, ConditionallyCompleteLinearOrderedField.inducedMap, Rat.cast, congr, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans, Rat.cast_one
-- Module: Mathlib.Algebra.Order.CompleteField
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
⊢ 0 ≤ inducedMap α β a

Tactic:
(inducedMap_zero α _).ge.trans <| inducedMap_mono _ _ ha

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap_mono, Eq.ge, ConditionallyCompleteLinearOrderedField.inducedMap_zero, LE.le.trans
-- Module: Mathlib.Algebra.Order.CompleteField
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 : α
q : ℚ
⊢ (↑q : β) < inducedMap α β a ↔ (↑q : α) < a

Tactic:
⟨fun h => ?_, fun hq => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Order.CompleteField
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 : α
q : ℚ
refine_1 : ∀ (h : (↑q : β) < inducedMap α β a), (↑q : α) < a
refine_2 : ∀ (hq : (↑q : α) < a), (↑q : β) < inducedMap α β a
⊢ (↑q : β) < inducedMap α β a ↔ (↑q : α) < a

Tactic:
refine ⟨fun h => ?_, fun hq => ?_⟩
-- Module: Mathlib.Algebra.Order.CompleteField
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 : α
q : ℚ
h : (↑q : β) < inducedMap α β a
⊢ inducedMap α β (↑q : α) < inducedMap α β a

Tactic:
rw [← inducedMap_rat α] at h

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap_rat
-- Module: Mathlib.Algebra.Order.CompleteField
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 : α
q : ℚ
h : inducedMap α β (↑q : α) < inducedMap α β a
⊢ (↑q : α) < a

Tactic:
(inducedMap_mono α β).reflect_lt h

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap_mono, Monotone.reflect_lt
-- Module: Mathlib.Algebra.Order.CompleteField
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 : α
q : ℚ
h : inducedMap α β (↑q : α) < inducedMap α β a
⊢ (↑q : α) < a

Tactic:
exact (inducedMap_mono α β).reflect_lt h

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap_mono, Monotone.reflect_lt
-- Module: Mathlib.Algebra.Order.CompleteField
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 : α
q : ℚ
hq : (↑q : α) < a
refine_2 : ∀ (q' : ℚ) (hq : LT.lt.{u_2} (α := α) (↑q : α) (↑q' : α)) (hqa : (↑q' : α) < a), (↑q : β) < inducedMap α β a
⊢ (↑q : β) < inducedMap α β a

Tactic:
obtain ⟨q', hq, hqa⟩ := exists_rat_btwn hq

Premises used: exists_rat_btwn
-- Module: Mathlib.Algebra.Order.CompleteField
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 : α
q : ℚ
hq_1 : (↑q : α) < a
q' : ℚ
hq : LT.lt.{u_2} (α := α) (↑q : α) (↑q' : α)
hqa : (↑q' : α) < a
refine_2 : LT.lt.{u_3} (α := β) (↑q : β) (↑q' : β)
⊢ (↑q : β) < inducedMap α β a

Tactic:
apply lt_csSup_of_lt (cutMap_bddAbove β a) (coe_mem_cutMap_iff.mpr hqa)

Premises used: Iff.mpr, LinearOrderedField.coe_mem_cutMap_iff, lt_csSup_of_lt, LinearOrderedField.cutMap_bddAbove
-- Module: Mathlib.Algebra.Order.CompleteField
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 : α
q : ℚ
hq_1 : (↑q : α) < a
q' : ℚ
hq : LT.lt.{u_2} (α := α) (↑q : α) (↑q' : α)
hqa : (↑q' : α) < a
⊢ LT.lt.{u_3} (α := β) (↑q : β) (↑q' : β)

Tactic:
mod_cast hq

Premises used: cast, Rat.cast_lt._simp_1, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Order.CompleteField
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 : α
q : ℚ
hq_1 : (↑q : α) < a
q' : ℚ
hq : LT.lt.{u_2} (α := α) (↑q : α) (↑q' : α)
hqa : (↑q' : α) < a
⊢ LT.lt.{u_3} (α := β) (↑q : β) (↑q' : β)

Tactic:
exact mod_cast hq
-- Module: Mathlib.Algebra.Order.CompleteField
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 : α
b : β
h : ∃ (q : ℚ), b < (↑q : β) ∧ (↑q : α) < a
q : ℚ
hbq : b < (↑q : β)
hqa rwa rwa₁ rwa₂ rwa₃ : (↑q : α) < a
⊢ (↑q : β) < inducedMap α β a

Tactic:
rwa [coe_lt_inducedMap_iff]

Premises used: ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iff
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
β : Type u_3
inst : Field β
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : IsStrictOrderedRing β
b : β
⊢ inducedMap β β b = b

Tactic:
eq_of_forall_rat_lt_iff_lt fun _ => coe_lt_inducedMap_iff

Premises used: ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iff, eq_of_forall_rat_lt_iff_lt
-- Module: Mathlib.Algebra.Order.CompleteField
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
rw₃ rw₄ : (↑q : α) < a ↔ (↑q : α) < a
⊢ (↑q : γ) < inducedMap β γ (inducedMap α β a) ↔ (↑q : γ) < inducedMap α γ a

Tactic:
rw [coe_lt_inducedMap_iff, coe_lt_inducedMap_iff, Iff.comm, coe_lt_inducedMap_iff]

Premises used: ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iff, Iff.comm
-- Module: Mathlib.Algebra.Order.CompleteField
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
rw₁ rw₂ : b = b
⊢ inducedMap γ β (inducedMap β γ b) = b

Tactic:
rw [inducedMap_inducedMap, inducedMap_self]

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap_inducedMap, ConditionallyCompleteLinearOrderedField.inducedMap_self
-- Module: Mathlib.Algebra.Order.CompleteField
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 : α
rw : sSup (cutMap β x + cutMap β y) = inducedMap α β x + inducedMap α β y
⊢ inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y

Tactic:
rw [inducedMap, cutMap_add]

Premises used: LinearOrderedField.cutMap_add, ConditionallyCompleteLinearOrderedField.inducedMap
-- Module: Mathlib.Algebra.Order.CompleteField
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 : α
⊢ sSup (cutMap β x + cutMap β y) = inducedMap α β x + inducedMap α β y

Tactic:
csSup_add (cutMap_nonempty β x) (cutMap_bddAbove β x) (cutMap_nonempty β y)
    (cutMap_bddAbove β y)

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap, LinearOrderedField.cutMap_nonempty, csSup_add, LinearOrderedField.cutMap_bddAbove
-- Module: Mathlib.Algebra.Order.CompleteField
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 : α
⊢ sSup (cutMap β x + cutMap β y) = inducedMap α β x + inducedMap α β y

Tactic:
exact csSup_add (cutMap_nonempty β x) (cutMap_bddAbove β x) (cutMap_nonempty β y)
    (cutMap_bddAbove β y)

Premises used: LinearOrderedField.cutMap_nonempty, csSup_add, LinearOrderedField.cutMap_bddAbove
-- Module: Mathlib.Algebra.Order.CompleteField
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)
obtain :
  ∀ (q : ℚ) (hb : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a * a} q),
    (↑q : β) ≤ inducedMap α β a * inducedMap α β a
⊢ b ≤ inducedMap α β a * inducedMap α β a

Tactic:
obtain ⟨q, hb, rfl⟩ := hb

Premises used: rfl
-- Module: Mathlib.Algebra.Order.CompleteField
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
obtain :
  ∀ (q' : ℚ) (hq' : 0 < q') (hqq' : (↑q : α) < HPow.hPow (α := α) (β := ℕ) (↑q' : α) 2)
    (hqa : HPow.hPow (α := α) (β := ℕ) (↑q' : α) 2 < a * a), (↑q : β) ≤ inducedMap α β a * inducedMap α β 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')

Premises used: exists_rat_pow_btwn, Iff.mpr, mul_self_pos, LT.lt.ne', two_ne_zero
-- Module: Mathlib.Algebra.Order.CompleteField
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
trans₁ : HPow.hPow (α := β) (β := ℕ) (↑q' : β) 2 ≤ inducedMap α β a * inducedMap α β a
⊢ (↑q : β) ≤ inducedMap α β a * inducedMap α β a

Tactic:
trans (q' : β) ^ 2

Premises used: Rat.cast
-- Module: Mathlib.Algebra.Order.CompleteField
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 : β) ≤ HPow.hPow (α := β) (β := ℕ) (↑q' : β) 2

Tactic:
mod_cast hqq'.le

Premises used: congrArg, cast, LT.lt.le, Rat.cast, LE.le, Rat.cast_pow._simp_1, OfNat.ofNat, Eq.symm, Rat.cast_le._simp_1, Eq.trans
-- Module: Mathlib.Algebra.Order.CompleteField
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 : β) ≤ HPow.hPow (α := β) (β := ℕ) (↑q' : β) 2

Tactic:
exact mod_cast hqq'.le

Premises used: LT.lt.le
-- Module: Mathlib.Algebra.Order.CompleteField
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
rw :
  ∀ (hqa : HMul.hMul (α := α) (↑q' : α) (↑q' : α) < a * a),
    HMul.hMul (α := β) (↑q' : β) (↑q' : β) ≤ inducedMap α β a * inducedMap α β a
⊢ HPow.hPow (α := β) (β := ℕ) (↑q' : β) 2 ≤ inducedMap α β a * inducedMap α β a

Tactic:
rw [pow_two] at hqa ⊢

Premises used: pow_two
-- Module: Mathlib.Algebra.Order.CompleteField
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 : HMul.hMul (α := α) (↑q' : α) (↑q' : α) < a * a
⊢ HMul.hMul (α := β) (↑q' : β) (↑q' : β) ≤ inducedMap α β a * inducedMap α β a

Tactic:
mul_self_le_mul_self (mod_cast hq'.le)
      (le_csSup (cutMap_bddAbove β a) <|
        coe_mem_cutMap_iff.2 <| lt_of_mul_self_lt_mul_self₀ ha.le hqa)

Premises used: Iff.mpr, mul_self_le_mul_self, congrArg, cast, LT.lt.le, Rat.cast, Rat.natCast_le_cast._simp_1, LE.le, LinearOrderedField.coe_mem_cutMap_iff, lt_of_mul_self_lt_mul_self₀, congrFun', Nat.cast_zero, le_csSup, LinearOrderedField.cutMap_bddAbove, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Order.CompleteField
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 : HMul.hMul (α := α) (↑q' : α) (↑q' : α) < a * a
⊢ HMul.hMul (α := β) (↑q' : β) (↑q' : β) ≤ inducedMap α β a * inducedMap α β a

Tactic:
exact mul_self_le_mul_self (mod_cast hq'.le)
      (le_csSup (cutMap_bddAbove β a) <|
        coe_mem_cutMap_iff.2 <| lt_of_mul_self_lt_mul_self₀ ha.le hqa)

Premises used: Iff.mpr, mul_self_le_mul_self, LT.lt.le, LinearOrderedField.coe_mem_cutMap_iff, lt_of_mul_self_lt_mul_self₀, le_csSup, LinearOrderedField.cutMap_bddAbove
-- Module: Mathlib.Algebra.Order.CompleteField
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
inr : ∀ (hb : 0 ≤ b), ∃ c ∈ cutMap β (a * a), b < c
⊢ ∃ c ∈ cutMap β (a * a), b < c

Tactic:
obtain hb | hb := lt_or_ge b 0

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.CompleteField
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

Tactic:
⟨0, ?_, hb⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.CompleteField
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
inl : 0 ∈ cutMap β (a * a)
⊢ ∃ c ∈ cutMap β (a * a), b < c

Tactic:
refine ⟨0, ?_, hb⟩
-- Module: Mathlib.Algebra.Order.CompleteField
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
inl : 0 < a * a
⊢ 0 ∈ cutMap β (a * a)

Tactic:
rw [← Rat.cast_zero, coe_mem_cutMap_iff, Rat.cast_zero]

Premises used: LinearOrderedField.coe_mem_cutMap_iff, Rat.cast_zero
-- Module: Mathlib.Algebra.Order.CompleteField
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 < a * a

Tactic:
mul_self_pos.2 ha.ne'

Premises used: Iff.mpr, mul_self_pos, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.CompleteField
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 < a * a

Tactic:
exact mul_self_pos.2 ha.ne'

Premises used: Iff.mpr, mul_self_pos, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.CompleteField
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
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
⊢ ∃ c ∈ cutMap β (a * a), b < c

Tactic:
obtain ⟨q, hq, hbq, hqa⟩ := exists_rat_pow_btwn two_ne_zero hba (hb.trans_lt hba)

Premises used: exists_rat_pow_btwn, two_ne_zero, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.CompleteField
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
⊢ b < (↑(HPow.hPow (β := ℕ) q 2) : β)

Tactic:
rw [← cast_pow] at hbq

Premises used: Rat.cast_pow
-- Module: Mathlib.Algebra.Order.CompleteField
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
hbq₁ : b < (↑(HPow.hPow (β := ℕ) q 2) : β)
⊢ HPow.hPow (α := β) (β := ℕ) (↑q : β) 2 < inducedMap α β a * inducedMap α β a

Tactic:
rw [← cast_pow] at hbq

Premises used: Rat.cast_pow
-- Module: Mathlib.Algebra.Order.CompleteField
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

Tactic:
⟨(q ^ 2 : ℚ), coe_mem_cutMap_iff.2 ?_, hbq⟩

Premises used: Iff.mpr, Rat.cast, LinearOrderedField.coe_mem_cutMap_iff, HPow.hPow, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.CompleteField
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
inr : (↑(HPow.hPow (β := ℕ) q 2) : α) < a * a
⊢ ∃ c ∈ cutMap β (a * a), b < c

Tactic:
refine ⟨(q ^ 2 : ℚ), coe_mem_cutMap_iff.2 ?_, hbq⟩
-- Module: Mathlib.Algebra.Order.CompleteField
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
inr : ∀ (hqa : HMul.hMul (α := β) (↑q : β) (↑q : β) < inducedMap α β a * inducedMap α β a), (↑(q * q) : α) < a * a
⊢ (↑(HPow.hPow (β := ℕ) q 2) : α) < a * a

Tactic:
rw [pow_two] at hqa ⊢

Premises used: pow_two
-- Module: Mathlib.Algebra.Order.CompleteField
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
inr : HMul.hMul (α := α) (↑q : α) (↑q : α) < a * a
⊢ (↑(q * q) : α) < a * a

Tactic:
push_cast
-- Module: Mathlib.Algebra.Order.CompleteField
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
inr :
  ∀ (q' : ℚ) (hq' : LT.lt.{u_3} (α := β) (↑q : β) (↑q' : β)) (hqa' : (↑q' : α) < a),
    HMul.hMul (α := α) (↑q : α) (↑q : α) < a * 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)

Premises used: lt_of_mul_self_lt_mul_self₀, Iff.mp, ConditionallyCompleteLinearOrderedField.lt_inducedMap_iff