awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
⊢ ∀ ⦃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 mpr : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
Tactic: tauto
-- 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)
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
mpr : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R → (I_1 ⊆ I ∧ 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 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
Tactic: tauto
-- 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)
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
mpr : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₁ mp₂ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → ((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 ⊆ R → 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 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)
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
mpr : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₁ mp₂ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₃ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ I
⊢ ∀ ⦃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 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ R
Tactic: tauto
-- 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)
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
mpr : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₁ mp₂ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₃ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ I
mp₄ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → 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 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ E
Tactic: tauto
-- 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)
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
mpr : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₁ mp₂ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₃ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ I
mp₄ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ R
mp₅ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ E
mp₆ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → 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 mpr₁ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
Tactic: tauto
-- 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)
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
mpr : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₁ mp₂ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₃ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ I
mp₄ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ R
mp₅ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ E
mp₆ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ R
mpr₁ mpr₂ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → (I_1 ⊆ I ∧ 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 mpr₃ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → I_1 ⊆ I
Tactic: tauto
-- 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)
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
mpr : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₁ mp₂ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₃ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ I
mp₄ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ R
mp₅ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ E
mp₆ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ R
mpr₁ mpr₂ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mpr₃ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → I_1 ⊆ I
⊢ ∀ ⦃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 mpr₄ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → I_1 ⊆ E
Tactic: tauto
-- 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)
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
mpr : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₁ mp₂ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mp₃ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ I
mp₄ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ R
mp₅ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ E
mp₆ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ I → I_1 ⊆ E → I_1 ⊆ R
mpr₁ mpr₂ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
mpr₃ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → I_1 ⊆ I
mpr₄ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → I_1 ⊆ E
⊢ ∀ ⦃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 mpr₅ : ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → I_1 ⊆ R → I_1 ⊆ E → I_1 ⊆ I → I_1 ⊆ R → I_1 ⊆ R
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I : Set α
h : I ⊆ E
R : Set α
⊢ uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R) R
have rw : uniqueBaseOn (I ∩ R ∩ E) R = uniqueBaseOn (I ∩ R) R
Tactic: rw [uniqueBaseOn_restrict', inter_right_comm, inter_eq_self_of_subset_left h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I : Set α
h : I ⊆ E
R : Set α
rw : uniqueBaseOn (I ∩ R ∩ E) R = uniqueBaseOn (I ∩ R) R
⊢ uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R) R
have rw₁ : uniqueBaseOn (I ∩ E ∩ R) R = uniqueBaseOn (I ∩ R) R
Tactic: rw [uniqueBaseOn_restrict', inter_right_comm, inter_eq_self_of_subset_left h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I : Set α
h : I ⊆ E
R : Set α
rw : uniqueBaseOn (I ∩ R ∩ E) R = uniqueBaseOn (I ∩ R) R
rw₁ : uniqueBaseOn (I ∩ E ∩ R) R = uniqueBaseOn (I ∩ R) R
⊢ uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R) R
have rw₂ : uniqueBaseOn (I ∩ R) R = uniqueBaseOn (I ∩ R) R
Tactic: rw [uniqueBaseOn_restrict', inter_right_comm, inter_eq_self_of_subset_left h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn I E).RankFinite
have rw : (uniqueBaseOn (I ∩ E) E).RankFinite
Tactic: rw [← uniqueBaseOn_inter_ground_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).RankFinite
have refine : (uniqueBaseOn (I ∩ E) E).IsBase (I ∩ E) ∧ (I ∩ E).Finite
Tactic: refine ⟨I ∩ E, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).IsBase (I ∩ E) ∧ (I ∩ E).Finite
have rw : (I ∩ E).Finite
Tactic: rw [uniqueBaseOn_isBase_iff inter_subset_right, and_iff_right rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
E B I X R J : Set α
⊢ (uniqueBaseOn I E).Finitary
have refine : ∀ (K : Set α) (hK : ∀ J ⊆ K, J.Finite → (uniqueBaseOn I E).Indep J), (uniqueBaseOn I E).Indep K
Tactic: refine ⟨fun K hK ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Constructions (goal)
Goal:
α : Type u_1
M : Matroid α
E B I X R J K : Set α
hK : ∀ J ⊆ K, J.Finite → (uniqueBaseOn I E).Indep J
⊢ (uniqueBaseOn I E).Indep K
have simp : ∀ (hK : ∀ J ⊆ K, J.Finite → J ⊆ I ∩ E), K ⊆ I ∩ E
Tactic: simp only [uniqueBaseOn_indep_iff'] at hK ⊢
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B
have hXE : X ⊆ M.E
Tactic: have hXE := hX_max.1.1
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B
have hB' : M.IsBase (M.E \ X)
Tactic: have hB' := (isBase_compl_iff_maximal_disjoint_isBase hXE).mpr hX_max
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
hB' : M.IsBase (M.E \ X)
hB'₁ :
  let B' := M.E \ X;
  M.IsBase B'
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B
have hX : let B' := M.E \ X;
B' = M.E \ X
Tactic: set B' := M.E \ X with hX
Cleared hypotheses: hB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B
have hI : ¬M.IsBase (M.E \ I)
Tactic: have hI := (not_iff_not.mpr (isBase_compl_iff_maximal_disjoint_isBase)).mpr hI_not_max
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B
have obtain : ∀ (B'' : Set α) (hB'' : M.IsBase B'') (hB''₁ : B' \ I ⊆ B'') (hB''₂ : B'' ⊆ B' \ I ∪ B),
  ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B
Tactic: obtain ⟨B'', hB'', hB''₁, hB''₂⟩ := (hB'.indep.diff I).exists_isBase_subset_union_isBase hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' \ I ∪ B
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B
have hB''₃ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
Tactic: rw [← compl_subset_compl, ← hIB.sdiff_eq_right, ← union_diff_distrib, diff_eq, compl_inter,
      compl_compl, union_subset_iff, compl_subset_compl] at hB''₂
Cleared hypotheses: hB''₂
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
⊢ False
have apply : M.IsBase (M.E \ (B''ᶜ ∩ M.E))
Tactic: apply hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I B_1 X_1 : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
⊢ M.IsBase (M.E \ (B''ᶜ ∩ M.E))
have h : M.E \ (B''ᶜ ∩ M.E) = B''
Tactic: convert! hB''
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
⊢ I ≠ B''ᶜ ∩ M.E
have rintro : ∀ (hIE : B''ᶜ ∩ M.E ⊆ M.E) (hIB : Disjoint (B''ᶜ ∩ M.E) B)
  (hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E))
  (hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))) (hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B'') (hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ),
  False
Tactic: { rintro rfl; apply hI; convert! hB''; simp [hB''.subset_ground] }
Cleared hypotheses: I, hIE, hIB, hI_not_max, hI, hB''₁, hB''₂
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
rintro rintro₁ :
  ∀ (hIE : B''ᶜ ∩ M.E ⊆ M.E) (hIB : Disjoint (B''ᶜ ∩ M.E) B)
    (hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E))
    (hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))) (hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B'') (hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ),
    False
⊢ I ≠ B''ᶜ ∩ M.E
have rintro₂ : ∀ (hIE : B''ᶜ ∩ M.E ⊆ M.E) (hIB : Disjoint (B''ᶜ ∩ M.E) B)
  (hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E))
  (hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))) (hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B'') (hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ),
  M.IsBase (M.E \ (B''ᶜ ∩ M.E))
Tactic: { rintro rfl; apply hI; convert! hB''; simp [hB''.subset_ground] }
Cleared hypotheses: I, hIE, hIB, hI_not_max, hI, hB''₁, hB''₂
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
rintro rintro₁ :
  ∀ (hIE : B''ᶜ ∩ M.E ⊆ M.E) (hIB : Disjoint (B''ᶜ ∩ M.E) B)
    (hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E))
    (hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))) (hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B'') (hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ),
    False
rintro₂ rintro₃ :
  ∀ (hIE : B''ᶜ ∩ M.E ⊆ M.E) (hIB : Disjoint (B''ᶜ ∩ M.E) B)
    (hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E))
    (hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))) (hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B'') (hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ),
    M.IsBase (M.E \ (B''ᶜ ∩ M.E))
⊢ I ≠ B''ᶜ ∩ M.E
have h : ∀ (hIE : B''ᶜ ∩ M.E ⊆ M.E) (hIB : Disjoint (B''ᶜ ∩ M.E) B)
  (hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E))
  (hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))) (hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B'') (hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ),
  M.E \ (B''ᶜ ∩ M.E) = B''
Tactic: { rintro rfl; apply hI; convert! hB''; simp [hB''.subset_ground] }
Cleared hypotheses: I, hIE, hIB, hI_not_max, hI, hB''₁, hB''₂
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (hypothesis)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B
have hssu : I ⊂ B''ᶜ ∩ M.E
Tactic: have hssu := (subset_inter (hB''₂.2) hIE).ssubset_of_ne
      (by { rintro rfl; apply hI; convert! hB''; simp [hB''.subset_ground] })
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B
have obtain : ∀ (e : α) (heI : e ∉ I) (heB'' : e ∉ B'') (heE : e ∈ M.E),
  ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B
Tactic: obtain ⟨e, ⟨(heB'' : e ∉ _), heE⟩, heI⟩ := exists_of_ssubset hssu
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert x I) B
have h : e ∈ X \ I ∧ insert e I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert e I) B
Tactic: use e
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Dual (goal)
Goal:
α : Type u_1
M_1 : Matroid α
I_1 B_1 X_1 : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun (I : Set α) ↦ I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ e ∈ X \ I ∧ insert e I ⊆ M.E ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert e I) B
have h : e ∈ X ∧ ∃ (B : Set α), M.IsBase B ∧ Disjoint (insert e I) B
Tactic: simp_rw [mem_diff, insert_subset_iff, and_iff_left heI, and_iff_right heE, and_iff_right hIE]