awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Quantale
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
rw₂ 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)
⊢ x * (y ⊔ z) = x * y ⊔ x * z

Tactic:
rw [← iSup_pair, ← sSup_pair, mul_sSup_distrib]

Premises used: iSup_pair, mul_sSup_distrib, sSup_pair
-- Module: Mathlib.Algebra.Order.Quantale
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
rw₂ 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)
⊢ (x ⊔ y) * z = x * z ⊔ y * z

Tactic:
rw [← (@iSup_pair _ _ _ (fun _? => _? * z) _ _), ← sSup_pair, sSup_mul_distrib]

Premises used: iSup_pair, sSup_mul_distrib, sSup_pair
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
m : α
_ :
  ∀ {n₁ n₂ : α},
    (fun (x1 x2 : α) ↦ x1 ≤ x2) n₁ n₂ →
      (fun (x1 x2 : α) ↦ x1 ≤ x2) ((fun (x1 x2 : α) ↦ x1 * x2) m n₁) ((fun (x1 x2 : α) ↦ x1 * x2) m n₂)
⊢ ∀ {n₁ n₂ : α},
    (fun (x1 x2 : α) ↦ x1 ≤ x2) n₁ n₂ →
      (fun (x1 x2 : α) ↦ x1 ≤ x2) ((fun (x1 x2 : α) ↦ x1 * x2) m n₁) ((fun (x1 x2 : α) ↦ x1 * x2) m n₂)

Tactic:
_
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
m n₁ : α
_ :
  ∀ {n₂ : α},
    (fun (x1 x2 : α) ↦ x1 ≤ x2) n₁ n₂ →
      (fun (x1 x2 : α) ↦ x1 ≤ x2) ((fun (x1 x2 : α) ↦ x1 * x2) m n₁) ((fun (x1 x2 : α) ↦ x1 * x2) m n₂)
⊢ ∀ {n₂ : α},
    (fun (x1 x2 : α) ↦ x1 ≤ x2) n₁ n₂ →
      (fun (x1 x2 : α) ↦ x1 ≤ x2) ((fun (x1 x2 : α) ↦ x1 * x2) m n₁) ((fun (x1 x2 : α) ↦ x1 * x2) m n₂)

Tactic:
_
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
m n₁ n₂ : α
simp : n₁ ≤ n₂ → m * n₁ ≤ m * n₂
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) n₁ n₂ →
    (fun (x1 x2 : α) ↦ x1 ≤ x2) ((fun (x1 x2 : α) ↦ x1 * x2) m n₁) ((fun (x1 x2 : α) ↦ x1 * x2) m n₂)

Tactic:
simp only
-- Module: Mathlib.Algebra.Order.Quantale
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₁)
rwa₂ : m * n₂ = m * n₂
rwa₃ : n₁ ≤ n₂
rwa₄ : m * n₂ = m * n₂
rwa₅ rwa₆ rwa₇ : n₁ ≤ n₂
⊢ m * n₁ ≤ m * n₂

Tactic:
rwa [← left_eq_sup, ← mul_sup_distrib, sup_of_le_left]

Premises used: Quantale.mul_sup_distrib, left_eq_sup, sup_of_le_left
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
m : α
_ :
  ∀ {n₁ n₂ : α},
    (fun (x1 x2 : α) ↦ x1 ≤ x2) n₁ n₂ →
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₁)
        (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂)
⊢ ∀ {n₁ n₂ : α},
    (fun (x1 x2 : α) ↦ x1 ≤ x2) n₁ n₂ →
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (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:
_
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
m n₁ : α
_ :
  ∀ {n₂ : α},
    (fun (x1 x2 : α) ↦ x1 ≤ x2) n₁ n₂ →
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₁)
        (swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂)
⊢ ∀ {n₂ : α},
    (fun (x1 x2 : α) ↦ x1 ≤ x2) n₁ n₂ →
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (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:
_
-- Module: Mathlib.Algebra.Order.Quantale
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
rwa₂ : swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ = n₂ * m
rwa₃ : n₁ ≤ n₂
rwa₄ : swap (φ := fun (a a_1 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) m n₂ = n₂ * m
rwa₅ rwa₆ rwa₇ : 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₂ : α)

Tactic:
rwa [← left_eq_sup, ← sup_mul_distrib, sup_of_le_left]

Premises used: Quantale.sup_mul_distrib, left_eq_sup, sup_of_le_left
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_1
x y z : α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
h1 : x ≤ y ⇨ₗ z
grw : (y ⇨ₗ z) * y ≤ z
⊢ x * y ≤ z

Tactic:
grw [h1]
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_1
x y z : α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
h1 : x ≤ y ⇨ₗ z
⊢ (y ⇨ₗ z) * y ≤ z

Tactic:
simp_all only [leftMulResiduation, sSup_mul_distrib, Set.mem_setOf_eq,
      iSup_le_iff, implies_true]

Premises used: Set.mem_setOf_eq, Quantale.leftMulResiduation, sSup_mul_distrib, implies_true, iSup_le_iff
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_1
x y z : α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
h1 : x ≤ y ⇨ᵣ z
grw : y * (y ⇨ᵣ z) ≤ z
⊢ y * x ≤ z

Tactic:
grw [h1]
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_1
x y z : α
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
h1 : x ≤ y ⇨ᵣ z
⊢ y * (y ⇨ᵣ z) ≤ z

Tactic:
simp_all only [rightMulResiduation, mul_sSup_distrib, Set.mem_setOf_eq,
      iSup_le_iff, implies_true]

Premises used: Set.mem_setOf_eq, Quantale.rightMulResiduation, mul_sSup_distrib, implies_true, iSup_le_iff
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_3
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
x : α
rw : Eq.{u_3 + 1} (α := α) (⨆ (y : α), ⨆ (_ : Membership.mem (γ := Set α) ∅ y), y * x) (sSup ∅)
⊢ ⊥ * x = ⊥

Tactic:
rw [← sSup_empty, sSup_mul_distrib]

Premises used: sSup_empty, sSup_mul_distrib
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_3
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
x : α
⊢ Eq.{u_3 + 1} (α := α) (⨆ (y : α), ⨆ (_ : Membership.mem (γ := Set α) ∅ y), y * x) (sSup ∅)

Tactic:
simp only [Set.mem_empty_iff_false, not_false_eq_true, iSup_neg, iSup_bot, sSup_empty]

Premises used: sSup_empty, iSup_neg, Set.mem_empty_iff_false, not_false_eq_true, iSup_bot
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_3
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
x : α
rw : Eq.{u_3 + 1} (α := α) (⨆ (y : α), ⨆ (_ : Membership.mem (γ := Set α) ∅ y), x * y) (sSup ∅)
⊢ x * ⊥ = ⊥

Tactic:
rw [← sSup_empty, mul_sSup_distrib]

Premises used: sSup_empty, mul_sSup_distrib
-- Module: Mathlib.Algebra.Order.Quantale
Goal:
α : Type u_3
inst : Semigroup α
inst_1 : CompleteLattice α
inst_2 : IsQuantale α
x : α
⊢ Eq.{u_3 + 1} (α := α) (⨆ (y : α), ⨆ (_ : Membership.mem (γ := Set α) ∅ y), x * y) (sSup ∅)

Tactic:
simp only [Set.mem_empty_iff_false, not_false_eq_true, iSup_neg, iSup_bot, sSup_empty]

Premises used: sSup_empty, iSup_neg, Set.mem_empty_iff_false, not_false_eq_true, iSup_bot
-- Module: Mathlib.Algebra.Order.Rearrangement
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 : ι → β
σ : Perm ι
hfg : MonovaryOn f g (↑∅ : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑∅ : Set ι)
⊢ LE.le.{u_3} (α := β) (∑ i ∈ ∅, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ ∅, f i • g i)

Tactic:
simp only [le_rfl, Finset.sum_empty]

Premises used: le_rfl, Finset.sum_empty
-- Module: Mathlib.Algebra.Order.Rearrangement
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)

Tactic:
?_
-- Module: Mathlib.Algebra.Order.Rearrangement
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 ι)
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.insert a s) : Set ι))
    (hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑(Insert.insert a s) : Set ι)),
    LE.le.{u_3} (α := β) (∑ i ∈ Insert.insert a s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ Insert.insert a s, f i • g i)
⊢ LE.le.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ 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 => ?_

Premises used: le_rfl, MonovaryOn.empty, Insert.insert, Finset.sum_empty
-- Module: Mathlib.Algebra.Order.Rearrangement
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 ι)
⊢ let τ := Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a));
  τ = Equiv.trans σ (Equiv.swap a ((σ : (a : ι) → ι) a))

Tactic:
set τ : Perm ι := σ.trans (swap a (σ a)) with hτ

Premises used: Equiv.trans, Equiv.swap, Equiv.Perm, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Rearrangement
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
⊢ ¬(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

Premises used: Equiv.swap_comp_apply, Ne, Set.mem_setOf_eq
-- Module: Mathlib.Algebra.Order.Rearrangement
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 ι)
neg :
  ∀ (h₁ : ¬(σ : (a : ι) → ι) x = a) (h₂ : ¬Eq (α := ι) ((σ : (a : ι) → ι) x : ι) ((σ : (a : ι) → ι) a : ι))
    (hx : ¬(σ : (a : ι) → ι) x = x), x ∈ (↑s : Set ι)
⊢ x ∈ (↑s : Set ι)

Tactic:
split_ifs at hx with h₁ h₂
-- Module: Mathlib.Algebra.Order.Rearrangement
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 ι)
pos₁ : ∀ (hax : x ≠ a), x ∈ (↑s : Set ι)
⊢ x ∈ (↑s : Set ι)

Tactic:
obtain rfl | hax := eq_or_ne x a

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Algebra.Order.Rearrangement
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 : ι → β
s : Finset ι
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 ι
x : ι
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 ι)
τ : Perm ι := 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:
contradiction
-- Module: Mathlib.Algebra.Order.Rearrangement
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
hax : x ≠ a
⊢ x ∈ (↑s : Set ι)

Tactic:
mem_of_mem_insert_of_ne (hσ fun h ↦ hax <| h.symm.trans h₁) hax

Premises used: Finset.mem_of_mem_insert_of_ne, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Order.Rearrangement
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
hax : x ≠ a
⊢ x ∈ (↑s : Set ι)

Tactic:
exact mem_of_mem_insert_of_ne (hσ fun h ↦ hax <| h.symm.trans h₁) hax

Premises used: Finset.mem_of_mem_insert_of_ne, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Order.Rearrangement
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
h₂ : Eq (α := ι) ((σ : (a : ι) → ι) x : ι) ((σ : (a : ι) → ι) a : ι)
hx : ¬a = x
⊢ x ∈ (↑s : Set ι)

Tactic:
(hx <| σ.injective h₂.symm).elim

Premises used: False.elim, Equiv.injective, Eq.symm
-- Module: Mathlib.Algebra.Order.Rearrangement
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
h₂ : Eq (α := ι) ((σ : (a : ι) → ι) x : ι) ((σ : (a : ι) → ι) a : ι)
hx : ¬a = x
⊢ x ∈ (↑s : Set ι)

Tactic:
exact (hx <| σ.injective h₂.symm).elim

Premises used: False.elim, Equiv.injective, Eq.symm