awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₂.IsLoop e
⊢ ¬M₂.Indep (I \ M₂.coloops)

Tactic:
exact hel.not_indep_of_mem ⟨heI, hel.not_isColoop⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
⊢ M.loops = ∅

Tactic:
‹Loopless M›.loops_eq_empty

Premises used: Matroid.Loopless.loops_eq_empty
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
inst : M.Loopless
he : e ∈ M.E
rw : e ∉ ∅
⊢ M.IsNonloop e

Tactic:
rw [← not_isLoop_iff, isLoop_iff, loops_eq_empty]

Premises used: Matroid.loops_eq_empty, Matroid.isLoop_iff, Matroid.not_isLoop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
inst : M.Loopless
he : e ∈ M.E
⊢ e ∉ ∅

Tactic:
notMem_empty _

Premises used: Set.notMem_empty
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
inst : M.Loopless
he : e ∈ M.E
⊢ e ∉ ∅

Tactic:
exact notMem_empty _

Premises used: Set.notMem_empty
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I : Set α
inst : M.Loopless
hI : I.Subsingleton
hIE : I ⊆ M.E
inl : ∀ (hI : Set.Subsingleton.{u_1} (α := α) ∅) (hIE : ∅ ⊆ M.E), M.Indep ∅
inr : ∀ (x : α) (hI : Set.Subsingleton (α := α) {x}) (hIE : {x} ⊆ M.E), M.Indep {x}
⊢ M.Indep I

Tactic:
obtain rfl | ⟨x, rfl⟩ := hI.eq_empty_or_singleton

Premises used: Set.Subsingleton.eq_empty_or_singleton, rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
hI : Set.Subsingleton.{u_1} (α := α) ∅
hIE : ∅ ⊆ M.E
⊢ M.Indep ∅

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
x : α
hI : Set.Subsingleton (α := α) {x}
hIE : {x} ⊆ M.E
⊢ M.Indep {x}

Tactic:
simpa using M.isNonloop_of_loopless

Premises used: Matroid.isNonloop_of_loopless
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
e : α
⊢ ¬M.IsLoop e

Tactic:
fun h ↦ (isNonloop_of_loopless (e := e)).not_isLoop h

Premises used: Matroid.IsNonloop.not_isLoop, Matroid.isNonloop_of_loopless, Not
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.Loopless ↔ ∀ e ∈ M.E, M.IsNonloop e

Tactic:
⟨fun _ _ he ↦ isNonloop_of_loopless he,
    fun h ↦ ⟨subset_empty_iff.1 (fun e (he : M.IsLoop e) ↦ (h e he.mem_ground).not_isLoop he)⟩⟩

Premises used: Matroid.IsNonloop.not_isLoop, Matroid.isNonloop_of_loopless, Matroid.Loopless.mk, Iff.intro, Iff.mp, Set.subset_empty_iff, Matroid.IsLoop.mem_ground
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.Loopless ↔ ∀ e ∈ M.E, ¬M.IsLoop e

Tactic:
⟨fun _ e _ ↦ M.not_isLoop e,
    fun h ↦ loopless_iff_forall_isNonloop.2 fun e he ↦ (not_isLoop_iff he).1 (h e he)⟩

Premises used: Iff.mpr, Matroid.loopless_iff_forall_isNonloop, Matroid.not_isLoop, Iff.intro, Iff.mp, Matroid.not_isLoop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
this : (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton
rw : (∀ e ∈ M.E, ¬M.IsLoop e) ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial
⊢ M.Loopless ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial

Tactic:
rw [loopless_iff_forall_not_isLoop]

Premises used: Matroid.loopless_iff_forall_not_isLoop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
this contrapose! : (∃ e ∈ M.E, M.IsLoop e) ↔ ∃ (C : Set α), M.IsCircuit C ∧ C.Subsingleton
⊢ (∀ e ∈ M.E, ¬M.IsLoop e) ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial

Tactic:
contrapose!
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
this : (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton
⊢ (∃ e ∈ M.E, M.IsLoop e) ↔ ∃ (C : Set α), M.IsCircuit C ∧ C.Subsingleton

Tactic:
this
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
this : (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton
⊢ (∃ e ∈ M.E, M.IsLoop e) ↔ ∃ (C : Set α), M.IsCircuit C ∧ C.Subsingleton

Tactic:
exact this
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
suffices : (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton
⊢ M.Loopless ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial

Tactic:
suffices (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ x, M.IsCircuit x ∧ x.Subsingleton by
    rw [loopless_iff_forall_not_isLoop]
    contrapose!
    exact this
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
h : ∃ x ∈ M.E, M.IsLoop x
e : α
left : e ∈ M.E
he : M.IsLoop e
⊢ Set.Subsingleton (α := α) {e}

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
refine :
  (∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton) →
    ∀ (C : Set α) (hC : M.IsCircuit C) (hCs : C.Subsingleton), ∃ x ∈ M.E, M.IsLoop x
⊢ (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton

Tactic:
refine ⟨fun ⟨e, _, he⟩ ↦ ⟨{e}, he.isCircuit, by simp⟩, fun ⟨C, hC, hCs⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
h : ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton
C : Set α
hC : M.IsCircuit C
hCs : C.Subsingleton
inl : ∀ (hC : M.IsCircuit ∅) (hCs : Set.Subsingleton.{u_1} (α := α) ∅), ∃ x ∈ M.E, M.IsLoop x
inr : ∀ (e : α) (hC : M.IsCircuit {e}) (hCs : Set.Subsingleton (α := α) {e}), ∃ x ∈ M.E, M.IsLoop x
⊢ ∃ x ∈ M.E, M.IsLoop x

Tactic:
obtain (rfl | ⟨e, rfl⟩) := hCs.eq_empty_or_singleton

Premises used: Set.Subsingleton.eq_empty_or_singleton, rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
h : ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton
hC : M.IsCircuit ∅
hCs : Set.Subsingleton.{u_1} (α := α) ∅
⊢ ∃ x ∈ M.E, M.IsLoop x

Tactic:
simpa using hC.nonempty

Premises used: Matroid.IsCircuit.nonempty
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
h : ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton
e : α
hC : M.IsCircuit {e}
hCs : Set.Subsingleton (α := α) {e}
⊢ ∃ x ∈ M.E, M.IsLoop x

Tactic:
⟨e, (singleton_isCircuit.1 hC).mem_ground, singleton_isCircuit.1 hC⟩

Premises used: Matroid.singleton_isCircuit, And.intro, Exists.intro, Iff.mp, Matroid.IsLoop.mem_ground
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
h : ∃ (x : Set α), M.IsCircuit x ∧ x.Subsingleton
e : α
hC : M.IsCircuit {e}
hCs : Set.Subsingleton (α := α) {e}
⊢ ∃ x ∈ M.E, M.IsLoop x

Tactic:
exact ⟨e, (singleton_isCircuit.1 hC).mem_ground, singleton_isCircuit.1 hC⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
⊢ M.E = {e : α | M.IsNonloop e}

Tactic:
Set.ext fun _ ↦ ⟨fun he ↦ isNonloop_of_loopless he, IsNonloop.mem_ground⟩

Premises used: Matroid.IsNonloop.mem_ground, Set.ext, Matroid.isNonloop_of_loopless, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M N : Matroid α
inst : M.Loopless
hR : N ≤r M
obtain : ∀ (R : Set α) (hR : R ⊆ M.E), (M ↾ R).Loopless
⊢ N.Loopless

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

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
R : Set α
hR : R ⊆ M.E
rw : (M ↾ R).loops = ∅
rw₁ : M.loops ∩ R = ∅
rw₂ : ∅ ∩ R = ∅
rw₃ rw₄ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
⊢ (M ↾ R).Loopless

Tactic:
rw [loopless_iff, restrict_loops_eq hR, M.loops_eq_empty, empty_inter]

Premises used: Matroid.loops_eq_empty, Matroid.restrict_loops_eq, Set.empty_inter, Matroid.loopless_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
β : Type u_2
M_1 N : Matroid α
e f : α
F X C I : Set α
M : Matroid α
inst : M.Nonempty
inst_1 : M.Loopless
⊢ M.RankPos

Tactic:
M.ground_nonempty.elim fun _ he ↦ (isNonloop_of_loopless he).rankPos

Premises used: Matroid.ground_nonempty, Matroid.isNonloop_of_loopless, Matroid.IsNonloop.rankPos, Exists.elim
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
E : Set α
⊢ (loopyOn E).Loopless ↔ E = ∅

Tactic:
simp [loopless_iff_forall_not_isLoop, eq_empty_iff_forall_notMem]

Premises used: Matroid.loopless_iff_forall_not_isLoop, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.removeLoops = M ↾ {e : α | M.IsNonloop e}

Tactic:
rfl

Premises used: Matroid.removeLoops, rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.removeLoops.E = {e : α | M.IsNonloop e}

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
β : Type u_2
M_1 N : Matroid α
e f : α
F X C I : Set α
M : Matroid α
⊢ M.removeLoops.Loopless

Tactic:
simp [loopless_iff_forall_isNonloop, removeLoops]

Premises used: Matroid.loopless_iff_forall_isNonloop, Matroid.removeLoops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
inst : M.Loopless
rw : M ↾ {e : α | M.IsNonloop e} = M
rw₁ : M ↾ M.E = M
rw₂ rw₃ : M = M
⊢ M.removeLoops = M

Tactic:
rw [removeLoops, ← Loopless.ground_eq, restrict_ground_eq_self]

Premises used: Matroid.removeLoops, Matroid.restrict_ground_eq_self, Matroid.Loopless.ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.removeLoops = M ↔ M.Loopless

Tactic:
⟨fun h ↦ ?_, fun h ↦ M.removeLoops_eq_self⟩

Premises used: Matroid.removeLoops_eq_self, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
refine : ∀ (h : M.removeLoops = M), M.Loopless
⊢ M.removeLoops = M ↔ M.Loopless

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ M.removeLoops_eq_self⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
h : M.removeLoops = M
rw : M.removeLoops.Loopless
⊢ M.Loopless

Tactic:
rw [← h]
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
h : M.removeLoops = M
⊢ M.removeLoops.Loopless

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.removeLoops ≤r M

Tactic:
restrict_isRestriction _ _ (fun _ h ↦ IsNonloop.mem_ground h)

Premises used: Matroid.IsNonloop.mem_ground, Matroid.restrict_isRestriction, Matroid.removeLoops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
rw :
  (M ↾ {e : α | M.IsNonloop e} ↾ M.E).E = M.E ∧
    ∀ ⦃I : Set α⦄, I ⊆ (M ↾ {e : α | M.IsNonloop e} ↾ M.E).E → ((M ↾ {e : α | M.IsNonloop e} ↾ M.E).Indep I ↔ M.Indep I)
⊢ M.removeLoops ↾ M.E = M

Tactic:
rw [removeLoops, ext_iff_indep]

Premises used: Matroid.removeLoops, Matroid.ext_iff_indep
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
simp : ∀ ⦃I : Set α⦄, I ⊆ M.E → ((M.Indep I ∧ I ⊆ {e : α | M.IsNonloop e}) ∧ I ⊆ M.E ↔ M.Indep I)
⊢ (M ↾ {e : α | M.IsNonloop e} ↾ M.E).E = M.E ∧
    ∀ ⦃I : Set α⦄, I ⊆ (M ↾ {e : α | M.IsNonloop e} ↾ M.E).E → ((M ↾ {e : α | M.IsNonloop e} ↾ M.E).Indep I ↔ M.Indep I)

Tactic:
simp only [restrict_ground_eq, restrict_indep_iff, true_and]

Premises used: Matroid.restrict_ground_eq, Matroid.restrict_indep_iff, true_and
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ ∀ ⦃I : Set α⦄, I ⊆ M.E → ((M.Indep I ∧ I ⊆ {e : α | M.IsNonloop e}) ∧ I ⊆ M.E ↔ M.Indep I)

Tactic:
fun I hIE ↦ ⟨ fun hI ↦ hI.1.1, fun hI ↦ ⟨⟨hI,fun e heI ↦ hI.isNonloop_of_mem heI⟩, hIE⟩⟩

Premises used: And.left, And.intro, Iff.intro, Matroid.Indep.isNonloop_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ ∀ ⦃I : Set α⦄, I ⊆ M.E → ((M.Indep I ∧ I ⊆ {e : α | M.IsNonloop e}) ∧ I ⊆ M.E ↔ M.Indep I)

Tactic:
exact fun I hIE ↦ ⟨ fun hI ↦ hI.1.1, fun hI ↦ ⟨⟨hI,fun e heI ↦ hI.isNonloop_of_mem heI⟩, hIE⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
h : ∀ (I : Set α), M.removeLoops.Indep I ↔ M.Indep I
⊢ M.removeLoops.Indep = M.Indep

Tactic:
ext I
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I : Set α
h : M.Indep I → I ⊆ {e : α | M.IsNonloop e}
⊢ M.removeLoops.Indep I ↔ M.Indep I

Tactic:
rw [removeLoops_eq_restrict, restrict_indep_iff, and_iff_left_iff_imp]

Premises used: Matroid.removeLoops_eq_restrict, Matroid.restrict_indep_iff, and_iff_left_iff_imp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I → I ⊆ {e : α | M.IsNonloop e}

Tactic:
fun h e ↦ h.isNonloop_of_mem

Premises used: Set.Mem, setOf, Set.Subset, Matroid.Indep.isNonloop_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I → I ⊆ {e : α | M.IsNonloop e}

Tactic:
exact fun h e ↦ h.isNonloop_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
h : ∀ (x x_1 : Set α), M.removeLoops.IsBasis' x x_1 ↔ M.IsBasis' x x_1
⊢ M.removeLoops.IsBasis' = M.IsBasis'

Tactic:
ext
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
x x_1 : Set α
⊢ M.removeLoops.IsBasis' x x_1 ↔ M.IsBasis' x x_1

Tactic:
simp [IsBasis']

Premises used: Matroid.IsBasis'
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
h : ∀ (B : Set α), M.removeLoops.IsBase B ↔ M.IsBase B
⊢ M.removeLoops.IsBase = M.IsBase

Tactic:
ext B
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
B : Set α
h : Maximal M.removeLoops.Indep B ↔ M.IsBase B
h₁ : Maximal M.Indep B ↔ M.IsBase B
h₂ h₃ : Maximal M.Indep B ↔ Maximal M.Indep B
⊢ M.removeLoops.IsBase B ↔ M.IsBase B

Tactic:
rw [isBase_iff_maximal_indep, removeLoops_indep_eq, isBase_iff_maximal_indep]

Premises used: Matroid.removeLoops_indep_eq, Matroid.isBase_iff_maximal_indep
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
h : ∀ (e : α), M.removeLoops.IsNonloop e ↔ M.IsNonloop e
⊢ M.removeLoops.IsNonloop = M.IsNonloop

Tactic:
ext e
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
h : (M ↾ {e : α | M.IsNonloop e}).IsNonloop e ↔ M.IsNonloop e
h₁ : M.IsNonloop e ∧ Membership.mem (γ := Set α) {e : α | M.IsNonloop e} e ↔ M.IsNonloop e
h₂ : M.IsNonloop e ∧ M.IsNonloop e ↔ M.IsNonloop e
h₃ h₄ : M.IsNonloop e ↔ M.IsNonloop e
⊢ M.removeLoops.IsNonloop e ↔ M.IsNonloop e

Tactic:
rw [removeLoops_eq_restrict, restrict_isNonloop_iff, mem_setOf, and_self]

Premises used: and_self, Set.mem_setOf, Matroid.removeLoops_eq_restrict, Matroid.restrict_isNonloop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
⊢ M.removeLoops.IsNonloop e

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.removeLoops.removeLoops = M.removeLoops

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ {e : α | M.IsNonloop e}
rwa : M ↾ {e : α | M.IsNonloop e} ↾ X = M ↾ X
rwa₁ : M ↾ X = M ↾ X
hR : X ⊆ {e : α | M.IsNonloop e}
rwa₂ : M ↾ X = M ↾ X
hR₁ hR₂ hR₃ : X ⊆ {e : α | M.IsNonloop e}
⊢ M.removeLoops ↾ X = M ↾ X

Tactic:
rwa [removeLoops_eq_restrict, restrict_restrict_eq]

Premises used: Matroid.removeLoops_eq_restrict, Matroid.restrict_restrict_eq
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
rw : M ↾ {e : α | (M ↾ univ).IsNonloop e} = M ↾ {e : α | M.IsNonloop e}
⊢ (M ↾ univ).removeLoops = M.removeLoops

Tactic:
rw [removeLoops_eq_restrict, restrict_restrict_eq _ (subset_univ _), removeLoops_eq_restrict]

Premises used: Set.subset_univ, Matroid.removeLoops_eq_restrict, Matroid.restrict_restrict_eq
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M ↾ {e : α | (M ↾ univ).IsNonloop e} = M ↾ {e : α | M.IsNonloop e}

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M N : Matroid α
hNM : N ≤r M
inst : N.Loopless
obtain : ∀ (R : Set α) (hR : R ⊆ M.E) (hNM : M ↾ R ≤r M) [(M ↾ R).Loopless], M ↾ R ≤r M.removeLoops
⊢ N ≤r M.removeLoops

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM.exists_eq_restrict

Premises used: Matroid.IsRestriction.exists_eq_restrict, rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
hNM : M ↾ R ≤r M
inst : (M ↾ R).Loopless
⊢ M ↾ R ≤r M.removeLoops

Tactic:
IsRestriction.of_subset M fun e heR ↦ ((M ↾ R).isNonloop_of_loopless heR).of_restrict

Premises used: Matroid.IsRestriction.of_subset, Matroid.removeLoops, Matroid.isNonloop_of_loopless, Matroid.IsNonloop.of_restrict
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
hNM : M ↾ R ≤r M
inst : (M ↾ R).Loopless
⊢ M ↾ R ≤r M.removeLoops

Tactic:
exact IsRestriction.of_subset M fun e heR ↦ ((M ↾ R).isNonloop_of_loopless heR).of_restrict

Premises used: Matroid.IsRestriction.of_subset, Matroid.isNonloop_of_loopless, Matroid.IsNonloop.of_restrict
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M N : Matroid α
hNM : N ≤r M
⊢ N.removeLoops ≤r M.removeLoops

Tactic:
((removeLoops_isRestriction _).trans hNM).isRestriction_removeLoops

Premises used: Matroid.removeLoops_isRestriction, Matroid.IsRestriction.trans, Matroid.IsRestriction.isRestriction_removeLoops
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
⊢ N.Indep (f '' ∅) ∧ InjOn f ∅

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
obtain :
  ∀ (I' : Set α) (hII' : I ⊂ I') (hI' : N.Indep (f '' I')) (hI'inj : InjOn f I'),
    ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)

Tactic:
obtain ⟨I', hII', hI', hI'inj⟩ := (not_maximal_subset_iff ⟨hI, hIinj⟩).1 hImax

Premises used: not_maximal_subset_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
⊢ ¬(N ↾ range f).IsBase (f '' I)

Tactic:
fun hB ↦ hII'.ne ?_

Premises used: HasSSubset.SSubset.ne, Not
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
refine : ∀ (hB : (N ↾ range f).IsBase (f '' I)), I = I'
⊢ ¬(N ↾ range f).IsBase (f '' I)

Tactic:
refine fun hB ↦ hII'.ne ?_

Premises used: HasSSubset.SSubset.ne
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
hB : (N ↾ range f).IsBase (f '' I)
⊢ (N ↾ range f).Indep (f '' I')

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
hB : (N ↾ range f).IsBase (f '' I)
⊢ f '' I = f '' I'

Tactic:
have h_im := hB.eq_of_subset_indep (by simpa) (image_mono hII'.subset)
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
hB : (N ↾ range f).IsBase (f '' I)
h_im : f '' I = f '' I'
rwa rwa₁ rwa₂ rwa₃ : ∀ (h_im : I = I'), I = I'
⊢ I = I'

Tactic:
rwa [hI'inj.image_eq_image_iff hII'.subset Subset.rfl] at h_im

Premises used: HasSSubset.SSubset.subset, Set.Subset.rfl, Set.InjOn.image_eq_image_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
⊢ ¬(N ↾ range f).IsBase (f '' I)

Tactic:
have h₁ : ¬(N ↾ range f).IsBase (f '' I) := by
        refine fun hB ↦ hII'.ne ?_
        have h_im := hB.eq_of_subset_indep (by simpa) (image_mono hII'.subset)
        rwa [hI'inj.image_eq_image_iff hII'.subset Subset.rfl] at h_im
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
⊢ (N ↾ range f).Indep (f '' B)

Tactic:
simpa using hBmax.1.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
refine : ∀ e ∈ (N ↾ range f).E \ f '' B, ¬(N ↾ range f).Indep (insert e (f '' B))
⊢ (N ↾ range f).IsBase (f '' B)

Tactic:
refine Indep.isBase_of_forall_insert (by simpa using hBmax.1.1) ?_

Premises used: Matroid.Indep.isBase_of_forall_insert
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
e : α
hfe : f e ∉ f '' B
hi : (N ↾ range f).Indep (insert (f e) (f '' B))
⊢ N.Indep (f '' insert e B) ∧ f '' insert e B ⊆ range f

Tactic:
rw [restrict_indep_iff, ← image_insert_eq] at hi

Premises used: Matroid.restrict_indep_iff, Set.image_insert_eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I_1 : Set α
M : Matroid α
N_1 N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun (I : Set α) ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
e : α
hfe : f e ∉ f '' B
hi : N.Indep (f '' insert e B) ∧ f '' insert e B ⊆ range f
rw : InjOn f B ∧ f e ∉ f '' B
⊢ InjOn f (insert e B)

Tactic:
rw [injOn_insert (fun heB ↦ hfe (mem_image_of_mem f heB))]

Premises used: Set.injOn_insert, Set.mem_image_of_mem