Theorem: Matroid.unif_isoMinor_unif_iff (Matroid/Constructions/Uniform.lean)

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ d₂ : ℕ
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂)) ↔ a₁ ≤ a₂ ∧ d₁ ≤ d₂
Tactic:
refine ⟨fun ⟨e⟩ ↦ ⟨by simpa using e.rk_le, by simpa using IsoMinor.rk_le e.dual⟩, fun h ↦ ?_⟩
State after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ d₂ : ℕ
h : a₁ ≤ a₂ ∧ d₁ ≤ d₂
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂))

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ d₂ : ℕ
h : a₁ ≤ a₂ ∧ d₁ ≤ d₂
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂))
Tactic:
obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le h.1
State after:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ d₁ d₂ j : ℕ
h : a₁ ≤ a₁ + j ∧ d₁ ≤ d₂
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif (a₁ + j) (a₁ + j + d₂))

State before:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ d₁ d₂ j : ℕ
h : a₁ ≤ a₁ + j ∧ d₁ ≤ d₂
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif (a₁ + j) (a₁ + j + d₂))
Tactic:
exact ⟨(unif_isoMinor_contr a₁ (a₁ + d₁) j).trans (unif_isoRestr_unif _ (by linarith)).isoMinor⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ d₂ : ℕ
x✝ : Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂))
e : unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂)
⊢ a₁ ≤ a₂
Tactic:
simpa using e.rk_le
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ d₂ : ℕ
x✝ : Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂))
e : unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂)
⊢ d₁ ≤ d₂
Tactic:
simpa using IsoMinor.rk_le e.dual
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ d₁ d₂ j : ℕ
h : a₁ ≤ a₁ + j ∧ d₁ ≤ d₂
⊢ a₁ + d₁ + j ≤ a₁ + j + d₂
Tactic:
linarith
State after:
no goals