awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
b : WithBot α
a : α
⊢ map (⇑f : (a : α) → β) ((↑a : WithBot α) + b) =
    HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (map (⇑f : (a : α) → β) b)
have coe : map (⇑f : (a : α) → β) ((↑a : WithBot α) + ⊥) =
  HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊥)
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
b : WithBot α
a : α
coe :
  map (⇑f : (a : α) → β) ((↑a : WithBot α) + ⊥) =
    HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊥)
⊢ map (⇑f : (a : α) → β) ((↑a : WithBot α) + b) =
    HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (map (⇑f : (a : α) → β) b)
have coe₁ : ∀ (a_1 : α),
  map (⇑f : (a : α) → β) ((↑a : WithBot α) + (↑a_1 : WithBot α)) =
    HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (map (⇑f : (a : α) → β) (↑a_1 : WithBot α))
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
a a_1 : α
⊢ map (⇑f : (a : α) → β) ((↑a : WithBot α) + (↑a_1 : WithBot α)) =
    HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (map (⇑f : (a : α) → β) (↑a_1 : WithBot α))
have coe : Eq.{v + 1} (α := WithBot β) (map (⇑f : (a : α) → β) (↑(a + a_1) : WithBot α) : WithBot β)
  ((↑((f : (a : α) → β) (a + a_1)) : WithBot β) : WithBot β)
Tactic: rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst : One M
inst_1 : One N
f : OneHom M N
⊢ Eq.{u_2 + 1} (α := WithBot N) (map.{u_1, u_2} (α := M) (⇑f : (a : M) → N) 1) 1
have rw : Eq.{u_2 + 1} (α := WithBot N) ((↑((f : (a : M) → N) 1) : WithBot N) : WithBot N) (1 : WithBot N)
Tactic: rw [WithBot.map_one, map_one, coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst : One M
inst_1 : One N
f : OneHom M N
rw : Eq.{u_2 + 1} (α := WithBot N) ((↑((f : (a : M) → N) 1) : WithBot N) : WithBot N) (1 : WithBot N)
⊢ Eq.{u_2 + 1} (α := WithBot N) (map.{u_1, u_2} (α := M) (⇑f : (a : M) → N) 1) 1
have rw₁ : Eq.{u_2 + 1} (α := WithBot N) (↑1 : WithBot N) 1
Tactic: rw [WithBot.map_one, map_one, coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst : One M
inst_1 : One N
f : OneHom M N
rw : Eq.{u_2 + 1} (α := WithBot N) ((↑((f : (a : M) → N) 1) : WithBot N) : WithBot N) (1 : WithBot N)
rw₁ : Eq.{u_2 + 1} (α := WithBot N) (↑1 : WithBot N) 1
⊢ Eq.{u_2 + 1} (α := WithBot N) (map.{u_1, u_2} (α := M) (⇑f : (a : M) → N) 1) 1
have rw₂ : Eq.{u_2 + 1} (α := WithBot N) 1 1
Tactic: rw [WithBot.map_one, map_one, coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : Add α
inst_1 : Add β
inst_2 : Add γ
e₁ : α ≃+ β
e₂ : β ≃+ γ
⊢ (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr
have h : ∀ (x : WithBot α),
  Eq.{u_1 + 1} (α := WithBot γ) (((e₁.trans e₂).withBotCongr : (a : WithBot α) → WithBot γ) x : WithBot γ)
    ((e₁.withBotCongr.trans e₂.withBotCongr : (a : WithBot α) → WithBot γ) x : WithBot γ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Units (goal)
Goal:
α : Type u_1
inst : Monoid α
inst_1 : LinearOrder α
a b : αˣ
⊢ (↑(a ⊔ b) : α) = max (↑a : α) (↑b : α)
have simp_rw : (↑(a ⊔ b) : α) = (↑(if a ≤ b then b else a) : α)
Tactic: simp_rw [max_def, val_le_val, ← apply_ite]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Units (goal)
Goal:
α : Type u_1
inst : Monoid α
inst_1 : LinearOrder α
a b : αˣ
⊢ (↑(a ⊓ b) : α) = min (↑a : α) (↑b : α)
have simp_rw : (↑(a ⊓ b) : α) = (↑(if a ≤ b then a else b) : α)
Tactic: simp_rw [min_def, val_le_val, ← apply_ite]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.WithTop (goal)
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
x : WithBot α
hx : x ≠ ⊥
y : WithBot α
⊢ y ≤ y + x
have bot : ∀ (hx : Ne.{u + 1} (α := WithBot α) ⊥ ⊥), y ≤ y + ⊥
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.WithTop (goal)
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
x : WithBot α
hx : x ≠ ⊥
y : WithBot α
bot : ∀ (hx : Ne.{u + 1} (α := WithBot α) ⊥ ⊥), y ≤ y + ⊥
⊢ y ≤ y + x
have coe : ∀ (a : α) (hx : (↑a : WithBot α) ≠ ⊥), y ≤ y + (↑a : WithBot α)
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.WithTop (goal)
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
y : WithBot α
a : α
hx : (↑a : WithBot α) ≠ ⊥
⊢ y ≤ y + (↑a : WithBot α)
have coe : ⊥ ≤ ⊥ + (↑a : WithBot α)
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.WithTop (goal)
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
y : WithBot α
a : α
hx : (↑a : WithBot α) ≠ ⊥
coe : ⊥ ≤ ⊥ + (↑a : WithBot α)
⊢ y ≤ y + (↑a : WithBot α)
have coe₁ : ∀ (a_1 : α), (↑a_1 : WithBot α) ≤ (↑a_1 : WithBot α) + (↑a : WithBot α)
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.WithTop (goal)
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
a : α
hx : (↑a : WithBot α) ≠ ⊥
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ (↑a_1 : WithBot α) + (↑a : WithBot α)
have coe : a_1 ≤ a_1 + a
Tactic: rw [← WithBot.coe_add, WithBot.coe_le_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.WithTop (goal)
Goal:
α : Type u
inst : AddCommMagma α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
x : WithBot α
hx : x ≠ ⊥
y : WithBot α
⊢ y ≤ x + y
have bot : ∀ (hx : Ne.{u + 1} (α := WithBot α) ⊥ ⊥), y ≤ ⊥ + y
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.WithTop (goal)
Goal:
α : Type u
inst : AddCommMagma α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
x : WithBot α
hx : x ≠ ⊥
y : WithBot α
bot : ∀ (hx : Ne.{u + 1} (α := WithBot α) ⊥ ⊥), y ≤ ⊥ + y
⊢ y ≤ x + y
have coe : ∀ (a : α) (hx : (↑a : WithBot α) ≠ ⊥), y ≤ (↑a : WithBot α) + y
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.WithTop (goal)
Goal:
α : Type u
inst : AddCommMagma α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
y : WithBot α
a : α
hx : (↑a : WithBot α) ≠ ⊥
⊢ y ≤ (↑a : WithBot α) + y
have coe : ⊥ ≤ (↑a : WithBot α) + ⊥
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.WithTop (goal)
Goal:
α : Type u
inst : AddCommMagma α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
y : WithBot α
a : α
hx : (↑a : WithBot α) ≠ ⊥
coe : ⊥ ≤ (↑a : WithBot α) + ⊥
⊢ y ≤ (↑a : WithBot α) + y
have coe₁ : ∀ (a_1 : α), (↑a_1 : WithBot α) ≤ (↑a : WithBot α) + (↑a_1 : WithBot α)
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.WithTop (goal)
Goal:
α : Type u
inst : AddCommMagma α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
a : α
hx : (↑a : WithBot α) ≠ ⊥
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ (↑a : WithBot α) + (↑a_1 : WithBot α)
have coe : a_1 ≤ a + a_1
Tactic: rw [← WithBot.coe_add, WithBot.coe_le_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.WithTop (goal)
Goal:
α : Type u_1
inst : AddMonoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedAdd α
a : WithBot α
⊢ a < 0 ↔ a = ⊥
have bot : LT.lt.{u_1} (α := WithBot α) ⊥ 0 ↔ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.WithTop (goal)
Goal:
α : Type u_1
inst : AddMonoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedAdd α
a : WithBot α
bot : LT.lt.{u_1} (α := WithBot α) ⊥ 0 ↔ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
⊢ a < 0 ↔ a = ⊥
have coe : ∀ (a : α), (↑a : WithBot α) < 0 ↔ (↑a : WithBot α) = ⊥
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monovary (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Semifield β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 < f i
hg : ∀ (i : ι), i ∈ s → 0 < g i
⊢ MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s
have rw : AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s
Tactic: rw [monovaryOn_inv_left₀ hf, antivaryOn_inv_right₀ hg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monovary (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Semifield β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 < f i
hg : ∀ (i : ι), i ∈ s → 0 < g i
rw : AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s
⊢ MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s
have rw₁ : MonovaryOn f g s ↔ MonovaryOn f g s
Tactic: rw [monovaryOn_inv_left₀ hf, antivaryOn_inv_right₀ hg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monovary (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Semifield β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 < f i
hg : ∀ (i : ι), i ∈ s → 0 < g i
⊢ AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s
have rw : MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s
Tactic: rw [antivaryOn_inv_left₀ hf, monovaryOn_inv_right₀ hg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monovary (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Semifield β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 < f i
hg : ∀ (i : ι), i ∈ s → 0 < g i
rw : MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s
⊢ AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s
have rw₁ : AntivaryOn f g s ↔ AntivaryOn f g s
Tactic: rw [antivaryOn_inv_left₀ hf, monovaryOn_inv_right₀ hg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monovary (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Semifield β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
f : ι → α
g : ι → β
hf : StrongLT (π := fun (i : ι) ↦ α) 0 f
hg : StrongLT (π := fun (i : ι) ↦ β) 0 g
⊢ Monovary f⁻¹ g⁻¹ ↔ Monovary f g
have rw : Antivary f g⁻¹ ↔ Monovary f g
Tactic: rw [monovary_inv_left₀ hf, antivary_inv_right₀ hg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monovary (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Semifield β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
f : ι → α
g : ι → β
hf : StrongLT (π := fun (i : ι) ↦ α) 0 f
hg : StrongLT (π := fun (i : ι) ↦ β) 0 g
rw : Antivary f g⁻¹ ↔ Monovary f g
⊢ Monovary f⁻¹ g⁻¹ ↔ Monovary f g
have rw₁ : Monovary f g ↔ Monovary f g
Tactic: rw [monovary_inv_left₀ hf, antivary_inv_right₀ hg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monovary (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Semifield β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
f : ι → α
g : ι → β
hf : StrongLT (π := fun (i : ι) ↦ α) 0 f
hg : StrongLT (π := fun (i : ι) ↦ β) 0 g
⊢ Antivary f⁻¹ g⁻¹ ↔ Antivary f g
have rw : Monovary f g⁻¹ ↔ Antivary f g
Tactic: rw [antivary_inv_left₀ hf, monovary_inv_right₀ hg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monovary (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Semifield β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
f : ι → α
g : ι → β
hf : StrongLT (π := fun (i : ι) ↦ α) 0 f
hg : StrongLT (π := fun (i : ι) ↦ β) 0 g
rw : Monovary f g⁻¹ ↔ Antivary f g
⊢ Antivary f⁻¹ g⁻¹ ↔ Antivary f g
have rw₁ : Antivary f g ↔ Antivary f g
Tactic: rw [antivary_inv_left₀ hf, monovary_inv_right₀ hg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monovary (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : IsStrictOrderedModule α β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) • (g j - g i)
have simp_rw : MonovaryOn f g s ↔
  (∀ (x : ι) (x_1 : x ∈ s) (x_2 : ι) (x_3 : x_2 ∈ s), f x < f x_2 → g x ≤ g x_2) ∧
    ∀ (x : ι) (x_1 : x ∈ s) (x_2 : ι) (x_3 : x_2 ∈ s), g x < g x_2 → f x ≤ f x_2
Tactic: simp_rw [smul_nonneg_iff_pos_imp_nonneg, sub_pos, sub_nonneg, forall_and]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monovary (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : IsStrictOrderedModule α β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn (β := βᵒᵈ) f ((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) s ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0
have rw : (∀ ⦃i : ι⦄,
    i ∈ s →
      ∀ ⦃j : ι⦄,
        j ∈ s →
          0 ≤
            (f j - f i) •
              HSub.hSub (α := βᵒᵈ) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j)
                (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i)) ↔
  ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0
Tactic: rw [monovaryOn_iff_forall_smul_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monovary (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : IsStrictOrderedModule α β
f : ι → α
g : ι → β
⊢ Monovary (β := βᵒᵈ) f ((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) ↔ ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0
have rw : (∀ (i j : ι),
    0 ≤
      (f j - f i) •
        HSub.hSub (α := βᵒᵈ) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j)
          (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i)) ↔
  ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0
Tactic: rw [monovary_iff_forall_smul_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monovary (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : IsStrictOrderedModule α β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn (β := βᵒᵈ) f ((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) s ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i
have rw : (∀ ⦃i : ι⦄,
    i ∈ s →
      ∀ ⦃j : ι⦄,
        j ∈ s →
          HSMul.hSMul (β := βᵒᵈ) (f i) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j) +
              HSMul.hSMul (β := βᵒᵈ) (f j) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i) ≤
            HSMul.hSMul (β := βᵒᵈ) (f i) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i) +
              HSMul.hSMul (β := βᵒᵈ) (f j) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j)) ↔
  ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i
Tactic: rw [monovaryOn_iff_smul_rearrangement]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monovary (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : IsStrictOrderedModule α β
f : ι → α
g : ι → β
⊢ Monovary (β := βᵒᵈ) f ((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) ↔
    ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i
have rw : (∀ (i j : ι),
    HSMul.hSMul (β := βᵒᵈ) (f i) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j) +
        HSMul.hSMul (β := βᵒᵈ) (f j) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i) ≤
      HSMul.hSMul (β := βᵒᵈ) (f i) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) i) +
        HSMul.hSMul (β := βᵒᵈ) (f j) (((⇑OrderDual.toDual : (a : β) → βᵒᵈ) ∘ g) j)) ↔
  ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i
Tactic: rw [monovary_iff_smul_rearrangement]
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
⊢ Eq.{u_1 + 1} (α := { x : α // 0 ≤ x }) (↑0) 0
have a : Eq.{u_1 + 1} (α := α) (↑↑0 : α) (↑0 : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Basic (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
x : ℕ
⊢ ↑(x + 1) = HAdd.hAdd (α := { x : α // 0 ≤ x }) (↑x) 1
have a : (↑↑(x + 1) : α) = (↑(HAdd.hAdd (α := { x : α // 0 ≤ x }) (↑x) 1) : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Basic (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : SemilatticeSup α
a : α
b : { x : α // 0 ≤ x }
⊢ toNonneg a ≤ b ↔ a ≤ (↑b : α)
have obtain : ∀ (b : α) (hb : 0 ≤ b),
  toNonneg a ≤ Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) b hb ↔ a ≤ (↑(Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) b hb) : α)
Tactic: obtain ⟨b, hb⟩ := b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Basic (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : { x : α // 0 ≤ x }
b : α
⊢ a < toNonneg b ↔ (↑a : α) < b
have obtain : ∀ (a : α) (ha : 0 ≤ a),
  Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) a ha < toNonneg b ↔ (↑(Subtype.mk (p := fun (x : α) ↦ 0 ≤ x) a ha) : α) < b
Tactic: obtain ⟨a, ha⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ≥0
⊢ LE.le.{u_1} (α := α) 0 (↑q : α)
have rw : 0 ≤ HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
Tactic: rw [cast_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
q : ℚ≥0
ha : 0 ≤ a
⊢ 0 ≤ q • a
have rw : 0 ≤ (↑q : α) * a
Tactic: rw [NNRat.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Field (goal)
Goal:
α : Type u_1
R : Type u_2
inst : DivisionSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : PosMulReflectLT R
r : { r : R // 0 < r }
⊢ Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯ * Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯ = 1
have a : (↑(Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) sorry * Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ sorry) : R) =
  (↑1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Field (goal)
Goal:
α : Type u_1
R : Type u_2
inst : DivisionSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : PosMulReflectLT R
r : { r : R // 0 < r }
⊢ Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯ * Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯ = 1
have a : (↑(Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ sorry * Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) sorry) : R) =
  (↑1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Field (goal)
Goal:
α : Type u_1
R : Type u_2
inst : DivisionSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : PosMulReflectLT R
r : { r : R // 0 ≤ r }ˣ
⊢ (fun (r : { r : R // 0 < r }) ↦
        ({ val := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯,
            inv := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯, val_inv := ⋯, inv_val := ⋯ } :
          { r : R // 0 ≤ r }ˣ))
      ((fun (r : { r : R // 0 ≤ r }ˣ) ↦ Subtype.mk (p := fun (r : R) ↦ 0 < r) (↑(↑r : { r : R // 0 ≤ r }) : R) ⋯) r) =
    r
have huv : (↑(↑((fun (r : { r : R // 0 < r }) ↦
              ({ val := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) sorry,
                  inv := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ sorry, val_inv := sorry, inv_val := sorry } :
                { r : R // 0 ≤ r }ˣ))
            ((fun (r : { r : R // 0 ≤ r }ˣ) ↦ Subtype.mk (p := fun (r : R) ↦ 0 < r) (↑(↑r : { r : R // 0 ≤ r }) : R) sorry)
              r)) :
        { r : R // 0 ≤ r }) :
    R) =
  (↑(↑r : { r : R // 0 ≤ r }) : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Field (goal)
Goal:
α : Type u_1
R : Type u_2
inst : DivisionSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : PosMulReflectLT R
r : { r : R // 0 < r }
⊢ (fun (r : { r : R // 0 ≤ r }ˣ) ↦ Subtype.mk (p := fun (r : R) ↦ 0 < r) (↑(↑r : { r : R // 0 ≤ r }) : R) ⋯)
      ((fun (r : { r : R // 0 < r }) ↦
          ({ val := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) ⋯,
              inv := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ ⋯, val_inv := ⋯, inv_val := ⋯ } :
            { r : R // 0 ≤ r }ˣ))
        r) =
    r
have a : (↑((fun (r : { r : R // 0 ≤ r }ˣ) ↦ Subtype.mk (p := fun (r : R) ↦ 0 < r) (↑(↑r : { r : R // 0 ≤ r }) : R) sorry)
        ((fun (r : { r : R // 0 < r }) ↦
            ({ val := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R) sorry,
                inv := Subtype.mk (p := fun (r : R) ↦ 0 ≤ r) (↑r : R)⁻¹ sorry, val_inv := sorry, inv_val := sorry } :
              { r : R // 0 ≤ r }ˣ))
          r)) :
    R) =
  (↑r : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : { x : α // 0 ≤ x }
⊢ 0 ≤ q • (↑a : α)
have rw : 0 ≤ (↑q : α) * (↑a : α)
Tactic: rw [NNRat.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Field (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ 0 ≤ q • a
have rw : 0 ≤ (↑q : α) * a
Tactic: rw [NNRat.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Ring (hypothesis)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
a b : { x : α // 0 ≤ x }
h : a ≤ b
⊢ ∃ (c : { x : α // 0 ≤ x }), b = a + c
have h₁ : (↑a : α) ≤ (↑b : α)
Tactic: rw [← Subtype.coe_le_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Ring (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
a b : { x : α // 0 ≤ x }
h : (↑a : α) ≤ (↑b : α)
⊢ ∃ (c : { x : α // 0 ≤ x }), b = a + c
have obtain : ∀ (c : α) (hc : (↑b : α) = (↑a : α) + c), ∃ (c : { x : α // 0 ≤ x }), b = a + c
Tactic: obtain ⟨c, hc⟩ := exists_add_of_le h
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Ring (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
a b : { x : α // 0 ≤ x }
h : (↑a : α) ≤ (↑b : α)
c : α
hc : (↑b : α) = (↑a : α) + c
⊢ ∃ (c : { x : α // 0 ≤ x }), b = a + c
have refine : 0 ≤ c
Tactic: refine ⟨⟨c, ?_⟩, by simp [Subtype.ext_iff, hc]⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Ring (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
a b : { x : α // 0 ≤ x }
h : (↑a : α) ≤ (↑b : α)
c : α
hc : (↑b : α) = (↑a : α) + c
⊢ 0 ≤ c
have rw : ∀ (c : α) (h : (↑a : α) + 0 ≤ (↑a : α) + c) (hc : (↑b : α) = (↑a : α) + c), 0 ≤ c
Tactic: rw [← add_zero a.val, hc] at h
Cleared hypotheses: h, c, hc