internlm/Lean-Github huggingface dataset:
Theorem: Weight.condition_of_feasible
Proof state before:
case hbd'.inr
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hk₁✝ : 1 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hk₁ : 2 ≤ k₁
⊢ 2 * d < s₂ + t₂
Tactic:
have hs₂bd : 2 * I.a₁ + 3 * I.a₂ ≤ s₂ := by rw [hks₂]; gcongr
Proof state after:
case hbd'.inr
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hk₁✝ : 1 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hk₁ : 2 ≤ k₁
hs₂bd : 2 * I.a₁ + 3 * I.a₂ ≤ s₂
⊢ 2 * d < s₂ + t₂
Theorem: Weight.condition_of_feasible
Proof state before:
case hbd'.inr
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hk₁✝ : 1 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hk₁ : 2 ≤ k₁
hs₂bd : 2 * I.a₁ + 3 * I.a₂ ≤ s₂
⊢ 2 * d < s₂ + t₂
Tactic:
have ht₂bd : 2 * I.b₁ + 3 * I.b₂ ≤ t₂ := by rw [hkt₂]; gcongr
Proof state after:
case hbd'.inr
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hk₁✝ : 1 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hk₁ : 2 ≤ k₁
hs₂bd : 2 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 2 * I.b₁ + 3 * I.b₂ ≤ t₂
⊢ 2 * d < s₂ + t₂
Theorem: Weight.condition_of_feasible
Proof state before:
case hbd'.inr
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hk₁✝ : 1 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hk₁ : 2 ≤ k₁
hs₂bd : 2 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 2 * I.b₁ + 3 * I.b₂ ≤ t₂
⊢ 2 * d < s₂ + t₂
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hk₁✝ : 1 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hk₁ : 2 ≤ k₁
⊢ 2 * I.a₁ + 3 * I.a₂ ≤ s₂
Tactic:
rw [hks₂]
Proof state after:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hk₁✝ : 1 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hk₁ : 2 ≤ k₁
⊢ 2 * I.a₁ + 3 * I.a₂ ≤ k₁ * I.a₁ + k₂ * I.a₂
Theorem: Weight.condition_of_feasible
Proof state before:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hk₁✝ : 1 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hk₁ : 2 ≤ k₁
⊢ 2 * I.a₁ + 3 * I.a₂ ≤ k₁ * I.a₁ + k₂ * I.a₂
Tactic:
gcongr
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hk₁✝ : 1 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hk₁ : 2 ≤ k₁
hs₂bd : 2 * I.a₁ + 3 * I.a₂ ≤ s₂
⊢ 2 * I.b₁ + 3 * I.b₂ ≤ t₂
Tactic:
rw [hkt₂]
Proof state after:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hk₁✝ : 1 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hk₁ : 2 ≤ k₁
hs₂bd : 2 * I.a₁ + 3 * I.a₂ ≤ s₂
⊢ 2 * I.b₁ + 3 * I.b₂ ≤ k₁ * I.b₁ + k₂ * I.b₂
Theorem: Weight.condition_of_feasible
Proof state before:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hk₁✝ : 1 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hk₁ : 2 ≤ k₁
hs₂bd : 2 * I.a₁ + 3 * I.a₂ ≤ s₂
⊢ 2 * I.b₁ + 3 * I.b₂ ≤ k₁ * I.b₁ + k₂ * I.b₂
Tactic:
gcongr
Proof state after:
no goals
Theorem: Weight.dom_by_max_le_d
Proof state before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
cases' le_or_lt (a + b) d with h h
Proof state after:
case inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : a + b ≤ d
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b

case inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Theorem: Weight.dom_by_max_le_d
Proof state before:
case inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : a + b ≤ d
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
exact ⟨a, b, h, Eq.le rfl⟩
Proof state after:
no goals
Theorem: Weight.dom_by_max_le_d
Proof state before:
case inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
obtain ⟨I, hI, hIab⟩ := mem_feasible d a b
Proof state after:
case inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Theorem: Weight.dom_by_max_le_d
Proof state before:
case inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
have hab : a ≠ 0 ∨ b ≠ 0 := by by_contra! hab; linarith
Proof state after:
case inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Theorem: Weight.dom_by_max_le_d
Proof state before:
case inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
cases' dom_of_mem d hab hIab (condition_of_feasible hI) with H H
Proof state after:
case inr.intro.intro.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
H : of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b

case inr.intro.intro.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
H : of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Theorem: Weight.dom_by_max_le_d
Proof state before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
⊢ a ≠ 0 ∨ b ≠ 0
Tactic:
by_contra! hab
Proof state after:
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a = 0 ∧ b = 0
⊢ False
Theorem: Weight.dom_by_max_le_d
Proof state before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a = 0 ∧ b = 0
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.dom_by_max_le_d
Proof state before:
case inr.intro.intro.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
H : of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
exact ⟨I.a₁, I.b₁, hI.1, H⟩
Proof state after:
no goals
Theorem: Weight.dom_by_max_le_d
Proof state before:
case inr.intro.intro.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
H : of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
Tactic:
exact ⟨I.a₂, I.b₂, hI.2.1, H⟩
Proof state after:
no goals
Theorem: Weight.theorem_1_6
Proof state before:
d : ℕ
inst✝ : NeZero d
⊢ ∀ w ∈ M 2 d, ∀ (i : Fin (Nat.succ 2)), w i ≤ d
Tactic:
intro w hw
Proof state after:
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
hw : w ∈ M 2 d
⊢ ∀ (i : Fin (Nat.succ 2)), w i ≤ d
Theorem: Weight.theorem_1_6
Proof state before:
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
hw : w ∈ M 2 d
⊢ ∀ (i : Fin (Nat.succ 2)), w i ≤ d
Tactic:
obtain ⟨a, b, hab⟩ := ex_of_fraction hw.1
Proof state after:
case intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
hw : w ∈ M 2 d
a b : ℕ
hab : w = of_fraction d a b
⊢ ∀ (i : Fin (Nat.succ 2)), w i ≤ d
Theorem: Weight.theorem_1_6
Proof state before:
case intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
hw : w ∈ M 2 d
a b : ℕ
hab : w = of_fraction d a b
⊢ ∀ (i : Fin (Nat.succ 2)), w i ≤ d
Tactic:
obtain ⟨s, t, hle, hdom⟩ := dom_by_max_le_d d a b
Proof state after:
case intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
hw : w ∈ M 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
⊢ ∀ (i : Fin (Nat.succ 2)), w i ≤ d
Theorem: Weight.theorem_1_6
Proof state before:
case intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
hw : w ∈ M 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
⊢ ∀ (i : Fin (Nat.succ 2)), w i ≤ d
Tactic:
contrapose! hw
Proof state after:
case intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
hw : ∃ i, d < w i
⊢ w ∉ M 2 d
Theorem: Weight.theorem_1_6
Proof state before:
case intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
hw : ∃ i, d < w i
⊢ w ∉ M 2 d
Tactic:
obtain ⟨i, hi⟩ := hw
Proof state after:
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hi : d < w i
⊢ w ∉ M 2 d
Theorem: Weight.theorem_1_6
Proof state before:
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hi : d < w i
⊢ w ∉ M 2 d
Tactic:
refine not_in_M_of_dom_ne ⟨of_fraction d s t, normalized_of_of_fraction d s t, hab ▸ hdom,
                           fun H ↦ ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hi : d < w i
H : of_fraction d s t = w
⊢ False
Theorem: Weight.theorem_1_6
Proof state before:
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hi : d < w i
H : of_fraction d s t = w
⊢ False
Tactic:
subst H
Proof state after:
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
a b s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hab : of_fraction d s t = of_fraction d a b
hi : d < of_fraction d s t i
⊢ False
Theorem: Weight.theorem_1_6
Proof state before:
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
a b s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hab : of_fraction d s t = of_fraction d a b
hi : d < of_fraction d s t i
⊢ False
Tactic:
exact lt_irrefl d <| hi.trans_le <| (of_fraction_le d s t i).trans hle
Proof state after:
no goals
Theorem: Disjoint.sumSubtypeEmbedding_preimage_inl
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s t r : Set α
h : Disjoint s t
⊢ ↑(Sum.inl ⁻¹' (⇑h.sumSubtypeEmbedding ⁻¹' r)) = r ∩ s
Tactic:
ext
Proof state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s t r : Set α
h : Disjoint s t
x✝ : α
⊢ x✝ ∈ ↑(Sum.inl ⁻¹' (⇑h.sumSubtypeEmbedding ⁻¹' r)) ↔ x✝ ∈ r ∩ s
Theorem: Disjoint.sumSubtypeEmbedding_preimage_inl
Proof state before:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s t r : Set α
h : Disjoint s t
x✝ : α
⊢ x✝ ∈ ↑(Sum.inl ⁻¹' (⇑h.sumSubtypeEmbedding ⁻¹' r)) ↔ x✝ ∈ r ∩ s
Tactic:
simp
Proof state after:
no goals
Theorem: Disjoint.sumSubtypeEmbedding_preimage_inr
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s t r : Set α
h : Disjoint s t
⊢ ↑(Sum.inr ⁻¹' (⇑h.sumSubtypeEmbedding ⁻¹' r)) = r ∩ t
Tactic:
ext
Proof state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s t r : Set α
h : Disjoint s t
x✝ : α
⊢ x✝ ∈ ↑(Sum.inr ⁻¹' (⇑h.sumSubtypeEmbedding ⁻¹' r)) ↔ x✝ ∈ r ∩ t
Theorem: Disjoint.sumSubtypeEmbedding_preimage_inr
Proof state before:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s t r : Set α
h : Disjoint s t
x✝ : α
⊢ x✝ ∈ ↑(Sum.inr ⁻¹' (⇑h.sumSubtypeEmbedding ⁻¹' r)) ↔ x✝ ∈ r ∩ t
Tactic:
simp
Proof state after:
no goals
Theorem: Disjoint.sumSubtypeEmbedding_range
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s t : Set α
h : Disjoint s t
⊢ range ⇑h.sumSubtypeEmbedding = s ∪ t
Tactic:
ext
Proof state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s t : Set α
h : Disjoint s t
x✝ : α
⊢ x✝ ∈ range ⇑h.sumSubtypeEmbedding ↔ x✝ ∈ s ∪ t
Theorem: Disjoint.sumSubtypeEmbedding_range
Proof state before:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s t : Set α
h : Disjoint s t
x✝ : α
⊢ x✝ ∈ range ⇑h.sumSubtypeEmbedding ↔ x✝ ∈ s ∪ t
Tactic:
simp
Proof state after:
no goals
Theorem: Set.PairwiseDisjoint.sigmaSubtypeEmbedding_preimage
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : ι → Set α
h : univ.PairwiseDisjoint s
i : ι
r : Set α
⊢ ↑(Sigma.mk i ⁻¹' (⇑h.sigmaSubtypeEmbedding ⁻¹' r)) = r ∩ s i
Tactic:
ext
Proof state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s : ι → Set α
h : univ.PairwiseDisjoint s
i : ι
r : Set α
x✝ : α
⊢ x✝ ∈ ↑(Sigma.mk i ⁻¹' (⇑h.sigmaSubtypeEmbedding ⁻¹' r)) ↔ x✝ ∈ r ∩ s i
Theorem: Set.PairwiseDisjoint.sigmaSubtypeEmbedding_preimage
Proof state before:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s : ι → Set α
h : univ.PairwiseDisjoint s
i : ι
r : Set α
x✝ : α
⊢ x✝ ∈ ↑(Sigma.mk i ⁻¹' (⇑h.sigmaSubtypeEmbedding ⁻¹' r)) ↔ x✝ ∈ r ∩ s i
Tactic:
simp
Proof state after:
no goals
Theorem: Set.PairwiseDisjoint.sigmaSubtypeEmbedding_range
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : ι → Set α
h : univ.PairwiseDisjoint s
⊢ Set.range ⇑h.sigmaSubtypeEmbedding = ⋃ i, s i
Tactic:
ext
Proof state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s : ι → Set α
h : univ.PairwiseDisjoint s
x✝ : α
⊢ x✝ ∈ Set.range ⇑h.sigmaSubtypeEmbedding ↔ x✝ ∈ ⋃ i, s i
Theorem: Set.PairwiseDisjoint.sigmaSubtypeEmbedding_range
Proof state before:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s : ι → Set α
h : univ.PairwiseDisjoint s
x✝ : α
⊢ x✝ ∈ Set.range ⇑h.sigmaSubtypeEmbedding ↔ x✝ ∈ ⋃ i, s i
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.iUnion_preimage_image_sigma_mk_eq
Proof state before:
α✝ : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
α : ι → Type u_5
f : (i : ι) → Set (α i)
j : ι
⊢ ⋃ i, Sigma.mk j ⁻¹' (Sigma.mk i '' f i) = f j
Tactic:
aesop
Proof state after:
no goals
Theorem: Matroid.sigmaDisjoint_ground_eq
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
M : ι → Matroid α
h : univ.PairwiseDisjoint fun i => (M i).E
⊢ (Matroid.sigmaDisjoint M h).E = ⋃ i, (M i).E
Tactic:
ext
Proof state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : ι → Matroid α
h : univ.PairwiseDisjoint fun i => (M i).E
x✝ : α
⊢ x✝ ∈ (Matroid.sigmaDisjoint M h).E ↔ x✝ ∈ ⋃ i, (M i).E
Theorem: Matroid.sigmaDisjoint_ground_eq
Proof state before:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : ι → Matroid α
h : univ.PairwiseDisjoint fun i => (M i).E
x✝ : α
⊢ x✝ ∈ (Matroid.sigmaDisjoint M h).E ↔ x✝ ∈ ⋃ i, (M i).E
Tactic:
simp [Matroid.sigmaDisjoint, mapEmbedding, restrictSubtype]
Proof state after:
no goals
Theorem: Matroid.sigma'_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
M : ι → Matroid α
h : univ.PairwiseDisjoint fun i => (M i).E
I : Set α
⊢ (Matroid.sigmaDisjoint M h).Indep I ↔ (∀ (i : ι), (M i).Indep (I ∩ (M i).E)) ∧ I ⊆ ⋃ i, (M i).E
Tactic:
simp [Matroid.sigmaDisjoint, h.sigmaSubtypeEmbedding_preimage]
Proof state after:
no goals
Theorem: Matroid.disjointSum_ground_eq
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
M N : Matroid α
h : Disjoint M.E N.E
⊢ (M.disjointSum N h).E = M.E ∪ N.E
Tactic:
simp [disjointSum, restrictSubtype, mapEmbedding]
Proof state after:
no goals
Theorem: Matroid.disjointSum_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
⊢ (M.disjointSum N h).Indep I ↔ M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
Tactic:
simp [disjointSum, and_assoc]
Proof state after:
no goals
Theorem: Matroid.Indep.eq_union_image_of_disjointSum
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : (M.disjointSum N h).Indep I
⊢ ∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN
Tactic:
rw [disjointSum_indep_iff] at hI
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ ∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN
Theorem: Matroid.Indep.eq_union_image_of_disjointSum
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ ∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN
Tactic:
refine ⟨I ∩ M.E, I ∩ N.E, hI.1, hI.2.1, h.mono inf_le_right inf_le_right, ?_⟩
Proof state after:
α : Type u_1
β : Type u_2
ι : Type u_3
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ I = I ∩ M.E ∪ I ∩ N.E
Theorem: Matroid.Indep.eq_union_image_of_disjointSum
Proof state before:
α : Type u_1
β : Type u_2
ι : Type u_3
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ I = I ∩ M.E ∪ I ∩ N.E
Tactic:
rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hI.2.2]
Proof state after:
no goals
Theorem: Matroid.singleton_dep
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ M.Dep {e} ↔ M.Loop e
Tactic:
rw [loop_iff_mem_cl_empty, M.empty_indep.mem_cl_iff_of_not_mem (not_mem_empty e),insert_emptyc_eq]
Proof state after:
no goals
Theorem: Matroid.singleton_not_indep
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : autoParam (e ∈ M.E) _auto✝
⊢ ¬M.Indep {e} ↔ M.Loop e
Tactic:
rw [← singleton_dep, ← not_indep_iff]
Proof state after:
no goals
Theorem: Matroid.singleton_circuit
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ M.Circuit {e} ↔ M.Loop e
Tactic:
simp_rw [← singleton_dep, circuit_def, mem_minimals_setOf_iff, and_iff_left_iff_imp,
  subset_singleton_iff_eq]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ M.Dep {e} → ∀ ⦃y : Set α⦄, M.Dep y → y = ∅ ∨ y = {e} → {e} = y