awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ (((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 → 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
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
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
mpr₄ : I ⊆ R → (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) → M.Indep I → I ⊆ X → 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 → 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
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
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
mpr₄ : I ⊆ R → (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) → M.Indep I → I ⊆ X → I ⊆ R → I ⊆ R
mpr₅ : I ⊆ R → (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) → M.Indep I → I ⊆ X → 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 mpr₆ : I ⊆ R →
  (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ≤ y → I = y) →
    M.Indep I → I ⊆ X → I ⊆ R → ∀ ⦃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 α
⊢ (M ↾ R).IsBasis I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ R
have rw : X ⊆ R → (M.IsBasis' I (X ∩ R) ∧ I ⊆ R ↔ M.IsBasis' I X)
Tactic: rw [isBasis_iff_isBasis'_subset_ground, isBasis'_restrict_iff, restrict_ground_eq,
    and_congr_left_iff, ← isBasis'_iff_isBasis_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
⊢ M.IsBasis' I (X ∩ R) ∧ I ⊆ R ↔ M.IsBasis' I X
have rw : M.IsBasis' I X → I ⊆ R
Tactic: rw [inter_eq_self_of_subset_left hXR, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsBasis I X ↔ M.IsBasis I X ∧ X ⊆ R
have rw : X ⊆ R → (M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X)
Tactic: rw [isBasis_restrict_iff', and_congr_left_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R I X : Set α
hR : R ⊆ M.E
hXR : X ⊆ R
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X
have rw : M.IsBasis' I X ↔ M.IsBasis I X
Tactic: rw [← isBasis'_iff_isBasis_inter_ground, isBasis'_iff_isBasis]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X
have rw₁ : M.IsBasis I X ↔ M.IsBasis I X
Tactic: rw [← isBasis'_iff_isBasis_inter_ground, isBasis'_iff_isBasis]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis' I X ↔ (M ↾ univ).IsBasis I X
have rw : M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ univ
Tactic: rw [isBasis_restrict_iff', isBasis'_iff_isBasis_inter_ground, and_iff_left (subset_univ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
rw : M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ univ
⊢ M.IsBasis' I X ↔ (M ↾ univ).IsBasis I X
have rw₁ : M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ univ
Tactic: rw [isBasis_restrict_iff', isBasis'_iff_isBasis_inter_ground, and_iff_left (subset_univ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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
⊢ M.IsBasis' I X ↔ (M ↾ univ).IsBasis I X
have rw₂ : M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (X ∩ M.E)
Tactic: rw [isBasis_restrict_iff', isBasis'_iff_isBasis_inter_ground, and_iff_left (subset_univ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M M' : Matroid α
X : Set α
⊢ M ↾ X = M' ↾ X ↔ ∀ I ⊆ X, M.Indep I ↔ M'.Indep I
have refine_1 : ∀ (h : M ↾ X = M' ↾ X) (I : Set α) (hIX : I ⊆ X), M.Indep I ↔ M'.Indep I
Tactic: refine ⟨fun h I hIX ↦ ?_, fun h ↦ ext_indep rfl fun I (hI : I ⊆ X) ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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
⊢ M ↾ X = M' ↾ X ↔ ∀ I ⊆ X, M.Indep I ↔ M'.Indep I
have refine_2 : ∀ (h : ∀ I ⊆ X, M.Indep I ↔ M'.Indep I) (I : Set α) (hI : I ⊆ X), (M ↾ X).Indep I ↔ (M' ↾ X).Indep I
Tactic: refine ⟨fun h I hIX ↦ ?_, fun h ↦ ext_indep rfl fun I (hI : I ⊆ X) ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M M' : Matroid α
X : Set α
h : M ↾ X = M' ↾ X
I : Set α
hIX : I ⊆ X
⊢ M.Indep I ↔ M'.Indep I
have refine_1 : M.Indep I ∧ I ⊆ X ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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
⊢ M.Indep I ↔ M'.Indep I
have refine_1₁ : M.Indep I ∧ I ⊆ X ↔ M'.Indep I ∧ I ⊆ X
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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
⊢ M.Indep I ↔ M'.Indep I
have refine_1₂ : (M ↾ X).Indep I ↔ M'.Indep I ∧ I ⊆ X
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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
⊢ M.Indep I ↔ M'.Indep I
have refine_1₃ : (M' ↾ X).Indep I ↔ M'.Indep I ∧ I ⊆ X
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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
⊢ M.Indep I ↔ M'.Indep I
have refine_1₄ : M'.Indep I ∧ I ⊆ X ↔ M'.Indep I ∧ I ⊆ X
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M M' : Matroid α
X : Set α
h : ∀ I ⊆ X, M.Indep I ↔ M'.Indep I
I : Set α
hI : I ⊆ X
⊢ (M ↾ X).Indep I ↔ (M' ↾ X).Indep I
have refine_2 : M.Indep I ∧ I ⊆ X ↔ (M' ↾ X).Indep I
Tactic: rw [restrict_indep_iff, and_iff_left hI, restrict_indep_iff, and_iff_left hI, h _ hI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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
⊢ (M ↾ X).Indep I ↔ (M' ↾ X).Indep I
have refine_2₁ : M.Indep I ↔ (M' ↾ X).Indep I
Tactic: rw [restrict_indep_iff, and_iff_left hI, restrict_indep_iff, and_iff_left hI, h _ hI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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
⊢ (M ↾ X).Indep I ↔ (M' ↾ X).Indep I
have refine_2₂ : M.Indep I ↔ M'.Indep I ∧ I ⊆ X
Tactic: rw [restrict_indep_iff, and_iff_left hI, restrict_indep_iff, and_iff_left hI, h _ hI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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
⊢ (M ↾ X).Indep I ↔ (M' ↾ X).Indep I
have refine_2₃ : M.Indep I ↔ M'.Indep I
Tactic: rw [restrict_indep_iff, and_iff_left hI, restrict_indep_iff, and_iff_left hI, h _ hI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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
⊢ (M ↾ X).Indep I ↔ (M' ↾ X).Indep I
have refine_2₄ : M'.Indep I ↔ M'.Indep I
Tactic: rw [restrict_indep_iff, and_iff_left hI, restrict_indep_iff, and_iff_left hI, h _ hI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R = M
⊢ R = M.E
have rw : R = (M ↾ R).E
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
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'
⊢ M₁.toMatroid ≤r M₃.toMatroid
have hR₁ : R ⊆ (M₃.toMatroid ↾ R').E
Tactic: rw [h₂] at h₁ hR
Cleared hypotheses: hR, h₁, hR', h₂
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
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 ≤r M₃.toMatroid
have h₃ : M₁.toMatroid = M₃.toMatroid ↾ R' ↾ R
Tactic: rw [h₂] at h₁ hR
Cleared hypotheses: hR, h₁, hR', h₂
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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 M₃.toMatroid
have rw : M₃.toMatroid ↾ R ≤r M₃.toMatroid
Tactic: rw [h₁, restrict_restrict_eq _ (show R ⊆ R' from hR)]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
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'
⊢ M₁ = M₂
have hR₁ : R ⊆ R'
Tactic: rw [h', restrict_ground_eq] at hR
Cleared hypotheses: hR, hR', h'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
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'
⊢ M₁ = M₂
have hR'₁ : R' ⊆ R
Tactic: rw [h, restrict_ground_eq] at hR'
Cleared hypotheses: hR', h'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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'
⊢ M₁ = M₂
have rw : M₁.toMatroid = M₂.toMatroid
Tactic: rw [← Matroidᵣ.coe_inj, h, h', hR.antisymm hR', restrict_idem]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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
⊢ M₁ = M₂
have rw₁ : M₂.toMatroid ↾ R = M₂.toMatroid
Tactic: rw [← Matroidᵣ.coe_inj, h, h', hR.antisymm hR', restrict_idem]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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
⊢ M₁ = M₂
have rw₂ : M₁.toMatroid ↾ R' ↾ R = M₁.toMatroid ↾ R'
Tactic: rw [← Matroidᵣ.coe_inj, h, h', hR.antisymm hR', restrict_idem]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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'
⊢ M₁ = M₂
have rw₃ : M₁.toMatroid ↾ R' ↾ R' = M₁.toMatroid ↾ R'
Tactic: rw [← Matroidᵣ.coe_inj, h, h', hR.antisymm hR', restrict_idem]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
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'
⊢ M₁ = M₂
have rw₄ : M₁.toMatroid ↾ R' = M₁.toMatroid ↾ R'
Tactic: rw [← Matroidᵣ.coe_inj, h, h', hR.antisymm hR', restrict_idem]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M N : Matroid α
h : N ≤r M
⊢ M ↾ N.E = N
have obtain : ∀ (R : Set α), M ↾ (M ↾ R).E = M ↾ R
Tactic: obtain ⟨R, -, rfl⟩ := h
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
⊢ M ↾ (M ↾ R).E = M ↾ R
have rw : M ↾ R = M ↾ R
Tactic: rw [restrict_ground_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M N : Matroid α
h : N ≤r M
⊢ N.E ⊆ M.E
have obtain : ∀ (R : Set α) (hR : R ⊆ M.E), (M ↾ R).E ⊆ M.E
Tactic: obtain ⟨R, hR, rfl⟩ := h
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
R R' : Set α
M : Matroid α
h : R ⊆ R'
⊢ M ↾ R ≤r M ↾ R'
have rw : M ↾ R' ↾ R ≤r M ↾ R'
Tactic: rw [← restrict_restrict_eq M h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M N : Matroid α
⊢ N ≤r M ↔ ∃ R ⊆ M.E, N = M ↾ R
have mpr : (∃ R ⊆ M.E, N = M ↾ R) → N ≤r M
Tactic: use IsRestriction.exists_eq_restrict
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
N : Matroid α
h : N <r N
⊢ False
have h₁ : { toMatroid := N : Matroidᵣ α } < { toMatroid := N }
Tactic: rw [← ofMatroid_lt_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M N : Matroid α
h : N <r M
⊢ N.E ⊂ M.E
have obtain : ∀ (R : Set α) (h : M ↾ R <r M), (M ↾ R).E ⊂ M.E
Tactic: obtain ⟨R, -, rfl⟩ := h.1
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
⊢ (M ↾ R).E ⊂ M.E
have refine : ∀ (h' : (M ↾ R).E = M.E), M = M ↾ R ↾ R
Tactic: refine h.isRestriction.subset.ssubset_of_ne (fun h' ↦ h.2 ⟨R, Subset.rfl, ?_⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
h' : (M ↾ R).E = M.E
⊢ M = M ↾ R ↾ R
have rw : M = M ↾ M.E ↾ M.E
Tactic: rw [show R = M.E from h', restrict_idem, restrict_ground_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
h' : (M ↾ R).E = M.E
rw : M = M ↾ M.E ↾ M.E
⊢ M = M ↾ R ↾ R
have rw₁ : M = M ↾ M.E
Tactic: rw [show R = M.E from h', restrict_idem, restrict_ground_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
h' : (M ↾ R).E = M.E
rw : M = M ↾ M.E ↾ M.E
rw₁ : M = M ↾ M.E
⊢ M = M ↾ R ↾ R
have rw₂ : M = M
Tactic: rw [show R = M.E from h', restrict_idem, restrict_ground_eq_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M N : Matroid α
h : N <r M
⊢ N = M ↾ N.E
have rw : N = N
Tactic: rw [h.eq_restrict]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ M.E
⊢ M ↾ R <r M
have refine : ∀ (h : M ↾ R = M), False
Tactic: refine (M.restrict_isRestriction R hR.subset).isStrictRestriction_of_ne (fun h ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (hypothesis)
Goal:
α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ M.E
h : M ↾ R = M
⊢ False
have hR₁ : R ⊂ R
Tactic: rw [← h, restrict_ground_eq] at hR
Cleared hypotheses: hR, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N.E ≠ M.E
⊢ N <r M
have rw : M ↾ N.E <r M
Tactic: rw [← h.eq_restrict]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
N M : Matroid α
inst : M.Finite
h : N ≤r M
⊢ N.Finite
have obtain : ∀ (R : Set α) (hR : R ⊆ M.E), (M ↾ R).Finite
Tactic: obtain ⟨R, hR, rfl⟩ := h
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
N M : Matroid α
inst : M.RankFinite
h : N ≤r M
⊢ N.RankFinite
have obtain : ∀ (R : Set α), (M ↾ R).RankFinite
Tactic: obtain ⟨R, -, rfl⟩ := h
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
N M : Matroid α
inst : M.Finitary
h : N ≤r M
⊢ N.Finitary
have obtain : ∀ (R : Set α), (M ↾ R).Finitary
Tactic: obtain ⟨R, -, rfl⟩ := h
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Restrict (goal)
Goal:
α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hI : N.Indep I
hNM : N ≤r M
⊢ M.Indep I
have obtain : ∀ (R : Set α) (hI : (M ↾ R).Indep I), M.Indep I
Tactic: obtain ⟨R, -, rfl⟩ := hNM
Cleared hypotheses: N, hI, hNM