[GOAL]
α : Type u_1
a b c d x y z : α
inst✝⁶ : LinearOrderedCommMonoidWithZero α
β : Type u_2
inst✝⁵ : Zero β
inst✝⁴ : One β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : Sup β
inst✝ : Inf β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : β), f (x * y) = f x * f y
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
hsup : ∀ (x y : β), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : β), f (x ⊓ y) = min (f x) (f y)
src✝² : LinearOrder β := LinearOrder.lift f hf hsup hinf
src✝¹ : OrderedCommMonoid β := orderedCommMonoid f hf one mul npow
src✝ : CommMonoidWithZero β := Injective.commMonoidWithZero f hf zero one mul npow
⊢ f 0 ≤ f 1
[PROOFSTEP]
simp only [zero, one, LinearOrderedCommMonoidWithZero.zero_le_one]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommMonoidWithZero α
⊢ 0 ≤ a
[PROOFSTEP]
simpa only [mul_zero, mul_one] using mul_le_mul_left' zero_le_one a
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : c ≠ 0
hab : a * c ≤ b * c
⊢ a ≤ b
[PROOFSTEP]
simpa only [mul_inv_cancel_right₀ h] using mul_le_mul_right' hab c⁻¹
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : c ≠ 0
hab : a * c ≤ b
⊢ a * c ≤ b * c⁻¹ * c
[PROOFSTEP]
simpa [h] using hab
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
⊢ a * c⁻¹ ≤ b
[PROOFSTEP]
by_cases h : c = 0
[GOAL]
case pos
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
h : c = 0
⊢ a * c⁻¹ ≤ b
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
h : ¬c = 0
⊢ a * c⁻¹ ≤ b
[PROOFSTEP]
exact le_of_le_mul_right h (by simpa [h] using hab)
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
h : ¬c = 0
⊢ a * c⁻¹ * c ≤ b * c
[PROOFSTEP]
simpa [h] using hab
[GOAL]
α : Type u_1
a✝ b✝ c✝ d✝ x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
hb : b ≠ 0
hd : d ≠ 0
⊢ a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
[PROOFSTEP]
rw [mul_inv_le_iff₀ hb, mul_right_comm, le_mul_inv_iff₀ hd]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : a = 0
⊢ a * c < b * d
[PROOFSTEP]
rw [ha, zero_mul, zero_lt_iff]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : a = 0
⊢ b * d ≠ 0
[PROOFSTEP]
exact mul_ne_zero hb hd
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : ¬a = 0
hc : c = 0
⊢ a * c < b * d
[PROOFSTEP]
rw [hc, mul_zero, zero_lt_iff]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : ¬a = 0
hc : c = 0
⊢ b * d ≠ 0
[PROOFSTEP]
exact mul_ne_zero hb hd
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : x < y * z
⊢ x * z⁻¹ < y
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : y ≤ x * z⁻¹
⊢ y * z ≤ x
[PROOFSTEP]
simpa only [inv_inv] using mul_inv_le_of_le_mul h
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : x < y * z
⊢ y⁻¹ * x < z
[PROOFSTEP]
rw [mul_comm] at *
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : x < z * y
⊢ x * y⁻¹ < z
[PROOFSTEP]
exact mul_inv_lt_of_lt_mul₀ h
[GOAL]
α : Type u_1
a b c✝ d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
c : α
h : a < b
hc : c ≠ 0
⊢ a * c < b * c
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
a b c✝ d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
c : α
hc : c ≠ 0
h : b * c ≤ a * c
⊢ b ≤ a
[PROOFSTEP]
exact le_of_le_mul_right hc h
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
⊢ b < d
[PROOFSTEP]
have ha : a ≠ 0 := ne_of_gt (lt_of_lt_of_le hc hh)
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
ha : a ≠ 0
⊢ b < d
[PROOFSTEP]
simp_rw [← inv_le_inv₀ ha (ne_of_gt hc)] at hh
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : a * b < c * d
hc : 0 < c
ha : a ≠ 0
hh : a⁻¹ ≤ c⁻¹
⊢ b < d
[PROOFSTEP]
have := mul_lt_mul_of_lt_of_le₀ hh (inv_ne_zero (ne_of_gt hc)) h
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : a * b < c * d
hc : 0 < c
ha : a ≠ 0
hh : a⁻¹ ≤ c⁻¹
this : a⁻¹ * (a * b) < c⁻¹ * (c * d)
⊢ b < d
[PROOFSTEP]
simpa [inv_mul_cancel_left₀ ha, inv_mul_cancel_left₀ (ne_of_gt hc)] using this
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
ha : a ≠ 0
⊢ a * b ≤ a * c ↔ b ≤ c
[PROOFSTEP]
simp only [mul_comm a]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
ha : a ≠ 0
⊢ b * a ≤ c * a ↔ b ≤ c
[PROOFSTEP]
exact mul_le_mul_right₀ ha
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hc : c ≠ 0
⊢ a / c ≤ b / c ↔ a ≤ b
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, mul_le_mul_right₀ (inv_ne_zero hc)]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a / b ≤ a / c ↔ c ≤ b
[PROOFSTEP]
simp only [div_eq_mul_inv, mul_le_mul_left₀ ha, inv_le_inv₀ hb hc]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hc : c ≠ 0
⊢ a ≤ b / c ↔ a * c ≤ b
[PROOFSTEP]
rw [div_eq_mul_inv, le_mul_inv_iff₀ hc]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hc : c ≠ 0
⊢ a / c ≤ b ↔ a ≤ b * c
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_le_iff₀ hc]
[GOAL]
α : Type u_1
a✝ b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
⊢ symm (mulLeft₀' ha) = mulLeft₀' (_ : a⁻¹ ≠ 0)
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
a✝ b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
x✝ : α
⊢ ↑(symm (mulLeft₀' ha)) x✝ = ↑(mulLeft₀' (_ : a⁻¹ ≠ 0)) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
a✝ b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
⊢ symm (mulRight₀' ha) = mulRight₀' (_ : a⁻¹ ≠ 0)
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
a✝ b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
x✝ : α
⊢ ↑(symm (mulRight₀' ha)) x✝ = ↑(mulRight₀' (_ : a⁻¹ ≠ 0)) x✝
[PROOFSTEP]
rfl


[GOAL]
α : Type u_1
inst✝¹ : OrderedAddCommGroup α
inst✝ : Archimedean α
x y : αᵒᵈ
hy : 0 < y
n : ℕ
hn : -↑ofDual x ≤ n • -y
⊢ x ≤ n • y
[PROOFSTEP]
rwa [neg_nsmul, neg_le_neg_iff] at hn
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
let s : Set ℤ := {n : ℤ | n • a ≤ g}
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
obtain ⟨k, hk : -g ≤ k • a⟩ := Archimedean.arch (-g) ha
[GOAL]
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k : ℕ
hk : -g ≤ k • a
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
have h_ne : s.Nonempty := ⟨-k, by simpa using neg_le_neg hk⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k : ℕ
hk : -g ≤ k • a
⊢ -↑k ∈ s
[PROOFSTEP]
simpa using neg_le_neg hk
[GOAL]
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k : ℕ
hk : -g ≤ k • a
h_ne : Set.Nonempty s
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
obtain ⟨k, hk⟩ := Archimedean.arch g ha
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
have h_bdd : ∀ n ∈ s, n ≤ (k : ℤ) := by
  intro n hn
  apply (zsmul_le_zsmul_iff ha).mp
  rw [← coe_nat_zsmul] at hk
  exact le_trans hn hk
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
⊢ ∀ (n : ℤ), n ∈ s → n ≤ ↑k
[PROOFSTEP]
intro n hn
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
n : ℤ
hn : n ∈ s
⊢ n ≤ ↑k
[PROOFSTEP]
apply (zsmul_le_zsmul_iff ha).mp
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
n : ℤ
hn : n ∈ s
⊢ n • a ≤ ↑k • a
[PROOFSTEP]
rw [← coe_nat_zsmul] at hk
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ ↑k • a
n : ℤ
hn : n ∈ s
⊢ n • a ≤ ↑k • a
[PROOFSTEP]
exact le_trans hn hk
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
obtain ⟨m, hm, hm'⟩ := Int.exists_greatest_of_bdd ⟨k, h_bdd⟩ h_ne
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
have hm'' : g < (m + 1) • a := by
  contrapose! hm'
  exact ⟨m + 1, hm', lt_add_one _⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
⊢ g < (m + 1) • a
[PROOFSTEP]
contrapose! hm'
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : (m + 1) • a ≤ g
⊢ ∃ z, z ∈ {n | n • a ≤ g} ∧ m < z
[PROOFSTEP]
exact ⟨m + 1, hm', lt_add_one _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
hm'' : g < (m + 1) • a
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
refine' ⟨m, ⟨hm, hm''⟩, fun n hn => (hm' n hn.1).antisymm <| Int.le_of_lt_add_one _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
hm'' : g < (m + 1) • a
n : ℤ
hn : (fun k => k • a ≤ g ∧ g < (k + 1) • a) n
⊢ m < n + 1
[PROOFSTEP]
rw [← zsmul_lt_zsmul_iff ha]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
hm'' : g < (m + 1) • a
n : ℤ
hn : (fun k => k • a ≤ g ∧ g < (k + 1) • a) n
⊢ m • a < (n + 1) • a
[PROOFSTEP]
exact lt_of_le_of_lt hm hn.2
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
⊢ ∃! k, 0 ≤ g - k • a ∧ g - k • a < a
[PROOFSTEP]
simpa only [sub_nonneg, add_zsmul, one_zsmul, sub_lt_iff_lt_add'] using existsUnique_zsmul_near_of_pos ha g
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
b c : α
⊢ ∃! m, b - m • a ∈ Ico c (c + a)
[PROOFSTEP]
simpa only [mem_Ico, le_sub_iff_add_le, zero_add, add_comm c, sub_lt_iff_lt_add', add_assoc] using
  existsUnique_zsmul_near_of_pos' ha (b - c)
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
b c : α
⊢ ∃! x, b + ↑(Equiv.neg ℤ) x • a ∈ Ico c (c + a)
[PROOFSTEP]
simpa only [Equiv.neg_apply, mem_Ico, neg_zsmul, ← sub_eq_add_neg, le_sub_iff_add_le, zero_add, add_comm c,
  sub_lt_iff_lt_add', add_assoc] using existsUnique_zsmul_near_of_pos' ha (b - c)
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
b c : α
⊢ ∃! x, b + ↑(Equiv.addRight 1) x • a ∈ Ioc c (c + a)
[PROOFSTEP]
simpa only [add_zsmul, sub_lt_iff_lt_add', le_sub_iff_add_le', ← add_assoc, and_comm, mem_Ioc, Equiv.coe_addRight,
  one_zsmul, add_le_add_iff_right] using existsUnique_zsmul_near_of_pos ha (c - b)
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
b c : α
⊢ ∃! x, b - ↑(Equiv.neg ℤ) x • a ∈ Ioc c (c + a)
[PROOFSTEP]
simpa only [Equiv.neg_apply, neg_zsmul, sub_neg_eq_add] using existsUnique_add_zsmul_mem_Ioc ha b c
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
inst✝ : Archimedean α
x : α
n : ℕ
hn : x < n • 1
⊢ x < ↑n
[PROOFSTEP]
rwa [← nsmul_one]
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Archimedean α
x : α
⊢ ∃ n, x ≤ ↑n
[PROOFSTEP]
nontriviality α
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Archimedean α
x : α
✝ : Nontrivial α
⊢ ∃ n, x ≤ ↑n
[PROOFSTEP]
exact (Archimedean.arch x one_pos).imp fun n h => by rwa [← nsmul_one]
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Archimedean α
x : α
✝ : Nontrivial α
n : ℕ
h : x ≤ n • 1
⊢ x ≤ ↑n
[PROOFSTEP]
rwa [← nsmul_one]
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
inst✝ : Archimedean α
x y : α
hy : 0 < y
this : 0 ≤ 1 + y
n : ℕ
h : x ≤ n • y
⊢ (1 + y) ^ n = (y + 1) ^ n
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
n : ℕ
h : x < ↑n
⊢ x < ↑↑n
[PROOFSTEP]
rwa [Int.cast_ofNat]
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
n : ℤ
h : -x < ↑n
⊢ ↑(-n) < x
[PROOFSTEP]
rw [Int.cast_neg]
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
n : ℤ
h : -x < ↑n
⊢ -↑n < x
[PROOFSTEP]
exact neg_lt.1 h
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
[PROOFSTEP]
haveI := Classical.propDecidable
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this : (a : Prop) → Decidable a
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
[PROOFSTEP]
have : ∃ ub : ℤ, (ub : α) ≤ x ∧ ∀ z : ℤ, (z : α) ≤ x → z ≤ ub :=
  Int.exists_greatest_of_bdd
    (let ⟨n, hn⟩ := exists_int_gt x
    ⟨n, fun z h' => Int.cast_le.1 <| le_trans h' <| le_of_lt hn⟩)
    (let ⟨n, hn⟩ := exists_int_lt x
    ⟨n, le_of_lt hn⟩)
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
[PROOFSTEP]
refine' this.imp fun fl h z => _
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
fl : ℤ
h : ↑fl ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ fl
z : ℤ
⊢ z ≤ fl ↔ ↑z ≤ x
[PROOFSTEP]
cases' h with h₁ h₂
[GOAL]
case intro
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
fl z : ℤ
h₁ : ↑fl ≤ x
h₂ : ∀ (z : ℤ), ↑z ≤ x → z ≤ fl
⊢ z ≤ fl ↔ ↑z ≤ x
[PROOFSTEP]
exact ⟨fun h => le_trans (Int.cast_le.2 h) h₁, h₂ z⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
[PROOFSTEP]
have h : ∃ n : ℕ, x < y ^ n := pow_unbounded_of_one_lt _ hy
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
[PROOFSTEP]
classical exact
  let n := Nat.find h
  have hn : x < y ^ n := Nat.find_spec h
  have hnp : 0 < n := pos_iff_ne_zero.2 fun hn0 => by rw [hn0, pow_zero] at hn ; exact not_le_of_gt hn hx
  have hnsp : Nat.pred n + 1 = n := Nat.succ_pred_eq_of_pos hnp
  have hltn : Nat.pred n < n := Nat.pred_lt (ne_of_gt hnp)
  ⟨Nat.pred n, le_of_not_lt (Nat.find_min h hltn), by rwa [hnsp]⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
[PROOFSTEP]
exact
  let n := Nat.find h
  have hn : x < y ^ n := Nat.find_spec h
  have hnp : 0 < n := pos_iff_ne_zero.2 fun hn0 => by rw [hn0, pow_zero] at hn ; exact not_le_of_gt hn hx
  have hnsp : Nat.pred n + 1 = n := Nat.succ_pred_eq_of_pos hnp
  have hltn : Nat.pred n < n := Nat.pred_lt (ne_of_gt hnp)
  ⟨Nat.pred n, le_of_not_lt (Nat.find_min h hltn), by rwa [hnsp]⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < y ^ n
hn0 : n = 0
⊢ False
[PROOFSTEP]
rw [hn0, pow_zero] at hn
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < 1
hn0 : n = 0
⊢ False
[PROOFSTEP]
exact not_le_of_gt hn hx
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < y ^ n
hnp : 0 < n
hnsp : Nat.pred n + 1 = n
hltn : Nat.pred n < n
⊢ x < y ^ (Nat.pred n + 1)
[PROOFSTEP]
rwa [hnsp]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))
[PROOFSTEP]
classical exact
  let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
  have he : ∃ m : ℤ, y ^ m ≤ x :=
    ⟨-N,
      le_of_lt
        (by
          rw [zpow_neg y ↑N, zpow_ofNat]
          exact (inv_lt hx (lt_trans (inv_pos.2 hx) hN)).1 hN)⟩
  let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
  have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b :=
    ⟨M, fun m hm =>
      le_of_not_lt fun hlt =>
        not_lt_of_ge (zpow_le_of_le hy.le hlt.le) (lt_of_le_of_lt hm (by rwa [← zpow_ofNat] at hM ))⟩
  let ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
  ⟨n, hn₁, lt_of_not_ge fun hge => not_le_of_gt (Int.lt_succ _) (hn₂ _ hge)⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))
[PROOFSTEP]
exact
  let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
  have he : ∃ m : ℤ, y ^ m ≤ x :=
    ⟨-N,
      le_of_lt
        (by
          rw [zpow_neg y ↑N, zpow_ofNat]
          exact (inv_lt hx (lt_trans (inv_pos.2 hx) hN)).1 hN)⟩
  let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
  have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b :=
    ⟨M, fun m hm =>
      le_of_not_lt fun hlt =>
        not_lt_of_ge (zpow_le_of_le hy.le hlt.le) (lt_of_le_of_lt hm (by rwa [← zpow_ofNat] at hM ))⟩
  let ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
  ⟨n, hn₁, lt_of_not_ge fun hge => not_le_of_gt (Int.lt_succ _) (hn₂ _ hge)⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ y ^ (-↑N) < x
[PROOFSTEP]
rw [zpow_neg y ↑N, zpow_ofNat]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ (y ^ N)⁻¹ < x
[PROOFSTEP]
exact (inv_lt hx (lt_trans (inv_pos.2 hx) hN)).1 hN
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
he : ∃ m, y ^ m ≤ x
M : ℕ
hM : x < y ^ M
m : ℤ
hm : y ^ m ≤ x
hlt : ↑M < m
⊢ x < y ^ ↑M
[PROOFSTEP]
rwa [← zpow_ofNat] at hM
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ y ^ (-(m + 1)) < x
[PROOFSTEP]
rwa [zpow_neg, inv_lt (zpow_pos_of_pos hyp _) hx]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ x ≤ y ^ (-(m + 1) + 1)
[PROOFSTEP]
rwa [neg_add, neg_add_cancel_right, zpow_neg, le_inv hx (zpow_pos_of_pos hyp _)]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
⊢ ∃ n, y ^ n < x
[PROOFSTEP]
by_cases y_pos : y ≤ 0
[GOAL]
case pos
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ ∃ n, y ^ n < x
[PROOFSTEP]
use 1
[GOAL]
case h
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ y ^ 1 < x
[PROOFSTEP]
simp only [pow_one]
[GOAL]
case h
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ y < x
[PROOFSTEP]
linarith
[GOAL]
case neg
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : ¬y ≤ 0
⊢ ∃ n, y ^ n < x
[PROOFSTEP]
rw [not_le] at y_pos
[GOAL]
case neg
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : 0 < y
⊢ ∃ n, y ^ n < x
[PROOFSTEP]
rcases pow_unbounded_of_one_lt x⁻¹ (one_lt_inv y_pos hy) with ⟨q, hq⟩
[GOAL]
case neg.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < y⁻¹ ^ q
⊢ ∃ n, y ^ n < x
[PROOFSTEP]
exact ⟨q, by rwa [inv_pow, inv_lt_inv hx (pow_pos y_pos _)] at hq ⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < y⁻¹ ^ q
⊢ y ^ q < x
[PROOFSTEP]
rwa [inv_pow, inv_lt_inv hx (pow_pos y_pos _)] at hq
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
⊢ ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n
[PROOFSTEP]
rcases exists_nat_pow_near (one_le_inv_iff.2 ⟨xpos, hx⟩) (one_lt_inv_iff.2 ⟨ypos, hy⟩) with ⟨n, hn, h'n⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n
[PROOFSTEP]
refine' ⟨n, _, _⟩
[GOAL]
case intro.intro.refine'_1
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ y ^ (n + 1) < x
[PROOFSTEP]
rwa [inv_pow, inv_lt_inv xpos (pow_pos ypos _)] at h'n
[GOAL]
case intro.intro.refine'_2
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ x ≤ y ^ n
[PROOFSTEP]
rwa [inv_pow, inv_le_inv (pow_pos ypos _) xpos] at hn
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y ε x : α
n : ℕ
h : x < ↑n
⊢ x < ↑↑n
[PROOFSTEP]
rwa [Rat.cast_coe_nat]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y ε x : α
n : ℤ
h : ↑n < x
⊢ ↑↑n < x
[PROOFSTEP]
rwa [Rat.cast_coe_int]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
⊢ ∃ q, x < ↑q ∧ ↑q < y
[PROOFSTEP]
cases' exists_nat_gt (y - x)⁻¹ with n nh
[GOAL]
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
⊢ ∃ q, x < ↑q ∧ ↑q < y
[PROOFSTEP]
cases' exists_floor (x * n) with z zh
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
⊢ ∃ q, x < ↑q ∧ ↑q < y
[PROOFSTEP]
refine' ⟨(z + 1 : ℤ) / n, _⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
⊢ x < ↑(↑(z + 1) / ↑n) ∧ ↑(↑(z + 1) / ↑n) < y
[PROOFSTEP]
have n0' := (inv_pos.2 (sub_pos.2 h)).trans nh
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ x < ↑(↑(z + 1) / ↑n) ∧ ↑(↑(z + 1) / ↑n) < y
[PROOFSTEP]
have n0 := Nat.cast_pos.1 n0'
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ x < ↑(↑(z + 1) / ↑n) ∧ ↑(↑(z + 1) / ↑n) < y
[PROOFSTEP]
rw [Rat.cast_div_of_ne_zero, Rat.cast_coe_nat, Rat.cast_coe_int, div_lt_iff n0']
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ x < ↑(z + 1) / ↑n ∧ ↑(z + 1) < y * ↑n
case intro.intro.md
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑(z + 1)).den ≠ 0
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).num ≠ 0
case intro.intro.nd
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).den ≠ 0
[PROOFSTEP]
refine' ⟨(lt_div_iff n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), _⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(z + 1) < y * ↑n
case intro.intro.md
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑(z + 1)).den ≠ 0
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).num ≠ 0
case intro.intro.nd
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).den ≠ 0
[PROOFSTEP]
rw [Int.cast_add, Int.cast_one]
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑z + 1 < y * ↑n
case intro.intro.md
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑(z + 1)).den ≠ 0
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).num ≠ 0
case intro.intro.nd
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).den ≠ 0
[PROOFSTEP]
refine' lt_of_le_of_lt (add_le_add_right ((zh _).1 le_rfl) _) _
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ x * ↑n + 1 < y * ↑n
case intro.intro.md
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑(z + 1)).den ≠ 0
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).num ≠ 0
case intro.intro.nd
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).den ≠ 0
[PROOFSTEP]
rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff' (sub_pos.2 h), one_div]
[GOAL]
case intro.intro.md
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑(z + 1)).den ≠ 0
[PROOFSTEP]
rw [Rat.coe_int_den, Nat.cast_one]
[GOAL]
case intro.intro.md
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).num ≠ 0
[PROOFSTEP]
intro H
[GOAL]
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
H : ↑(↑n).num = 0
⊢ False
[PROOFSTEP]
rw [Rat.coe_nat_num, Int.cast_ofNat, Nat.cast_eq_zero] at H
[GOAL]
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
H : n = 0
⊢ False
[PROOFSTEP]
subst H
[GOAL]
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
z : ℤ
nh : (y - x)⁻¹ < ↑0
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑0
n0' : 0 < ↑0
n0 : 0 < 0
⊢ False
[PROOFSTEP]
cases n0
[GOAL]
case intro.intro.nd
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).den ≠ 0
[PROOFSTEP]
rw [Rat.coe_nat_den, Nat.cast_one]
[GOAL]
case intro.intro.nd
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
⊢ ∃ n, 1 / (↑n + 1) < ε
[PROOFSTEP]
cases' exists_nat_gt (1 / ε) with n hn
[GOAL]
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ∃ n, 1 / (↑n + 1) < ε
[PROOFSTEP]
use n
[GOAL]
case h
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / (↑n + 1) < ε
[PROOFSTEP]
rw [div_lt_iff, ← div_lt_iff' hε]
[GOAL]
case h
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / ε < ↑n + 1
[PROOFSTEP]
apply hn.trans
[GOAL]
case h
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ↑n < ↑n + 1
[PROOFSTEP]
simp [zero_lt_one]
[GOAL]
case h
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 0 < ↑n + 1
[PROOFSTEP]
exact n.cast_add_one_pos
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y ε x : α
x0 : 0 < x
⊢ ∃ q, 0 < q ∧ ↑q < x
[PROOFSTEP]
simpa only [Rat.cast_pos] using exists_rat_btwn x0
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
H : ∀ (x : α), ∃ n, x < ↑n
x y : α
y0 : 0 < y
n : ℕ
h : x / y < ↑n
⊢ x < n • y
[PROOFSTEP]
rwa [div_lt_iff y0, ← nsmul_eq_mul] at h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
⊢ (∀ (x : α), ∃ n, x < ↑n) → Archimedean α
[PROOFSTEP]
rw [archimedean_iff_nat_lt]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
⊢ (∀ (x : α), ∃ n, x < ↑n) → ∀ (x : α), ∃ n, x < ↑n
[PROOFSTEP]
intro h x
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
h : ∀ (x : α), ∃ n, x < ↑n
x : α
⊢ ∃ n, x < ↑n
[PROOFSTEP]
obtain ⟨n, h⟩ := h x
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
h✝ : ∀ (x : α), ∃ n, x < ↑n
x : α
n : ℤ
h : x < ↑n
⊢ ∃ n, x < ↑n
[PROOFSTEP]
refine' ⟨n.toNat, h.trans_le _⟩
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
h✝ : ∀ (x : α), ∃ n, x < ↑n
x : α
n : ℤ
h : x < ↑n
⊢ ↑n ≤ ↑(toNat n)
[PROOFSTEP]
exact_mod_cast Int.self_le_toNat _
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
H : ∀ (x : α), ∃ q, x < ↑q
x : α
q : ℚ
h : x < ↑q
⊢ ↑q ≤ ↑⌈q⌉₊
[PROOFSTEP]
simpa only [Rat.cast_coe_nat] using (@Rat.cast_le α _ _ _).2 (Nat.le_ceil _)
[GOAL]
α : Type u_1
n m : ℕ
m0 : 0 < m
⊢ n ≤ n • m
[PROOFSTEP]
rw [← mul_one n, smul_eq_mul, mul_assoc, one_mul m]
[GOAL]
α : Type u_1
n m : ℕ
m0 : 0 < m
⊢ n * 1 ≤ n * m
[PROOFSTEP]
exact Nat.mul_le_mul_left n (by linarith)
[GOAL]
α : Type u_1
n m : ℕ
m0 : 0 < m
⊢ 1 ≤ m
[PROOFSTEP]
linarith
[GOAL]
α : Type u_1
n m : ℤ
m0 : 0 < m
⊢ ↑(toNat n) ≤ toNat n • m
[PROOFSTEP]
simpa only [nsmul_eq_mul, zero_add, mul_one] using
  mul_le_mul_of_nonneg_left (Int.add_one_le_iff.2 m0) (Int.ofNat_zero_le n.toNat)
[GOAL]
α : Type u_1
q : ℚ
⊢ q ≤ ↑q
[PROOFSTEP]
rw [Rat.cast_id]
[GOAL]
α✝ : Type u_1
α : Type ?u.91487
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
⊢ Archimedean α
[PROOFSTEP]
rw [archimedean_iff_int_le]
[GOAL]
α✝ : Type u_1
α : Type ?u.91487
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
⊢ ∀ (x : α), ∃ n, x ≤ ↑n
[PROOFSTEP]
exact fun x => ⟨⌈x⌉, Int.le_ceil x⟩


[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedSemiring k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : 0 < c
⊢ c • a < 0 ↔ a < 0
[PROOFSTEP]
rw [← neg_neg a, smul_neg, neg_neg_iff_pos, neg_neg_iff_pos]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedSemiring k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : 0 < c
⊢ 0 < c • -a ↔ 0 < -a
[PROOFSTEP]
exact smul_pos_iff_of_pos hc
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : a < b
hc : c < 0
⊢ c • b < c • a
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : a < b
hc : c < 0
⊢ -c • a < -c • b
[PROOFSTEP]
exact smul_lt_smul_of_pos h (neg_pos_of_neg hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : a ≤ b
hc : c ≤ 0
⊢ c • b ≤ c • a
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_le_neg_iff]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : a ≤ b
hc : c ≤ 0
⊢ -c • a ≤ -c • b
[PROOFSTEP]
exact smul_le_smul_of_nonneg h (neg_nonneg_of_nonpos hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hab : c • a = c • b
hc : c < 0
h : a ≤ b
⊢ a = b
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_inj] at hab
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hab : -c • a = -c • b
hc : c < 0
h : a ≤ b
⊢ a = b
[PROOFSTEP]
exact eq_of_smul_eq_smul_of_pos_of_le hab (neg_pos_of_neg hc) h
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : c • a < c • b
hc : c ≤ 0
⊢ b < a
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff] at h
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : -c • b < -c • a
hc : c ≤ 0
⊢ b < a
[PROOFSTEP]
exact lt_of_smul_lt_smul_of_nonneg h (neg_nonneg_of_nonpos hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ c • a < c • b ↔ b < a
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ -c • b < -c • a ↔ b < a
[PROOFSTEP]
exact smul_lt_smul_iff_of_pos (neg_pos_of_neg hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ c • a < 0 ↔ 0 < a
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_neg_iff_pos]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ 0 < -c • a ↔ 0 < a
[PROOFSTEP]
exact smul_pos_iff_of_pos (neg_pos_of_neg hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ 0 < c • a ↔ a < 0
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_pos]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ -c • a < 0 ↔ a < 0
[PROOFSTEP]
exact smul_neg_iff_of_pos (neg_pos_of_neg hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : k
c d : M
hab : a ≤ b
hcd : c ≤ d
⊢ a • d + b • c ≤ a • c + b • d
[PROOFSTEP]
obtain ⟨b, rfl⟩ := exists_add_of_le hab
[GOAL]
case intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c d : M
hcd : c ≤ d
b : k
hab : a ≤ a + b
⊢ a • d + (a + b) • c ≤ a • c + (a + b) • d
[PROOFSTEP]
obtain ⟨d, rfl⟩ := exists_add_of_le hcd
[GOAL]
case intro.intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c : M
b : k
hab : a ≤ a + b
d : M
hcd : c ≤ c + d
⊢ a • (c + d) + (a + b) • c ≤ a • c + (a + b) • (c + d)
[PROOFSTEP]
rw [smul_add, add_right_comm, smul_add, ← add_assoc, add_smul _ _ d]
[GOAL]
case intro.intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c : M
b : k
hab : a ≤ a + b
d : M
hcd : c ≤ c + d
⊢ a • c + (a + b) • c + a • d ≤ a • c + (a + b) • c + (a • d + b • d)
[PROOFSTEP]
rw [le_add_iff_nonneg_right] at hab hcd
[GOAL]
case intro.intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c : M
b : k
hab : 0 ≤ b
d : M
hcd : 0 ≤ d
⊢ a • c + (a + b) • c + a • d ≤ a • c + (a + b) • c + (a • d + b • d)
[PROOFSTEP]
exact add_le_add_left (le_add_of_nonneg_right <| smul_nonneg hab hcd) _
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : k
c d : M
hba : b ≤ a
hdc : d ≤ c
⊢ a • d + b • c ≤ a • c + b • d
[PROOFSTEP]
rw [add_comm (a • d), add_comm (a • c)]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : k
c d : M
hba : b ≤ a
hdc : d ≤ c
⊢ b • c + a • d ≤ b • d + a • c
[PROOFSTEP]
exact smul_add_smul_le_smul_add_smul hba hdc
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : k
c d : M
hab : a < b
hcd : c < d
⊢ a • d + b • c < a • c + b • d
[PROOFSTEP]
obtain ⟨b, rfl⟩ := exists_add_of_le hab.le
[GOAL]
case intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : k
c d : M
hcd : c < d
b : k
hab : a < a + b
⊢ a • d + (a + b) • c < a • c + (a + b) • d
[PROOFSTEP]
obtain ⟨d, rfl⟩ := exists_add_of_le hcd.le
[GOAL]
case intro.intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : k
c : M
b : k
hab : a < a + b
d : M
hcd : c < c + d
⊢ a • (c + d) + (a + b) • c < a • c + (a + b) • (c + d)
[PROOFSTEP]
rw [smul_add, add_right_comm, smul_add, ← add_assoc, add_smul _ _ d]
[GOAL]
case intro.intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : k
c : M
b : k
hab : a < a + b
d : M
hcd : c < c + d
⊢ a • c + (a + b) • c + a • d < a • c + (a + b) • c + (a • d + b • d)
[PROOFSTEP]
rw [lt_add_iff_pos_right] at hab hcd
[GOAL]
case intro.intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : k
c : M
b : k
hab : 0 < b
d : M
hcd : 0 < d
⊢ a • c + (a + b) • c + a • d < a • c + (a + b) • c + (a • d + b • d)
[PROOFSTEP]
exact add_lt_add_left (lt_add_of_pos_right _ <| smul_pos hab hcd) _
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : k
c d : M
hba : b < a
hdc : d < c
⊢ a • d + b • c < a • c + b • d
[PROOFSTEP]
rw [add_comm (a • d), add_comm (a • c)]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : k
c d : M
hba : b < a
hdc : d < c
⊢ b • c + a • d < b • d + a • c
[PROOFSTEP]
exact smul_add_smul_lt_smul_add_smul hba hdc
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ c • a ≤ c • b ↔ b ≤ a
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_le_neg_iff]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ -c • b ≤ -c • a ↔ b ≤ a
[PROOFSTEP]
exact smul_le_smul_iff_of_pos (neg_pos_of_neg hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : c < 0
⊢ c⁻¹ • a ≤ b ↔ c • b ≤ a
[PROOFSTEP]
rw [← smul_le_smul_iff_of_neg h, smul_inv_smul₀ h.ne]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : c < 0
⊢ c⁻¹ • a < b ↔ c • b < a
[PROOFSTEP]
rw [← smul_lt_smul_iff_of_neg h, smul_inv_smul₀ h.ne]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : c < 0
⊢ a ≤ c⁻¹ • b ↔ b ≤ c • a
[PROOFSTEP]
rw [← smul_le_smul_iff_of_neg h, smul_inv_smul₀ h.ne]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : c < 0
⊢ a < c⁻¹ • b ↔ b < c • a
[PROOFSTEP]
rw [← smul_lt_smul_iff_of_neg h, smul_inv_smul₀ h.ne]


[GOAL]
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r₁ r₂ : R
⊢ 0 = r₁ • 0 + op r₂ • 0
[PROOFSTEP]
rw [smul_zero, zero_add, smul_zero]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
m₁ m₂ : M
⊢ 0 • m₂ + 0 • m₁ = 0
[PROOFSTEP]
rw [zero_smul, zero_add, zero_smul]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
r : R
m : M
⊢ r • m + 0 • 0 = r • m
[PROOFSTEP]
rw [smul_zero, add_zero]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
r : R
m : M
⊢ 0 • 0 + op r • m = op r • m
[PROOFSTEP]
rw [smul_zero, zero_add]
[GOAL]
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
src✝¹ : One (tsze R M) := one
src✝ : Mul (tsze R M) := mul
x : tsze R M
⊢ 1 • x.snd + op x.fst • 0 = x.snd
[PROOFSTEP]
rw [one_smul, smul_zero, add_zero]
[GOAL]
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
src✝¹ : One (tsze R M) := one
src✝ : Mul (tsze R M) := mul
x : tsze R M
⊢ x.fst • 0 + 1 • x.snd = x.snd
[PROOFSTEP]
rw [smul_zero, zero_add, one_smul]
[GOAL]
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
src✝¹ : AddMonoid (tsze R M) := addMonoid
src✝ : One (tsze R M) := one
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
simp [Nat.cast]
[GOAL]
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
src✝¹ : AddMonoid (tsze R M) := addMonoid
src✝ : One (tsze R M) := one
x✝ : ℕ
⊢ NatCast.natCast (x✝ + 1) = NatCast.natCast x✝ + 1
[PROOFSTEP]
ext
[GOAL]
case h1
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
src✝¹ : AddMonoid (tsze R M) := addMonoid
src✝ : One (tsze R M) := one
x✝ : ℕ
⊢ fst (NatCast.natCast (x✝ + 1)) = fst (NatCast.natCast x✝ + 1)
[PROOFSTEP]
simp [Nat.cast]
[GOAL]
case h2
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
src✝¹ : AddMonoid (tsze R M) := addMonoid
src✝ : One (tsze R M) := one
x✝ : ℕ
⊢ snd (NatCast.natCast (x✝ + 1)) = snd (NatCast.natCast x✝ + 1)
[PROOFSTEP]
simp [Nat.cast]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
src✝² : AddMonoidWithOne (tsze R M) := addMonoidWithOne
src✝¹ : MulOneClass (tsze R M) := mulOneClass
src✝ : AddCommMonoid (tsze R M) := addCommMonoid
x₁ x₂ x₃ : tsze R M
⊢ x₁.fst • (x₂.snd + x₃.snd) + (op x₂.fst + op x₃.fst) • x₁.snd =
    x₁.fst • x₂.snd + op x₂.fst • x₁.snd + (x₁.fst • x₃.snd + op x₃.fst • x₁.snd)
[PROOFSTEP]
simp_rw [smul_add, add_smul, add_add_add_comm]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
src✝² : AddMonoidWithOne (tsze R M) := addMonoidWithOne
src✝¹ : MulOneClass (tsze R M) := mulOneClass
src✝ : AddCommMonoid (tsze R M) := addCommMonoid
x₁ x₂ x₃ : tsze R M
⊢ (x₁.fst + x₂.fst) • x₃.snd + op x₃.fst • (x₁.snd + x₂.snd) =
    x₁.fst • x₃.snd + op x₃.fst • x₁.snd + (x₂.fst • x₃.snd + op x₃.fst • x₂.snd)
[PROOFSTEP]
simp_rw [add_smul, smul_add, add_add_add_comm]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
src✝² : AddMonoidWithOne (tsze R M) := addMonoidWithOne
src✝¹ : MulOneClass (tsze R M) := mulOneClass
src✝ : AddCommMonoid (tsze R M) := addCommMonoid
x : tsze R M
⊢ 0 • x.snd + op x.fst • 0 = 0
[PROOFSTEP]
rw [zero_smul, zero_add, smul_zero]
[GOAL]
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
src✝² : AddMonoidWithOne (tsze R M) := addMonoidWithOne
src✝¹ : MulOneClass (tsze R M) := mulOneClass
src✝ : AddCommMonoid (tsze R M) := addCommMonoid
x : tsze R M
⊢ x.fst • 0 + 0 • x.snd = 0
[PROOFSTEP]
rw [smul_zero, zero_add, zero_smul]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : op (fst x) • snd x = fst x • snd x
⊢ snd (x ^ n) = n • fst x ^ Nat.pred n • snd x
[PROOFSTEP]
have : ∀ n : ℕ, op (x.fst ^ n) • x.snd = x.fst ^ n • x.snd :=
  by
  intro n
  induction' n with n ih
  · simp
  · rw [pow_succ', MulOpposite.op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : op (fst x) • snd x = fst x • snd x
⊢ ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
[PROOFSTEP]
intro n
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
n : ℕ
⊢ op (fst x ^ n) • snd x = fst x ^ n • snd x
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : op (fst x) • snd x = fst x • snd x
⊢ op (fst x ^ Nat.zero) • snd x = fst x ^ Nat.zero • snd x
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
n : ℕ
ih : op (fst x ^ n) • snd x = fst x ^ n • snd x
⊢ op (fst x ^ Nat.succ n) • snd x = fst x ^ Nat.succ n • snd x
[PROOFSTEP]
rw [pow_succ', MulOpposite.op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
⊢ snd (x ^ n) = n • fst x ^ Nat.pred n • snd x
[PROOFSTEP]
simp_rw [snd_pow_eq_sum, this, smul_smul, ← pow_add]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
⊢ List.sum (List.map (fun i => fst x ^ (Nat.pred n - i + i) • snd x) (List.range n)) = n • fst x ^ Nat.pred n • snd x
[PROOFSTEP]
match n with
| 0 => rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
| (Nat.succ n) =>
  simp_rw [Nat.pred_succ]
  refine' (List.sum_eq_card_nsmul _ (x.fst ^ n • x.snd) _).trans _
  · rintro m hm
    simp_rw [List.mem_map, List.mem_range] at hm
    obtain ⟨i, hi, rfl⟩ := hm
    rw [tsub_add_cancel_of_le (Nat.lt_succ_iff.mp hi)]
  · rw [List.length_map, List.length_range]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
⊢ List.sum (List.map (fun i => fst x ^ (Nat.pred 0 - i + i) • snd x) (List.range 0)) = 0 • fst x ^ Nat.pred 0 • snd x
[PROOFSTEP]
rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n : ℕ
⊢ List.sum (List.map (fun i => fst x ^ (Nat.pred (Nat.succ n) - i + i) • snd x) (List.range (Nat.succ n))) =
    Nat.succ n • fst x ^ Nat.pred (Nat.succ n) • snd x
[PROOFSTEP]
simp_rw [Nat.pred_succ]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n : ℕ
⊢ List.sum (List.map (fun i => fst x ^ (n - i + i) • snd x) (List.range (Nat.succ n))) = Nat.succ n • fst x ^ n • snd x
[PROOFSTEP]
refine' (List.sum_eq_card_nsmul _ (x.fst ^ n • x.snd) _).trans _
[GOAL]
case refine'_1
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n : ℕ
⊢ ∀ (x_1 : M), x_1 ∈ List.map (fun i => fst x ^ (n - i + i) • snd x) (List.range (Nat.succ n)) → x_1 = fst x ^ n • snd x
[PROOFSTEP]
rintro m hm
[GOAL]
case refine'_1
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n : ℕ
m : M
hm : m ∈ List.map (fun i => fst x ^ (n - i + i) • snd x) (List.range (Nat.succ n))
⊢ m = fst x ^ n • snd x
[PROOFSTEP]
simp_rw [List.mem_map, List.mem_range] at hm
[GOAL]
case refine'_1
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n : ℕ
m : M
hm : ∃ a, a < Nat.succ n ∧ fst x ^ (n - a + a) • snd x = m
⊢ m = fst x ^ n • snd x
[PROOFSTEP]
obtain ⟨i, hi, rfl⟩ := hm
[GOAL]
case refine'_1.intro.intro
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n i : ℕ
hi : i < Nat.succ n
⊢ fst x ^ (n - i + i) • snd x = fst x ^ n • snd x
[PROOFSTEP]
rw [tsub_add_cancel_of_le (Nat.lt_succ_iff.mp hi)]
[GOAL]
case refine'_2
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : op (fst x) • snd x = fst x • snd x
this : ∀ (n : ℕ), op (fst x ^ n) • snd x = fst x ^ n • snd x
n : ℕ
⊢ List.length (List.map (fun i => fst x ^ (n - i + i) • snd x) (List.range (Nat.succ n))) • fst x ^ n • snd x =
    Nat.succ n • fst x ^ n • snd x
[PROOFSTEP]
rw [List.length_map, List.length_range]
[GOAL]
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
n : ℕ
⊢ snd (inl r ^ n) = snd (inl (r ^ n))
[PROOFSTEP]
simp [snd_pow_eq_sum]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x y z : tsze R M
⊢ (x.fst * y.fst) • z.snd + op z.fst • (x.fst • y.snd + op y.fst • x.snd) =
    x.fst • (y.fst • z.snd + op z.fst • y.snd) + (op z.fst * op y.fst) • x.snd
[PROOFSTEP]
simp_rw [smul_add, ← mul_smul, add_assoc, smul_comm]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
⊢ snd ((fun n x => x ^ n) 0 x) = snd 1
[PROOFSTEP]
simp [snd_pow_eq_sum]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
n : ℕ
x : tsze R M
⊢ snd ((fun n x => x ^ n) (n + 1) x) = snd (x * (fun n x => x ^ n) n x)
[PROOFSTEP]
simp_rw [snd_mul, snd_pow_eq_sum, Nat.pred_succ]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
n : ℕ
x : tsze R M
⊢ List.sum (List.map (fun i => fst x ^ (n - i) • op (fst x ^ i) • snd x) (List.range (n + 1))) =
    fst x • List.sum (List.map (fun i => fst x ^ (Nat.pred n - i) • op (fst x ^ i) • snd x) (List.range n)) +
      op (fst (x ^ n)) • snd x
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
⊢ List.sum (List.map (fun i => fst x ^ (Nat.zero - i) • op (fst x ^ i) • snd x) (List.range (Nat.zero + 1))) =
    fst x •
        List.sum (List.map (fun i => fst x ^ (Nat.pred Nat.zero - i) • op (fst x ^ i) • snd x) (List.range Nat.zero)) +
      op (fst (x ^ Nat.zero)) • snd x
[PROOFSTEP]
simp [List.range_succ]
[GOAL]
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ : ℕ
⊢ List.sum (List.map (fun i => fst x ^ (Nat.succ n✝ - i) • op (fst x ^ i) • snd x) (List.range (Nat.succ n✝ + 1))) =
    fst x •
        List.sum
          (List.map (fun i => fst x ^ (Nat.pred (Nat.succ n✝) - i) • op (fst x ^ i) • snd x)
            (List.range (Nat.succ n✝))) +
      op (fst (x ^ Nat.succ n✝)) • snd x
[PROOFSTEP]
simp_rw [Nat.pred_succ]
[GOAL]
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ : ℕ
⊢ List.sum (List.map (fun i => fst x ^ (Nat.succ n✝ - i) • op (fst x ^ i) • snd x) (List.range (Nat.succ n✝ + 1))) =
    fst x • List.sum (List.map (fun i => fst x ^ (n✝ - i) • op (fst x ^ i) • snd x) (List.range (Nat.succ n✝))) +
      op (fst (x ^ Nat.succ n✝)) • snd x
[PROOFSTEP]
rw [List.range_succ, List.map_append, List.sum_append, List.map_singleton, List.sum_singleton, Nat.sub_self, pow_zero,
  one_smul, List.smul_sum, List.map_map, fst_pow]
  --porting note: `Function.comp` no longer works in `rw` so move to `simp_rw`
[GOAL]
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ : ℕ
⊢ List.sum (List.map (fun i => fst x ^ (Nat.succ n✝ - i) • op (fst x ^ i) • snd x) (List.range (n✝ + 1))) +
      op (fst x ^ (n✝ + 1)) • snd x =
    List.sum
        (List.map ((fun x x_1 => x • x_1) (fst x) ∘ fun i => fst x ^ (n✝ - i) • op (fst x ^ i) • snd x)
          (List.range (Nat.succ n✝))) +
      op (fst x ^ Nat.succ n✝) • snd x
[PROOFSTEP]
simp_rw [Function.comp, smul_smul, ← pow_succ, Nat.succ_eq_add_one]
[GOAL]
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ : ℕ
⊢ List.sum (List.map (fun i => fst x ^ (n✝ + 1 - i) • op (fst x ^ i) • snd x) (List.range (n✝ + 1))) +
      op (fst x ^ (n✝ + 1)) • snd x =
    List.sum (List.map (fun x_1 => fst x ^ (n✝ - x_1 + 1) • op (fst x ^ x_1) • snd x) (List.range (n✝ + 1))) +
      op (fst x ^ (n✝ + 1)) • snd x
[PROOFSTEP]
congr 2
[GOAL]
case succ.e_a.e_a
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ : ℕ
⊢ List.map (fun i => fst x ^ (n✝ + 1 - i) • op (fst x ^ i) • snd x) (List.range (n✝ + 1)) =
    List.map (fun x_1 => fst x ^ (n✝ - x_1 + 1) • op (fst x ^ x_1) • snd x) (List.range (n✝ + 1))
[PROOFSTEP]
refine' List.map_congr fun i hi => _
[GOAL]
case succ.e_a.e_a
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ i : ℕ
hi : i ∈ List.range (n✝ + 1)
⊢ fst x ^ (n✝ + 1 - i) • op (fst x ^ i) • snd x = fst x ^ (n✝ - i + 1) • op (fst x ^ i) • snd x
[PROOFSTEP]
rw [List.mem_range, Nat.lt_succ_iff] at hi
[GOAL]
case succ.e_a.e_a
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
src✝ : MulOneClass (tsze R M) := mulOneClass
x : tsze R M
n✝ i : ℕ
hi : i ≤ n✝
⊢ fst x ^ (n✝ + 1 - i) • op (fst x ^ i) • snd x = fst x ^ (n✝ - i + 1) • op (fst x ^ i) • snd x
[PROOFSTEP]
rw [Nat.sub_add_comm hi]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
l : List (tsze R M)
⊢ snd (List.prod l) =
    List.sum
      (List.map
        (fun x =>
          List.prod (List.take x.fst (List.map fst l)) •
            op (List.prod (List.drop (Nat.succ x.fst) (List.map fst l))) • snd x.snd)
        (List.enum l))
[PROOFSTEP]
induction' l with x xs ih
[GOAL]
case nil
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
⊢ snd (List.prod []) =
    List.sum
      (List.map
        (fun x =>
          List.prod (List.take x.fst (List.map fst [])) •
            op (List.prod (List.drop (Nat.succ x.fst) (List.map fst []))) • snd x.snd)
        (List.enum []))
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  snd (List.prod xs) =
    List.sum
      (List.map
        (fun x =>
          List.prod (List.take x.fst (List.map fst xs)) •
            op (List.prod (List.drop (Nat.succ x.fst) (List.map fst xs))) • snd x.snd)
        (List.enum xs))
⊢ snd (List.prod (x :: xs)) =
    List.sum
      (List.map
        (fun x_1 =>
          List.prod (List.take x_1.fst (List.map fst (x :: xs))) •
            op (List.prod (List.drop (Nat.succ x_1.fst) (List.map fst (x :: xs)))) • snd x_1.snd)
        (List.enum (x :: xs)))
[PROOFSTEP]
rw [List.enum_cons, ← List.map_fst_add_enum_eq_enumFrom]
[GOAL]
case cons
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  snd (List.prod xs) =
    List.sum
      (List.map
        (fun x =>
          List.prod (List.take x.fst (List.map fst xs)) •
            op (List.prod (List.drop (Nat.succ x.fst) (List.map fst xs))) • snd x.snd)
        (List.enum xs))
⊢ snd (List.prod (x :: xs)) =
    List.sum
      (List.map
        (fun x_1 =>
          List.prod (List.take x_1.fst (List.map fst (x :: xs))) •
            op (List.prod (List.drop (Nat.succ x_1.fst) (List.map fst (x :: xs)))) • snd x_1.snd)
        ((0, x) :: List.map (Prod.map (fun x => x + 1) id) (List.enum xs)))
[PROOFSTEP]
simp_rw [List.map_cons, List.map_map, Function.comp, Prod.map_snd, Prod.map_fst, id, List.take_zero, List.take_cons,
  List.prod_nil, List.prod_cons, snd_mul, one_smul, List.drop, mul_smul, List.sum_cons, fst_list_prod, ih,
  List.smul_sum, List.map_map]
[GOAL]
case cons
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  snd (List.prod xs) =
    List.sum
      (List.map
        (fun x =>
          List.prod (List.take x.fst (List.map fst xs)) •
            op (List.prod (List.drop (Nat.succ x.fst) (List.map fst xs))) • snd x.snd)
        (List.enum xs))
⊢ List.sum
        (List.map
          ((fun x_1 => fst x • x_1) ∘ fun x =>
            List.prod (List.take x.fst (List.map fst xs)) •
              op (List.prod (List.drop (Nat.succ x.fst) (List.map fst xs))) • snd x.snd)
          (List.enum xs)) +
      op (List.prod (List.map fst xs)) • snd x =
    op (List.prod (List.map fst xs)) • snd x +
      List.sum
        (List.map
          (fun x_1 =>
            fst x •
              List.prod (List.take x_1.fst (List.map fst xs)) •
                op (List.prod (List.drop (x_1.fst + 1) (List.map fst xs))) • snd x_1.snd)
          (List.enum xs))
[PROOFSTEP]
exact add_comm _ _
[GOAL]
R : Type u
M : Type v
inst✝⁴ : CommMonoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
src✝ : Monoid (tsze R M) := monoid
x₁ x₂ : tsze R M
⊢ x₁.fst • x₂.snd + op x₂.fst • x₁.snd = x₂.fst • x₁.snd + op x₁.fst • x₂.snd
[PROOFSTEP]
rw [op_smul_eq_smul, op_smul_eq_smul, add_comm]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Semiring R
inst✝¹³ : CommSemiring R'
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Algebra S R
inst✝¹⁰ : Algebra S R'
inst✝⁹ : Module S M
inst✝⁸ : Module R M
inst✝⁷ : Module Rᵐᵒᵖ M
inst✝⁶ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S Rᵐᵒᵖ M
inst✝³ : Module R' M
inst✝² : Module R'ᵐᵒᵖ M
inst✝¹ : IsCentralScalar R' M
inst✝ : IsScalarTower S R' M
src✝ : S →+* tsze R M := RingHom.comp (inlHom R M) (algebraMap S R)
s : S
x : (fun x => tsze R M) s
⊢ ↑(algebraMap S R) s • snd x + op (fst x) • 0 = fst x • 0 + op (↑(algebraMap S R) s) • snd x
[PROOFSTEP]
rw [smul_zero, smul_zero, add_zero, zero_add]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Semiring R
inst✝¹³ : CommSemiring R'
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Algebra S R
inst✝¹⁰ : Algebra S R'
inst✝⁹ : Module S M
inst✝⁸ : Module R M
inst✝⁷ : Module Rᵐᵒᵖ M
inst✝⁶ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S Rᵐᵒᵖ M
inst✝³ : Module R' M
inst✝² : Module R'ᵐᵒᵖ M
inst✝¹ : IsCentralScalar R' M
inst✝ : IsScalarTower S R' M
src✝ : S →+* tsze R M := RingHom.comp (inlHom R M) (algebraMap S R)
s : S
x : (fun x => tsze R M) s
⊢ ↑(algebraMap S R) s • snd x = op (↑(algebraMap S R) s) • snd x
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one, MulOpposite.op_smul, MulOpposite.op_one, smul_assoc, one_smul, smul_assoc, one_smul]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Semiring R
inst✝¹³ : CommSemiring R'
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Algebra S R
inst✝¹⁰ : Algebra S R'
inst✝⁹ : Module S M
inst✝⁸ : Module R M
inst✝⁷ : Module Rᵐᵒᵖ M
inst✝⁶ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S Rᵐᵒᵖ M
inst✝³ : Module R' M
inst✝² : Module R'ᵐᵒᵖ M
inst✝¹ : IsCentralScalar R' M
inst✝ : IsScalarTower S R' M
src✝ : S →+* tsze R M := RingHom.comp (inlHom R M) (algebraMap S R)
r : S
x : (fun x => tsze R M) r
⊢ r • x.snd = ↑(algebraMap S R) r • x.snd + op x.fst • 0
[PROOFSTEP]
rw [smul_zero, add_zero, algebraMap_smul]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Semiring R
inst✝¹⁵ : CommSemiring R'
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Algebra S R
inst✝¹² : Algebra S R'
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
inst✝² : IsScalarTower S R' M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R' A
f : M →ₗ[R'] A
hf : ∀ (x y : M), ↑f x * ↑f y = 0
⊢ ↑(algebraMap R' A) 1 + ↑f 0 = 1
[PROOFSTEP]
rw [map_zero, map_one, add_zero]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Semiring R
inst✝¹⁵ : CommSemiring R'
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Algebra S R
inst✝¹² : Algebra S R'
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
inst✝² : IsScalarTower S R' M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R' A
f : M →ₗ[R'] A
hf : ∀ (x y : M), ↑f x * ↑f y = 0
r₁ : R'
m₁ : M
r₂ : R'
m₂ : M
⊢ ↑(LinearMap.comp (Algebra.linearMap R' A) (AlgHom.toLinearMap (fstHom R' R' M)) + LinearMap.comp f (sndHom R' M))
      ((inl r₁ + inr m₁) * (inl r₂ + inr m₂)) =
    ↑(LinearMap.comp (Algebra.linearMap R' A) (AlgHom.toLinearMap (fstHom R' R' M)) + LinearMap.comp f (sndHom R' M))
        (inl r₁ + inr m₁) *
      ↑(LinearMap.comp (Algebra.linearMap R' A) (AlgHom.toLinearMap (fstHom R' R' M)) + LinearMap.comp f (sndHom R' M))
        (inl r₂ + inr m₂)
[PROOFSTEP]
dsimp
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Semiring R
inst✝¹⁵ : CommSemiring R'
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Algebra S R
inst✝¹² : Algebra S R'
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
inst✝² : IsScalarTower S R' M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R' A
f : M →ₗ[R'] A
hf : ∀ (x y : M), ↑f x * ↑f y = 0
r₁ : R'
m₁ : M
r₂ : R'
m₂ : M
⊢ ↑(algebraMap R' A) ((r₁ + 0) * (r₂ + 0)) + ↑f ((r₁ + 0) • (0 + m₂) + (op r₂ + 0) • (0 + m₁)) =
    (↑(algebraMap R' A) (r₁ + 0) + ↑f (0 + m₁)) * (↑(algebraMap R' A) (r₂ + 0) + ↑f (0 + m₂))
[PROOFSTEP]
simp only [add_zero, zero_add, add_mul, mul_add, smul_mul_smul, hf, smul_zero, op_smul_eq_smul]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Semiring R
inst✝¹⁵ : CommSemiring R'
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Algebra S R
inst✝¹² : Algebra S R'
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
inst✝² : IsScalarTower S R' M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R' A
f : M →ₗ[R'] A
hf : ∀ (x y : M), ↑f x * ↑f y = 0
r₁ : R'
m₁ : M
r₂ : R'
m₂ : M
⊢ ↑(algebraMap R' A) (r₁ * r₂) + ↑f (r₁ • m₂ + r₂ • m₁) =
    ↑(algebraMap R' A) r₁ * ↑(algebraMap R' A) r₂ + ↑f m₁ * ↑(algebraMap R' A) r₂ + ↑(algebraMap R' A) r₁ * ↑f m₂
[PROOFSTEP]
rw [← RingHom.map_mul, LinearMap.map_add, ← Algebra.commutes _ (f _), ← Algebra.smul_def, ← Algebra.smul_def,
  add_right_comm, add_assoc, LinearMap.map_smul, LinearMap.map_smul]
[GOAL]
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Semiring R
inst✝¹⁵ : CommSemiring R'
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Algebra S R
inst✝¹² : Algebra S R'
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
inst✝² : IsScalarTower S R' M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R' A
f : M →ₗ[R'] A
hf : ∀ (x y : M), ↑f x * ↑f y = 0
m : M
⊢ ↑(algebraMap R' A) 0 + ↑f m = ↑f m
[PROOFSTEP]
rw [RingHom.map_zero, zero_add]


[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
⊢ (∑ i in s, f i) • ∑ i in s, g i ≤ card s • ∑ i in s, f i • g i
[PROOFSTEP]
classical
obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn
rw [← card_range s.card, sum_smul_sum_eq_sum_perm hσ]
exact
  sum_le_card_nsmul _ _ _ fun n _ =>
    hfg.sum_smul_comp_perm_le_sum_smul fun x hx => hs fun h => hx <| IsFixedPt.perm_pow 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
⊢ (∑ i in s, f i) • ∑ i in s, g i ≤ card s • ∑ i in s, f i • g i
[PROOFSTEP]
obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn
[GOAL]
case 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
σ : Perm ι
hσ : IsCycleOn σ ↑s
hs : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ (∑ i in s, f i) • ∑ i in s, g i ≤ card s • ∑ i in s, f i • g i
[PROOFSTEP]
rw [← card_range s.card, sum_smul_sum_eq_sum_perm hσ]
[GOAL]
case 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
σ : Perm ι
hσ : IsCycleOn σ ↑s
hs : {x | ↑σ x ≠ x} ⊆ ↑s
⊢ ∑ k in range (card s), ∑ i in s, f i • g (↑(σ ^ k) i) ≤ card (range (card s)) • ∑ i in s, f i • g i
[PROOFSTEP]
exact
  sum_le_card_nsmul _ _ _ fun n _ =>
    hfg.sum_smul_comp_perm_le_sum_smul fun x hx => hs fun h => hx <| IsFixedPt.perm_pow 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
⊢ card s • ∑ i in s, f i • g i ≤ (∑ i in s, f i) • ∑ i in s, g i
[PROOFSTEP]
refine hfg.dual_right.sum_smul_sum_le_card_smul_sum
[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
⊢ Fintype.card ι • ∑ i : ι, f i • g i ≤ (∑ i : ι, f i) • ∑ i : ι, g i
[PROOFSTEP]
refine (hfg.dual_right.monovaryOn _).sum_smul_sum_le_card_smul_sum
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : MonovaryOn f g ↑s
⊢ (∑ i in s, f i) * ∑ i in s, g i ≤ ↑(card s) * ∑ i in s, f i * g i
[PROOFSTEP]
rw [← nsmul_eq_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : MonovaryOn f g ↑s
⊢ (∑ i in s, f i) * ∑ i in s, g i ≤ card s • ∑ i in s, f i * g i
[PROOFSTEP]
exact hfg.sum_smul_sum_le_card_smul_sum
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : AntivaryOn f g ↑s
⊢ ↑(card s) * ∑ i in s, f i * g i ≤ (∑ i in s, f i) * ∑ i in s, g i
[PROOFSTEP]
rw [← nsmul_eq_mul]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : AntivaryOn f g ↑s
⊢ card s • ∑ i in s, f i * g i ≤ (∑ i in s, f i) * ∑ i in s, g i
[PROOFSTEP]
exact hfg.card_smul_sum_le_sum_smul_sum
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
⊢ (∑ i in s, f i) ^ 2 ≤ ↑(card s) * ∑ i in s, f i ^ 2
[PROOFSTEP]
simp_rw [sq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
⊢ (∑ i in s, f i) * ∑ i in s, f i ≤ ↑(card s) * ∑ x in s, f x * f x
[PROOFSTEP]
exact (monovaryOn_self _ _).sum_mul_sum_le_card_mul_sum
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
⊢ ((∑ i in s, f i) / ↑(card s)) ^ 2 ≤ (∑ i in s, f i ^ 2) / ↑(card s)
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
f : ι → α
⊢ ((∑ i in ∅, f i) / ↑(card ∅)) ^ 2 ≤ (∑ i in ∅, f i ^ 2) / ↑(card ∅)
[PROOFSTEP]
simp
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
⊢ ((∑ i in s, f i) / ↑(card s)) ^ 2 ≤ (∑ i in s, f i ^ 2) / ↑(card s)
[PROOFSTEP]
rw [← card_pos, ← @Nat.cast_pos α] at hs
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
hs : 0 < ↑(card s)
⊢ ((∑ i in s, f i) / ↑(card s)) ^ 2 ≤ (∑ i in s, f i ^ 2) / ↑(card s)
[PROOFSTEP]
rw [div_pow, div_le_div_iff (sq_pos_of_ne_zero _ hs.ne') hs, sq (s.card : α), mul_left_comm, ← mul_assoc]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
hs : 0 < ↑(card s)
⊢ (∑ i in s, f i) ^ 2 * ↑(card s) ≤ (↑(card s) * ∑ i in s, f i ^ 2) * ↑(card s)
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right sq_sum_le_card_mul_sum_sq hs.le


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
a : WithTop α
⊢ a - ⊤ = 0
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
⊢ none - ⊤ = 0
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
val✝ : α
⊢ Option.some val✝ - ⊤ = 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
a b : WithTop α
⊢ a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
[PROOFSTEP]
induction a using recTopCoe
[GOAL]
case top
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
b : WithTop α
⊢ ⊤ - b = ⊤ ↔ ⊤ = ⊤ ∧ b ≠ ⊤
[PROOFSTEP]
induction b using recTopCoe
[GOAL]
case coe
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
b : WithTop α
a✝ : α
⊢ ↑a✝ - b = ⊤ ↔ ↑a✝ = ⊤ ∧ b ≠ ⊤
[PROOFSTEP]
induction b using recTopCoe
[GOAL]
case top.top
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
⊢ ⊤ - ⊤ = ⊤ ↔ ⊤ = ⊤ ∧ ⊤ ≠ ⊤
[PROOFSTEP]
simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, coe_ne_top, top_sub_coe, false_and, Ne.def]
[GOAL]
case top.coe
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
a✝ : α
⊢ ⊤ - ↑a✝ = ⊤ ↔ ⊤ = ⊤ ∧ ↑a✝ ≠ ⊤
[PROOFSTEP]
simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, coe_ne_top, top_sub_coe, false_and, Ne.def]
[GOAL]
case coe.top
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
a✝ : α
⊢ ↑a✝ - ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∧ ⊤ ≠ ⊤
[PROOFSTEP]
simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, coe_ne_top, top_sub_coe, false_and, Ne.def]
[GOAL]
case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : Sub α
inst✝ : Zero α
a✝¹ a✝ : α
⊢ ↑a✝¹ - ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∧ ↑a✝ ≠ ⊤
[PROOFSTEP]
simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, coe_ne_top, top_sub_coe, false_and, Ne.def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Sub α
inst✝² : Zero α
inst✝¹ : Sub β
inst✝ : Zero β
f : α → β
h : ∀ (x y : α), f (x - y) = f x - f y
h₀ : f 0 = 0
x✝ : WithTop α
⊢ map f (x✝ - ⊤) = map f x✝ - map f ⊤
[PROOFSTEP]
simp only [h₀, sub_top, WithTop.map_zero, coe_zero, map_top]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Sub α
inst✝² : Zero α
inst✝¹ : Sub β
inst✝ : Zero β
f : α → β
h : ∀ (x y : α), f (x - y) = f x - f y
h₀ : f 0 = 0
x y : α
⊢ map f (↑x - ↑y) = map f ↑x - map f ↑y
[PROOFSTEP]
simp only [← coe_sub, map_coe, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
⊢ OrderedSub (WithTop α)
[PROOFSTEP]
constructor
[GOAL]
case tsub_le_iff_right
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
⊢ ∀ (a b c : WithTop α), a - b ≤ c ↔ a ≤ c + b
[PROOFSTEP]
rintro x y z
[GOAL]
case tsub_le_iff_right
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y z : WithTop α
⊢ x - y ≤ z ↔ x ≤ z + y
[PROOFSTEP]
induction y using WithTop.recTopCoe
[GOAL]
case tsub_le_iff_right.top
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x z : WithTop α
⊢ x - ⊤ ≤ z ↔ x ≤ z + ⊤
[PROOFSTEP]
simp
[GOAL]
case tsub_le_iff_right.coe
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x z : WithTop α
a✝ : α
⊢ x - ↑a✝ ≤ z ↔ x ≤ z + ↑a✝
[PROOFSTEP]
induction x using WithTop.recTopCoe
[GOAL]
case tsub_le_iff_right.coe.top
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
z : WithTop α
a✝ : α
⊢ ⊤ - ↑a✝ ≤ z ↔ ⊤ ≤ z + ↑a✝
[PROOFSTEP]
simp
[GOAL]
case tsub_le_iff_right.coe.coe
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
z : WithTop α
a✝¹ a✝ : α
⊢ ↑a✝ - ↑a✝¹ ≤ z ↔ ↑a✝ ≤ z + ↑a✝¹
[PROOFSTEP]
induction z using WithTop.recTopCoe
[GOAL]
case tsub_le_iff_right.coe.coe.top
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝¹ a✝ : α
⊢ ↑a✝ - ↑a✝¹ ≤ ⊤ ↔ ↑a✝ ≤ ⊤ + ↑a✝¹
[PROOFSTEP]
simp
[GOAL]
case tsub_le_iff_right.coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝² a✝¹ a✝ : α
⊢ ↑a✝¹ - ↑a✝² ≤ ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝ + ↑a✝²
[PROOFSTEP]
norm_cast
[GOAL]
case tsub_le_iff_right.coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝² a✝¹ a✝ : α
⊢ a✝¹ - a✝² ≤ a✝ ↔ a✝¹ ≤ a✝ + a✝²
[PROOFSTEP]
exact tsub_le_iff_right


[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : OrderedSemiring S
abv f g : AbsoluteValue R S
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : OrderedSemiring S
abv g : AbsoluteValue R S
toFun✝ : R → S
map_mul'✝ : ∀ (x y : R), toFun✝ (x * y) = toFun✝ x * toFun✝ y
nonneg'✝ : ∀ (x : R), 0 ≤ MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } x
eq_zero'✝ : ∀ (x : R), MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } x = 0 ↔ x = 0
add_le'✝ :
  ∀ (x y : R),
    MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } (x + y) ≤
      MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } x +
        MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } y
h :
  (fun f => f.toFun)
      { toMulHom := { toFun := toFun✝, map_mul' := map_mul'✝ }, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝,
        add_le' := add_le'✝ } =
    (fun f => f.toFun) g
⊢ { toMulHom := { toFun := toFun✝, map_mul' := map_mul'✝ }, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝,
      add_le' := add_le'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : OrderedSemiring S
abv : AbsoluteValue R S
toFun✝¹ : R → S
map_mul'✝¹ : ∀ (x y : R), toFun✝¹ (x * y) = toFun✝¹ x * toFun✝¹ y
nonneg'✝¹ : ∀ (x : R), 0 ≤ MulHom.toFun { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } x
eq_zero'✝¹ : ∀ (x : R), MulHom.toFun { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } x = 0 ↔ x = 0
add_le'✝¹ :
  ∀ (x y : R),
    MulHom.toFun { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } (x + y) ≤
      MulHom.toFun { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } x +
        MulHom.toFun { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } y
toFun✝ : R → S
map_mul'✝ : ∀ (x y : R), toFun✝ (x * y) = toFun✝ x * toFun✝ y
nonneg'✝ : ∀ (x : R), 0 ≤ MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } x
eq_zero'✝ : ∀ (x : R), MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } x = 0 ↔ x = 0
add_le'✝ :
  ∀ (x y : R),
    MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } (x + y) ≤
      MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } x +
        MulHom.toFun { toFun := toFun✝, map_mul' := map_mul'✝ } y
h :
  (fun f => f.toFun)
      { toMulHom := { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }, nonneg' := nonneg'✝¹, eq_zero' := eq_zero'✝¹,
        add_le' := add_le'✝¹ } =
    (fun f => f.toFun)
      { toMulHom := { toFun := toFun✝, map_mul' := map_mul'✝ }, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝,
        add_le' := add_le'✝ }
⊢ { toMulHom := { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }, nonneg' := nonneg'✝¹, eq_zero' := eq_zero'✝¹,
      add_le' := add_le'✝¹ } =
    { toMulHom := { toFun := toFun✝, map_mul' := map_mul'✝ }, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝,
      add_le' := add_le'✝ }
[PROOFSTEP]
congr
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : OrderedSemiring S
abv : AbsoluteValue R S
h : IsLeftRegular (↑abv 1)
⊢ (fun x => ↑abv 1 * x) (↑abv 1) = (fun x => ↑abv 1 * x) 1
[PROOFSTEP]
simp [← abv.map_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : OrderedSemiring S
abv : AbsoluteValue R S
a b c : R
⊢ ↑abv (a - c) ≤ ↑abv (a - b) + ↑abv (b - c)
[PROOFSTEP]
simpa [sub_eq_add_neg, add_assoc] using abv.add_le (a - b) (b - c)
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : OrderedRing S
abv : AbsoluteValue R S
a b : R
⊢ ↑abv a ≤ ↑abv (a - b) + ↑abv b
[PROOFSTEP]
simpa using abv.add_le (a - b) b
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
⊢ ↑abv (-a) = ↑abv a
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : a = 0
⊢ ↑abv (-a) = ↑abv a
[PROOFSTEP]
simp [ha]
[GOAL]
case neg
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ↑abv (-a) = ↑abv a
[PROOFSTEP]
refine' (mul_self_eq_mul_self_iff.mp (by rw [← abv.map_mul, neg_mul_neg, abv.map_mul])).resolve_right _
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ↑abv (-a) * ↑abv (-a) = ↑abv a * ↑abv a
[PROOFSTEP]
rw [← abv.map_mul, neg_mul_neg, abv.map_mul]
[GOAL]
case neg
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ¬↑abv (-a) = -↑abv a
[PROOFSTEP]
exact ((neg_lt_zero.mpr (abv.pos ha)).trans (abv.pos (neg_ne_zero.mpr ha))).ne'
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a b : R
⊢ ↑abv (a - b) = ↑abv (b - a)
[PROOFSTEP]
rw [← neg_sub, abv.map_neg]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
a b : R
⊢ ↑abv b - ↑abv a ≤ ↑abv (a - b)
[PROOFSTEP]
rw [abv.map_sub]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
a b : R
⊢ ↑abv b - ↑abv a ≤ ↑abv (b - a)
[PROOFSTEP]
apply abv.le_sub
[GOAL]
S : Type u_1
inst✝² : OrderedRing S
R : Type u_2
inst✝¹ : Ring R
abv : R → S
inst✝ : IsAbsoluteValue abv
a b c : R
⊢ abv (a - c) ≤ abv (a - b) + abv (b - c)
[PROOFSTEP]
simpa [sub_eq_add_neg, add_assoc] using abv_add abv (a - b) (b - c)