internlm/Lean-Github huggingface dataset:
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
case right
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
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 : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge d (-ai) bi
aa : ℕ
haa : ↑aa = -ai
bb : ℕ
hbb : ↑bb = bi
H : ¬0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
⊢ ↑aa * ↑I.b₂ ≤ ↑bb * ↑I.a₂
Tactic:
rw [haa, hbb]
Proof state after:
case right
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
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 : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge d (-ai) bi
aa : ℕ
haa : ↑aa = -ai
bb : ℕ
hbb : ↑bb = bi
H : ¬0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
⊢ -ai * ↑I.b₂ ≤ bi * ↑I.a₂
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
case right
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
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 : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge d (-ai) bi
aa : ℕ
haa : ↑aa = -ai
bb : ℕ
hbb : ↑bb = bi
H : ¬0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
⊢ -ai * ↑I.b₂ ≤ bi * ↑I.a₂
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
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 : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)
hi' : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
⊢ pair' (of_fraction d I.a₂ I.b₂) (v i) =
    0 * pair' (of_fraction d I.a₁ I.b₁) (v i) + 1 * pair' (of_fraction d I.a₂ I.b₂) (v i)
Tactic:
rw [one_mul, zero_mul, zero_add]
Proof state after:
no goals
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
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 : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)
hi' : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
⊢ 0 ≤ ↑k₁
Tactic:
exact_mod_cast hk₁.le
Proof state after:
no goals
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
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 : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)
hi' : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
⊢ 1 ≤ ↑k₂
Tactic:
exact_mod_cast hk₂
Proof state after:
no goals
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
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 : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)
hi' : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
⊢ ↑k₁ * pair' (of_fraction d I.a₁ I.b₁) (v i) + ↑k₂ * pair' (of_fraction d I.a₂ I.b₂) (v i) =
    pair' (of_fraction d a b) (v i)
Tactic:
rw [h₁, h₂, pair'_of_fraction_add, Pi.add_apply, pair'_of_fraction_mul,
    pair'_of_fraction_mul]
Proof state after:
no goals
Theorem: Weight.dom_of_proportional
Proof state before:
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
⊢ of_fraction d a' b' ≤ of_fraction d a b
Tactic:
obtain ⟨m, ha, hb⟩ := Nat.proportional_of_mul_eq_mul_of_coprime h hc
Proof state after:
case intro.intro
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
⊢ of_fraction d a' b' ≤ of_fraction d a b
Theorem: Weight.dom_of_proportional
Proof state before:
case intro.intro
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
⊢ of_fraction d a' b' ≤ of_fraction d a b
Tactic:
have hmz : m ≠ 0 :=
  hab.elim (fun haz ↦ left_ne_zero_of_mul <| ha ▸ haz)
           (fun hbz ↦ left_ne_zero_of_mul <| hb ▸ hbz)
Proof state after:
case intro.intro
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
⊢ of_fraction d a' b' ≤ of_fraction d a b
Theorem: Weight.dom_of_proportional
Proof state before:
case intro.intro
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
⊢ of_fraction d a' b' ≤ of_fraction d a b
Tactic:
have hm : (1 : ℤ) ≤ m := Int.toNat_le.mp <| Nat.one_le_iff_ne_zero.mpr hmz
Proof state after:
case intro.intro
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
⊢ of_fraction d a' b' ≤ of_fraction d a b
Theorem: Weight.dom_of_proportional
Proof state before:
case intro.intro
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
⊢ of_fraction d a' b' ≤ of_fraction d a b
Tactic:
apply dom_of_pair_le
Proof state after:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
⊢ ∀ (a_1 : ↑(testvecs 2 d)),
    0 ≤ pair' (of_fraction d a' b') (v a_1) → pair' (of_fraction d a' b') (v a_1) ≤ pair' (of_fraction d a b) (v a_1)
Theorem: Weight.dom_of_proportional
Proof state before:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
⊢ ∀ (a_1 : ↑(testvecs 2 d)),
    0 ≤ pair' (of_fraction d a' b') (v a_1) → pair' (of_fraction d a' b') (v a_1) ≤ pair' (of_fraction d a b) (v a_1)
Tactic:
intro i hi
Proof state after:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d a' b') (v i)
⊢ pair' (of_fraction d a' b') (v i) ≤ pair' (of_fraction d a b) (v i)
Theorem: Weight.dom_of_proportional
Proof state before:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d a' b') (v i)
⊢ pair' (of_fraction d a' b') (v i) ≤ pair' (of_fraction d a b) (v i)
Tactic:
simp_rw [pair'_of_fraction] at hi ⊢
Proof state after:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2)
⊢ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2) ≤ ↑a * v i 2 + ↑b * (v i 1 + v i 2)
Theorem: Weight.dom_of_proportional
Proof state before:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2)
⊢ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2) ≤ ↑a * v i 2 + ↑b * (v i 1 + v i 2)
Tactic:
rw [ha, hb, Nat.cast_mul, Nat.cast_mul, mul_assoc, mul_assoc, ← mul_add]
Proof state after:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2)
⊢ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2) ≤ ↑m * (↑a' * v i 2 + ↑b' * (v i 1 + v i 2))
Theorem: Weight.dom_of_proportional
Proof state before:
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2)
⊢ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2) ≤ ↑m * (↑a' * v i 2 + ↑b' * (v i 1 + v i 2))
Tactic:
exact le_mul_of_one_le_left hi hm
Proof state after:
no goals
Theorem: Weight.dom_of_mem
Proof state before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
have help {a b c d : ℕ} (hyp : a * b = c * d) : d * c = b * a
Proof state after:
case help
d✝ : ℕ
inst✝ : NeZero d✝
a✝ b✝ : ℕ
I : BasicInterval
hab : a✝ ≠ 0 ∨ b✝ ≠ 0
hm : mem a✝ b✝ I
h :
  (∀ (a' b' : ℕ), mem_S_le d✝ ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d✝ ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
a b c d : ℕ
hyp : a * b = c * d
⊢ d * c = b * a

d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Theorem: Weight.dom_of_mem
Proof state before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
rcases eq_or_eq_or_mem_interior_of_mem hm with H | H | H
Proof state after:
case inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : a * I.b₁ = b * I.a₁
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b

case inr.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : a * I.b₂ = b * I.a₂
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b

case inr.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : BasicInterval.mem_interior a b I
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Theorem: Weight.dom_of_mem
Proof state before:
case help
d✝ : ℕ
inst✝ : NeZero d✝
a✝ b✝ : ℕ
I : BasicInterval
hab : a✝ ≠ 0 ∨ b✝ ≠ 0
hm : mem a✝ b✝ I
h :
  (∀ (a' b' : ℕ), mem_S_le d✝ ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d✝ ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
a b c d : ℕ
hyp : a * b = c * d
⊢ d * c = b * a
Tactic:
rw [mul_comm b, mul_comm d, hyp]
Proof state after:
no goals
Theorem: Weight.dom_of_mem
Proof state before:
case inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : a * I.b₁ = b * I.a₁
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
exact Or.inl <| dom_of_proportional d hab I.coprime₁ <| help H
Proof state after:
no goals
Theorem: Weight.dom_of_mem
Proof state before:
case inr.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : a * I.b₂ = b * I.a₂
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
exact Or.inr <| dom_of_proportional d hab I.coprime₂ <| help H
Proof state after:
no goals
Theorem: Weight.dom_of_mem
Proof state before:
case inr.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : BasicInterval.mem_interior a b I
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
rcases h with h | h
Proof state after:
case inr.inr.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b

case inr.inr.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Theorem: Weight.dom_of_mem
Proof state before:
case inr.inr.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
exact Or.inl <| dom_of_mem_interior_left d H h
Proof state after:
no goals
Theorem: Weight.dom_of_mem
Proof state before:
case inr.inr.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
exact Or.inr <| dom_of_mem_interior_right d H h
Proof state after:
no goals
Theorem: Weight.condition_iff_weaker_le
Proof state before:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
⊢ (∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂) ↔
    ∀ (a b : ℕ), mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
Tactic:
refine ⟨fun H a b h₁ h₂ ↦ ?_, fun H a b _ ↦ H a b⟩
Proof state after:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
a b : ℕ
h₁ : mem_S_le d ↑a ↑b
h₂ : mem a b I
⊢ a * I.b₂ = b * I.a₂
Theorem: Weight.condition_iff_weaker_le
Proof state before:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
a b : ℕ
h₁ : mem_S_le d ↑a ↑b
h₂ : mem a b I
⊢ a * I.b₂ = b * I.a₂
Tactic:
cases' Nat.eq_zero_or_pos (Nat.gcd a b) with h₀ h₀
Proof state after:
case inl
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
a b : ℕ
h₁ : mem_S_le d ↑a ↑b
h₂ : mem a b I
h₀ : Nat.gcd a b = 0
⊢ a * I.b₂ = b * I.a₂

case inr
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
a b : ℕ
h₁ : mem_S_le d ↑a ↑b
h₂ : mem a b I
h₀ : Nat.gcd a b > 0
⊢ a * I.b₂ = b * I.a₂
Theorem: Weight.condition_iff_weaker_le
Proof state before:
case inr
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
a b : ℕ
h₁ : mem_S_le d ↑a ↑b
h₂ : mem a b I
h₀ : Nat.gcd a b > 0
⊢ a * I.b₂ = b * I.a₂
Tactic:
obtain ⟨g, a', b', hg₁, hcop, rfl, rfl⟩ := Nat.exists_coprime' h₀
Proof state after:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_le d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
h₀ : Nat.gcd (a' * g) (b' * g) > 0
⊢ a' * g * I.b₂ = b' * g * I.a₂
Theorem: Weight.condition_iff_weaker_le
Proof state before:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_le d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
h₀ : Nat.gcd (a' * g) (b' * g) > 0
⊢ a' * g * I.b₂ = b' * g * I.a₂
Tactic:
clear h₀
Proof state after:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_le d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
⊢ a' * g * I.b₂ = b' * g * I.a₂
Theorem: Weight.condition_iff_weaker_le
Proof state before:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_le d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
⊢ a' * g * I.b₂ = b' * g * I.a₂
Tactic:
simp_rw [mul_comm _ g, mul_assoc]
Proof state after:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_le d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
⊢ g * (a' * I.b₂) = g * (b' * I.a₂)
Theorem: Weight.condition_iff_weaker_le
Proof state before:
case inl
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
a b : ℕ
h₁ : mem_S_le d ↑a ↑b
h₂ : mem a b I
h₀ : Nat.gcd a b = 0
⊢ a * I.b₂ = b * I.a₂
Tactic:
obtain ⟨rfl, rfl⟩ := Nat.gcd_eq_zero_iff.mp h₀
Proof state after:
case inl.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
h₁ : mem_S_le d ↑0 ↑0
h₂ : mem 0 0 I
h₀ : Nat.gcd 0 0 = 0
⊢ 0 * I.b₂ = 0 * I.a₂
Theorem: Weight.condition_iff_weaker_le
Proof state before:
case inl.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_le d ↑a ↑b → mem a b I → a * I.b₂ = b * I.a₂
h₁ : mem_S_le d ↑0 ↑0
h₂ : mem 0 0 I
h₀ : Nat.gcd 0 0 = 0
⊢ 0 * I.b₂ = 0 * I.a₂
Tactic:
simp only [zero_mul]
Proof state after:
no goals
Theorem: Weight.condition_iff_weaker_ge
Proof state before:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
⊢ (∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁) ↔
    ∀ (a b : ℕ), mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
Tactic:
refine ⟨fun H a b h₁ h₂ ↦ ?_, fun H a b _ ↦ H a b⟩
Proof state after:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
a b : ℕ
h₁ : mem_S_ge d ↑a ↑b
h₂ : mem a b I
⊢ a * I.b₁ = b * I.a₁
Theorem: Weight.condition_iff_weaker_ge
Proof state before:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
a b : ℕ
h₁ : mem_S_ge d ↑a ↑b
h₂ : mem a b I
⊢ a * I.b₁ = b * I.a₁
Tactic:
cases' Nat.eq_zero_or_pos (Nat.gcd a b) with h₀ h₀
Proof state after:
case inl
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
a b : ℕ
h₁ : mem_S_ge d ↑a ↑b
h₂ : mem a b I
h₀ : Nat.gcd a b = 0
⊢ a * I.b₁ = b * I.a₁

case inr
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
a b : ℕ
h₁ : mem_S_ge d ↑a ↑b
h₂ : mem a b I
h₀ : Nat.gcd a b > 0
⊢ a * I.b₁ = b * I.a₁
Theorem: Weight.condition_iff_weaker_ge
Proof state before:
case inr
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
a b : ℕ
h₁ : mem_S_ge d ↑a ↑b
h₂ : mem a b I
h₀ : Nat.gcd a b > 0
⊢ a * I.b₁ = b * I.a₁
Tactic:
obtain ⟨g, a', b', hg₁, hcop, rfl, rfl⟩ := Nat.exists_coprime' h₀
Proof state after:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_ge d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
h₀ : Nat.gcd (a' * g) (b' * g) > 0
⊢ a' * g * I.b₁ = b' * g * I.a₁
Theorem: Weight.condition_iff_weaker_ge
Proof state before:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_ge d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
h₀ : Nat.gcd (a' * g) (b' * g) > 0
⊢ a' * g * I.b₁ = b' * g * I.a₁
Tactic:
clear h₀
Proof state after:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_ge d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
⊢ a' * g * I.b₁ = b' * g * I.a₁
Theorem: Weight.condition_iff_weaker_ge
Proof state before:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_ge d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
⊢ a' * g * I.b₁ = b' * g * I.a₁
Tactic:
simp_rw [mul_comm _ g, mul_assoc]
Proof state after:
case inr.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
g : ℕ
a' b' : ℕ
hg₁ : 0 < g
hcop : Nat.Coprime a' b'
h₁ : mem_S_ge d ↑(a' * g) ↑(b' * g)
h₂ : mem (a' * g) (b' * g) I
⊢ g * (a' * I.b₁) = g * (b' * I.a₁)