awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i) ↔
    ¬MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)

Tactic:
simp [← hfg.sum_smul_comp_perm_eq_sum_smul_iff hσ, lt_iff_le_and_ne,
    hfg.sum_smul_comp_perm_le_sum_smul hσ]

Premises used: lt_iff_le_and_ne, MonovaryOn.sum_smul_comp_perm_le_sum_smul, MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g i) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) ↔
    ¬AntivaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)

Tactic:
simp [← hfg.sum_smul_comp_perm_eq_sum_smul_iff hσ, lt_iff_le_and_ne, eq_comm,
    hfg.sum_smul_le_sum_smul_comp_perm hσ]

Premises used: lt_iff_le_and_ne, eq_comm, AntivaryOn.sum_smul_comp_perm_eq_sum_smul_iff, AntivaryOn.sum_smul_le_sum_smul_comp_perm
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LT.lt.{u_3} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
    ¬MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)

Tactic:
simp [← hfg.sum_comp_perm_smul_eq_sum_smul_iff hσ, lt_iff_le_and_ne,
    hfg.sum_comp_perm_smul_le_sum_smul hσ]

Premises used: lt_iff_le_and_ne, MonovaryOn.sum_comp_perm_smul_le_sum_smul, MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LT.lt.{u_3} (α := β) (∑ i ∈ s, f i • g i) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) ↔
    ¬AntivaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)

Tactic:
simp [← hfg.sum_comp_perm_smul_eq_sum_smul_iff hσ, eq_comm, lt_iff_le_and_ne,
    hfg.sum_smul_le_sum_comp_perm_smul hσ]

Premises used: lt_iff_le_and_ne, AntivaryOn.sum_comp_perm_smul_eq_sum_smul_iff, AntivaryOn.sum_smul_le_sum_comp_perm_smul, eq_comm
-- 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 : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Monovary f g
⊢ LT.lt.{u_3} (α := β) (∑ i : ι, f i • g ((σ : (a : ι) → ι) i)) (∑ i : ι, f i • g i) ↔
    ¬Monovary f (g ∘ (⇑σ : (a : ι) → ι))

Tactic:
simp [(hfg.monovaryOn _).sum_smul_comp_perm_lt_sum_smul_iff fun _ _ ↦ mem_univ _]

Premises used: Finset.mem_univ, Monovary.monovaryOn, MonovaryOn.sum_smul_comp_perm_lt_sum_smul_iff
-- 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 : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Monovary f g
⊢ LT.lt.{u_3} (α := β) (∑ i : ι, f ((σ : (a : ι) → ι) i) • g i) (∑ i : ι, f i • g i) ↔
    ¬Monovary (f ∘ (⇑σ : (a : ι) → ι)) g

Tactic:
simp [(hfg.monovaryOn _).sum_comp_perm_smul_lt_sum_smul_iff fun _ _ ↦ mem_univ _]

Premises used: Finset.mem_univ, Monovary.monovaryOn, MonovaryOn.sum_comp_perm_smul_lt_sum_smul_iff
-- 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 : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Antivary f g
⊢ LT.lt.{u_3} (α := β) (∑ i : ι, f i • g i) (∑ i : ι, f i • g ((σ : (a : ι) → ι) i)) ↔
    ¬Antivary f (g ∘ (⇑σ : (a : ι) → ι))

Tactic:
simp [(hfg.antivaryOn _).sum_smul_lt_sum_smul_comp_perm_iff fun _ _ ↦ mem_univ _]

Premises used: Finset.mem_univ, AntivaryOn.sum_smul_lt_sum_smul_comp_perm_iff, Antivary.antivaryOn
-- 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 : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst_9 : Fintype ι
hfg : Antivary f g
⊢ LT.lt.{u_3} (α := β) (∑ i : ι, f i • g i) (∑ i : ι, f ((σ : (a : ι) → ι) i) • g i) ↔
    ¬Antivary (f ∘ (⇑σ : (a : ι) → ι)) g

Tactic:
simp [(hfg.antivaryOn _).sum_smul_lt_sum_comp_perm_smul_iff fun _ _ ↦ mem_univ _]

Premises used: Finset.mem_univ, AntivaryOn.sum_smul_lt_sum_comp_perm_smul_iff, Antivary.antivaryOn
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LE.le.{u_2} (α := α) (∑ i ∈ s, f i * g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i * g i)

Tactic:
hfg.sum_smul_comp_perm_le_sum_smul hσ

Premises used: MonovaryOn.sum_smul_comp_perm_le_sum_smul
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_2 + 1} (α := α) (∑ i ∈ s, f i * g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i * g i) ↔
    MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)

Tactic:
hfg.sum_smul_comp_perm_eq_sum_smul_iff hσ

Premises used: MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LT.lt.{u_2} (α := α) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i) ↔
    ¬MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)

Tactic:
hfg.sum_smul_comp_perm_lt_sum_smul_iff hσ

Premises used: MonovaryOn.sum_smul_comp_perm_lt_sum_smul_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LE.le.{u_2} (α := α) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) * g i) (∑ i ∈ s, f i * g i)

Tactic:
hfg.sum_comp_perm_smul_le_sum_smul hσ

Premises used: MonovaryOn.sum_comp_perm_smul_le_sum_smul
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_2 + 1} (α := α) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) * g i) (∑ i ∈ s, f i * g i) ↔
    MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)

Tactic:
hfg.sum_comp_perm_smul_eq_sum_smul_iff hσ

Premises used: MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LT.lt.{u_2} (α := α) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) * g i) (∑ i ∈ s, f i * g i) ↔
    ¬MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)

Tactic:
hfg.sum_comp_perm_smul_lt_sum_smul_iff hσ

Premises used: MonovaryOn.sum_comp_perm_smul_lt_sum_smul_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : AntivaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LE.le.{u_2} (α := α) (∑ i ∈ s, f i * g i) (∑ i ∈ s, f i * g ((σ : (a : ι) → ι) i))

Tactic:
hfg.sum_smul_le_sum_smul_comp_perm hσ

Premises used: AntivaryOn.sum_smul_le_sum_smul_comp_perm
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : AntivaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_2 + 1} (α := α) (∑ i ∈ s, f i * g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i * g i) ↔
    AntivaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)

Tactic:
hfg.sum_smul_comp_perm_eq_sum_smul_iff hσ

Premises used: AntivaryOn.sum_smul_comp_perm_eq_sum_smul_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : AntivaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LT.lt.{u_2} (α := α) (∑ i ∈ s, f i * g i) (∑ i ∈ s, f i * g ((σ : (a : ι) → ι) i)) ↔
    ¬AntivaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)

Tactic:
hfg.sum_smul_lt_sum_smul_comp_perm_iff hσ

Premises used: AntivaryOn.sum_smul_lt_sum_smul_comp_perm_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : AntivaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LE.le.{u_2} (α := α) (∑ i ∈ s, f i * g i) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) * g i)

Tactic:
hfg.sum_smul_le_sum_comp_perm_smul hσ

Premises used: AntivaryOn.sum_smul_le_sum_comp_perm_smul
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : AntivaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_2 + 1} (α := α) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) * g i) (∑ i ∈ s, f i * g i) ↔
    AntivaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)

Tactic:
hfg.sum_comp_perm_smul_eq_sum_smul_iff hσ

Premises used: AntivaryOn.sum_comp_perm_smul_eq_sum_smul_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : AntivaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ LT.lt.{u_2} (α := α) (∑ i ∈ s, f i * g i) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) * g i) ↔
    ¬AntivaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)

Tactic:
hfg.sum_smul_lt_sum_comp_perm_smul_iff hσ

Premises used: AntivaryOn.sum_smul_lt_sum_comp_perm_smul_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
σ : Perm ι
f g : ι → α
inst_4 : Fintype ι
hfg : Monovary f g
⊢ LE.le.{u_2} (α := α) (∑ i : ι, f i * g ((σ : (a : ι) → ι) i)) (∑ i : ι, f i * g i)

Tactic:
hfg.sum_smul_comp_perm_le_sum_smul

Premises used: Monovary.sum_smul_comp_perm_le_sum_smul
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
σ : Perm ι
f g : ι → α
inst_4 : Fintype ι
hfg : Monovary f g
⊢ Eq.{u_2 + 1} (α := α) (∑ i : ι, f i * g ((σ : (a : ι) → ι) i)) (∑ i : ι, f i * g i) ↔
    Monovary f (g ∘ (⇑σ : (a : ι) → ι))

Tactic:
hfg.sum_smul_comp_perm_eq_sum_smul_iff

Premises used: Monovary.sum_smul_comp_perm_eq_sum_smul_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
σ : Perm ι
f g : ι → α
inst_4 : Fintype ι
hfg : Monovary f g
⊢ LT.lt.{u_2} (α := α) (∑ i : ι, f i * g ((σ : (a : ι) → ι) i)) (∑ i : ι, f i * g i) ↔
    ¬Monovary f (g ∘ (⇑σ : (a : ι) → ι))

Tactic:
hfg.sum_smul_comp_perm_lt_sum_smul_iff

Premises used: Monovary.sum_smul_comp_perm_lt_sum_smul_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
σ : Perm ι
f g : ι → α
inst_4 : Fintype ι
hfg : Monovary f g
⊢ LE.le.{u_2} (α := α) (∑ i : ι, f ((σ : (a : ι) → ι) i) * g i) (∑ i : ι, f i * g i)

Tactic:
hfg.sum_comp_perm_smul_le_sum_smul

Premises used: Monovary.sum_comp_perm_smul_le_sum_smul
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
σ : Perm ι
f g : ι → α
inst_4 : Fintype ι
hfg : Monovary f g
⊢ Eq.{u_2 + 1} (α := α) (∑ i : ι, f ((σ : (a : ι) → ι) i) * g i) (∑ i : ι, f i * g i) ↔
    Monovary (f ∘ (⇑σ : (a : ι) → ι)) g

Tactic:
hfg.sum_comp_perm_smul_eq_sum_smul_iff

Premises used: Monovary.sum_comp_perm_smul_eq_sum_smul_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
σ : Perm ι
f g : ι → α
inst_4 : Fintype ι
hfg : Monovary f g
⊢ LT.lt.{u_2} (α := α) (∑ i : ι, f ((σ : (a : ι) → ι) i) * g i) (∑ i : ι, f i * g i) ↔
    ¬Monovary (f ∘ (⇑σ : (a : ι) → ι)) g

Tactic:
hfg.sum_comp_perm_smul_lt_sum_smul_iff

Premises used: Monovary.sum_comp_perm_smul_lt_sum_smul_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
σ : Perm ι
f g : ι → α
inst_4 : Fintype ι
hfg : Antivary f g
⊢ LE.le.{u_2} (α := α) (∑ i : ι, f i * g i) (∑ i : ι, f i * g ((σ : (a : ι) → ι) i))

Tactic:
hfg.sum_smul_le_sum_smul_comp_perm

Premises used: Antivary.sum_smul_le_sum_smul_comp_perm
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
σ : Perm ι
f g : ι → α
inst_4 : Fintype ι
hfg : Antivary f g
⊢ Eq.{u_2 + 1} (α := α) (∑ i : ι, f i * g ((σ : (a : ι) → ι) i)) (∑ i : ι, f i * g i) ↔
    Antivary f (g ∘ (⇑σ : (a : ι) → ι))

Tactic:
hfg.sum_smul_comp_perm_eq_sum_smul_iff

Premises used: Antivary.sum_smul_comp_perm_eq_sum_smul_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
σ : Perm ι
f g : ι → α
inst_4 : Fintype ι
hfg : Antivary f g
⊢ LT.lt.{u_2} (α := α) (∑ i : ι, f i • g i) (∑ i : ι, f i • g ((σ : (a : ι) → ι) i)) ↔
    ¬Antivary f (g ∘ (⇑σ : (a : ι) → ι))

Tactic:
hfg.sum_smul_lt_sum_smul_comp_perm_iff

Premises used: Antivary.sum_smul_lt_sum_smul_comp_perm_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
σ : Perm ι
f g : ι → α
inst_4 : Fintype ι
hfg : Antivary f g
⊢ LE.le.{u_2} (α := α) (∑ i : ι, f i * g i) (∑ i : ι, f ((σ : (a : ι) → ι) i) * g i)

Tactic:
hfg.sum_smul_le_sum_comp_perm_smul

Premises used: Antivary.sum_smul_le_sum_comp_perm_smul
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
σ : Perm ι
f g : ι → α
inst_4 : Fintype ι
hfg : Antivary f g
⊢ Eq.{u_2 + 1} (α := α) (∑ i : ι, f ((σ : (a : ι) → ι) i) * g i) (∑ i : ι, f i * g i) ↔
    Antivary (f ∘ (⇑σ : (a : ι) → ι)) g

Tactic:
hfg.sum_comp_perm_smul_eq_sum_smul_iff

Premises used: Antivary.sum_comp_perm_smul_eq_sum_smul_iff
-- Module: Mathlib.Algebra.Order.Rearrangement
Goal:
ι : Type u_1
α : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
σ : Perm ι
f g : ι → α
inst_4 : Fintype ι
hfg : Antivary f g
⊢ LT.lt.{u_2} (α := α) (∑ i : ι, f i * g i) (∑ i : ι, f ((σ : (a : ι) → ι) i) * g i) ↔
    ¬Antivary (f ∘ (⇑σ : (a : ι) → ι)) g

Tactic:
hfg.sum_smul_lt_sum_comp_perm_smul_iff

Premises used: Antivary.sum_smul_lt_sum_comp_perm_smul_iff
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a : α
inl : ∀ (n0 : 0 ≤ n), |a ^ n|ₘ = |a|ₘ ^ |n|
inr : ∀ (n0 : n ≤ 0), |a ^ n|ₘ = |a|ₘ ^ |n|
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|

Tactic:
obtain n0 | n0 := le_total 0 n

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a : α
n0 : 0 ≤ n
inl : ∀ (n : ℕ) (n0 : LE.le (α := ℤ) 0 (↑n : ℤ)), |HPow.hPow (β := ℤ) a (↑n : ℤ)|ₘ = HPow.hPow (β := ℤ) |a|ₘ |(↑n : ℤ)|
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|

Tactic:
obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le n0

Premises used: Int.eq_ofNat_of_zero_le, rfl
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
n : ℕ
n0 : LE.le (α := ℤ) 0 (↑n : ℤ)
⊢ |HPow.hPow (β := ℤ) a (↑n : ℤ)|ₘ = HPow.hPow (β := ℤ) |a|ₘ |(↑n : ℤ)|

Tactic:
simp only [mabs_pow, zpow_natCast, Nat.abs_cast]

Premises used: zpow_natCast, mabs_pow, Nat.abs_cast
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
inr : ∀ (m : ℕ) (h : -n = (↑m : ℤ)), |a ^ n|ₘ = |a|ₘ ^ |n|
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|

Tactic:
obtain ⟨m, h⟩ := Int.eq_ofNat_of_zero_le (neg_nonneg.2 n0)

Premises used: Iff.mpr, Int.eq_ofNat_of_zero_le, neg_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = (↑m : ℤ)
inr : |a ^ m|ₘ = |a|ₘ ^ m
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|

Tactic:
rw [← mabs_inv, ← zpow_neg, ← abs_neg, h, zpow_natCast, Nat.abs_cast, zpow_natCast]

Premises used: zpow_natCast, abs_neg, Nat.abs_cast, zpow_neg, mabs_inv
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = (↑m : ℤ)
⊢ |a ^ m|ₘ = |a|ₘ ^ m

Tactic:
mabs_pow m _

Premises used: mabs_pow
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = (↑m : ℤ)
⊢ |a ^ m|ₘ = |a|ₘ ^ m

Tactic:
exact mabs_pow m _

Premises used: mabs_pow
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Ring α
a : α
inl : ∀ (h : |a| = a), Odd |a| ↔ Odd a
inr : ∀ (h : |a| = -a), Odd |a| ↔ Odd a
⊢ Odd |a| ↔ Odd a

Tactic:
rcases abs_choice a with h | h

Premises used: abs_choice
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Ring α
a : α
h : |a| = a
⊢ Odd |a| ↔ Odd a

Tactic:
simp only [h, odd_neg]

Premises used: odd_neg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Ring α
a : α
h : |a| = -a
⊢ Odd |a| ↔ Odd a

Tactic:
simp only [h, odd_neg]

Premises used: odd_neg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
⊢ Eq.{u_1 + 1} (α := α) |1| 1

Tactic:
abs_of_nonneg zero_le_one

Premises used: zero_le_one, abs_of_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
⊢ Eq.{u_1 + 1} (α := α) |2| 2

Tactic:
abs_of_nonneg zero_le_two

Premises used: abs_of_nonneg, zero_le_two
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
rw : a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
⊢ |a * b| = |a| * |b|

Tactic:
rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))]

Premises used: mul_nonneg, abs_eq, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
inl : ∀ (ha : a ≤ 0), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
inr : ∀ (ha : 0 ≤ a), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
rcases le_total a 0 with ha | ha

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
ha : a ≤ 0
inl : ∀ (hb : b ≤ 0), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
inl₁ : ∀ (hb : 0 ≤ b), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
rcases le_total b 0 with hb | hb

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
ha : 0 ≤ a
inr : ∀ (hb : b ≤ 0), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
inr₁ : ∀ (hb : 0 ≤ b), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
rcases le_total b 0 with hb | hb

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
ha : a ≤ 0
hb : b ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, neg_mul, mul_neg, neg_neg, *]

Premises used: true_or, neg_neg, abs_of_nonpos, abs_of_nonneg, neg_mul, or_true, mul_neg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, neg_mul, mul_neg, neg_neg, *]

Premises used: true_or, neg_neg, abs_of_nonpos, abs_of_nonneg, neg_mul, or_true, mul_neg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, neg_mul, mul_neg, neg_neg, *]

Premises used: true_or, neg_neg, abs_of_nonpos, abs_of_nonneg, neg_mul, or_true, mul_neg