awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
h : X ∩ M.E ⊆ M.loops
e : α
heI : e ∈ I
⊢ False

Tactic:
(hI.indep.isNonloop_of_mem heI).not_isLoop (h (hI.subset heI))

Premises used: Matroid.IsBasis.subset, Matroid.IsNonloop.not_isLoop, Matroid.Indep.isNonloop_of_mem, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
h : X ∩ M.E ⊆ M.loops
e : α
heI : e ∈ I
⊢ False

Tactic:
exact (hI.indep.isNonloop_of_mem heI).not_isLoop (h (hI.subset heI))

Premises used: Matroid.IsBasis.subset, Matroid.IsNonloop.not_isLoop, Matroid.Indep.isNonloop_of_mem, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
rw : X ∩ M.E ⊆ M.loops ↔ X ⊆ M.loops
rw₁ rw₂ : X ⊆ M.loops ↔ X ⊆ M.loops
⊢ M.eRk X = 0 ↔ X ⊆ M.loops

Tactic:
rw [eRk_eq_zero_iff', inter_eq_self_of_subset_left hX]

Premises used: Matroid.eRk_eq_zero_iff', Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
⊢ M.eRk M.loops = 0

Tactic:
simp [eRk_eq_zero_iff']

Premises used: Matroid.eRk_eq_zero_iff'
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
obtain : ∀ (Ii : Set α) (hIi : M.IsBasis' Ii (X ∩ Y)), M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
⊢ M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y

Tactic:
obtain ⟨Ii, hIi⟩ := M.exists_isBasis' (X ∩ Y)

Premises used: Inter.inter, Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
obtain : ∀ (IX : Set α) (hIX : M.IsBasis' IX X) (hIX' : Ii ⊆ IX), M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
⊢ M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y

Tactic:
obtain ⟨IX, hIX, hIX'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_left)

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Matroid.IsBasis'.indep, Matroid.Indep.subset_isBasis'_of_subset, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
obtain : ∀ (IY : Set α) (hIY : M.IsBasis' IY Y) (hIY' : Ii ⊆ IY), M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
⊢ M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y

Tactic:
obtain ⟨IY, hIY, hIY'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_right)

Premises used: HasSubset.Subset.trans, Matroid.IsBasis'.indep, Matroid.Indep.subset_isBasis'_of_subset, Matroid.IsBasis'.subset, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
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
rw : M.eRk (IX ∪ IY) + Ii.encard ≤ (IX ∪ IY).encard + (IX ∩ IY).encard
⊢ M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y

Tactic:
rw [← hIX.eRk_eq_eRk_union, union_comm, ← hIY.eRk_eq_eRk_union, ← hIi.encard_eq_eRk,
    ← hIX.encard_eq_eRk, ← hIY.encard_eq_eRk, union_comm, ← encard_union_add_encard_inter, add_comm]

Premises used: Set.encard_union_add_encard_inter, Matroid.IsBasis'.encard_eq_eRk, Set.union_comm, add_comm, Matroid.IsBasis'.eRk_eq_eRk_union
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
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.eRk (IX ∪ IY) + Ii.encard ≤ (IX ∪ IY).encard + (IX ∩ IY).encard

Tactic:
add_le_add (eRk_le_encard _ _) (encard_mono (subset_inter hIX' hIY'))

Premises used: add_le_add, Set.encard_mono, Set.subset_inter, Matroid.eRk_le_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
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.eRk (IX ∪ IY) + Ii.encard ≤ (IX ∪ IY).encard + (IX ∩ IY).encard

Tactic:
exact add_le_add (eRk_le_encard _ _) (encard_mono (subset_inter hIX' hIY'))

Premises used: add_le_add, Set.encard_mono, Set.subset_inter, Matroid.eRk_le_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
e : α
M : Matroid α
X Y : Set α
rw : M.eRk (insert e X ∩ insert e Y) + M.eRk (insert e X ∪ insert e Y) ≤ M.eRk (insert e X) + M.eRk (insert e Y)
⊢ M.eRk (insert e (X ∩ Y)) + M.eRk (insert e (X ∪ Y)) ≤ M.eRk (insert e X) + M.eRk (insert e Y)

Tactic:
rw [insert_inter_distrib, insert_union_distrib]

Premises used: Set.insert_inter_distrib, Set.insert_union_distrib
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (insert e X ∩ insert e Y) + M.eRk (insert e X ∪ insert e Y) ≤ M.eRk (insert e X) + M.eRk (insert e Y)

Tactic:
apply M.eRk_submod

Premises used: Matroid.eRk_submod
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
rw : M.eRk (M.E \ X ∩ (M.E \ Y)) + M.eRk (M.E \ X ∪ M.E \ Y) ≤ M.eRk (M.E \ X) + M.eRk (M.E \ Y)
⊢ M.eRk (M.E \ (X ∪ Y)) + M.eRk (M.E \ (X ∩ Y)) ≤ M.eRk (M.E \ X) + M.eRk (M.E \ Y)

Tactic:
rw [← diff_inter_diff, diff_inter]

Premises used: Set.diff_inter_diff, Set.diff_inter
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (M.E \ X ∩ (M.E \ Y)) + M.eRk (M.E \ X ∪ M.E \ Y) ≤ M.eRk (M.E \ X) + M.eRk (M.E \ Y)

Tactic:
apply M.eRk_submod

Premises used: Matroid.eRk_submod
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
e : α
M : Matroid α
X Y : Set α
rw :
  M.eRk (M.E \ (insert e X ∪ insert e Y)) + M.eRk (M.E \ (insert e X ∩ insert e Y)) ≤
    M.eRk (M.E \ insert e X) + M.eRk (M.E \ insert e Y)
⊢ M.eRk (M.E \ insert e (X ∪ Y)) + M.eRk (M.E \ insert e (X ∩ Y)) ≤ M.eRk (M.E \ insert e X) + M.eRk (M.E \ insert e Y)

Tactic:
rw [insert_union_distrib, insert_inter_distrib]

Premises used: Set.insert_inter_distrib, Set.insert_union_distrib
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (M.E \ (insert e X ∪ insert e Y)) + M.eRk (M.E \ (insert e X ∩ insert e Y)) ≤
    M.eRk (M.E \ insert e X) + M.eRk (M.E \ insert e Y)

Tactic:
M.eRk_compl_union_add_eRk_compl_inter_le (insert e X) (insert e Y)

Premises used: Insert.insert, Matroid.eRk_compl_union_add_eRk_compl_inter_le
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (M.E \ (insert e X ∪ insert e Y)) + M.eRk (M.E \ (insert e X ∩ insert e Y)) ≤
    M.eRk (M.E \ insert e X) + M.eRk (M.E \ insert e Y)

Tactic:
exact M.eRk_compl_union_add_eRk_compl_inter_le (insert e X) (insert e Y)

Premises used: Insert.insert, Matroid.eRk_compl_union_add_eRk_compl_inter_le
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y

Tactic:
le_add_self.trans (M.eRk_submod X Y)

Premises used: LE.le.trans, le_add_self, Matroid.eRk_submod
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
Y X : Set α
hY : M.eRk Y ≤ 0
⊢ M.eRk X + M.eRk Y ≤ M.eRk X + 0

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
Y X : Set α
hY : M.eRk Y ≤ 0
rw : M.eRk (X \ Y ∪ Y) = M.eRk X
rw₁ : M.eRk (X ∪ Y) = M.eRk X
rw₂ rw₃ : M.eRk X = M.eRk X
⊢ M.eRk (X \ Y) = M.eRk X

Tactic:
rw [← eRk_eq_eRk_union_eRk_le_zero (X \ Y) hY, diff_union_self, eRk_eq_eRk_union_eRk_le_zero _ hY]

Premises used: Set.diff_union_self, SDiff.sdiff, Matroid.eRk_eq_eRk_union_eRk_le_zero
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
nth_rw : M.eRk (X ∩ Y ∪ X \ Y) ≤ M.eRk (X ∩ Y) + M.eRk (X \ Y)
⊢ M.eRk X ≤ M.eRk (X ∩ Y) + M.eRk (X \ Y)

Tactic:
nth_rw 1 [← inter_union_diff X Y]

Premises used: Set.inter_union_diff
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (X ∩ Y ∪ X \ Y) ≤ M.eRk (X ∩ Y) + M.eRk (X \ Y)

Tactic:
apply eRk_union_le_eRk_add_eRk

Premises used: Matroid.eRk_union_le_eRk_add_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
X Y : Set α
M : Matroid α
h : Y ⊆ X
nth_rw : M.eRk (Y ∪ X \ Y) ≤ M.eRk Y + M.eRk (X \ Y)
⊢ M.eRk X ≤ M.eRk Y + M.eRk (X \ Y)

Tactic:
nth_rw 1 [← union_diff_cancel h]

Premises used: Set.union_diff_cancel
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
X Y : Set α
M : Matroid α
h : Y ⊆ X
⊢ M.eRk (Y ∪ X \ Y) ≤ M.eRk Y + M.eRk (X \ Y)

Tactic:
apply eRk_union_le_eRk_add_eRk

Premises used: Matroid.eRk_union_le_eRk_add_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
grw grw₁ : X.encard + M.eRk Y ≤ X.encard + M.eRk Y
⊢ M.eRk X + M.eRk Y ≤ X.encard + M.eRk Y

Tactic:
grw [M.eRk_le_encard]

Premises used: Matroid.eRk_le_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
grw grw₁ : M.eRk X + M.eRk Y ≤ M.eRk X + M.eRk Y
⊢ M.eRk X + M.eRk Y ≤ M.eRk X + Y.encard

Tactic:
grw [← M.eRk_le_encard]

Premises used: Matroid.eRk_le_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.eRank ≤ M.eRk ((X ∪ M.E \ X) ∩ M.E)
rw₁ : M.eRk M.E ≤ M.eRk ((X ∪ M.E \ X) ∩ M.E)
rw₂ : M.eRk M.E ≤ M.eRk ((X ∪ M.E) ∩ M.E)
rw₃ rw₄ : M.eRk M.E ≤ M.eRk M.E
⊢ M.eRank ≤ M.eRk (X ∪ M.E \ X)

Tactic:
rw [← eRk_inter_ground, eRank_def, union_diff_self,
    union_inter_cancel_right]

Premises used: Matroid.eRank_def, Matroid.eRk_inter_ground, Set.union_inter_cancel_right, Set.union_diff_self
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
obtain : ∀ (B : Set α) (hB : M.IsBase B), M.eRank ≠ ⊤ ↔ M.RankFinite
⊢ M.eRank ≠ ⊤ ↔ M.RankFinite

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

Premises used: Matroid.exists_isBase
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
rw : B.Finite ↔ M.RankFinite
⊢ M.eRank ≠ ⊤ ↔ M.RankFinite

Tactic:
rw [← hB.encard_eq_eRank, encard_ne_top_iff]

Premises used: Matroid.IsBase.encard_eq_eRank, Set.encard_ne_top_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B.Finite ↔ M.RankFinite

Tactic:
⟨fun h ↦ hB.rankFinite_of_finite h, fun h ↦ hB.finite⟩

Premises used: Matroid.IsBase.rankFinite_of_finite, Iff.intro, Matroid.IsBase.finite
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B.Finite ↔ M.RankFinite

Tactic:
exact ⟨fun h ↦ hB.rankFinite_of_finite h, fun h ↦ hB.finite⟩
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
rw : M.eRank = ⊤ ↔ ¬M.RankFinite
rw₁ : M.eRank = ⊤ ↔ ¬M.eRank ≠ ⊤
rw₂ rw₃ : M.eRank = ⊤ ↔ M.eRank = ⊤
⊢ M.eRank = ⊤ ↔ M.RankInfinite

Tactic:
rw [← not_rankFinite_iff, ← eRank_ne_top_iff, not_not]

Premises used: Classical.not_not, Matroid.not_rankFinite_iff, Matroid.eRank_ne_top_iff
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
⊢ M.eRank < ⊤ ↔ M.RankFinite

Tactic:
simp [lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
inst : M.RankInfinite
⊢ M.RankInfinite

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk X = ⊤ ↔ ¬M.IsRkFinite X
⊢ M.eRk X = ⊤ ↔ ¬M.IsRkFinite X

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

Premises used: Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
rw : I.encard = ⊤ ↔ ¬M.IsRkFinite X
rw₁ : I.Infinite ↔ ¬M.IsRkFinite X
rw₂ : I.Infinite ↔ ¬I.Finite
rw₃ rw₄ : ¬I.Finite ↔ ¬I.Finite
⊢ M.eRk X = ⊤ ↔ ¬M.IsRkFinite X

Tactic:
rw [hI.eRk_eq_encard, encard_eq_top_iff, ← hI.finite_iff_isRkFinite, Set.Infinite]

Premises used: Set.encard_eq_top_iff, Matroid.IsBasis'.finite_iff_isRkFinite, Matroid.IsBasis'.eRk_eq_encard, Set.Infinite
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X ≠ ⊤ ↔ M.IsRkFinite X

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : M.eRk X ≠ ⊤ ↔ M.IsRkFinite X
rw₁ rw₂ : M.IsRkFinite X ↔ M.IsRkFinite X
⊢ M.eRk X < ⊤ ↔ M.IsRkFinite X

Tactic:
rw [lt_top_iff_ne_top, eRk_ne_top_iff]

Premises used: Matroid.eRk_ne_top_iff, lt_top_iff_ne_top
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
h : M.IsRkFinite X
⊢ M.eRk X < ⊤

Tactic:
eRk_lt_top_iff.2 h

Premises used: Matroid.eRk_lt_top_iff, Iff.mpr
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure I
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
obtain : ∀ (J : Set α) (hJ : M.IsBasis J (I ∩ M.E)), M.IsBasis I X
⊢ M.IsBasis I X

Tactic:
obtain ⟨J, hJ⟩ := M.exists_isBasis (I ∩ M.E)

Premises used: Matroid.E, Inter.inter, Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure I
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
⊢ J ⊆ I

Tactic:
have hIJ := hJ.subset.trans inter_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure I
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
rw :
  ∀ (hXI : X ⊆ M.closure (I ∩ M.E)) (hIX : I ⊆ X) (hI : I.encard ≤ M.eRk X) (J : Set α) (hJ : M.IsBasis J (I ∩ M.E))
    (hIJ : J ⊆ I), M.IsBasis I X
⊢ M.IsBasis I X

Tactic:
rw [← closure_inter_ground] at hXI

Premises used: Matroid.closure_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure (I ∩ M.E)
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ X ⊆ M.closure J

Tactic:
replace hXI := hXI.trans <| M.closure_subset_closure_of_subset_closure hJ.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
⊢ M.IsBasis J X

Tactic:
have hJX := hJ.indep.isBasis_of_subset_of_subset_closure (hIJ.trans hIX) hXI
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
⊢ I.encard ≤ J.encard

Tactic:
rw [← hJX.encard_eq_eRk] at hI

Premises used: Matroid.IsBasis.encard_eq_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
hI₁ : I.encard ≤ J.encard
⊢ M.IsBasis J (I ∩ M.E)

Tactic:
rw [← hJX.encard_eq_eRk] at hI

Premises used: Matroid.IsBasis.encard_eq_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
hI₁ : I.encard ≤ J.encard
hJ₁ : M.IsBasis J (I ∩ M.E)
⊢ J ⊆ I

Tactic:
rw [← hJX.encard_eq_eRk] at hI

Premises used: Matroid.IsBasis.encard_eq_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
hI₁ : I.encard ≤ J.encard
hJ₁ : M.IsBasis J (I ∩ M.E)
hIJ₁ : J ⊆ I
⊢ X ⊆ M.closure J

Tactic:
rw [← hJX.encard_eq_eRk] at hI

Premises used: Matroid.IsBasis.encard_eq_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
hI₁ : I.encard ≤ J.encard
hJ₁ : M.IsBasis J (I ∩ M.E)
hIJ₁ : J ⊆ I
hXI₁ : X ⊆ M.closure J
⊢ M.IsBasis J X

Tactic:
rw [← hJX.encard_eq_eRk] at hI

Premises used: Matroid.IsBasis.encard_eq_eRk
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
J : Set α
hI : I.encard ≤ J.encard
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
rwa rwa₁ rwa₂ rwa₃ : M.IsBasis J X
⊢ M.IsBasis I X

Tactic:
rwa [← Finite.eq_of_subset_of_encard_le (hX.finite_of_isBasis hJX) hIJ hI]

Premises used: Matroid.IsRkFinite.finite_of_isBasis, Set.Finite.eq_of_subset_of_encard_le
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hr : M.eRk Y ≤ M.eRk X
obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.closure X = M.closure Y
⊢ M.closure X = M.closure Y

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

Premises used: Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hr : M.eRk Y ≤ M.eRk X
I : Set α
hI : M.IsBasis' I X
obtain : ∀ (J : Set α) (hJ : M.IsBasis' J Y) (hIJ : I ⊆ J), M.closure X = M.closure Y
⊢ M.closure X = M.closure Y

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis'_of_subset (hI.subset.trans hXY)

Premises used: HasSubset.Subset.trans, Matroid.IsBasis'.indep, Matroid.Indep.subset_isBasis'_of_subset, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hr : M.eRk Y ≤ M.eRk X
I : Set α
hI : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
rw :
  ∀ (hI : M.IsBasis' I X) (J : Set α) (hr : J.encard ≤ I.encard) (hJ : M.IsBasis' J Y) (hIJ : I ⊆ J),
    M.closure X = M.closure Y
⊢ M.closure X = M.closure Y

Tactic:
rw [hI.eRk_eq_encard, hJ.eRk_eq_encard] at hr

Premises used: Matroid.IsBasis'.eRk_eq_encard
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
rw : M.closure (X ∩ M.E) = M.closure Y
rw₁ : M.closure (X ∩ M.E) = M.closure (Y ∩ M.E)
rw₂ : M.closure I = M.closure (Y ∩ M.E)
rw₃ : M.closure I = M.closure J
rw₄ rw₅ : M.closure J = M.closure J
⊢ M.closure X = M.closure Y

Tactic:
rw [← closure_inter_ground, ← M.closure_inter_ground Y,
    ← hI.isBasis_inter_ground.closure_eq_closure,
    ← hJ.isBasis_inter_ground.closure_eq_closure, Finite.eq_of_subset_of_encard_le
      (hI.indep.finite_of_subset_isRkFinite hI.subset hX) hIJ hr]

Premises used: Matroid.IsBasis'.isBasis_inter_ground, Matroid.IsBasis'.indep, Matroid.closure_inter_ground, Matroid.Indep.finite_of_subset_isRkFinite, Matroid.IsBasis'.subset, Set.Finite.eq_of_subset_of_encard_le, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
bc : M.eRk {e} ≤ 1
⊢ M.eRk X + M.eRk {e} ≤ M.eRk X + 1

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
⊢ M.eRk {e} ≤ 1

Tactic:
simpa using M.eRk_le_encard {e}

Premises used: Matroid.eRk_le_encard, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
he : e ∈ M.E \ M.closure X
obtain : ∀ (I : Set α) (hI : M.IsBasis' I X), M.eRk (insert e X) = M.eRk X + 1
⊢ M.eRk (insert e X) = M.eRk X + 1

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

Premises used: Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
he : e ∈ M.E \ M.closure X
I : Set α
hI : M.IsBasis' I X
⊢ e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))

Tactic:
rw [← hI.closure_eq_closure, mem_diff, hI.indep.mem_closure_iff', not_and] at he

Premises used: Matroid.IsBasis'.closure_eq_closure, Matroid.Indep.mem_closure_iff', Matroid.IsBasis'.indep, Set.mem_diff, not_and
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
he : e ∈ M.E \ M.closure X
I : Set α
hI : M.IsBasis' I X
he₁ : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
⊢ M.IsBasis' I X

Tactic:
rw [← hI.closure_eq_closure, mem_diff, hI.indep.mem_closure_iff', not_and] at he

Premises used: Matroid.IsBasis'.closure_eq_closure, Matroid.Indep.mem_closure_iff', Matroid.IsBasis'.indep, Set.mem_diff, not_and
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
tauto tauto₁ tauto₂ : e ∈ M.E → (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I)) → M.Indep (insert e I)
inl : e ∈ M.E → e ∉ M.E → M.Indep (insert e I)
inr inr₁ inr₂ : e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I) → M.Indep (insert e I)
inr₃ inr₄ inr₅ : e ∈ M.E → M.Indep (insert e I) → e ∉ I → M.Indep (insert e I)
⊢ M.Indep (insert e I)

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
tauto tauto₁ tauto₂ : e ∈ I → e ∈ M.E → (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I)) → False
inl : e ∈ I → e ∈ M.E → e ∉ M.E → False
inr inr₁ inr₂ : e ∈ I → e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I) → False
inr₃ : e ∈ I → e ∈ M.E → M.Indep (insert e I) → e ∉ I → False
⊢ e ∉ I

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
rw : M.eRk (M.closure (insert e X)) = M.eRk X + 1
rw₁ : M.eRk (M.closure (insert e I)) = M.eRk X + 1
rw₂ : M.eRk (M.closure (insert e I)) = I.encard + 1
rw₃ : M.eRk (insert e I) = I.encard + 1
rw₄ : (insert e I).encard = I.encard + 1
rw₅ rw₆ : I.encard + 1 = I.encard + 1
⊢ M.eRk (insert e X) = M.eRk X + 1

Tactic:
rw [← eRk_closure_eq, ← closure_insert_congr_right hI.closure_eq_closure, hI.eRk_eq_encard,
    eRk_closure_eq, Indep.eRk_eq_encard (by tauto), encard_insert_of_notMem (by tauto)]

Premises used: Matroid.IsBasis'.closure_eq_closure, Matroid.Indep.eRk_eq_encard, Matroid.IsBasis'.eRk_eq_encard, Matroid.closure_insert_congr_right, Set.encard_insert_of_notMem, Matroid.eRk_closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.eRk X < M.eRk Y
contrapose! : ∀ (h : Y ∩ M.E ⊆ M.closure X), M.eRk Y ≤ M.eRk X
⊢ ¬Y ∩ M.E ⊆ M.closure X

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : Y ∩ M.E ⊆ M.closure X
⊢ M.eRk Y ≤ M.eRk X

Tactic:
simpa using M.eRk_mono h

Premises used: Matroid.eRk_mono
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.eRk X < M.eRk Y
⊢ ¬Y ∩ M.E ⊆ M.closure X

Tactic:
have hz : ¬ Y ∩ M.E ⊆ M.closure X := by
    contrapose! h
    simpa using M.eRk_mono h
-- Module: Mathlib.Combinatorics.Matroid.Rank.ENat
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.eRk X < M.eRk Y
hz : ¬Y ∩ M.E ⊆ M.closure X
obtain : ∀ (e : α) (heX : e ∉ M.closure X) (heZ : e ∈ Y) (heE : e ∈ M.E), ∃ y ∈ Y \ X, M.eRk (insert y X) = M.eRk X + 1
⊢ ∃ y ∈ Y \ X, M.eRk (insert y X) = M.eRk X + 1

Tactic:
obtain ⟨e, ⟨heZ, heE⟩, heX⟩ := not_subset.1 hz

Premises used: Set.not_subset, Iff.mp