internlm/Lean-Github huggingface dataset:
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_2.refine_2.h.inl
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
x✝ : support x ⊆ s ∧ ∃ l, ⇑l = s.restrict x ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
hsupp : support x ⊆ s
l : ↑s →₀ K
hlrs : ⇑l = s.restrict x
hl : ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
i : ι
his : i ∈ s
⊢ (Finsupp.mapDomain s.incl l) i = x i
Tactic:
convert Finsupp.mapDomain_apply Subtype.val_injective l ⟨i,his⟩
Proof state after:
case h.e'_3
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
x✝ : support x ⊆ s ∧ ∃ l, ⇑l = s.restrict x ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
hsupp : support x ⊆ s
l : ↑s →₀ K
hlrs : ⇑l = s.restrict x
hl : ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
i : ι
his : i ∈ s
⊢ x i = l ⟨i, his⟩
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.e'_3
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
x✝ : support x ⊆ s ∧ ∃ l, ⇑l = s.restrict x ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
hsupp : support x ⊆ s
l : ↑s →₀ K
hlrs : ⇑l = s.restrict x
hl : ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
i : ι
his : i ∈ s
⊢ x i = l ⟨i, his⟩
Tactic:
simp [hlrs]
Proof state after:
no goals
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_2.refine_2.h.inr
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
x✝ : support x ⊆ s ∧ ∃ l, ⇑l = s.restrict x ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
hsupp : support x ⊆ s
l : ↑s →₀ K
hlrs : ⇑l = s.restrict x
hl : ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
i : ι
his : i ∉ s
⊢ x i = 0
Tactic:
simpa using not_mem_subset hsupp his
Proof state after:
no goals
Theorem: Set.Finite.relOrthSpace_relOrthSpace
Proof state before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
hs : s.Finite
U : Submodule K (ι → K)
hU : U ≤ s.supportedFun K
⊢ s.relOrthSpace (s.relOrthSpace U) = U
Tactic:
set U' : {U : Submodule K (ι → K) // U ≤ s.supportedFun K} := ⟨U,hU⟩
Proof state after:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
hs : s.Finite
U : Submodule K (ι → K)
hU : U ≤ s.supportedFun K
U' : { U // U ≤ s.supportedFun K } := ⟨U, hU⟩
⊢ s.relOrthSpace (s.relOrthSpace U) = U
Theorem: Set.Finite.relOrthSpace_relOrthSpace
Proof state before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
hs : s.Finite
U : Submodule K (ι → K)
hU : U ≤ s.supportedFun K
U' : { U // U ≤ s.supportedFun K } := ⟨U, hU⟩
⊢ s.relOrthSpace (s.relOrthSpace U) = U
Tactic:
have := hs.fintype
Proof state after:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
hs : s.Finite
U : Submodule K (ι → K)
hU : U ≤ s.supportedFun K
U' : { U // U ≤ s.supportedFun K } := ⟨U, hU⟩
this : Fintype ↑s
⊢ s.relOrthSpace (s.relOrthSpace U) = U
Theorem: Set.Finite.relOrthSpace_relOrthSpace
Proof state before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
hs : s.Finite
U : Submodule K (ι → K)
hU : U ≤ s.supportedFun K
U' : { U // U ≤ s.supportedFun K } := ⟨U, hU⟩
this : Fintype ↑s
⊢ s.relOrthSpace (s.relOrthSpace U) = U
Tactic:
rw [(show U = U' from rfl), ← Subtype.val_inj.2 <| (s.subtypeFunEquiv K).apply_symm_apply U',
  s.relOrthSpace_subtypeFunEquiv, s.relOrthSpace_subtypeFunEquiv, orthSpace_orthSpace]
Proof state after:
no goals
Theorem: Matroid.Parallel.eq
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : M.Parallel e f
⊢ e = f
Tactic:
rwa [Simple.parallel_iff_eq h.mem_ground_left] at h
Proof state after:
no goals
Theorem: Matroid.Simple.loopless
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hM : M.Simple
⊢ M.Loopless
Tactic:
infer_instance
Proof state after:
no goals
Theorem: Matroid.simple_iff_loopless_eq_of_parallel_forall
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ M.Loopless
Tactic:
infer_instance
Proof state after:
no goals
Theorem: Matroid.simple_iff_loopless_eq_of_parallel_forall
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
left✝ : M.Loopless
h : ∀ (e f : α), M.Parallel e f → e = f
e✝ f✝ : α
heE : e✝ ∈ M.E
⊢ e✝ = f✝ → M.Parallel e✝ f✝
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
left✝ : M.Loopless
h : ∀ (e f : α), M.Parallel e f → e = f
e✝ : α
heE : e✝ ∈ M.E
⊢ M.Parallel e✝ e✝
Theorem: Matroid.simple_iff_loopless_eq_of_parallel_forall
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
left✝ : M.Loopless
h : ∀ (e f : α), M.Parallel e f → e = f
e✝ : α
heE : e✝ ∈ M.E
⊢ M.Parallel e✝ e✝
Tactic:
exact (toNonloop heE).parallel_self
Proof state after:
no goals
Theorem: Matroid.parallel_class_eq
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
he : autoParam (e ∈ M.E) _auto✝
⊢ {f | M.Parallel e f} = {e}
Tactic:
simp_rw [parallel_iff_eq he, setOf_eq_eq_singleton']
Proof state after:
no goals
Theorem: Matroid.cl_singleton_eq
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
he : autoParam (e ∈ M.E) _auto✝
⊢ M.cl {e} = {e}
Tactic:
rw [cl_eq_parallel_class_union_loops, parallel_class_eq he, cl_empty_eq_empty, union_empty]
Proof state after:
no goals
Theorem: Matroid.simple_iff_cl_subset_self_forall
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
⊢ M.Simple ↔ ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
Tactic:
refine ⟨fun h e he ↦ by rw [cl_singleton_eq], fun h ↦ ?_⟩
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
⊢ M.Simple
Theorem: Matroid.simple_iff_cl_subset_self_forall
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
⊢ M.Simple
Tactic:
have hl : M.Loopless := by
  rw [loopless_iff_forall_not_loop]
  intro e _ hel
  obtain ⟨f, hf⟩ := M.exists_nonloop
  obtain (rfl : e = f) := (h f hf).subset (hel.mem_cl _)
  exact hf.not_loop hel
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
hl : M.Loopless
⊢ M.Simple
Theorem: Matroid.simple_iff_cl_subset_self_forall
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
hl : M.Loopless
⊢ M.Simple
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall, and_iff_right hl]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
hl : M.Loopless
⊢ ∀ (e f : α), M.Parallel e f → e = f
Theorem: Matroid.simple_iff_cl_subset_self_forall
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
hl : M.Loopless
⊢ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
exact fun e f hp ↦ (h _ hp.nonloop_right) hp.mem_cl
Proof state after:
no goals
Theorem: Matroid.simple_iff_cl_subset_self_forall
Proof state before:
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
inst✝ : M.RkPos
h : M.Simple
e : α
he : M.Nonloop e
⊢ M.cl {e} ⊆ {e}
Tactic:
rw [cl_singleton_eq]
Proof state after:
no goals
Theorem: Matroid.simple_iff_cl_subset_self_forall
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
⊢ M.Loopless
Tactic:
rw [loopless_iff_forall_not_loop]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
⊢ ∀ e ∈ M.E, ¬M.Loop e
Theorem: Matroid.simple_iff_cl_subset_self_forall
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
⊢ ∀ e ∈ M.E, ¬M.Loop e
Tactic:
intro e _ hel
Proof state after:
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
⊢ False
Theorem: Matroid.simple_iff_cl_subset_self_forall
Proof state before:
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
⊢ False
Tactic:
obtain ⟨f, hf⟩ := M.exists_nonloop
Proof state after:
case intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
f : α
hf : M.Nonloop f
⊢ False
Theorem: Matroid.simple_iff_cl_subset_self_forall
Proof state before:
case intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
f : α
hf : M.Nonloop f
⊢ False
Tactic:
obtain (rfl : e = f) := (h f hf).subset (hel.mem_cl _)
Proof state after:
case intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
hf : M.Nonloop e
⊢ False
Theorem: Matroid.simple_iff_cl_subset_self_forall
Proof state before:
case intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
inst✝ : M.RkPos
h : ∀ (e : α), M.Nonloop e → M.cl {e} ⊆ {e}
e : α
a✝ : e ∈ M.E
hel : M.Loop e
hf : M.Nonloop e
⊢ False
Tactic:
exact hf.not_loop hel
Proof state after:
no goals
Theorem: Matroid.cl_eq_self_of_subset_singleton
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
he : e ∈ M.E
hX : X ⊆ {e}
⊢ M.cl X = X
Tactic:
obtain (rfl | rfl) := subset_singleton_iff_eq.1 hX
Proof state after:
case inl
α : Type u_1
M N : Matroid α
e f g : α
I P D : Set α
inst✝ : M.Simple
he : e ∈ M.E
hX : ∅ ⊆ {e}
⊢ M.cl ∅ = ∅

case inr
α : Type u_1
M N : Matroid α
e f g : α
I P D : Set α
inst✝ : M.Simple
he : e ∈ M.E
hX : {e} ⊆ {e}
⊢ M.cl {e} = {e}
Theorem: Matroid.cl_eq_self_of_subset_singleton
Proof state before:
case inr
α : Type u_1
M N : Matroid α
e f g : α
I P D : Set α
inst✝ : M.Simple
he : e ∈ M.E
hX : {e} ⊆ {e}
⊢ M.cl {e} = {e}
Tactic:
exact cl_singleton_eq he
Proof state after:
no goals
Theorem: Matroid.cl_eq_self_of_subset_singleton
Proof state before:
case inl
α : Type u_1
M N : Matroid α
e f g : α
I P D : Set α
inst✝ : M.Simple
he : e ∈ M.E
hX : ∅ ⊆ {e}
⊢ M.cl ∅ = ∅
Tactic:
exact M.cl_empty_eq_empty
Proof state after:
no goals
Theorem: Matroid.singleton_flat
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
he : autoParam (e ∈ M.E) _auto✝
⊢ M.Flat {e}
Tactic:
rw [← cl_singleton_eq]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
he : autoParam (e ∈ M.E) _auto✝
⊢ M.Flat (M.cl {e})
Theorem: Matroid.singleton_flat
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
he : autoParam (e ∈ M.E) _auto✝
⊢ M.Flat (M.cl {e})
Tactic:
apply cl_flat
Proof state after:
no goals
Theorem: Matroid.pair_indep
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
he : autoParam (e ∈ M.E) _auto✝
hf : autoParam (f ∈ M.E) _auto✝
⊢ M.Indep {e, f}
Tactic:
obtain (rfl | hne) := eq_or_ne e f
Proof state after:
case inl
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
inst✝ : M.Simple
he : autoParam (e ∈ M.E) _auto✝
hf : autoParam (e ∈ M.E) _auto✝
⊢ M.Indep {e, e}

case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
he : autoParam (e ∈ M.E) _auto✝
hf : autoParam (f ∈ M.E) _auto✝
hne : e ≠ f
⊢ M.Indep {e, f}
Theorem: Matroid.pair_indep
Proof state before:
case inr
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
he : autoParam (e ∈ M.E) _auto✝
hf : autoParam (f ∈ M.E) _auto✝
hne : e ≠ f
⊢ M.Indep {e, f}
Tactic:
rwa [← not_dep_iff, ← (toNonloop he).parallel_iff_dep (toNonloop hf) hne, parallel_iff_eq he]
Proof state after:
no goals
Theorem: Matroid.pair_indep
Proof state before:
case inl
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
inst✝ : M.Simple
he : autoParam (e ∈ M.E) _auto✝
hf : autoParam (e ∈ M.E) _auto✝
⊢ M.Indep {e, e}
Tactic:
rw [pair_eq_singleton, indep_singleton]
Proof state after:
case inl
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
inst✝ : M.Simple
he : autoParam (e ∈ M.E) _auto✝
hf : autoParam (e ∈ M.E) _auto✝
⊢ M.Nonloop e
Theorem: Matroid.pair_indep
Proof state before:
case inl
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
inst✝ : M.Simple
he : autoParam (e ∈ M.E) _auto✝
hf : autoParam (e ∈ M.E) _auto✝
⊢ M.Nonloop e
Tactic:
exact toNonloop he
Proof state after:
no goals
Theorem: Matroid.indep_of_encard_le_two
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard ≤ 2
hI : autoParam (I ⊆ M.E) _auto✝
⊢ M.Indep I
Tactic:
have hne : I.encard ≠ ⊤ := (h.trans_lt (by exact (cmp_eq_lt_iff 2 ⊤).mp rfl : (2 : ℕ∞) < ⊤ )).ne
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard ≤ 2
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ M.Indep I
Theorem: Matroid.indep_of_encard_le_two
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard ≤ 2
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ M.Indep I
Tactic:
rw [le_iff_lt_or_eq, encard_eq_two, ← ENat.add_one_le_iff hne, (by norm_num : (2 : ℕ∞) = 1 + 1),
  WithTop.add_le_add_iff_right, encard_le_one_iff_eq] at h
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : (I = ∅ ∨ ∃ x, I = {x}) ∨ ∃ x y, x ≠ y ∧ I = {x, y}
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ M.Indep I

α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard + 1 ≤ 1 + 1 ∨ ∃ x y, x ≠ y ∧ I = {x, y}
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ 1 ≠ ⊤
Theorem: Matroid.indep_of_encard_le_two
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard + 1 ≤ 1 + 1 ∨ ∃ x y, x ≠ y ∧ I = {x, y}
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ 1 ≠ ⊤
Tactic:
norm_num
Proof state after:
no goals
Theorem: Matroid.indep_of_encard_le_two
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard ≤ 2
hI : autoParam (I ⊆ M.E) _auto✝
⊢ 2 < ⊤
Tactic:
exact (cmp_eq_lt_iff 2 ⊤).mp rfl
Proof state after:
no goals
Theorem: Matroid.indep_of_encard_le_two
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard + 1 ≤ 2 ∨ ∃ x y, x ≠ y ∧ I = {x, y}
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ 2 = 1 + 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Matroid.indep_of_encard_le_two
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : (I = ∅ ∨ ∃ x, I = {x}) ∨ ∃ x y, x ≠ y ∧ I = {x, y}
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ M.Indep I
Tactic:
obtain (rfl | ⟨x, rfl⟩) | ⟨x, y, -, rfl⟩ := h
Proof state after:
case inl.inl
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
hI : autoParam (∅ ⊆ M.E) _auto✝
hne : ∅.encard ≠ ⊤
⊢ M.Indep ∅

case inl.inr.intro
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x : α
hI : autoParam ({x} ⊆ M.E) _auto✝
hne : {x}.encard ≠ ⊤
⊢ M.Indep {x}

case inr.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x y : α
hI : autoParam ({x, y} ⊆ M.E) _auto✝
hne : {x, y}.encard ≠ ⊤
⊢ M.Indep {x, y}
Theorem: Matroid.indep_of_encard_le_two
Proof state before:
case inr.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x y : α
hI : autoParam ({x, y} ⊆ M.E) _auto✝
hne : {x, y}.encard ≠ ⊤
⊢ M.Indep {x, y}
Tactic:
exact pair_indep
Proof state after:
no goals
Theorem: Matroid.indep_of_encard_le_two
Proof state before:
case inl.inl
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
hI : autoParam (∅ ⊆ M.E) _auto✝
hne : ∅.encard ≠ ⊤
⊢ M.Indep ∅
Tactic:
exact M.empty_indep
Proof state after:
no goals
Theorem: Matroid.indep_of_encard_le_two
Proof state before:
case inl.inr.intro
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x : α
hI : autoParam ({x} ⊆ M.E) _auto✝
hne : {x}.encard ≠ ⊤
⊢ M.Indep {x}
Tactic:
refine indep_singleton.2 (toNonloop (by aesop_mat))
Proof state after:
no goals
Theorem: Matroid.indep_of_encard_le_two
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x : α
hI : autoParam ({x} ⊆ M.E) _auto✝
hne : {x}.encard ≠ ⊤
⊢ x ∈ M.E
Tactic:
aesop_mat
Proof state after:
no goals
Theorem: Matroid.er_pair_eq
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
hef : e ≠ f
he : autoParam (e ∈ M.E) _auto✝
hf : autoParam (f ∈ M.E) _auto✝
⊢ M.er {e, f} = 2
Tactic:
rw [(pair_indep he).er, encard_pair hef]
Proof state after:
no goals
Theorem: Matroid.simple_iff_three_le_girth
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ 3 ≤ M.girth
Tactic:
rw [le_girth_iff]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
Theorem: Matroid.simple_iff_three_le_girth
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
Tactic:
refine ⟨fun h C hC ↦ le_of_not_lt fun hlt ↦ ?_, fun h ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
C : Set α
hC : M.Circuit C
hlt : C.encard < 3
⊢ False

case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ M.Simple
Theorem: Matroid.simple_iff_three_le_girth
Proof state before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ M.Simple
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall, loopless_iff_forall_circuit, and_iff_left]
Proof state after:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ ∀ (C : Set α), M.Circuit C → 1 < C.encard

case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ ∀ (e f : α), M.Parallel e f → e = f
Theorem: Matroid.simple_iff_three_le_girth
Proof state before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
refine fun e f hef ↦ by_contra fun hne ↦ ?_
Proof state after:
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
e f : α
hef : M.Parallel e f
hne : ¬e = f
⊢ False
Theorem: Matroid.simple_iff_three_le_girth
Proof state before:
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
e f : α
hef : M.Parallel e f
hne : ¬e = f
⊢ False
Tactic:
have hcon := (h _ (hef.circuit_of_ne hne)).trans_eq (encard_pair hne)
Proof state after:
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
e f : α
hef : M.Parallel e f
hne : ¬e = f
hcon : 3 ≤ 2
⊢ False
Theorem: Matroid.simple_iff_three_le_girth
Proof state before:
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
e f : α
hef : M.Parallel e f
hne : ¬e = f
hcon : 3 ≤ 2
⊢ False
Tactic:
norm_num at hcon
Proof state after:
no goals
Theorem: Matroid.simple_iff_three_le_girth
Proof state before:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
C : Set α
hC : M.Circuit C
hlt : C.encard < 3
⊢ False
Tactic:
exact hC.dep.not_indep <| indep_of_encard_le_two (ENat.le_of_lt_add_one hlt)
Proof state after:
no goals
Theorem: Matroid.simple_iff_three_le_girth
Proof state before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ ∀ (C : Set α), M.Circuit C → 1 < C.encard
Tactic:
exact fun C hC ↦ (show (1 : ℕ∞) < 3 from Nat.one_lt_ofNat).trans_le (h C hC)
Proof state after:
no goals
Theorem: Matroid.simple_iff_forall_circuit
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ ∀ (C : Set α), M.Circuit C → 2 < C.encard
Tactic:
simp_rw [← ENat.add_one_le_iff (show 2 ≠ ⊤ by norm_num), show (2 : ℕ∞) + 1 = 3 from rfl,
  simple_iff_three_le_girth, le_girth_iff]
Proof state after:
no goals
Theorem: Matroid.simple_iff_forall_circuit
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ 2 ≠ ⊤
Tactic:
norm_num
Proof state after:
no goals
Theorem: Matroid.simple_iff_forall_pair_indep
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
Tactic:
refine ⟨fun h _ _ he hf ↦ pair_indep he hf, fun h ↦ ?_⟩
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
⊢ M.Simple
Theorem: Matroid.simple_iff_forall_pair_indep
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
⊢ M.Simple
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall, loopless_iff_forall_not_loop]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
⊢ (∀ e ∈ M.E, ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
Theorem: Matroid.simple_iff_forall_pair_indep
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
⊢ (∀ e ∈ M.E, ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
exact ⟨fun e he hl ↦ hl.dep.not_indep <| by simpa using h he he,
  fun e f hef ↦ hef.eq_of_indep (h hef.mem_ground_left hef.mem_ground_right) ⟩
Proof state after:
no goals
Theorem: Matroid.simple_iff_forall_pair_indep
Proof state before:
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
h : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
e : α
he : e ∈ M.E
hl : M.Loop e
⊢ M.Indep {e}
Tactic:
simpa using h he he
Proof state after:
no goals
Theorem: Matroid.simple_uniqueBaseOn_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D E : Set α
⊢ (uniqueBaseOn I E).Simple ↔ E ⊆ I
Tactic:
simp only [simple_iff_forall_pair_indep, uniqueBaseOn_ground, uniqueBaseOn_indep_iff',
  subset_inter_iff, pair_subset_iff]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D E : Set α
⊢ (∀ ⦃e f : α⦄, e ∈ E → f ∈ E → (e ∈ I ∧ f ∈ I) ∧ e ∈ E ∧ f ∈ E) ↔ E ⊆ I
Theorem: Matroid.simple_uniqueBaseOn_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D E : Set α
⊢ (∀ ⦃e f : α⦄, e ∈ E → f ∈ E → (e ∈ I ∧ f ∈ I) ∧ e ∈ E ∧ f ∈ E) ↔ E ⊆ I
Tactic:
exact ⟨fun h e heE ↦ (h heE heE).1.1, by tauto⟩
Proof state after:
no goals