internlm/Lean-Github huggingface dataset:
Theorem: Weight.BasicInterval.feasible_left_or_right
Proof state before:
case neg
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h' : ¬(I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂)
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂
Tactic:
simp only [not_and_or, not_le, not_lt] at h'
Proof state after:
case neg
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h' : Nat.succ d < I.a₁ + I.b₁ ∨ Nat.succ d < I.a₂ + I.b₂ ∨ I.a₁ + I.a₂ + I.b₁ + I.b₂ ≤ Nat.succ d
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂
Theorem: Weight.BasicInterval.feasible_left_or_right
Proof state before:
case neg
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h' : Nat.succ d < I.a₁ + I.b₁ ∨ Nat.succ d < I.a₂ + I.b₂ ∨ I.a₁ + I.a₂ + I.b₁ + I.b₂ ≤ Nat.succ d
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂
Tactic:
rcases h' with _ | _ | _ <;> try exfalso; linarith
Proof state after:
case neg.inr.inr
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h✝ : I.a₁ + I.a₂ + I.b₁ + I.b₂ ≤ Nat.succ d
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂
Theorem: Weight.BasicInterval.feasible_left_or_right
Proof state before:
case neg.inr.inr
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h✝ : I.a₁ + I.a₂ + I.b₁ + I.b₂ ≤ Nat.succ d
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂
Tactic:
refine Or.inr ⟨⟨?_, ?_, ?_⟩, ⟨?_, ?_, ?_⟩⟩ <;> simp <;> linarith
Proof state after:
no goals
Theorem: Weight.BasicInterval.feasible_left_or_right
Proof state before:
case neg.inr.inr
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h✝ : I.a₁ + I.a₂ + I.b₁ + I.b₂ ≤ Nat.succ d
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂
Tactic:
exfalso
Proof state after:
case neg.inr.inr
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h✝ : I.a₁ + I.a₂ + I.b₁ + I.b₂ ≤ Nat.succ d
⊢ False
Theorem: Weight.BasicInterval.feasible_left_or_right
Proof state before:
case neg.inr.inl
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h✝ : Nat.succ d < I.a₂ + I.b₂
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_feasible
Proof state before:
d a b : ℕ
inst✝ : NeZero d
⊢ ∃ I, feasible d I ∧ mem a b I
Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne d)
Proof state after:
case intro
a b n : ℕ
inst✝ : NeZero (Nat.succ n)
⊢ ∃ I, feasible (Nat.succ n) I ∧ mem a b I
Theorem: Weight.BasicInterval.mem_feasible
Proof state before:
case intro
a b n : ℕ
inst✝ : NeZero (Nat.succ n)
⊢ ∃ I, feasible (Nat.succ n) I ∧ mem a b I
Tactic:
induction' n with n ih
Proof state after:
case intro.zero
a b n : ℕ
inst✝ : NeZero (Nat.succ n)
⊢ ∃ I, feasible (Nat.succ Nat.zero) I ∧ mem a b I

case intro.succ
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
ih : ∃ I, feasible (Nat.succ n) I ∧ mem a b I
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
Theorem: Weight.BasicInterval.mem_feasible
Proof state before:
case intro.zero
a b n : ℕ
inst✝ : NeZero (Nat.succ n)
⊢ ∃ I, feasible (Nat.succ Nat.zero) I ∧ mem a b I
Tactic:
exact ⟨base, feasible_base, mem_base _ _⟩
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_feasible
Proof state before:
case intro.succ
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
ih : ∃ I, feasible (Nat.succ n) I ∧ mem a b I
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
Tactic:
obtain ⟨I', hf, hm⟩ := ih
Proof state after:
case intro.succ.intro.intro
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm : mem a b I'
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
Theorem: Weight.BasicInterval.mem_feasible
Proof state before:
case intro.succ.intro.intro.inl
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm : mem a b I'
h : feasible (Nat.succ (Nat.succ n)) I'
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
Tactic:
exact ⟨I', h, hm⟩
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_feasible
Proof state before:
case intro.succ.intro.intro.inr
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm : mem a b I'
h : feasible (Nat.succ (Nat.succ n)) (left I') ∧ feasible (Nat.succ (Nat.succ n)) (right I')
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
Tactic:
rcases mem_left_or_mem_right I' hm with hm | hm
Proof state after:
case intro.succ.intro.intro.inr.inl
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm✝ : mem a b I'
h : feasible (Nat.succ (Nat.succ n)) (left I') ∧ feasible (Nat.succ (Nat.succ n)) (right I')
hm : mem a b (left I')
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I

case intro.succ.intro.intro.inr.inr
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm✝ : mem a b I'
h : feasible (Nat.succ (Nat.succ n)) (left I') ∧ feasible (Nat.succ (Nat.succ n)) (right I')
hm : mem a b (right I')
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
Theorem: Weight.BasicInterval.mem_feasible
Proof state before:
case intro.succ.intro.intro.inr.inl
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm✝ : mem a b I'
h : feasible (Nat.succ (Nat.succ n)) (left I') ∧ feasible (Nat.succ (Nat.succ n)) (right I')
hm : mem a b (left I')
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
Tactic:
exact ⟨I'.left, h.1, hm⟩
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_feasible
Proof state before:
case intro.succ.intro.intro.inr.inr
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm✝ : mem a b I'
h : feasible (Nat.succ (Nat.succ n)) (left I') ∧ feasible (Nat.succ (Nat.succ n)) (right I')
hm : mem a b (right I')
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
Tactic:
exact ⟨I'.right, h.2, hm⟩
Proof state after:
no goals
Theorem: Weight.BasicInterval.gt_of_mem_interior_feasible
Proof state before:
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
⊢ d < a + b
Tactic:
obtain ⟨k₁, k₂, hk₁, hk₂, h₁, h₂⟩ := exists_of_mem_interior hab
Proof state after:
case intro.intro.intro.intro.intro
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ d < a + b
Theorem: Weight.BasicInterval.gt_of_mem_interior_feasible
Proof state before:
case intro.intro.intro.intro.intro
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ d < a + b
Tactic:
calc
  d < I.a₁ + I.a₂ + I.b₁ + I.b₂                       := hI.2.2
  _ = I.a₁ + I.b₁ + (I.a₂ + I.b₂)                     := by abel
  _ ≤ k₁ * (I.a₁ + I.b₁) + k₂ * (I.a₂ + I.b₂)         :=
    Nat.add_le_add (Nat.le_mul_of_pos_left _ hk₁) (Nat.le_mul_of_pos_left _ hk₂)
  _ = k₁ * I.a₁ + k₂ * I.a₂ + (k₁ * I.b₁ + k₂ * I.b₂) := by ring
  _ = a + b                                           := by rw [h₁, h₂]
Proof state after:
no goals
Theorem: Weight.BasicInterval.gt_of_mem_interior_feasible
Proof state before:
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ I.a₁ + I.a₂ + I.b₁ + I.b₂ = I.a₁ + I.b₁ + (I.a₂ + I.b₂)
Tactic:
abel
Proof state after:
no goals
Theorem: Weight.BasicInterval.gt_of_mem_interior_feasible
Proof state before:
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ k₁ * (I.a₁ + I.b₁) + k₂ * (I.a₂ + I.b₂) = k₁ * I.a₁ + k₂ * I.a₂ + (k₁ * I.b₁ + k₂ * I.b₂)
Tactic:
ring
Proof state after:
no goals
Theorem: Weight.BasicInterval.gt_of_mem_interior_feasible
Proof state before:
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ k₁ * I.a₁ + k₂ * I.a₂ + (k₁ * I.b₁ + k₂ * I.b₂) = a + b
Tactic:
rw [h₁, h₂]
Proof state after:
no goals
Theorem: Weight.pair'_of_fraction
Proof state before:
d a b : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ pair' (of_fraction d a b) z = ↑a * z 2 + ↑b * (z 1 + z 2)
Tactic:
simp only [pair', of_fraction, Fin.sum_univ_three, cons_val_zero, cons_val_one, head_cons,
  cons_val_two, tail_cons, Nat.cast_add]
Proof state after:
d a b : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ z 0 * ↑0 + z 1 * ↑b + z 2 * (↑a + ↑b) = ↑a * z 2 + ↑b * (z 1 + z 2)
Theorem: Weight.pair'_of_fraction
Proof state before:
d a b : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ z 0 * ↑0 + z 1 * ↑b + z 2 * (↑a + ↑b) = ↑a * z 2 + ↑b * (z 1 + z 2)
Tactic:
ring
Proof state after:
no goals
Theorem: Weight.pair'_of_fraction_add
Proof state before:
d a₁ b₁ a₂ b₂ : ℕ
⊢ pair' (of_fraction d (a₁ + a₂) (b₁ + b₂)) = pair' (of_fraction d a₁ b₁) + pair' (of_fraction d a₂ b₂)
Tactic:
ext z
Proof state after:
case h
d a₁ b₁ a₂ b₂ : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ pair' (of_fraction d (a₁ + a₂) (b₁ + b₂)) z = (pair' (of_fraction d a₁ b₁) + pair' (of_fraction d a₂ b₂)) z
Theorem: Weight.pair'_of_fraction_add
Proof state before:
case h
d a₁ b₁ a₂ b₂ : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ pair' (of_fraction d (a₁ + a₂) (b₁ + b₂)) z = (pair' (of_fraction d a₁ b₁) + pair' (of_fraction d a₂ b₂)) z
Tactic:
simp_rw [Pi.add_apply, pair'_of_fraction, Nat.cast_add]
Proof state after:
case h
d a₁ b₁ a₂ b₂ : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ (↑a₁ + ↑a₂) * z 2 + (↑b₁ + ↑b₂) * (z 1 + z 2) = ↑a₁ * z 2 + ↑b₁ * (z 1 + z 2) + (↑a₂ * z 2 + ↑b₂ * (z 1 + z 2))
Theorem: Weight.pair'_of_fraction_add
Proof state before:
case h
d a₁ b₁ a₂ b₂ : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ (↑a₁ + ↑a₂) * z 2 + (↑b₁ + ↑b₂) * (z 1 + z 2) = ↑a₁ * z 2 + ↑b₁ * (z 1 + z 2) + (↑a₂ * z 2 + ↑b₂ * (z 1 + z 2))
Tactic:
ring
Proof state after:
no goals
Theorem: Weight.pair'_of_fraction_mul
Proof state before:
d a b k : ℕ
z : Fin 3 → ℤ
⊢ pair' (of_fraction d (k * a) (k * b)) z = ↑k * pair' (of_fraction d a b) z
Tactic:
simp_rw [pair'_of_fraction, Nat.cast_mul]
Proof state after:
d a b k : ℕ
z : Fin 3 → ℤ
⊢ ↑k * ↑a * z 2 + ↑k * ↑b * (z 1 + z 2) = ↑k * (↑a * z 2 + ↑b * (z 1 + z 2))
Theorem: Weight.pair'_of_fraction_mul
Proof state before:
d a b k : ℕ
z : Fin 3 → ℤ
⊢ ↑k * ↑a * z 2 + ↑k * ↑b * (z 1 + z 2) = ↑k * (↑a * z 2 + ↑b * (z 1 + z 2))
Tactic:
ring
Proof state after:
no goals
Theorem: Weight.ex_of_fraction
Proof state before:
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ ∃ a b, w = of_fraction d a b
Tactic:
refine ⟨w 2 - w 1, w 1, funext <| fun i ↦ ?_⟩
Proof state after:
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
i : Fin (Nat.succ 2)
⊢ w i = of_fraction d (w 2 - w 1) (w 1) i
Theorem: Weight.ex_of_fraction
Proof state before:
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
i : Fin (Nat.succ 2)
⊢ w i = of_fraction d (w 2 - w 1) (w 1) i
Tactic:
fin_cases i
Proof state after:
case head
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ w { val := 0, isLt := (_ : 0 < Nat.succ 2) } =
    of_fraction d (w 2 - w 1) (w 1) { val := 0, isLt := (_ : 0 < Nat.succ 2) }

case tail.head
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ w { val := 1, isLt := (_ : (fun a => a < Nat.succ 2) 1) } =
    of_fraction d (w 2 - w 1) (w 1) { val := 1, isLt := (_ : (fun a => a < Nat.succ 2) 1) }

case tail.tail.head
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ w { val := 2, isLt := (_ : (fun a => (fun a => a < Nat.succ 2) a) 2) } =
    of_fraction d (w 2 - w 1) (w 1) { val := 2, isLt := (_ : (fun a => (fun a => a < Nat.succ 2) a) 2) }
Theorem: Weight.ex_of_fraction
Proof state before:
case head
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ w { val := 0, isLt := (_ : 0 < Nat.succ 2) } =
    of_fraction d (w 2 - w 1) (w 1) { val := 0, isLt := (_ : 0 < Nat.succ 2) }
Tactic:
simp [of_fraction, h.1]
Proof state after:
no goals
Theorem: Weight.ex_of_fraction
Proof state before:
case tail.head
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ w { val := 1, isLt := (_ : (fun a => a < Nat.succ 2) 1) } =
    of_fraction d (w 2 - w 1) (w 1) { val := 1, isLt := (_ : (fun a => a < Nat.succ 2) 1) }
Tactic:
simp [of_fraction]
Proof state after:
no goals
Theorem: Weight.ex_of_fraction
Proof state before:
case tail.tail.head
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ w { val := 2, isLt := (_ : (fun a => (fun a => a < Nat.succ 2) a) 2) } =
    of_fraction d (w 2 - w 1) (w 1) { val := 2, isLt := (_ : (fun a => (fun a => a < Nat.succ 2) a) 2) }
Tactic:
exact Nat.eq_add_of_sub_eq (h.2 (Fin.coe_sub_iff_le.mp rfl)) rfl
Proof state after:
no goals
Theorem: Weight.normalized_of_of_fraction
Proof state before:
d a b : ℕ
inst✝ : NeZero d
⊢ normalized (of_fraction d a b)
Tactic:
refine ⟨?_, ?_⟩
Proof state after:
case refine_1
d a b : ℕ
inst✝ : NeZero d
⊢ of_fraction d a b 0 = 0

case refine_2
d a b : ℕ
inst✝ : NeZero d
⊢ Monotone (of_fraction d a b)
Theorem: Weight.normalized_of_of_fraction
Proof state before:
case refine_1
d a b : ℕ
inst✝ : NeZero d
⊢ of_fraction d a b 0 = 0
Tactic:
simp [of_fraction]
Proof state after:
no goals
Theorem: Weight.normalized_of_of_fraction
Proof state before:
case refine_2
d a b : ℕ
inst✝ : NeZero d
⊢ Monotone (of_fraction d a b)
Tactic:
have help : ∀ i j : Fin 3, i ≤ j → i = 0 ∨ (i = j) ∨ (i = 1 ∧ j = 2)
Proof state after:
case help
d a b : ℕ
inst✝ : NeZero d
⊢ ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2

case refine_2
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
⊢ Monotone (of_fraction d a b)
Theorem: Weight.normalized_of_of_fraction
Proof state before:
case refine_2
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
⊢ Monotone (of_fraction d a b)
Tactic:
intro i j hij
Proof state after:
case refine_2
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
i j : Fin (Nat.succ 2)
hij : i ≤ j
⊢ of_fraction d a b i ≤ of_fraction d a b j
Theorem: Weight.normalized_of_of_fraction
Proof state before:
case refine_2
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
i j : Fin (Nat.succ 2)
hij : i ≤ j
⊢ of_fraction d a b i ≤ of_fraction d a b j
Tactic:
rcases help i j hij with rfl | rfl | ⟨rfl, rfl⟩
Proof state after:
case refine_2.inl
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
j : Fin (Nat.succ 2)
hij : 0 ≤ j
⊢ of_fraction d a b 0 ≤ of_fraction d a b j

case refine_2.inr.inl
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
i : Fin (Nat.succ 2)
hij : i ≤ i
⊢ of_fraction d a b i ≤ of_fraction d a b i

case refine_2.inr.inr.intro
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
hij : 1 ≤ 2
⊢ of_fraction d a b 1 ≤ of_fraction d a b 2
Theorem: Weight.normalized_of_of_fraction
Proof state before:
case help
d a b : ℕ
inst✝ : NeZero d
⊢ ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
Tactic:
decide
Proof state after:
no goals
Theorem: Weight.normalized_of_of_fraction
Proof state before:
case refine_2.inl
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
j : Fin (Nat.succ 2)
hij : 0 ≤ j
⊢ of_fraction d a b 0 ≤ of_fraction d a b j
Tactic:
simp [of_fraction]
Proof state after:
no goals
Theorem: Weight.normalized_of_of_fraction
Proof state before:
case refine_2.inr.inl
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
i : Fin (Nat.succ 2)
hij : i ≤ i
⊢ of_fraction d a b i ≤ of_fraction d a b i
Tactic:
exact le_rfl
Proof state after:
no goals
Theorem: Weight.normalized_of_of_fraction
Proof state before:
case refine_2.inr.inr.intro
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
hij : 1 ≤ 2
⊢ of_fraction d a b 1 ≤ of_fraction d a b 2
Tactic:
simp [of_fraction]
Proof state after:
no goals
Theorem: Weight.mem_S_le_of_proportional
Proof state before:
d g : ℕ
a b : ℤ
hg : 0 < g
h : mem_S_le d (a * ↑g) (b * ↑g)
⊢ mem_S_le d a b
Tactic:
obtain ⟨h₁, i₁, i₂, h₂, h₃, h₄⟩ := h
Proof state after:
case intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
hg : 0 < g
h₁ : 0 < b * ↑g
i₁ i₂ : ℕ
h₂ : 3 * i₁ + 3 * i₂ ≤ 2 * d
h₃ : d < 3 * i₂
h₄ : a * ↑g * (3 * ↑i₂ - ↑d) = b * ↑g * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
⊢ mem_S_le d a b
Theorem: Weight.mem_S_le_of_proportional
Proof state before:
case intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
hg : 0 < g
h₁ : 0 < b * ↑g
i₁ i₂ : ℕ
h₂ : 3 * i₁ + 3 * i₂ ≤ 2 * d
h₃ : d < 3 * i₂
h₄ : a * ↑g * (3 * ↑i₂ - ↑d) = b * ↑g * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
⊢ mem_S_le d a b
Tactic:
simp_rw [mul_comm _ (g : ℤ), mul_assoc] at h₄
Proof state after:
case intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
hg : 0 < g
h₁ : 0 < b * ↑g
i₁ i₂ : ℕ
h₂ : 3 * i₁ + 3 * i₂ ≤ 2 * d
h₃ : d < 3 * i₂
h₄ : ↑g * (a * (3 * ↑i₂ - ↑d)) = ↑g * (b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ mem_S_le d a b
Theorem: Weight.mem_S_le_of_proportional
Proof state before:
case intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
hg : 0 < g
h₁ : 0 < b * ↑g
i₁ i₂ : ℕ
h₂ : 3 * i₁ + 3 * i₂ ≤ 2 * d
h₃ : d < 3 * i₂
h₄ : ↑g * (a * (3 * ↑i₂ - ↑d)) = ↑g * (b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ mem_S_le d a b
Tactic:
replace hg : (0 : ℤ) < g := Nat.cast_pos.mpr hg
Proof state after:
case intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
h₁ : 0 < b * ↑g
i₁ i₂ : ℕ
h₂ : 3 * i₁ + 3 * i₂ ≤ 2 * d
h₃ : d < 3 * i₂
h₄ : ↑g * (a * (3 * ↑i₂ - ↑d)) = ↑g * (b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
hg : 0 < ↑g
⊢ mem_S_le d a b
Theorem: Weight.mem_S_le_of_proportional
Proof state before:
case intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
h₁ : 0 < b * ↑g
i₁ i₂ : ℕ
h₂ : 3 * i₁ + 3 * i₂ ≤ 2 * d
h₃ : d < 3 * i₂
h₄ : ↑g * (a * (3 * ↑i₂ - ↑d)) = ↑g * (b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
hg : 0 < ↑g
⊢ mem_S_le d a b
Tactic:
exact ⟨(mul_pos_iff_of_pos_right hg).mp h₁, i₁, i₂, h₂, h₃, Int.eq_of_mul_eq_mul_left hg.ne' h₄⟩
Proof state after:
no goals
Theorem: Weight.mem_S_ge_of_proportional
Proof state before:
d g : ℕ
a b : ℤ
hg : 0 < g
h : mem_S_ge d (a * ↑g) (b * ↑g)
⊢ mem_S_ge d a b
Tactic:
obtain ⟨h₁, i₁, i₂, h', h₂, h₃, h₄⟩ := h
Proof state after:
case intro.intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
hg : 0 < g
h₁ : 0 < a * ↑g
i₁ i₂ : ℕ
h' : i₁ + i₂ ≤ d
h₂ : 2 * d < 3 * i₁ + 3 * i₂
h₃ : 3 * i₂ ≤ d
h₄ : a * ↑g * (3 * ↑i₂ - ↑d) = b * ↑g * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
⊢ mem_S_ge d a b
Theorem: Weight.mem_S_ge_of_proportional
Proof state before:
case intro.intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
hg : 0 < g
h₁ : 0 < a * ↑g
i₁ i₂ : ℕ
h' : i₁ + i₂ ≤ d
h₂ : 2 * d < 3 * i₁ + 3 * i₂
h₃ : 3 * i₂ ≤ d
h₄ : a * ↑g * (3 * ↑i₂ - ↑d) = b * ↑g * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
⊢ mem_S_ge d a b
Tactic:
simp_rw [mul_comm _ (g : ℤ), mul_assoc] at h₄
Proof state after:
case intro.intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
hg : 0 < g
h₁ : 0 < a * ↑g
i₁ i₂ : ℕ
h' : i₁ + i₂ ≤ d
h₂ : 2 * d < 3 * i₁ + 3 * i₂
h₃ : 3 * i₂ ≤ d
h₄ : ↑g * (a * (3 * ↑i₂ - ↑d)) = ↑g * (b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ mem_S_ge d a b
Theorem: Weight.mem_S_ge_of_proportional
Proof state before:
case intro.intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
hg : 0 < g
h₁ : 0 < a * ↑g
i₁ i₂ : ℕ
h' : i₁ + i₂ ≤ d
h₂ : 2 * d < 3 * i₁ + 3 * i₂
h₃ : 3 * i₂ ≤ d
h₄ : ↑g * (a * (3 * ↑i₂ - ↑d)) = ↑g * (b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ mem_S_ge d a b
Tactic:
replace hg : (0 : ℤ) < g := Nat.cast_pos.mpr hg
Proof state after:
case intro.intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
h₁ : 0 < a * ↑g
i₁ i₂ : ℕ
h' : i₁ + i₂ ≤ d
h₂ : 2 * d < 3 * i₁ + 3 * i₂
h₃ : 3 * i₂ ≤ d
h₄ : ↑g * (a * (3 * ↑i₂ - ↑d)) = ↑g * (b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
hg : 0 < ↑g
⊢ mem_S_ge d a b
Theorem: Weight.mem_S_ge_of_proportional
Proof state before:
case intro.intro.intro.intro.intro.intro
d g : ℕ
a b : ℤ
h₁ : 0 < a * ↑g
i₁ i₂ : ℕ
h' : i₁ + i₂ ≤ d
h₂ : 2 * d < 3 * i₁ + 3 * i₂
h₃ : 3 * i₂ ≤ d
h₄ : ↑g * (a * (3 * ↑i₂ - ↑d)) = ↑g * (b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
hg : 0 < ↑g
⊢ mem_S_ge d a b
Tactic:
exact ⟨(mul_pos_iff_of_pos_right hg).mp h₁, i₁, i₂, h', h₂, h₃,
  Int.eq_of_mul_eq_mul_left hg.ne' h₄⟩
Proof state after:
no goals
Theorem: Weight.not_eq_neg_self
Proof state before:
d : ℕ
hd : ↑d ≠ 0
⊢ -↑d ≠ ↑d
Tactic:
have hch : ringChar (ZMod 3) ≠ 2 := by rw [ZMod.ringChar_zmod_n]; norm_num
Proof state after:
d : ℕ
hd : ↑d ≠ 0
hch : ringChar (ZMod 3) ≠ 2
⊢ -↑d ≠ ↑d
Theorem: Weight.not_eq_neg_self
Proof state before:
d : ℕ
hd : ↑d ≠ 0
hch : ringChar (ZMod 3) ≠ 2
⊢ -↑d ≠ ↑d
Tactic:
exact mt (Ring.eq_self_iff_eq_zero_of_char_ne_two hch).mp hd
Proof state after:
no goals
Theorem: Weight.not_eq_neg_self
Proof state before:
d : ℕ
hd : ↑d ≠ 0
⊢ ringChar (ZMod 3) ≠ 2
Tactic:
rw [ZMod.ringChar_zmod_n]
Proof state after:
d : ℕ
hd : ↑d ≠ 0
⊢ 3 ≠ 2
Theorem: Weight.not_eq_neg_self
Proof state before:
d : ℕ
hd : ↑d ≠ 0
⊢ 3 ≠ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Weight.eq_mod_3_of_rel
Proof state before:
d a b i₁ i₂ : ℕ
hd : ↑d ≠ 0
rel : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑a = ↑b
Tactic:
reduce_mod_3 rel
Proof state after:
d a b i₁ i₂ : ℕ
hd : ↑d ≠ 0
H₁✝ : 3 = 0
H₂✝ : 2 = -1
rel : ↑a = ↑b ∨ ↑d = 0
⊢ ↑a = ↑b
Theorem: Weight.eq_mod_3_of_rel
Proof state before:
d a b i₁ i₂ : ℕ
hd : ↑d ≠ 0
H₁✝ : 3 = 0
H₂✝ : 2 = -1
rel : ↑a = ↑b ∨ ↑d = 0
⊢ ↑a = ↑b
Tactic:
exact rel.resolve_right hd
Proof state after:
no goals
Theorem: Weight.eq_or_eq_neg_in_zmod_3
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
⊢ ↑a = ↑d ∨ ↑a = -↑d
Tactic:
have hdd := not_eq_neg_self hd
Proof state after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
⊢ ↑a = ↑d ∨ ↑a = -↑d