awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
⊢ M ／ (C ∩ M.E) = M ／ C
have rw : (M✶ ＼ (C ∩ M.E))✶ = M ／ C
Tactic: rw [← dual_delete_dual, ← dual_ground, delete_inter_ground_eq, dual_delete_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : (M✶ ＼ (C ∩ M.E))✶ = M ／ C
⊢ M ／ (C ∩ M.E) = M ／ C
have rw₁ : (M✶ ＼ (C ∩ M✶.E))✶ = M ／ C
Tactic: rw [← dual_delete_dual, ← dual_ground, delete_inter_ground_eq, dual_delete_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : (M✶ ＼ (C ∩ M.E))✶ = M ／ C
rw₁ : (M✶ ＼ (C ∩ M✶.E))✶ = M ／ C
⊢ M ／ (C ∩ M.E) = M ／ C
have rw₂ : (M✶ ＼ C)✶ = M ／ C
Tactic: rw [← dual_delete_dual, ← dual_ground, delete_inter_ground_eq, dual_delete_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : (M✶ ＼ (C ∩ M.E))✶ = M ／ C
rw₁ : (M✶ ＼ (C ∩ M✶.E))✶ = M ／ C
rw₂ : (M✶ ＼ C)✶ = M ／ C
⊢ M ／ (C ∩ M.E) = M ／ C
have rw₃ : M ／ C = M ／ C
Tactic: rw [← dual_delete_dual, ← dual_ground, delete_inter_ground_eq, dual_delete_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
⊢ (M ／ C).Coindep X ↔ M.Coindep X ∧ Disjoint X C
have rw : (M ／ C)✶.Indep X ↔ M.Coindep X ∧ Disjoint X C
Tactic: rw [coindep_def, dual_contract, delete_indep_iff, ← coindep_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
rw : (M ／ C)✶.Indep X ↔ M.Coindep X ∧ Disjoint X C
⊢ (M ／ C).Coindep X ↔ M.Coindep X ∧ Disjoint X C
have rw₁ : (M✶ ＼ C).Indep X ↔ M.Coindep X ∧ Disjoint X C
Tactic: rw [coindep_def, dual_contract, delete_indep_iff, ← coindep_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
rw : (M ／ C)✶.Indep X ↔ M.Coindep X ∧ Disjoint X C
rw₁ : (M✶ ＼ C).Indep X ↔ M.Coindep X ∧ Disjoint X C
⊢ (M ／ C).Coindep X ↔ M.Coindep X ∧ Disjoint X C
have rw₂ : M✶.Indep X ∧ Disjoint X C ↔ M.Coindep X ∧ Disjoint X C
Tactic: rw [coindep_def, dual_contract, delete_indep_iff, ← coindep_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
rw : (M ／ C)✶.Indep X ↔ M.Coindep X ∧ Disjoint X C
rw₁ : (M✶ ＼ C).Indep X ↔ M.Coindep X ∧ Disjoint X C
rw₂ : M✶.Indep X ∧ Disjoint X C ↔ M.Coindep X ∧ Disjoint X C
⊢ (M ／ C).Coindep X ↔ M.Coindep X ∧ Disjoint X C
have rw₃ : M.Coindep X ∧ Disjoint X C ↔ M.Coindep X ∧ Disjoint X C
Tactic: rw [coindep_def, dual_contract, delete_indep_iff, ← coindep_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K C : Set α
⊢ (M ／ C).IsCocircuit K ↔ M.IsCocircuit K ∧ Disjoint K C
have rw : (M ／ C)✶.IsCircuit K ↔ M.IsCocircuit K ∧ Disjoint K C
Tactic: rw [isCocircuit_def, dual_contract, delete_isCircuit_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K C : Set α
rw : (M ／ C)✶.IsCircuit K ↔ M.IsCocircuit K ∧ Disjoint K C
⊢ (M ／ C).IsCocircuit K ↔ M.IsCocircuit K ∧ Disjoint K C
have rw₁ : (M✶ ＼ C).IsCircuit K ↔ M.IsCocircuit K ∧ Disjoint K C
Tactic: rw [isCocircuit_def, dual_contract, delete_isCircuit_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K C : Set α
rw : (M ／ C)✶.IsCircuit K ↔ M.IsCocircuit K ∧ Disjoint K C
rw₁ : (M✶ ＼ C).IsCircuit K ↔ M.IsCocircuit K ∧ Disjoint K C
⊢ (M ／ C).IsCocircuit K ↔ M.IsCocircuit K ∧ Disjoint K C
have rw₂ : M✶.IsCircuit K ∧ Disjoint K C ↔ M.IsCocircuit K ∧ Disjoint K C
Tactic: rw [isCocircuit_def, dual_contract, delete_isCircuit_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ (M ／ I).IsBase B ↔ M.IsBase (B ∪ I) ∧ Disjoint B I
have rw : Disjoint B I → B ⊆ M.E → (M✶.IsBase (M.E \ (I ∪ B)) ↔ M✶.IsBase (M.E \ (I ∪ B)))
Tactic: rw [← dual_delete_dual, dual_isBase_iff', delete_ground, dual_ground, delete_isBase_iff,
    subset_diff, ← and_assoc, and_congr_left_iff, ← dual_dual M, dual_isBase_iff', dual_dual,
    dual_dual, union_comm, dual_ground, union_subset_iff, and_iff_right hI.subset_ground,
    and_congr_left_iff, ← isBase_restrict_iff, diff_diff, Spanning.isBase_restrict_iff,
    and_iff_left (diff_subset_diff_right subset_union_left)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
rw : Disjoint B I → B ⊆ M.E → (M✶.IsBase (M.E \ (I ∪ B)) ↔ M✶.IsBase (M.E \ (I ∪ B)))
⊢ (M ／ I).IsBase B ↔ M.IsBase (B ∪ I) ∧ Disjoint B I
have rw₁ : M✶.Spanning (M.E \ I)
Tactic: rw [← dual_delete_dual, dual_isBase_iff', delete_ground, dual_ground, delete_isBase_iff,
    subset_diff, ← and_assoc, and_congr_left_iff, ← dual_dual M, dual_isBase_iff', dual_dual,
    dual_dual, union_comm, dual_ground, union_subset_iff, and_iff_right hI.subset_ground,
    and_congr_left_iff, ← isBase_restrict_iff, diff_diff, Spanning.isBase_restrict_iff,
    and_iff_left (diff_subset_diff_right subset_union_left)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ M✶.Spanning (M.E \ I)
have rwa : M✶.Spanning (M✶.E \ I)
Tactic: rwa [← dual_ground, ← coindep_iff_compl_spanning, dual_coindep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
rwa : M✶.Spanning (M✶.E \ I)
⊢ M✶.Spanning (M.E \ I)
have rwa₁ : M✶.Coindep I
Tactic: rwa [← dual_ground, ← coindep_iff_compl_spanning, dual_coindep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ (M ／ I).Indep J ↔ Disjoint J I ∧ M.Indep (J ∪ I)
have simp_rw : (∃ (B : Set α), (M.IsBase (B ∪ I) ∧ Disjoint B I) ∧ J ⊆ B) ↔ Disjoint J I ∧ ∃ (B : Set α), M.IsBase B ∧ J ⊆ B ∧ I ⊆ B
Tactic: simp_rw [indep_iff, hI.contract_isBase_iff, union_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ M.Indep (I ∪ J) ↔ (M ／ I).Indep (J \ I)
have rw : M.Indep (I ∪ J) ↔ Disjoint (J \ I) I ∧ M.Indep (J \ I ∪ I)
Tactic: rw [hI.contract_indep_iff, and_iff_right disjoint_sdiff_left, diff_union_self, union_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
rw : M.Indep (I ∪ J) ↔ Disjoint (J \ I) I ∧ M.Indep (J \ I ∪ I)
⊢ M.Indep (I ∪ J) ↔ (M ／ I).Indep (J \ I)
have rw₁ : M.Indep (I ∪ J) ↔ M.Indep (J \ I ∪ I)
Tactic: rw [hI.contract_indep_iff, and_iff_right disjoint_sdiff_left, diff_union_self, union_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
rw : M.Indep (I ∪ J) ↔ Disjoint (J \ I) I ∧ M.Indep (J \ I ∪ I)
rw₁ : M.Indep (I ∪ J) ↔ M.Indep (J \ I ∪ I)
⊢ M.Indep (I ∪ J) ↔ (M ／ I).Indep (J \ I)
have rw₂ : M.Indep (I ∪ J) ↔ M.Indep (J ∪ I)
Tactic: rw [hI.contract_indep_iff, and_iff_right disjoint_sdiff_left, diff_union_self, union_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
rw : M.Indep (I ∪ J) ↔ Disjoint (J \ I) I ∧ M.Indep (J \ I ∪ I)
rw₁ : M.Indep (I ∪ J) ↔ M.Indep (J \ I ∪ I)
rw₂ : M.Indep (I ∪ J) ↔ M.Indep (J ∪ I)
⊢ M.Indep (I ∪ J) ↔ (M ／ I).Indep (J \ I)
have rw₃ : M.Indep (J ∪ I) ↔ M.Indep (J ∪ I)
Tactic: rw [hI.contract_indep_iff, and_iff_right disjoint_sdiff_left, diff_union_self, union_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
⊢ (M ／ I).Indep (J \ I)
have rwa : M.Indep (I ∪ J)
Tactic: rwa [← (hJ.subset hIJ).union_indep_iff_contract_indep, union_eq_self_of_subset_left hIJ]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ (M ／ I).Dep J ↔ Disjoint J I ∧ M.Dep (J ∪ I)
have rw : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
Tactic: rw [dep_iff, hI.contract_indep_iff, dep_iff, contract_ground, subset_diff, disjoint_comm,
    union_subset_iff, and_iff_left hI.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
have mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
have mpr : Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mpr : Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
have mp₁ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mpr : Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mp₁ mp₂ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
have mp₃ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mpr : Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mp₁ mp₂ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mp₃ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
have mp₄ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → ¬M.Indep (J ∪ I)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mpr : Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mp₁ mp₂ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mp₃ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J
mp₄ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → ¬M.Indep (J ∪ I)
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
have mp₅ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → J ⊆ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mpr : Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mp₁ mp₂ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mp₃ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J
mp₄ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → ¬M.Indep (J ∪ I)
mp₅ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → J ⊆ M.E
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
have mpr₁ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mpr : Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mp₁ mp₂ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mp₃ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J
mp₄ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → ¬M.Indep (J ∪ I)
mp₅ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → J ⊆ M.E
mpr₁ mpr₂ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
have mpr₃ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mpr : Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mp₁ mp₂ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mp₃ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J
mp₄ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → ¬M.Indep (J ∪ I)
mp₅ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → J ⊆ M.E
mpr₁ mpr₂ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mpr₃ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I))
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
have mpr₄ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → J ⊆ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mpr : Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mp₁ mp₂ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mp₃ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J
mp₄ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → ¬M.Indep (J ∪ I)
mp₅ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → J ⊆ M.E
mpr₁ mpr₂ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mpr₃ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I))
mpr₄ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → J ⊆ M.E
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
have mpr₅ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → Disjoint I J
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mpr : Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mp₁ mp₂ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mp₃ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J
mp₄ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → ¬M.Indep (J ∪ I)
mp₅ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → J ⊆ M.E
mpr₁ mpr₂ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mpr₃ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I))
mpr₄ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → J ⊆ M.E
mpr₅ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → Disjoint I J
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
have mp₆ : J ⊆ M.E → Disjoint I J → M.Indep (J ∪ I) → ¬Disjoint I J → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mpr : Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mp₁ mp₂ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mp₃ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J
mp₄ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → ¬M.Indep (J ∪ I)
mp₅ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → J ⊆ M.E
mpr₁ mpr₂ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mpr₃ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I))
mpr₄ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → J ⊆ M.E
mpr₅ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → Disjoint I J
mp₆ : J ⊆ M.E → Disjoint I J → M.Indep (J ∪ I) → ¬Disjoint I J → False
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
have mp₇ : J ⊆ M.E → Disjoint I J → M.Indep (J ∪ I) → ¬M.Indep (J ∪ I) → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mpr : Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mp₁ mp₂ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mp₃ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J
mp₄ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → ¬M.Indep (J ∪ I)
mp₅ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → J ⊆ M.E
mpr₁ mpr₂ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mpr₃ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I))
mpr₄ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → J ⊆ M.E
mpr₅ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → Disjoint I J
mp₆ : J ⊆ M.E → Disjoint I J → M.Indep (J ∪ I) → ¬Disjoint I J → False
mp₇ : J ⊆ M.E → Disjoint I J → M.Indep (J ∪ I) → ¬M.Indep (J ∪ I) → False
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
have mpr₆ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → Disjoint I J → M.Indep (J ∪ I) → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ M ／ X = M ／ I ＼ (X \ I)
have nth_rw : (M✶ ＼ I ＼ (X \ I)).E = (M✶ ＼ I ／ (X \ I)).E ∧
  ∀ ⦃I_1 : Set α⦄, I_1 ⊆ (M✶ ＼ I ＼ (X \ I)).E → ((M✶ ＼ I ＼ (X \ I)).Indep I_1 ↔ (M✶ ＼ I ／ (X \ I)).Indep I_1)
Tactic: nth_rw 1 [← diff_union_of_subset hI.subset, ← dual_inj, dual_contract_delete, dual_contract,
    union_comm, ← delete_delete, ext_iff_indep]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ (M✶ ＼ I ＼ (X \ I)).E = (M✶ ＼ I ／ (X \ I)).E ∧
    ∀ ⦃I_1 : Set α⦄, I_1 ⊆ (M✶ ＼ I ＼ (X \ I)).E → ((M✶ ＼ I ＼ (X \ I)).Indep I_1 ↔ (M✶ ＼ I ／ (X \ I)).Indep I_1)
have refine : ∀ (J : Set α) (hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E), (M✶ ＼ I ＼ (X \ I)).Indep J ↔ (M✶ ＼ I ／ (X \ I)).Indep J
Tactic: refine ⟨rfl, fun J hJ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ e ∈ (M✶ ＼ I).coloops
have rw : e ∈ M.closure X \ I
Tactic: rw [← dual_contract, dual_coloops, ← IsLoop, ← singleton_dep, hI.indep.contract_dep_iff,
      singleton_union, and_iff_right (by simpa using he.2), hI.indep.insert_dep_iff,
      hI.closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
⊢ (M✶ ＼ I ＼ (X \ I)).Indep J ↔ (M✶ ＼ I ／ (X \ I)).Indep J
have hss : X \ I ⊆ (M✶ ＼ I).coloops
Tactic: have hss : X \ I ⊆ (M✶ ＼ I).coloops := fun e he ↦ by
    rw [← dual_contract, dual_coloops, ← IsLoop, ← singleton_dep, hI.indep.contract_dep_iff,
      singleton_union, and_iff_right (by simpa using he.2), hI.indep.insert_dep_iff,
      hI.closure_eq_closure]
    exact diff_subset_diff_left (M.subset_closure X) he
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
hss : X \ I ⊆ (M✶ ＼ I).coloops
⊢ (M✶ ＼ I ＼ (X \ I)).Indep J ↔ (M✶ ＼ I ／ (X \ I)).Indep J
have rw : (M✶ ＼ I ＼ (X \ I)).Indep J ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep (J ∪ X \ I)
Tactic: rw [((coloops_indep _).subset hss).contract_indep_iff, delete_indep_iff,
    union_indep_iff_indep_of_subset_coloops hss, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
hss : X \ I ⊆ (M✶ ＼ I).coloops
rw : (M✶ ＼ I ＼ (X \ I)).Indep J ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep (J ∪ X \ I)
⊢ (M✶ ＼ I ＼ (X \ I)).Indep J ↔ (M✶ ＼ I ／ (X \ I)).Indep J
have rw₁ : (M✶ ＼ I).Indep J ∧ Disjoint J (X \ I) ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep (J ∪ X \ I)
Tactic: rw [((coloops_indep _).subset hss).contract_indep_iff, delete_indep_iff,
    union_indep_iff_indep_of_subset_coloops hss, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
hss : X \ I ⊆ (M✶ ＼ I).coloops
rw : (M✶ ＼ I ＼ (X \ I)).Indep J ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep (J ∪ X \ I)
rw₁ : (M✶ ＼ I).Indep J ∧ Disjoint J (X \ I) ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep (J ∪ X \ I)
⊢ (M✶ ＼ I ＼ (X \ I)).Indep J ↔ (M✶ ＼ I ／ (X \ I)).Indep J
have rw₂ : (M✶ ＼ I).Indep J ∧ Disjoint J (X \ I) ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep J
Tactic: rw [((coloops_indep _).subset hss).contract_indep_iff, delete_indep_iff,
    union_indep_iff_indep_of_subset_coloops hss, and_comm]