Theorem: Weight.min_Monotone_iff_min_normalized (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ (∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w') ↔ ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
Tactic:
refine ⟨fun h w' hw' hle ↦ h _ hw'.2 hle, fun h w' hw' hle ↦ ?_⟩
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw' : Monotone w'
hle : w' ≤ w
⊢ w ≤ w'

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw' : Monotone w'
hle : w' ≤ w
⊢ w ≤ w'
Tactic:
obtain ⟨k, wr, hwr₁, hwr₂⟩ := normalized_of_Monotone hw'
State after:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw' : Monotone w'
hle : w' ≤ w
k : ℕ
wr : Weight n d
hwr₁ : w' = wr + k • 1
hwr₂ : normalized wr
⊢ w ≤ w'

State before:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw' : Monotone w'
hle : w' ≤ w
k : ℕ
wr : Weight n d
hwr₁ : w' = wr + k • 1
hwr₂ : normalized wr
⊢ w ≤ w'
Tactic:
have h₁ := le_of_le_of_eq (dom_dom_of_shift wr k).1 hwr₁.symm
State after:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw' : Monotone w'
hle : w' ≤ w
k : ℕ
wr : Weight n d
hwr₁ : w' = wr + k • 1
hwr₂ : normalized wr
h₁ : wr ≤ w'
⊢ w ≤ w'

State before:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw' : Monotone w'
hle : w' ≤ w
k : ℕ
wr : Weight n d
hwr₁ : w' = wr + k • 1
hwr₂ : normalized wr
h₁ : wr ≤ w'
⊢ w ≤ w'
Tactic:
exact (h wr hwr₂ (h₁.trans hle)).trans h₁
State after:
no goals