awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D : Set α
inst : M.RankPos
hD : M.Coindep D
⊢ (M ＼ D).RankPos
have rw : ¬(M.IsBase ∅ ∧ Disjoint ∅ D)
Tactic: rw [rankPos_iff, hD.delete_isBase_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D S : Set α
hD : M.Coindep D
⊢ (M ＼ D).Spanning S ↔ M.Spanning S ∧ Disjoint S D
have simp : S ⊆ M.E → Disjoint S D → ((∃ (B : Set α), M.IsBase B ∧ Disjoint B D ∧ B ⊆ S) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S)
Tactic: simp only [spanning_iff_exists_isBase_subset', hD.delete_isBase_iff, and_assoc, delete_ground,
    subset_diff, and_congr_left_iff, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D S : Set α
hD : M.Coindep D
⊢ S ⊆ M.E → Disjoint S D → ((∃ (B : Set α), M.IsBase B ∧ Disjoint B D ∧ B ⊆ S) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S)
have refine : ∀ (hSE : S ⊆ M.E) (hSD : Disjoint S D),
  (∃ (B : Set α), M.IsBase B ∧ B ⊆ S) → ∀ (B : Set α) (hB : M.IsBase B) (hBS : B ⊆ S), Disjoint B D
Tactic: refine fun hSE hSD ↦ ⟨fun ⟨B, hB, hBD, hBS⟩ ↦ ⟨B, hB, hBS⟩, fun ⟨B, hB, hBS⟩ ↦ ⟨B, hB, ?_, hBS⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ (M ＼ D).IsLoop e ↔ M.IsLoop e ∧ e ∉ D
have rw : (M ＼ D).Dep {e} ↔ M.IsLoop e ∧ e ∉ D
Tactic: rw [← singleton_dep, delete_dep_iff, disjoint_singleton_left, singleton_dep]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
D : Set α
rw : (M ＼ D).Dep {e} ↔ M.IsLoop e ∧ e ∉ D
⊢ (M ＼ D).IsLoop e ↔ M.IsLoop e ∧ e ∉ D
have rw₁ : M.Dep {e} ∧ Disjoint {e} D ↔ M.IsLoop e ∧ e ∉ D
Tactic: rw [← singleton_dep, delete_dep_iff, disjoint_singleton_left, singleton_dep]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
D : Set α
rw : (M ＼ D).Dep {e} ↔ M.IsLoop e ∧ e ∉ D
rw₁ : M.Dep {e} ∧ Disjoint {e} D ↔ M.IsLoop e ∧ e ∉ D
⊢ (M ＼ D).IsLoop e ↔ M.IsLoop e ∧ e ∉ D
have rw₂ : M.Dep {e} ∧ e ∉ D ↔ M.IsLoop e ∧ e ∉ D
Tactic: rw [← singleton_dep, delete_dep_iff, disjoint_singleton_left, singleton_dep]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
D : Set α
rw : (M ＼ D).Dep {e} ↔ M.IsLoop e ∧ e ∉ D
rw₁ : M.Dep {e} ∧ Disjoint {e} D ↔ M.IsLoop e ∧ e ∉ D
rw₂ : M.Dep {e} ∧ e ∉ D ↔ M.IsLoop e ∧ e ∉ D
⊢ (M ＼ D).IsLoop e ↔ M.IsLoop e ∧ e ∉ D
have rw₃ : M.IsLoop e ∧ e ∉ D ↔ M.IsLoop e ∧ e ∉ D
Tactic: rw [← singleton_dep, delete_dep_iff, disjoint_singleton_left, singleton_dep]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ (M ＼ D).IsNonloop e ↔ M.IsNonloop e ∧ e ∉ D
have rw : (M ＼ D).Indep {e} ↔ M.IsNonloop e ∧ e ∉ D
Tactic: rw [← indep_singleton, delete_indep_iff, disjoint_singleton_left, indep_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
D : Set α
rw : (M ＼ D).Indep {e} ↔ M.IsNonloop e ∧ e ∉ D
⊢ (M ＼ D).IsNonloop e ↔ M.IsNonloop e ∧ e ∉ D
have rw₁ : M.Indep {e} ∧ Disjoint {e} D ↔ M.IsNonloop e ∧ e ∉ D
Tactic: rw [← indep_singleton, delete_indep_iff, disjoint_singleton_left, indep_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
D : Set α
rw : (M ＼ D).Indep {e} ↔ M.IsNonloop e ∧ e ∉ D
rw₁ : M.Indep {e} ∧ Disjoint {e} D ↔ M.IsNonloop e ∧ e ∉ D
⊢ (M ＼ D).IsNonloop e ↔ M.IsNonloop e ∧ e ∉ D
have rw₂ : M.Indep {e} ∧ e ∉ D ↔ M.IsNonloop e ∧ e ∉ D
Tactic: rw [← indep_singleton, delete_indep_iff, disjoint_singleton_left, indep_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
D : Set α
rw : (M ＼ D).Indep {e} ↔ M.IsNonloop e ∧ e ∉ D
rw₁ : M.Indep {e} ∧ Disjoint {e} D ↔ M.IsNonloop e ∧ e ∉ D
rw₂ : M.Indep {e} ∧ e ∉ D ↔ M.IsNonloop e ∧ e ∉ D
⊢ (M ＼ D).IsNonloop e ↔ M.IsNonloop e ∧ e ∉ D
have rw₃ : M.IsNonloop e ∧ e ∉ D ↔ M.IsNonloop e ∧ e ∉ D
Tactic: rw [← indep_singleton, delete_indep_iff, disjoint_singleton_left, indep_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M ＼ M.loops = M.removeLoops
have rw : M ＼ M.loops = M ↾ {e : α | M.IsNonloop e}
Tactic: rw [removeLoops, delete_eq_restrict, compl_loops_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
rw : M ＼ M.loops = M ↾ {e : α | M.IsNonloop e}
⊢ M ＼ M.loops = M.removeLoops
have rw₁ : M ↾ M.E \ M.loops = M ↾ {e : α | M.IsNonloop e}
Tactic: rw [removeLoops, delete_eq_restrict, compl_loops_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
rw : M ＼ M.loops = M ↾ {e : α | M.IsNonloop e}
rw₁ : M ↾ M.E \ M.loops = M ↾ {e : α | M.IsNonloop e}
⊢ M ＼ M.loops = M.removeLoops
have rw₂ : M ↾ {e : α | M.IsNonloop e} = M ↾ {e : α | M.IsNonloop e}
Tactic: rw [removeLoops, delete_eq_restrict, compl_loops_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D C : Set α
⊢ (M ＼ D).IsCircuit C ↔ M.IsCircuit C ∧ Disjoint C D
have rw : M.IsCircuit C → Disjoint C D → C ⊆ M.E
Tactic: rw [delete_eq_restrict, restrict_isCircuit_iff, and_congr_right_iff, subset_diff,
    and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
⊢ (M ＼ D).closure X = M.closure (X \ D) \ D
have rw : M.closure (X \ D) \ D ⊆ M.E
Tactic: rw [← restrict_compl, restrict_closure_eq', sdiff_sdiff_self, bot_eq_empty, union_empty,
    diff_eq, inter_comm M.E, ← inter_assoc X, ← diff_eq, closure_inter_ground,
    ← inter_assoc, ← diff_eq, inter_eq_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
hXD : Disjoint X D
⊢ (M ＼ D).closure X = M.closure X \ D
have rw : M.closure (X \ D) \ D = M.closure X \ D
Tactic: rw [delete_closure_eq, hXD.sdiff_eq_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
hXD : Disjoint X D
rw : M.closure (X \ D) \ D = M.closure X \ D
⊢ (M ＼ D).closure X = M.closure X \ D
have rw₁ : M.closure X \ D = M.closure X \ D
Tactic: rw [delete_closure_eq, hXD.sdiff_eq_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
e : α
M : Matroid α
D : Set α
⊢ (M ＼ D).IsColoop e ↔ e ∉ M.closure ((M.E \ D) \ {e}) ∧ e ∈ M.E ∧ e ∉ D
have rw : e ∈ M.E → e ∉ D → (e ∉ M.closure ((M.E \ D) \ {e}) ↔ e ∉ M.closure ((M.E \ D) \ {e}))
Tactic: rw [delete_eq_restrict, restrict_isColoop_iff diff_subset, mem_diff, and_congr_left_iff, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M N : Matroid α
h : N ≤m M
⊢ ∃ (C : Set α) (D : Set α), C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D
have obtain : ∀ (C D : Set α), ∃ (C_1 : Set α) (D_1 : Set α), C_1 ⊆ M.E ∧ D_1 ⊆ M.E ∧ Disjoint C_1 D_1 ∧ M ／ C ＼ D = M ／ C_1 ＼ D_1
Tactic: obtain ⟨C, D, rfl⟩ := h
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M N : Matroid α
h : N ≤m M
⊢ N.E ⊆ M.E
have obtain : ∀ (C D : Set α), (M ／ C ＼ D).E ⊆ M.E
Tactic: obtain ⟨C, D, rfl⟩ := h
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M₁ M₂ M₃ : Matroid α
h : M₁ ≤m M₂
h' : M₂ ≤m M₃
⊢ M₁ ≤m M₃
have obtain : ∀ (C₁ D₁ : Set α), M₂ ／ C₁ ＼ D₁ ≤m M₃
Tactic: obtain ⟨C₁, D₁, rfl⟩ := h
Cleared hypotheses: M₁, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M₂ M₃ : Matroid α
h' : M₂ ≤m M₃
C₁ D₁ : Set α
⊢ M₂ ／ C₁ ＼ D₁ ≤m M₃
have obtain : ∀ (C₂ D₂ : Set α), M₃ ／ C₂ ＼ D₂ ／ C₁ ＼ D₁ ≤m M₃
Tactic: obtain ⟨C₂, D₂, rfl⟩ := h'
Cleared hypotheses: M₂, h'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M₃ : Matroid α
C₁ D₁ C₂ D₂ : Set α
⊢ M₃ ／ C₂ ＼ D₂ ／ C₁ ＼ D₁ = M₃ ／ (C₂ ∪ C₁ \ D₂) ＼ (D₂ ∪ D₁)
have rw : M₃ ／ (C₂ ∪ C₁ \ D₂) ＼ (D₂ ∪ D₁) = M₃ ／ (C₂ ∪ C₁ \ D₂) ＼ (D₂ ∪ D₁)
Tactic: rw [contract_delete_contract_delete']
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M N : Matroid α
h : N ≤m M
hE : M.E ⊆ N.E
⊢ M = N
have obtain : ∀ (C D : Set α) (hE : M.E ⊆ (M ／ C ＼ D).E), M = M ／ C ＼ D
Tactic: obtain ⟨C, D, rfl⟩ := h
Cleared hypotheses: N, h, hE
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (hypothesis)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
hE : M.E ⊆ (M ／ C ＼ D).E
⊢ M = M ／ C ＼ D
have hE₁ : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
Tactic: rw [delete_ground, contract_ground, subset_diff, subset_diff] at hE
Cleared hypotheses: hE
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
⊢ M = M ／ C ＼ D
have rw : M = M ／ (C ∩ M.E) ＼ D
Tactic: rw [← contract_inter_ground_eq, hE.1.2.symm.inter_eq, contract_empty, ← delete_inter_ground_eq,
    hE.2.symm.inter_eq, delete_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
rw : M = M ／ (C ∩ M.E) ＼ D
⊢ M = M ／ C ＼ D
have rw₁ : M = M ／ ∅ ＼ D
Tactic: rw [← contract_inter_ground_eq, hE.1.2.symm.inter_eq, contract_empty, ← delete_inter_ground_eq,
    hE.2.symm.inter_eq, delete_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
rw : M = M ／ (C ∩ M.E) ＼ D
rw₁ : M = M ／ ∅ ＼ D
⊢ M = M ／ C ＼ D
have rw₂ : M = M ＼ D
Tactic: rw [← contract_inter_ground_eq, hE.1.2.symm.inter_eq, contract_empty, ← delete_inter_ground_eq,
    hE.2.symm.inter_eq, delete_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
rw : M = M ／ (C ∩ M.E) ＼ D
rw₁ : M = M ／ ∅ ＼ D
rw₂ : M = M ＼ D
⊢ M = M ／ C ＼ D
have rw₃ : M = M ＼ (D ∩ M.E)
Tactic: rw [← contract_inter_ground_eq, hE.1.2.symm.inter_eq, contract_empty, ← delete_inter_ground_eq,
    hE.2.symm.inter_eq, delete_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
rw : M = M ／ (C ∩ M.E) ＼ D
rw₁ : M = M ／ ∅ ＼ D
rw₂ : M = M ＼ D
rw₃ : M = M ＼ (D ∩ M.E)
⊢ M = M ／ C ＼ D
have rw₄ : M = M ＼ ∅
Tactic: rw [← contract_inter_ground_eq, hE.1.2.symm.inter_eq, contract_empty, ← delete_inter_ground_eq,
    hE.2.symm.inter_eq, delete_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
rw : M = M ／ (C ∩ M.E) ＼ D
rw₁ : M = M ／ ∅ ＼ D
rw₂ : M = M ＼ D
rw₃ : M = M ＼ (D ∩ M.E)
rw₄ : M = M ＼ ∅
⊢ M = M ／ C ＼ D
have rw₅ : M = M
Tactic: rw [← contract_inter_ground_eq, hE.1.2.symm.inter_eq, contract_empty, ← delete_inter_ground_eq,
    hE.2.symm.inter_eq, delete_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M N : Matroid α
h_1 : N ≤m M ∧ N.E ⊂ M.E
h : N ≤m M
hss : N.E ⊂ M.E
h' : M ≤m N
⊢ N.E = M.E
have rw : N.E = N.E
Tactic: rw [h'.antisymm h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M N : Matroid α
I : Set α
hI : N.Indep I
hNM : N ≤m M
⊢ M.Indep I
have obtain : ∀ (C D : Set α) (hI : (M ／ C ＼ D).Indep I), M.Indep I
Tactic: obtain ⟨C, D, rfl⟩ := hNM
Cleared hypotheses: N, hI, hNM
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M N : Matroid α
e : α
h : N.IsNonloop e
hNM : N ≤m M
⊢ M.IsNonloop e
have obtain : ∀ (C D : Set α) (h : (M ／ C ＼ D).IsNonloop e), M.IsNonloop e
Tactic: obtain ⟨C, D, rfl⟩ := hNM
Cleared hypotheses: N, h, hNM
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Order (goal)
Goal:
α : Type u_1
M N : Matroid α
e : α
he : M.IsLoop e
heN : e ∈ N.E
hNM : N ≤m M
⊢ N.IsLoop e
have rw : ∀ (he : M.Dep {e}) (heN : e ∈ N.E) (hNM : N ≤m M), N.Dep {e}
Tactic: rw [← singleton_dep] at he ⊢
Cleared hypotheses: he, heN, hNM
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I I' : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis' I R
hI' : M.IsBasis' I' R
⊢ ∃ x ∈ I' \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have hIn₁ : ¬M.IsBasis I (R ∩ M.E)
Tactic: rw [isBasis'_iff_isBasis_inter_ground] at hIn hI'
Cleared hypotheses: hIn, hI'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I I' : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis' I R
hI' : M.IsBasis' I' R
hIn₁ : ¬M.IsBasis I (R ∩ M.E)
⊢ ∃ x ∈ I' \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have hI'₁ : M.IsBasis I' (R ∩ M.E)
Tactic: rw [isBasis'_iff_isBasis_inter_ground] at hIn hI'
Cleared hypotheses: hIn, hI'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I I' : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
hI' : M.IsBasis I' (R ∩ M.E)
⊢ ∃ x ∈ I' \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have obtain : ∀ (B' : Set α) (hB' : M.IsBase B') (hI' : M.IsBasis (B' ∩ (R ∩ M.E)) (R ∩ M.E)),
  ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
Tactic: obtain ⟨B', hB', rfl⟩ := hI'.exists_isBase
Cleared hypotheses: I', hI'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M.IsBasis (B' ∩ (R ∩ M.E)) (R ∩ M.E)
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have obtain : ∀ (B : Set α) (hB : M.IsBase B) (hIB : I ⊆ B) (hBIB' : B ⊆ I ∪ B'),
  ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
Tactic: obtain ⟨B, hB, hIB, hBIB'⟩ := hI.exists_isBase_subset_union_isBase hB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M.IsBasis (B' ∩ (R ∩ M.E)) (R ∩ M.E)
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have rw : ∀ (hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))) (B : Set α) (hB : M.IsBase B) (hIB : I ⊆ B)
  (hBIB' : B ⊆ I ∪ B'), ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
Tactic: rw [hB'.inter_isBasis_iff_compl_inter_isBasis_dual, diff_inter_diff] at hI'
Cleared hypotheses: hI', B, hB, hIB, hBIB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
have h : B ∪ R ∩ M.E ⊆ B' ∪ R ∩ M.E
Tactic: apply diff_subset_diff_right
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ B ∪ R ∩ M.E ⊆ B' ∪ R ∩ M.E
have h : B ⊆ R ∩ M.E ∪ B'
Tactic: rw [union_subset_iff, and_iff_left subset_union_right, union_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
Tactic: have hss : M.E \ (B' ∪ (R ∩ M.E)) ⊆ M.E \ (B ∪ (R ∩ M.E)) := by
      apply diff_subset_diff_right
      rw [union_subset_iff, and_iff_left subset_union_right, union_comm]
      exact hBIB'.trans (union_subset_union_left _ (subset_inter hIY hI.subset_ground))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
⊢ M✶.Indep (M.E \ (B ∪ R ∩ M.E))
have rw : ∃ (B_1 : Set α), M.IsBase B_1 ∧ Disjoint (M.E \ (B ∪ R ∩ M.E)) B_1
Tactic: rw [dual_indep_iff_exists]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
Tactic: have hi : M✶.Indep (M.E \ (B ∪ (R ∩ M.E))) := by
      rw [dual_indep_iff_exists]
      exact ⟨B, hB, disjoint_of_subset_right subset_union_left disjoint_sdiff_left⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
Tactic: have h_eq := hI'.eq_of_subset_indep hi hss
      (diff_subset_diff_right subset_union_right)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have hI'₁ : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
Tactic: rw [h_eq, ← diff_inter_diff, ← hB.inter_isBasis_iff_compl_inter_isBasis_dual] at hI'
Cleared hypotheses: hI', hB, hIB, hBIB', hss, hi, h_eq
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have obtain : ∀ (J : Set α) (hJ : M.IsBasis J (B ∩ (R ∩ M.E))) (hIJ : I ⊆ J),
  ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
Tactic: obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis_of_subset
      (subset_inter hIB (subset_inter hIY hI.subset_ground))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
J : Set α
hJ : M.IsBasis J (B ∩ (R ∩ M.E))
hIJ : I ⊆ J
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have hJ₁ : M.IsBasis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))
Tactic: obtain rfl := hI'.indep.eq_of_isBasis hJ
Cleared hypotheses: J, hJ, hIJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
J : Set α
hJ : M.IsBasis J (B ∩ (R ∩ M.E))
hIJ : I ⊆ J
hJ₁ : M.IsBasis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have hIJ₁ : I ⊆ B ∩ (R ∩ M.E)
Tactic: obtain rfl := hI'.indep.eq_of_isBasis hJ
Cleared hypotheses: J, hJ, hIJ
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hJ : M.IsBasis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))
hIJ : I ⊆ B ∩ (R ∩ M.E)
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have hIJ' : I ⊂ B ∩ (R ∩ M.E)
Tactic: have hIJ' : I ⊂ B ∩ (R ∩ M.E) := hIJ.ssubset_of_ne (fun he ↦ hIn (by rwa [he]))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hJ : M.IsBasis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))
hIJ : I ⊆ B ∩ (R ∩ M.E)
hIJ' : I ⊂ B ∩ (R ∩ M.E)
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
have obtain : ∀ (e : α) (he : e ∈ B ∩ (R ∩ M.E) ∧ e ∉ I), ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
Tactic: obtain ⟨e, he⟩ := exists_of_ssubset hIJ'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M_1 : Matroid α
R_1 I_1 X Y : Set α
M : Matroid α
R A : Set α
hAR : A ⊆ R
I : Set α
hI : M.Indep I
right : I ⊆ R
hIA : I ⊆ A
⊢ ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ R) K ∧ K ⊆ A) J
have obtain : ∀ (J : Set α) (hJ : M.IsBasis' J A) (hIJ : I ⊆ J),
  ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ R) K ∧ K ⊆ A) J
Tactic: obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis'_of_subset hIA