awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJI : insert (f x) (f '' I) = f '' J
hJ : (M.map f hf).Indep (f '' J)
hrw : f '' insert x I = f '' J
mpr : ∀ (hJ : (M.map f hf).Indep (f '' insert x I)) (hrw : f '' insert x I = f '' J), M.Indep (insert x I)
⊢ M.Indep (insert x I)
have mpr₁ : ∀ (hJ : M.Indep (insert x I)) (hrw : f '' insert x I = f '' J), M.Indep (insert x I)
Tactic: rwa [← hrw, map_image_indep_iff (insert_subset hxE hI.subset_ground)] at hJ
Cleared hypotheses: hJ, hrw
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
⊢ (M ↾ R).Spanning S ↔ R ⊆ M.closure S
have rw : (M ↾ R).closure S = (M ↾ R).E ∧ S ⊆ (M ↾ R).E ↔ R ⊆ M.closure S
Tactic: rw [spanning_iff, restrict_ground_eq, and_iff_left hSR, restrict_closure_eq _ hSR, inter_eq_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
rw : (M ↾ R).closure S = (M ↾ R).E ∧ S ⊆ (M ↾ R).E ↔ R ⊆ M.closure S
⊢ (M ↾ R).Spanning S ↔ R ⊆ M.closure S
have rw₁ : (M ↾ R).closure S = R ∧ S ⊆ R ↔ R ⊆ M.closure S
Tactic: rw [spanning_iff, restrict_ground_eq, and_iff_left hSR, restrict_closure_eq _ hSR, inter_eq_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
rw : (M ↾ R).closure S = (M ↾ R).E ∧ S ⊆ (M ↾ R).E ↔ R ⊆ M.closure S
rw₁ : (M ↾ R).closure S = R ∧ S ⊆ R ↔ R ⊆ M.closure S
⊢ (M ↾ R).Spanning S ↔ R ⊆ M.closure S
have rw₂ : (M ↾ R).closure S = R ↔ R ⊆ M.closure S
Tactic: rw [spanning_iff, restrict_ground_eq, and_iff_left hSR, restrict_closure_eq _ hSR, inter_eq_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
rw : (M ↾ R).closure S = (M ↾ R).E ∧ S ⊆ (M ↾ R).E ↔ R ⊆ M.closure S
rw₁ : (M ↾ R).closure S = R ∧ S ⊆ R ↔ R ⊆ M.closure S
rw₂ : (M ↾ R).closure S = R ↔ R ⊆ M.closure S
⊢ (M ↾ R).Spanning S ↔ R ⊆ M.closure S
have rw₃ : M.closure S ∩ R = R ↔ R ⊆ M.closure S
Tactic: rw [spanning_iff, restrict_ground_eq, and_iff_left hSR, restrict_closure_eq _ hSR, inter_eq_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
rw : (M ↾ R).closure S = (M ↾ R).E ∧ S ⊆ (M ↾ R).E ↔ R ⊆ M.closure S
rw₁ : (M ↾ R).closure S = R ∧ S ⊆ R ↔ R ⊆ M.closure S
rw₂ : (M ↾ R).closure S = R ↔ R ⊆ M.closure S
rw₃ : M.closure S ∩ R = R ↔ R ⊆ M.closure S
⊢ (M ↾ R).Spanning S ↔ R ⊆ M.closure S
have rw₄ : R ⊆ M.closure S ↔ R ⊆ M.closure S
Tactic: rw [spanning_iff, restrict_ground_eq, and_iff_left hSR, restrict_closure_eq _ hSR, inter_eq_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
R S : Set α
⊢ (M ↾ R).Spanning S ↔ R ∩ M.E ⊆ M.closure S ∧ S ⊆ R
have rw : S ⊆ R → (R ∩ M.E ⊆ M.closure (S ∩ R) ↔ R ∩ M.E ⊆ M.closure S)
Tactic: rw [spanning_iff, restrict_closure_eq', restrict_ground_eq, and_congr_left_iff,
    diff_eq_compl_inter, ← union_inter_distrib_right, inter_eq_right, union_comm,
    ← diff_subset_iff, diff_compl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Closure (goal)
Goal:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
⊢ R ∩ M.E ⊆ M.closure (S ∩ R) ↔ R ∩ M.E ⊆ M.closure S
have rw : R ∩ M.E ⊆ M.closure S ↔ R ∩ M.E ⊆ M.closure S
Tactic: rw [inter_eq_self_of_subset_left hSR]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.E = ∅ ↔ M = emptyOn α
have simp : M.E = ∅ → ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)
Tactic: simp only [emptyOn, ext_iff_indep, iff_self_and]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
⊢ (emptyOn α)✶ = emptyOn α
have rw : (emptyOn α)✶.E = ∅
Tactic: rw [← ground_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M = emptyOn α ∨ M.Nonempty
have rw : M.E = ∅ ∨ M.Nonempty
Tactic: rw [← ground_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
inst : IsEmpty α
M : Matroid α
⊢ M = emptyOn α
have rw : M.E = ∅
Tactic: rw [← ground_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_2
⊢ loopyOn ∅ = emptyOn α
have rw : Eq.{u_2 + 1} (α := Set α) (E (loopyOn ∅)) ∅
Tactic: rw [← ground_eq_empty_iff, loopyOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_2
rw : Eq.{u_2 + 1} (α := Set α) (E (loopyOn ∅)) ∅
⊢ loopyOn ∅ = emptyOn α
have rw₁ : Eq.{u_2 + 1} (α := Set α) ∅ ∅
Tactic: rw [← ground_eq_empty_iff, loopyOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I : Set α
⊢ (loopyOn E).Indep I ↔ I = ∅
have simp : I = ∅ → I ⊆ E
Tactic: simp only [loopyOn, restrict_indep_iff, emptyOn_indep_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
⊢ M = loopyOn E ↔ M.E = E ∧ ∀ X ⊆ M.E, M.Indep X → X = ∅
have simp : M.E = E → ((∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)) ↔ ∀ X ⊆ M.E, M.Indep X → X = ∅)
Tactic: simp only [ext_iff_indep, loopyOn_ground, loopyOn_indep_iff, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).IsBasis ∅ X
have rw : (loopyOn E).Indep ∅ ∧ ∅ ⊆ X ∧ ∀ (J : Set α), (loopyOn E).Indep J → ∅ ⊆ J → J ⊆ X → ∅ = J
Tactic: rw [isBasis_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E R : Set α
⊢ loopyOn E ↾ R = loopyOn R
have refine : ∀ ⦃I : Set α⦄, I ⊆ (loopyOn E ↾ R).E → ((loopyOn E ↾ R).Indep I ↔ (loopyOn R).Indep I)
Tactic: refine ext_indep rfl ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E R : Set α
⊢ ∀ ⦃I : Set α⦄, I ⊆ (loopyOn E ↾ R).E → ((loopyOn E ↾ R).Indep I ↔ (loopyOn R).Indep I)
have simp : ∀ ⦃I : Set α⦄, I ⊆ R → I = ∅ → I ⊆ R
Tactic: simp only [restrict_ground_eq, restrict_indep_iff, loopyOn_indep_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M.IsBase ∅ ↔ M = loopyOn M.E
have simp : (∀ ⦃y : Set α⦄, M.Indep y → y = ∅) ↔ ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)
Tactic: simp only [isBase_iff_maximal_indep, Maximal, empty_indep, le_eq_subset, empty_subset,
    subset_empty_iff, true_implies, true_and, ext_iff_indep, loopyOn_ground,
    loopyOn_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M = loopyOn M.E ∨ M.RankPos
have rw : M.IsBase ∅ ∨ ¬M.IsBase ∅
Tactic: rw [← empty_isBase_iff, rankPos_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ ¬M.RankPos ↔ M = loopyOn M.E
have rw : ¬¬M.IsBase ∅ ↔ M = loopyOn M.E
Tactic: rw [rankPos_iff, not_iff_comm, empty_isBase_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
rw : ¬¬M.IsBase ∅ ↔ M = loopyOn M.E
⊢ ¬M.RankPos ↔ M = loopyOn M.E
have rw₁ : ¬M = loopyOn M.E ↔ ¬M.IsBase ∅
Tactic: rw [rankPos_iff, not_iff_comm, empty_isBase_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
rw : ¬¬M.IsBase ∅ ↔ M = loopyOn M.E
rw₁ : ¬M = loopyOn M.E ↔ ¬M.IsBase ∅
⊢ ¬M.RankPos ↔ M = loopyOn M.E
have rw₂ : ¬M = loopyOn M.E ↔ ¬M = loopyOn M.E
Tactic: rw [rankPos_iff, not_iff_comm, empty_isBase_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E : Set α
⊢ (freeOn E)✶ = loopyOn E
have rw : (loopyOn E)✶✶ = loopyOn E
Tactic: rw [freeOn, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E : Set α
rw : (loopyOn E)✶✶ = loopyOn E
⊢ (freeOn E)✶ = loopyOn E
have rw₁ : loopyOn E = loopyOn E
Tactic: rw [freeOn, dual_dual]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I X : Set α
⊢ (freeOn E).IsBasis I X ↔ I = X ∧ X ⊆ E
have mpr : I = X ∧ X ⊆ E → (freeOn E).IsBasis I X
Tactic: use fun h ↦ ⟨(freeOn_indep h.subset_ground).eq_of_isBasis h, h.subset_ground⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I X : Set α
⊢ (freeOn E).IsBasis' I X ↔ I = X ∩ E
have rw : (freeOn E).IsBasis I (X ∩ (freeOn E).E) ↔ I = X ∩ E
Tactic: rw [isBasis'_iff_isBasis_inter_ground, freeOn_isBasis_iff, freeOn_ground,
    and_iff_left inter_subset_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I X : Set α
rw : (freeOn E).IsBasis I (X ∩ (freeOn E).E) ↔ I = X ∩ E
⊢ (freeOn E).IsBasis' I X ↔ I = X ∩ E
have rw₁ : I = X ∩ (freeOn E).E ∧ X ∩ (freeOn E).E ⊆ E ↔ I = X ∩ E
Tactic: rw [isBasis'_iff_isBasis_inter_ground, freeOn_isBasis_iff, freeOn_ground,
    and_iff_left inter_subset_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I X : Set α
rw : (freeOn E).IsBasis I (X ∩ (freeOn E).E) ↔ I = X ∩ E
rw₁ : I = X ∩ (freeOn E).E ∧ X ∩ (freeOn E).E ⊆ E ↔ I = X ∩ E
⊢ (freeOn E).IsBasis' I X ↔ I = X ∩ E
have rw₂ : I = X ∩ E ∧ X ∩ E ⊆ E ↔ I = X ∩ E
Tactic: rw [isBasis'_iff_isBasis_inter_ground, freeOn_isBasis_iff, freeOn_ground,
    and_iff_left inter_subset_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I X : Set α
rw : (freeOn E).IsBasis I (X ∩ (freeOn E).E) ↔ I = X ∩ E
rw₁ : I = X ∩ (freeOn E).E ∧ X ∩ (freeOn E).E ⊆ E ↔ I = X ∩ E
rw₂ : I = X ∩ E ∧ X ∩ E ⊆ E ↔ I = X ∩ E
⊢ (freeOn E).IsBasis' I X ↔ I = X ∩ E
have rw₃ : I = X ∩ E ↔ I = X ∩ E
Tactic: rw [isBasis'_iff_isBasis_inter_ground, freeOn_isBasis_iff, freeOn_ground,
    and_iff_left inter_subset_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
⊢ M = freeOn E ↔ M.E = E ∧ M.Indep E
have refine_1 : M = freeOn E → M.E = E ∧ M.Indep E
Tactic: refine ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
refine_1 : M = freeOn E → M.E = E ∧ M.Indep E
⊢ M = freeOn E ↔ M.E = E ∧ M.Indep E
have refine_2 : ∀ (h : M.E = E ∧ M.Indep E), M = freeOn E
Tactic: refine ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
E : Set α
h : M.E = E ∧ M.Indep E
⊢ M = freeOn E
have refine_2 : ∀ ⦃I : Set α⦄, I ⊆ E → (M.Indep I ↔ I ⊆ E)
Tactic: simp only [ext_iff_indep, freeOn_ground, freeOn_indep_iff, h.1, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M ↾ I = freeOn I ↔ M.Indep I
have rw : (M ↾ I).E = I ∧ (M ↾ I).Indep I ↔ M.Indep I
Tactic: rw [eq_freeOn_iff, and_iff_right M.restrict_ground_eq, restrict_indep_iff,
    and_iff_left Subset.rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
rw : (M ↾ I).E = I ∧ (M ↾ I).Indep I ↔ M.Indep I
⊢ M ↾ I = freeOn I ↔ M.Indep I
have rw₁ : (M ↾ I).Indep I ↔ M.Indep I
Tactic: rw [eq_freeOn_iff, and_iff_right M.restrict_ground_eq, restrict_indep_iff,
    and_iff_left Subset.rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
rw : (M ↾ I).E = I ∧ (M ↾ I).Indep I ↔ M.Indep I
rw₁ : (M ↾ I).Indep I ↔ M.Indep I
⊢ M ↾ I = freeOn I ↔ M.Indep I
have rw₂ : M.Indep I ∧ I ⊆ I ↔ M.Indep I
Tactic: rw [eq_freeOn_iff, and_iff_right M.restrict_ground_eq, restrict_indep_iff,
    and_iff_left Subset.rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
rw : (M ↾ I).E = I ∧ (M ↾ I).Indep I ↔ M.Indep I
rw₁ : (M ↾ I).Indep I ↔ M.Indep I
rw₂ : M.Indep I ∧ I ⊆ I ↔ M.Indep I
⊢ M ↾ I = freeOn I ↔ M.Indep I
have rw₃ : M.Indep I ↔ M.Indep I
Tactic: rw [eq_freeOn_iff, and_iff_right M.restrict_ground_eq, restrict_indep_iff,
    and_iff_left Subset.rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
E B I X R J : Set α
⊢ (freeOn E).Finitary
have simp : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → J ⊆ E) → I ⊆ E
Tactic: simp only [finitary_iff, freeOn_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E B I : Set α
hIE : I ⊆ E
⊢ (uniqueBaseOn I E).IsBase B ↔ B = I
have rw : (freeOn I ↾ E).IsBase B ↔ B = I
Tactic: rw [uniqueBaseOn, isBase_restrict_iff', freeOn_isBasis'_iff, inter_eq_self_of_subset_right hIE]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E B I : Set α
hIE : I ⊆ E
rw : (freeOn I ↾ E).IsBase B ↔ B = I
⊢ (uniqueBaseOn I E).IsBase B ↔ B = I
have rw₁ : (freeOn I).IsBasis' B E ↔ B = I
Tactic: rw [uniqueBaseOn, isBase_restrict_iff', freeOn_isBasis'_iff, inter_eq_self_of_subset_right hIE]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E B I : Set α
hIE : I ⊆ E
rw : (freeOn I ↾ E).IsBase B ↔ B = I
rw₁ : (freeOn I).IsBasis' B E ↔ B = I
⊢ (uniqueBaseOn I E).IsBase B ↔ B = I
have rw₂ : B = E ∩ I ↔ B = I
Tactic: rw [uniqueBaseOn, isBase_restrict_iff', freeOn_isBasis'_iff, inter_eq_self_of_subset_right hIE]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E B I : Set α
hIE : I ⊆ E
rw : (freeOn I ↾ E).IsBase B ↔ B = I
rw₁ : (freeOn I).IsBasis' B E ↔ B = I
rw₂ : B = E ∩ I ↔ B = I
⊢ (uniqueBaseOn I E).IsBase B ↔ B = I
have rw₃ : B = I ↔ B = I
Tactic: rw [uniqueBaseOn, isBase_restrict_iff', freeOn_isBasis'_iff, inter_eq_self_of_subset_right hIE]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E : Set α
⊢ uniqueBaseOn (I ∩ E) E = uniqueBaseOn I E
have simp : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
Tactic: simp only [uniqueBaseOn, restrict_eq_restrict_iff, freeOn_indep_iff, subset_inter_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E : Set α
tauto tauto₁ : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
⊢ ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
have mp : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E → I_1 ⊆ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E : Set α
tauto tauto₁ : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
mp : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E → I_1 ⊆ I
⊢ ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
have mpr : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ I ∧ I_1 ⊆ E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E : Set α
tauto tauto₁ : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
mp : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E → I_1 ⊆ I
mpr : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ I ∧ I_1 ⊆ E
⊢ ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
have mp₁ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E : Set α
tauto tauto₁ : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
mp : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E → I_1 ⊆ I
mpr : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ I ∧ I_1 ⊆ E
mp₁ mp₂ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ I
⊢ ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
have mp₃ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ E → ∀ ⦃a : α⦄, a ∈ I_1 → a ∈ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E : Set α
tauto tauto₁ : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
mp : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E → I_1 ⊆ I
mpr : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ I ∧ I_1 ⊆ E
mp₁ mp₂ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ I
mp₃ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ E → ∀ ⦃a : α⦄, a ∈ I_1 → a ∈ I
mpr₁ mpr₂ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ I ∧ I_1 ⊆ E
⊢ ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
have mpr₃ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E : Set α
tauto tauto₁ : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
mp : ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E → I_1 ⊆ I
mpr : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ I ∧ I_1 ⊆ E
mp₁ mp₂ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ I
mp₃ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ E → ∀ ⦃a : α⦄, a ∈ I_1 → a ∈ I
mpr₁ mpr₂ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ I ∧ I_1 ⊆ E
mpr₃ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ I
⊢ ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
have mpr₄ : ∀ I_1 ⊆ E, I_1 ⊆ I → I_1 ⊆ E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I J : Set α
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I ∩ E
have rw : (freeOn I ↾ E).Indep J ↔ J ⊆ I ∩ E
Tactic: rw [uniqueBaseOn, restrict_indep_iff, freeOn_indep_iff, subset_inter_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I J : Set α
rw : (freeOn I ↾ E).Indep J ↔ J ⊆ I ∩ E
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I ∩ E
have rw₁ : (freeOn I).Indep J ∧ J ⊆ E ↔ J ⊆ I ∩ E
Tactic: rw [uniqueBaseOn, restrict_indep_iff, freeOn_indep_iff, subset_inter_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I J : Set α
rw : (freeOn I ↾ E).Indep J ↔ J ⊆ I ∩ E
rw₁ : (freeOn I).Indep J ∧ J ⊆ E ↔ J ⊆ I ∩ E
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I ∩ E
have rw₂ : J ⊆ I ∧ J ⊆ E ↔ J ⊆ I ∩ E
Tactic: rw [uniqueBaseOn, restrict_indep_iff, freeOn_indep_iff, subset_inter_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I J : Set α
rw : (freeOn I ↾ E).Indep J ↔ J ⊆ I ∩ E
rw₁ : (freeOn I).Indep J ∧ J ⊆ E ↔ J ⊆ I ∩ E
rw₂ : J ⊆ I ∧ J ⊆ E ↔ J ⊆ I ∩ E
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I ∩ E
have rw₃ : J ⊆ I ∧ J ⊆ E ↔ J ⊆ I ∧ J ⊆ E
Tactic: rw [uniqueBaseOn, restrict_indep_iff, freeOn_indep_iff, subset_inter_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I
have rw : J ⊆ I → J ⊆ E
Tactic: rw [uniqueBaseOn, restrict_indep_iff, freeOn_indep_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ (uniqueBaseOn I E).IsBasis J X ↔ J = X ∩ I
have rw : Maximal (fun (I_1 : Set α) ↦ (uniqueBaseOn I E).Indep I_1 ∧ I_1 ⊆ X) J ↔ J = X ∩ I
Tactic: rw [isBasis_iff_maximal]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I X : Set α
hX : X ⊆ E
⊢ (uniqueBaseOn I E).IsBasis (X ∩ I) X
have rw : X ∩ I = X ∩ I
Tactic: rw [uniqueBaseOn_isBasis_iff hX]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E : Set α
⊢ (uniqueBaseOn I E)✶ = uniqueBaseOn (E \ I) E
have rw : (uniqueBaseOn (I ∩ E) E)✶ = uniqueBaseOn (E \ I) E
Tactic: rw [← uniqueBaseOn_inter_ground_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E : Set α
⊢ (uniqueBaseOn (I ∩ E) E)✶ = uniqueBaseOn (E \ I) E
have refine : ∀ (B : Set α) (hB : B ⊆ E), (uniqueBaseOn (I ∩ E) E)✶.IsBase B ↔ (uniqueBaseOn (E \ I) E).IsBase B
Tactic: refine ext_isBase rfl (fun B (hB : B ⊆ E) ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E B : Set α
hB : B ⊆ E
⊢ (uniqueBaseOn (I ∩ E) E)✶.IsBase B ↔ (uniqueBaseOn (E \ I) E).IsBase B
have rw : E \ B = I ∩ E ↔ B = E \ I
Tactic: rw [dual_isBase_iff, uniqueBaseOn_isBase_iff inter_subset_right,
    uniqueBaseOn_isBase_iff diff_subset, uniqueBaseOn_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E B : Set α
hB : B ⊆ E
h : E \ B = I ∩ E
⊢ B = E \ I
have rw : E \ (E \ B) = E \ I
Tactic: rw [← diff_diff_cancel_left hB, h, diff_inter_self_eq_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E B : Set α
hB : B ⊆ E
h : E \ B = I ∩ E
rw : E \ (E \ B) = E \ I
⊢ B = E \ I
have rw₁ : E \ (I ∩ E) = E \ I
Tactic: rw [← diff_diff_cancel_left hB, h, diff_inter_self_eq_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E B : Set α
hB : B ⊆ E
h : E \ B = I ∩ E
rw : E \ (E \ B) = E \ I
rw₁ : E \ (I ∩ E) = E \ I
⊢ B = E \ I
have rw₂ : E \ I = E \ I
Tactic: rw [← diff_diff_cancel_left hB, h, diff_inter_self_eq_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E B : Set α
hB : B ⊆ E
h : B = E \ I
⊢ E \ B = I ∩ E
have rw : E \ (E \ I) = E ∩ I
Tactic: rw [h, inter_comm I]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I : Set α
⊢ uniqueBaseOn I I = freeOn I
have rw : freeOn I ↾ I = freeOn I
Tactic: rw [uniqueBaseOn, freeOn_restrict rfl.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I : Set α
rw : freeOn I ↾ I = freeOn I
⊢ uniqueBaseOn I I = freeOn I
have rw₁ : freeOn I = freeOn I
Tactic: rw [uniqueBaseOn, freeOn_restrict rfl.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I : Set α
⊢ uniqueBaseOn ∅ I = loopyOn I
have rw : (uniqueBaseOn ∅ I)✶ = (loopyOn I)✶
Tactic: rw [← dual_inj, uniqueBaseOn_dual_eq, diff_empty, uniqueBaseOn_self, loopyOn_dual_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I : Set α
rw : (uniqueBaseOn ∅ I)✶ = (loopyOn I)✶
⊢ uniqueBaseOn ∅ I = loopyOn I
have rw₁ : uniqueBaseOn (I \ ∅) I = (loopyOn I)✶
Tactic: rw [← dual_inj, uniqueBaseOn_dual_eq, diff_empty, uniqueBaseOn_self, loopyOn_dual_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I : Set α
rw : (uniqueBaseOn ∅ I)✶ = (loopyOn I)✶
rw₁ : uniqueBaseOn (I \ ∅) I = (loopyOn I)✶
⊢ uniqueBaseOn ∅ I = loopyOn I
have rw₂ : uniqueBaseOn I I = (loopyOn I)✶
Tactic: rw [← dual_inj, uniqueBaseOn_dual_eq, diff_empty, uniqueBaseOn_self, loopyOn_dual_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I : Set α
rw : (uniqueBaseOn ∅ I)✶ = (loopyOn I)✶
rw₁ : uniqueBaseOn (I \ ∅) I = (loopyOn I)✶
rw₂ : uniqueBaseOn I I = (loopyOn I)✶
⊢ uniqueBaseOn ∅ I = loopyOn I
have rw₃ : freeOn I = (loopyOn I)✶
Tactic: rw [← dual_inj, uniqueBaseOn_dual_eq, diff_empty, uniqueBaseOn_self, loopyOn_dual_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I : Set α
rw : (uniqueBaseOn ∅ I)✶ = (loopyOn I)✶
rw₁ : uniqueBaseOn (I \ ∅) I = (loopyOn I)✶
rw₂ : uniqueBaseOn I I = (loopyOn I)✶
rw₃ : freeOn I = (loopyOn I)✶
⊢ uniqueBaseOn ∅ I = loopyOn I
have rw₄ : freeOn I = freeOn I
Tactic: rw [← dual_inj, uniqueBaseOn_dual_eq, diff_empty, uniqueBaseOn_self, loopyOn_dual_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E R : Set α
⊢ uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R ∩ E) R
have simp_rw : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R ↔ ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R)
Tactic: simp_rw [ext_iff_indep, restrict_ground_eq, uniqueBaseOn_ground, true_and,
    restrict_indep_iff, uniqueBaseOn_indep_iff', subset_inter_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
I E R : Set α
tauto tauto₁ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R ↔ ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R)
⊢ ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R ↔ ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R)
have mp : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
Tactic: tauto