awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : LinearOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
obtain :
  ∀ (σ : Perm ι) (hσ : σ.IsCycleOn (↑s : Set ι)) (hs : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    HSMul.hSMul.{u_2, u_3, u_3} (α := α) (β := β) (∑ i ∈ s, f i) (∑ i ∈ s, g i) ≤
      HSMul.hSMul (β := β) (#s) (∑ i ∈ s, f i • g i)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := α) (β := β) (∑ i ∈ s, f i) (∑ i ∈ s, g i) ≤
    HSMul.hSMul (β := β) (#s) (∑ i ∈ s, f i • g i)
have obtain₁ : ∀ (σ : Perm ι) (hσ : σ.IsCycleOn (↑s : Set ι)) (hs : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
  ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i) ≤ HSMul.hSMul (β := β) (#(range #s)) (∑ i ∈ s, f i • g i)
Tactic: classical
  obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn
  rw [← card_range #s, sum_smul_sum_eq_sum_perm hσ]
  exact sum_le_card_nsmul _ _ _ fun n _ ↦
    hfg.sum_smul_comp_perm_le_sum_smul fun x hx ↦ hs fun h ↦ hx <| IsFixedPt.perm_pow h _
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : MonovaryOn f g (↑s : Set ι)
⊢ HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, g i) ≤ HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, f i * g i)
have rw : HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, g i) ≤ HSMul.hSMul (β := α) (#s) (∑ i ∈ s, f i * g i)
Tactic: rw [← nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : AntivaryOn f g (↑s : Set ι)
⊢ HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, f i * g i) ≤ HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have rw : HSMul.hSMul (β := α) (#s) (∑ i ∈ s, f i * g i) ≤ HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
Tactic: rw [← nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1 + 1) = HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) * ∑ i ∈ s, f i
have rw : HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) * ∑ i ∈ s, f i = HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) * ∑ i ∈ s, f i
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) * ∑ i ∈ s, f i ≤
    (HPow.hPow (α := α) (↑(#s) : α) n * ∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i
have ha : LE.le.{u_2} (α := α) 0 (∑ i ∈ s, f i)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
ha : LE.le.{u_2} (α := α) 0 (∑ i ∈ s, f i)
⊢ HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) * ∑ i ∈ s, f i ≤
    (HPow.hPow (α := α) (↑(#s) : α) n * ∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i
have hbc : HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) ≤ HPow.hPow (α := α) (↑(#s) : α) n * ∑ i ∈ s, f i ^ (n + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (HPow.hPow (α := α) (↑(#s) : α) n * ∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i =
    HPow.hPow (α := α) (↑(#s) : α) n * HMul.hMul (α := α) (∑ i ∈ s, f i ^ (n + 1)) (∑ i ∈ s, f i)
have rw : HPow.hPow (α := α) (↑(#s) : α) n * HMul.hMul (α := α) (∑ i ∈ s, f i ^ (n + 1)) (∑ i ∈ s, f i) =
  HPow.hPow (α := α) (↑(#s) : α) n * HMul.hMul (α := α) (∑ i ∈ s, f i ^ (n + 1)) (∑ i ∈ s, f i)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ HPow.hPow (α := α) (↑(#s) : α) n * HMul.hMul (α := α) (∑ i ∈ s, f i ^ (n + 1)) (∑ i ∈ s, f i) ≤
    HPow.hPow (α := α) (↑(#s) : α) n * HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, f i ^ (n + 1) * f i)
have hbc : HMul.hMul (α := α) (∑ i ∈ s, f i ^ (n + 1)) (∑ i ∈ s, f i) ≤
  HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, f i ^ (n + 1) * f i)
Tactic: gcongr _ * ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ HPow.hPow (α := α) (↑(#s) : α) n * HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, f i ^ (n + 1) * f i) =
    HPow.hPow (α := α) (↑(#s) : α) (n + 1) * ∑ i ∈ s, f i ^ (n + 1 + 1)
have simp_rw : HPow.hPow (α := α) (↑(#s) : α) n * (↑(#s) : α) * ∑ i ∈ s, f i ^ (n + 1) * f i =
  HPow.hPow (α := α) (↑(#s) : α) (n + 1) * ∑ i ∈ s, f i ^ (n + 1 + 1)
Tactic: simp_rw [← mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
⊢ HPow.hPow (α := α) (β := ℕ) (∑ i ∈ s, f i) 2 ≤ HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2)
have simp_rw : HMul.hMul (α := α) (∑ i ∈ s, f i) (∑ i ∈ s, f i) ≤ HMul.hMul (α := α) (↑(#s) : α) (∑ x ∈ s, f x * f x)
Tactic: simp_rw [sq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
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 : ℕ
⊢ HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) / HPow.hPow (α := α) (↑(#s) : α) n ≤ ∑ i ∈ s, f i ^ (n + 1)
have inl : ∀ (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: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
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 : ℕ
inl :
  ∀ (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)
⊢ HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) / HPow.hPow (α := α) (↑(#s) : α) n ≤ ∑ i ∈ s, f i ^ (n + 1)
have inr : ∀ (hs : s.Nonempty),
  HPow.hPow (α := α) (∑ i ∈ s, f i) (n + 1) / HPow.hPow (α := α) (↑(#s) : α) n ≤ ∑ i ∈ s, f i ^ (n + 1)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
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)
have inr : 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)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
f : ι → α
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := α) (∑ i ∈ s, f i) (↑(#s) : α)) 2 ≤
    HDiv.hDiv (α := α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (↑(#s) : α)
have inl : HPow.hPow (β := ℕ) (HDiv.hDiv (α := α) (∑ i ∈ ∅, f i) (↑(card.{u_1} (α := ι) ∅) : α)) 2 ≤
  HDiv.hDiv (α := α) (∑ i ∈ ∅, HPow.hPow (β := ℕ) (f i) 2) (↑(card.{u_1} (α := ι) ∅) : α)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
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} (α := ι) ∅) : α)
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := α) (∑ i ∈ s, f i) (↑(#s) : α)) 2 ≤
    HDiv.hDiv (α := α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (↑(#s) : α)
have inr : ∀ (hs : s.Nonempty),
  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
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
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 (β := ℕ) (HDiv.hDiv (α := α) (∑ i ∈ s, f i) (↑(#s) : α)) 2 ≤
    HDiv.hDiv (α := α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (↑(#s) : α)
have inr : HPow.hPow (α := α) (β := ℕ) (∑ i ∈ s, f i) 2 * (↑(#s) : α) ≤
  HMul.hMul (α := α) (↑(#s) : α) (∑ 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Chebyshev (goal)
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 * (↑(#s) : α) ≤
    HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) * (↑(#s) : α)
have inr : HPow.hPow (α := α) (β := ℕ) (∑ i ∈ s, f i) 2 ≤ HMul.hMul (α := α) (↑(#s) : α) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2)
Tactic: gcongr
-- 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 : ConditionallyCompleteLinearOrder α
inst_2 : IsStrictOrderedRing α
⊢ ∀ (x : α), ∃ (n : ℕ), x < (↑n : α)
have by_contra! : ∀ (x : α) (h : ∀ (n : ℕ), (↑n : α) ≤ x), False
Tactic: by_contra! ⟨x, h⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.CompleteField (hypothesis)
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
⊢ False
have this : 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⟩)
-- 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 : ConditionallyCompleteLinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
h : ∀ (n : ℕ), (↑n : α) ≤ x
this : sSup (range Nat.cast) ≤ HSub.hSub (α := α) (sSup (range Nat.cast)) 1
⊢ False
have linarith : -1 + (sSup (range Nat.cast) - HSub.hSub (α := α) (sSup (range Nat.cast)) 1) = 0
Tactic: linarith
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
⊢ BddAbove (cutMap β a)
have obtain : ∀ (q : ℚ) (hq : a < (↑q : α)), BddAbove (cutMap β a)
Tactic: obtain ⟨q, hq⟩ := exists_rat_gt a
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
⊢ cutMap β (a + b) = cutMap β a + cutMap β b
have refine_1 : ∀ (q : ℚ) (hq : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a + b} q), q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
Tactic: refine (image_subset_iff.2 fun q hq => ?_).antisymm ?_
-- 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 : 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)
⊢ cutMap β (a + b) = cutMap β a + cutMap β b
have refine_2 : cutMap β a + cutMap β b ⊆ Rat.cast '' {t : ℚ | (↑t : α) < a + b}
Tactic: refine (image_subset_iff.2 fun q hq => ?_).antisymm ?_
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
q : ℚ
hq : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a + b} q
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
have hq₁ : (↑q : α) - b < a
Tactic: rw [mem_setOf_eq, ← sub_lt_iff_lt_add] at hq
Cleared hypotheses: hq
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
q : ℚ
hq : (↑q : α) - b < a
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
have refine_1 : ∀ (q₁ : ℚ) (hq₁q : (↑q : α) - b < (↑q₁ : α)) (hq₁ab : (↑q₁ : α) < a), q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
Tactic: obtain ⟨q₁, hq₁q, hq₁ab⟩ := exists_rat_btwn hq
-- 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 : 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 ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
have refine_1 : HSub.hSub (α := β) (↑q : β) (↑q₁ : β) ∈ cutMap β b
Tactic: refine ⟨q₁, by rwa [coe_mem_cutMap_iff], q - q₁, ?_, add_sub_cancel _ _⟩
-- 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 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a b : α
q : ℚ
hq : (↑q : α) - b < a
q₁ : ℚ
hq₁q : (↑q : α) - b < (↑q₁ : α)
hq₁ab : (↑q₁ : α) < a
⊢ HSub.hSub (α := β) (↑q : β) (↑q₁ : β) ∈ cutMap β b
have refine_1 : (↑(q - q₁) : β) ∈ cutMap β b
Tactic: norm_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 : 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₁) : β) ∈ cutMap β b
have refine_1 : (↑(q - q₁) : α) < b
Tactic: rw [coe_mem_cutMap_iff]
-- 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 : 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
⊢ (↑(qa + qb) : β) = HAdd.hAdd (α := β) (↑qa : β) (↑qb : β)
have norm_cast : qa + qb = qa + qb
Tactic: norm_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 : 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
⊢ Membership.mem (γ := Set β) (Rat.cast '' {t : ℚ | (↑t : α) < a + b}) ((fun (x1 x2 : β) ↦ x1 + x2) (↑qa : β) (↑qb : β))
have refine_2 : Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a + b} (qa + qb)
Tactic: refine ⟨qa + qb, ?_, by beta_reduce; norm_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 : 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
⊢ Membership.mem (γ := Set ℚ) {t : ℚ | (↑t : α) < a + b} (qa + qb)
have refine_2 : HAdd.hAdd (α := α) (↑qa : α) (↑qb : α) < a + b
Tactic: rw [mem_setOf_eq, cast_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 α
q : ℚ
⊢ inducedMap α β (↑q : α) = (↑q : β)
have refine_1 : ∀ (x : β) (h : x ∈ cutMap.{u_2, u_3} (α := α) β (↑q : α)), x ≤ (↑q : β)
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt
    (cutMap_nonempty β (q : α)) (fun x h => ?_) fun w h => ?_
-- 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 α
q : ℚ
refine_1 : ∀ (x : β) (h : x ∈ cutMap.{u_2, u_3} (α := α) β (↑q : α)), x ≤ (↑q : β)
⊢ inducedMap α β (↑q : α) = (↑q : β)
have refine_2 : ∀ (w : β) (h : w < (↑q : β)), ∃ a ∈ cutMap.{u_2, u_3} (α := α) β (↑q : α), w < a
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt
    (cutMap_nonempty β (q : α)) (fun x h => ?_) fun w h => ?_
-- 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 α
q : ℚ
x : β
h : x ∈ cutMap.{u_2, u_3} (α := α) β (↑q : α)
⊢ x ≤ (↑q : β)
have h₁ : Membership.mem (γ := Set β) (Rat.cast '' {r : ℚ | LT.lt.{u_3} (α := β) (↑r : β) (↑q : β)}) x
Tactic: rw [cutMap_coe] at h
Cleared hypotheses: h
-- 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 α
q : ℚ
x : β
h : Membership.mem (γ := Set β) (Rat.cast '' {r : ℚ | LT.lt.{u_3} (α := β) (↑r : β) (↑q : β)}) x
⊢ x ≤ (↑q : β)
have refine_1 : ∀ (r : ℚ) (h : Membership.mem (γ := Set ℚ) {r : ℚ | LT.lt.{u_3} (α := β) (↑r : β) (↑q : β)} r),
  LE.le.{u_3} (α := β) (↑r : β) (↑q : β)
Tactic: obtain ⟨r, h, rfl⟩ := h
Cleared hypotheses: x, h
-- 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 α
q : ℚ
w : β
h : w < (↑q : β)
⊢ ∃ a ∈ cutMap.{u_2, u_3} (α := α) β (↑q : α), w < a
have refine_2 : ∀ (q' : ℚ) (hwq : w < (↑q' : β)) (hq : LT.lt.{u_3} (α := β) (↑q' : β) (↑q : β)),
  ∃ a ∈ cutMap.{u_2, u_3} (α := α) β (↑q : α), w < a
Tactic: obtain ⟨q', hwq, hq⟩ := exists_rat_btwn h
-- 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 α
q : ℚ
w : β
h : w < (↑q : β)
q' : ℚ
hwq : w < (↑q' : β)
hq : LT.lt.{u_3} (α := β) (↑q' : β) (↑q : β)
⊢ ∃ a ∈ cutMap.{u_2, u_3} (α := α) β (↑q : α), w < a
have refine_2 : ∃ (a : β), Membership.mem (γ := Set β) (Rat.cast '' {r : ℚ | LT.lt.{u_3} (α := β) (↑r : β) (↑q : β)}) a ∧ w < a
Tactic: rw [cutMap_coe]
-- 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 : α
q : ℚ
⊢ (↑q : β) < inducedMap α β a ↔ (↑q : α) < a
have refine_1 : ∀ (h : (↑q : β) < inducedMap α β a), (↑q : α) < a
Tactic: refine ⟨fun h => ?_, fun hq => ?_⟩
-- 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 : α
q : ℚ
refine_1 : ∀ (h : (↑q : β) < inducedMap α β a), (↑q : α) < a
⊢ (↑q : β) < inducedMap α β a ↔ (↑q : α) < a
have refine_2 : ∀ (hq : (↑q : α) < a), (↑q : β) < inducedMap α β a
Tactic: refine ⟨fun h => ?_, fun hq => ?_⟩
-- 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 : α
q : ℚ
h : (↑q : β) < inducedMap α β a
⊢ (↑q : α) < a
have h₁ : inducedMap α β (↑q : α) < inducedMap α β a
Tactic: rw [← inducedMap_rat α] at h
Cleared hypotheses: h
-- 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 : α
q : ℚ
hq : (↑q : α) < a
⊢ (↑q : β) < inducedMap α β a
have refine_2 : ∀ (q' : ℚ) (hq : LT.lt.{u_2} (α := α) (↑q : α) (↑q' : α)) (hqa : (↑q' : α) < a), (↑q : β) < inducedMap α β a
Tactic: obtain ⟨q', hq, hqa⟩ := exists_rat_btwn hq
-- 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 : α
q : ℚ
hq_1 : (↑q : α) < a
q' : ℚ
hq : LT.lt.{u_2} (α := α) (↑q : α) (↑q' : α)
hqa : (↑q' : α) < a
⊢ (↑q : β) < inducedMap α β a
have refine_2 : LT.lt.{u_3} (α := β) (↑q : β) (↑q' : β)
Tactic: apply lt_csSup_of_lt (cutMap_bddAbove β a) (coe_mem_cutMap_iff.mpr hqa)
-- 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 : ℚ
⊢ (↑q : γ) < inducedMap β γ (inducedMap α β a) ↔ (↑q : γ) < inducedMap α γ a
have rw : (↑q : β) < inducedMap α β a ↔ (↑q : γ) < inducedMap α γ a
Tactic: rw [coe_lt_inducedMap_iff, coe_lt_inducedMap_iff, Iff.comm, coe_lt_inducedMap_iff]