internlm/Lean-Github huggingface dataset:
Theorem: Partition.exists_extend_partial_repFun'
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
t : Set α
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel x y → x = y
⊢ ∃ f, EqOn (⇑f) id t
Tactic:
simpa using P.exists_extend_partial_repFun (fun x : t ↦ x) (by simp)
  (by simp [P.rel_self_iff_mem]) (fun x y ↦ h x.2 y.2)
Proof state after:
no goals
Theorem: Partition.exists_extend_partial_repFun'
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
t : Set α
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel x y → x = y
⊢ ∀ (x : ↑t), ↑x ∉ s → (fun x => ↑x) x = ↑x
Tactic:
simp
Proof state after:
no goals
Theorem: Partition.exists_extend_partial_repFun'
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
t : Set α
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel x y → x = y
⊢ ∀ (x : ↑t), ↑x ∈ s → P.Rel (↑x) ((fun x => ↑x) x)
Tactic:
simp [P.rel_self_iff_mem]
Proof state after:
no goals
Theorem: Partition.nonempty_repFun
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
⊢ Nonempty P.RepFun
Tactic:
obtain ⟨f, -⟩ := P.exists_extend_partial_repFun' (t := ∅) (by simp)
Proof state after:
case intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
f : P.RepFun
⊢ Nonempty P.RepFun
Theorem: Partition.nonempty_repFun
Proof state before:
case intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
f : P.RepFun
⊢ Nonempty P.RepFun
Tactic:
exact ⟨f⟩
Proof state after:
no goals
Theorem: Partition.nonempty_repFun
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
⊢ ∀ ⦃x y : α⦄, x ∈ ∅ → y ∈ ∅ → P.Rel x y → x = y
Tactic:
simp
Proof state after:
no goals
Theorem: Partition.repFun_repFun
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z a b : α
s : Set α
P : Partition s
f f' : P.RepFun
x : α
⊢ f (f' x) = f x
Tactic:
obtain (hx | hx) := em (x ∈ s)
Proof state after:
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z a b : α
s : Set α
P : Partition s
f f' : P.RepFun
x : α
hx : x ∈ s
⊢ f (f' x) = f x

case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z a b : α
s : Set α
P : Partition s
f f' : P.RepFun
x : α
hx : x ∉ s
⊢ f (f' x) = f x
Theorem: Partition.repFun_repFun
Proof state before:
case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z a b : α
s : Set α
P : Partition s
f f' : P.RepFun
x : α
hx : x ∉ s
⊢ f (f' x) = f x
Tactic:
rw [f'.apply_of_not_mem hx, f.apply_of_not_mem hx]
Proof state after:
no goals
Theorem: Partition.repFun_repFun
Proof state before:
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z a b : α
s : Set α
P : Partition s
f f' : P.RepFun
x : α
hx : x ∈ s
⊢ f (f' x) = f x
Tactic:
exact f.apply_eq_apply (f'.rel_apply hx).symm
Proof state after:
no goals
Theorem: Partition.repFun_discrete_coeFun
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
⊢ ⇑f = id
Tactic:
ext x
Proof state after:
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
⊢ f x = id x
Theorem: Partition.repFun_discrete_coeFun
Proof state before:
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
⊢ f x = id x
Tactic:
obtain (hx | hx) := em (x ∈ s)
Proof state after:
case h.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
hx : x ∈ s
⊢ f x = id x

case h.inr
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
hx : x ∉ s
⊢ f x = id x
Theorem: Partition.repFun_discrete_coeFun
Proof state before:
case h.inr
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
hx : x ∉ s
⊢ f x = id x
Tactic:
rw [f.apply_of_not_mem hx, id]
Proof state after:
no goals
Theorem: Partition.repFun_discrete_coeFun
Proof state before:
case h.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
hx : x ∈ s
⊢ f x = id x
Tactic:
have hx' := f.rel_apply hx
Proof state after:
case h.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
hx : x ∈ s
hx' : (Partition.discrete s).Rel x (f x)
⊢ f x = id x
Theorem: Partition.repFun_discrete_coeFun
Proof state before:
case h.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
hx : x ∈ s
hx' : (Partition.discrete s).Rel x (f x)
⊢ f x = id x
Tactic:
simp only [discrete.rel_iff_eq] at hx'
Proof state after:
case h.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
hx : x ∈ s
hx' : x = f x ∧ x ∈ s
⊢ f x = id x
Theorem: Partition.repFun_discrete_coeFun
Proof state before:
case h.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝¹ x✝ y z a b : α
s✝ : Set α
P : Partition s✝
s : Set α
f : (Partition.discrete s).RepFun
x : α
hx : x ∈ s
hx' : x = f x ∧ x ∈ s
⊢ f x = id x
Tactic:
exact hx'.1.symm
Proof state after:
no goals
Theorem: Partition.RepFun.coeFun_eq_id_of_eq_discrete
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hP : P = Partition.discrete s
⊢ ⇑f = id
Tactic:
subst hP
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
f : (Partition.discrete s).RepFun
⊢ ⇑f = id
Theorem: Partition.RepFun.coeFun_eq_id_of_eq_discrete
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
f : (Partition.discrete s).RepFun
⊢ ⇑f = id
Tactic:
exact repFun_discrete_coeFun s f
Proof state after:
no goals
Theorem: ENat.lt_one_iff
Proof state before:
α : Type u_1
M : Matroid α
n : ℕ∞
⊢ n < 1 ↔ n = 0
Tactic:
rw [← not_iff_not, not_lt, ENat.one_le_iff_ne_zero]
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.exists_circuit_of_ne
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ f ∈ C
Tactic:
simpa [ConnectedTo, hne] using h
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.symm
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
⊢ M.ConnectedTo f e
Tactic:
obtain (⟨rfl, hef⟩ | ⟨C, hC, heC, hfC⟩) := h
Proof state after:
case inl.intro
α : Type u_1
M : Matroid α
C K : Set α
e g : α
hef : e ∈ M.E
⊢ M.ConnectedTo e e

case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M.ConnectedTo f e
Theorem: Matroid.ConnectedTo.symm
Proof state before:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M.ConnectedTo f e
Tactic:
exact .inr ⟨C, hC, hfC, heC⟩
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.symm
Proof state before:
case inl.intro
α : Type u_1
M : Matroid α
C K : Set α
e g : α
hef : e ∈ M.E
⊢ M.ConnectedTo e e
Tactic:
exact connectedTo_self hef
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.mem_ground_left
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
⊢ e ∈ M.E
Tactic:
obtain (⟨rfl, hef⟩ | ⟨C, hC, heC, -⟩) := h
Proof state after:
case inl.intro
α : Type u_1
M : Matroid α
C K : Set α
e g : α
hef : e ∈ M.E
⊢ e ∈ M.E

case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hC : M.Circuit C
heC : e ∈ C
⊢ e ∈ M.E
Theorem: Matroid.ConnectedTo.mem_ground_left
Proof state before:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hC : M.Circuit C
heC : e ∈ C
⊢ e ∈ M.E
Tactic:
exact hC.subset_ground heC
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.mem_ground_left
Proof state before:
case inl.intro
α : Type u_1
M : Matroid α
C K : Set α
e g : α
hef : e ∈ M.E
⊢ e ∈ M.E
Tactic:
exact hef
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.nonloop_left_of_ne
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
hef : e ≠ f
⊢ M.Nonloop e
Tactic:
obtain ⟨C, hC, heC, hfC⟩ := h.exists_circuit_of_ne hef
Proof state after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hef : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M.Nonloop e
Theorem: Matroid.ConnectedTo.nonloop_left_of_ne
Proof state before:
case intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hef : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M.Nonloop e
Tactic:
exact hC.nonloop_of_mem ⟨e, heC, f, hfC, hef⟩ heC
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.to_dual
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
⊢ M✶.ConnectedTo e f
Tactic:
obtain (rfl | hne) := eq_or_ne e f
Proof state after:
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.ConnectedTo e e
⊢ M✶.ConnectedTo e e

case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
⊢ M✶.ConnectedTo e f
Theorem: Matroid.ConnectedTo.to_dual
Proof state before:
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.ConnectedTo e e
⊢ M✶.ConnectedTo e e

case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
⊢ M✶.ConnectedTo e f
Tactic:
exact connectedTo_self h.mem_ground_left
Proof state after:
case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
⊢ M✶.ConnectedTo e f
Theorem: Matroid.ConnectedTo.to_dual
Proof state before:
case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
⊢ M✶.ConnectedTo e f
Tactic:
obtain ⟨C, hC, heC, hfC⟩ := h.exists_circuit_of_ne hne
Proof state after:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M✶.ConnectedTo e f
Theorem: Matroid.ConnectedTo.to_dual
Proof state before:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M✶.ConnectedTo e f
Tactic:
have hpara : (M ／ (C \ {e,f})).Parallel e f := by
  rw [parallel_iff_circuit hne]
  apply hC.contract_diff_circuit (by simp) (by simp [pair_subset_iff, heC, hfC])
Proof state after:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
⊢ M✶.ConnectedTo e f
Theorem: Matroid.ConnectedTo.to_dual
Proof state before:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
⊢ M✶.ConnectedTo e f
Tactic:
obtain ⟨B, hB, heB⟩ := hpara.nonloop_left.exists_mem_base
Proof state after:
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
⊢ M✶.ConnectedTo e f
Theorem: Matroid.ConnectedTo.to_dual
Proof state before:
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
⊢ M✶.ConnectedTo e f
Tactic:
have hK := fundCocct_cocircuit heB hB
Proof state after:
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
hK : (M ／ (C \ {e, f})).Cocircuit (fundCocct e B)
⊢ M✶.ConnectedTo e f
Theorem: Matroid.ConnectedTo.to_dual
Proof state before:
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
hK : (M ／ (C \ {e, f})).Cocircuit (fundCocct e B)
⊢ M✶.ConnectedTo e f
Tactic:
refine Circuit.mem_connectedTo_mem hK.of_contract.circuit (mem_fundCocct _ _ _) ?_
Proof state after:
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
hK : (M ／ (C \ {e, f})).Cocircuit (fundCocct e B)
⊢ f ∈ fundCocct e B
Theorem: Matroid.ConnectedTo.to_dual
Proof state before:
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
hK : (M ／ (C \ {e, f})).Cocircuit (fundCocct e B)
⊢ f ∈ fundCocct e B
Tactic:
exact hpara.mem_cocircuit_of_mem hK (mem_fundCocct _ _ _)
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.to_dual
Proof state before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ (M ／ (C \ {e, f})).Parallel e f
Tactic:
rw [parallel_iff_circuit hne]
Proof state after:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ (M ／ (C \ {e, f})).Circuit {e, f}
Theorem: Matroid.ConnectedTo.to_dual
Proof state before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ (M ／ (C \ {e, f})).Circuit {e, f}
Tactic:
apply hC.contract_diff_circuit (by simp) (by simp [pair_subset_iff, heC, hfC])
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.to_dual
Proof state before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ {e, f}.Nonempty
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.to_dual
Proof state before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ {e, f} ⊆ C
Tactic:
simp [pair_subset_iff, heC, hfC]
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.of_dual
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M✶.ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
simpa using h.to_dual
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.of_restrict
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
obtain (rfl | hne) := eq_or_ne e f
Proof state after:
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e e
⊢ M.ConnectedTo e e

case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
⊢ M.ConnectedTo e f
Theorem: Matroid.ConnectedTo.of_restrict
Proof state before:
case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
⊢ M.ConnectedTo e f
Tactic:
obtain ⟨C, hC, heC, hfC⟩ := hef.exists_circuit_of_ne hne
Proof state after:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
C : Set α
hC : (M ↾ R).Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M.ConnectedTo e f
Theorem: Matroid.ConnectedTo.of_restrict
Proof state before:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
C : Set α
hC : (M ↾ R).Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M.ConnectedTo e f
Tactic:
rw [restrict_circuit_iff] at hC
Proof state after:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C ∧ C ⊆ R
heC : e ∈ C
hfC : f ∈ C
⊢ M.ConnectedTo e f
Theorem: Matroid.ConnectedTo.of_restrict
Proof state before:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C ∧ C ⊆ R
heC : e ∈ C
hfC : f ∈ C
⊢ M.ConnectedTo e f
Tactic:
exact hC.1.mem_connectedTo_mem heC hfC
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.of_restrict
Proof state before:
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e e
⊢ M.ConnectedTo e e
Tactic:
simp [hR hef.mem_ground_left]
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.of_delete
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
D : Set α
hef : (M ＼ D).ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
rw [delete_eq_restrict] at hef
Proof state after:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
D : Set α
hef : (M ↾ M.E \ D).ConnectedTo e f
⊢ M.ConnectedTo e f
Theorem: Matroid.ConnectedTo.of_delete
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
D : Set α
hef : (M ↾ M.E \ D).ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
apply hef.of_restrict diff_subset
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.of_contract
Proof state before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hef : (M ／ C).ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
replace hef := hef.to_dual
Proof state after:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hef : (M ／ C)✶.ConnectedTo e f
⊢ M.ConnectedTo e f
Theorem: Matroid.ConnectedTo.of_contract
Proof state before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hef : (M ／ C)✶.ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
rw [contract_dual_eq_dual_delete] at hef
Proof state after:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hef : (M✶ ＼ C).ConnectedTo e f
⊢ M.ConnectedTo e f
Theorem: Matroid.ConnectedTo.of_contract
Proof state before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hef : (M✶ ＼ C).ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
exact hef.of_delete.of_dual
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.of_minor
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
N : Matroid α
hef : N.ConnectedTo e f
h : N ≤m M
⊢ M.ConnectedTo e f
Tactic:
obtain ⟨C, D, -, -, -, rfl⟩ := h
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C D : Set α
hef : (M ／ C ＼ D).ConnectedTo e f
⊢ M.ConnectedTo e f
Theorem: Matroid.ConnectedTo.of_minor
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C D : Set α
hef : (M ／ C ＼ D).ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
exact hef.of_delete.of_contract
Proof state after:
no goals
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hf : ¬M.Coloop f
hB : M.Base (insert e I)
⊢ M.ConnectedTo e f
Tactic:
simp only [hB.mem_coloop_iff_forall_not_mem_fundCct (.inr hfI), mem_diff, mem_insert_iff, not_or,
  and_imp, not_forall, Classical.not_imp, not_not, exists_prop, exists_and_left] at hf
Proof state after:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
hf : ∃ x ∈ M.E, ¬x = e ∧ x ∉ I ∧ f ∈ M.fundCct x (insert e I)
⊢ M.ConnectedTo e f
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
hf : ∃ x ∈ M.E, ¬x = e ∧ x ∉ I ∧ f ∈ M.fundCct x (insert e I)
⊢ M.ConnectedTo e f
Tactic:
obtain ⟨x, hx, hxe, hxI, hfC⟩ := hf
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
⊢ M.ConnectedTo e f
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof state before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
⊢ M.ConnectedTo e f
Tactic:
have hxi : M.Indep ((insert x I) \ {e}) := by
  rw [diff_singleton_eq_self (by simp [Ne.symm hxe, heI.2]), hI.insert_indep_iff_of_not_mem hxI,
    hI'.flat.cl]
  exact ⟨hx, hxI⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
⊢ M.ConnectedTo e f
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof state before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
⊢ M.ConnectedTo e f
Tactic:
have hC := Base.fundCct_circuit hB (show x ∈ M.E \ insert e I by simp [hx, hxI, hxe])
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
hC : M.Circuit (M.fundCct x (insert e I))
⊢ M.ConnectedTo e f
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof state before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
hC : M.Circuit (M.fundCct x (insert e I))
⊢ M.ConnectedTo e f
Tactic:
refine hC.mem_connectedTo_mem (by_contra fun heC ↦ ?_) hfC
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
hC : M.Circuit (M.fundCct x (insert e I))
heC : e ∉ M.fundCct x (insert e I)
⊢ False