awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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 : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : x < 0
h₁ :
  HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
    HMul.hMul (α := β) (β := β) (-(inducedAddHom α β : (a : α) → β) x : β) (-(inducedAddHom α β : (a : α) → β) x : β)
⊢ HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) (-x) : β)
      ((inducedAddHom α β : (a : α) → β) (-x) : β)
have h₂ : HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
  -HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) (-(inducedAddHom α β : (a : α) → β) x : β)
Tactic: simp_rw [map_neg, neg_mul, mul_neg, neg_neg]
-- 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 : 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 : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : x < 0
h₁ :
  HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
    HMul.hMul (α := β) (β := β) (-(inducedAddHom α β : (a : α) → β) x : β) (-(inducedAddHom α β : (a : α) → β) x : β)
h₂ :
  HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
    -HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) (-(inducedAddHom α β : (a : α) → β) x : β)
⊢ HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) (-x) : β)
      ((inducedAddHom α β : (a : α) → β) (-x) : β)
have h₃ : HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
  - -HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
Tactic: simp_rw [map_neg, neg_mul, mul_neg, neg_neg]
-- 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 : 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 : α
b : β
q : ℚ
⊢ ∀ (x : α),
    (inducedAddHom α β : (a : α) → β) (x * x) =
      HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
have suffices : ∀ (x : α),
  0 < x →
    (inducedAddHom α β : (a : α) → β) (x * x) =
      HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
Tactic: suffices ∀ x, 0 < x → inducedAddHom α β (x * x) = inducedAddHom α β x * inducedAddHom α β x by
        intro x
        obtain h | rfl | h := lt_trichotomy x 0
        · convert! this (-x) (neg_pos.2 h) using 1
          · rw [neg_mul, mul_neg, neg_neg]
          · simp_rw [map_neg, neg_mul, mul_neg, neg_neg]
        · simp only [mul_zero, map_zero]
        · exact this x h
-- 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 : 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 : α
b : β
q : ℚ
⊢ ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
have refine_1 : ∀ (x : α) (hx : 0 < x),
  ∀ a ∈ cutMap β (x * x),
    a ≤ HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
Tactic: refine fun x hx => csSup_eq_of_forall_le_of_forall_lt_exists_gt (cutMap_nonempty β _) ?_ ?_
-- 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 : 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 : α
b : β
q : ℚ
refine_1 :
  ∀ (x : α) (hx : 0 < x),
    ∀ a ∈ cutMap β (x * x),
      a ≤
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
⊢ ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
have refine_2 : ∀ (x : α) (hx : 0 < x),
  ∀ w < HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β),
    ∃ a ∈ cutMap β (x * x), w < a
Tactic: refine fun x hx => csSup_eq_of_forall_le_of_forall_lt_exists_gt (cutMap_nonempty β _) ?_ ?_
-- 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 : 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 : α
b : β
q : ℚ
⊢ ∀ {a b : β},
    OneHom.toFun (↑(↑(OrderRingHom.toRingHom (inducedOrderRingHom β γ)) : β →* γ) : OneHom β γ) a ≤
        OneHom.toFun (↑(↑(OrderRingHom.toRingHom (inducedOrderRingHom β γ)) : β →* γ) : OneHom β γ) b ↔
      a ≤ b
have dsimp : ∀ {a b : β},
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a : γ)
      ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b : γ) ↔
    a ≤ b
Tactic: dsimp
-- 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 : 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 : α
b : β
q : ℚ
⊢ ∀ {a b : β},
    LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a : γ)
        ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b : γ) ↔
      a ≤ b
have refine : ∀ {a b : β}
  (h :
    LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a : γ)
      ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b : γ)),
  a ≤ b
Tactic: refine ⟨fun h => ?_, fun h => inducedMap_mono _ _ h⟩
-- 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 : 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 : α
b : β
q : ℚ
a_1 b_1 : β
h :
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
    ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
⊢ a_1 ≤ b_1
have h₁ : a_1 = inducedMap.{u_4, u_3} γ β ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
Tactic: convert! inducedMap_mono γ β h
-- 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 : 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 : α
b : β
q : ℚ
a_1 b_1 : β
h :
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
    ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
h₁ : a_1 = inducedMap.{u_4, u_3} γ β ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
⊢ a_1 ≤ b_1
have h₂ : b_1 = inducedMap.{u_4, u_3} γ β ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
Tactic: convert! inducedMap_mono γ β h
-- 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 : 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 : α
b : β
q : ℚ
a_1 b_1 : β
h :
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
    ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
⊢ a_1 = inducedMap.{u_4, u_3} γ β ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
have h₁ : a_1 =
  inducedMap.{u_4, u_3} γ β
    (({ toFun := inducedMap β γ, map_zero' := sorry, map_add' := sorry : β →+ γ } : (a : β) → γ) a_1 : γ)
Tactic: rw [inducedOrderRingHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero, inducedAddHom]
-- 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 : 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 : α
b : β
q : ℚ
a_1 b_1 : β
h :
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
    ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
⊢ a_1 =
    inducedMap.{u_4, u_3} γ β
      (({ toFun := inducedMap β γ, map_zero' := ⋯, map_add' := ⋯ : β →+ γ } : (a : β) → γ) a_1 : γ)
have h₁ : a_1 = inducedMap γ β (inducedMap β γ a_1)
Tactic: dsimp
-- 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 : 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 : α
b : β
q : ℚ
a_1 b_1 : β
h :
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
    ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
⊢ a_1 = inducedMap γ β (inducedMap β γ a_1)
have h₁ : a_1 = a_1
Tactic: rw [inducedMap_inv_self β γ _]
-- 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 : 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 : α
b : β
q : ℚ
a_1 b_1 : β
h :
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
    ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
⊢ b_1 = inducedMap.{u_4, u_3} γ β ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
have h₁ : b_1 =
  inducedMap.{u_4, u_3} γ β
    (({ toFun := inducedMap β γ, map_zero' := sorry, map_add' := sorry : β →+ γ } : (a : β) → γ) b_1 : γ)
Tactic: rw [inducedOrderRingHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero, inducedAddHom]
-- 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 : 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 : α
b : β
q : ℚ
a_1 b_1 : β
h :
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
    ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
⊢ b_1 =
    inducedMap.{u_4, u_3} γ β
      (({ toFun := inducedMap β γ, map_zero' := ⋯, map_add' := ⋯ : β →+ γ } : (a : β) → γ) b_1 : γ)
have h₁ : b_1 = inducedMap γ β (inducedMap β γ b_1)
Tactic: dsimp
-- 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 : 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 : α
b : β
q : ℚ
a_1 b_1 : β
h :
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
    ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
⊢ b_1 = inducedMap γ β (inducedMap β γ b_1)
have h₁ : b_1 = b_1
Tactic: rw [inducedMap_inv_self β γ _]
-- Lean 4 proof step from Mathlib.Algebra.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Add ι
inst_4 : One ι
inst_5 : SuccAddOrder ι
f : ι → α
i : ι
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (i + 1) : α)
    ((partialSups f : (a : ι) → α) i ⊔ disjointed f (i + 1) : α)
have pos : ∀ (hi : IsMax i),
  Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (i + 1) : α)
    ((partialSups f : (a : ι) → α) i ⊔ disjointed f (i + 1) : α)
Tactic: by_cases hi : IsMax i
-- Lean 4 proof step from Mathlib.Algebra.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Add ι
inst_4 : One ι
inst_5 : SuccAddOrder ι
f : ι → α
i : ι
pos :
  ∀ (hi : IsMax i),
    Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (i + 1) : α)
      ((partialSups f : (a : ι) → α) i ⊔ disjointed f (i + 1) : α)
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (i + 1) : α)
    ((partialSups f : (a : ι) → α) i ⊔ disjointed f (i + 1) : α)
have neg : ∀ (hi : ¬IsMax i),
  Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (i + 1) : α)
    ((partialSups f : (a : ι) → α) i ⊔ disjointed f (i + 1) : α)
Tactic: by_cases hi : IsMax i
-- Lean 4 proof step from Mathlib.Algebra.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Add ι
inst_4 : One ι
inst_5 : SuccAddOrder ι
f : ι → α
i : ι
hi : IsMax i
⊢ i ≤ i + 1
have rw : i ≤ succ i
Tactic: rw [← Order.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Disjointed (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Add ι
inst_4 : One ι
inst_5 : SuccAddOrder ι
f : ι → α
i : ι
hi : IsMax i
⊢ i + 1 = i
have h : i ≤ i + 1
Tactic: have h : i ≤ i + 1 := by
        rw [← Order.succ_eq_add_one]
        apply Order.le_succ
-- Lean 4 proof step from Mathlib.Algebra.Order.Disjointed (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Add ι
inst_4 : One ι
inst_5 : SuccAddOrder ι
f : ι → α
i : ι
hi : IsMax i
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (i + 1) : α)
    ((partialSups f : (a : ι) → α) i ⊔ disjointed f (i + 1) : α)
have this : i + 1 = i
Tactic: have : i + 1 = i := by
      have h : i ≤ i + 1 := by
        rw [← Order.succ_eq_add_one]
        apply Order.le_succ
      exact le_antisymm (hi h) h
-- Lean 4 proof step from Mathlib.Algebra.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Add ι
inst_4 : One ι
inst_5 : SuccAddOrder ι
f : ι → α
i : ι
hi : IsMax i
this : i + 1 = i
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (i + 1) : α)
    ((partialSups f : (a : ι) → α) i ⊔ disjointed f (i + 1) : α)
have pos : f i ≤ (Finset.Iio i).sup f ⊔ (partialSups f : (a : ι) → α) i
Tactic: simp only [this, left_eq_sup, ge_iff_le, disjointed, sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Add ι
inst_4 : One ι
inst_5 : SuccAddOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (i + 1) : α)
    ((partialSups f : (a : ι) → α) i ⊔ disjointed f (i + 1) : α)
have neg : Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (succ i) : α)
  ((partialSups f : (a : ι) → α) i ⊔ f (succ i) \ (partialSups f : (a : ι) → α) i : α)
Tactic: rw [← Order.succ_eq_add_one, disjointed_succ _ hi]
-- Lean 4 proof step from Mathlib.Algebra.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Add ι
inst_4 : One ι
inst_5 : SuccAddOrder ι
inst_6 : NoMaxOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ disjointed f (i + 1) = f (i + 1) \ f i
have rw : ¬IsMax i
Tactic: rw [← succ_eq_add_one, hf.disjointed_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
⊢ p (disjointed f (n + 1))
have suffices : (k : ℕ) → p (f (n + 1) \ (partialSups f : (a : ℕ) → α) k)
Tactic: suffices H : ∀ k, p (f (n + 1) \ partialSups f k) from disjointed_add_one f n ▸ H n
-- Lean 4 proof step from Mathlib.Algebra.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
k : ℕ
⊢ p (f (n + 1) \ (partialSups f : (a : ℕ) → α) k)
have zero : p (f (n + 1) \ (partialSups f : (a : ℕ) → α) 0)
Tactic: induction k with
    | zero => exact hdiff h
    | succ k ih => simpa only [partialSups_add_one, ← sdiff_sdiff_left] using hdiff ih
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
k : ℕ
zero : p (f (n + 1) \ (partialSups f : (a : ℕ) → α) 0)
⊢ p (f (n + 1) \ (partialSups f : (a : ℕ) → α) k)
have succ : (k : ℕ) → (ih : p (f (n + 1) \ (partialSups f : (a : ℕ) → α) k)) → p (f (n + 1) \ (partialSups f : (a : ℕ) → α) (k + 1))
Tactic: induction k with
    | zero => exact hdiff h
    | succ k ih => simpa only [partialSups_add_one, ← sdiff_sdiff_left] using hdiff ih
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ 1 ≤ a / b ↔ b ≤ a
have rw : 1 * b ≤ a ↔ b ≤ a
Tactic: rw [le_div_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
hb : 0 < b
rw : 1 * b ≤ a ↔ b ≤ a
⊢ 1 ≤ a / b ↔ b ≤ a
have rw₁ : b ≤ a ↔ b ≤ a
Tactic: rw [le_div_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ a / b ≤ 1 ↔ a ≤ b
have rw : a ≤ 1 * b ↔ a ≤ b
Tactic: rw [div_le_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
hb : 0 < b
rw : a ≤ 1 * b ↔ a ≤ b
⊢ a / b ≤ 1 ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [div_le_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ b < a
have rw : 1 * b < a ↔ b < a
Tactic: rw [lt_div_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
hb : 0 < b
rw : 1 * b < a ↔ b < a
⊢ 1 < a / b ↔ b < a
have rw₁ : b < a ↔ b < a
Tactic: rw [lt_div_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ a / b < 1 ↔ a < b
have rw : a < 1 * b ↔ a < b
Tactic: rw [div_lt_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
hb : 0 < b
rw : a < 1 * b ↔ a < b
⊢ a / b < 1 ↔ a < b
have rw₁ : a < b ↔ a < b
Tactic: rw [div_lt_iff₀ hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
ha : 0 < a
h : a < b
⊢ 1 / b < 1 / a
have rwa : a * (1 / b) < 1
Tactic: rwa [lt_div_iff₀' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
ha : 0 < a
h : a < b
rwa : a * (1 / b) < 1
⊢ 1 / b < 1 / a
have rwa₁ : a / b < 1
Tactic: rwa [lt_div_iff₀' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
h1 : 0 < a
h2 : a < 1
⊢ 1 < 1 / a
have rwa : a < 1 / 1
Tactic: rwa [lt_one_div (@zero_lt_one α _ _ _ _ _) h1, one_div_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
h1 : 0 < a
h2 : a ≤ 1
⊢ 1 ≤ 1 / a
have rwa : a ≤ 1 / 1
Tactic: rwa [le_one_div (@zero_lt_one α _ _ _ _ _) h1, one_div_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
⊢ a / 2 ≤ a ↔ 0 ≤ a
have rw : a ≤ a * 2 ↔ 0 ≤ a
Tactic: rw [div_le_iff₀ (zero_lt_two' α), mul_two, le_add_iff_nonneg_left]