internlm/Lean-Github huggingface dataset:
Theorem: Matroid.isSimplification_iff
Proof state before:
case h.e'_3.h.e'_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
          apply_eq_of_rel := ⋯ } ''
      {e | M.Nonloop e} =
    N.E
Tactic:
refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩
Proof state after:
case h.e'_3.h.e'_3.refine_1
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
⊢ x ∈
      ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
            apply_eq_of_rel := ⋯ } ''
        {e | M.Nonloop e} →
    x ∈ N.E

case h.e'_3.h.e'_3.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
⊢ x ∈
    ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
          apply_eq_of_rel := ⋯ } ''
      {e | M.Nonloop e}
Theorem: Matroid.isSimplification_iff
Proof state before:
case h.e'_3.h.e'_3.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
⊢ x ∈
    ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
          apply_eq_of_rel := ⋯ } ''
      {e | M.Nonloop e}
Tactic:
have hx := ((toNonloop h).of_restriction hr)
Proof state after:
case h.e'_3.h.e'_3.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
hx : M.Nonloop x
⊢ x ∈
    ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
          apply_eq_of_rel := ⋯ } ''
      {e | M.Nonloop e}
Theorem: Matroid.isSimplification_iff
Proof state before:
case h.e'_3.h.e'_3.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
hx : M.Nonloop x
⊢ x ∈
    ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
          apply_eq_of_rel := ⋯ } ''
      {e | M.Nonloop e}
Tactic:
simp only [Partition.RepFun.mk_apply, mem_image, mem_setOf_eq]
Proof state after:
case h.e'_3.h.e'_3.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
hx : M.Nonloop x
⊢ ∃ x_1, M.Nonloop x_1 ∧ (if hx : M.Nonloop x_1 then f hx else x_1) = x
Theorem: Matroid.isSimplification_iff
Proof state before:
case h.e'_3.h.e'_3.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
hx : M.Nonloop x
⊢ ∃ x_1, M.Nonloop x_1 ∧ (if hx : M.Nonloop x_1 then f hx else x_1) = x
Tactic:
exact ⟨x, hx, by rw [dif_pos hx, ← (hf hx).2 _ ⟨h, hx.parallel_self⟩]⟩
Proof state after:
no goals
Theorem: Matroid.isSimplification_iff
Proof state before:
case refine_1
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
e : α
he : M.Nonloop e
⊢ ∃! f, f ∈ N.E ∧ M.Parallel e f
Tactic:
obtain ⟨f, rfl⟩ := h
Proof state after:
case refine_1.intro
α : Type u_1
M : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y e : α
he : M.Nonloop e
f : M.parallelClasses.RepFun
⊢ ∃! f_1, f_1 ∈ (M ↾ ⇑f '' {e | M.Nonloop e}).E ∧ M.Parallel e f_1
Theorem: Matroid.isSimplification_iff
Proof state before:
case refine_1.intro
α : Type u_1
M : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y e : α
he : M.Nonloop e
f : M.parallelClasses.RepFun
⊢ ∃! f_1, f_1 ∈ (M ↾ ⇑f '' {e | M.Nonloop e}).E ∧ M.Parallel e f_1
Tactic:
refine ⟨f e, ⟨⟨e, he, rfl⟩, f.rel_apply he⟩, ?_⟩
Proof state after:
case refine_1.intro
α : Type u_1
M : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y e : α
he : M.Nonloop e
f : M.parallelClasses.RepFun
⊢ ∀ (y : α), (fun f_1 => f_1 ∈ (M ↾ ⇑f '' {e | M.Nonloop e}).E ∧ M.Parallel e f_1) y → y = f e
Theorem: Matroid.isSimplification_iff
Proof state before:
case refine_1.intro
α : Type u_1
M : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y e : α
he : M.Nonloop e
f : M.parallelClasses.RepFun
⊢ ∀ (y : α), (fun f_1 => f_1 ∈ (M ↾ ⇑f '' {e | M.Nonloop e}).E ∧ M.Parallel e f_1) y → y = f e
Tactic:
rintro _ ⟨⟨y, -, rfl⟩, hey⟩
Proof state after:
case refine_1.intro.intro.intro.intro
α : Type u_1
M : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y✝ e : α
he : M.Nonloop e
f : M.parallelClasses.RepFun
y : α
hey : M.Parallel e (f y)
⊢ f y = f e
Theorem: Matroid.isSimplification_iff
Proof state before:
case refine_1.intro.intro.intro.intro
α : Type u_1
M : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y✝ e : α
he : M.Nonloop e
f : M.parallelClasses.RepFun
y : α
hey : M.Parallel e (f y)
⊢ f y = f e
Tactic:
simp [f.apply_eq_apply hey]
Proof state after:
no goals
Theorem: Matroid.isSimplification_iff
Proof state before:
case refine_2.refine_1
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ ∀ a ∉ {e | M.Nonloop e}, (fun x => if hx : M.Nonloop x then f hx else x) a = a
Tactic:
exact fun a ha ↦ by simp_rw [dif_neg (show ¬ M.Nonloop a from ha)]
Proof state after:
no goals
Theorem: Matroid.isSimplification_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a : α
ha : a ∉ {e | M.Nonloop e}
⊢ (fun x => if hx : M.Nonloop x then f hx else x) a = a
Tactic:
simp_rw [dif_neg (show ¬ M.Nonloop a from ha)]
Proof state after:
no goals
Theorem: Matroid.isSimplification_iff
Proof state before:
case refine_2.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ ∀ a ∈ {e | M.Nonloop e}, M.parallelClasses.Rel a ((fun x => if hx : M.Nonloop x then f hx else x) a)
Tactic:
intro a (ha : M.Nonloop a)
Proof state after:
case refine_2.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a : α
ha : M.Nonloop a
⊢ M.parallelClasses.Rel a ((fun x => if hx : M.Nonloop x then f hx else x) a)
Theorem: Matroid.isSimplification_iff
Proof state before:
case refine_2.refine_2
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a : α
ha : M.Nonloop a
⊢ M.parallelClasses.Rel a ((fun x => if hx : M.Nonloop x then f hx else x) a)
Tactic:
simp [dif_pos ha, (hf ha).1.2]
Proof state after:
no goals
Theorem: Matroid.isSimplification_iff
Proof state before:
case refine_2.refine_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
⊢ ∀ (a b : α),
    M.parallelClasses.Rel a b →
      (fun x => if hx : M.Nonloop x then f hx else x) a = (fun x => if hx : M.Nonloop x then f hx else x) b
Tactic:
intro a b (hab : M.Parallel a b)
Proof state after:
case refine_2.refine_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a b : α
hab : M.Parallel a b
⊢ (fun x => if hx : M.Nonloop x then f hx else x) a = (fun x => if hx : M.Nonloop x then f hx else x) b
Theorem: Matroid.isSimplification_iff
Proof state before:
case refine_2.refine_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a b : α
hab : M.Parallel a b
⊢ (fun x => if hx : M.Nonloop x then f hx else x) a = (fun x => if hx : M.Nonloop x then f hx else x) b
Tactic:
simp only [hab.nonloop_left, ↓reduceDite, hab.nonloop_right]
Proof state after:
case refine_2.refine_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a b : α
hab : M.Parallel a b
⊢ f ⋯ = f ⋯
Theorem: Matroid.isSimplification_iff
Proof state before:
case refine_2.refine_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a b : α
hab : M.Parallel a b
⊢ f ⋯ = f ⋯
Tactic:
exact Eq.symm <| (hf hab.nonloop_left).2 (f hab.nonloop_right)
  ⟨(hf hab.nonloop_right).1.1, hab.trans (hf hab.nonloop_right).1.2⟩
Proof state after:
no goals
Theorem: Matroid.isSimplification_iff
Proof state before:
case h.e'_3.h.e'_3.refine_1
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
⊢ x ∈
      ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
            apply_eq_of_rel := ⋯ } ''
        {e | M.Nonloop e} →
    x ∈ N.E
Tactic:
rintro ⟨x,(hx : M.Nonloop x),rfl⟩
Proof state after:
case h.e'_3.h.e'_3.refine_1.intro.intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
hx : M.Nonloop x
⊢ { toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
        apply_eq_of_rel := ⋯ }
      x ∈
    N.E
Theorem: Matroid.isSimplification_iff
Proof state before:
case h.e'_3.h.e'_3.refine_1.intro.intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
hx : M.Nonloop x
⊢ { toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
        apply_eq_of_rel := ⋯ }
      x ∈
    N.E
Tactic:
simp [hx, (hf hx).1.1]
Proof state after:
no goals
Theorem: Matroid.isSimplification_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x✝¹ y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h✝ : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
x : α
h : x ∈ N.E
hx : M.Nonloop x
⊢ (if hx : M.Nonloop x then f hx else x) = x
Tactic:
rw [dif_pos hx, ← (hf hx).2 _ ⟨h, hx.parallel_self⟩]
Proof state after:
no goals
Theorem: Matroid.IsSimplification.of_restriction
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
M' : Matroid α
h : N.IsSimplification M
hNM' : N ≤r M'
hM'M : M' ≤r M
⊢ N.IsSimplification M'
Tactic:
obtain ⟨R, hR, rfl⟩ := hM'M.exists_eq_restrict
Proof state after:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
⊢ N.IsSimplification (M ↾ R)
Theorem: Matroid.IsSimplification.of_restriction
Proof state before:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
⊢ N.IsSimplification (M ↾ R)
Tactic:
rw [isSimplification_iff] at h ⊢
Proof state after:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
⊢ N.Loopless ∧ N ≤r M ↾ R ∧ ∀ ⦃e : α⦄, (M ↾ R).Nonloop e → ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f
Theorem: Matroid.IsSimplification.of_restriction
Proof state before:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
⊢ N.Loopless ∧ N ≤r M ↾ R ∧ ∀ ⦃e : α⦄, (M ↾ R).Nonloop e → ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f
Tactic:
refine ⟨h.1, hNM', fun e he ↦ ?_⟩
Proof state after:
case intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
⊢ ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f
Theorem: Matroid.IsSimplification.of_restriction
Proof state before:
case intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
⊢ ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f
Tactic:
obtain ⟨f, hf, hf'⟩ := h.2.2 (he.of_restriction hM'M)
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
f : α
hf : f ∈ N.E ∧ M.Parallel e f
hf' : ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f
⊢ ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f
Theorem: Matroid.IsSimplification.of_restriction
Proof state before:
case intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
f : α
hf : f ∈ N.E ∧ M.Parallel e f
hf' : ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f
⊢ ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f
Tactic:
simp only [restrict_parallel_iff]
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
f : α
hf : f ∈ N.E ∧ M.Parallel e f
hf' : ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f
⊢ ∃! f, f ∈ N.E ∧ M.Parallel e f ∧ e ∈ R ∧ f ∈ R
Theorem: Matroid.IsSimplification.of_restriction
Proof state before:
case intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
f : α
hf : f ∈ N.E ∧ M.Parallel e f
hf' : ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f
⊢ ∃! f, f ∈ N.E ∧ M.Parallel e f ∧ e ∈ R ∧ f ∈ R
Tactic:
exact ⟨f, ⟨hf.1, hf.2, he.mem_ground, hNM'.subset hf.1⟩, by tauto⟩
Proof state after:
no goals
Theorem: Matroid.IsSimplification.of_restriction
Proof state before:
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
f : α
hf : f ∈ N.E ∧ M.Parallel e f
hf' : ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f
⊢ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f ∧ e ∈ R ∧ f ∈ R) y → y = f
Tactic:
tauto
Proof state after:
no goals
Theorem: Matroid.IsSimplification.exists_of_strictRestriction
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
Tactic:
obtain ⟨e, heM, heN⟩ := exists_of_ssubset hNM.ssubset
Proof state after:
case intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
Theorem: Matroid.IsSimplification.exists_of_strictRestriction
Proof state before:
case intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
Tactic:
obtain (he | he) := M.loop_or_nonloop e
Proof state after:
case intro.intro.inl
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Loop e
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E

case intro.intro.inr
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
Theorem: Matroid.IsSimplification.exists_of_strictRestriction
Proof state before:
case intro.intro.inr
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
Tactic:
obtain ⟨f, hN⟩ := hN
Proof state after:
case intro.intro.inr.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
f : M.parallelClasses.RepFun
hN : N = M ↾ ⇑f '' {e | M.Nonloop e}
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
Theorem: Matroid.IsSimplification.exists_of_strictRestriction
Proof state before:
case intro.intro.inr.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
f : M.parallelClasses.RepFun
hN : N = M ↾ ⇑f '' {e | M.Nonloop e}
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
Tactic:
refine .inr ⟨e, f e, f.rel_apply he, heM, heN, ?_⟩
Proof state after:
case intro.intro.inr.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
f : M.parallelClasses.RepFun
hN : N = M ↾ ⇑f '' {e | M.Nonloop e}
⊢ f e ∈ N.E
Theorem: Matroid.IsSimplification.exists_of_strictRestriction
Proof state before:
case intro.intro.inr.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
f : M.parallelClasses.RepFun
hN : N = M ↾ ⇑f '' {e | M.Nonloop e}
⊢ f e ∈ N.E
Tactic:
simp only [hN, restrict_ground_eq, mem_image, mem_setOf_eq]
Proof state after:
case intro.intro.inr.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
f : M.parallelClasses.RepFun
hN : N = M ↾ ⇑f '' {e | M.Nonloop e}
⊢ ∃ x, M.Nonloop x ∧ f x = f e
Theorem: Matroid.IsSimplification.exists_of_strictRestriction
Proof state before:
case intro.intro.inr.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
f : M.parallelClasses.RepFun
hN : N = M ↾ ⇑f '' {e | M.Nonloop e}
⊢ ∃ x, M.Nonloop x ∧ f x = f e
Tactic:
exact ⟨e, he, rfl⟩
Proof state after:
no goals
Theorem: Matroid.IsSimplification.exists_of_strictRestriction
Proof state before:
case intro.intro.inl
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Loop e
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
Tactic:
exact .inl ⟨e, he, heN⟩
Proof state after:
no goals