awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I : Set β
hI : (M.map f hf).IsBasis I (f '' X)
refine_1 :
  ∀ (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) : Type v) ≤
      lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))
⊢ lift.{u, v} #(↑I : Type v) ≤ lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))

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

Premises used: Iff.mp, Matroid.map_isBasis_iff', rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
refine_1 : #(↑I : Type u) ≤ ⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)
⊢ lift.{u, v} #(↑(f '' I) : Type v) ≤ lift.{v, u} (⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))

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

Premises used: Cardinal.mk_image_eq_of_injOn_lift, Matroid.Indep.subset_ground, Set.InjOn.mono, Matroid.IsBasis.indep, Cardinal.lift_le
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
rwa rwa₁ rwa₂ rwa₃ : ∀ (hXX' : X = X') (hI : (M.map f hf).IsBasis (f '' I) (f '' X)), X = X'
⊢ X = X'

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

Premises used: Matroid.IsBasis.subset_ground, Set.InjOn.image_eq_image_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ M.IsBasis I X

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

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
hIX₁ : M.IsBasis I X
⊢ f '' X = f '' X

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

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I : Set α
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
hIX : M.IsBasis I X
hXX' : f '' X = f '' X
⊢ #(↑I : Type u) ≤ ⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)

Tactic:
hIX.cardinalMk_le_cRk

Premises used: Matroid.IsBasis.cardinalMk_le_cRk, Matroid.cRank, Matroid.cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I : Set α
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
hIX : M.IsBasis I X
hXX' : f '' X = f '' X
⊢ #(↑I : Type u) ≤ ⨆ (B : { B : Set α // (M ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)

Tactic:
exact hIX.cardinalMk_le_cRk

Premises used: Matroid.IsBasis.cardinalMk_le_cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
refine_2 : #(↑(f '' I) : Type v) ≤ ⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)
⊢ lift.{v, u} #(↑I : Type u) ≤
    lift.{u, v} (⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))

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

Premises used: Cardinal.mk_image_eq_of_injOn_lift, Matroid.Indep.subset_ground, Set.InjOn.mono, Matroid.IsBasis.indep, Cardinal.lift_le
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ #(↑(f '' I) : Type v) ≤ ⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)

Tactic:
(hI.map hf).cardinalMk_le_cRk

Premises used: Matroid.IsBasis.cardinalMk_le_cRk, Matroid.cRank, Matroid.IsBasis.map, Matroid.cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ #(↑(f '' I) : Type v) ≤ ⨆ (B : { B : Set β // (M.map f hf ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)

Tactic:
exact (hI.map hf).cardinalMk_le_cRk

Premises used: Matroid.IsBasis.cardinalMk_le_cRk, Matroid.IsBasis.map
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α β : Type u
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ (M.map f hf).cRk (f '' X) = M.cRk X

Tactic:
lift_inj.1 <| M.cRk_map_image_lift ..

Premises used: Cardinal.lift_inj, Matroid.cRk_map_image_lift, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α β : Type u
f : α → β
X : Set β
M : Matroid α
hf : InjOn f M.E
rw : (M.map f hf).cRk X = M.cRk (f ⁻¹' X ∩ M.E)
rw₁ : (M.map f hf).cRk X = (M.map f hf).cRk (f '' (f ⁻¹' X ∩ M.E))
rw₂ : (M.map f hf).cRk X = (M.map f hf).cRk (X ∩ f '' M.E)
rw₃ : (M.map f hf).cRk X = (M.map f hf).cRk (X ∩ (M.map f hf).E)
rw₄ rw₅ : (M.map f hf).cRk X = (M.map f hf).cRk X
⊢ (M.map f hf).cRk X = M.cRk (f ⁻¹' X)

Tactic:
rw [← M.cRk_inter_ground, ← M.cRk_map_image hf _, image_preimage_inter, ← map_ground _ _ hf,
    cRk_inter_ground]

Premises used: Matroid.cRk_inter_ground, Matroid.map_ground, Set.image_preimage_inter, Matroid.cRk_map_image
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
nth_rw :
  ⨆ (i : { B : Set α // (M.comap f ↾ X).IsBase B }), lift.{v, u} #(↑(↑i : Set α) : Type u) ≤
      lift.{u, v} (⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)) ∧
    lift.{u, v} (⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)) ≤
      lift.{v, u} (⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))
⊢ 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_of_small, cRk, cRank, cRk, cRank]

Premises used: Cardinal.lift_iSup, Matroid.cRank, le_antisymm_iff, Matroid.cRk, Cardinal.bddAbove_of_small
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
nth_rw :
  ⨆ (i : { B : Set α // (M.comap f ↾ X).IsBase B }), lift.{v, u} #(↑(↑i : Set α) : Type u) ≤
      lift.{u, v} (⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)) ∧
    ⨆ (i : { B : Set β // (M ↾ f '' X).IsBase B }), lift.{u, v} #(↑(↑i : Set β) : Type v) ≤
      lift.{v, u} (⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))
⊢ ⨆ (i : { B : Set α // (M.comap f ↾ X).IsBase B }), lift.{v, u} #(↑(↑i : Set α) : Type u) ≤
      lift.{u, v} (⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)) ∧
    lift.{u, v} (⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)) ≤
      lift.{v, u} (⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))

Tactic:
nth_rw 2 [lift_iSup bddAbove_of_small]

Premises used: Cardinal.lift_iSup, Cardinal.bddAbove_of_small
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
simp :
  (∀ (a : Set α),
      M.IsBasis' (f '' a) (f '' X) →
        InjOn f a →
          a ⊆ X →
            lift.{v, u} #(↑a : Type u) ≤
              lift.{u, v} (⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))) ∧
    ∀ (a : Set β) (b : M.IsBasis' a (f '' X)),
      lift.{u, v} #(↑a : Type v) ≤
        lift.{v, u} (⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))
⊢ ⨆ (i : { B : Set α // (M.comap f ↾ X).IsBase B }), lift.{v, u} #(↑(↑i : Set α) : Type u) ≤
      lift.{u, v} (⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)) ∧
    ⨆ (i : { B : Set β // (M ↾ f '' X).IsBase B }), lift.{u, v} #(↑(↑i : Set β) : Type v) ≤
      lift.{v, u} (⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))

Tactic:
simp only [ciSup_le_iff bddAbove_of_small, Subtype.forall, isBase_restrict_iff',
    comap_isBasis'_iff, and_imp]

Premises used: Matroid.comap_isBasis'_iff, Matroid.isBase_restrict_iff', ciSup_le_iff, and_imp, Subtype.forall, Cardinal.bddAbove_of_small
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : 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 : Type u) ≤
              lift.{u, v} (⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))) ∧
    ∀ (a : Set β) (b : M.IsBasis' a (f '' X)),
      lift.{u, v} #(↑a : Type v) ≤
        lift.{v, u} (⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))

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

Premises used: And.intro
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
refine_1 :
  ∀ (I : Set α) (hI : M.IsBasis' (f '' I) (f '' X)) (hfI : InjOn f I) (hIX : I ⊆ X),
    lift.{v, u} #(↑I : Type u) ≤ lift.{u, v} (⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))
refine_2 :
  ∀ (I : Set β) (hIX : M.IsBasis' I (f '' X)),
    lift.{u, v} #(↑I : Type v) ≤
      lift.{v, u} (⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))
⊢ (∀ (a : Set α),
      M.IsBasis' (f '' a) (f '' X) →
        InjOn f a →
          a ⊆ X →
            lift.{v, u} #(↑a : Type u) ≤
              lift.{u, v} (⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))) ∧
    ∀ (a : Set β) (b : M.IsBasis' a (f '' X)),
      lift.{u, v} #(↑a : Type v) ≤
        lift.{v, u} (⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))

Tactic:
refine ⟨fun I hI hfI hIX ↦ ?_, fun I hIX ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
M : Matroid β
f : α → β
X I : Set α
hI : M.IsBasis' (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
refine_1 : #(↑(f '' I) : Type v) ≤ ⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)
⊢ lift.{v, u} #(↑I : Type u) ≤ lift.{u, v} (⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))

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

Premises used: Cardinal.mk_image_eq_of_injOn_lift, Cardinal.lift_le
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : 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) : Type v) ≤ ⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)

Tactic:
hI.cardinalMk_le_cRk

Premises used: Matroid.cRank, Matroid.cRk, Matroid.IsBasis'.cardinalMk_le_cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : 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) : Type v) ≤ ⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)

Tactic:
exact hI.cardinalMk_le_cRk

Premises used: Matroid.IsBasis'.cardinalMk_le_cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
obtain :
  ∀ (I₀ : Set α) (hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X) (hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))), ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀
⊢ ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀

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

Premises used: Inter.inter, Set.preimage, Set.exists_subset_bijOn
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : 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:
⟨I₀, hI₀ss.trans inter_subset_right, ?_, hbij.injOn⟩

Premises used: HasSubset.Subset.trans, Set.BijOn.injOn, And.intro, Exists.intro, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : 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))
refine : f '' I₀ = I
⊢ ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀

Tactic:
refine ⟨I₀, hI₀ss.trans inter_subset_right, ?_, hbij.injOn⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : 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))
rw : f '' (f ⁻¹' I ∩ X) = I
rw₁ : I ∩ f '' X = I
rw₂ rw₃ : I = I
⊢ f '' I₀ = I

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

Premises used: Set.image_preimage_inter, Set.BijOn.image_eq, Matroid.IsBasis'.subset, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
refine_2 :
  ∀ (I₀ : Set α) (hI₀X : I₀ ⊆ X) (hfI₀ : InjOn f I₀) (hIX : M.IsBasis' (f '' I₀) (f '' X)),
    lift.{u, v} #(↑(f '' I₀) : Type v) ≤
      lift.{v, u} (⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))
⊢ lift.{u, v} #(↑I : Type v) ≤
    lift.{v, u} (⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))

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]

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : 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)
refine_2 : #(↑I₀ : Type u) ≤ ⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)
⊢ lift.{u, v} #(↑(f '' I₀) : Type v) ≤
    lift.{v, u} (⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))

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

Premises used: Cardinal.mk_image_eq_of_injOn_lift, Cardinal.lift_le
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : 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₀ : Type u) ≤ ⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)

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

Premises used: Iff.mpr, Matroid.comap_isBasis'_iff, Matroid.cRank, Matroid.cRk, And.intro, Matroid.IsBasis'.cardinalMk_le_cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : 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₀ : Type u) ≤ ⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u)

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

Premises used: Iff.mpr, Matroid.comap_isBasis'_iff, And.intro, Matroid.IsBasis'.cardinalMk_le_cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α β : Type u
M : Matroid β
f : α → β
X : Set α
⊢ (M.comap f).cRk X = M.cRk (f '' X)

Tactic:
lift_inj.1 <| M.cRk_comap_lift ..

Premises used: Matroid.cRk_comap_lift, Cardinal.lift_inj, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I J X : Set α
inst : M.InvariantCardinalRank
hIX : M.IsBasis I X
hJX : M.IsBasis J X
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)

Tactic:
InvariantCardinalRank.forall_card_isBasis_diff hIX hJX

Premises used: Matroid.InvariantCardinalRank.forall_card_isBasis_diff
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I J X : Set α
inst : M.InvariantCardinalRank
hIX : M.IsBasis' I X
hJX : M.IsBasis' J X
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)

Tactic:
hIX.isBasis_inter_ground.cardinalMk_diff_comm hJX.isBasis_inter_ground

Premises used: Matroid.IsBasis.cardinalMk_diff_comm, Matroid.IsBasis'.isBasis_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
B B' : Set α
inst : M.InvariantCardinalRank
hB : M.IsBase B
hB' : M.IsBase B'
⊢ #(↑(B \ B') : Type u) = #(↑(B' \ B) : Type u)

Tactic:
hB.isBasis_ground.cardinalMk_diff_comm hB'.isBasis_ground

Premises used: Matroid.IsBasis.cardinalMk_diff_comm, Matroid.IsBase.isBasis_ground
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I J X : Set α
inst : M.InvariantCardinalRank
hIX : M.IsBasis I X
hJX : M.IsBasis J X
rw : #(↑(I \ J ∪ I ∩ J) : Type u) = #(↑J : Type u)
rw₁ : #(↑(I \ J) : Type u) + #(↑(I ∩ J) : Type u) = #(↑J : Type u)
rw₂ : #(↑(J \ I) : Type u) + #(↑(I ∩ J) : Type u) = #(↑J : Type u)
rw₃ : #(↑(J \ I ∪ I ∩ J) : Type u) = #(↑J : Type u)
rw₄ : #(↑(J \ I ∪ J ∩ I) : Type u) = #(↑J : Type u)
rw₅ rw₆ : #(↑J : Type u) = #(↑J : Type u)
⊢ #(↑I : Type u) = #(↑J : Type u)

Tactic:
rw [← diff_union_inter I J,
    mk_union_of_disjoint (disjoint_sdiff_left.mono_right inter_subset_right),
    hIX.cardinalMk_diff_comm hJX,
    ← mk_union_of_disjoint (disjoint_sdiff_left.mono_right inter_subset_left),
    inter_comm, diff_union_inter]

Premises used: Matroid.IsBasis.cardinalMk_diff_comm, Set.inter_subset_left, Cardinal.mk_union_of_disjoint, Set.inter_comm, Set.disjoint_sdiff_left, Set.diff_union_inter, Disjoint.mono_right, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I J X : Set α
inst : M.InvariantCardinalRank
hIX : M.IsBasis' I X
hJX : M.IsBasis' J X
⊢ #(↑I : Type u) = #(↑J : Type u)

Tactic:
hIX.isBasis_inter_ground.cardinalMk_eq hJX.isBasis_inter_ground

Premises used: Matroid.IsBasis'.isBasis_inter_ground, Matroid.IsBasis.cardinalMk_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
B B' : Set α
inst : M.InvariantCardinalRank
hB : M.IsBase B
hB' : M.IsBase B'
⊢ #(↑B : Type u) = #(↑B' : Type u)

Tactic:
hB.isBasis_ground.cardinalMk_eq hB'.isBasis_ground

Premises used: Matroid.IsBase.isBasis_ground, Matroid.IsBasis.cardinalMk_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I B : Set α
inst : M.InvariantCardinalRank
hI : M.Indep I
hB : M.IsBase B
⊢ #(↑I : Type u) ≤ #(↑B : Type u)

Tactic:
have ⟨_B', hB', hIB'⟩ := hI.exists_isBase_superset
  hB'.cardinalMk_eq hB ▸ mk_le_mk_of_subset hIB'

Premises used: Cardinal.mk, Eq.rec, Set.Elem, Matroid.IsBase.cardinalMk_eq, LE.le, Matroid.Indep.exists_isBase_superset, _private.0.Matroid.Indep.cardinalMk_le_cRank.match_1, Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I J X : Set α
inst : M.InvariantCardinalRank
hI : M.Indep I
hJ : M.IsBasis' J X
hIX : I ⊆ X
⊢ #(↑I : Type u) ≤ #(↑J : Type u)

Tactic:
have ⟨_J', hJ', hIJ'⟩ := hI.subset_isBasis'_of_subset hIX
  hJ'.cardinalMk_eq hJ ▸ mk_le_mk_of_subset hIJ'

Premises used: Matroid.IsBasis'.cardinalMk_eq, Cardinal.mk, Eq.rec, Set.Elem, LE.le, _private.0.Matroid.Indep.cardinalMk_le_isBasis'.match_1, Matroid.Indep.subset_isBasis'_of_subset, Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I J X : Set α
inst : M.InvariantCardinalRank
hI : M.Indep I
hJ : M.IsBasis J X
hIX : I ⊆ X
⊢ #(↑I : Type u) ≤ #(↑J : Type u)

Tactic:
hI.cardinalMk_le_isBasis' hJ.isBasis' hIX

Premises used: Matroid.IsBasis.isBasis', Matroid.Indep.cardinalMk_le_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
B : Set α
inst : M.InvariantCardinalRank
hB : M.IsBase B
⊢ ∀ (B' : { B : Set α // M.IsBase B }), #(↑(↑B' : Set α) : Type u) = #(↑B : Type u)

Tactic:
have hrw : ∀ B' : {B : Set α // M.IsBase B}, #B' = #B := fun B' ↦ B'.2.cardinalMk_eq hB
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
B : Set α
inst : M.InvariantCardinalRank
hB : M.IsBase B
hrw : ∀ (B' : { B : Set α // M.IsBase B }), #(↑(↑B' : Set α) : Type u) = #(↑B : Type u)
⊢ #(↑B : Type u) = M.cRank

Tactic:
simp [cRank, hrw]

Premises used: Matroid.cRank
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B B' X Y : Set α
inst : M.InvariantCardinalRank
⊢ (M ↾ X).InvariantCardinalRank

Tactic:
⟨fun I J Y hI hJ ↦ ?_⟩

Premises used: Matroid.InvariantCardinalRank.mk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B B' X Y : Set α
inst : M.InvariantCardinalRank
refine :
  ∀ (I J Y : Set α) (hI : (M ↾ X).IsBasis I Y) (hJ : (M ↾ X).IsBasis J Y), #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)
⊢ (M ↾ X).InvariantCardinalRank

Tactic:
refine ⟨fun I J Y hI hJ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I_1 J_1 B B' X Y_1 : Set α
inst : M.InvariantCardinalRank
I J Y : Set α
hI : (M ↾ X).IsBasis I Y
hJ : (M ↾ X).IsBasis J Y
⊢ M.IsBasis I (Y ∩ M.E) ∧ Y ⊆ X

Tactic:
rw [isBasis_restrict_iff'] at hI hJ

Premises used: Matroid.isBasis_restrict_iff'
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I_1 J_1 B B' X Y_1 : Set α
inst : M.InvariantCardinalRank
I J Y : Set α
hI : (M ↾ X).IsBasis I Y
hJ : (M ↾ X).IsBasis J Y
hI₁ : M.IsBasis I (Y ∩ M.E) ∧ Y ⊆ X
⊢ M.IsBasis J (Y ∩ M.E) ∧ Y ⊆ X

Tactic:
rw [isBasis_restrict_iff'] at hI hJ

Premises used: Matroid.isBasis_restrict_iff'
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I_1 J_1 B B' X Y_1 : Set α
inst : M.InvariantCardinalRank
I J Y : Set α
hI : M.IsBasis I (Y ∩ M.E) ∧ Y ⊆ X
hJ : M.IsBasis J (Y ∩ M.E) ∧ Y ⊆ X
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)

Tactic:
hI.1.cardinalMk_diff_comm hJ.1

Premises used: Matroid.IsBasis.cardinalMk_diff_comm, And.left
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I_1 J_1 B B' X Y_1 : Set α
inst : M.InvariantCardinalRank
I J Y : Set α
hI : M.IsBasis I (Y ∩ M.E) ∧ Y ⊆ X
hJ : M.IsBasis J (Y ∩ M.E) ∧ Y ⊆ X
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)

Tactic:
exact hI.1.cardinalMk_diff_comm hJ.1

Premises used: Matroid.IsBasis.cardinalMk_diff_comm, And.left
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I X : Set α
inst : M.InvariantCardinalRank
hIX : M.IsBasis' I X
rw : #(↑I : Type u) = (M ↾ X).cRank
rw₁ rw₂ : (M ↾ X).cRank = (M ↾ X).cRank
⊢ #(↑I : Type u) = M.cRk X

Tactic:
rw [cRk, (isBase_restrict_iff'.2 hIX).cardinalMk_eq_cRank]

Premises used: Iff.mpr, Matroid.isBase_restrict_iff', Matroid.IsBase.cardinalMk_eq_cRank, Matroid.cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I X : Set α
inst : M.InvariantCardinalRank
hIX : M.IsBasis I X
⊢ #(↑I : Type u) = M.cRk X

Tactic:
hIX.isBasis'.cardinalMk_eq_cRk

Premises used: Matroid.IsBasis.isBasis', Matroid.IsBasis'.cardinalMk_eq_cRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X : Set α
obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.cRk (M.closure X) = M.cRk X
⊢ M.cRk (M.closure X) = M.cRk X

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X

Premises used: Matroid.exists_isBasis'