awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
refine :
  ∀ (h : ¬MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
refine₁ :
  ∀
    (h :
      ¬∀ ⦃i : ι⦄,
          i ∈ (↑s : Set ι) →
            ∀ ⦃j : ι⦄, j ∈ (↑s : Set ι) → (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j → f i ≤ f j),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
refine₂ :
  ∀ (h : ∃ i ∈ (↑s : Set ι), ∃ j ∈ (↑s : Set ι), (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j ∧ f j < f i),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)
have refine₃ : ∀ (x : ι) (hx : x ∈ (↑s : Set ι)) (y : ι) (hy : y ∈ (↑s : Set ι))
  (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f x),
  ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
Tactic: classical
  refine ⟨not_imp_not.1 fun h ↦ ?_, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm <| by
    simpa using h.sum_smul_comp_perm_le_sum_smul ((set_support_symm_eq _).subset.trans hσ)⟩
  rw [MonovaryOn] at h
  push Not at h
  obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
  set τ : Perm ι := (Equiv.swap x y).trans σ
  have hτs : {x | τ x ≠ x} ⊆ s := by
    refine (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)
    obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
  refine ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' ?_).ne
  obtain rfl | hxy := eq_or_ne x y
  · cases lt_irrefl _ hfxy
  simp only [τ, ← s.sum_erase_add _ hx,
    ← (s.erase x).sum_erase_add _ (mem_erase.2 ⟨hxy.symm, hy⟩),
    add_assoc, Equiv.coe_trans, Function.comp_apply, swap_apply_right, swap_apply_left]
  refine add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ ?_).le
    (smul_add_smul_lt_smul_add_smul hfxy hgxy)
  simp_rw [mem_erase] at hz
  rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
refine :
  ∀ (h : ¬MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
refine₁ :
  ∀
    (h :
      ¬∀ ⦃i : ι⦄,
          i ∈ (↑s : Set ι) →
            ∀ ⦃j : ι⦄, j ∈ (↑s : Set ι) → (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j → f i ≤ f j),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
refine₂ :
  ∀ (h : ∃ i ∈ (↑s : Set ι), ∃ j ∈ (↑s : Set ι), (g ∘ (⇑σ : (a : ι) → ι)) i < (g ∘ (⇑σ : (a : ι) → ι)) j ∧ f j < f i),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
refine₃ refine₄ :
  ∀ (x : ι) (hx : x ∈ (↑s : Set ι)) (y : ι) (hy : y ∈ (↑s : Set ι))
    (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f x),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn f (g ∘ (⇑σ : (a : ι) → ι)) (↑s : Set ι)
have refine₅ : ∀ (x : ι) (hx : x ∈ (↑s : Set ι)) (y : ι) (hy : y ∈ (↑s : Set ι))
  (hgxy : (g ∘ (⇑σ : (a : ι) → ι)) x < (g ∘ (⇑σ : (a : ι) → ι)) y) (hfxy : f y < f x),
  let τ := Equiv.trans (Equiv.swap x y) σ;
  ∀ (hτs : {x : ι | (τ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)),
    ¬Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
Tactic: classical
  refine ⟨not_imp_not.1 fun h ↦ ?_, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm <| by
    simpa using h.sum_smul_comp_perm_le_sum_smul ((set_support_symm_eq _).subset.trans hσ)⟩
  rw [MonovaryOn] at h
  push Not at h
  obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
  set τ : Perm ι := (Equiv.swap x y).trans σ
  have hτs : {x | τ x ≠ x} ⊆ s := by
    refine (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)
    obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
  refine ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' ?_).ne
  obtain rfl | hxy := eq_or_ne x y
  · cases lt_irrefl _ hfxy
  simp only [τ, ← s.sum_erase_add _ hx,
    ← (s.erase x).sum_erase_add _ (mem_erase.2 ⟨hxy.symm, hy⟩),
    add_assoc, Equiv.coe_trans, Function.comp_apply, swap_apply_right, swap_apply_left]
  refine add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ ?_).le
    (smul_add_smul_lt_smul_add_smul hfxy hgxy)
  simp_rw [mem_erase] at hz
  rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
have hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
Tactic: have hσinv : { x | σ⁻¹ x ≠ x } ⊆ s := (set_support_symm_eq _).subset.trans hσ
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
have refine_1 : Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
  Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
Tactic: refine (Iff.trans ?_ <| hfg.sum_smul_comp_perm_eq_sum_smul_iff hσinv).trans
    ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
refine_1 :
  Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
    Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
have refine_2 : ∀ (h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)), MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
Tactic: refine (Iff.trans ?_ <| hfg.sum_smul_comp_perm_eq_sum_smul_iff hσinv).trans
    ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
refine_1 :
  Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
    Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
refine_2 :
  ∀ (h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)), MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
    MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
have refine_3 : ∀ (h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)), MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
Tactic: refine (Iff.trans ?_ <| hfg.sum_smul_comp_perm_eq_sum_smul_iff hσinv).trans
    ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g i) ↔
    Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i)) (∑ i ∈ s, f i • g i)
have refine_1 : Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i))
Tactic: apply eq_iff_eq_cancel_right.2
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := β) (∑ i ∈ s, f ((σ : (a : ι) → ι) i) • g i) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i))
have refine_1 : Eq.{u_3 + 1} (α := β) (∑ x ∈ s, f x • g ((Equiv.symm σ : (a : ι) → ι) x)) (∑ i ∈ s, f i • g ((σ⁻¹ : (a : ι) → ι) i))
Tactic: rw [σ.sum_comp' s (fun i j ↦ f i • g j) hσ]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
⊢ MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
have h₁ : g = comp (β := ι) (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (⇑σ : (a : ι) → ι)
Tactic: convert! h.comp_right σ
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
h₁ : g = comp (β := ι) (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (⇑σ : (a : ι) → ι)
⊢ MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
have h₂ : (↑s : Set ι) = (⇑σ : (a : ι) → ι) ⁻¹' (↑s : Set ι)
Tactic: convert! h.comp_right σ
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
⊢ g = comp (β := ι) (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (⇑σ : (a : ι) → ι)
have h₁ : g = g ∘ comp (β := ι) (⇑σ⁻¹ : (a : ι) → ι) (⇑σ : (a : ι) → ι)
Tactic: rw [comp_assoc, inv_def, symm_comp_self, comp_id]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
h₁ : g = g ∘ comp (β := ι) (⇑σ⁻¹ : (a : ι) → ι) (⇑σ : (a : ι) → ι)
⊢ g = comp (β := ι) (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (⇑σ : (a : ι) → ι)
have h₂ : g = g ∘ comp (β := ι) (⇑(Equiv.symm σ) : (a : ι) → ι) (⇑σ : (a : ι) → ι)
Tactic: rw [comp_assoc, inv_def, symm_comp_self, comp_id]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
h₁ : g = g ∘ comp (β := ι) (⇑σ⁻¹ : (a : ι) → ι) (⇑σ : (a : ι) → ι)
h₂ : g = g ∘ comp (β := ι) (⇑(Equiv.symm σ) : (a : ι) → ι) (⇑σ : (a : ι) → ι)
⊢ g = comp (β := ι) (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (⇑σ : (a : ι) → ι)
have h₃ : g = g ∘ id
Tactic: rw [comp_assoc, inv_def, symm_comp_self, comp_id]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
h₁ : g = g ∘ comp (β := ι) (⇑σ⁻¹ : (a : ι) → ι) (⇑σ : (a : ι) → ι)
h₂ : g = g ∘ comp (β := ι) (⇑(Equiv.symm σ) : (a : ι) → ι) (⇑σ : (a : ι) → ι)
h₃ : g = g ∘ id
⊢ g = comp (β := ι) (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (⇑σ : (a : ι) → ι)
have h₄ : g = g
Tactic: rw [comp_assoc, inv_def, symm_comp_self, comp_id]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
⊢ (↑s : Set ι) = (⇑σ : (a : ι) → ι) ⁻¹' (↑s : Set ι)
have h₁ : (⇑σ : (a : ι) → ι) '' (↑s : Set ι) = (↑s : Set ι)
Tactic: rw [σ.eq_preimage_iff_image_eq, Set.image_perm hσ]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
h₁ : (⇑σ : (a : ι) → ι) '' (↑s : Set ι) = (↑s : Set ι)
⊢ (↑s : Set ι) = (⇑σ : (a : ι) → ι) ⁻¹' (↑s : Set ι)
have h₂ : (↑s : Set ι) = (↑s : Set ι)
Tactic: rw [σ.eq_preimage_iff_image_eq, Set.image_perm hσ]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
⊢ MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
have h₁ : f = comp (β := ι) (f ∘ (⇑σ : (a : ι) → ι)) (⇑(Equiv.symm σ) : (a : ι) → ι)
Tactic: convert! h.comp_right σ.symm
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
h₁ : f = comp (β := ι) (f ∘ (⇑σ : (a : ι) → ι)) (⇑(Equiv.symm σ) : (a : ι) → ι)
⊢ MonovaryOn f (g ∘ (⇑σ⁻¹ : (a : ι) → ι)) (↑s : Set ι)
have h₂ : (↑s : Set ι) = (⇑(Equiv.symm σ) : (a : ι) → ι) ⁻¹' (↑s : Set ι)
Tactic: convert! h.comp_right σ.symm
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
⊢ f = comp (β := ι) (f ∘ (⇑σ : (a : ι) → ι)) (⇑(Equiv.symm σ) : (a : ι) → ι)
have h₁ : f = f ∘ comp (β := ι) (⇑σ : (a : ι) → ι) (⇑(Equiv.symm σ) : (a : ι) → ι)
Tactic: rw [comp_assoc, self_comp_symm, comp_id]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
h₁ : f = f ∘ comp (β := ι) (⇑σ : (a : ι) → ι) (⇑(Equiv.symm σ) : (a : ι) → ι)
⊢ f = comp (β := ι) (f ∘ (⇑σ : (a : ι) → ι)) (⇑(Equiv.symm σ) : (a : ι) → ι)
have h₂ : f = f ∘ id
Tactic: rw [comp_assoc, self_comp_symm, comp_id]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
h₁ : f = f ∘ comp (β := ι) (⇑σ : (a : ι) → ι) (⇑(Equiv.symm σ) : (a : ι) → ι)
h₂ : f = f ∘ id
⊢ f = comp (β := ι) (f ∘ (⇑σ : (a : ι) → ι)) (⇑(Equiv.symm σ) : (a : ι) → ι)
have h₃ : f = f
Tactic: rw [comp_assoc, self_comp_symm, comp_id]
-- 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 : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g (↑s : Set ι)
hσ : {x : ι | (σ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
hσinv : {x : ι | (σ⁻¹ : (a : ι) → ι) x ≠ x} ⊆ (↑s : Set ι)
h : MonovaryOn (f ∘ (⇑σ : (a : ι) → ι)) g (↑s : Set ι)
⊢ (↑s : Set ι) = (⇑(Equiv.symm σ) : (a : ι) → ι) ⁻¹' (↑s : Set ι)
have h₁ : (⇑(Equiv.symm σ) : (a : ι) → ι) '' (↑s : Set ι) = (↑s : Set ι)
Tactic: rw [σ.symm.eq_preimage_iff_image_eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a : α
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|
have inl : ∀ (n0 : 0 ≤ n), |a ^ n|ₘ = |a|ₘ ^ |n|
Tactic: obtain n0 | n0 := le_total 0 n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a : α
inl : ∀ (n0 : 0 ≤ n), |a ^ n|ₘ = |a|ₘ ^ |n|
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|
have inr : ∀ (n0 : n ≤ 0), |a ^ n|ₘ = |a|ₘ ^ |n|
Tactic: obtain n0 | n0 := le_total 0 n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a : α
n0 : 0 ≤ n
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|
have inl : ∀ (n : ℕ) (n0 : LE.le (α := ℤ) 0 (↑n : ℤ)), |HPow.hPow (β := ℤ) a (↑n : ℤ)|ₘ = HPow.hPow (β := ℤ) |a|ₘ |(↑n : ℤ)|
Tactic: obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le n0
Cleared hypotheses: n, n0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|
have inr : ∀ (m : ℕ) (h : -n = (↑m : ℤ)), |a ^ n|ₘ = |a|ₘ ^ |n|
Tactic: obtain ⟨m, h⟩ := Int.eq_ofNat_of_zero_le (neg_nonneg.2 n0)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = (↑m : ℤ)
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|
have inr : |a ^ m|ₘ = |a|ₘ ^ m
Tactic: rw [← mabs_inv, ← zpow_neg, ← abs_neg, h, zpow_natCast, Nat.abs_cast, zpow_natCast]