awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B_1 B'_1 X Y : Set α
inst : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite.{u + 1} (↑(B' \ B) : Type u)
S : (a : α) → (ha : a ∈ B' \ B) → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite.{u + 1} (↑(S a ha) : Type u)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ (a : (↑(B' \ B) : Type u)), S (↑a : α) ⋯
hUB : B ∩ B' ∪ U ⊆ B
hBU : ¬B ⊆ B ∩ B' ∪ U
a : α
ha : a ∈ B' \ (B ∩ B' ∪ U)
ind : N.Indep (insert a (B ∩ B' ∪ U))
this : a ∈ B' \ B
⊢ S a this ⊆ U

Tactic:
exact subset_iUnion_of_subset ⟨a, this⟩ subset_rfl

Premises used: Set.subset_iUnion_of_subset, subset_rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M_1 : Matroid α
I J B B' X Y : Set α
M : Matroid α
inst : M.InvariantCardinalRank
hf : InjOn f M.E
⊢ (M.map f hf).InvariantCardinalRank

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

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

Tactic:
refine ⟨fun I J X hI hJ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid α
inst : M.InvariantCardinalRank
hf : InjOn f M.E
I J X : Set β
hI : (M.map f hf).IsBasis I X
hJ : (M.map f hf).IsBasis J X
obtain :
  ∀ (I X : Set α) (hIX : M.IsBasis I X) (hJ : (M.map f hf).IsBasis J (f '' X))
    (hI : (M.map f hf).IsBasis (f '' I) (f '' X)), #(↑(f '' I \ J) : Type v) = #(↑(J \ f '' I) : Type v)
⊢ #(↑(I \ J) : Type v) = #(↑(J \ I) : Type v)

Tactic:
obtain ⟨I, X, hIX, rfl, rfl⟩ := 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_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid α
inst : M.InvariantCardinalRank
hf : InjOn f M.E
J : Set β
I X : Set α
hIX : M.IsBasis I X
hJ : (M.map f hf).IsBasis J (f '' X)
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
obtain :
  ∀ (J X' : Set α) (hJX : M.IsBasis J X') (h' : f '' X = f '' X') (hJ : (M.map f hf).IsBasis (f '' J) (f '' X)),
    #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
⊢ #(↑(f '' I \ J) : Type v) = #(↑(J \ f '' I) : Type v)

Tactic:
obtain ⟨J, X', hJX, rfl, h'⟩ := map_isBasis_iff'.1 hJ

Premises used: Iff.mp, Matroid.map_isBasis_iff', rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid α
inst : M.InvariantCardinalRank
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
J X' : Set α
hJX : M.IsBasis J X'
h' : f '' X = f '' X'
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
rwa rwa₁ rwa₂ rwa₃ : ∀ (h' : X = X') (hJ : (M.map f hf).IsBasis (f '' J) (f '' X)), X = X'
⊢ X = X'

Tactic:
rwa [InjOn.image_eq_image_iff hf hIX.subset_ground hJX.subset_ground] at h'

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_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid α
inst : M.InvariantCardinalRank
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
J X' : Set α
hJX : M.IsBasis J X'
h' : f '' X = f '' X'
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
⊢ M.IsBasis J X

Tactic:
obtain rfl : X = X' := by
    rwa [InjOn.image_eq_image_iff hf hIX.subset_ground hJX.subset_ground] at h'

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid α
inst : M.InvariantCardinalRank
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
J X' : Set α
hJX : M.IsBasis J X'
h' : f '' X = f '' X'
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
hJX₁ : M.IsBasis J X
⊢ f '' X = f '' X

Tactic:
obtain rfl : X = X' := by
    rwa [InjOn.image_eq_image_iff hf hIX.subset_ground hJX.subset_ground] at h'

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid α
inst : M.InvariantCardinalRank
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
J : Set α
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
hJX : M.IsBasis J X
h' : f '' X = f '' X
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)

Tactic:
have hcard := hIX.cardinalMk_diff_comm hJX
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid α
inst : M.InvariantCardinalRank
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
J : Set α
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
hJX : M.IsBasis J X
h' : f '' X = f '' X
hcard : #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)
rwa :
  ∀ (hcard : lift.{v, u} #(↑(I \ J) : Type u) = lift.{v, u} #(↑(J \ I) : Type u)),
    #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
rwa₁ :
  ∀ (hcard : lift.{u, v} #(↑(f '' (I \ J)) : Type v) = lift.{v, u} #(↑(J \ I) : Type u)),
    #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
rwa₂ :
  ∀ (hcard : lift.{u, v} #(↑(f '' (I \ J)) : Type v) = lift.{u, v} #(↑(f '' (J \ I)) : Type v)),
    #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
rwa₃ :
  ∀ (hcard : #(↑(f '' (I \ J)) : Type v) = #(↑(f '' (J \ I)) : Type v)),
    #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
rwa₄ :
  ∀ (hcard : #(↑(f '' I \ f '' (I ∩ J)) : Type v) = #(↑(f '' (J \ I)) : Type v)),
    #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
rwa₅ :
  ∀ (hcard : #(↑(f '' I \ f '' (I ∩ J)) : Type v) = #(↑(f '' J \ f '' (J ∩ I)) : Type v)),
    #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
rwa₆ :
  ∀ (hcard : #(↑(f '' I \ f '' (J ∩ I)) : Type v) = #(↑(f '' J \ f '' (J ∩ I)) : Type v)),
    #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
rwa₇ :
  ∀ (hcard : #(↑(f '' I \ (f '' J ∩ f '' I)) : Type v) = #(↑(f '' J \ (f '' J ∩ f '' I)) : Type v)),
    #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
rwa₈ :
  ∀ (hcard : #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ (f '' J ∩ f '' I)) : Type v)),
    #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
rwa₉ rwa₁₀ rwa₁₁ rwa₁₂ :
  ∀ (hcard : #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)),
    #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
⊢ #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)

Tactic:
rwa [← lift_inj.{u, v},
    ← mk_image_eq_of_injOn_lift _ _ (hf.mono ((hIX.indep.diff _).subset_ground)),
    ← mk_image_eq_of_injOn_lift _ _ (hf.mono ((hJX.indep.diff _).subset_ground)),
    lift_inj, (hf.mono hIX.indep.subset_ground).image_diff,
    (hf.mono hJX.indep.subset_ground).image_diff, inter_comm,
    hf.image_inter hJX.indep.subset_ground hIX.indep.subset_ground,
    diff_inter_self_eq_diff, diff_self_inter] at hcard

Premises used: Set.diff_self_inter, Matroid.Indep.diff, Set.InjOn.image_diff, Set.InjOn.image_inter, Cardinal.mk_image_eq_of_injOn_lift, Set.inter_comm, Matroid.Indep.subset_ground, Set.diff_inter_self_eq_diff, Cardinal.lift_inj, Set.InjOn.mono, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f_1 : α → β
M_1 : Matroid α
I J B B' X Y : Set α
M : Matroid β
inst : M.InvariantCardinalRank
f : α → β
⊢ (M.comap f).InvariantCardinalRank

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

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

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

Tactic:
obtain ⟨hI, hfI, hIX⟩ := comap_isBasis_iff.1 hI

Premises used: Matroid.comap_isBasis_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f_1 : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid β
inst : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI : (M.comap f).IsBasis I X
hJ : (M.comap f).IsBasis J X
hI₁ : M.IsBasis (f '' I) (f '' X)
⊢ InjOn f I

Tactic:
obtain ⟨hI, hfI, hIX⟩ := comap_isBasis_iff.1 hI

Premises used: Matroid.comap_isBasis_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f_1 : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid β
inst : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI : (M.comap f).IsBasis I X
hJ : (M.comap f).IsBasis J X
hI₁ : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
⊢ I ⊆ X

Tactic:
obtain ⟨hI, hfI, hIX⟩ := comap_isBasis_iff.1 hI

Premises used: Matroid.comap_isBasis_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f_1 : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid β
inst : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI_1 : (M.comap f).IsBasis I X
hJ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
⊢ M.IsBasis (f '' J) (f '' X)

Tactic:
obtain ⟨hJ, hfJ, hJX⟩ := comap_isBasis_iff.1 hJ

Premises used: Matroid.comap_isBasis_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f_1 : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid β
inst : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI_1 : (M.comap f).IsBasis I X
hJ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ₁ : M.IsBasis (f '' J) (f '' X)
⊢ InjOn f J

Tactic:
obtain ⟨hJ, hfJ, hJX⟩ := comap_isBasis_iff.1 hJ

Premises used: Matroid.comap_isBasis_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f_1 : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid β
inst : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI_1 : (M.comap f).IsBasis I X
hJ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ₁ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
⊢ J ⊆ X

Tactic:
obtain ⟨hJ, hfJ, hJX⟩ := comap_isBasis_iff.1 hJ

Premises used: Matroid.comap_isBasis_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f_1 : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid β
inst : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI_1 : (M.comap f).IsBasis I X
hJ_1 : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
rw : Disjoint (f '' J \ f '' I) ((f '' I ∩ f '' J) \ f '' (J ∩ I))
rw₁ : Disjoint (f '' I \ f '' J) ((f '' J ∩ f '' I) \ f '' (I ∩ J))
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)

Tactic:
rw [← lift_inj.{u, v}, ← mk_image_eq_of_injOn_lift _ _ (hfI.mono diff_subset),
    ← mk_image_eq_of_injOn_lift _ _ (hfJ.mono diff_subset), lift_inj, hfI.image_diff,
    hfJ.image_diff, ← diff_union_diff_cancel inter_subset_left (image_inter_subset f I J),
    inter_comm, diff_inter_self_eq_diff, mk_union_of_disjoint, hI.cardinalMk_diff_comm hJ,
    ← diff_union_diff_cancel inter_subset_left (image_inter_subset f J I), inter_comm,
    diff_inter_self_eq_diff, mk_union_of_disjoint, inter_comm J I]

Premises used: Set.diff_subset, Set.diff_union_diff_cancel, Set.InjOn.image_diff, Matroid.IsBasis.cardinalMk_diff_comm, Cardinal.mk_image_eq_of_injOn_lift, Set.image_inter_subset, Set.inter_subset_left, Cardinal.mk_union_of_disjoint, Set.inter_comm, Set.diff_inter_self_eq_diff, Cardinal.lift_inj, Set.InjOn.mono
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f_1 : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid β
inst : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI_1 : (M.comap f).IsBasis I X
hJ_1 : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' J \ f '' I) ((f '' I ∩ f '' J) \ f '' (J ∩ I))

Tactic:
disjoint_sdiff_left.mono_right (diff_subset.trans inter_subset_left)

Premises used: Set.diff_subset, HasSubset.Subset.trans, Set.inter_subset_left, Set.disjoint_sdiff_left, Disjoint.mono_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f_1 : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid β
inst : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI_1 : (M.comap f).IsBasis I X
hJ_1 : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' J \ f '' I) ((f '' I ∩ f '' J) \ f '' (J ∩ I))

Tactic:
exact disjoint_sdiff_left.mono_right (diff_subset.trans inter_subset_left)

Premises used: Set.diff_subset, HasSubset.Subset.trans, Set.inter_subset_left, Set.disjoint_sdiff_left, Disjoint.mono_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f_1 : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid β
inst : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI_1 : (M.comap f).IsBasis I X
hJ_1 : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' I \ f '' J) ((f '' J ∩ f '' I) \ f '' (I ∩ J))

Tactic:
disjoint_sdiff_left.mono_right (diff_subset.trans inter_subset_left)

Premises used: Set.diff_subset, HasSubset.Subset.trans, Set.inter_subset_left, Set.disjoint_sdiff_left, Disjoint.mono_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
β : Type v
f_1 : α → β
M_1 : Matroid α
I_1 J_1 B B' X_1 Y : Set α
M : Matroid β
inst : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI_1 : (M.comap f).IsBasis I X
hJ_1 : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' I \ f '' J) ((f '' J ∩ f '' I) \ f '' (I ∩ J))

Tactic:
exact disjoint_sdiff_left.mono_right (diff_subset.trans inter_subset_left)

Premises used: Set.diff_subset, HasSubset.Subset.trans, Set.inter_subset_left, Set.disjoint_sdiff_left, Disjoint.mono_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
⊢ M.RankFinite ↔ M.cRank < ℵ₀

Tactic:
⟨fun h ↦ ?_, fun h ↦ ⟨?_⟩⟩

Premises used: Matroid.RankFinite.mk, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
refine_1 : ∀ (h : M.RankFinite), M.cRank < ℵ₀
refine_2 : ∀ (h : M.cRank < ℵ₀), ∃ (B : Set α), M.IsBase B ∧ B.Finite
⊢ M.RankFinite ↔ M.cRank < ℵ₀

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨?_⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
h : M.RankFinite
refine_1 : ∀ (B : Set α) (hB : M.IsBase B) (fin : B.Finite), M.cRank < ℵ₀
⊢ M.cRank < ℵ₀

Tactic:
have ⟨B, hB, fin⟩ := h
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
h : M.RankFinite
B : Set α
hB : M.IsBase B
fin : B.Finite
⊢ M.cRank < ℵ₀

Tactic:
hB.cardinalMk_eq_cRank ▸ lt_aleph0_iff_finite.mpr fin

Premises used: Iff.mpr, Matroid.IsBase.cardinalMk_eq_cRank, Eq.rec, Cardinal.lt_aleph0_iff_finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
h : M.RankFinite
B : Set α
hB : M.IsBase B
fin : B.Finite
⊢ M.cRank < ℵ₀

Tactic:
exact hB.cardinalMk_eq_cRank ▸ lt_aleph0_iff_finite.mpr fin
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
refine_2 : ∀ (B : Set α) (hB : M.IsBase B), ∃ (B : Set α), M.IsBase B ∧ B.Finite
⊢ ∃ (B : Set α), M.IsBase B ∧ B.Finite

Tactic:
have ⟨B, hB⟩ := M.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
B : Set α
hB : M.IsBase B
refine_2 : ∃ (B : Set α), M.IsBase B ∧ #(↑B : Type u) < ℵ₀
⊢ ∃ (B : Set α), M.IsBase B ∧ B.Finite

Tactic:
simp_rw [← finite_coe_iff, ← lt_aleph0_iff_finite]

Premises used: Set.finite_coe_iff, Cardinal.lt_aleph0_iff_finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
B : Set α
hB : M.IsBase B
⊢ ∃ (B : Set α), M.IsBase B ∧ #(↑B : Type u) < ℵ₀

Tactic:
⟨B, hB, hB.cardinalMk_le_cRank.trans_lt h⟩

Premises used: Matroid.IsBase.cardinalMk_le_cRank, And.intro, Exists.intro, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
B : Set α
hB : M.IsBase B
⊢ ∃ (B : Set α), M.IsBase B ∧ #(↑B : Type u) < ℵ₀

Tactic:
exact ⟨B, hB, hB.cardinalMk_le_cRank.trans_lt h⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
rw : M.RankInfinite ↔ ¬M.cRank < ℵ₀
rw₁ : M.RankInfinite ↔ ¬M.RankFinite
rw₂ rw₃ : M.RankInfinite ↔ M.RankInfinite
⊢ M.RankInfinite ↔ ℵ₀ ≤ M.cRank

Tactic:
rw [← not_lt, ← rankFinite_iff_cRank_lt_aleph0, not_rankFinite_iff]

Premises used: not_lt, Matroid.rankFinite_iff_cRank_lt_aleph0, Matroid.not_rankFinite_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X : Set α
rw : (M ↾ X).RankFinite ↔ M.cRk X < ℵ₀
rw₁ : (M ↾ X).cRank < ℵ₀ ↔ M.cRk X < ℵ₀
rw₂ rw₃ : M.cRk X < ℵ₀ ↔ M.cRk X < ℵ₀
⊢ M.IsRkFinite X ↔ M.cRk X < ℵ₀

Tactic:
rw [IsRkFinite, rankFinite_iff_cRank_lt_aleph0, cRank_restrict]

Premises used: Matroid.cRank_restrict, Matroid.rankFinite_iff_cRank_lt_aleph0, Matroid.IsRkFinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I : Set α
inst : M.RankFinite
ind : M.Indep I
le : M.cRank ≤ #(↑I : Type u)
⊢ M.IsBase I

Tactic:
ind.isBase_of_maximal fun _J ind_J hIJ ↦ ind.finite.eq_of_subset_of_encard_le hIJ <|
    toENat.monotone' <| ind_J.cardinalMk_le_cRank.trans le

Premises used: Matroid.Indep.isBase_of_maximal, Matroid.Indep.finite, Matroid.Indep.cardinalMk_le_cRank, OrderRingHom.monotone', Cardinal.toENat, LE.le.trans, Set.Finite.eq_of_subset_of_encard_le
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X : Set α
inst : M.RankFinite
h : M.Spanning X
le : #(↑X : Type u) ≤ M.cRank
have : ∀ (B : Set α) (hB : M.IsBase B) (hBX : B ⊆ X), M.IsBase X
⊢ M.IsBase X

Tactic:
have ⟨B, hB, hBX⟩ := h.exists_isBase_subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X : Set α
inst : M.RankFinite
h : M.Spanning X
le : #(↑X : Type u) ≤ M.cRank
B : Set α
hB : M.IsBase B
hBX : B ⊆ X
rwa rwa₁ rwa₂ rwa₃ : M.IsBase B
⊢ M.IsBase X

Tactic:
rwa [← hB.finite.eq_of_subset_of_encard_le hBX
    (toENat.monotone' <| le.trans hB.cardinalMk_eq_cRank.ge)]

Premises used: Eq.ge, Matroid.IsBase.cardinalMk_eq_cRank, OrderRingHom.monotone', Cardinal.toENat, LE.le.trans, Set.Finite.eq_of_subset_of_encard_le, Matroid.IsBase.finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
I : Set α
ind : M.Indep I
le : M.cRank ≤ #(↑I : Type u)
fin : I.Finite
⊢ M.IsBase I

Tactic:
have := rankFinite_iff_cRank_lt_aleph0.mpr (le.trans_lt <| lt_aleph0_iff_finite.mpr fin)
  ind.isBase_of_cRank_le le

Premises used: Iff.mpr, Matroid.Indep.isBase_of_cRank_le, Cardinal.lt_aleph0_iff_finite, Matroid.rankFinite_iff_cRank_lt_aleph0, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X : Set α
h : M.Spanning X
le : #(↑X : Type u) ≤ M.cRank
fin : X.Finite
⊢ M.IsBase X

Tactic:
have ⟨_B, hB, hBX⟩ := h.exists_isBase_subset
  have := hB.rankFinite_of_finite (fin.subset hBX)
  h.isBase_of_le_cRank le

Premises used: Matroid.IsBase.rankFinite_of_finite, Matroid.IsBase, Set.Finite.subset, Matroid.Spanning.exists_isBase_subset, _private.0.Matroid.Spanning.cRank_le_cardinalMk.match_1, Matroid.Spanning.isBase_of_le_cRank
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
inl : ∀ (h : M.RankFinite), (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank
inr : ∀ (h : M.RankInfinite), (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank

Tactic:
obtain h | h := M.rankFinite_or_rankInfinite

Premises used: Matroid.rankFinite_or_rankInfinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
h : M.RankFinite
inl : ∀ (B : Set α) (hB : M.IsBase B), (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank

Tactic:
obtain ⟨B, hB⟩ := M.exists_isBase

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
h : M.RankFinite
B : Set α
hB : M.IsBase B
inl : (toENat : (a : Cardinal.{u}) → ℕ∞) #(↑B : Type u) = M.eRank
inl₁ : (toENat : (a : Cardinal.{u}) → ℕ∞) #(↑B : Type u) = B.encard
inl₂ inl₃ : B.encard = B.encard
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank

Tactic:
rw [← hB.cardinalMk_eq_cRank, ← hB.encard_eq_eRank, toENat_cardinalMk]

Premises used: Matroid.IsBase.encard_eq_eRank, Matroid.IsBase.cardinalMk_eq_cRank, Set.toENat_cardinalMk
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
h : M.RankInfinite
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank

Tactic:
simp [rankInfinite_iff_aleph0_le_cRank.1 h]

Premises used: Matroid.rankInfinite_iff_aleph0_le_cRank, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal
Goal:
α : Type u
M : Matroid α
X : Set α
rw : (toENat : (a : Cardinal.{u}) → ℕ∞) (M ↾ X).cRank = M.eRk X
rw₁ : (M ↾ X).eRank = M.eRk X
rw₂ rw₃ : (M ↾ X).eRank = (M ↾ X).eRank
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) (M.cRk X) = M.eRk X

Tactic:
rw [cRk, toENat_cRank_eq, eRk]

Premises used: Matroid.cRk, Matroid.eRk, Matroid.toENat_cRank_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
rw : M.eRank = (M ↾ M.E).eRank
rw₁ rw₂ : M.eRank = M.eRank
⊢ M.eRank = M.eRk M.E

Tactic:
rw [eRk, restrict_ground_eq_self]

Premises used: Matroid.restrict_ground_eq_self, Matroid.eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
⊢ M.eRk M.E = M.eRank

Tactic:
M.eRank_def.symm

Premises used: Matroid.eRank_def, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ (M ↾ X).eRank = M.eRk X

Tactic:
rfl

Premises used: Matroid.eRk, rfl
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B.encard = M.eRank

Tactic:
simp [eRank, show ∀ B' : {B // M.IsBase B}, B'.1.encard = B.encard from
    fun B' ↦ B'.2.encard_eq_encard_of_isBase hB]

Premises used: Matroid.IsBase.encard_eq_encard_of_isBase, Matroid.eRank, Subtype.property
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ I.encard = M.eRk X

Tactic:
hI.isBase_restrict.encard_eq_eRank

Premises used: Matroid.IsBase.encard_eq_eRank, Matroid.IsBasis'.isBase_restrict, Matroid.eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ I.encard = M.eRk X

Tactic:
hI.isBasis'.encard_eq_eRk

Premises used: Matroid.IsBasis.isBasis', Matroid.IsBasis'.encard_eq_eRk