awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
⊢ #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
have 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)
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
Cleared hypotheses: hcard
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
⊢ #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
have 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)
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
Cleared hypotheses: hcard
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
⊢ #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
have 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)
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
Cleared hypotheses: hcard
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
⊢ #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
have 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)
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
Cleared hypotheses: hcard
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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
have 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)
Tactic: refine ⟨fun I J X hI hJ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)
have hI₁ : M.IsBasis (f '' I) (f '' X)
Tactic: obtain ⟨hI, hfI, hIX⟩ := comap_isBasis_iff.1 hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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)
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)
have hfI : InjOn f I
Tactic: obtain ⟨hI, hfI, hIX⟩ := comap_isBasis_iff.1 hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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 \ J) : Type u) = #(↑(J \ I) : Type u)
have hIX : I ⊆ X
Tactic: obtain ⟨hI, hfI, hIX⟩ := comap_isBasis_iff.1 hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)
have hJ₁ : M.IsBasis (f '' J) (f '' X)
Tactic: obtain ⟨hJ, hfJ, hJX⟩ := comap_isBasis_iff.1 hJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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)
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)
have hfJ : InjOn f J
Tactic: obtain ⟨hJ, hfJ, hJX⟩ := comap_isBasis_iff.1 hJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)
have hJX : J ⊆ X
Tactic: obtain ⟨hJ, hfJ, hJX⟩ := comap_isBasis_iff.1 hJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)
have rw : Disjoint (f '' J \ f '' I) ((f '' I ∩ f '' J) \ f '' (J ∩ I))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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))
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)
have rw₁ : Disjoint (f '' I \ f '' J) ((f '' J ∩ f '' I) \ f '' (I ∩ J))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
⊢ M.RankFinite ↔ M.cRank < ℵ₀
have refine_1 : ∀ (h : M.RankFinite), M.cRank < ℵ₀
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
refine_1 : ∀ (h : M.RankFinite), M.cRank < ℵ₀
⊢ M.RankFinite ↔ M.cRank < ℵ₀
have refine_2 : ∀ (h : M.cRank < ℵ₀), ∃ (B : Set α), M.IsBase B ∧ B.Finite
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
h : M.RankFinite
⊢ M.cRank < ℵ₀
have refine_1 : ∀ (B : Set α) (hB : M.IsBase B) (fin : B.Finite), M.cRank < ℵ₀
Tactic: have ⟨B, hB, fin⟩ := h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
⊢ ∃ (B : Set α), M.IsBase B ∧ B.Finite
have refine_2 : ∀ (B : Set α) (hB : M.IsBase B), ∃ (B : Set α), M.IsBase B ∧ B.Finite
Tactic: have ⟨B, hB⟩ := M.exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
B : Set α
hB : M.IsBase B
⊢ ∃ (B : Set α), M.IsBase B ∧ B.Finite
have refine_2 : ∃ (B : Set α), M.IsBase B ∧ #(↑B : Type u) < ℵ₀
Tactic: simp_rw [← finite_coe_iff, ← lt_aleph0_iff_finite]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
⊢ M.RankInfinite ↔ ℵ₀ ≤ M.cRank
have rw : M.RankInfinite ↔ ¬M.cRank < ℵ₀
Tactic: rw [← not_lt, ← rankFinite_iff_cRank_lt_aleph0, not_rankFinite_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
rw : M.RankInfinite ↔ ¬M.cRank < ℵ₀
⊢ M.RankInfinite ↔ ℵ₀ ≤ M.cRank
have rw₁ : M.RankInfinite ↔ ¬M.RankFinite
Tactic: rw [← not_lt, ← rankFinite_iff_cRank_lt_aleph0, not_rankFinite_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
rw : M.RankInfinite ↔ ¬M.cRank < ℵ₀
rw₁ : M.RankInfinite ↔ ¬M.RankFinite
⊢ M.RankInfinite ↔ ℵ₀ ≤ M.cRank
have rw₂ : M.RankInfinite ↔ M.RankInfinite
Tactic: rw [← not_lt, ← rankFinite_iff_cRank_lt_aleph0, not_rankFinite_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X : Set α
⊢ M.IsRkFinite X ↔ M.cRk X < ℵ₀
have rw : (M ↾ X).RankFinite ↔ M.cRk X < ℵ₀
Tactic: rw [IsRkFinite, rankFinite_iff_cRank_lt_aleph0, cRank_restrict]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X : Set α
rw : (M ↾ X).RankFinite ↔ M.cRk X < ℵ₀
⊢ M.IsRkFinite X ↔ M.cRk X < ℵ₀
have rw₁ : (M ↾ X).cRank < ℵ₀ ↔ M.cRk X < ℵ₀
Tactic: rw [IsRkFinite, rankFinite_iff_cRank_lt_aleph0, cRank_restrict]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X : Set α
rw : (M ↾ X).RankFinite ↔ M.cRk X < ℵ₀
rw₁ : (M ↾ X).cRank < ℵ₀ ↔ M.cRk X < ℵ₀
⊢ M.IsRkFinite X ↔ M.cRk X < ℵ₀
have rw₂ : M.cRk X < ℵ₀ ↔ M.cRk X < ℵ₀
Tactic: rw [IsRkFinite, rankFinite_iff_cRank_lt_aleph0, cRank_restrict]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X : Set α
inst : M.RankFinite
h : M.Spanning X
le : #(↑X : Type u) ≤ M.cRank
⊢ M.IsBase X
have have : ∀ (B : Set α) (hB : M.IsBase B) (hBX : B ⊆ X), M.IsBase X
Tactic: have ⟨B, hB, hBX⟩ := h.exists_isBase_subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank
have inl : ∀ (h : M.RankFinite), (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank
Tactic: obtain h | h := M.rankFinite_or_rankInfinite
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
inl : ∀ (h : M.RankFinite), (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank
have inr : ∀ (h : M.RankInfinite), (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank
Tactic: obtain h | h := M.rankFinite_or_rankInfinite
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
h : M.RankFinite
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank
have inl : ∀ (B : Set α) (hB : M.IsBase B), (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank
Tactic: obtain ⟨B, hB⟩ := M.exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
h : M.RankFinite
B : Set α
hB : M.IsBase B
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank
have inl : (toENat : (a : Cardinal.{u}) → ℕ∞) #(↑B : Type u) = M.eRank
Tactic: rw [← hB.cardinalMk_eq_cRank, ← hB.encard_eq_eRank, toENat_cardinalMk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
h : M.RankFinite
B : Set α
hB : M.IsBase B
inl : (toENat : (a : Cardinal.{u}) → ℕ∞) #(↑B : Type u) = M.eRank
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank
have inl₁ : (toENat : (a : Cardinal.{u}) → ℕ∞) #(↑B : Type u) = B.encard
Tactic: rw [← hB.cardinalMk_eq_cRank, ← hB.encard_eq_eRank, toENat_cardinalMk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) M.cRank = M.eRank
have inl₂ : B.encard = B.encard
Tactic: rw [← hB.cardinalMk_eq_cRank, ← hB.encard_eq_eRank, toENat_cardinalMk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X : Set α
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) (M.cRk X) = M.eRk X
have rw : (toENat : (a : Cardinal.{u}) → ℕ∞) (M ↾ X).cRank = M.eRk X
Tactic: rw [cRk, toENat_cRank_eq, eRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X : Set α
rw : (toENat : (a : Cardinal.{u}) → ℕ∞) (M ↾ X).cRank = M.eRk X
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) (M.cRk X) = M.eRk X
have rw₁ : (M ↾ X).eRank = M.eRk X
Tactic: rw [cRk, toENat_cRank_eq, eRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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
⊢ (toENat : (a : Cardinal.{u}) → ℕ∞) (M.cRk X) = M.eRk X
have rw₂ : (M ↾ X).eRank = (M ↾ X).eRank
Tactic: rw [cRk, toENat_cRank_eq, eRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.eRank = M.eRk M.E
have rw : M.eRank = (M ↾ M.E).eRank
Tactic: rw [eRk, restrict_ground_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
rw : M.eRank = (M ↾ M.E).eRank
⊢ M.eRank = M.eRk M.E
have rw₁ : M.eRank = M.eRank
Tactic: rw [eRk, restrict_ground_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
hX : X ⊆ M.E
h : M.eRk X = n
I : Set α
hI : M.IsBasis I X
rw : M.eRk X = n
⊢ I.encard = n
have rw₁ : M.eRk X = M.eRk X
Tactic: rw [hI.encard_eq_eRk, ← h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
hX : X ⊆ M.E
h : ∃ (I : Set α), M.IsBasis I X ∧ I.encard = n
I : Set α
hI : M.IsBasis I X
hIc rw : I.encard = n
⊢ M.eRk X = n
have rw₁ : n = n
Tactic: rw [← hI.encard_eq_eRk, hIc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
⊢ M.eRk I = M.eRk X
have rw : M.eRk I = I.encard
Tactic: rw [← hIX.encard_eq_eRk, hIX.indep.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
rw : M.eRk I = I.encard
⊢ M.eRk I = M.eRk X
have rw₁ : I.encard = I.encard
Tactic: rw [← hIX.encard_eq_eRk, hIX.indep.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ M.eRk I = M.eRk X
have rw : M.eRk I = I.encard
Tactic: rw [← hIX.encard_eq_eRk, hIX.indep.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
rw : M.eRk I = I.encard
⊢ M.eRk I = M.eRk X
have rw₁ : I.encard = I.encard
Tactic: rw [← hIX.encard_eq_eRk, hIX.indep.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
⊢ M.eRk X = I.encard
have rw : M.eRk I = I.encard
Tactic: rw [← hIX.eRk_eq_eRk, hIX.indep.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
rw : M.eRk I = I.encard
⊢ M.eRk X = I.encard
have rw₁ : I.encard = I.encard
Tactic: rw [← hIX.eRk_eq_eRk, hIX.indep.eRk_eq_encard]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.ENat (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ M.eRk X = I.encard
have rw : M.eRk I = I.encard
Tactic: rw [← hIX.eRk_eq_eRk, hIX.indep.eRk_eq_encard]