-- Mathlib/Algebra/Order/CompleteField.lean
theorem exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self (ha : 0 < a) (b : β)
    (hba : b < inducedMap α β a * inducedMap α β a) : ∃ c ∈ cutMap β (a * a), b < c

Proof state:
case inr
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
⊢ ∃ c ∈ cutMap β (a * a), b < c

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

Result:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑q ^ 2
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c

Proof state:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
⊢ ↑(q * q) < a * a

Tactic:
push_cast

Result:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
⊢ ↑q * ↑q < a * a

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ 0 ∈ cutMap β (a * a)

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

Result:
case inl
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ 0 < a * a

Proof state:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
⊢ ↑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)

Result:
case inr.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
q' : ℚ
hq' : ↑q < ↑q'
hqa' : ↑q' < a
⊢ ↑q * ↑q < a * a

Proof state:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ↑(q ^ 2) < a * a

Tactic:
rw [pow_two] at hqa ⊢

Result:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
⊢ ↑(q * q) < a * a

Proof state:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c

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

Result:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ↑(q ^ 2) < a * a

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ ∃ c ∈ cutMap β (a * a), b < c

Tactic:
refine ⟨0, ?_, hb⟩

Result:
case inl
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ 0 ∈ cutMap β (a * a)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
q' : ℚ
hq' : ↑q < ↑q'
hqa' : ↑q' < a
⊢ ↑q < ↑q'

Tactic:
assumption_mod_cast

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c

Tactic:
obtain hb | hb := lt_or_le b 0

Result:
case inl
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ ∃ c ∈ cutMap β (a * a), b < c

case inr
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
⊢ ∃ c ∈ cutMap β (a * a), b < c

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : 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'

Result:
no goals

Proof state:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑q ^ 2
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c

Tactic:
rw [← cast_pow] at hbq

Result:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c

Proof state:
case inr.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
q' : ℚ
hq' : ↑q < ↑q'
hqa' : ↑q' < a
⊢ ↑q * ↑q < a * a

Tactic:
exact mul_self_lt_mul_self (mod_cast hq.le) (hqa'.trans' <| by assumption_mod_cast)

Result:
no goals