awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
⊢ (M.map f hf).cRk X = M.cRk (f ⁻¹' X)
have rw₁ : (M.map f hf).cRk X = (M.map f hf).cRk (f '' (f ⁻¹' X ∩ M.E))
Tactic: rw [← M.cRk_inter_ground, ← M.cRk_map_image hf _, image_preimage_inter, ← map_ground _ _ hf,
    cRk_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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))
⊢ (M.map f hf).cRk X = M.cRk (f ⁻¹' X)
have rw₂ : (M.map f hf).cRk X = (M.map f hf).cRk (X ∩ f '' M.E)
Tactic: rw [← M.cRk_inter_ground, ← M.cRk_map_image hf _, image_preimage_inter, ← map_ground _ _ hf,
    cRk_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
⊢ (M.map f hf).cRk X = M.cRk (f ⁻¹' X)
have rw₃ : (M.map f hf).cRk X = (M.map f hf).cRk (X ∩ (M.map f hf).E)
Tactic: rw [← M.cRk_inter_ground, ← M.cRk_map_image hf _, image_preimage_inter, ← map_ground _ _ hf,
    cRk_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
⊢ (M.map f hf).cRk X = M.cRk (f ⁻¹' X)
have rw₄ : (M.map f hf).cRk X = (M.map f hf).cRk X
Tactic: rw [← M.cRk_inter_ground, ← M.cRk_map_image hf _, image_preimage_inter, ← map_ground _ _ hf,
    cRk_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ lift.{v, u} ((M.comap f).cRk X) = lift.{u, v} (M.cRk (f '' X))
have 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))
Tactic: nth_rw 1 [cRk, cRank, le_antisymm_iff, lift_iSup bddAbove_of_small, cRk, cRank, cRk, cRank]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ ⨆ (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))
have 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))
Tactic: nth_rw 2 [lift_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ ⨆ (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))
have 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))
Tactic: simp only [ciSup_le_iff bddAbove_of_small, Subtype.forall, isBase_restrict_iff',
    comap_isBasis'_iff, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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))
have 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))
Tactic: refine ⟨fun I hI hfI hIX ↦ ?_, fun I hIX ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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))
⊢ (∀ (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))
have 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))
Tactic: refine ⟨fun I hI hfI hIX ↦ ?_, fun I hIX ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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
⊢ lift.{v, u} #(↑I : Type u) ≤ lift.{u, v} (⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v))
have refine_1 : #(↑(f '' I) : Type v) ≤ ⨆ (B : { B : Set β // (M ↾ f '' X).IsBase B }), #(↑(↑B : Set β) : Type v)
Tactic: rw [← mk_image_eq_of_injOn_lift _ _ hfI, lift_le]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
⊢ ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀
have 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₀
Tactic: obtain ⟨I₀, hI₀ss, hbij⟩ := exists_subset_bijOn (f ⁻¹' I ∩ X) f
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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₀
have refine : f '' I₀ = I
Tactic: refine ⟨I₀, hI₀ss.trans inter_subset_right, ?_, hbij.injOn⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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))
⊢ f '' I₀ = I
have rw : f '' (f ⁻¹' I ∩ X) = I
Tactic: rw [hbij.image_eq, image_preimage_inter, inter_eq_self_of_subset_left hIX.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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
⊢ f '' I₀ = I
have rw₁ : I ∩ f '' X = I
Tactic: rw [hbij.image_eq, image_preimage_inter, inter_eq_self_of_subset_left hIX.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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
⊢ f '' I₀ = I
have rw₂ : I = I
Tactic: rw [hbij.image_eq, image_preimage_inter, inter_eq_self_of_subset_left hIX.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
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))
have 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))
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]
Cleared hypotheses: I, hIX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
⊢ lift.{u, v} #(↑(f '' I₀) : Type v) ≤
    lift.{v, u} (⨆ (B : { B : Set α // (M.comap f ↾ X).IsBase B }), #(↑(↑B : Set α) : Type u))
have refine_2 : #(↑I₀ : Type 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
have rw : #(↑(I \ J ∪ I ∩ J) : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
⊢ #(↑I : Type u) = #(↑J : Type u)
have rw₁ : #(↑(I \ J) : Type u) + #(↑(I ∩ J) : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
⊢ #(↑I : Type u) = #(↑J : Type u)
have rw₂ : #(↑(J \ I) : Type u) + #(↑(I ∩ J) : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
⊢ #(↑I : Type u) = #(↑J : Type u)
have rw₃ : #(↑(J \ I ∪ I ∩ J) : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
⊢ #(↑I : Type u) = #(↑J : Type u)
have rw₄ : #(↑(J \ I ∪ J ∩ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
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)
⊢ #(↑I : Type u) = #(↑J : Type u)
have rw₅ : #(↑J : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
Goal:
α : Type u
M : Matroid α
B : Set α
inst : M.InvariantCardinalRank
hB : M.IsBase B
⊢ #(↑B : Type u) = M.cRank
have hrw : ∀ (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
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B B' X Y : Set α
inst : M.InvariantCardinalRank
⊢ (M ↾ X).InvariantCardinalRank
have 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)
Tactic: refine ⟨fun I J Y hI hJ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)
have hI₁ : M.IsBasis I (Y ∩ M.E) ∧ Y ⊆ X
Tactic: rw [isBasis_restrict_iff'] at hI hJ
Cleared hypotheses: hI, hJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (hypothesis)
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
⊢ #(↑(I \ J) : Type u) = #(↑(J \ I) : Type u)
have hJ₁ : M.IsBasis J (Y ∩ M.E) ∧ Y ⊆ X
Tactic: rw [isBasis_restrict_iff'] at hI hJ
Cleared hypotheses: hI, hJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
I X : Set α
inst : M.InvariantCardinalRank
hIX : M.IsBasis' I X
⊢ #(↑I : Type u) = M.cRk X
have rw : #(↑I : Type u) = (M ↾ X).cRank
Tactic: rw [cRk, (isBase_restrict_iff'.2 hIX).cardinalMk_eq_cRank]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
I X : Set α
inst : M.InvariantCardinalRank
hIX : M.IsBasis' I X
rw : #(↑I : Type u) = (M ↾ X).cRank
⊢ #(↑I : Type u) = M.cRk X
have rw₁ : (M ↾ X).cRank = (M ↾ X).cRank
Tactic: rw [cRk, (isBase_restrict_iff'.2 hIX).cardinalMk_eq_cRank]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X : Set α
⊢ M.cRk (M.closure X) = M.cRk X
have obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.cRk (M.closure X) = M.cRk X
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis' X
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X I : Set α
hI : M.IsBasis' I X
⊢ M.cRk (M.closure X) = M.cRk X
have rw : #(↑I : Type u) = M.cRk X
Tactic: rw [← hI.isBasis_closure_right.cardinalMk_eq_cRk, ← hI.cardinalMk_eq_cRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X I : Set α
hI : M.IsBasis' I X
rw : #(↑I : Type u) = M.cRk X
⊢ M.cRk (M.closure X) = M.cRk X
have rw₁ : #(↑I : Type u) = #(↑I : Type u)
Tactic: rw [← hI.isBasis_closure_right.cardinalMk_eq_cRk, ← hI.cardinalMk_eq_cRk]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X Y : Set α
inst : M.InvariantCardinalRank
hXY : M.closure X = M.closure Y
⊢ M.cRk X = M.cRk Y
have rw : M.cRk (M.closure X) = M.cRk Y
Tactic: rw [← cRk_closure, hXY, cRk_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X Y : Set α
inst : M.InvariantCardinalRank
hXY : M.closure X = M.closure Y
rw : M.cRk (M.closure X) = M.cRk Y
⊢ M.cRk X = M.cRk Y
have rw₁ : M.cRk (M.closure Y) = M.cRk Y
Tactic: rw [← cRk_closure, hXY, cRk_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
X Y : Set α
inst : M.InvariantCardinalRank
hXY : M.closure X = M.closure Y
rw : M.cRk (M.closure X) = M.cRk Y
rw₁ : M.cRk (M.closure Y) = M.cRk Y
⊢ M.cRk X = M.cRk Y
have rw₂ : M.cRk Y = M.cRk Y
Tactic: rw [← cRk_closure, hXY, cRk_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
e : α
X : Set α
⊢ M.cRk (insert e (M.closure X)) = M.cRk (insert e X)
have rw : M.cRk (M.closure X ∪ {e}) = M.cRk (insert e X)
Tactic: rw [← union_singleton, cRk_union_closure_left_eq, union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
e : α
X : Set α
rw : M.cRk (M.closure X ∪ {e}) = M.cRk (insert e X)
⊢ M.cRk (insert e (M.closure X)) = M.cRk (insert e X)
have rw₁ : M.cRk (X ∪ {e}) = M.cRk (insert e X)
Tactic: rw [← union_singleton, cRk_union_closure_left_eq, union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
e : α
X : Set α
rw : M.cRk (M.closure X ∪ {e}) = M.cRk (insert e X)
rw₁ : M.cRk (X ∪ {e}) = M.cRk (insert e X)
⊢ M.cRk (insert e (M.closure X)) = M.cRk (insert e X)
have rw₂ : M.cRk (insert e X) = M.cRk (insert e X)
Tactic: rw [← union_singleton, cRk_union_closure_left_eq, union_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X Y : Set α
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y
have obtain : ∀ (Ii : Set α) (hIi : M.IsBasis' Ii (X ∩ Y)), M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y
Tactic: obtain ⟨Ii, hIi⟩ := M.exists_isBasis' (X ∩ Y)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y
have obtain : ∀ (IX : Set α) (hIX : M.IsBasis' IX X) (hIX' : Ii ⊆ IX), M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y
Tactic: obtain ⟨IX, hIX, hIX'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_left)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y
have obtain : ∀ (IY : Set α) (hIY : M.IsBasis' IY Y) (hIY' : Ii ⊆ IY), M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y
Tactic: obtain ⟨IY, hIY, hIY'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_right)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
M : Matroid α
inst : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y
have rw : M.cRk (IX ∪ IY) + #(↑Ii : Type u) ≤ #(↑(IX ∪ IY) : Type u) + #(↑(IX ∩ IY) : Type u)
Tactic: rw [← cRk_union_closure_eq, ← hIX.closure_eq_closure, ← hIY.closure_eq_closure,
    cRk_union_closure_eq, ← hIi.cardinalMk_eq_cRk, ← hIX.cardinalMk_eq_cRk,
    ← hIY.cardinalMk_eq_cRk, ← mk_union_add_mk_inter, add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Rank.Cardinal (goal)
Goal:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B B' X Y : Set α
inst : M.Finitary
⊢ M.InvariantCardinalRank
have suffices : ∀ ⦃B B' : Set α⦄ ⦃N : Matroid α⦄, N.Finitary → N.IsBase B → N.IsBase B' → #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
Tactic: suffices aux : ∀ ⦃B B'⦄ ⦃N : Matroid α⦄, Finitary N → N.IsBase B → N.IsBase B' →
      #(B \ B' : Set α) ≤ #(B' \ B : Set α) from
    ⟨fun I J X hI hJ ↦ (aux (restrict_finitary X) hI.isBase_restrict hJ.isBase_restrict).antisymm
      (aux (restrict_finitary X) hJ.isBase_restrict hI.isBase_restrict)⟩
-- 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'
⊢ #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
have pos : ∀ (h : (B' \ B).Finite), #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
Tactic: by_cases h : (B' \ B).Finite
-- 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'
pos : ∀ (h : (B' \ B).Finite), #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
⊢ #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
have neg : ∀ (h : ¬(B' \ B).Finite), #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
Tactic: by_cases h : (B' \ B).Finite
-- 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 : (B' \ B).Finite
⊢ #(↑(B \ B') : Type u) ≤ #(↑(B' \ B) : Type u)
have pos : (B \ B').Finite
Tactic: rw [← cast_ncard h, ← cast_ncard, hB.ncard_diff_comm hB']