awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
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
have h : I ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ R) K ∧ K ⊆ A) J
Tactic: use J
-- 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 α
hJ : M.IsBasis' J A
hIJ : I ⊆ J
⊢ I ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ R) K ∧ K ⊆ A) J
have h : ∀ ⦃t : Set α⦄, M.Indep t → t ⊆ R → t ⊆ A → J ⊆ t → J = t
Tactic: simp only [hIJ, and_assoc, maximal_subset_iff, hJ.indep, hJ.subset, and_imp, true_and,
      hJ.subset.trans hAR]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R X : Set α
⊢ (M ↾ R).Dep X ↔ ¬M.Indep X ∧ X ⊆ R
have rw : ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
Tactic: rw [Dep, restrict_indep_iff, restrict_ground_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R X : Set α
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
have mp : ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R → ¬M.Indep X ∧ X ⊆ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R X : Set α
mp : ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R → ¬M.Indep X ∧ X ⊆ R
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
have mpr : ¬M.Indep X ∧ X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R X : Set α
mp : ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mpr : ¬M.Indep X ∧ X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
have mp₁ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X ∧ X ⊆ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R X : Set α
mp : ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mpr : ¬M.Indep X ∧ X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
mp₁ mp₂ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X ∧ X ⊆ R
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
have mp₃ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R X : Set α
mp : ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mpr : ¬M.Indep X ∧ X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
mp₁ mp₂ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mp₃ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
have mp₄ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → X ⊆ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R X : Set α
mp : ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mpr : ¬M.Indep X ∧ X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
mp₁ mp₂ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mp₃ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → X ⊆ R
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
have mpr₁ : ¬M.Indep X → X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R X : Set α
mp : ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mpr : ¬M.Indep X ∧ X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
mp₁ mp₂ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mp₃ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → X ⊆ R
mpr₁ mpr₂ : ¬M.Indep X → X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
have mpr₃ : ¬M.Indep X → X ⊆ R → ¬(M.Indep X ∧ X ⊆ R)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R X : Set α
mp : ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mpr : ¬M.Indep X ∧ X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
mp₁ mp₂ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mp₃ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → X ⊆ R
mpr₁ mpr₂ : ¬M.Indep X → X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
mpr₃ : ¬M.Indep X → X ⊆ R → ¬(M.Indep X ∧ X ⊆ R)
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
have mpr₄ : ¬M.Indep X → X ⊆ R → X ⊆ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R X : Set α
mp : ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mpr : ¬M.Indep X ∧ X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
mp₁ mp₂ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mp₃ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → X ⊆ R
mpr₁ mpr₂ : ¬M.Indep X → X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
mpr₃ : ¬M.Indep X → X ⊆ R → ¬(M.Indep X ∧ X ⊆ R)
mpr₄ : ¬M.Indep X → X ⊆ R → X ⊆ R
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
have mp₅ : X ⊆ R → M.Indep X → ¬M.Indep X → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R X : Set α
mp : ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mpr : ¬M.Indep X ∧ X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
mp₁ mp₂ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mp₃ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → X ⊆ R
mpr₁ mpr₂ : ¬M.Indep X → X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
mpr₃ : ¬M.Indep X → X ⊆ R → ¬(M.Indep X ∧ X ⊆ R)
mpr₄ : ¬M.Indep X → X ⊆ R → X ⊆ R
mp₅ : X ⊆ R → M.Indep X → ¬M.Indep X → False
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
have mp₆ : X ⊆ R → M.Indep X → ¬X ⊆ R → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R X : Set α
mp : ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mpr : ¬M.Indep X ∧ X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
mp₁ mp₂ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X ∧ X ⊆ R
mp₃ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ X ⊆ R) → X ⊆ R → X ⊆ R
mpr₁ mpr₂ : ¬M.Indep X → X ⊆ R → ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R
mpr₃ : ¬M.Indep X → X ⊆ R → ¬(M.Indep X ∧ X ⊆ R)
mpr₄ : ¬M.Indep X → X ⊆ R → X ⊆ R
mp₅ : X ⊆ R → M.Indep X → ¬M.Indep X → False
mp₆ : X ⊆ R → M.Indep X → ¬X ⊆ R → False
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
have mpr₅ : ¬M.Indep X → X ⊆ R → M.Indep X → X ⊆ R → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M ↾ M.E = M
have refine : ∀ ⦃I : Set α⦄, I ⊆ (M ↾ M.E).E → ((M ↾ M.E).Indep I ↔ M.Indep I)
Tactic: refine ext_indep rfl ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
⊢ M ↾ R₁ ↾ R₂ = M ↾ R₂
have refine : ∀ ⦃I : Set α⦄, I ⊆ (M ↾ R₁ ↾ R₂).E → ((M ↾ R₁ ↾ R₂).Indep I ↔ (M ↾ R₂).Indep I)
Tactic: refine ext_indep rfl ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
⊢ ∀ ⦃I : Set α⦄, I ⊆ (M ↾ R₁ ↾ R₂).E → ((M ↾ R₁ ↾ R₂).Indep I ↔ (M ↾ R₂).Indep I)
have simp : ∀ ⦃I : Set α⦄, I ⊆ R₂ → I ⊆ R₂ → M.Indep I → I ⊆ R₁
Tactic: simp only [restrict_ground_eq, restrict_indep_iff, and_congr_left_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
⊢ M ↾ R ↾ R = M ↾ R
have rw : M ↾ R = M ↾ R
Tactic: rw [M.restrict_restrict_eq Subset.rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ (M ↾ X).IsBase I ↔ M.IsBasis I X
have simp_rw : Maximal (M ↾ X).Indep I ↔ M.IsBasis I X
Tactic: simp_rw [isBase_iff_maximal_indep, IsBasis, and_iff_left hX, maximal_iff, restrict_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
simp_rw : Maximal (M ↾ X).Indep I ↔ M.IsBasis I X
⊢ (M ↾ X).IsBase I ↔ M.IsBasis I X
have simp_rw₁ : Maximal (M ↾ X).Indep I ↔ Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E
Tactic: simp_rw [isBase_iff_maximal_indep, IsBasis, and_iff_left hX, maximal_iff, restrict_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
simp_rw : Maximal (M ↾ X).Indep I ↔ M.IsBasis I X
simp_rw₁ : Maximal (M ↾ X).Indep I ↔ Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E
⊢ (M ↾ X).IsBase I ↔ M.IsBasis I X
have simp_rw₂ : Maximal (M ↾ X).Indep I ↔ Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ X) I
Tactic: simp_rw [isBase_iff_maximal_indep, IsBasis, and_iff_left hX, maximal_iff, restrict_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
simp_rw : Maximal (M ↾ X).Indep I ↔ M.IsBasis I X
simp_rw₁ : Maximal (M ↾ X).Indep I ↔ Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E
simp_rw₂ : Maximal (M ↾ X).Indep I ↔ Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ X) I
⊢ (M ↾ X).IsBase I ↔ M.IsBasis I X
have simp_rw₃ : ((M ↾ X).Indep I ∧ ∀ ⦃y : Set α⦄, (M ↾ X).Indep y → I ≤ y → I = y) ↔
  (M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y ∧ y ⊆ X → I ≤ y → I = y
Tactic: simp_rw [isBase_iff_maximal_indep, IsBasis, and_iff_left hX, maximal_iff, restrict_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
⊢ (M ↾ X).IsBase I ↔ M.IsBasis' I X
have simp_rw : Maximal (M ↾ X).Indep I ↔ M.IsBasis' I X
Tactic: simp_rw [isBase_iff_maximal_indep, IsBasis', maximal_iff, restrict_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
simp_rw : Maximal (M ↾ X).Indep I ↔ M.IsBasis' I X
⊢ (M ↾ X).IsBase I ↔ M.IsBasis' I X
have simp_rw₁ : Maximal (M ↾ X).Indep I ↔ Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ X) I
Tactic: simp_rw [isBase_iff_maximal_indep, IsBasis', maximal_iff, restrict_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
simp_rw : Maximal (M ↾ X).Indep I ↔ M.IsBasis' I X
simp_rw₁ : Maximal (M ↾ X).Indep I ↔ Maximal (fun (A : Set α) ↦ M.Indep A ∧ A ⊆ X) I
⊢ (M ↾ X).IsBase I ↔ M.IsBasis' I X
have simp_rw₂ : ((M ↾ X).Indep I ∧ ∀ ⦃y : Set α⦄, (M ↾ X).Indep y → I ≤ y → I = y) ↔
  (M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y ∧ y ⊆ X → I ≤ y → I = y
Tactic: simp_rw [isBase_iff_maximal_indep, IsBasis', maximal_iff, restrict_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R_1 I X Y : Set α
inst : M.Finitary
R : Set α
⊢ (M ↾ R).Finitary
have refine : ∀ (I : Set α) (hI : ∀ J ⊆ I, J.Finite → (M ↾ R).Indep J), (M ↾ R).Indep I
Tactic: refine ⟨fun I hI ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
M : Matroid α
R_1 I_1 X Y : Set α
inst : M.Finitary
R I : Set α
hI : ∀ J ⊆ I, J.Finite → (M ↾ R).Indep J
⊢ (M ↾ R).Indep I
have hI₁ : ∀ J ⊆ I, J.Finite → M.Indep J ∧ J ⊆ R
Tactic: simp only [restrict_indep_iff] at *
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R_1 I_1 X Y : Set α
inst : M.Finitary
R I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J ∧ J ⊆ R
⊢ M.Indep I ∧ I ⊆ R
have rw : (∀ J ⊆ I, J.Finite → M.Indep J) ∧ I ⊆ R
Tactic: rw [indep_iff_forall_finite_subset_indep]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
⊢ (M ↾ Y).IsBasis I X
have rwa : (M ↾ Y ↾ X).IsBase I
Tactic: rwa [← isBase_restrict_iff, M.restrict_restrict_eq hXY, isBase_restrict_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
rwa : (M ↾ Y ↾ X).IsBase I
⊢ (M ↾ Y).IsBasis I X
have rwa₁ : (M ↾ X).IsBase I
Tactic: rwa [← isBase_restrict_iff, M.restrict_restrict_eq hXY, isBase_restrict_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ (M ↾ R).IsBasis' I X ↔ M.IsBasis' I (X ∩ R) ∧ I ⊆ R
have simp_rw : (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) ↔
  ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
Tactic: simp_rw [IsBasis', maximal_iff, restrict_indep_iff, subset_inter_iff, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) ↔
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
have mp : (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
  ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
mp :
  (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
⊢ (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) ↔
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
have mpr : ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R →
  ((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
mp :
  (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mpr :
  ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R →
    ((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
⊢ (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) ↔
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
have mp₁ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
  I ⊆ X →
    M.Indep I → I ⊆ R → ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
mp :
  (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mpr :
  ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R →
    ((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
mp₁ mp₂ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X →
      M.Indep I →
        I ⊆ R → ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
⊢ (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) ↔
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
have mp₃ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → M.Indep I
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
mp :
  (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mpr :
  ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R →
    ((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
mp₁ mp₂ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X →
      M.Indep I →
        I ⊆ R → ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mp₃ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → M.Indep I
⊢ (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) ↔
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
have mp₄ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ X
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
mp :
  (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mpr :
  ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R →
    ((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
mp₁ mp₂ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X →
      M.Indep I →
        I ⊆ R → ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mp₃ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → M.Indep I
mp₄ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ X
⊢ (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) ↔
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
have mp₅ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
mp :
  (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mpr :
  ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R →
    ((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
mp₁ mp₂ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X →
      M.Indep I →
        I ⊆ R → ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mp₃ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → M.Indep I
mp₄ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ X
mp₅ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ R
⊢ (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) ↔
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
have mp₆ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
  I ⊆ X → M.Indep I → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
mp :
  (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mpr :
  ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R →
    ((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
mp₁ mp₂ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X →
      M.Indep I →
        I ⊆ R → ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mp₃ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → M.Indep I
mp₄ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ X
mp₅ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ R
mp₆ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X → M.Indep I → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y
mp₇ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ R
⊢ (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) ↔
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
have mpr₁ : I ⊆ R →
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) →
    M.Indep I → I ⊆ X → I ⊆ R → ((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
mp :
  (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mpr :
  ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R →
    ((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
mp₁ mp₂ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X →
      M.Indep I →
        I ⊆ R → ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
mp₃ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → M.Indep I
mp₄ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ X
mp₅ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ R
mp₆ :
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) →
    I ⊆ X → M.Indep I → I ⊆ R → ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y
mp₇ : (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) → I ⊆ X → M.Indep I → I ⊆ R → I ⊆ R
mpr₁ mpr₂ :
  I ⊆ R →
    (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) →
      M.Indep I →
        I ⊆ X → I ⊆ R → ((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y
⊢ (((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ≤ y → I = y) ↔
    ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) ∧ I ⊆ R
have mpr₃ : I ⊆ R → (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) → M.Indep I → I ⊆ X → I ⊆ R → M.Indep I
Tactic: tauto