[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
[PROOFSTEP]
classical
revert hσ σ hfg
apply
  Finset.induction_on_max_value (fun i ↦ toLex (g i, f i)) (p := fun t ↦
    ∀ {σ : Perm ι}, MonovaryOn f g t → {x | σ x ≠ x} ⊆ t → (∑ i in t, f i • g (σ i)) ≤ ∑ i in t, f i • g i) s
· simp only [le_rfl, Finset.sum_empty, imp_true_iff]
intro a s has hamax hind σ hfg hσ
set τ : Perm ι := σ.trans (swap a (σ a)) with hτ
have hτs : {x | τ x ≠ x} ⊆ s := by
  intro x hx
  simp only [Ne.def, Set.mem_setOf_eq, Equiv.coe_trans, Equiv.swap_comp_apply] at hx
  split_ifs at hx  with h₁ h₂
  · obtain rfl | hax := eq_or_ne x a
    · contradiction
    · exact mem_of_mem_insert_of_ne (hσ fun h ↦ hax <| h.symm.trans h₁) hax
  · exact (hx <| σ.injective h₂.symm).elim
  · exact mem_of_mem_insert_of_ne (hσ hx) (ne_of_apply_ne _ h₂)
specialize hind (hfg.subset <| subset_insert _ _) hτs
simp_rw [sum_insert has]
refine' le_trans _ (add_le_add_left hind _)
obtain hσa | hσa := eq_or_ne a (σ a)
· rw [hτ, ← hσa, swap_self, trans_refl]
have h1s : σ⁻¹ a ∈ s := by
  rw [Ne.def, ← inv_eq_iff_eq] at hσa
  refine' mem_of_mem_insert_of_ne (hσ fun h ↦ hσa _) hσa
  rwa [apply_inv_self, eq_comm] at h
simp only [← s.sum_erase_add _ h1s, add_comm]
rw [← add_assoc, ← add_assoc]
simp only [hτ, swap_apply_left, Function.comp_apply, Equiv.coe_trans, apply_inv_self]
refine' add_le_add (smul_add_smul_le_smul_add_smul' _ _) (sum_congr rfl fun x hx ↦ _).le
· specialize hamax (σ⁻¹ a) h1s
  rw [Prod.Lex.le_iff] at hamax
  cases' hamax with hamax hamax
  · exact hfg (mem_insert_of_mem h1s) (mem_insert_self _ _) hamax
  · exact hamax.2
· specialize hamax (σ a) (mem_of_mem_insert_of_ne (hσ <| σ.injective.ne hσa.symm) hσa.symm)
  rw [Prod.Lex.le_iff] at hamax
  cases' hamax with hamax hamax
  · exact hamax.le
  · exact hamax.1.le
· rw [mem_erase, Ne.def, eq_inv_iff_eq] at hx
  rw [swap_apply_of_ne_of_ne hx.1 (σ.injective.ne _)]
  rintro rfl
  exact has hx.2
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
[PROOFSTEP]
revert hσ σ hfg
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
⊢ ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
[PROOFSTEP]
apply
  Finset.induction_on_max_value (fun i ↦ toLex (g i, f i)) (p := fun t ↦
    ∀ {σ : Perm ι}, MonovaryOn f g t → {x | σ x ≠ x} ⊆ t → (∑ i in t, f i • g (σ i)) ≤ ∑ i in t, f i • g i) s
[GOAL]
case h0
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
⊢ ∀ {σ : Perm ι}, MonovaryOn f g ↑∅ → {x | ↑σ x ≠ x} ⊆ ↑∅ → ∑ i in ∅, f i • g (↑σ i) ≤ ∑ i in ∅, f i • g i
[PROOFSTEP]
simp only [le_rfl, Finset.sum_empty, imp_true_iff]
[GOAL]
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
⊢ ∀ (a : ι) (s : Finset ι),
    ¬a ∈ s →
      (∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)) →
        (∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i) →
          ∀ {σ : Perm ι},
            MonovaryOn f g ↑(insert a s) →
              {x | ↑σ x ≠ x} ⊆ ↑(insert a s) → ∑ i in insert a s, f i • g (↑σ i) ≤ ∑ i in insert a s, f i • g i
[PROOFSTEP]
intro a s has hamax hind σ hfg hσ
[GOAL]
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
⊢ ∑ i in insert a s, f i • g (↑σ i) ≤ ∑ i in insert a s, f i • g i
[PROOFSTEP]
set τ : Perm ι := σ.trans (swap a (σ a)) with hτ
[GOAL]
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
⊢ ∑ i in insert a s, f i • g (↑σ i) ≤ ∑ i in insert a s, f i • g i
[PROOFSTEP]
have hτs : {x | τ x ≠ x} ⊆ s := by
  intro x hx
  simp only [Ne.def, Set.mem_setOf_eq, Equiv.coe_trans, Equiv.swap_comp_apply] at hx
  split_ifs at hx  with h₁ h₂
  · obtain rfl | hax := eq_or_ne x a
    · contradiction
    · exact mem_of_mem_insert_of_ne (hσ fun h ↦ hax <| h.symm.trans h₁) hax
  · exact (hx <| σ.injective h₂.symm).elim
  · exact mem_of_mem_insert_of_ne (hσ hx) (ne_of_apply_ne _ h₂)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
⊢ {x | ↑τ x ≠ x} ⊆ ↑s
[PROOFSTEP]
intro x hx
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
hx : x ∈ {x | ↑τ x ≠ x}
⊢ x ∈ ↑s
[PROOFSTEP]
simp only [Ne.def, Set.mem_setOf_eq, Equiv.coe_trans, Equiv.swap_comp_apply] at hx
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
hx : ¬(if ↑σ x = a then ↑σ a else if ↑σ x = ↑σ a then a else ↑σ x) = x
⊢ x ∈ ↑s
[PROOFSTEP]
split_ifs at hx  with h₁ h₂
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
h₁ : ↑σ x = a
hx : ¬↑σ a = x
⊢ x ∈ ↑s
[PROOFSTEP]
obtain rfl | hax := eq_or_ne x a
[GOAL]
case pos.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
s : Finset ι
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
x : ι
has : ¬x ∈ s
hamax : ∀ (x_1 : ι), x_1 ∈ s → ↑toLex (g x_1, f x_1) ≤ ↑toLex (g x, f x)
hfg : MonovaryOn f g ↑(insert x s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert x s)
τ : Perm ι := σ.trans (Equiv.swap x (↑σ x))
hτ : τ = σ.trans (Equiv.swap x (↑σ x))
h₁ : ↑σ x = x
hx : ¬↑σ x = x
⊢ x ∈ ↑s
[PROOFSTEP]
contradiction
[GOAL]
case pos.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
h₁ : ↑σ x = a
hx : ¬↑σ a = x
hax : x ≠ a
⊢ x ∈ ↑s
[PROOFSTEP]
exact mem_of_mem_insert_of_ne (hσ fun h ↦ hax <| h.symm.trans h₁) hax
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
h₁ : ¬↑σ x = a
h₂ : ↑σ x = ↑σ a
hx : ¬a = x
⊢ x ∈ ↑s
[PROOFSTEP]
exact (hx <| σ.injective h₂.symm).elim
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
x : ι
h₁ : ¬↑σ x = a
h₂ : ¬↑σ x = ↑σ a
hx : ¬↑σ x = x
⊢ x ∈ ↑s
[PROOFSTEP]
exact mem_of_mem_insert_of_ne (hσ hx) (ne_of_apply_ne _ h₂)
[GOAL]
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | ↑σ x ≠ x} ⊆ ↑s → ∑ i in s, f i • g (↑σ i) ≤ ∑ i in s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
⊢ ∑ i in insert a s, f i • g (↑σ i) ≤ ∑ i in insert a s, f i • g i
[PROOFSTEP]
specialize hind (hfg.subset <| subset_insert _ _) hτs
[GOAL]
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
⊢ ∑ i in insert a s, f i • g (↑σ i) ≤ ∑ i in insert a s, f i • g i
[PROOFSTEP]
simp_rw [sum_insert has]
[GOAL]
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g i
[PROOFSTEP]
refine' le_trans _ (add_le_add_left hind _)
[GOAL]
case step
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g (↑τ i)
[PROOFSTEP]
obtain hσa | hσa := eq_or_ne a (σ a)
[GOAL]
case step.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a = ↑σ a
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g (↑τ i)
[PROOFSTEP]
rw [hτ, ← hσa, swap_self, trans_refl]
[GOAL]
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g (↑τ i)
[PROOFSTEP]
have h1s : σ⁻¹ a ∈ s := by
  rw [Ne.def, ← inv_eq_iff_eq] at hσa
  refine' mem_of_mem_insert_of_ne (hσ fun h ↦ hσa _) hσa
  rwa [apply_inv_self, eq_comm] at h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
⊢ ↑σ⁻¹ a ∈ s
[PROOFSTEP]
rw [Ne.def, ← inv_eq_iff_eq] at hσa
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : ¬↑σ⁻¹ a = a
⊢ ↑σ⁻¹ a ∈ s
[PROOFSTEP]
refine' mem_of_mem_insert_of_ne (hσ fun h ↦ hσa _) hσa
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : ¬↑σ⁻¹ a = a
h : ↑σ (↑σ⁻¹ a) = ↑σ⁻¹ a
⊢ ↑σ⁻¹ a = a
[PROOFSTEP]
rwa [apply_inv_self, eq_comm] at h
[GOAL]
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f a • g (↑σ a) + ∑ x in s, f x • g (↑σ x) ≤ f a • g a + ∑ i in s, f i • g (↑τ i)
[PROOFSTEP]
simp only [← s.sum_erase_add _ h1s, add_comm]
[GOAL]
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f a • g (↑σ a) + (f (↑σ⁻¹ a) • g (↑σ (↑σ⁻¹ a)) + ∑ x in erase s (↑σ⁻¹ a), f x • g (↑σ x)) ≤
    f a • g a +
      (f (↑σ⁻¹ a) • g (↑(σ.trans (Equiv.swap a (↑σ a))) (↑σ⁻¹ a)) +
        ∑ x in erase s (↑σ⁻¹ a), f x • g (↑(σ.trans (Equiv.swap a (↑σ a))) x))
[PROOFSTEP]
rw [← add_assoc, ← add_assoc]
[GOAL]
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f a • g (↑σ a) + f (↑σ⁻¹ a) • g (↑σ (↑σ⁻¹ a)) + ∑ x in erase s (↑σ⁻¹ a), f x • g (↑σ x) ≤
    f a • g a + f (↑σ⁻¹ a) • g (↑(σ.trans (Equiv.swap a (↑σ a))) (↑σ⁻¹ a)) +
      ∑ x in erase s (↑σ⁻¹ a), f x • g (↑(σ.trans (Equiv.swap a (↑σ a))) x)
[PROOFSTEP]
simp only [hτ, swap_apply_left, Function.comp_apply, Equiv.coe_trans, apply_inv_self]
[GOAL]
case step.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f a • g (↑σ a) + f (↑σ⁻¹ a) • g a + ∑ x in erase s (↑σ⁻¹ a), f x • g (↑σ x) ≤
    f a • g a + f (↑σ⁻¹ a) • g (↑σ a) + ∑ x in erase s (↑σ⁻¹ a), f x • g (↑(Equiv.swap a (↑σ a)) (↑σ x))
[PROOFSTEP]
refine' add_le_add (smul_add_smul_le_smul_add_smul' _ _) (sum_congr rfl fun x hx ↦ _).le
[GOAL]
case step.inr.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ f (↑σ⁻¹ a) ≤ f a
[PROOFSTEP]
specialize hamax (σ⁻¹ a) h1s
[GOAL]
case step.inr.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : ↑toLex (g (↑σ⁻¹ a), f (↑σ⁻¹ a)) ≤ ↑toLex (g a, f a)
⊢ f (↑σ⁻¹ a) ≤ f a
[PROOFSTEP]
rw [Prod.Lex.le_iff] at hamax
[GOAL]
case step.inr.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax :
  (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).fst < (g a, f a).fst ∨
    (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).fst = (g a, f a).fst ∧ (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).snd ≤ (g a, f a).snd
⊢ f (↑σ⁻¹ a) ≤ f a
[PROOFSTEP]
cases' hamax with hamax hamax
[GOAL]
case step.inr.refine'_1.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).fst < (g a, f a).fst
⊢ f (↑σ⁻¹ a) ≤ f a
[PROOFSTEP]
exact hfg (mem_insert_of_mem h1s) (mem_insert_self _ _) hamax
[GOAL]
case step.inr.refine'_1.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).fst = (g a, f a).fst ∧ (g (↑σ⁻¹ a), f (↑σ⁻¹ a)).snd ≤ (g a, f a).snd
⊢ f (↑σ⁻¹ a) ≤ f a
[PROOFSTEP]
exact hamax.2
[GOAL]
case step.inr.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
⊢ g (↑σ a) ≤ g a
[PROOFSTEP]
specialize hamax (σ a) (mem_of_mem_insert_of_ne (hσ <| σ.injective.ne hσa.symm) hσa.symm)
[GOAL]
case step.inr.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : ↑toLex (g (↑σ a), f (↑σ a)) ≤ ↑toLex (g a, f a)
⊢ g (↑σ a) ≤ g a
[PROOFSTEP]
rw [Prod.Lex.le_iff] at hamax
[GOAL]
case step.inr.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax :
  (g (↑σ a), f (↑σ a)).fst < (g a, f a).fst ∨
    (g (↑σ a), f (↑σ a)).fst = (g a, f a).fst ∧ (g (↑σ a), f (↑σ a)).snd ≤ (g a, f a).snd
⊢ g (↑σ a) ≤ g a
[PROOFSTEP]
cases' hamax with hamax hamax
[GOAL]
case step.inr.refine'_2.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : (g (↑σ a), f (↑σ a)).fst < (g a, f a).fst
⊢ g (↑σ a) ≤ g a
[PROOFSTEP]
exact hamax.le
[GOAL]
case step.inr.refine'_2.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
hamax : (g (↑σ a), f (↑σ a)).fst = (g a, f a).fst ∧ (g (↑σ a), f (↑σ a)).snd ≤ (g a, f a).snd
⊢ g (↑σ a) ≤ g a
[PROOFSTEP]
exact hamax.1.le
[GOAL]
case step.inr.refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
x : ι
hx : x ∈ erase s (↑σ⁻¹ a)
⊢ f x • g (↑σ x) = f x • g (↑(Equiv.swap a (↑σ a)) (↑σ x))
[PROOFSTEP]
rw [mem_erase, Ne.def, eq_inv_iff_eq] at hx
[GOAL]
case step.inr.refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
x : ι
hx : ¬↑σ x = a ∧ x ∈ s
⊢ f x • g (↑σ x) = f x • g (↑(Equiv.swap a (↑σ a)) (↑σ x))
[PROOFSTEP]
rw [swap_apply_of_ne_of_ne hx.1 (σ.injective.ne _)]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : ¬a ∈ s
hamax : ∀ (x : ι), x ∈ s → ↑toLex (g x, f x) ≤ ↑toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := σ.trans (Equiv.swap a (↑σ a))
hτ : τ = σ.trans (Equiv.swap a (↑σ a))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : a ≠ ↑σ a
h1s : ↑σ⁻¹ a ∈ s
x : ι
hx : ¬↑σ x = a ∧ x ∈ s
⊢ x ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s✝ : Finset ι
f : ι → α
g : ι → β
s : Finset ι
σ : Perm ι
x : ι
has : ¬x ∈ s
hamax : ∀ (x_1 : ι), x_1 ∈ s → ↑toLex (g x_1, f x_1) ≤ ↑toLex (g x, f x)
hfg : MonovaryOn f g ↑(insert x s)
hσ : {x | ↑σ x ≠ x} ⊆ ↑(insert x s)
τ : Perm ι := σ.trans (Equiv.swap x (↑σ x))
hτ : τ = σ.trans (Equiv.swap x (↑σ x))
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hind : ∑ i in s, f i • g (↑τ i) ≤ ∑ i in s, f i • g i
hσa : x ≠ ↑σ x
h1s : ↑σ⁻¹ x ∈ s
hx : ¬↑σ x = x ∧ x ∈ s
⊢ False
[PROOFSTEP]
exact has hx.2
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i ↔ MonovaryOn f (g ∘ ↑σ) ↑s
[PROOFSTEP]
classical
refine' ⟨not_imp_not.1 fun h ↦ _, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm _⟩
· rw [MonovaryOn] at h
  push_neg 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]
· convert h.sum_smul_comp_perm_le_sum_smul ((set_support_inv_eq _).subset.trans hσ) using 1
  simp_rw [Function.comp_apply, apply_inv_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i ↔ MonovaryOn f (g ∘ ↑σ) ↑s
[PROOFSTEP]
refine' ⟨not_imp_not.1 fun h ↦ _, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
h : ¬MonovaryOn f (g ∘ ↑σ) ↑s
⊢ ¬∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i
[PROOFSTEP]
rw [MonovaryOn] at h
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
h : ¬∀ ⦃i : ι⦄, i ∈ ↑s → ∀ ⦃j : ι⦄, j ∈ ↑s → (g ∘ ↑σ) i < (g ∘ ↑σ) j → f i ≤ f j
⊢ ¬∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i
[PROOFSTEP]
push_neg at h
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
h : Exists fun ⦃i⦄ => i ∈ ↑s ∧ Exists fun ⦃j⦄ => j ∈ ↑s ∧ (g ∘ ↑σ) i < (g ∘ ↑σ) j ∧ f j < f i
⊢ ¬∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i
[PROOFSTEP]
obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
⊢ ¬∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i
[PROOFSTEP]
set τ : Perm ι := (Equiv.swap x y).trans σ
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
⊢ ¬∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i
[PROOFSTEP]
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
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
⊢ {x | ↑τ x ≠ x} ⊆ ↑s
[PROOFSTEP]
refine' (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ _)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
z : ι
hz : z ∈ {x_1 | ↑(Equiv.swap x y) x_1 ≠ x_1}
⊢ z ∈ ↑s
[PROOFSTEP]
obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz
[GOAL]
case intro.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
y : ι
hy : y ∈ ↑s
z : ι
hx : z ∈ ↑s
hgxy : (g ∘ ↑σ) z < (g ∘ ↑σ) y
hfxy : f y < f z
τ : Perm ι := (Equiv.swap z y).trans σ
hz : z ∈ {x | ↑(Equiv.swap z y) x ≠ x}
left✝ : z ≠ y
⊢ z ∈ ↑s
[PROOFSTEP]
assumption
[GOAL]
case intro.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
z : ι
hy : z ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) z
hfxy : f z < f x
τ : Perm ι := (Equiv.swap x z).trans σ
hz : z ∈ {x_1 | ↑(Equiv.swap x z) x_1 ≠ x_1}
left✝ : x ≠ z
⊢ z ∈ ↑s
[PROOFSTEP]
assumption
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
⊢ ¬∑ i in s, f i • g (↑σ i) = ∑ i in s, f i • g i
[PROOFSTEP]
refine' ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' _).ne
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g (↑σ i) < ∑ i in s, f i • g (↑τ i)
[PROOFSTEP]
obtain rfl | hxy := eq_or_ne x y
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
x : ι
hx hy : x ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) x
hfxy : f x < f x
τ : Perm ι := (Equiv.swap x x).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g (↑σ i) < ∑ i in s, f i • g (↑τ i)
[PROOFSTEP]
cases lt_irrefl _ hfxy
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hxy : x ≠ y
⊢ ∑ i in s, f i • g (↑σ i) < ∑ i in s, f i • g (↑τ i)
[PROOFSTEP]
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]
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hxy : x ≠ y
⊢ ∑ x in erase (erase s x) y, f x • g (↑σ x) + (f y • g (↑σ y) + f x • g (↑σ x)) <
    ∑ x_1 in erase (erase s x) y, f x_1 • g (↑σ (↑(Equiv.swap x y) x_1)) + (f y • g (↑σ x) + f x • g (↑σ y))
[PROOFSTEP]
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)
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hxy : x ≠ y
z : ι
hz : z ∈ erase (erase s x) y
⊢ f z • g (↑σ z) = f z • g (↑σ (↑(Equiv.swap x y) z))
[PROOFSTEP]
simp_rw [mem_erase] at hz
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ↑σ) x < (g ∘ ↑σ) y
hfxy : f y < f x
τ : Perm ι := (Equiv.swap x y).trans σ
hτs : {x | ↑τ x ≠ x} ⊆ ↑s
hxy : x ≠ y
z : ι
hz : z ≠ y ∧ z ≠ x ∧ z ∈ s
⊢ f z • g (↑σ z) = f z • g (↑σ (↑(Equiv.swap x y) z))
[PROOFSTEP]
rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ↑σ) ↑s
⊢ ∑ i in s, f i • g i ≤ ∑ i in s, f i • g (↑σ i)
[PROOFSTEP]
convert h.sum_smul_comp_perm_le_sum_smul ((set_support_inv_eq _).subset.trans hσ) using 1
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ↑σ) ↑s
⊢ ∑ i in s, f i • g i = ∑ i in s, f i • (g ∘ ↑σ) (↑σ⁻¹ i)
[PROOFSTEP]
simp_rw [Function.comp_apply, apply_inv_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g (↑σ i) < ∑ i in s, f i • g i ↔ ¬MonovaryOn f (g ∘ ↑σ) ↑s
[PROOFSTEP]
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σ]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f (↑σ i) • g i ≤ ∑ i in s, f i • g i
[PROOFSTEP]
convert hfg.sum_smul_comp_perm_le_sum_smul (show {x | σ⁻¹ x ≠ x} ⊆ s by simp only [set_support_inv_eq, hσ]) using 1
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
[PROOFSTEP]
simp only [set_support_inv_eq, hσ]
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f (↑σ i) • g i = ∑ i in s, f i • g (↑σ⁻¹ i)
[PROOFSTEP]
exact σ.sum_comp' s (fun i j ↦ f i • g j) hσ
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f (↑σ i) • g i = ∑ i in s, f i • g i ↔ MonovaryOn (f ∘ ↑σ) g ↑s
[PROOFSTEP]
have hσinv : {x | σ⁻¹ x ≠ x} ⊆ s := (set_support_inv_eq _).subset.trans hσ
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f (↑σ i) • g i = ∑ i in s, f i • g i ↔ MonovaryOn (f ∘ ↑σ) g ↑s
[PROOFSTEP]
refine' (Iff.trans _ <| hfg.sum_smul_comp_perm_eq_sum_smul_iff hσinv).trans ⟨fun h ↦ _, fun h ↦ _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f (↑σ i) • g i = ∑ i in s, f i • g i ↔ ∑ i in s, f i • g (↑σ⁻¹ i) = ∑ i in s, f i • g i
[PROOFSTEP]
apply eq_iff_eq_cancel_right.2
[GOAL]
case refine'_1.a
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f (↑σ i) • g i = ∑ i in s, f i • g (↑σ⁻¹ i)
[PROOFSTEP]
rw [σ.sum_comp' s (fun i j ↦ f i • g j) hσ]
[GOAL]
case refine'_1.a
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
⊢ ∑ x in s, f x • g (↑σ.symm x) = ∑ i in s, f i • g (↑σ⁻¹ i)
[PROOFSTEP]
congr
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ↑σ⁻¹) ↑s
⊢ MonovaryOn (f ∘ ↑σ) g ↑s
[PROOFSTEP]
convert h.comp_right σ
[GOAL]
case h.e'_7
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ↑σ⁻¹) ↑s
⊢ g = (g ∘ ↑σ⁻¹) ∘ ↑σ
[PROOFSTEP]
rw [comp.assoc, inv_def, symm_comp_self, comp.right_id]
[GOAL]
case h.e'_8
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ↑σ⁻¹) ↑s
⊢ ↑s = ↑σ ⁻¹' ↑s
[PROOFSTEP]
rw [σ.eq_preimage_iff_image_eq, Set.image_perm hσ]
[GOAL]
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ↑σ) g ↑s
⊢ MonovaryOn f (g ∘ ↑σ⁻¹) ↑s
[PROOFSTEP]
convert h.comp_right σ.symm
[GOAL]
case h.e'_6
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ↑σ) g ↑s
⊢ f = (f ∘ ↑σ) ∘ ↑σ.symm
[PROOFSTEP]
rw [comp.assoc, self_comp_symm, comp.right_id]
[GOAL]
case h.e'_8
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ↑σ) g ↑s
⊢ ↑s = ↑σ.symm ⁻¹' ↑s
[PROOFSTEP]
rw [σ.symm.eq_preimage_iff_image_eq]
[GOAL]
case h.e'_8
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
hσinv : {x | ↑σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ↑σ) g ↑s
⊢ ↑σ.symm '' ↑s = ↑s
[PROOFSTEP]
exact Set.image_perm hσinv
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f (↑σ i) • g i < ∑ i in s, f i • g i ↔ ¬MonovaryOn (f ∘ ↑σ) g ↑s
[PROOFSTEP]
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σ]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g i < ∑ i in s, f i • g (↑σ i) ↔ ¬AntivaryOn f (g ∘ ↑σ) ↑s
[PROOFSTEP]
simp [← hfg.sum_smul_eq_sum_smul_comp_perm_iff hσ, lt_iff_le_and_ne, eq_comm, hfg.sum_smul_le_sum_smul_comp_perm hσ]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g ↑s
hσ : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ i in s, f i • g i < ∑ i in s, f (↑σ i) • g i ↔ ¬AntivaryOn (f ∘ ↑σ) g ↑s
[PROOFSTEP]
simp [← hfg.sum_smul_eq_sum_comp_perm_smul_iff hσ, eq_comm, lt_iff_le_and_ne, hfg.sum_smul_le_sum_comp_perm_smul hσ]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i : ι, f i • g (↑σ i) = ∑ i : ι, f i • g i ↔ Monovary f (g ∘ ↑σ)
[PROOFSTEP]
simp [(hfg.monovaryOn _).sum_smul_comp_perm_eq_sum_smul_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i : ι, f i • g (↑σ i) < ∑ i : ι, f i • g i ↔ ¬Monovary f (g ∘ ↑σ)
[PROOFSTEP]
simp [(hfg.monovaryOn _).sum_smul_comp_perm_lt_sum_smul_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i : ι, f (↑σ i) • g i = ∑ i : ι, f i • g i ↔ Monovary (f ∘ ↑σ) g
[PROOFSTEP]
simp [(hfg.monovaryOn _).sum_comp_perm_smul_eq_sum_smul_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i : ι, f (↑σ i) • g i < ∑ i : ι, f i • g i ↔ ¬Monovary (f ∘ ↑σ) g
[PROOFSTEP]
simp [(hfg.monovaryOn _).sum_comp_perm_smul_lt_sum_smul_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i : ι, f i • g (↑σ i) = ∑ i : ι, f i • g i ↔ Antivary f (g ∘ ↑σ)
[PROOFSTEP]
simp [(hfg.antivaryOn _).sum_smul_eq_sum_smul_comp_perm_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i : ι, f i • g i < ∑ i : ι, f i • g (↑σ i) ↔ ¬Antivary f (g ∘ ↑σ)
[PROOFSTEP]
simp [(hfg.antivaryOn _).sum_smul_lt_sum_smul_comp_perm_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i : ι, f (↑σ i) • g i = ∑ i : ι, f i • g i ↔ Antivary (f ∘ ↑σ) g
[PROOFSTEP]
simp [(hfg.antivaryOn _).sum_smul_eq_sum_comp_perm_smul_iff fun _ _ ↦ mem_univ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i : ι, f i • g i < ∑ i : ι, f (↑σ i) • g i ↔ ¬Antivary (f ∘ ↑σ) g
[PROOFSTEP]
simp [(hfg.antivaryOn _).sum_smul_lt_sum_comp_perm_smul_iff fun _ _ ↦ mem_univ _]


[GOAL]
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
a✝ b✝ c d : α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : AddHom α β
hf : Monotone ↑f
a b : α
⊢ ↑f a - ↑f b ≤ ↑f (a - b)
[PROOFSTEP]
rw [tsub_le_iff_right, ← f.map_add]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
a✝ b✝ c d : α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : AddHom α β
hf : Monotone ↑f
a b : α
⊢ ↑f a ≤ ↑f (a - b + b)
[PROOFSTEP]
exact hf le_tsub_add
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁸ : Preorder α
inst✝⁷ : Add α
inst✝⁶ : Sub α
inst✝⁵ : OrderedSub α
a✝ b✝ c✝ d : α
R : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Preorder R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : CovariantClass R R (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : R
⊢ a * c - b * c ≤ (a - b) * c
[PROOFSTEP]
simpa only [mul_comm _ c] using le_mul_tsub
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Preorder M
inst✝⁶ : Add M
inst✝⁵ : Sub M
inst✝⁴ : OrderedSub M
inst✝³ : PartialOrder N
inst✝² : Add N
inst✝¹ : Sub N
inst✝ : OrderedSub N
e : M ≃o N
h_add : ∀ (a b : M), ↑e (a + b) = ↑e a + ↑e b
a b : M
⊢ ↑e (a - b) = ↑e a - ↑e b
[PROOFSTEP]
let e_add : M ≃+ N := { e with map_add' := h_add }
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Preorder M
inst✝⁶ : Add M
inst✝⁵ : Sub M
inst✝⁴ : OrderedSub M
inst✝³ : PartialOrder N
inst✝² : Add N
inst✝¹ : Sub N
inst✝ : OrderedSub N
e : M ≃o N
h_add : ∀ (a b : M), ↑e (a + b) = ↑e a + ↑e b
a b : M
e_add : M ≃+ N := { toEquiv := e.toEquiv, map_add' := h_add }
⊢ ↑e (a - b) = ↑e a - ↑e b
[PROOFSTEP]
refine' le_antisymm _ (e_add.toAddHom.le_map_tsub e.monotone a b)
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Preorder M
inst✝⁶ : Add M
inst✝⁵ : Sub M
inst✝⁴ : OrderedSub M
inst✝³ : PartialOrder N
inst✝² : Add N
inst✝¹ : Sub N
inst✝ : OrderedSub N
e : M ≃o N
h_add : ∀ (a b : M), ↑e (a + b) = ↑e a + ↑e b
a b : M
e_add : M ≃+ N := { toEquiv := e.toEquiv, map_add' := h_add }
⊢ ↑e (a - b) ≤ ↑e a - ↑e b
[PROOFSTEP]
suffices e (e.symm (e a) - e.symm (e b)) ≤ e (e.symm (e a - e b)) by simpa
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Preorder M
inst✝⁶ : Add M
inst✝⁵ : Sub M
inst✝⁴ : OrderedSub M
inst✝³ : PartialOrder N
inst✝² : Add N
inst✝¹ : Sub N
inst✝ : OrderedSub N
e : M ≃o N
h_add : ∀ (a b : M), ↑e (a + b) = ↑e a + ↑e b
a b : M
e_add : M ≃+ N := { toEquiv := e.toEquiv, map_add' := h_add }
this : ↑e (↑(symm e) (↑e a) - ↑(symm e) (↑e b)) ≤ ↑e (↑(symm e) (↑e a - ↑e b))
⊢ ↑e (a - b) ≤ ↑e a - ↑e b
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Preorder M
inst✝⁶ : Add M
inst✝⁵ : Sub M
inst✝⁴ : OrderedSub M
inst✝³ : PartialOrder N
inst✝² : Add N
inst✝¹ : Sub N
inst✝ : OrderedSub N
e : M ≃o N
h_add : ∀ (a b : M), ↑e (a + b) = ↑e a + ↑e b
a b : M
e_add : M ≃+ N := { toEquiv := e.toEquiv, map_add' := h_add }
⊢ ↑e (↑(symm e) (↑e a) - ↑(symm e) (↑e b)) ≤ ↑e (↑(symm e) (↑e a - ↑e b))
[PROOFSTEP]
exact e.monotone (e_add.symm.toAddHom.le_map_tsub e.symm.monotone _ _)


[GOAL]
α : Type u_1
inst✝¹ : OrderedAddCommMonoid α
inst✝ : Archimedean α
x y : { x // 0 ≤ x }
hy : 0 < y
n : ℕ
hr : ↑x ≤ n • (fun a => ↑a) y
⊢ ↑x ≤ ↑(n • y)
[PROOFSTEP]
simp [*, -nsmul_eq_mul, nsmul_coe]


[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝ b c d a : α
⊢ symm (mulRight a) = mulRight a⁻¹
[PROOFSTEP]
ext x
[GOAL]
case h.h
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝ b c d a x : α
⊢ ↑(symm (mulRight a)) x = ↑(mulRight a⁻¹) x
[PROOFSTEP]
rfl
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ symm (mulLeft a) = mulLeft a⁻¹
[PROOFSTEP]
ext x
[GOAL]
case h.h
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a x : α
⊢ ↑(symm (mulLeft a)) x = ↑(mulLeft a⁻¹) x
[PROOFSTEP]
rfl


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : ConditionallyCompleteLinearOrderedField α
⊢ ∀ (x : α), ∃ n, x < ↑n
[PROOFSTEP]
by_contra' h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : ConditionallyCompleteLinearOrderedField α
h : ∃ x, ∀ (n : ℕ), ↑n ≤ x
⊢ False
[PROOFSTEP]
obtain ⟨x, h⟩ := h
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : ConditionallyCompleteLinearOrderedField α
x : α
h : ∀ (n : ℕ), ↑n ≤ x
⊢ False
[PROOFSTEP]
have :=
  csSup_le _ _ (range_nonempty Nat.cast)
    (forall_range_iff.2 fun m => le_sub_iff_add_le.2 <| le_csSup _ _ ⟨x, forall_range_iff.2 h⟩ ⟨m + 1, Nat.cast_succ m⟩)
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : ConditionallyCompleteLinearOrderedField α
x : α
h : ∀ (n : ℕ), ↑n ≤ x
this : sSup (range Nat.cast) ≤ sSup (range fun i => ↑i) - 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a : α
⊢ cutMap α a = Iio a ∩ range Rat.cast
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a x✝ : α
⊢ x✝ ∈ cutMap α a ↔ x✝ ∈ Iio a ∩ range Rat.cast
[PROOFSTEP]
constructor
[GOAL]
case h.mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a x✝ : α
⊢ x✝ ∈ cutMap α a → x✝ ∈ Iio a ∩ range Rat.cast
[PROOFSTEP]
rintro ⟨q, h, rfl⟩
[GOAL]
case h.mp.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
a : α
q : ℚ
h : q ∈ {t | ↑t < a}
⊢ ↑q ∈ Iio a ∩ range Rat.cast
[PROOFSTEP]
exact ⟨h, q, rfl⟩
[GOAL]
case h.mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q : ℚ
a x✝ : α
⊢ x✝ ∈ Iio a ∩ range Rat.cast → x✝ ∈ cutMap α a
[PROOFSTEP]
rintro ⟨h, q, rfl⟩
[GOAL]
case h.mpr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : DivisionRing β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
a : α
q : ℚ
h : ↑q ∈ Iio a
⊢ ↑q ∈ cutMap α a
[PROOFSTEP]
exact ⟨q, h, rfl⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : LinearOrderedField α
inst✝ : LinearOrderedField β
a a₁ a₂ : α
b : β
q✝ q : ℚ
⊢ cutMap β ↑q = Rat.cast '' {r | ↑r < ↑q}
[PROOFSTEP]
simp_rw [cutMap, Rat.cast_lt]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b : β
q : ℚ
inst✝ : Archimedean α
a : α
⊢ BddAbove (cutMap β a)
[PROOFSTEP]
obtain ⟨q, hq⟩ := exists_rat_gt a
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
inst✝ : Archimedean α
a : α
q : ℚ
hq : a < ↑q
⊢ BddAbove (cutMap β a)
[PROOFSTEP]
exact ⟨q, ball_image_iff.2 fun r hr => by exact_mod_cast (hq.trans' hr).le⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b : β
q✝ : ℚ
inst✝ : Archimedean α
a : α
q : ℚ
hq : a < ↑q
r : ℚ
hr : r ∈ {t | ↑t < a}
⊢ ↑r ≤ ↑q
[PROOFSTEP]
exact_mod_cast (hq.trans' hr).le
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q : ℚ
inst✝ : Archimedean α
a b : α
⊢ cutMap β (a + b) = cutMap β a + cutMap β b
[PROOFSTEP]
refine (image_subset_iff.2 fun q hq => ?_).antisymm ?_
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : q ∈ {t | ↑t < a + b}
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
[PROOFSTEP]
rw [mem_setOf_eq, ← sub_lt_iff_lt_add] at hq
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
[PROOFSTEP]
obtain ⟨q₁, hq₁q, hq₁ab⟩ := exists_rat_btwn hq
[GOAL]
case refine_1.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
[PROOFSTEP]
refine ⟨q₁, q - q₁, by rwa [coe_mem_cutMap_iff], ?_, add_sub_cancel'_right _ _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑q₁ ∈ cutMap β a
[PROOFSTEP]
rwa [coe_mem_cutMap_iff]
[GOAL]
case refine_1.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑q - ↑q₁ ∈ cutMap β b
[PROOFSTEP]
norm_cast
[GOAL]
case refine_1.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑(q - q₁) ∈ cutMap β b
[PROOFSTEP]
rw [coe_mem_cutMap_iff]
[GOAL]
case refine_1.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q✝ : ℚ
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ ↑(q - q₁) < b
[PROOFSTEP]
exact_mod_cast sub_lt_comm.mp hq₁q
[GOAL]
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q : ℚ
inst✝ : Archimedean α
a b : α
⊢ cutMap β a + cutMap β b ⊆ Rat.cast '' {t | ↑t < a + b}
[PROOFSTEP]
rintro _ ⟨_, _, ⟨qa, ha, rfl⟩, ⟨qb, hb, rfl⟩, rfl⟩
[GOAL]
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q : ℚ
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ (fun x x_1 => x + x_1) ↑qa ↑qb ∈ Rat.cast '' {t | ↑t < a + b}
[PROOFSTEP]
refine' ⟨qa + qb, _, by norm_cast⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q : ℚ
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑(qa + qb) = (fun x x_1 => x + x_1) ↑qa ↑qb
[PROOFSTEP]
norm_cast
[GOAL]
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q : ℚ
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ qa + qb ∈ {t | ↑t < a + b}
[PROOFSTEP]
rw [mem_setOf_eq, cast_add]
[GOAL]
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
a✝ a₁ a₂ : α
b✝ : β
q : ℚ
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑qa + ↑qb < a + b
[PROOFSTEP]
exact add_lt_add ha hb
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
⊢ inducedMap α β ↑q = ↑q
[PROOFSTEP]
refine csSup_eq_of_forall_le_of_forall_lt_exists_gt (cutMap_nonempty β (q : α)) (fun x h => ?_) fun w h => ?_
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ cutMap β ↑q
⊢ x ≤ ↑q
[PROOFSTEP]
rw [cutMap_coe] at h
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ Rat.cast '' {r | ↑r < ↑q}
⊢ x ≤ ↑q
[PROOFSTEP]
obtain ⟨r, h, rfl⟩ := h
[GOAL]
case refine_1.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q r : ℚ
h : r ∈ {r | ↑r < ↑q}
⊢ ↑r ≤ ↑q
[PROOFSTEP]
exact le_of_lt h
[GOAL]
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
⊢ ∃ a, a ∈ cutMap β ↑q ∧ w < a
[PROOFSTEP]
obtain ⟨q', hwq, hq⟩ := exists_rat_btwn h
[GOAL]
case refine_2.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
q' : ℚ
hwq : w < ↑q'
hq : ↑q' < ↑q
⊢ ∃ a, a ∈ cutMap β ↑q ∧ w < a
[PROOFSTEP]
rw [cutMap_coe]
[GOAL]
case refine_2.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
q' : ℚ
hwq : w < ↑q'
hq : ↑q' < ↑q
⊢ ∃ a, a ∈ Rat.cast '' {r | ↑r < ↑q} ∧ w < a
[PROOFSTEP]
exact ⟨q', ⟨_, hq, rfl⟩, hwq⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
⊢ inducedMap α β 0 = 0
[PROOFSTEP]
exact_mod_cast inducedMap_rat α β 0
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
⊢ inducedMap α β 1 = 1
[PROOFSTEP]
exact_mod_cast inducedMap_rat α β 1
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
⊢ ↑q < inducedMap α β a ↔ ↑q < a
[PROOFSTEP]
refine ⟨fun h => ?_, fun hq => ?_⟩
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
h : ↑q < inducedMap α β a
⊢ ↑q < a
[PROOFSTEP]
rw [← inducedMap_rat α] at h
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
h : inducedMap α β ↑q < inducedMap α β a
⊢ ↑q < a
[PROOFSTEP]
exact (inducedMap_mono α β).reflect_lt h
[GOAL]
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
hq : ↑q < a
⊢ ↑q < inducedMap α β a
[PROOFSTEP]
obtain ⟨q', hq, hqa⟩ := exists_rat_btwn hq
[GOAL]
case refine_2.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
hq✝ : ↑q < a
q' : ℚ
hq : ↑q < ↑q'
hqa : ↑q' < a
⊢ ↑q < inducedMap α β a
[PROOFSTEP]
apply lt_csSup_of_lt (cutMap_bddAbove β a) (coe_mem_cutMap_iff.mpr hqa)
[GOAL]
case refine_2.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
hq✝ : ↑q < a
q' : ℚ
hq : ↑q < ↑q'
hqa : ↑q' < a
⊢ ↑q < ↑q'
[PROOFSTEP]
exact_mod_cast hq
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
x✝ : ∃ q, b < ↑q ∧ ↑q < a
q : ℚ
hbq : b < ↑q
hqa : ↑q < a
⊢ ↑q < inducedMap α β a
[PROOFSTEP]
rwa [coe_lt_inducedMap_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a✝ : α
b : β
q✝ : ℚ
a : α
q : ℚ
⊢ ↑q < inducedMap β γ (inducedMap α β a) ↔ ↑q < inducedMap α γ a
[PROOFSTEP]
rw [coe_lt_inducedMap_iff, coe_lt_inducedMap_iff, Iff.comm, coe_lt_inducedMap_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
b : β
⊢ inducedMap γ β (inducedMap β γ b) = b
[PROOFSTEP]
rw [inducedMap_inducedMap, inducedMap_self]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
x y : α
⊢ inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y
[PROOFSTEP]
rw [inducedMap, cutMap_add]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
x y : α
⊢ sSup (cutMap β x + cutMap β y) = inducedMap α β x + inducedMap α β y
[PROOFSTEP]
exact csSup_add (cutMap_nonempty β x) (cutMap_bddAbove β x) (cutMap_nonempty β y) (cutMap_bddAbove β y)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
ha : 0 < a
b : β
hb : b ∈ cutMap β (a * a)
⊢ b ≤ inducedMap α β a * inducedMap α β a
[PROOFSTEP]
obtain ⟨q, hb, rfl⟩ := hb
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
⊢ ↑q ≤ inducedMap α β a * inducedMap α β a
[PROOFSTEP]
obtain ⟨q', hq', hqq', hqa⟩ := exists_rat_pow_btwn two_ne_zero hb (mul_self_pos.2 ha.ne')
[GOAL]
case intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' ^ 2 < a * a
⊢ ↑q ≤ inducedMap α β a * inducedMap α β a
[PROOFSTEP]
trans (q' : β) ^ 2
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' ^ 2 < a * a
⊢ ↑q ≤ ↑q' ^ 2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' ^ 2 < a * a
⊢ ↑q' ^ 2 ≤ inducedMap α β a * inducedMap α β a
[PROOFSTEP]
exact_mod_cast hqq'.le
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' ^ 2 < a * a
⊢ ↑q' ^ 2 ≤ inducedMap α β a * inducedMap α β a
[PROOFSTEP]
rw [pow_two] at hqa ⊢
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' * ↑q' < a * a
⊢ ↑q' * ↑q' ≤ inducedMap α β a * inducedMap α β a
[PROOFSTEP]
exact
  mul_self_le_mul_self (by exact_mod_cast hq'.le)
    (le_csSup (cutMap_bddAbove β a) <| coe_mem_cutMap_iff.2 <| lt_of_mul_self_lt_mul_self ha.le hqa)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q✝ : ℚ
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' * ↑q' < a * a
⊢ 0 ≤ ↑q'
[PROOFSTEP]
exact_mod_cast hq'.le
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
⊢ ∃ c, c ∈ cutMap β (a * a) ∧ b < c
[PROOFSTEP]
obtain hb | hb := lt_or_le b 0
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ ∃ c, c ∈ cutMap β (a * a) ∧ b < c
[PROOFSTEP]
refine ⟨0, ?_, hb⟩
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ 0 ∈ cutMap β (a * a)
[PROOFSTEP]
rw [← Rat.cast_zero, coe_mem_cutMap_iff, Rat.cast_zero]
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ 0 < a * a
[PROOFSTEP]
exact mul_self_pos.2 ha.ne'
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
⊢ ∃ c, c ∈ cutMap β (a * a) ∧ b < c
[PROOFSTEP]
obtain ⟨q, hq, hbq, hqa⟩ := exists_rat_pow_btwn two_ne_zero hba (hb.trans_lt hba)
[GOAL]
case inr.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑q ^ 2
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c, c ∈ cutMap β (a * a) ∧ b < c
[PROOFSTEP]
rw [← cast_pow] at hbq
[GOAL]
case inr.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c, c ∈ cutMap β (a * a) ∧ b < c
[PROOFSTEP]
refine ⟨(q ^ 2 : ℚ), coe_mem_cutMap_iff.2 ?_, hbq⟩
[GOAL]
case inr.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ↑(q ^ 2) < a * a
[PROOFSTEP]
rw [pow_two] at hqa ⊢
[GOAL]
case inr.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
⊢ ↑(q * q) < a * a
[PROOFSTEP]
push_cast
[GOAL]
case inr.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
⊢ ↑q * ↑q < a * a
[PROOFSTEP]
obtain ⟨q', hq', hqa'⟩ := lt_inducedMap_iff.1 (lt_of_mul_self_lt_mul_self (inducedMap_nonneg ha.le) hqa)
[GOAL]
case inr.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
q' : ℚ
hq' : ↑q < ↑q'
hqa' : ↑q' < a
⊢ ↑q * ↑q < a * a
[PROOFSTEP]
exact mul_self_lt_mul_self (by exact_mod_cast hq.le) (hqa'.trans' <| by assumption_mod_cast)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
q' : ℚ
hq' : ↑q < ↑q'
hqa' : ↑q' < a
⊢ 0 ≤ ↑q
[PROOFSTEP]
exact_mod_cast hq.le
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b✝ : β
q✝ : ℚ
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
q' : ℚ
hq' : ↑q < ↑q'
hqa' : ↑q' < a
⊢ ↑q < ↑q'
[PROOFSTEP]
assumption_mod_cast
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
⊢ ∀ (x : α), ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
suffices : ∀ x, 0 < x → inducedAddHom α β (x * x) = inducedAddHom α β x * inducedAddHom α β x
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
⊢ ∀ (x : α), ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
intro x
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
x : α
⊢ ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
obtain h | rfl | h := lt_trichotomy x 0
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
x : α
h : x < 0
⊢ ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
convert this (-x) (neg_pos.2 h) using 1
[GOAL]
case h.e'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
x : α
h : x < 0
⊢ ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) (-x * -x)
[PROOFSTEP]
rw [neg_mul, mul_neg, neg_neg]
[GOAL]
case h.e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
x : α
h : x < 0
⊢ ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x = ↑(inducedAddHom α β) (-x) * ↑(inducedAddHom α β) (-x)
[PROOFSTEP]
simp_rw [AddMonoidHom.map_neg, neg_mul, mul_neg, neg_neg]
[GOAL]
case inr.inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
⊢ ↑(inducedAddHom α β) (0 * 0) = ↑(inducedAddHom α β) 0 * ↑(inducedAddHom α β) 0
[PROOFSTEP]
simp only [mul_zero, AddMonoidHom.map_zero]
[GOAL]
case inr.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
x : α
h : 0 < x
⊢ ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
exact this x h
[GOAL]
case this
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
⊢ ∀ (x : α), 0 < x → ↑(inducedAddHom α β) (x * x) = ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
refine fun x hx => csSup_eq_of_forall_le_of_forall_lt_exists_gt (cutMap_nonempty β _) ?_ ?_
[GOAL]
case this.refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
x : α
hx : 0 < x
⊢ ∀ (a : (fun x => β) (x * x)), a ∈ cutMap β (x * x) → a ≤ ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x
[PROOFSTEP]
exact le_inducedMap_mul_self_of_mem_cutMap hx
[GOAL]
case this.refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
x : α
hx : 0 < x
⊢ ∀ (w : (fun x => β) (x * x)), w < ↑(inducedAddHom α β) x * ↑(inducedAddHom α β) x → ∃ a, a ∈ cutMap β (x * x) ∧ w < a
[PROOFSTEP]
exact exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self hx
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
⊢ ∀ {a b : β},
    Equiv.toFun
          {
              toEquiv :=
                { toFun := src✝.toFun, invFun := inducedMap γ β,
                  left_inv := (_ : ∀ (b : β), inducedMap γ β (inducedMap β γ b) = b),
                  right_inv := (_ : ∀ (b : γ), inducedMap β γ (inducedMap γ β b) = b) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun (↑↑src✝.toRingHom) (x * y) =
                      OneHom.toFun (↑↑src✝.toRingHom) x * OneHom.toFun (↑↑src✝.toRingHom) y),
              map_add' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun (↑↑src✝.toRingHom) (x + y) =
                      OneHom.toFun (↑↑src✝.toRingHom) x + OneHom.toFun (↑↑src✝.toRingHom) y) }.toEquiv
          a ≤
        Equiv.toFun
          {
              toEquiv :=
                { toFun := src✝.toFun, invFun := inducedMap γ β,
                  left_inv := (_ : ∀ (b : β), inducedMap γ β (inducedMap β γ b) = b),
                  right_inv := (_ : ∀ (b : γ), inducedMap β γ (inducedMap γ β b) = b) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun (↑↑src✝.toRingHom) (x * y) =
                      OneHom.toFun (↑↑src✝.toRingHom) x * OneHom.toFun (↑↑src✝.toRingHom) y),
              map_add' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun (↑↑src✝.toRingHom) (x + y) =
                      OneHom.toFun (↑↑src✝.toRingHom) x + OneHom.toFun (↑↑src✝.toRingHom) y) }.toEquiv
          b ↔
      a ≤ b
[PROOFSTEP]
dsimp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
⊢ ∀ {a b : β}, ↑(inducedOrderRingHom β γ).toRingHom a ≤ ↑(inducedOrderRingHom β γ).toRingHom b ↔ a ≤ b
[PROOFSTEP]
refine ⟨fun h => ?_, fun h => inducedMap_mono _ _ h⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ ≤ b✝
[PROOFSTEP]
convert inducedMap_mono γ β h
[GOAL]
case h.e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ = inducedMap γ β (↑(inducedOrderRingHom β γ).toRingHom a✝)
[PROOFSTEP]
rw [inducedOrderRingHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero, inducedAddHom]
[GOAL]
case h.e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ =
    inducedMap γ β
      (↑{ toZeroHom := { toFun := inducedMap β γ, map_zero' := (_ : inducedMap β γ 0 = 0) },
            map_add' := (_ : ∀ (x y : β), inducedMap β γ (x + y) = inducedMap β γ x + inducedMap β γ y) }
        a✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ = inducedMap γ β (inducedMap β γ a✝)
[PROOFSTEP]
rw [inducedMap_inv_self β γ _]
[GOAL]
case h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ b✝ = inducedMap γ β (↑(inducedOrderRingHom β γ).toRingHom b✝)
[PROOFSTEP]
rw [inducedOrderRingHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero, inducedAddHom]
[GOAL]
case h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ b✝ =
    inducedMap γ β
      (↑{ toZeroHom := { toFun := inducedMap β γ, map_zero' := (_ : inducedMap β γ 0 = 0) },
            map_add' := (_ : ∀ (x y : β), inducedMap β γ (x + y) = inducedMap β γ x + inducedMap β γ y) }
        b✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedField α
inst✝² : ConditionallyCompleteLinearOrderedField β
inst✝¹ : ConditionallyCompleteLinearOrderedField γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
src✝ : β →+*o γ := inducedOrderRingHom β γ
a✝ b✝ : β
h : ↑(inducedOrderRingHom β γ).toRingHom a✝ ≤ ↑(inducedOrderRingHom β γ).toRingHom b✝
⊢ b✝ = inducedMap γ β (inducedMap β γ b✝)
[PROOFSTEP]
rw [inducedMap_inv_self β γ _]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
R : Type u_5
S : Type u_6
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
r : R
h : 0 ≤ r
⊢ 0 ≤ ↑f r
[PROOFSTEP]
obtain ⟨s, rfl⟩ := hR r h
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
R : Type u_5
S : Type u_6
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
s : R
h : 0 ≤ s ^ 2
⊢ 0 ≤ ↑f (s ^ 2)
[PROOFSTEP]
rw [map_pow]
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
R : Type u_5
S : Type u_6
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
s : R
h : 0 ≤ s ^ 2
⊢ 0 ≤ ↑f s ^ 2
[PROOFSTEP]
apply sq_nonneg