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₂ b₁ b₂ : ℕ
h₁ : a₁ ≤ b₁
h₂ : a₂ ≤ b₂
⊢ Nonempty (unif a₁ b₁ ≤i unif a₂ b₂) ↔ a₁ ≤ a₂ ∧ b₁ - a₁ ≤ b₂ - a₂
Tactic:
obtain ⟨d₁, rfl⟩ := Nat.exists_eq_add_of_le h₁
State after:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ b₂ : ℕ
h₂ : a₂ ≤ b₂
d₁ : ℕ
h₁ : a₁ ≤ a₁ + d₁
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ b₂) ↔ a₁ ≤ a₂ ∧ a₁ + d₁ - a₁ ≤ b₂ - a₂

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

State before:
case intro.intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ : ℕ
h₁ : a₁ ≤ a₁ + d₁
d₂ : ℕ
h₂ : a₂ ≤ a₂ + d₂
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂)) ↔ a₁ ≤ a₂ ∧ a₁ + d₁ - a₁ ≤ a₂ + d₂ - a₂
Tactic:
rw [add_tsub_cancel_left, add_tsub_cancel_left, unif_isoMinor_unif_iff]
State after:
no goals