-- Mathlib/Algebra/Order/CompleteField.lean
theorem cutMap_add (a b : α) : cutMap β (a + b) = cutMap β a + cutMap β b

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑q₁ ∈ cutMap β a

Tactic:
rwa [coe_mem_cutMap_iff]

Result:
no goals

Proof state:
case refine_1.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)

Tactic:
refine ⟨q₁, by rwa [coe_mem_cutMap_iff], q - q₁, ?_, add_sub_cancel _ _⟩

Result:
case refine_1.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑q - ↑q₁ ∈ cutMap β b

Proof state:
case refine_1.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑q - ↑q₁ ∈ cutMap β b

Tactic:
norm_cast

Result:
case refine_1.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑(q - q₁) ∈ cutMap β b

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑qa + ↑qb < a + b

Tactic:
exact add_lt_add ha hb

Result:
no goals

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : q ∈ {t | ↑t < a + b}
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)

Tactic:
rw [mem_setOf_eq, ← sub_lt_iff_lt_add] at hq

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)

Proof state:
case refine_1.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑(q - q₁) < b

Tactic:
exact mod_cast sub_lt_comm.mp hq₁q

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
⊢ cutMap β (a + b) = cutMap β a + cutMap β b

Tactic:
refine (image_subset_iff.2 fun q hq => ?_).antisymm ?_

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : q ∈ {t | ↑t < a + b}
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)

case refine_2
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
⊢ cutMap β a + cutMap β b ⊆ Rat.cast '' {t | ↑t < a + b}

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑(qa + qb) = ↑qa + ↑qb

Tactic:
norm_cast

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑(qa + qb) = (fun x1 x2 => x1 + x2) ↑qa ↑qb

Tactic:
beta_reduce

Result:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑(qa + qb) = ↑qa + ↑qb

Proof state:
case refine_1.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑(q - q₁) ∈ cutMap β b

Tactic:
rw [coe_mem_cutMap_iff]

Result:
case refine_1.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑(q - q₁) < b

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ (fun x1 x2 => x1 + x2) ↑qa ↑qb ∈ Rat.cast '' {t | ↑t < a + b}

Tactic:
refine ⟨qa + qb, ?_, by beta_reduce; norm_cast⟩

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ qa + qb ∈ {t | ↑t < a + b}

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
⊢ cutMap β a + cutMap β b ⊆ Rat.cast '' {t | ↑t < a + b}

Tactic:
rintro _ ⟨_, ⟨qa, ha, rfl⟩, _, ⟨qb, hb, rfl⟩, rfl⟩

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ (fun x1 x2 => x1 + x2) ↑qa ↑qb ∈ Rat.cast '' {t | ↑t < a + b}

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)

Tactic:
obtain ⟨q₁, hq₁q, hq₁ab⟩ := exists_rat_btwn hq

Result:
case refine_1.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ qa + qb ∈ {t | ↑t < a + b}

Tactic:
rw [mem_setOf_eq, cast_add]

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑qa + ↑qb < a + b