awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Ring (goal)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : AddGroup α
inst_2 : LinearOrder α
inst_3 : AddLeftMono α
⊢ Nontrivial.{u_1} { x : α // 0 ≤ x }
have have : ∀ (a : α) (ha : a ≠ 0), Nontrivial.{u_1} { x : α // 0 ≤ x }
Tactic: have ⟨a, ha⟩ := exists_ne (0 : α)
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Ring (goal)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : AddGroup α
inst_2 : LinearOrder α
inst_3 : AddLeftMono α
a : α
ha : a ≠ 0
⊢ Nontrivial.{u_1} { x : α // 0 ≤ x }
have inl : ∀ (lt : a < 0), Nontrivial.{u_1} { x : α // 0 ≤ x }
Tactic: obtain lt | lt := ha.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Nonneg.Ring (goal)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : AddGroup α
inst_2 : LinearOrder α
inst_3 : AddLeftMono α
a : α
ha : a ≠ 0
inl : ∀ (lt : a < 0), Nontrivial.{u_1} { x : α // 0 ≤ x }
⊢ Nontrivial.{u_1} { x : α // 0 ≤ x }
have inr : ∀ (lt : 0 < a), Nontrivial.{u_1} { x : α // 0 ≤ x }
Tactic: obtain lt | lt := ha.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
ι : Type u_2
x : α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
⊢ x * ⨆ (i : ι), f i = ⨆ (i : ι), x * f i
have rw : x * sSup (Set.range fun (i : ι) ↦ f i) = ⨆ (i : ι), x * f i
Tactic: rw [iSup, mul_sSup_distrib, iSup_range]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
ι : Type u_2
x : α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
rw : x * sSup (Set.range fun (i : ι) ↦ f i) = ⨆ (i : ι), x * f i
⊢ x * ⨆ (i : ι), f i = ⨆ (i : ι), x * f i
have rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (y : α), ⨆ (_ : Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ f i) y), x * y)
  (⨆ (i : ι), x * f i)
Tactic: rw [iSup, mul_sSup_distrib, iSup_range]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
ι : Type u_2
x : α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
rw : x * sSup (Set.range fun (i : ι) ↦ f i) = ⨆ (i : ι), x * f i
rw₁ :
  Eq.{u_1 + 1} (α := α) (⨆ (y : α), ⨆ (_ : Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ f i) y), x * y)
    (⨆ (i : ι), x * f i)
⊢ x * ⨆ (i : ι), f i = ⨆ (i : ι), x * f i
have rw₂ : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), x * f i) (⨆ (i : ι), x * f i)
Tactic: rw [iSup, mul_sSup_distrib, iSup_range]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
ι : Type u_2
x : α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
⊢ (⨆ (i : ι), f i) * x = ⨆ (i : ι), f i * x
have rw : sSup (Set.range fun (i : ι) ↦ f i) * x = ⨆ (i : ι), f i * x
Tactic: rw [iSup, sSup_mul_distrib, iSup_range]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
ι : Type u_2
x : α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
rw : sSup (Set.range fun (i : ι) ↦ f i) * x = ⨆ (i : ι), f i * x
⊢ (⨆ (i : ι), f i) * x = ⨆ (i : ι), f i * x
have rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (y : α), ⨆ (_ : Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ f i) y), y * x)
  (⨆ (i : ι), f i * x)
Tactic: rw [iSup, sSup_mul_distrib, iSup_range]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
ι : Type u_2
x : α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
rw : sSup (Set.range fun (i : ι) ↦ f i) * x = ⨆ (i : ι), f i * x
rw₁ :
  Eq.{u_1 + 1} (α := α) (⨆ (y : α), ⨆ (_ : Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ f i) y), y * x)
    (⨆ (i : ι), f i * x)
⊢ (⨆ (i : ι), f i) * x = ⨆ (i : ι), f i * x
have rw₂ : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i * x) (⨆ (i : ι), f i * x)
Tactic: rw [iSup, sSup_mul_distrib, iSup_range]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
x y z : α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
⊢ x * (y ⊔ z) = x * y ⊔ x * z
have rw : x * (y ⊔ z) = ⨆ (x_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {y, z} x_1), x * x_1
Tactic: rw [← iSup_pair, ← sSup_pair, mul_sSup_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
x y z : α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
rw : x * (y ⊔ z) = ⨆ (x_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {y, z} x_1), x * x_1
⊢ x * (y ⊔ z) = x * y ⊔ x * z
have rw₁ : x * sSup {y, z} = ⨆ (x_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {y, z} x_1), x * x_1
Tactic: rw [← iSup_pair, ← sSup_pair, mul_sSup_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
x y z : α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
rw : x * (y ⊔ z) = ⨆ (x_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {y, z} x_1), x * x_1
rw₁ : x * sSup {y, z} = ⨆ (x_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {y, z} x_1), x * x_1
⊢ x * (y ⊔ z) = x * y ⊔ x * z
have rw₂ : Eq.{u_1 + 1} (α := α) (⨆ (y_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {y, z} y_1), x * y_1)
  (⨆ (x_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {y, z} x_1), x * x_1)
Tactic: rw [← iSup_pair, ← sSup_pair, mul_sSup_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
x y z : α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
⊢ (x ⊔ y) * z = x * z ⊔ y * z
have rw : (x ⊔ y) * z = ⨆ (x_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {x, y} x_1), x_1 * z
Tactic: rw [← (@iSup_pair _ _ _ (fun _? => _? * z) _ _), ← sSup_pair, sSup_mul_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
x y z : α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
rw : (x ⊔ y) * z = ⨆ (x_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {x, y} x_1), x_1 * z
⊢ (x ⊔ y) * z = x * z ⊔ y * z
have rw₁ : sSup {x, y} * z = ⨆ (x_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {x, y} x_1), x_1 * z
Tactic: rw [← (@iSup_pair _ _ _ (fun _? => _? * z) _ _), ← sSup_pair, sSup_mul_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
x y z : α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
rw : (x ⊔ y) * z = ⨆ (x_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {x, y} x_1), x_1 * z
rw₁ : sSup {x, y} * z = ⨆ (x_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {x, y} x_1), x_1 * z
⊢ (x ⊔ y) * z = x * z ⊔ y * z
have rw₂ : Eq.{u_1 + 1} (α := α) (⨆ (y_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {x, y} y_1), y_1 * z)
  (⨆ (x_1 : α), ⨆ (_ : Membership.mem (γ := Set α) {x, y} x_1), x_1 * z)
Tactic: rw [← (@iSup_pair _ _ _ (fun _? => _? * z) _ _), ← sSup_pair, sSup_mul_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
m n₁ n₂ : α
h : n₁ ≤ n₂
⊢ m * n₁ ≤ m * n₂
have rwa : m * n₂ = m * n₂ ⊔ m * n₁
Tactic: rwa [← left_eq_sup, ← mul_sup_distrib, sup_of_le_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
m n₁ n₂ : α
h : n₁ ≤ n₂
rwa : m * n₂ = m * n₂ ⊔ m * n₁
⊢ m * n₁ ≤ m * n₂
have rwa₁ : m * n₂ = m * (n₂ ⊔ n₁)
Tactic: rwa [← left_eq_sup, ← mul_sup_distrib, sup_of_le_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
m n₁ n₂ : α
h : n₁ ≤ n₂
rwa : m * n₂ = m * n₂ ⊔ m * n₁
rwa₁ : m * n₂ = m * (n₂ ⊔ n₁)
⊢ m * n₁ ≤ m * n₂
have rwa₂ : m * n₂ = m * n₂
Tactic: rwa [← left_eq_sup, ← mul_sup_distrib, sup_of_le_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
m n₁ n₂ : α
h : n₁ ≤ n₂
⊢ LE.le (α := α) (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₁ : α)
    (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ : α)
have rwa : Eq (α := α) (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ : α)
  (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ ⊔
      swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₁ :
    α)
Tactic: rwa [← left_eq_sup, ← sup_mul_distrib, sup_of_le_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
m n₁ n₂ : α
h : n₁ ≤ n₂
rwa :
  Eq (α := α) (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ : α)
    (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ ⊔
        swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₁ :
      α)
⊢ LE.le (α := α) (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₁ : α)
    (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ : α)
have rwa₁ : swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ = (n₂ ⊔ n₁) * m
Tactic: rwa [← left_eq_sup, ← sup_mul_distrib, sup_of_le_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
m n₁ n₂ : α
h : n₁ ≤ n₂
rwa :
  Eq (α := α) (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ : α)
    (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ ⊔
        swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₁ :
      α)
rwa₁ : swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ = (n₂ ⊔ n₁) * m
⊢ LE.le (α := α) (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₁ : α)
    (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ : α)
have rwa₂ : swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ = n₂ * m
Tactic: rwa [← left_eq_sup, ← sup_mul_distrib, sup_of_le_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
x y z : α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
h1 : x ≤ y ⇨ₗ z
⊢ x * y ≤ z
have grw : (y ⇨ₗ z) * y ≤ z
Tactic: grw [h1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_1
x y z : α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
h1 : x ≤ y ⇨ᵣ z
⊢ y * x ≤ z
have grw : y * (y ⇨ᵣ z) ≤ z
Tactic: grw [h1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_3
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
x : α
⊢ ⊥ * x = ⊥
have rw : Eq.{u_3 + 1} (α := α) (⨆ (y : α), ⨆ (_ : Membership.mem (γ := Set α) ∅ y), y * x) (sSup ∅)
Tactic: rw [← sSup_empty, sSup_mul_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Order.Quantale (goal)
Goal:
α : Type u_3
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
x : α
⊢ x * ⊥ = ⊥
have rw : Eq.{u_3 + 1} (α := α) (⨆ (y : α), ⨆ (_ : Membership.mem (γ := Set α) ∅ y), x * y) (sSup ∅)
Tactic: rw [← sSup_empty, mul_sSup_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (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 ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (hamax :
    ∀ x ∈ s,
      LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
        ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α)))
  (hind :
    ∀ {σ : Perm ι} (hfg : MonovaryOn f g (↑s : Set ι)) (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
      LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i))
  {σ : Perm ι} (hfg : MonovaryOn f g (↑(insert a s) : Set ι))
  (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert a s) : Set ι)),
  LE.le.{u_3} (α := β) (∑ i ∈ insert a s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ insert a s, f i • g i)
Tactic: induction s using induction_on_max_value fun i ↦ toLex (g i, f i) generalizing σ with
  | empty => simp only [le_rfl, Finset.sum_empty]
  | insert a s has hamax hind => ?_
Cleared hypotheses: s, σ, hfg, hσ
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (hypothesis)
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 α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
hind :
  ∀ {σ : Perm ι} (hfg : MonovaryOn f g (↑s : Set ι)) (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
σ : Perm ι
hfg : MonovaryOn f g (↑(insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert a s) : Set ι)
⊢ LE.le.{u_3} (α := β) (∑ i ∈ insert a s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ insert a s, f i • g i)
have hτ : let τ := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a));
τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
Tactic: set τ : Perm ι := σ.trans (swap a (σ a)) with hτ
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (hypothesis)
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 α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
hind :
  ∀ {σ : Perm ι} (hfg : MonovaryOn f g (↑s : Set ι)) (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
σ : Perm ι
hfg : MonovaryOn f g (↑(insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
x : ι
hx : Membership.mem (γ := Set ι) {x : ι | (τ : (a : ι) → ι) x ≠ x} x
⊢ x ∈ (↑s : Set ι)
have hx₁ : ¬(if (σ : (a : ι) → ι) x = a then (σ : (a : ι) → ι) a
    else if Eq (α := ι) ((σ : (a : ι) → ι) x : ι) ((σ : (a : ι) → ι) a : ι) then a else (σ : (a : ι) → ι) x) =
    x
Tactic: simp only [τ, Ne, Set.mem_setOf_eq, Equiv.swap_comp_apply] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (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 α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
hind :
  ∀ {σ : Perm ι} (hfg : MonovaryOn f g (↑s : Set ι)) (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
σ : Perm ι
hfg : MonovaryOn f g (↑(insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
x : ι
hx :
  ¬(if (σ : (a : ι) → ι) x = a then (σ : (a : ι) → ι) a
      else if Eq (α := ι) ((σ : (a : ι) → ι) x : ι) ((σ : (a : ι) → ι) a : ι) then a else (σ : (a : ι) → ι) x) =
      x
⊢ x ∈ (↑s : Set ι)
have pos : ∀ (h₁ : (σ : (a : ι) → ι) x = a) (hx : ¬(σ : (a : ι) → ι) a = x), x ∈ (↑s : Set ι)
Tactic: split_ifs at hx with h₁ h₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (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 α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
hind :
  ∀ {σ : Perm ι} (hfg : MonovaryOn f g (↑s : Set ι)) (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
σ : Perm ι
hfg : MonovaryOn f g (↑(insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
x : ι
hx :
  ¬(if (σ : (a : ι) → ι) x = a then (σ : (a : ι) → ι) a
      else if Eq (α := ι) ((σ : (a : ι) → ι) x : ι) ((σ : (a : ι) → ι) a : ι) then a else (σ : (a : ι) → ι) x) =
      x
pos : ∀ (h₁ : (σ : (a : ι) → ι) x = a) (hx : ¬(σ : (a : ι) → ι) a = x), x ∈ (↑s : Set ι)
⊢ x ∈ (↑s : Set ι)
have pos₁ : ∀ (h₁ : ¬(σ : (a : ι) → ι) x = a) (h₂ : Eq (α := ι) ((σ : (a : ι) → ι) x : ι) ((σ : (a : ι) → ι) a : ι)) (hx : ¬a = x),
  x ∈ (↑s : Set ι)
Tactic: split_ifs at hx with h₁ h₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (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 α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
hind :
  ∀ {σ : Perm ι} (hfg : MonovaryOn f g (↑s : Set ι)) (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
σ : Perm ι
hfg : MonovaryOn f g (↑(insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
x : ι
hx :
  ¬(if (σ : (a : ι) → ι) x = a then (σ : (a : ι) → ι) a
      else if Eq (α := ι) ((σ : (a : ι) → ι) x : ι) ((σ : (a : ι) → ι) a : ι) then a else (σ : (a : ι) → ι) x) =
      x
pos : ∀ (h₁ : (σ : (a : ι) → ι) x = a) (hx : ¬(σ : (a : ι) → ι) a = x), x ∈ (↑s : Set ι)
pos₁ :
  ∀ (h₁ : ¬(σ : (a : ι) → ι) x = a) (h₂ : Eq (α := ι) ((σ : (a : ι) → ι) x : ι) ((σ : (a : ι) → ι) a : ι))
    (hx : ¬a = x), x ∈ (↑s : Set ι)
⊢ x ∈ (↑s : Set ι)
have neg : ∀ (h₁ : ¬(σ : (a : ι) → ι) x = a) (h₂ : ¬Eq (α := ι) ((σ : (a : ι) → ι) x : ι) ((σ : (a : ι) → ι) a : ι))
  (hx : ¬(σ : (a : ι) → ι) x = x), x ∈ (↑s : Set ι)
Tactic: split_ifs at hx with h₁ h₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (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 α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
hind :
  ∀ {σ : Perm ι} (hfg : MonovaryOn f g (↑s : Set ι)) (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
σ : Perm ι
hfg : MonovaryOn f g (↑(insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
x : ι
h₁ : (σ : (a : ι) → ι) x = a
hx : ¬(σ : (a : ι) → ι) a = x
⊢ x ∈ (↑s : Set ι)
have pos : ∀ (has : x ∉ s)
  (hamax :
    ∀ x_1 ∈ s,
      LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x_1, f x_1) : Lex (β × α))
        ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α)))
  (hfg : MonovaryOn f g (↑(insert x s) : Set ι)) (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert x s) : Set ι)),
  let τ := Equiv.trans σ (Equiv.swap x ((σ : (a : ι) → ι) x));
  ∀ (hτ : τ = Equiv.trans σ (Equiv.swap x ((σ : (a : ι) → ι) x))) (h₁ : (σ : (a : ι) → ι) x = x)
    (hx : ¬(σ : (a : ι) → ι) x = x), x ∈ (↑s : Set ι)
Tactic: obtain rfl | hax := eq_or_ne x a
Cleared hypotheses: a, has, hamax, hfg, hσ, τ, hτ, h₁, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Rearrangement (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 α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax :
  ∀ x ∈ s,
    LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α))
      ((toLex : (a : β × α) → Lex (β × α)) (g a, f a) : Lex (β × α))
hind :
  ∀ {σ : Perm ι} (hfg : MonovaryOn f g (↑s : Set ι)) (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
σ : Perm ι
hfg : MonovaryOn f g (↑(insert a s) : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert a s) : Set ι)
τ : Perm ι := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
hτ : τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))
x : ι
h₁ : (σ : (a : ι) → ι) x = a
hx : ¬(σ : (a : ι) → ι) a = x
pos :
  ∀ (has : x ∉ s)
    (hamax :
      ∀ x_1 ∈ s,
        LE.le (α := Lex (β × α)) ((toLex : (a : β × α) → Lex (β × α)) (g x_1, f x_1) : Lex (β × α))
          ((toLex : (a : β × α) → Lex (β × α)) (g x, f x) : Lex (β × α)))
    (hfg : MonovaryOn f g (↑(insert x s) : Set ι)) (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(insert x s) : Set ι)),
    let τ := Equiv.trans σ (Equiv.swap x ((σ : (a : ι) → ι) x));
    ∀ (hτ : τ = Equiv.trans σ (Equiv.swap x ((σ : (a : ι) → ι) x))) (h₁ : (σ : (a : ι) → ι) x = x)
      (hx : ¬(σ : (a : ι) → ι) x = x), x ∈ (↑s : Set ι)
⊢ x ∈ (↑s : Set ι)
have pos₁ : ∀ (hax : x ≠ a), x ∈ (↑s : Set ι)
Tactic: obtain rfl | hax := eq_or_ne x a