Theorem: Matroid.rado_necessary (Matroid/Intersection.lean)

State before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
⊢ S.ncard ≤ M.r (f ⁻¹' S)
Tactic:
have hinj : Function.Injective x := fun i j h ↦ by rw [← hx i, ← hx j, h]
State after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
⊢ S.ncard ≤ M.r (f ⁻¹' S)

State before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
⊢ S.ncard ≤ M.r (f ⁻¹' S)
Tactic:
have hS := (h_ind.subset (image_subset_range x S)).r
State after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = (x '' S).ncard
⊢ S.ncard ≤ M.r (f ⁻¹' S)

State before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = (x '' S).ncard
⊢ S.ncard ≤ M.r (f ⁻¹' S)
Tactic:
rw [ncard_image_of_injective _ hinj] at hS
State after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
⊢ S.ncard ≤ M.r (f ⁻¹' S)

State before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
⊢ S.ncard ≤ M.r (f ⁻¹' S)
Tactic:
refine hS.symm.le.trans (M.r_le_of_subset ?_)
State after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
⊢ x '' S ⊆ f ⁻¹' S

State before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
⊢ x '' S ⊆ f ⁻¹' S
Tactic:
rintro f ⟨i, hi, rfl⟩
State after:
case intro.intro
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
i : ι
hi : i ∈ S
⊢ x i ∈ f ⁻¹' S

State before:
case intro.intro
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
i : ι
hi : i ∈ S
⊢ x i ∈ f ⁻¹' S
Tactic:
simpa [hx i]
State after:
no goals

State before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
i j : ι
h : x i = x j
⊢ i = j
Tactic:
rw [← hx i, ← hx j, h]
State after:
no goals