awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.CompleteField
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₁ :
  b_1 =
    inducedMap.{u_4, u_3} γ β
      (({ toFun := inducedMap β γ, map_zero' := ⋯, map_add' := ⋯ : β →+ γ } : (a : β) → γ) b_1 : γ)
⊢ b_1 = inducedMap.{u_4, u_3} γ β ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)

Tactic:
rw [inducedOrderRingHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero, inducedAddHom]

Premises used: ConditionallyCompleteLinearOrderedField.inducedOrderRingHom, ConditionallyCompleteLinearOrderedField.inducedAddHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero
-- Module: Mathlib.Algebra.Order.CompleteField
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₁ : b_1 = inducedMap γ β (inducedMap β γ b_1)
⊢ b_1 =
    inducedMap.{u_4, u_3} γ β
      (({ toFun := inducedMap β γ, map_zero' := ⋯, map_add' := ⋯ : β →+ γ } : (a : β) → γ) b_1 : γ)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Order.CompleteField
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₁ h₂ : b_1 = b_1
⊢ b_1 = inducedMap γ β (inducedMap β γ b_1)

Tactic:
rw [inducedMap_inv_self β γ _]

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap_inv_self
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
β : Type u_3
γ : Type u_4
inst : Field β
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : Field γ
inst_4 : ConditionallyCompleteLinearOrder γ
inst_5 : IsStrictOrderedRing γ
⊢ (⇑(inducedOrderRingIso β γ) : (a : β) → γ) = inducedMap β γ

Tactic:
rfl

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap, rfl
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
β : Type u_3
γ : Type u_4
inst : Field β
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : Field γ
inst_4 : ConditionallyCompleteLinearOrder γ
inst_5 : IsStrictOrderedRing γ
⊢ Eq (α := γ ≃+*o β) (OrderRingIso.symm (inducedOrderRingIso β γ)) (inducedOrderRingIso γ β)

Tactic:
rfl

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap, OrderRingIso.symm, Equiv.symm, RingEquiv.symm, rfl, ConditionallyCompleteLinearOrderedField.inducedOrderRingIso
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
β : Type u_3
inst : Field β
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : IsStrictOrderedRing β
⊢ Eq (α := β ≃+*o β) (inducedOrderRingIso β β) (OrderRingIso.refl β)

Tactic:
OrderRingIso.ext inducedMap_self

Premises used: OrderRingIso.ext, ConditionallyCompleteLinearOrderedField.inducedMap_self
-- Module: Mathlib.Algebra.Order.Disjointed
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 : ι → α
i : ι
⊢ disjointed f (i + 1) = f (i + 1) \ (partialSups f : (a : ι) → α) i

Tactic:
simpa only [succ_eq_add_one] using disjointed_succ f (not_isMax i)

Premises used: Order.succ_eq_add_one, not_isMax, disjointed_succ
-- Module: Mathlib.Algebra.Order.Disjointed
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) : α)
neg :
  ∀ (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) : α)

Tactic:
by_cases hi : IsMax i

Premises used: IsMax
-- Module: Mathlib.Algebra.Order.Disjointed
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
rw : i ≤ succ i
⊢ i ≤ i + 1

Tactic:
rw [← Order.succ_eq_add_one]

Premises used: Order.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.Disjointed
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 ≤ succ i

Tactic:
apply Order.le_succ

Premises used: Order.le_succ
-- Module: Mathlib.Algebra.Order.Disjointed
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

Tactic:
have h : i ≤ i + 1 := by
        rw [← Order.succ_eq_add_one]
        apply Order.le_succ
-- Module: Mathlib.Algebra.Order.Disjointed
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
h : i ≤ i + 1
⊢ i + 1 = i

Tactic:
le_antisymm (hi h) h

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Order.Disjointed
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
h : i ≤ i + 1
⊢ i + 1 = i

Tactic:
exact le_antisymm (hi h) h

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Order.Disjointed
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

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
-- Module: Mathlib.Algebra.Order.Disjointed
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
pos : f i ≤ (Finset.Iio i).sup f ⊔ (partialSups f : (a : ι) → α) i
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (i + 1) : α)
    ((partialSups f : (a : ι) → α) i ⊔ disjointed f (i + 1) : α)

Tactic:
simp only [this, left_eq_sup, ge_iff_le, disjointed, sdiff_le_iff]

Premises used: ge_iff_le, disjointed, left_eq_sup, sdiff_le_iff
-- Module: Mathlib.Algebra.Order.Disjointed
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
⊢ f i ≤ (Finset.Iio i).sup f ⊔ (partialSups f : (a : ι) → α) i

Tactic:
apply le_trans (le_partialSups _ _) le_sup_right

Premises used: le_sup_right, le_partialSups, le_trans
-- Module: Mathlib.Algebra.Order.Disjointed
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
neg :
  Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (succ i) : α)
    ((partialSups f : (a : ι) → α) i ⊔ f (succ i) \ (partialSups f : (a : ι) → α) i : α)
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (i + 1) : α)
    ((partialSups f : (a : ι) → α) i ⊔ disjointed f (i + 1) : α)

Tactic:
rw [← Order.succ_eq_add_one, disjointed_succ _ hi]

Premises used: Order.succ_eq_add_one, disjointed_succ
-- Module: Mathlib.Algebra.Order.Disjointed
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 : ι) → α) (succ i) : α)
    ((partialSups f : (a : ι) → α) i ⊔ f (succ i) \ (partialSups f : (a : ι) → α) i : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Disjointed
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 : ι → α
hf : Monotone f
i : ι
⊢ disjointed f (i + 1) ⊔ f i = f (i + 1)

Tactic:
simpa only [succ_eq_add_one i] using hf.disjointed_succ_sup i

Premises used: Order.succ_eq_add_one, Monotone.disjointed_succ_sup
-- Module: Mathlib.Algebra.Order.Disjointed
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 : ι
rw : ¬IsMax i
⊢ disjointed f (i + 1) = f (i + 1) \ f i

Tactic:
rw [← succ_eq_add_one, hf.disjointed_succ]

Premises used: Order.succ_eq_add_one, Monotone.disjointed_succ
-- Module: Mathlib.Algebra.Order.Disjointed
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 : ι
⊢ ¬IsMax i

Tactic:
not_isMax i

Premises used: not_isMax
-- Module: Mathlib.Algebra.Order.Disjointed
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 : ι
⊢ ¬IsMax i

Tactic:
exact not_isMax i

Premises used: not_isMax
-- Module: Mathlib.Algebra.Order.Disjointed
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))
suffices : (k : ℕ) → p (f (n + 1) \ (partialSups f : (a : ℕ) → α) k)
⊢ p (disjointed f (n + 1))

Tactic:
suffices H : ∀ k, p (f (n + 1) \ partialSups f k) from disjointed_add_one f n ▸ H n
-- Module: Mathlib.Algebra.Order.Disjointed
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 (f (n + 1) \ (partialSups f : (a : ℕ) → α) 0)

Tactic:
exact hdiff h
-- Module: Mathlib.Algebra.Order.Disjointed
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 : ℕ
ih : p (f (n + 1) \ (partialSups f : (a : ℕ) → α) k)
⊢ p (f (n + 1) \ (partialSups f : (a : ℕ) → α) (k + 1))

Tactic:
simpa only [partialSups_add_one, ← sdiff_sdiff_left] using hdiff ih

Premises used: partialSups_add_one, sdiff_sdiff_left
-- Module: Mathlib.Algebra.Order.Disjointed
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)
succ :
  (k : ℕ) →
    (ih : p (f (n + 1) \ (partialSups f : (a : ℕ) → α) k)) → p (f (n + 1) \ (partialSups f : (a : ℕ) → α) (k + 1))
⊢ p (f (n + 1) \ (partialSups f : (a : ℕ) → α) k)

Tactic:
induction k with
    | zero => exact hdiff h
    | succ k ih => simpa only [partialSups_add_one, ← sdiff_sdiff_left] using hdiff ih

Premises used: partialSups_add_one, sdiff_sdiff_left, Nat.zero, Nat.succ
-- Module: Mathlib.Algebra.Order.Disjointed
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
h₀ : p (f 0)
⊢ Nat.disjointedRec (p := p) hdiff h₀ = @Eq.rec _ _ (fun (x : α) (h : f 0 = x) ↦ p x) h₀ (disjointed f 0) ⋯

Tactic:
rfl

Premises used: disjointed, Nat.disjointedRec, rfl
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
ha : 0 ≤ a
hb₀ : 0 < b
hb₁ : b ≤ 1
⊢ a ≤ a / b

Tactic:
simpa only [div_one] using div_le_div_of_nonneg_left ha hb₀ hb₁

Premises used: div_le_div_of_nonneg_left, div_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
hb : 0 < b
rw : 1 * b ≤ a ↔ b ≤ a
rw₁ rw₂ : b ≤ a ↔ b ≤ a
⊢ 1 ≤ a / b ↔ b ≤ a

Tactic:
rw [le_div_iff₀ hb, one_mul]

Premises used: le_div_iff₀, one_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
hb : 0 < b
rw : a ≤ 1 * b ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ a / b ≤ 1 ↔ a ≤ b

Tactic:
rw [div_le_iff₀ hb, one_mul]

Premises used: div_le_iff₀, one_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
hb : 0 < b
rw : 1 * b < a ↔ b < a
rw₁ rw₂ : b < a ↔ b < a
⊢ 1 < a / b ↔ b < a

Tactic:
rw [lt_div_iff₀ hb, one_mul]

Premises used: lt_div_iff₀, one_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
hb : 0 < b
rw : a < 1 * b ↔ a < b
rw₁ rw₂ : a < b ↔ a < b
⊢ a / b < 1 ↔ a < b

Tactic:
rw [div_lt_iff₀ hb, one_mul]

Premises used: div_lt_iff₀, one_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
ha : 0 < a
hb : 0 < b
⊢ 1 / a ≤ b ↔ 1 / b ≤ a

Tactic:
simpa using inv_le_comm₀ ha hb

Premises used: inv_le_comm₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
ha : 0 < a
hb : 0 < b
⊢ 1 / a < b ↔ 1 / b < a

Tactic:
simpa using inv_lt_comm₀ ha hb

Premises used: inv_lt_comm₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
ha : 0 < a
hb : 0 < b
⊢ a ≤ 1 / b ↔ b ≤ 1 / a

Tactic:
simpa using le_inv_comm₀ ha hb

Premises used: le_inv_comm₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
ha : 0 < a
hb : 0 < b
⊢ a < 1 / b ↔ b < 1 / a

Tactic:
simpa using lt_inv_comm₀ ha hb

Premises used: lt_inv_comm₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
b0 : 0 < b
⊢ b < a → 1 < a / b

Tactic:
(one_lt_div b0).mpr

Premises used: Iff.mpr, one_lt_div
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
b0 : 0 < b
⊢ a < b → a / b < 1

Tactic:
(div_lt_one b0).mpr

Premises used: Iff.mpr, div_lt_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
ha : 0 < a
h : a ≤ b
⊢ 1 / b ≤ 1 / a

Tactic:
simpa using inv_anti₀ ha h

Premises used: inv_anti₀
-- Module: Mathlib.Algebra.Order.Field.Basic
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
rwa₁ : a / b < 1
rwa₂ rwa₃ rwa₄ rwa₅ : a < b
⊢ 1 / b < 1 / a

Tactic:
rwa [lt_div_iff₀' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)]

Premises used: lt_div_iff₀', div_lt_one, div_eq_mul_one_div, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
ha : 0 < a
h : 1 / a ≤ 1 / b
⊢ 0 < 1 / a

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
ha : 0 < a
h : 1 / a ≤ 1 / b
⊢ b ≤ a

Tactic:
simpa using one_div_le_one_div_of_le (by simpa) h

Premises used: one_div_le_one_div_of_le
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
ha : 0 < a
h : 1 / a < 1 / b
⊢ 0 < 1 / a

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
ha : 0 < a
h : 1 / a < 1 / b
⊢ b < a

Tactic:
simpa using one_div_lt_one_div_of_lt (by simpa) h

Premises used: one_div_lt_one_div_of_lt
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
inst_3 : IsStrictOrderedRing α
ha : 0 ≤ a
hb : 1 ≤ b
⊢ a / b ≤ a

Tactic:
simpa only [div_one] using div_le_div_of_nonneg_left ha zero_lt_one hb

Premises used: zero_lt_one, div_le_div_of_nonneg_left, div_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
inst_3 : IsStrictOrderedRing α
ha : 0 < a
hb : 1 < b
⊢ a / b < a

Tactic:
simpa only [div_one] using div_lt_div_of_pos_left ha zero_lt_one hb

Premises used: div_lt_div_of_pos_left, zero_lt_one, div_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
inst_3 : IsStrictOrderedRing α
ha : 0 < a
hb : 0 < b
⊢ 1 / a ≤ 1 / b ↔ b ≤ a

Tactic:
div_le_div_iff_of_pos_left zero_lt_one ha hb

Premises used: div_le_div_iff_of_pos_left, zero_lt_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
inst_3 : IsStrictOrderedRing α
ha : 0 < a
hb : 0 < b
⊢ 1 / a < 1 / b ↔ b < a

Tactic:
div_lt_div_iff_of_pos_left zero_lt_one ha hb

Premises used: div_lt_div_iff_of_pos_left, zero_lt_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
h1 : 0 < a
h2 : a < 1
rwa : a < 1 / 1
rwa₁ rwa₂ rwa₃ rwa₄ : a < 1
⊢ 1 < 1 / a

Tactic:
rwa [lt_one_div (@zero_lt_one α _ _ _ _ _) h1, one_div_one]

Premises used: lt_one_div, zero_lt_one, one_div_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
h1 : 0 < a
h2 : a ≤ 1
rwa : a ≤ 1 / 1
rwa₁ rwa₂ rwa₃ rwa₄ : a ≤ 1
⊢ 1 ≤ 1 / a

Tactic:
rwa [le_one_div (@zero_lt_one α _ _ _ _ _) h1, one_div_one]

Premises used: zero_lt_one, one_div_one, le_one_div
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
h : 0 < a
⊢ 0 < a / 2

Tactic:
div_pos h zero_lt_two

Premises used: div_pos, zero_lt_two
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
⊢ 0 < 1 / 2

Tactic:
half_pos zero_lt_one

Premises used: half_pos, zero_lt_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
rw : a ≤ a * 2 ↔ 0 ≤ a
rw₁ : a ≤ a + a ↔ 0 ≤ a
rw₂ rw₃ : 0 ≤ a ↔ 0 ≤ a
⊢ a / 2 ≤ a ↔ 0 ≤ a

Tactic:
rw [div_le_iff₀ (zero_lt_two' α), mul_two, le_add_iff_nonneg_left]

Premises used: div_le_iff₀, zero_lt_two', mul_two, le_add_iff_nonneg_left
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
rw : a < a * 2 ↔ 0 < a
rw₁ : a < a + a ↔ 0 < a
rw₂ rw₃ : 0 < a ↔ 0 < a
⊢ a / 2 < a ↔ 0 < a

Tactic:
rw [div_lt_iff₀ (zero_lt_two' α), mul_two, lt_add_iff_pos_left]

Premises used: div_lt_iff₀, zero_lt_two', mul_two, lt_add_iff_pos_left
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
⊢ 1 / 2 < 1

Tactic:
half_lt_self zero_lt_one

Premises used: half_lt_self, zero_lt_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
⊢ LT.lt.{u_2} (α := α) 2⁻¹ 1

Tactic:
(one_div _).symm.trans_lt one_half_lt_one

Premises used: one_half_lt_one, one_div, Eq.trans_lt, Eq.symm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
inst_3 : IsStrictOrderedRing α
⊢ a < (a + b) / 2 ↔ a < b

Tactic:
simp [lt_div_iff₀, mul_two]

Premises used: lt_div_iff₀, mul_two
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
inst_3 : IsStrictOrderedRing α
⊢ (a + b) / 2 < b ↔ a < b

Tactic:
simp [div_lt_iff₀, mul_two]

Premises used: div_lt_iff₀, mul_two
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a : α
rw : (a + a) / 3 + a / 3 = a
rw₁ : (a + a + a) / 3 = a
rw₂ : (2 * a + a) / 3 = a
rw₃ : HAdd.hAdd (α := α) 2 1 * a / 3 = a
rw₄ : 3 * a / 3 = a
rw₅ rw₆ : a = a
⊢ a / 3 + a / 3 + a / 3 = a

Tactic:
rw [← add_div, ← add_div, ← two_mul, ← add_one_mul 2 a, two_add_one_eq_three,
    mul_div_cancel_left₀ a three_ne_zero]

Premises used: two_mul, mul_div_cancel_left₀, add_one_mul, three_ne_zero, OfNat.ofNat, two_add_one_eq_three, add_div
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
inst_3 : IsStrictOrderedRing α
ha : 0 < a
⊢ 0 < a / b ↔ 0 < b

Tactic:
simp only [div_eq_mul_inv, mul_pos_iff_of_pos_left ha, inv_pos]

Premises used: inv_pos, div_eq_mul_inv, mul_pos_iff_of_pos_left
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
inst_3 : IsStrictOrderedRing α
hb : 0 < b
⊢ 0 < a / b ↔ 0 < a

Tactic:
simp only [div_eq_mul_inv, mul_pos_iff_of_pos_right (inv_pos.2 hb)]

Premises used: Iff.mpr, inv_pos, mul_pos_iff_of_pos_right, div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b c d e : α
inst_3 : IsStrictOrderedRing α
h : a / b ≤ c / d
he : 0 ≤ e
rw : a / b * (1 / e) ≤ c / d * (1 / e)
⊢ a / (b * e) ≤ c / (d * e)

Tactic:
rw [div_mul_eq_div_mul_one_div, div_mul_eq_div_mul_one_div]

Premises used: div_mul_eq_div_mul_one_div
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b c d e : α
inst_3 : IsStrictOrderedRing α
h : a / b ≤ c / d
he : 0 ≤ e
ha : 0 ≤ 1 / e
⊢ a / b * (1 / e) ≤ c / d * (1 / e)

Tactic:
gcongr