awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
q : ℚ
rw : ofRat (↑q : β) = HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
⊢ (↑q : Cauchy abv) = HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
have rw₁ : ofRat (HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β)) =
  HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
Tactic: rw [← ofRat_ratCast, Rat.cast_def, ofRat_div, ofRat_natCast, ofRat_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
q : ℚ
rw : ofRat (↑q : β) = HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
rw₁ :
  ofRat (HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β)) =
    HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
⊢ (↑q : Cauchy abv) = HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
have rw₂ : HDiv.hDiv (α := Cauchy abv) (ofRat (↑q.num : β)) (ofRat (↑q.den : β)) =
  HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
Tactic: rw [← ofRat_ratCast, Rat.cast_def, ofRat_div, ofRat_natCast, ofRat_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
q : ℚ
rw : ofRat (↑q : β) = HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
rw₁ :
  ofRat (HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β)) =
    HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
rw₂ :
  HDiv.hDiv (α := Cauchy abv) (ofRat (↑q.num : β)) (ofRat (↑q.den : β)) =
    HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
⊢ (↑q : Cauchy abv) = HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
have rw₃ : HDiv.hDiv (α := Cauchy abv) (ofRat (↑q.num : β)) (↑q.den : Cauchy abv) =
  HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
Tactic: rw [← ofRat_ratCast, Rat.cast_def, ofRat_div, ofRat_natCast, ofRat_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : DivisionRing β
abv : β → α
inst_4 : IsAbsoluteValue abv
q : ℚ
rw : ofRat (↑q : β) = HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
rw₁ :
  ofRat (HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β)) =
    HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
rw₂ :
  HDiv.hDiv (α := Cauchy abv) (ofRat (↑q.num : β)) (ofRat (↑q.den : β)) =
    HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
rw₃ :
  HDiv.hDiv (α := Cauchy abv) (ofRat (↑q.num : β)) (↑q.den : Cauchy abv) =
    HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
⊢ (↑q : Cauchy abv) = HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
have rw₄ : HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv) =
  HDiv.hDiv (α := Cauchy abv) (↑q.num : Cauchy abv) (↑q.den : Cauchy abv)
Tactic: rw [← ofRat_ratCast, Rat.cast_def, ofRat_div, ofRat_natCast, ofRat_intCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
⊢ (const abv (f.lim + g.lim) - (f + g)).LimZero
have rw : (const abv f.lim - f + (const abv g.lim - g)).LimZero
Tactic: rw [const_add, add_sub_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
⊢ const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
have a : (↑(const abv (f.lim * g.lim) - f * g) : ℕ → β) =
  (↑((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)) : ℕ → β)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
⊢ (↑(const abv (f.lim * g.lim) - f * g) : ℕ → β) =
    (↑((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)) : ℕ → β)
have a : (↑(const abv (f.lim * g.lim) - f * g) : ℕ → β) =
  (↑((const abv f.lim - f) * g) : ℕ → β) + (↑(const abv f.lim * (const abv g.lim - g)) : ℕ → β)
Tactic: rw [coe_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
⊢ (const abv (f.lim * g.lim) - f * g).LimZero
have h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
Tactic: have h :
        const abv (lim f * lim g) - f * g =
          (const abv (lim f) - f) * g + const abv (lim f) * (const abv (lim g) - g) := by
              apply Subtype.ext
              rw [coe_add]
              simp [sub_mul, mul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
⊢ (const abv (f.lim * g.lim) - f * g).LimZero
have rw : ((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)).LimZero
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
x : β
⊢ f.lim * x = (f * const abv x).lim
have rw : f.lim * x = f.lim * lim (const abv x)
Tactic: rw [← lim_mul_lim, lim_const]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
x : β
rw : f.lim * x = f.lim * lim (const abv x)
⊢ f.lim * x = (f * const abv x).lim
have rw₁ : f.lim * x = f.lim * x
Tactic: rw [← lim_mul_lim, lim_const]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
⊢ (-f - const abv (-f.lim)).LimZero
have rw : (const abv f.lim - f).LimZero
Tactic: rw [const_neg, sub_neg_eq_add, add_comm, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
⊢ f.lim - g.lim = (f - g).lim
have rw : f.lim + -g.lim = (f - g).lim
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← lim_neg, lim_add f (-g)]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
rw : f.lim + -g.lim = (f - g).lim
⊢ f.lim - g.lim = (f - g).lim
have rw₁ : f.lim + -g.lim = (f + -g).lim
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← lim_neg, lim_add f (-g)]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
rw : f.lim + -g.lim = (f - g).lim
rw₁ : f.lim + -g.lim = (f + -g).lim
⊢ f.lim - g.lim = (f - g).lim
have rw₂ : f.lim + (-g).lim = (f + -g).lim
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← lim_neg, lim_add f (-g)]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f g : CauSeq β abv
rw : f.lim + -g.lim = (f - g).lim
rw₁ : f.lim + -g.lim = (f + -g).lim
rw₂ : f.lim + (-g).lim = (f + -g).lim
⊢ f.lim - g.lim = (f - g).lim
have rw₃ : (f + -g).lim = (f + -g).lim
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← lim_neg, lim_add f (-g)]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
⊢ f.LimZero
have hf : f ≈ const abv f.lim
Tactic: have hf := equiv_lim f
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
hf : f ≈ const abv f.lim
⊢ f.LimZero
have hf₁ : f ≈ const abv 0
Tactic: rw [h] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Ring β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
h : f.LimZero
⊢ f.lim = 0
have h₁ : f = f - const abv 0
Tactic: have h₁ : f = f - const abv 0 := ext fun n => by simp
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ f.lim ≠ 0
have rwa : ∀ (hf : ¬f.lim = 0), f.lim ≠ 0
Tactic: rwa [← lim_eq_zero_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
⊢ g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
have rw : g - f * f.inv hf * g = g - f * f.inv hf * g
Tactic: rw [one_mul g]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
⊢ (g - f * f.inv hf * g).LimZero
have h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
Tactic: have h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g := by rw [one_mul g]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
⊢ (g - f * f.inv hf * g).LimZero
have h₃ : f * f.inv hf * g = f * f.inv hf * g
Tactic: have h₃ : f * inv f hf * g = (f * inv f hf) * g := by simp [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
⊢ g - f * f.inv hf * g = (1 - f * f.inv hf) * g
have rw : 1 * g - f * f.inv hf * g = (1 - f * f.inv hf) * g
Tactic: rw [h₂, h₃, ← sub_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
rw rw₁ : 1 * g - f * f.inv hf * g = (1 - f * f.inv hf) * g
⊢ g - f * f.inv hf * g = (1 - f * f.inv hf) * g
have rw₂ : (1 - f * f.inv hf) * g = (1 - f * f.inv hf) * g
Tactic: rw [h₂, h₃, ← sub_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
⊢ (g - f * f.inv hf * g).LimZero
have h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
Tactic: have h₄ : g - f * inv f hf * g = (1 - f * inv f hf) * g := by rw [h₂, h₃, ← sub_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
⊢ g - f * f.inv hf * g = g * (1 - f * f.inv hf)
have rw : (1 - f * f.inv hf) * g = g * (1 - f * f.inv hf)
Tactic: rw [h₄, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
rw : (1 - f * f.inv hf) * g = g * (1 - f * f.inv hf)
⊢ g - f * f.inv hf * g = g * (1 - f * f.inv hf)
have rw₁ : g * (1 - f * f.inv hf) = g * (1 - f * f.inv hf)
Tactic: rw [h₄, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
⊢ (g - f * f.inv hf * g).LimZero
have h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)
Tactic: have h₅ : g - f * inv f hf * g = g * (1 - f * inv f hf) := by rw [h₄, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)
⊢ g - f * f.inv hf * g = g * (1 - f.inv hf * f)
have rw : g * (1 - f * f.inv hf) = g * (1 - f.inv hf * f)
Tactic: rw [h₅, mul_comm f]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)
rw : g * (1 - f * f.inv hf) = g * (1 - f.inv hf * f)
⊢ g - f * f.inv hf * g = g * (1 - f.inv hf * f)
have rw₁ : g * (1 - f.inv hf * f) = g * (1 - f.inv hf * f)
Tactic: rw [h₅, mul_comm f]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)
⊢ (g - f * f.inv hf * g).LimZero
have h₆ : g - f * f.inv hf * g = g * (1 - f.inv hf * f)
Tactic: have h₆ : g - f * inv f hf * g = g * (1 - inv f hf * f) := by rw [h₅, mul_comm f]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f_1 : CauSeq β abv
hf_1 : ¬f_1.LimZero
hl : f_1.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)
h₆ : g - f * f.inv hf * g = g * (1 - f.inv hf * f)
⊢ (g - f * f.inv hf * g).LimZero
have rw : (g * (1 - f.inv hf * f)).LimZero
Tactic: rw [h₆]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (f.inv hf - const abv f.lim⁻¹ - (const abv f.lim - f) * (f.inv hf * const abv f.lim⁻¹)).LimZero
have rw : (f.inv hf - const abv f.lim * (f.inv hf * const abv f.lim⁻¹) -
    (const abv f.lim⁻¹ - f * (f.inv hf * const abv f.lim⁻¹))).LimZero
Tactic: rw [sub_mul, ← sub_add, sub_sub, sub_add_eq_sub_sub, sub_right_comm, sub_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (f.inv hf - const abv f.lim * (f.inv hf * const abv f.lim⁻¹)).LimZero
have rw : (f.inv hf - HMul.hMul (α := CauSeq β abv) (const abv f.lim) (inv (const abv f.lim) sorry) * f.inv hf).LimZero
Tactic: rw [← mul_assoc, mul_right_comm, const_inv hl]
-- Lean 4 proof step from Mathlib.Algebra.Order.CauSeq.Completion (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
β : Type u_2
inst_3 : Field β
abv : β → α
inst_4 : IsAbsoluteValue abv
inst_5 : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (const abv f.lim⁻¹ - f * (f.inv hf * const abv f.lim⁻¹)).LimZero
have rw : (const abv f.lim⁻¹ - f * f.inv hf * const abv f.lim⁻¹).LimZero
Tactic: rw [← mul_assoc]
-- 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 ι)
⊢ 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 ι)),
  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)
Tactic: obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn
-- 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 ι)
σ : 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)
have rw : ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k : (a : ι) → ι) i) ≤ HSMul.hSMul (β := β) (#(range #s)) (∑ i ∈ s, f i • g i)
Tactic: rw [← card_range #s, sum_smul_sum_eq_sum_perm hσ]
-- 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 ι)
⊢ 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 ι)),
  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)
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 _