awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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 : ¬(B' \ B).Finite
⊢ #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
have h₁ : Infinite.{u + 1} (↑(B' \ B) : Type u)
Tactic: rw [← Set.Infinite, ← infinite_coe_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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)
a : α
ha : a ∈ B' \ B
⊢ ∃ (S : Set α), Finite.{u + 1} (↑S : Type u) ∧ S ⊆ B ∧ ¬N.Indep (insert a S)
have this : ¬N.Indep (insert a B)
Tactic: have := (hB.insert_dep ⟨hB'.subset_ground ha.1, ha.2⟩).1
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
a : α
ha : a ∈ B' \ B
this : ¬N.Indep (insert a B)
⊢ ∃ (S : Set α), Finite.{u + 1} (↑S : Type u) ∧ S ⊆ B ∧ ¬N.Indep (insert a S)
have contrapose! : ∀ (this : ∀ (S : Set α) (_ : Finite.{u + 1} (↑S : Type u)) (_ : S ⊆ B), N.Indep (insert a S)), N.Indep (insert a B)
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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)
⊢ #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
have this : ∀ (a : α) (ha : a ∈ B' \ B), ∃ (S : Set α), Finite.{u + 1} (↑S : Type u) ∧ S ⊆ B ∧ ¬N.Indep (insert a S)
Tactic: have (a : α) (ha : a ∈ B' \ B) : ∃ S : Set α, Finite S ∧ S ⊆ B ∧ ¬ N.Indep (insert a S) := by
    have := (hB.insert_dep ⟨hB'.subset_ground ha.1, ha.2⟩).1
    contrapose! this
    exact Finitary.indep_of_forall_finite _ fun J hJ fin ↦ (this (J \ {a}) fin.diff.to_subtype <|
      diff_singleton_subset_iff.mpr hJ).subset (subset_insert_diff_singleton ..)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
this : ∀ (a : α) (ha : a ∈ B' \ B), ∃ (S : Set α), Finite.{u + 1} (↑S : Type u) ∧ S ⊆ B ∧ ¬N.Indep (insert a S)
⊢ #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
have neg : ∀ (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))),
  #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
Tactic: choose S S_fin hSB dep using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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 : α) ⋯
this : B \ B' ⊆ U
⊢ #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
have refine : max (#(↑(B' \ B) : Type u)) (⨆ (i : (↑(B' \ B) : Type u)), #(↑(S (↑i : α) sorry) : Type u)) ≤ #(↑(B' \ B) : Type u)
Tactic: refine (mk_le_mk_of_subset this).trans <| (mk_iUnion_le ..).trans
      <| (mul_le_max_of_aleph0_le_left (by simp)).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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 : α) ⋯
this : B \ B' ⊆ U
⊢ max (#(↑(B' \ B) : Type u)) (⨆ (i : (↑(B' \ B) : Type u)), #(↑(S (↑i : α) ⋯) : Type u)) ≤ #(↑(B' \ B) : Type u)
have simp : ⨆ (i : (↑(B' \ B) : Type u)), #(↑(S (↑i : α) sorry) : Type u) ≤ #(↑(B' \ B) : Type u)
Tactic: simp only [sup_le_iff, le_refl, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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 : α) ⋯
⊢ #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
have neg : B \ B' ⊆ U
Tactic: suffices B \ B' ⊆ U by
    refine (mk_le_mk_of_subset this).trans <| (mk_iUnion_le ..).trans
      <| (mul_le_max_of_aleph0_le_left (by simp)).trans ?_
    simp only [sup_le_iff, le_refl, true_and]
    exact ciSup_le' fun e ↦ (lt_aleph0_of_finite _).le.trans <| by simp
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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 : α) ⋯
⊢ B \ B' ⊆ U
have neg : B ⊆ B ∩ B' ∪ U
Tactic: rw [← diff_inter_self_eq_diff, diff_subset_iff, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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 : α) ⋯
⊢ B ⊆ B ∩ B' ∪ U
have hUB : B ∩ B' ∪ U ⊆ B
Tactic: have hUB : (B ∩ B') ∪ U ⊆ B :=
    union_subset inter_subset_left (iUnion_subset fun e ↦ (hSB e.1 e.2))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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
⊢ B ⊆ B ∩ B' ∪ U
have neg : ∀ (hBU : ¬B ⊆ B ∩ B' ∪ U), False
Tactic: by_contra hBU
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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
⊢ False
have neg : ∀ (a : α) (ha : a ∈ B' \ (B ∩ B' ∪ U)) (ind : N.Indep (insert a (B ∩ B' ∪ U))), False
Tactic: have ⟨a, ha, ind⟩ := hB.exists_insert_of_ssubset ⟨hUB, hBU⟩ hB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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))
⊢ False
have this : a ∈ B' \ B
Tactic: have : a ∈ B' \ B := ⟨ha.1, fun haB ↦ ha.2 (.inl ⟨haB, ha.1⟩)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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
⊢ False
have neg : S a this ⊆ U
Tactic: refine dep a this (ind.subset <| insert_subset_insert <| .trans ?_ subset_union_right)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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
have 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)
Tactic: refine ⟨fun I J X hI hJ ↦ ?_⟩
-- 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 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)
have 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)
Tactic: obtain ⟨I, X, hIX, rfl, rfl⟩ := map_isBasis_iff'.1 hI
Cleared hypotheses: I, X, hI, hJ
-- 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
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)
⊢ #(↑(f '' I \ J) : Type v) = #(↑(J \ f '' I) : Type v)
have 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)
Tactic: obtain ⟨J, X', hJX, rfl, h'⟩ := map_isBasis_iff'.1 hJ
Cleared hypotheses: J, hJ
-- 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 X' : Set α
hJX : M.IsBasis J X'
h' : f '' X = f '' X'
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
⊢ X = X'
have rwa : ∀ (h' : X = X') (hJ : (M.map f hf).IsBasis (f '' J) (f '' X)), X = X'
Tactic: rwa [InjOn.image_eq_image_iff hf hIX.subset_ground hJX.subset_ground] at h'
Cleared hypotheses: h', hJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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)
⊢ #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
have hJX₁ : 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'
Cleared hypotheses: X', hJX, h'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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 '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
have h'₁ : 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'
Cleared hypotheses: X', hJX, h'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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
⊢ #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
have hcard : #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)
Tactic: have hcard := hIX.cardinalMk_diff_comm hJX
-- 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)
⊢ #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
have 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)
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)
⊢ #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
have 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)
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)
⊢ #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
have 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)
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)
⊢ #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
have rwa₃ : ∀ (hcard : #(↑(f '' (I \ J)) : Type v) = #(↑(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)
⊢ #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
have 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)
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)
⊢ #(↑(f '' I \ f '' J) : Type v) = #(↑(f '' J \ f '' I) : Type v)
have 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)
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