internlm/Lean-Github huggingface dataset:
Theorem: Weight.dom_of_dom_perm'
Proof 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 _
Proof 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)))))
Theorem: Weight.dom_of_dom_perm'
Proof 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))))
Proof 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)))))
Theorem: Weight.dom_of_dom_perm'
Proof 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]
Proof state after:
no goals
Theorem: Weight.dom_of_dom_perm'
Proof 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 _)
Proof 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))))
Theorem: Weight.dom_of_dom_perm'
Proof 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
Proof state after:
no goals
Theorem: Weight.dom_of_dom_perm'
Proof 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]
Proof 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)))
Theorem: Weight.dom_of_dom_perm'
Proof 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']
Proof 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)))
Theorem: Weight.dom_of_dom_perm'
Proof 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]
Proof 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)))
Theorem: Weight.dom_of_dom_perm'
Proof 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
Proof state after:
no goals
Theorem: Weight.M_is_complete
Proof state before:
n d : ℕ
inst✝ : NeZero d
⊢ complete_set (M n d)
Tactic:
intro w
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ normalized w → ∃ w' ∈ M n d, w' ≤ w
Theorem: Weight.M_is_complete
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ normalized w → ∃ w' ∈ M n d, w' ≤ w
Tactic:
refine WellFoundedLT.induction (α := Weight n d)
  (C := fun w ↦ normalized w → ∃ w', w' ∈ M n d ∧ w' ≤ w) w (fun w₁ h ↦ ?_)
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
⊢ (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) w₁
Theorem: Weight.M_is_complete
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
⊢ (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) w₁
Tactic:
intro hw₁n
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Theorem: Weight.M_is_complete
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Tactic:
by_cases hw₁ : ∃ w₂ : Weight n d, w₂.normalized ∧ w₂ < w₁
Proof state after:
case pos
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∃ w₂, normalized w₂ ∧ w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁

case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ¬∃ w₂, normalized w₂ ∧ w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Theorem: Weight.M_is_complete
Proof state before:
case pos
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∃ w₂, normalized w₂ ∧ w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Tactic:
obtain ⟨w₂, hw₂n, hw₂⟩ := hw₁
Proof state after:
case pos.intro.intro
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
w₂ : Weight n d
hw₂n : normalized w₂
hw₂ : w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Theorem: Weight.M_is_complete
Proof state before:
case pos.intro.intro
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
w₂ : Weight n d
hw₂n : normalized w₂
hw₂ : w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Tactic:
obtain ⟨w', hw'₁, hw'₂⟩ := h w₂ hw₂ hw₂n
Proof state after:
case pos.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
w₂ : Weight n d
hw₂n : normalized w₂
hw₂ : w₂ < w₁
w' : Weight n d
hw'₁ : w' ∈ M n d
hw'₂ : w' ≤ w₂
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Theorem: Weight.M_is_complete
Proof state before:
case pos.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
w₂ : Weight n d
hw₂n : normalized w₂
hw₂ : w₂ < w₁
w' : Weight n d
hw'₁ : w' ∈ M n d
hw'₂ : w' ≤ w₂
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Tactic:
exact ⟨w', hw'₁, hw'₂.trans <| le_of_lt hw₂⟩
Proof state after:
no goals
Theorem: Weight.M_is_complete
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ¬∃ w₂, normalized w₂ ∧ w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Tactic:
push_neg at hw₁
Proof state after:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Theorem: Weight.M_is_complete
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
Tactic:
refine ⟨w₁, ⟨hw₁n, fun w' hw' h' ↦ ?_⟩, le_refl w₁⟩
Proof state after:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
⊢ w₁ ≤ w'
Theorem: Weight.M_is_complete
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
⊢ w₁ ≤ w'
Tactic:
by_contra hf
Proof state after:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
⊢ False
Theorem: Weight.M_is_complete
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
⊢ False
Tactic:
have := hw₁ w' hw'
Proof state after:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
this : ¬w' < w₁
⊢ False
Theorem: Weight.M_is_complete
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
this : ¬w' < w₁
⊢ False
Tactic:
rw [lt_iff_le_not_le] at this
Proof state after:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
this : ¬(w' ≤ w₁ ∧ ¬w₁ ≤ w')
⊢ False
Theorem: Weight.M_is_complete
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
this : ¬(w' ≤ w₁ ∧ ¬w₁ ≤ w')
⊢ False
Tactic:
push_neg at this
Proof state after:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
this : w' ≤ w₁ → w₁ ≤ w'
⊢ False
Theorem: Weight.M_is_complete
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
this : w' ≤ w₁ → w₁ ≤ w'
⊢ False
Tactic:
exact hf (this h')
Proof state after:
no goals
Theorem: Weight.M_is_unique
Proof state before:
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
⊢ S = M n d
Tactic:
ext w
Proof state after:
case h
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
⊢ w ∈ S ↔ w ∈ M n d
Theorem: Weight.M_is_unique
Proof state before:
case h
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
⊢ w ∈ S ↔ w ∈ M n d
Tactic:
refine ⟨fun h ↦ ⟨hS₁ w h, fun w' hw'₁ hw'₂ ↦ ?_⟩, fun h ↦ ?_⟩
Proof state after:
case h.refine_1
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
h : w ∈ S
w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
⊢ w ≤ w'

case h.refine_2
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
h : w ∈ M n d
⊢ w ∈ S
Theorem: Weight.M_is_unique
Proof state before:
case h.refine_1
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
h : w ∈ S
w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
⊢ w ≤ w'
Tactic:
obtain ⟨w₁, hw₁, hle⟩ := hS₂.1 w' hw'₁
Proof state after:
case h.refine_1.intro.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
h : w ∈ S
w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
w₁ : Weight n d
hw₁ : w₁ ∈ S
hle : w₁ ≤ w'
⊢ w ≤ w'
Theorem: Weight.M_is_unique
Proof state before:
case h.refine_1.intro.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
h : w ∈ S
w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
w₁ : Weight n d
hw₁ : w₁ ∈ S
hle : w₁ ≤ w'
⊢ w ≤ w'
Tactic:
exact le_of_eq_of_le (hS₂.2 w₁ w hw₁ h (hle.trans hw'₂)).symm hle
Proof state after:
no goals
Theorem: Weight.M_is_unique
Proof state before:
case h.refine_2
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
h : w ∈ M n d
⊢ w ∈ S
Tactic:
obtain ⟨hw₁, hw₂⟩ := h
Proof state after:
case h.refine_2.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
⊢ w ∈ S
Theorem: Weight.M_is_unique
Proof state before:
case h.refine_2.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
⊢ w ∈ S
Tactic:
obtain ⟨w', hw'₁, hw'₂⟩ := hS₂.1 w hw₁
Proof state after:
case h.refine_2.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw'₁ : w' ∈ S
hw'₂ : w' ≤ w
⊢ w ∈ S
Theorem: Weight.M_is_unique
Proof state before:
case h.refine_2.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw'₁ : w' ∈ S
hw'₂ : w' ≤ w
⊢ w ∈ S
Tactic:
suffices heq : w' = w
Proof state after:
case h.refine_2.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw'₁ : w' ∈ S
hw'₂ : w' ≤ w
heq : w' = w
⊢ w ∈ S

case heq
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw'₁ : w' ∈ S
hw'₂ : w' ≤ w
⊢ w' = w
Theorem: Weight.M_is_unique
Proof state before:
case heq
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw'₁ : w' ∈ S
hw'₂ : w' ≤ w
⊢ w' = w
Tactic:
exact eq_of_dom_and_min' (hS₁ w' hw'₁) hw₁ (hw₂ w' (hS₁ w' hw'₁) hw'₂)
                         (fun u hu₁ hu₂ ↦ hw'₂.trans (hw₂ u hu₁ (hu₂.trans hw'₂)))
Proof state after:
no goals
Theorem: Weight.M_is_unique
Proof state before:
case h.refine_2.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw'₁ : w' ∈ S
hw'₂ : w' ≤ w
heq : w' = w
⊢ w ∈ S
Tactic:
exact heq ▸ hw'₁
Proof state after:
no goals
Theorem: Weight.not_in_M_of_dom_ne
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : ∃ w', normalized w' ∧ w' ≤ w ∧ w' ≠ w
⊢ w ∉ M n d
Tactic:
obtain ⟨w', hw'₁, hw'₂, hw'₃⟩ := hw
Proof state after:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
hw'₃ : w' ≠ w
⊢ w ∉ M n d
Theorem: Weight.not_in_M_of_dom_ne
Proof state before:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
hw'₃ : w' ≠ w
⊢ w ∉ M n d
Tactic:
by_contra! hf
Proof state after:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
hw'₃ : w' ≠ w
hf : w ∈ M n d
⊢ False
Theorem: Weight.not_in_M_of_dom_ne
Proof state before:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
hw'₃ : w' ≠ w
hf : w ∈ M n d
⊢ False
Tactic:
exact hw'₃ (eq_of_dom_in_M hw'₁ hw'₂ hf)
Proof state after:
no goals
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
⊢ Finset.gcd Finset.univ w = 1
Tactic:
set g := Finset.univ.gcd w
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
⊢ g = 1
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
⊢ g = 1
Tactic:
by_contra hfg
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
⊢ False
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
⊢ False
Tactic:
have hg : 1 < g
Proof state after:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
⊢ 1 < g

n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
⊢ False
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
⊢ False
Tactic:
let w' : Weight n d := fun i ↦ (w i) / g
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
⊢ False
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
⊢ False
Tactic:
have hww' : w = g • w'
Proof state after:
case hww'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
⊢ w = g • w'

n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
⊢ False
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
⊢ False
Tactic:
have hww'i i : w i = g * w' i := congrFun hww' i
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ False