-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRk_map_image_lift (M : Matroid α) (hf : InjOn f M.E) (X : Set α)
    (hX : X ⊆ M.E

Proof state:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ lift.{u, v} ((M.map f hf).cRk (f '' X)) = lift.{v, u} (M.cRk X)

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

Result:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ⨆ i, lift.{u, v} #↑↑i ≤ lift.{v, u} (⨆ B, #↑↑B) ∧ lift.{v, u} (⨆ B, #↑↑B) ≤ lift.{u, v} (⨆ B, #↑↑B)

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
hIX : M.IsBasis I X
hXX' : f '' X = f '' X
⊢ #↑I ≤ ⨆ B, #↑↑B

Tactic:
exact hIX.cardinalMk_le_cRk

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ #↑I ≤ ⨆ B, #↑↑B

Tactic:
obtain rfl : X = X' := by rwa [hf.image_eq_image_iff hX hIX.subset_ground] at hXX'

Result:
case refine_1.intro.intro.intro.intro
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
hIX : M.IsBasis I X
hXX' : f '' X = f '' X
⊢ #↑I ≤ ⨆ B, #↑↑B

Proof state:
case refine_2
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.IsBasis I X
⊢ lift.{v, u} #↑I ≤ lift.{u, v} (⨆ B, #↑↑B)

Tactic:
rw [← mk_image_eq_of_injOn_lift _ _ (hf.mono hI.indep.subset_ground), lift_le]

Result:
case refine_2
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.IsBasis I X
⊢ #↑(f '' I) ≤ ⨆ B, #↑↑B

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

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

Result:
case refine_1
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set β
hI : (M.map f hf).IsBasis I (f '' X)
⊢ lift.{u, v} #↑I ≤ lift.{v, u} (⨆ B, #↑↑B)

case refine_2
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.IsBasis I X
⊢ lift.{v, u} #↑I ≤ lift.{u, v} (⨆ B, #↑↑B)

Proof state:
case refine_2
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.IsBasis I X
⊢ #↑(f '' I) ≤ ⨆ B, #↑↑B

Tactic:
exact (hI.map hf).cardinalMk_le_cRk

Result:
no goals

Proof state:
case refine_1
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set β
hI : (M.map f hf).IsBasis I (f '' X)
⊢ lift.{u, v} #↑I ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
obtain ⟨I, X', hIX, rfl, hXX'⟩ := map_isBasis_iff'.1 hI

Result:
case refine_1.intro.intro.intro.intro
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ lift.{u, v} #↑(f '' I) ≤ lift.{v, u} (⨆ B, #↑↑B)

Proof state:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ⨆ i, lift.{u, v} #↑↑i ≤ lift.{v, u} (⨆ B, #↑↑B) ∧ lift.{v, u} (⨆ B, #↑↑B) ≤ lift.{u, v} (⨆ B, #↑↑B)

Tactic:
nth_rw 2 [lift_iSup (bddAbove_range _)]

Result:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ⨆ i, lift.{u, v} #↑↑i ≤ lift.{v, u} (⨆ B, #↑↑B) ∧ ⨆ i, lift.{v, u} #↑↑i ≤ lift.{u, v} (⨆ B, #↑↑B)

Proof state:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ X = X'

Tactic:
rwa [hf.image_eq_image_iff hX hIX.subset_ground] at hXX'

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ⨆ i, lift.{u, v} #↑↑i ≤ lift.{v, u} (⨆ B, #↑↑B) ∧ ⨆ i, lift.{v, u} #↑↑i ≤ lift.{u, v} (⨆ B, #↑↑B)

Tactic:
simp only [ciSup_le_iff (bddAbove_range _), ge_iff_le, Subtype.forall, isBase_restrict_iff',
  isBasis'_iff_isBasis hX, isBasis'_iff_isBasis (show f '' X ⊆ (M.map f hf).E from image_mono hX)]

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

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ lift.{u, v} #↑(f '' I) ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
rw [mk_image_eq_of_injOn_lift _ _ (hf.mono hIX.indep.subset_ground), lift_le]

Result:
case refine_1.intro.intro.intro.intro
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ #↑I ≤ ⨆ B, #↑↑B