-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRk_comap_lift (M : Matroid β) (f : α → β) (X : Set α) :
    lift.{v,u} ((M.comap f).cRk X) = lift (M.cRk (f '' X))

Proof state:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ lift.{v, u} ((M.comap f).cRk X) = lift.{u, v} (M.cRk (f '' X))

Tactic:
nth_rw 1 [cRk, cRank, le_antisymm_iff, lift_iSup (bddAbove_range _), cRk, cRank, cRk, cRank]

Result:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ ⨆ i, lift.{v, u} #↑↑i ≤ lift.{u, v} (⨆ B, #↑↑B) ∧ lift.{u, v} (⨆ B, #↑↑B) ≤ lift.{v, u} (⨆ B, #↑↑B)

Proof state:
case refine_2.intro.intro.intro
α : Type u
β : Type v
M : Matroid β
f : α → β
X I₀ : Set α
hI₀X : I₀ ⊆ X
hfI₀ : InjOn f I₀
hIX : M.IsBasis' (f '' I₀) (f '' X)
⊢ lift.{u, v} #↑(f '' I₀) ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
rw [mk_image_eq_of_injOn_lift _ _ hfI₀, lift_le]

Result:
case refine_2.intro.intro.intro
α : Type u
β : Type v
M : Matroid β
f : α → β
X I₀ : Set α
hI₀X : I₀ ⊆ X
hfI₀ : InjOn f I₀
hIX : M.IsBasis' (f '' I₀) (f '' X)
⊢ #↑I₀ ≤ ⨆ B, #↑↑B

Proof state:
case refine_2.intro.intro.intro
α : Type u
β : Type v
M : Matroid β
f : α → β
X I₀ : Set α
hI₀X : I₀ ⊆ X
hfI₀ : InjOn f I₀
hIX : M.IsBasis' (f '' I₀) (f '' X)
⊢ #↑I₀ ≤ ⨆ B, #↑↑B

Tactic:
exact IsBasis'.cardinalMk_le_cRk <| comap_isBasis'_iff.2 ⟨hIX, hfI₀, hI₀X⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ (∀ (a : Set α), M.IsBasis' (f '' a) (f '' X) → InjOn f a → a ⊆ X → lift.{v, u} #↑a ≤ lift.{u, v} (⨆ B, #↑↑B)) ∧
    ∀ (a : Set β), M.IsBasis' a (f '' X) → lift.{u, v} #↑a ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
refine ⟨fun I hI hfI hIX ↦ ?_, fun I hIX ↦ ?_⟩

Result:
case refine_1
α : Type u
β : Type v
M : Matroid β
f : α → β
X I : Set α
hI : M.IsBasis' (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
⊢ lift.{v, u} #↑I ≤ lift.{u, v} (⨆ B, #↑↑B)

case refine_2
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
⊢ lift.{u, v} #↑I ≤ lift.{v, u} (⨆ B, #↑↑B)

Proof state:
case refine_1
α : Type u
β : Type v
M : Matroid β
f : α → β
X I : Set α
hI : M.IsBasis' (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
⊢ lift.{v, u} #↑I ≤ lift.{u, v} (⨆ B, #↑↑B)

Tactic:
rw [← mk_image_eq_of_injOn_lift _ _ hfI, lift_le]

Result:
case refine_1
α : Type u
β : Type v
M : Matroid β
f : α → β
X I : Set α
hI : M.IsBasis' (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
⊢ #↑(f '' I) ≤ ⨆ B, #↑↑B

Proof state:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ ⨆ i, lift.{v, u} #↑↑i ≤ lift.{u, v} (⨆ B, #↑↑B) ∧ lift.{u, v} (⨆ B, #↑↑B) ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
nth_rw 2 [lift_iSup (bddAbove_range _)]

Result:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ ⨆ i, lift.{v, u} #↑↑i ≤ lift.{u, v} (⨆ B, #↑↑B) ∧ ⨆ i, lift.{u, v} #↑↑i ≤ lift.{v, u} (⨆ B, #↑↑B)

Proof state:
case intro.intro
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
I₀ : Set α
hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X
hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))
⊢ ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀

Tactic:
refine ⟨I₀, hI₀ss.trans inter_subset_right, ?_, hbij.injOn⟩

Result:
case intro.intro
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
I₀ : Set α
hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X
hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))
⊢ f '' I₀ = I

Proof state:
case intro.intro
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
I₀ : Set α
hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X
hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))
⊢ f '' I₀ = I

Tactic:
rw [hbij.image_eq, image_preimage_inter, inter_eq_self_of_subset_left hIX.subset]

Result:
no goals

Proof state:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ ⨆ i, lift.{v, u} #↑↑i ≤ lift.{u, v} (⨆ B, #↑↑B) ∧ ⨆ i, lift.{u, v} #↑↑i ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
simp only [ciSup_le_iff (bddAbove_range _), ge_iff_le, Subtype.forall, isBase_restrict_iff',
  comap_isBasis'_iff, and_imp]

Result:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ (∀ (a : Set α), M.IsBasis' (f '' a) (f '' X) → InjOn f a → a ⊆ X → lift.{v, u} #↑a ≤ lift.{u, v} (⨆ B, #↑↑B)) ∧
    ∀ (a : Set β), M.IsBasis' a (f '' X) → lift.{u, v} #↑a ≤ lift.{v, u} (⨆ B, #↑↑B)

Proof state:
case refine_2
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
⊢ lift.{u, v} #↑I ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
obtain ⟨I₀, hI₀X, rfl, hfI₀⟩ := show ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀ by
  obtain ⟨I₀, hI₀ss, hbij⟩ := exists_subset_bijOn (f ⁻¹' I ∩ X) f
  refine ⟨I₀, hI₀ss.trans inter_subset_right, ?_, hbij.injOn⟩
  rw [hbij.image_eq, image_preimage_inter, inter_eq_self_of_subset_left hIX.subset]

Result:
case refine_2.intro.intro.intro
α : Type u
β : Type v
M : Matroid β
f : α → β
X I₀ : Set α
hI₀X : I₀ ⊆ X
hfI₀ : InjOn f I₀
hIX : M.IsBasis' (f '' I₀) (f '' X)
⊢ lift.{u, v} #↑(f '' I₀) ≤ lift.{v, u} (⨆ B, #↑↑B)

Proof state:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
⊢ ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀

Tactic:
obtain ⟨I₀, hI₀ss, hbij⟩ := exists_subset_bijOn (f ⁻¹' I ∩ X) f

Result:
case intro.intro
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
I₀ : Set α
hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X
hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))
⊢ ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀

Proof state:
case refine_1
α : Type u
β : Type v
M : Matroid β
f : α → β
X I : Set α
hI : M.IsBasis' (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
⊢ #↑(f '' I) ≤ ⨆ B, #↑↑B

Tactic:
exact hI.cardinalMk_le_cRk

Result:
no goals