internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
case intro.intro.intro
α : Type u_1
M : Matroid α
E I H B X : Set α
e f✝ : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
f : α
hfB✝ : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
hfB : f ∈ B
hfe : f = e
⊢ False
Tactic:
apply hB.indep.not_mem_cl_diff_of_mem he
Proof state after:
case intro.intro.intro
α : Type u_1
M : Matroid α
E I H B X : Set α
e f✝ : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
f : α
hfB✝ : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
hfB : f ∈ B
hfe : f = e
⊢ e ∈ M.cl (B \ {e})
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
case intro.intro.intro
α : Type u_1
M : Matroid α
E I H B X : Set α
e f✝ : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
f : α
hfB✝ : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
hfB : f ∈ B
hfe : f = e
⊢ e ∈ M.cl (B \ {e})
Tactic:
rwa [← hBH, ← hfe]
Proof state after:
no goals
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
⊢ H \ {e} ⊆ M.cl (B \ {e})
Tactic:
refine fun x hx ↦ by_contra fun hcl ↦ ?_
Proof state after:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
⊢ False
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
⊢ False
Tactic:
have hxB : x ∉ B
Proof state after:
case hxB
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
⊢ x ∉ B

case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
hxB : x ∉ B
⊢ False
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
hxB : x ∉ B
⊢ False
Tactic:
refine (h x ⟨hx.1, hxB⟩).1 (hB.exchange_base_of_indep hxB ?_)
Proof state after:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
hxB : x ∉ B
⊢ M.Indep (insert x (B \ {e}))
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
hxB : x ∉ B
⊢ M.Indep (insert x (B \ {e}))
Tactic:
rwa [← (hB.indep.diff {e}).not_mem_cl_iff_of_not_mem (not_mem_subset diff_subset hxB)
  (hH.subset_ground hx.1)]
Proof state after:
no goals
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
case hxB
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
⊢ x ∉ B
Tactic:
exact fun hxB' ↦ hcl (M.mem_cl_of_mem' ⟨hxB', hx.2⟩ (hH.subset_ground hx.1))
Proof state after:
no goals
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
case hb
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
⊢ M.Basis (B \ {e}) H
Tactic:
exact (hB.indep.diff _).basis_of_subset_of_subset_cl
  ((M.subset_cl (B \ {e}) (diff_subset.trans hB.subset_ground)).trans hBH.symm.subset) h1
Proof state after:
no goals
Theorem: Matroid.antichain_of_circuit_hyperplane
Proof state before:
α : Type u_1
M✝ : Matroid α
E I H B X : Set α
e f : α
M : Matroid α
⊢ IsAntichain (fun x x_1 => x ⊆ x_1) ({B | M.Base B} ∪ {H | M.Circuit H ∧ M.Hyperplane H})
Tactic:
rintro X ((hX : M.Base X) | ⟨hXc, -⟩) Y ((hY : M.Base Y) | ⟨hYc, hYh⟩) hne hss
Proof state after:
case inl.inl
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hX : M.Base X
Y : Set α
hY : M.Base Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False

case inl.inr.intro
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hX : M.Base X
Y : Set α
hYc : M.Circuit Y
hYh : M.Hyperplane Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False

case inr.intro.inl
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hXc : M.Circuit X
Y : Set α
hY : M.Base Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False

case inr.intro.inr.intro
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hXc : M.Circuit X
Y : Set α
hYc : M.Circuit Y
hYh : M.Hyperplane Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False
Theorem: Matroid.antichain_of_circuit_hyperplane
Proof state before:
case inr.intro.inr.intro
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hXc : M.Circuit X
Y : Set α
hYc : M.Circuit Y
hYh : M.Hyperplane Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False
Tactic:
exact hne (hXc.eq_of_subset_circuit hYc hss)
Proof state after:
no goals
Theorem: Matroid.antichain_of_circuit_hyperplane
Proof state before:
case inl.inl
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hX : M.Base X
Y : Set α
hY : M.Base Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False
Tactic:
exact hne (hX.eq_of_subset_base hY hss)
Proof state after:
no goals
Theorem: Matroid.antichain_of_circuit_hyperplane
Proof state before:
case inl.inr.intro
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hX : M.Base X
Y : Set α
hYc : M.Circuit Y
hYh : M.Hyperplane Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False
Tactic:
exact hYh.not_spanning (hX.spanning.superset hss)
Proof state after:
no goals
Theorem: Matroid.antichain_of_circuit_hyperplane
Proof state before:
case inr.intro.inl
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hXc : M.Circuit X
Y : Set α
hY : M.Base Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False
Tactic:
exact (hY.indep.subset hss).not_dep hXc.dep
Proof state after:
no goals
Theorem: Matroid.relaxSet_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
⊢ (M.relaxSet Hs).Base B ↔ M.Base B ∨ B ∈ Hs
Tactic:
simp only [relaxSet, Matroid.ofBase]
Proof state after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
⊢ M.Base B ∨ B ∈ Hs ∧ M.Circuit B ∧ M.Hyperplane B ↔ M.Base B ∨ B ∈ Hs
Theorem: Matroid.relaxSet_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
⊢ M.Base B ∨ B ∈ Hs ∧ M.Circuit B ∧ M.Hyperplane B ↔ M.Base B ∨ B ∈ Hs
Tactic:
exact ⟨fun h' ↦ h'.elim Or.inl (Or.inr ∘ And.left),
  fun h' ↦ h'.elim Or.inl (fun hBs ↦ Or.inr ⟨hBs, h B hBs⟩)⟩
Proof state after:
no goals
Theorem: Matroid.relaxSet_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
⊢ (M.relaxSet Hs).Indep I ↔ M.Indep I ∨ I ∈ Hs
Tactic:
simp_rw [indep_iff, relaxSet_base_iff h]
Proof state after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
⊢ (∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B) ↔ (∃ B, M.Base B ∧ I ⊆ B) ∨ I ∈ Hs
Theorem: Matroid.relaxSet_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
⊢ (∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B) ↔ (∃ B, M.Base B ∧ I ⊆ B) ∨ I ∈ Hs
Tactic:
refine' ⟨fun ⟨B, hB, hIB⟩ ↦ hB.elim (fun hB' ↦ Or.inl ⟨B, hB', hIB⟩) (fun hB' ↦ _),
  fun h ↦ h.elim (fun ⟨B, hB, hIB⟩ ↦ ⟨B, Or.inl hB, hIB⟩) fun hI ↦ ⟨I, Or.inr hI, rfl.subset⟩⟩
Proof state after:
α : Type u_1
M : Matroid α
E I H B✝ X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
x✝ : ∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B
B : Set α
hB : M.Base B ∨ B ∈ Hs
hIB : I ⊆ B
hB' : B ∈ Hs
⊢ (∃ B, M.Base B ∧ I ⊆ B) ∨ I ∈ Hs
Theorem: Matroid.relaxSet_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I H B✝ X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
x✝ : ∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B
B : Set α
hB : M.Base B ∨ B ∈ Hs
hIB : I ⊆ B
hB' : B ∈ Hs
⊢ (∃ B, M.Base B ∧ I ⊆ B) ∨ I ∈ Hs
Tactic:
refine hIB.eq_or_ssubset.elim (fun h ↦ Or.inr (by rwa [h])) (fun hss ↦ Or.inl ?_)
Proof state after:
α : Type u_1
M : Matroid α
E I H B✝ X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
x✝ : ∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B
B : Set α
hB : M.Base B ∨ B ∈ Hs
hIB : I ⊆ B
hB' : B ∈ Hs
hss : I ⊂ B
⊢ ∃ B, M.Base B ∧ I ⊆ B
Theorem: Matroid.relaxSet_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I H B✝ X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
x✝ : ∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B
B : Set α
hB : M.Base B ∨ B ∈ Hs
hIB : I ⊆ B
hB' : B ∈ Hs
hss : I ⊂ B
⊢ ∃ B, M.Base B ∧ I ⊆ B
Tactic:
apply Indep.exists_base_superset (hB.elim (fun h' ↦ h'.indep.subset hIB)
  (fun h' ↦ (h _ h').1.ssubset_indep hss))
Proof state after:
no goals
Theorem: Matroid.relaxSet_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I H B✝ X : Set α
e f : α
Hs : Set (Set α)
h✝ : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
x✝ : ∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B
B : Set α
hB : M.Base B ∨ B ∈ Hs
hIB : I ⊆ B
hB' : B ∈ Hs
h : I = B
⊢ I ∈ Hs
Tactic:
rwa [h]
Proof state after:
no goals
Theorem: Matroid.relax_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane X
hC : M.Circuit X
⊢ (M.relax X).Base B ↔ M.Base B ∨ B = X
Tactic:
rw [relax, relaxSet_base_iff, mem_singleton_iff]
Proof state after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane X
hC : M.Circuit X
⊢ ∀ H ∈ {X}, M.Circuit H ∧ M.Hyperplane H
Theorem: Matroid.relax_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane X
hC : M.Circuit X
⊢ ∀ H ∈ {X}, M.Circuit H ∧ M.Hyperplane H
Tactic:
simp [hH, hC]
Proof state after:
no goals
Theorem: Matroid.relax_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane X
hC : M.Circuit X
⊢ (M.relax X).Indep I ↔ M.Indep I ∨ I = X
Tactic:
rw [relax, relaxSet_indep_iff, mem_singleton_iff]
Proof state after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane X
hC : M.Circuit X
⊢ ∀ H ∈ {X}, M.Circuit H ∧ M.Hyperplane H
Theorem: Matroid.relax_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane X
hC : M.Circuit X
⊢ ∀ H ∈ {X}, M.Circuit H ∧ M.Hyperplane H
Tactic:
simp [hH, hC]
Proof state after:
no goals
Theorem: LinearEquiv.dualAnnihilator_map_eq
Proof state before:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
⊢ (map e U).dualAnnihilator = map e.symm.dualMap U.dualAnnihilator
Tactic:
ext x
Proof state after:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ x ∈ (map e U).dualAnnihilator ↔ x ∈ map e.symm.dualMap U.dualAnnihilator
Theorem: LinearEquiv.dualAnnihilator_map_eq
Proof state before:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ x ∈ (map e U).dualAnnihilator ↔ x ∈ map e.symm.dualMap U.dualAnnihilator
Tactic:
simp only [mem_dualAnnihilator, mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
  dualMap_apply_symm]
Proof state after:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ (∀ a ∈ U, x (e a) = 0) ↔ ∃ y, (∀ w ∈ U, y w = 0) ∧ y ∘ₗ ↑e.symm = x
Theorem: LinearEquiv.dualAnnihilator_map_eq
Proof state before:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ (∀ a ∈ U, x (e a) = 0) ↔ ∃ y, (∀ w ∈ U, y w = 0) ∧ y ∘ₗ ↑e.symm = x
Tactic:
refine ⟨fun h ↦ ⟨e.dualMap x, h, by ext; simp⟩, ?_⟩
Proof state after:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ (∃ y, (∀ w ∈ U, y w = 0) ∧ y ∘ₗ ↑e.symm = x) → ∀ a ∈ U, x (e a) = 0
Theorem: LinearEquiv.dualAnnihilator_map_eq
Proof state before:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ (∃ y, (∀ w ∈ U, y w = 0) ∧ y ∘ₗ ↑e.symm = x) → ∀ a ∈ U, x (e a) = 0
Tactic:
rintro ⟨y, hy, rfl⟩ x hxu
Proof state after:
case h.intro.intro
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
y : Module.Dual R M
hy : ∀ w ∈ U, y w = 0
x : M
hxu : x ∈ U
⊢ (y ∘ₗ ↑e.symm) (e x) = 0
Theorem: LinearEquiv.dualAnnihilator_map_eq
Proof state before:
case h.intro.intro
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
y : Module.Dual R M
hy : ∀ w ∈ U, y w = 0
x : M
hxu : x ∈ U
⊢ (y ∘ₗ ↑e.symm) (e x) = 0
Tactic:
simpa using hy x hxu
Proof state after:
no goals
Theorem: LinearEquiv.dualAnnihilator_map_eq
Proof state before:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
h : ∀ a ∈ U, x (e a) = 0
⊢ e.dualMap x ∘ₗ ↑e.symm = x
Tactic:
ext
Proof state after:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
h : ∀ a ∈ U, x (e a) = 0
x✝ : M'
⊢ (e.dualMap x ∘ₗ ↑e.symm) x✝ = x x✝
Theorem: LinearEquiv.dualAnnihilator_map_eq
Proof state before:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
h : ∀ a ∈ U, x (e a) = 0
x✝ : M'
⊢ (e.dualMap x ∘ₗ ↑e.symm) x✝ = x x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.unifOn_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ (unifOn E k).Indep I ↔ I.encard ≤ k ∧ I ⊆ E
Tactic:
simp [unifOn, and_comm]
Proof state after:
no goals
Theorem: Matroid.unifOn_top
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k : ℕ∞
E : Set α
⊢ unifOn E ⊤ = freeOn E
Tactic:
rw [unifOn, truncateTo_top]
Proof state after:
no goals
Theorem: Matroid.unifOn_zero
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k : ℕ∞
E : Set α
⊢ unifOn E 0 = loopyOn E
Tactic:
simp [unifOn]
Proof state after:
no goals
Theorem: Matroid.unifOn_empty
Proof state before:
α✝ : Type u_1
M : Matroid α✝
E I B X C : Set α✝
k : ℕ∞
α : Type u_2
a : ℕ
⊢ unifOn ∅ ↑a = emptyOn α
Tactic:
simp [unifOn]
Proof state after:
no goals
Theorem: Matroid.unifOn_eq_unifOn_min
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ unifOn E k = unifOn E (min k E.encard)
Tactic:
simp only [ge_iff_le, eq_iff_indep_iff_indep_forall, unifOn_ground_eq, unifOn_indep_iff,
  le_min_iff, and_congr_left_iff, iff_self_and, true_and]
Proof state after:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ∀ I ⊆ E, I ⊆ E → I.encard ≤ k → I.encard ≤ E.encard
Theorem: Matroid.unifOn_eq_unifOn_min
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ∀ I ⊆ E, I ⊆ E → I.encard ≤ k → I.encard ≤ E.encard
Tactic:
exact fun I hI _ _ ↦ encard_mono hI
Proof state after:
no goals
Theorem: Matroid.unifOn_encard
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ unifOn E E.encard = freeOn E
Tactic:
rw [unifOn, truncate_eq_self_of_rk_le (freeOn_erk_eq _).le]
Proof state after:
no goals
Theorem: Matroid.unifOn_eq_of_le
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
h : E.encard ≤ k
⊢ unifOn E k = freeOn E
Tactic:
rw [unifOn, truncate_eq_self_of_rk_le (by rwa [freeOn_erk_eq])]
Proof state after:
no goals
Theorem: Matroid.unifOn_eq_of_le
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
h : E.encard ≤ k
⊢ (freeOn E).erk ≤ k
Tactic:
rwa [freeOn_erk_eq]
Proof state after:
no goals
Theorem: Matroid.unifOn_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hBE : B ⊆ E
⊢ (unifOn E ↑k).Base B ↔ B.encard = ↑k
Tactic:
rw [unifOn, truncateTo_base_iff, freeOn_indep_iff, and_iff_right hBE]
Proof state after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hBE : B ⊆ E
⊢ ↑k ≤ (freeOn E).erk
Theorem: Matroid.unifOn_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hBE : B ⊆ E
⊢ ↑k ≤ (freeOn E).erk
Tactic:
rwa [freeOn_erk_eq]
Proof state after:
no goals
Theorem: Matroid.unifOn_base_iff'
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hktop : k ≠ ⊤
hk : k ≤ E.encard
hBE : B ⊆ E
⊢ (unifOn E k).Base B ↔ B.encard = k
Tactic:
lift k to ℕ using hktop
Proof state after:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
hBE : B ⊆ E
k : ℕ
hk : ↑k ≤ E.encard
⊢ (unifOn E ↑k).Base B ↔ B.encard = ↑k
Theorem: Matroid.unifOn_base_iff'
Proof state before:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
hBE : B ⊆ E
k : ℕ
hk : ↑k ≤ E.encard
⊢ (unifOn E ↑k).Base B ↔ B.encard = ↑k
Tactic:
rw [unifOn_base_iff hk hBE]
Proof state after:
no goals
Theorem: Matroid.unifOn_er_eq
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
hX : X ⊆ E
⊢ (unifOn E k).er X = min X.encard k
Tactic:
rw [unifOn, truncateTo_er_eq, freeOn_er_eq hX]
Proof state after:
no goals
Theorem: Matroid.unifOn_er_eq'
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ (unifOn E k).er X = min (X ∩ E).encard k
Tactic:
rw [← er_inter_ground_eq, unifOn_er_eq _ _ (by rw [unifOn_ground_eq]; apply inter_subset_right),
  unifOn_ground_eq]
Proof state after:
no goals
Theorem: Matroid.unifOn_er_eq'
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ X ∩ (unifOn E k).E ⊆ E
Tactic:
rw [unifOn_ground_eq]
Proof state after:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ X ∩ E ⊆ E
Theorem: Matroid.unifOn_er_eq'
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ X ∩ E ⊆ E
Tactic:
apply inter_subset_right
Proof state after:
no goals
Theorem: Matroid.unifOn_erk_eq
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ (unifOn E k).erk = min E.encard k
Tactic:
rw [erk_eq_er_ground, unifOn_ground_eq, unifOn_er_eq _ _ Subset.rfl]
Proof state after:
no goals
Theorem: Matroid.unifOn_dual_eq
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hE : E.Finite
⊢ (unifOn E k)✶ = unifOn E (E.encard - k)
Tactic:
obtain (rfl | hk) := eq_or_ne k ⊤
Proof state after:
case inl
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
⊢ (unifOn E ⊤)✶ = unifOn E (E.encard - ⊤)

case inr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hE : E.Finite
hk : k ≠ ⊤
⊢ (unifOn E k)✶ = unifOn E (E.encard - k)
Theorem: Matroid.unifOn_dual_eq
Proof state before:
case inl
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
⊢ (unifOn E ⊤)✶ = unifOn E (E.encard - ⊤)

case inr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hE : E.Finite
hk : k ≠ ⊤
⊢ (unifOn E k)✶ = unifOn E (E.encard - k)
Tactic:
simp
Proof state after:
case inr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hE : E.Finite
hk : k ≠ ⊤
⊢ (unifOn E k)✶ = unifOn E (E.encard - k)
Theorem: Matroid.unifOn_dual_eq
Proof state before:
case inr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hE : E.Finite
hk : k ≠ ⊤
⊢ (unifOn E k)✶ = unifOn E (E.encard - k)
Tactic:
lift k to ℕ using hk
Proof state after:
case inr.intro
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)
Theorem: Matroid.unifOn_dual_eq
Proof state before:
case inr.intro
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)
Tactic:
obtain (hle | hlt) := le_or_lt E.encard k
Proof state after:
case inr.intro.inl
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
hle : E.encard ≤ ↑k
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)

case inr.intro.inr
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)
Theorem: Matroid.unifOn_dual_eq
Proof state before:
case inr.intro.inr
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)
Tactic:
refine eq_of_base_iff_base_forall (by simp) (fun B hBE ↦ ?_)
Proof state after:
case inr.intro.inr
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
B : Set α
hBE : B ⊆ (unifOn E ↑k)✶.E
⊢ (unifOn E ↑k)✶.Base B ↔ (unifOn E (E.encard - ↑k)).Base B
Theorem: Matroid.unifOn_dual_eq
Proof state before:
case inr.intro.inr
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
B : Set α
hBE : B ⊆ (unifOn E ↑k)✶.E
⊢ (unifOn E ↑k)✶.Base B ↔ (unifOn E (E.encard - ↑k)).Base B
Tactic:
simp only [dual_ground, unifOn_ground_eq] at hBE
Proof state after:
case inr.intro.inr
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
B : Set α
hBE : B ⊆ E
⊢ (unifOn E ↑k)✶.Base B ↔ (unifOn E (E.encard - ↑k)).Base B