awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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
h : ∀ ⦃t : Set α⦄, M.Indep t → t ⊆ R → t ⊆ A → J ⊆ t → J = t
⊢ I ⊆ J ∧ Maximal (fun (K : Set α) ↦ (fun (I : Set α) ↦ M.Indep I ∧ I ⊆ R) K ∧ K ⊆ A) J

Tactic:
simp only [hIJ, and_assoc, maximal_subset_iff, hJ.indep, hJ.subset, and_imp, true_and,
      hJ.subset.trans hAR]

Premises used: and_imp, HasSubset.Subset.trans, Matroid.IsBasis'.indep, maximal_subset_iff, and_assoc, Matroid.IsBasis'.subset, true_and
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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
⊢ ∀ ⦃t : Set α⦄, M.Indep t → t ⊆ R → t ⊆ A → J ⊆ t → J = t

Tactic:
fun K hK _ hKA hJK ↦ hJ.eq_of_subset_indep hK hJK hKA

Premises used: Matroid.IsBasis'.eq_of_subset_indep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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
⊢ ∀ ⦃t : Set α⦄, M.Indep t → t ⊆ R → t ⊆ A → J ⊆ t → J = t

Tactic:
exact fun K hK _ hKA hJK ↦ hJ.eq_of_subset_indep hK hJK hKA

Premises used: Matroid.IsBasis'.eq_of_subset_indep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R I : Set α
⊢ (M ↾ R).Indep I ↔ M.Indep I ∧ I ⊆ R

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R I : Set α
h : M.Indep I
hIR : I ⊆ R
⊢ (M ↾ R).Indep I

Tactic:
restrict_indep_iff.mpr ⟨h,hIR⟩

Premises used: Iff.mpr, And.intro, Matroid.restrict_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R I : Set α
hI : (M ↾ R).Indep I
⊢ M.Indep I

Tactic:
(restrict_indep_iff.1 hI).1

Premises used: And.left, Iff.mp, Matroid.restrict_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
⊢ (M ↾ R).E = R

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R.Finite
⊢ (M ↾ R).Finite

Tactic:
⟨hR⟩

Premises used: Matroid.Finite.mk
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R X : Set α
rw : ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
⊢ (M ↾ R).Dep X ↔ ¬M.Indep X ∧ X ⊆ R

Tactic:
rw [Dep, restrict_indep_iff, restrict_ground_eq]

Premises used: Matroid.Dep, Matroid.restrict_ground_eq, Matroid.restrict_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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
mpr₅ : ¬M.Indep X → X ⊆ R → M.Indep X → X ⊆ R → False
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
⊢ M ↾ M.E = M

Tactic:
ext_indep rfl ?_

Premises used: Matroid.ext_indep, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
refine : ∀ ⦃I : Set α⦄, I ⊆ (M ↾ M.E).E → ((M ↾ M.E).Indep I ↔ M.Indep I)
⊢ M ↾ M.E = M

Tactic:
refine ext_indep rfl ?_

Premises used: Matroid.ext_indep, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
⊢ ∀ ⦃I : Set α⦄, I ⊆ (M ↾ M.E).E → ((M ↾ M.E).Indep I ↔ M.Indep I)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
⊢ M ↾ R₁ ↾ R₂ = M ↾ R₂

Tactic:
ext_indep rfl ?_

Premises used: Matroid.ext_indep, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
refine : ∀ ⦃I : Set α⦄, I ⊆ (M ↾ R₁ ↾ R₂).E → ((M ↾ R₁ ↾ R₂).Indep I ↔ (M ↾ R₂).Indep I)
⊢ M ↾ R₁ ↾ R₂ = M ↾ R₂

Tactic:
refine ext_indep rfl ?_

Premises used: Matroid.ext_indep, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
simp : ∀ ⦃I : Set α⦄, I ⊆ R₂ → I ⊆ R₂ → M.Indep I → I ⊆ R₁
⊢ ∀ ⦃I : Set α⦄, I ⊆ (M ↾ R₁ ↾ R₂).E → ((M ↾ R₁ ↾ R₂).Indep I ↔ (M ↾ R₂).Indep I)

Tactic:
simp only [restrict_ground_eq, restrict_indep_iff, and_congr_left_iff, and_iff_left_iff_imp]

Premises used: Matroid.restrict_ground_eq, and_congr_left_iff, Matroid.restrict_indep_iff, and_iff_left_iff_imp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
⊢ ∀ ⦃I : Set α⦄, I ⊆ R₂ → I ⊆ R₂ → M.Indep I → I ⊆ R₁

Tactic:
fun _ h _ _ ↦ h.trans hR

Premises used: HasSubset.Subset.trans
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
⊢ ∀ ⦃I : Set α⦄, I ⊆ R₂ → I ⊆ R₂ → M.Indep I → I ⊆ R₁

Tactic:
exact fun _ h _ _ ↦ h.trans hR
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
rw rw₁ : M ↾ R = M ↾ R
⊢ M ↾ R ↾ R = M ↾ R

Tactic:
rw [M.restrict_restrict_eq Subset.rfl]

Premises used: Set.Subset.rfl, Matroid.restrict_restrict_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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
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
⊢ (M ↾ X).IsBase I ↔ M.IsBasis I X

Tactic:
simp_rw [isBase_iff_maximal_indep, IsBasis, and_iff_left hX, maximal_iff, restrict_indep_iff]

Premises used: and_iff_left, Matroid.restrict_indep_iff, maximal_iff, Matroid.isBase_iff_maximal_indep, Matroid.IsBasis
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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
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
⊢ (M ↾ X).IsBase I ↔ M.IsBasis' I X

Tactic:
simp_rw [isBase_iff_maximal_indep, IsBasis', maximal_iff, restrict_indep_iff]

Premises used: Matroid.IsBasis', Matroid.restrict_indep_iff, maximal_iff, Matroid.isBase_iff_maximal_indep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ (M ↾ X).IsBase I

Tactic:
isBase_restrict_iff'.1 hI

Premises used: Matroid.isBase_restrict_iff', Matroid.IsBasis', Iff.mp, Maximal
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X : Set α
h : M.IsBasis I X
⊢ (M ↾ X).IsBase I

Tactic:
(isBase_restrict_iff h.subset_ground).2 h

Premises used: Iff.mpr, Matroid.IsBasis.subset_ground, Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R_1 I X Y : Set α
inst : M.RankFinite
R : Set α
⊢ (M ↾ R).RankFinite

Tactic:
let ⟨_, hB⟩ := (M ↾ R).exists_isBase
  hB.rankFinite_of_finite (hB.indep.of_restrict.finite)

Premises used: _private.0.Matroid.restrict_rankFinite.match_1, Matroid.IsBase.rankFinite_of_finite, Matroid.Indep.finite, Matroid.exists_isBase, Matroid.Indep.of_restrict, Matroid.IsBase.indep, Matroid.restrict, Matroid.RankFinite
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R_1 I X Y : Set α
inst : M.Finitary
R : Set α
⊢ (M ↾ R).Finitary

Tactic:
⟨fun I hI ↦ ?_⟩

Premises used: Matroid.Finitary.mk
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R_1 I X Y : Set α
inst : M.Finitary
R : Set α
refine : ∀ (I : Set α) (hI : ∀ J ⊆ I, J.Finite → (M ↾ R).Indep J), (M ↾ R).Indep I
⊢ (M ↾ R).Finitary

Tactic:
refine ⟨fun I hI ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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
⊢ ∀ J ⊆ I, J.Finite → M.Indep J ∧ J ⊆ R

Tactic:
simp only [restrict_indep_iff] at *

Premises used: Matroid.restrict_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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
rw : (∀ J ⊆ I, J.Finite → M.Indep J) ∧ I ⊆ R
⊢ M.Indep I ∧ I ⊆ R

Tactic:
rw [indep_iff_forall_finite_subset_indep]

Premises used: Matroid.indep_iff_forall_finite_subset_indep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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
e : α
heI : e ∈ I
⊢ {e} ⊆ I

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
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
⊢ (∀ J ⊆ I, J.Finite → M.Indep J) ∧ I ⊆ R

Tactic:
exact ⟨fun J hJ hJfin ↦ (hI J hJ hJfin).1,
    fun e heI ↦ singleton_subset_iff.1 (hI _ (by simpa) (toFinite _)).2⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X : Set α
h : M.IsBasis I X
⊢ (M ↾ X).IsBase I

Tactic:
(isBase_restrict_iff h.subset_ground).mpr h

Premises used: Iff.mpr, Matroid.IsBasis.subset_ground, Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
rwa : (M ↾ Y ↾ X).IsBase I
rwa₁ : (M ↾ X).IsBase I
rwa₂ rwa₃ rwa₄ rwa₅ : M.IsBasis I X
⊢ (M ↾ Y).IsBasis I X

Tactic:
rwa [← isBase_restrict_iff, M.restrict_restrict_eq hXY, isBase_restrict_iff]

Premises used: Matroid.restrict_restrict_eq, Matroid.isBase_restrict_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
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
⊢ (M ↾ R).IsBasis' I X ↔ M.IsBasis' I (X ∩ R) ∧ I ⊆ R

Tactic:
simp_rw [IsBasis', maximal_iff, restrict_indep_iff, subset_inter_iff, and_imp]

Premises used: and_imp, Set.subset_inter_iff, Matroid.IsBasis', Matroid.restrict_indep_iff, maximal_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
rw : X ⊆ R → (M.IsBasis' I (X ∩ R) ∧ I ⊆ R ↔ M.IsBasis' I X)
⊢ (M ↾ R).IsBasis I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ R

Tactic:
rw [isBasis_iff_isBasis'_subset_ground, isBasis'_restrict_iff, restrict_ground_eq,
    and_congr_left_iff, ← isBasis'_iff_isBasis_inter_ground]

Premises used: Matroid.isBasis_iff_isBasis'_subset_ground, Matroid.isBasis'_restrict_iff, Matroid.restrict_ground_eq, Matroid.isBasis'_iff_isBasis_inter_ground, and_congr_left_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
rw : M.IsBasis' I X → I ⊆ R
⊢ M.IsBasis' I (X ∩ R) ∧ I ⊆ R ↔ M.IsBasis' I X

Tactic:
rw [inter_eq_self_of_subset_left hXR, and_iff_left_iff_imp]

Premises used: and_iff_left_iff_imp, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
⊢ M.IsBasis' I X → I ⊆ R

Tactic:
fun h ↦ h.subset.trans hXR

Premises used: HasSubset.Subset.trans, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
⊢ M.IsBasis' I X → I ⊆ R

Tactic:
exact fun h ↦ h.subset.trans hXR
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
hR : R ⊆ M.E
rw : X ⊆ R → (M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X)
⊢ (M ↾ R).IsBasis I X ↔ M.IsBasis I X ∧ X ⊆ R

Tactic:
rw [isBasis_restrict_iff', and_congr_left_iff]

Premises used: Matroid.isBasis_restrict_iff', and_congr_left_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
hR : R ⊆ M.E
hXR : X ⊆ R
rw : M.IsBasis' I X ↔ M.IsBasis I X
rw₁ rw₂ : M.IsBasis I X ↔ M.IsBasis I X
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X

Tactic:
rw [← isBasis'_iff_isBasis_inter_ground, isBasis'_iff_isBasis]

Premises used: Matroid.isBasis'_iff_isBasis_inter_ground, Matroid.isBasis'_iff_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
I X : Set α
rw : M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ univ
rw₁ : M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ univ
rw₂ rw₃ : M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (X ∩ M.E)
⊢ M.IsBasis' I X ↔ (M ↾ univ).IsBasis I X

Tactic:
rw [isBasis_restrict_iff', isBasis'_iff_isBasis_inter_ground, and_iff_left (subset_univ _)]

Premises used: Set.subset_univ, and_iff_left, Matroid.isBasis'_iff_isBasis_inter_ground, Matroid.isBasis_restrict_iff'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M M' : Matroid α
X : Set α
⊢ M ↾ X = M' ↾ X ↔ ∀ I ⊆ X, M.Indep I ↔ M'.Indep I

Tactic:
⟨fun h I hIX ↦ ?_, fun h ↦ ext_indep rfl fun I (hI : I ⊆ X) ↦ ?_⟩

Premises used: Iff.intro, Matroid.ext_indep, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M M' : Matroid α
X : Set α
refine_1 : ∀ (h : M ↾ X = M' ↾ X) (I : Set α) (hIX : I ⊆ X), M.Indep I ↔ M'.Indep I
refine_2 : ∀ (h : ∀ I ⊆ X, M.Indep I ↔ M'.Indep I) (I : Set α) (hI : I ⊆ X), (M ↾ X).Indep I ↔ (M' ↾ X).Indep I
⊢ M ↾ X = M' ↾ X ↔ ∀ I ⊆ X, M.Indep I ↔ M'.Indep I

Tactic:
refine ⟨fun h I hIX ↦ ?_, fun h ↦ ext_indep rfl fun I (hI : I ⊆ X) ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M M' : Matroid α
X : Set α
h : M ↾ X = M' ↾ X
I : Set α
hIX : I ⊆ X
refine_1 : M.Indep I ∧ I ⊆ X ↔ M'.Indep I
refine_1₁ : M.Indep I ∧ I ⊆ X ↔ M'.Indep I ∧ I ⊆ X
refine_1₂ : (M ↾ X).Indep I ↔ M'.Indep I ∧ I ⊆ X
refine_1₃ : (M' ↾ X).Indep I ↔ M'.Indep I ∧ I ⊆ X
refine_1₄ refine_1₅ : M'.Indep I ∧ I ⊆ X ↔ M'.Indep I ∧ I ⊆ X
⊢ M.Indep I ↔ M'.Indep I

Tactic:
rw [← and_iff_left (a := (M.Indep I)) hIX, ← and_iff_left (a := (M'.Indep I)) hIX,
      ← restrict_indep_iff, h, restrict_indep_iff]

Premises used: and_iff_left, Matroid.restrict_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M M' : Matroid α
X : Set α
h : ∀ I ⊆ X, M.Indep I ↔ M'.Indep I
I : Set α
hI : I ⊆ X
refine_2 : M.Indep I ∧ I ⊆ X ↔ (M' ↾ X).Indep I
refine_2₁ : M.Indep I ↔ (M' ↾ X).Indep I
refine_2₂ : M.Indep I ↔ M'.Indep I ∧ I ⊆ X
refine_2₃ : M.Indep I ↔ M'.Indep I
refine_2₄ refine_2₅ : M'.Indep I ↔ M'.Indep I
⊢ (M ↾ X).Indep I ↔ (M' ↾ X).Indep I

Tactic:
rw [restrict_indep_iff, and_iff_left hI, restrict_indep_iff, and_iff_left hI, h _ hI]

Premises used: and_iff_left, Matroid.restrict_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R = M
rw : R = (M ↾ R).E
⊢ R = M.E

Tactic:
rw [← h]
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R = M
⊢ R = (M ↾ R).E

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
h : R = M.E
⊢ M ↾ R = M

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M₁ M₂ : Matroidᵣ α
⊢ M₁.toMatroid = M₂.toMatroid ↔ M₁ = M₂

Tactic:
Matroidᵣ.ext_iff.symm

Premises used: Matroid.Matroidᵣ.ext_iff, Iff.symm
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α_1 : Type u_1
M : Matroid α_1
R_1 I X Y : Set α_1
N : Matroid α_1
α : Type u_2
M₁ M₂ M₃ : Matroidᵣ α
R : Set α
hR : R ⊆ M₂.toMatroid.E
h₁ : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR' : R' ⊆ M₃.toMatroid.E
h₂ : M₂.toMatroid = M₃.toMatroid ↾ R'
⊢ R ⊆ (M₃.toMatroid ↾ R').E

Tactic:
rw [h₂] at h₁ hR
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α_1 : Type u_1
M : Matroid α_1
R_1 I X Y : Set α_1
N : Matroid α_1
α : Type u_2
M₁ M₂ M₃ : Matroidᵣ α
R : Set α
hR : R ⊆ M₂.toMatroid.E
h₁ : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR' : R' ⊆ M₃.toMatroid.E
h₂ : M₂.toMatroid = M₃.toMatroid ↾ R'
hR₁ : R ⊆ (M₃.toMatroid ↾ R').E
⊢ M₁.toMatroid = M₃.toMatroid ↾ R' ↾ R

Tactic:
rw [h₂] at h₁ hR
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α_1 : Type u_1
M : Matroid α_1
R_1 I X Y : Set α_1
N : Matroid α_1
α : Type u_2
M₁ M₂ M₃ : Matroidᵣ α
R : Set α
hR : R ⊆ M₂.toMatroid.E
h₁ : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR' : R' ⊆ M₃.toMatroid.E
h₂ : M₂.toMatroid = M₃.toMatroid ↾ R'
hR₁ : R ⊆ (M₃.toMatroid ↾ R').E
h₃ : M₁.toMatroid = M₃.toMatroid ↾ R' ↾ R
⊢ R' ⊆ M₃.toMatroid.E

Tactic:
rw [h₂] at h₁ hR
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α_1 : Type u_1
M : Matroid α_1
R_1 I X Y : Set α_1
N : Matroid α_1
α : Type u_2
M₁ M₂ M₃ : Matroidᵣ α
R : Set α
hR : R ⊆ M₂.toMatroid.E
h₁ : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR' : R' ⊆ M₃.toMatroid.E
h₂ : M₂.toMatroid = M₃.toMatroid ↾ R'
hR₁ : R ⊆ (M₃.toMatroid ↾ R').E
h₃ : M₁.toMatroid = M₃.toMatroid ↾ R' ↾ R
hR'₁ : R' ⊆ M₃.toMatroid.E
⊢ M₂.toMatroid = M₃.toMatroid ↾ R'

Tactic:
rw [h₂] at h₁ hR
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α_1 : Type u_1
M : Matroid α_1
R_1 I X Y : Set α_1
N : Matroid α_1
α : Type u_2
M₁ M₂ M₃ : Matroidᵣ α
R R' : Set α
hR : R ⊆ (M₃.toMatroid ↾ R').E
h₁ : M₁.toMatroid = M₃.toMatroid ↾ R' ↾ R
hR' : R' ⊆ M₃.toMatroid.E
h₂ : M₂.toMatroid = M₃.toMatroid ↾ R'
rw : M₃.toMatroid ↾ R ≤r M₃.toMatroid
⊢ M₁.toMatroid ≤r M₃.toMatroid

Tactic:
rw [h₁, restrict_restrict_eq _ (show R ⊆ R' from hR)]

Premises used: Matroid.restrict_restrict_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α_1 : Type u_1
M : Matroid α_1
R_1 I X Y : Set α_1
N : Matroid α_1
α : Type u_2
M₁ M₂ M₃ : Matroidᵣ α
R R' : Set α
hR : R ⊆ (M₃.toMatroid ↾ R').E
h₁ : M₁.toMatroid = M₃.toMatroid ↾ R' ↾ R
hR' : R' ⊆ M₃.toMatroid.E
h₂ : M₂.toMatroid = M₃.toMatroid ↾ R'
⊢ M₃.toMatroid ↾ R ≤r M₃.toMatroid

Tactic:
⟨R, hR.trans hR', rfl⟩

Premises used: HasSubset.Subset.trans, Matroid.IsRestriction, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α_1 : Type u_1
M : Matroid α_1
R_1 I X Y : Set α_1
N : Matroid α_1
α : Type u_2
M₁ M₂ M₃ : Matroidᵣ α
R R' : Set α
hR : R ⊆ (M₃.toMatroid ↾ R').E
h₁ : M₁.toMatroid = M₃.toMatroid ↾ R' ↾ R
hR' : R' ⊆ M₃.toMatroid.E
h₂ : M₂.toMatroid = M₃.toMatroid ↾ R'
⊢ M₃.toMatroid ↾ R ≤r M₃.toMatroid

Tactic:
exact ⟨R, hR.trans hR', rfl⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α_1 : Type u_1
M : Matroid α_1
R_1 I X Y : Set α_1
N : Matroid α_1
α : Type u_2
M₁ M₂ : Matroidᵣ α
R : Set α
hR : R ⊆ M₂.toMatroid.E
h : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR' : R' ⊆ M₁.toMatroid.E
h' : M₂.toMatroid = M₁.toMatroid ↾ R'
⊢ R ⊆ R'

Tactic:
rw [h', restrict_ground_eq] at hR

Premises used: Matroid.restrict_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α_1 : Type u_1
M : Matroid α_1
R_1 I X Y : Set α_1
N : Matroid α_1
α : Type u_2
M₁ M₂ : Matroidᵣ α
R : Set α
hR : R ⊆ M₂.toMatroid.E
h : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR' : R' ⊆ M₁.toMatroid.E
h' : M₂.toMatroid = M₁.toMatroid ↾ R'
hR₁ : R ⊆ R'
⊢ R' ⊆ M₁.toMatroid.E

Tactic:
rw [h', restrict_ground_eq] at hR

Premises used: Matroid.restrict_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α_1 : Type u_1
M : Matroid α_1
R_1 I X Y : Set α_1
N : Matroid α_1
α : Type u_2
M₁ M₂ : Matroidᵣ α
R : Set α
hR : R ⊆ M₂.toMatroid.E
h : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR' : R' ⊆ M₁.toMatroid.E
h' : M₂.toMatroid = M₁.toMatroid ↾ R'
hR₁ : R ⊆ R'
hR'₁ : R' ⊆ M₁.toMatroid.E
⊢ M₂.toMatroid = M₁.toMatroid ↾ R'

Tactic:
rw [h', restrict_ground_eq] at hR

Premises used: Matroid.restrict_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α_1 : Type u_1
M : Matroid α_1
R_1 I X Y : Set α_1
N : Matroid α_1
α : Type u_2
M₁ M₂ : Matroidᵣ α
R : Set α
h : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR : R ⊆ R'
hR' : R' ⊆ M₁.toMatroid.E
h' : M₂.toMatroid = M₁.toMatroid ↾ R'
⊢ R' ⊆ R

Tactic:
rw [h, restrict_ground_eq] at hR'

Premises used: Matroid.restrict_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α_1 : Type u_1
M : Matroid α_1
R_1 I X Y : Set α_1
N : Matroid α_1
α : Type u_2
M₁ M₂ : Matroidᵣ α
R : Set α
h : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR : R ⊆ R'
hR' : R' ⊆ M₁.toMatroid.E
h' : M₂.toMatroid = M₁.toMatroid ↾ R'
hR'₁ : R' ⊆ R
⊢ M₂.toMatroid = M₁.toMatroid ↾ R'

Tactic:
rw [h, restrict_ground_eq] at hR'

Premises used: Matroid.restrict_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α_1 : Type u_1
M : Matroid α_1
R_1 I X Y : Set α_1
N : Matroid α_1
α : Type u_2
M₁ M₂ : Matroidᵣ α
R : Set α
h : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR : R ⊆ R'
hR' : R' ⊆ R
h' : M₂.toMatroid = M₁.toMatroid ↾ R'
rw : M₁.toMatroid = M₂.toMatroid
rw₁ : M₂.toMatroid ↾ R = M₂.toMatroid
rw₂ : M₁.toMatroid ↾ R' ↾ R = M₁.toMatroid ↾ R'
rw₃ : M₁.toMatroid ↾ R' ↾ R' = M₁.toMatroid ↾ R'
rw₄ rw₅ : M₁.toMatroid ↾ R' = M₁.toMatroid ↾ R'
⊢ M₁ = M₂

Tactic:
rw [← Matroidᵣ.coe_inj, h, h', hR.antisymm hR', restrict_idem]

Premises used: Matroid.Matroidᵣ.coe_inj, HasSubset.Subset.antisymm, Matroid.restrict_idem
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M M' : Matroidᵣ α
⊢ M ≤ M' ↔ M.toMatroid ≤r M'.toMatroid

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M M' : Matroidᵣ α
⊢ M < M' ↔ M.toMatroid <r M'.toMatroid

Tactic:
Iff.rfl

Premises used: Iff.rfl, Matroid.IsStrictRestriction
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M M' : Matroid α
⊢ { toMatroid := M : Matroidᵣ α } ≤ { toMatroid := M' } ↔ M ≤r M'

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M M' : Matroid α
⊢ { toMatroid := M : Matroidᵣ α } < { toMatroid := M' } ↔ M <r M'

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
⊢ M ≤r M

Tactic:
le_refl (Matroidᵣ.ofMatroid M)

Premises used: le_refl, Matroid.Matroidᵣ.ofMatroid
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M M' : Matroid α
h : M ≤r M'
h' : M' ≤r M
⊢ M = M'

Tactic:
simpa using (ofMatroid_le_iff.2 h).antisymm (ofMatroid_le_iff.2 h')

Premises used: Iff.mpr, LE.le.antisymm, Matroid.ofMatroid_le_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M₁ M₂ M₃ : Matroid α
h : M₁ ≤r M₂
h' : M₂ ≤r M₃
⊢ M₁ ≤r M₃

Tactic:
le_trans (α := Matroidᵣ α) h h'

Premises used: le_trans
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R ≤r M

Tactic:
⟨R, hR, rfl⟩

Premises used: Matroid.IsRestriction, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
h : N ≤r M
obtain : ∀ (R : Set α), M ↾ (M ↾ R).E = M ↾ R
⊢ M ↾ N.E = N

Tactic:
obtain ⟨R, -, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M : Matroid α
R : Set α
rw rw₁ : M ↾ R = M ↾ R
⊢ M ↾ (M ↾ R).E = M ↾ R

Tactic:
rw [restrict_ground_eq]

Premises used: Matroid.restrict_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Restrict
Goal:
α : Type u_1
M N : Matroid α
h : N ≤r M
obtain : ∀ (R : Set α) (hR : R ⊆ M.E), (M ↾ R).E ⊆ M.E
⊢ N.E ⊆ M.E

Tactic:
obtain ⟨R, hR, rfl⟩ := h

Premises used: rfl