Theorem: Weight.dom_of_dom_perm' (Weights/Uniqueness.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ sorted w ≤ w'
Tactic:
convert dom_of_dom_perm (sorted_is_Monotone w) ((dom_perm w w' (Tuple.sort w)).mpr hd)
State after:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' = sorted (Weight.comp w' (Tuple.sort w))

State before:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' = sorted (Weight.comp w' (Tuple.sort w))
Tactic:
rw [sorted, comp_comp]
State after:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' = Weight.comp w' (Tuple.sort w * Tuple.sort (Weight.comp w' (Tuple.sort w)))

State before:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' = Weight.comp w' (Tuple.sort w * Tuple.sort (Weight.comp w' (Tuple.sort w)))
Tactic:
have help : w' = w'.comp (Tuple.sort w') ↔ Monotone w'
State after:
case help
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'

case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
⊢ w' = Weight.comp w' (Tuple.sort w * Tuple.sort (Weight.comp w' (Tuple.sort w)))

State before:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
⊢ w' = Weight.comp w' (Tuple.sort w * Tuple.sort (Weight.comp w' (Tuple.sort w)))
Tactic:
rw [help.mpr hw', comp_comp, eq_comm]
State after:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
⊢ Weight.comp w'
      (Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))) =
    Weight.comp w' (Tuple.sort w')

State before:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
⊢ Weight.comp w'
      (Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))) =
    Weight.comp w' (Tuple.sort w')
Tactic:
apply Tuple.comp_sort_eq_comp_iff_monotone.mpr
State after:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
⊢ Monotone
    (w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))))

State before:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
⊢ Monotone
    (w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))))
Tactic:
let w'' := (w'.comp (Tuple.sort w)).comp (Tuple.sort (w'.comp (Tuple.sort w)))
State after:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
⊢ Monotone
    (w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))))

State before:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
⊢ Monotone
    (w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))))
Tactic:
have hw'' : Monotone w'' := sorted_is_Monotone _
State after:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
⊢ Monotone
    (w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))))

State before:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
⊢ Monotone
    (w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))))
Tactic:
have h : w'' = w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w *
                  Tuple.sort ((w'.comp (Tuple.sort w')).comp (Tuple.sort w))))
State after:
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
⊢ w'' =
    w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w))))

case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
h :
  w'' =
    w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w))))
⊢ Monotone
    (w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))))

State before:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
h :
  w'' =
    w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w))))
⊢ Monotone
    (w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))))
Tactic:
rwa [← h]
State after:
no goals

State before:
case help
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
Tactic:
change w' ∘ Equiv.refl _ = _ ↔ Monotone (w' ∘ Equiv.refl _)
State after:
case help
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' ∘ ⇑(Equiv.refl (Fin (Nat.succ n))) = Weight.comp w' (Tuple.sort w') ↔
    Monotone (w' ∘ ⇑(Equiv.refl (Fin (Nat.succ n))))

State before:
case help
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' ∘ ⇑(Equiv.refl (Fin (Nat.succ n))) = Weight.comp w' (Tuple.sort w') ↔
    Monotone (w' ∘ ⇑(Equiv.refl (Fin (Nat.succ n))))
Tactic:
exact Tuple.comp_sort_eq_comp_iff_monotone
State after:
no goals

State before:
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
⊢ w'' =
    w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w))))
Tactic:
simp only [Weight.comp, Equiv.Perm.coe_mul]
State after:
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
⊢ (w' ∘ ⇑(Tuple.sort w)) ∘ ⇑(Tuple.sort (w' ∘ ⇑(Tuple.sort w))) =
    w' ∘ ⇑(Tuple.sort w') ∘ ⇑(Tuple.sort w) ∘ ⇑(Tuple.sort ((w' ∘ ⇑(Tuple.sort w')) ∘ ⇑(Tuple.sort w)))

State before:
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
⊢ (w' ∘ ⇑(Tuple.sort w)) ∘ ⇑(Tuple.sort (w' ∘ ⇑(Tuple.sort w))) =
    w' ∘ ⇑(Tuple.sort w') ∘ ⇑(Tuple.sort w) ∘ ⇑(Tuple.sort ((w' ∘ ⇑(Tuple.sort w')) ∘ ⇑(Tuple.sort w)))
Tactic:
rw [← Function.comp.assoc w' (Tuple.sort w'), Tuple.sort_eq_refl_iff_monotone.mpr hw']
State after:
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
⊢ (w' ∘ ⇑(Tuple.sort w)) ∘ ⇑(Tuple.sort (w' ∘ ⇑(Tuple.sort w))) =
    (w' ∘ ⇑(Equiv.refl (Fin (Nat.succ n)))) ∘
      ⇑(Tuple.sort w) ∘ ⇑(Tuple.sort ((w' ∘ ⇑(Equiv.refl (Fin (Nat.succ n)))) ∘ ⇑(Tuple.sort w)))

State before:
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
⊢ (w' ∘ ⇑(Tuple.sort w)) ∘ ⇑(Tuple.sort (w' ∘ ⇑(Tuple.sort w))) =
    (w' ∘ ⇑(Equiv.refl (Fin (Nat.succ n)))) ∘
      ⇑(Tuple.sort w) ∘ ⇑(Tuple.sort ((w' ∘ ⇑(Equiv.refl (Fin (Nat.succ n)))) ∘ ⇑(Tuple.sort w)))
Tactic:
simp only [Equiv.coe_refl, Function.comp_id]
State after:
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
⊢ (w' ∘ ⇑(Tuple.sort w)) ∘ ⇑(Tuple.sort (w' ∘ ⇑(Tuple.sort w))) =
    w' ∘ ⇑(Tuple.sort w) ∘ ⇑(Tuple.sort (w' ∘ ⇑(Tuple.sort w)))

State before:
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
hw'' : Monotone w''
⊢ (w' ∘ ⇑(Tuple.sort w)) ∘ ⇑(Tuple.sort (w' ∘ ⇑(Tuple.sort w))) =
    w' ∘ ⇑(Tuple.sort w) ∘ ⇑(Tuple.sort (w' ∘ ⇑(Tuple.sort w)))
Tactic:
rfl
State after:
no goals