awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
f : ι → α
n : ℕ
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ f i
⊢ HPow.hPow (α := α) (∑ i ∈ ∅, f i) (n + 1) / HPow.hPow (α := α) (↑(card.{u_1} (α := ι) ∅) : α) n ≤
    ∑ i ∈ ∅, f i ^ (n + 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hs : s.Nonempty
⊢ 0 < HPow.hPow (α := α) (↑(#s) : α) n

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hs : s.Nonempty
inr : HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) ≤ HPow.hPow (α := α) (↑(#s) : α) n * ∑ i ∈ s, f i ^ (n + 1)
⊢ HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) / HPow.hPow (α := α) (↑(#s) : α) n ≤ ∑ i ∈ s, f i ^ (n + 1)

Tactic:
rw [div_le_iff₀' (by positivity)]

Premises used: div_le_iff₀'
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hs : s.Nonempty
⊢ HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) ≤ HPow.hPow (α := α) (↑(#s) : α) n * ∑ i ∈ s, f i ^ (n + 1)

Tactic:
pow_sum_le_card_mul_sum_pow hf _

Premises used: pow_sum_le_card_mul_sum_pow
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hs : s.Nonempty
⊢ HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) ≤ HPow.hPow (α := α) (↑(#s) : α) n * ∑ i ∈ s, f i ^ (n + 1)

Tactic:
exact pow_sum_le_card_mul_sum_pow hf _

Premises used: pow_sum_le_card_mul_sum_pow
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
inl :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := α) (∑ i ∈ ∅, f i) (↑(card.{u_1} (α := ι) ∅) : α)) 2 ≤
    HDiv.hDiv (α := α) (∑ i ∈ ∅, HPow.hPow (β := ℕ) (f i) 2) (↑(card.{u_1} (α := ι) ∅) : α)
inr :
  ∀ (hs : s.Nonempty),
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := α) (∑ i ∈ s, f i) (↑(#s) : α)) 2 ≤
      HDiv.hDiv (α := α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (↑(#s) : α)
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := α) (∑ i ∈ s, f i) (↑(#s) : α)) 2 ≤
    HDiv.hDiv (α := α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (↑(#s) : α)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
f : ι → α
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := α) (∑ i ∈ ∅, f i) (↑(card.{u_1} (α := ι) ∅) : α)) 2 ≤
    HDiv.hDiv (α := α) (∑ i ∈ ∅, HPow.hPow (β := ℕ) (f i) 2) (↑(card.{u_1} (α := ι) ∅) : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ 0 < HPow.hPow (α := α) (β := ℕ) (↑(#s) : α) 2

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ LT.lt.{u_2} (α := α) 0 (↑(#s) : α)

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
inr :
  HPow.hPow (α := α) (β := ℕ) (∑ i ∈ s, f i) 2 * (↑(#s) : α) ≤
    HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) * (↑(#s) : α)
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := α) (∑ i ∈ s, f i) (↑(#s) : α)) 2 ≤
    HDiv.hDiv (α := α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (↑(#s) : α)

Tactic:
rw [div_pow, div_le_div_iff₀ (by positivity) (by positivity), sq (#s : α), mul_left_comm,
    ← mul_assoc]

Premises used: mul_assoc, sq, mul_left_comm, Nat.cast, div_le_div_iff₀, div_pow, Finset.card
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
inr :
  HPow.hPow (α := α) (β := ℕ) (∑ i ∈ s, f i) 2 ≤ HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2)
⊢ HPow.hPow (α := α) (β := ℕ) (∑ i ∈ s, f i) 2 * (↑(#s) : α) ≤
    HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) * (↑(#s) : α)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ HPow.hPow (α := α) (β := ℕ) (∑ i ∈ s, f i) 2 ≤ HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2)

Tactic:
sq_sum_le_card_mul_sum_sq

Premises used: sq_sum_le_card_mul_sum_sq
-- Module: Mathlib.Algebra.Order.Chebyshev
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ HPow.hPow (α := α) (β := ℕ) (∑ i ∈ s, f i) 2 ≤ HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2)

Tactic:
exact sq_sum_le_card_mul_sum_sq

Premises used: sq_sum_le_card_mul_sum_sq
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : IsStrictOrderedRing α
by_contra! : ∀ (x : α) (h : ∀ (n : ℕ), (↑n : α) ≤ x), False
⊢ ∀ (x : α), ∃ (n : ℕ), x < (↑n : α)

Tactic:
by_contra! ⟨x, h⟩
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
h : ∀ (n : ℕ), (↑n : α) ≤ x
⊢ sSup (range Nat.cast) ≤ HSub.hSub (α := α) (sSup (range Nat.cast)) 1

Tactic:
have := csSup_le (range_nonempty Nat.cast)
      (forall_mem_range.2 fun m =>
        le_sub_iff_add_le.2 <| le_csSup ⟨x, forall_mem_range.2 h⟩ ⟨m+1, Nat.cast_succ m⟩)
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
h : ∀ (n : ℕ), (↑n : α) ≤ x
this : sSup (range Nat.cast) ≤ HSub.hSub (α := α) (sSup (range Nat.cast)) 1
linarith : -1 + (sSup (range Nat.cast) - HSub.hSub (α := α) (sSup (range Nat.cast)) 1) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : DivisionRing β
a₁ a₂ : α
h : a₁ ≤ a₂
⊢ cutMap β a₁ ⊆ cutMap β a₂

Tactic:
image_mono fun _ => h.trans_lt'

Premises used: Set.image_mono, LE.le.trans_lt', LinearOrderedField.cutMap
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : DivisionRing β
a : α
b : β
⊢ b ∈ cutMap β a ↔ ∃ (q : ℚ), (↑q : α) < a ∧ (↑q : β) = b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, LinearOrderedField.cutMap, Set.image
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : DivisionRing β
a : α
q : ℚ
inst_3 : CharZero β
⊢ (↑q : β) ∈ cutMap β a ↔ (↑q : α) < a

Tactic:
Rat.cast_injective.mem_set_image

Premises used: Set.Mem, setOf, LinearOrderedField.cutMap, Rat.cast_injective, Function.Injective.mem_set_image
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
a : α
⊢ cutMap α a = Iio a ∩ range Rat.cast

Tactic:
grind [mem_cutMap_iff]

Premises used: LinearOrderedField.mem_cutMap_iff
-- 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 : Archimedean α
a : α
⊢ (cutMap β a).Nonempty

Tactic:
Nonempty.image _ <| exists_rat_lt a

Premises used: LinearOrderedField.cutMap, Set.Nonempty.image, exists_rat_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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
obtain : ∀ (q : ℚ) (hq : a < (↑q : α)), BddAbove (cutMap β a)
⊢ BddAbove (cutMap β a)

Tactic:
obtain ⟨q, hq⟩ := exists_rat_gt a

Premises used: exists_rat_gt
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
q : ℚ
hq : a < (↑q : α)
⊢ BddAbove (cutMap β a)

Tactic:
⟨q, forall_mem_image.2 fun r hr => mod_cast (hq.trans' hr).le⟩

Premises used: Iff.mpr, cast, LT.lt.le, Rat.cast, LT.lt.trans', BddAbove, Set.Nonempty, Exists.intro, Eq.symm, Rat.cast_le._simp_1, Set.forall_mem_image, 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
q : ℚ
hq : a < (↑q : α)
⊢ BddAbove (cutMap β a)

Tactic:
exact ⟨q, forall_mem_image.2 fun r hr => mod_cast (hq.trans' hr).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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
⊢ cutMap β (a + b) = cutMap β a + cutMap β b

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

Premises used: Iff.mpr, LinearOrderedField.cutMap, HasSubset.Subset.antisymm, Set.image_subset_iff
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
refine_1 :
  ∀ (q : ℚ) (hq : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a + b} q), q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
refine_2 : cutMap β a + cutMap β b ⊆ Rat.cast '' {t : ℚ | (↑t : α) < a + b}
⊢ cutMap β (a + b) = cutMap β a + cutMap β b

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

Premises used: Iff.mpr, HasSubset.Subset.antisymm, Set.image_subset_iff
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
q : ℚ
hq : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a + b} q
⊢ (↑q : α) - b < a

Tactic:
rw [mem_setOf_eq, ← sub_lt_iff_lt_add] at hq

Premises used: Set.mem_setOf_eq, sub_lt_iff_lt_add
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
q : ℚ
hq : (↑q : α) - b < a
refine_1 :
  ∀ (q₁ : ℚ) (hq₁q : (↑q : α) - b < (↑q₁ : α)) (hq₁ab : (↑q₁ : α) < a), q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)

Tactic:
obtain ⟨q₁, hq₁q, hq₁ab⟩ := 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
q : ℚ
hq : (↑q : α) - b < a
q₁ : ℚ
hq₁q : (↑q : α) - b < (↑q₁ : α)
hq₁ab rwa rwa₁ rwa₂ rwa₃ : (↑q₁ : α) < a
⊢ (↑q₁ : β) ∈ cutMap β a

Tactic:
rwa [coe_mem_cutMap_iff]

Premises used: LinearOrderedField.coe_mem_cutMap_iff
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
q : ℚ
hq : (↑q : α) - b < a
q₁ : ℚ
hq₁q : (↑q : α) - b < (↑q₁ : α)
hq₁ab : (↑q₁ : α) < a
refine_1 : HSub.hSub (α := β) (↑q : β) (↑q₁ : β) ∈ cutMap β b
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)

Tactic:
refine ⟨q₁, by rwa [coe_mem_cutMap_iff], q - q₁, ?_, add_sub_cancel _ _⟩
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
q : ℚ
hq : (↑q : α) - b < a
q₁ : ℚ
hq₁q : (↑q : α) - b < (↑q₁ : α)
hq₁ab : (↑q₁ : α) < a
refine_1 : (↑(q - q₁) : β) ∈ cutMap β b
⊢ HSub.hSub (α := β) (↑q : β) (↑q₁ : β) ∈ cutMap β b

Tactic:
norm_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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
q : ℚ
hq : (↑q : α) - b < a
q₁ : ℚ
hq₁q : (↑q : α) - b < (↑q₁ : α)
hq₁ab : (↑q₁ : α) < a
refine_1 : (↑(q - q₁) : α) < b
⊢ (↑(q - q₁) : β) ∈ cutMap β b

Tactic:
rw [coe_mem_cutMap_iff]

Premises used: LinearOrderedField.coe_mem_cutMap_iff
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
q : ℚ
hq : (↑q : α) - b < a
q₁ : ℚ
hq₁q : (↑q : α) - b < (↑q₁ : α)
hq₁ab : (↑q₁ : α) < a
⊢ (↑(q - q₁) : α) < b

Tactic:
mod_cast sub_lt_comm.mp hq₁q

Premises used: sub_lt_comm, congrArg, cast, Rat.cast_sub._simp_1, LT.lt, Iff.mp, congrFun'
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : 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

Premises used: sub_lt_comm, Iff.mp
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
qa : ℚ
ha : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a} qa
qb : ℚ
hb : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < b} qb
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : qa + qb = qa + qb
⊢ (↑(qa + qb) : β) = HAdd.hAdd (α := β) (↑qa : β) (↑qb : β)

Tactic:
norm_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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
qa : ℚ
ha : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a} qa
qb : ℚ
hb : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < b} qb
refine_2 : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a + b} (qa + qb)
⊢ Membership.mem (γ := Set β) (Rat.cast '' {t : ℚ | (↑t : α) < a + b}) ((fun (x1 x2 : β) ↦ x1 + x2) (↑qa : β) (↑qb : β))

Tactic:
refine ⟨qa + qb, ?_, by beta_reduce; norm_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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
qa : ℚ
ha : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a} qa
qb : ℚ
hb : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < b} qb
refine_2 : HAdd.hAdd (α := α) (↑qa : α) (↑qb : α) < a + b
⊢ Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a + b} (qa + qb)

Tactic:
rw [mem_setOf_eq, cast_add]

Premises used: Set.mem_setOf_eq, Rat.cast_add
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
qa : ℚ
ha : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a} qa
qb : ℚ
hb : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < b} qb
⊢ HAdd.hAdd (α := α) (↑qa : α) (↑qb : α) < a + b

Tactic:
add_lt_add ha hb

Premises used: add_lt_add
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
qa : ℚ
ha : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a} qa
qb : ℚ
hb : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < b} qb
⊢ HAdd.hAdd (α := α) (↑qa : α) (↑qb : α) < a + b

Tactic:
exact add_lt_add ha hb

Premises used: add_lt_add
-- 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 α
⊢ Monotone (inducedMap α β)

Tactic:
fun _ _ h =>
  csSup_le_csSup (cutMap_bddAbove β _) (cutMap_nonempty β _) (cutMap_mono β h)

Premises used: Monotone, ConditionallyCompleteLinearOrderedField.inducedMap, LinearOrderedField.cutMap_nonempty, LinearOrderedField.cutMap_bddAbove, csSup_le_csSup, LinearOrderedField.cutMap_mono
-- 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 α
q : ℚ
⊢ inducedMap α β (↑q : α) = (↑q : β)

Tactic:
csSup_eq_of_forall_le_of_forall_lt_exists_gt
    (cutMap_nonempty β (q : α)) (fun x h => ?_) fun w h => ?_

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap, Rat.cast, LinearOrderedField.cutMap_nonempty, csSup_eq_of_forall_le_of_forall_lt_exists_gt
-- 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 α
q : ℚ
refine_1 : ∀ (x : β) (h : x ∈ cutMap.{u_2, u_3} (α := α) β (↑q : α)), x ≤ (↑q : β)
refine_2 : ∀ (w : β) (h : w < (↑q : β)), ∃ a ∈ cutMap.{u_2, u_3} (α := α) β (↑q : α), w < a
⊢ inducedMap α β (↑q : α) = (↑q : β)

Tactic:
refine csSup_eq_of_forall_le_of_forall_lt_exists_gt
    (cutMap_nonempty β (q : α)) (fun x h => ?_) fun w h => ?_

Premises used: Rat.cast, LinearOrderedField.cutMap_nonempty, csSup_eq_of_forall_le_of_forall_lt_exists_gt
-- 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 α
q : ℚ
x : β
h : x ∈ cutMap.{u_2, u_3} (α := α) β (↑q : α)
⊢ Membership.mem (γ := Set β) (Rat.cast '' {r : ℚ | LT.lt.{u_3} (α := β) (↑r : β) (↑q : β)}) x

Tactic:
rw [cutMap_coe] at h

Premises used: LinearOrderedField.cutMap_coe
-- 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 α
q : ℚ
x : β
h : Membership.mem (γ := Set β) (Rat.cast '' {r : ℚ | LT.lt.{u_3} (α := β) (↑r : β) (↑q : β)}) x
refine_1 :
  ∀ (r : ℚ) (h : Membership.mem (γ := Set ℚ) {r : ℚ | LT.lt.{u_3} (α := β) (↑r : β) (↑q : β)} r),
    LE.le.{u_3} (α := β) (↑r : β) (↑q : β)
⊢ x ≤ (↑q : β)

Tactic:
obtain ⟨r, h, rfl⟩ := h

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 α
q r : ℚ
h : Membership.mem (γ := Set ℚ) {r : ℚ | LT.lt.{u_3} (α := β) (↑r : β) (↑q : β)} r
⊢ LE.le.{u_3} (α := β) (↑r : β) (↑q : β)

Tactic:
le_of_lt h

Premises used: le_of_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 α
q r : ℚ
h : Membership.mem (γ := Set ℚ) {r : ℚ | LT.lt.{u_3} (α := β) (↑r : β) (↑q : β)} r
⊢ LE.le.{u_3} (α := β) (↑r : β) (↑q : β)

Tactic:
exact le_of_lt h

Premises used: le_of_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 α
q : ℚ
w : β
h : w < (↑q : β)
refine_2 :
  ∀ (q' : ℚ) (hwq : w < (↑q' : β)) (hq : LT.lt.{u_3} (α := β) (↑q' : β) (↑q : β)),
    ∃ a ∈ cutMap.{u_2, u_3} (α := α) β (↑q : α), w < a
⊢ ∃ a ∈ cutMap.{u_2, u_3} (α := α) β (↑q : α), w < a

Tactic:
obtain ⟨q', hwq, hq⟩ := exists_rat_btwn h

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 α
q : ℚ
w : β
h : w < (↑q : β)
q' : ℚ
hwq : w < (↑q' : β)
hq : LT.lt.{u_3} (α := β) (↑q' : β) (↑q : β)
refine_2 :
  ∃ (a : β), Membership.mem (γ := Set β) (Rat.cast '' {r : ℚ | LT.lt.{u_3} (α := β) (↑r : β) (↑q : β)}) a ∧ w < a
⊢ ∃ a ∈ cutMap.{u_2, u_3} (α := α) β (↑q : α), w < a

Tactic:
rw [cutMap_coe]

Premises used: LinearOrderedField.cutMap_coe
-- 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 α
q : ℚ
w : β
h : w < (↑q : β)
q' : ℚ
hwq : w < (↑q' : β)
hq : LT.lt.{u_3} (α := β) (↑q' : β) (↑q : β)
⊢ ∃ (a : β), Membership.mem (γ := Set β) (Rat.cast '' {r : ℚ | LT.lt.{u_3} (α := β) (↑r : β) (↑q : β)}) a ∧ w < a

Tactic:
⟨q', ⟨_, hq, rfl⟩, hwq⟩

Premises used: Rat.cast, And.intro, Exists.intro, 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 α
q : ℚ
w : β
h : w < (↑q : β)
q' : ℚ
hwq : w < (↑q' : β)
hq : LT.lt.{u_3} (α := β) (↑q' : β) (↑q : β)
⊢ ∃ (a : β), Membership.mem (γ := Set β) (Rat.cast '' {r : ℚ | LT.lt.{u_3} (α := β) (↑r : β) (↑q : β)}) a ∧ w < a

Tactic:
exact ⟨q', ⟨_, hq, rfl⟩, hwq⟩
-- 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 α β 0 = 0

Tactic:
mod_cast inducedMap_rat α β 0

Premises used: congrArg, ConditionallyCompleteLinearOrderedField.inducedMap_rat, cast, ConditionallyCompleteLinearOrderedField.inducedMap, Rat.cast, congr, Rat.cast_zero, Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq, Eq.trans