internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∉ C
⊢ e = f
Tactic:
apply h
Proof state after:
case neg.a
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∉ C
⊢ (M ／ C).Parallel e f
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case neg.a
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∉ C
⊢ (M ／ C).Parallel e f
Tactic:
rw [parallel_iff, contract_cl_eq, contract_cl_eq, ← cl_union_cl_left_eq, hef.cl_eq_cl,
  cl_union_cl_left_eq, and_iff_left rfl]
Proof state after:
case neg.a
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∉ C
⊢ (M ／ C).Nonloop e ∧ (M ／ C).Nonloop f
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case neg.a
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∉ C
⊢ (M ／ C).Nonloop e ∧ (M ／ C).Nonloop f
Tactic:
exact ⟨toNonloop ⟨hef.mem_ground_left, heC⟩, toNonloop ⟨hef.mem_ground_right, hfC⟩⟩
Proof state after:
no goals
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
⊢ e = f
Tactic:
by_cases hfC : f ∈ C
Proof state after:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
hfC : f ∈ C
⊢ e = f

case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
hfC : f ∉ C
⊢ e = f
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
hfC : f ∉ C
⊢ e = f
Tactic:
refine by_contra fun hne ↦ not_loop (M ／ C) f ?_
Proof state after:
case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
hfC : f ∉ C
hne : ¬e = f
⊢ (M ／ C).Loop f
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
hfC : f ∉ C
hne : ¬e = f
⊢ (M ／ C).Loop f
Tactic:
exact (hef.loop_of_contract hne).minor ⟨hef.mem_ground_right, hfC⟩ (contract_minor_of_mem _ heC)
Proof state after:
no goals
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
hfC : f ∈ C
⊢ e = f
Tactic:
exact hC _ _ hef heC hfC
Proof state after:
no goals
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∈ C
⊢ e = f
Tactic:
refine by_contra fun (hne : e ≠ f) ↦ not_loop (M ／ C) e ?_
Proof state after:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∈ C
hne : e ≠ f
⊢ (M ／ C).Loop e
Theorem: Matroid.Simple.of_restrict_contract
Proof state before:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∈ C
hne : e ≠ f
⊢ (M ／ C).Loop e
Tactic:
exact (hef.symm.loop_of_contract hne.symm).minor ⟨hef.mem_ground_left, heC⟩
  (contract_minor_of_mem _ hfC)
Proof state after:
no goals
Theorem: Matroid.IsSimplification.repFun_apply_mem_ground
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
he : M.Nonloop e
⊢ h.repFun e ∈ N.E
Tactic:
rw [← congr_arg Matroid.E h.image_restrict_repFun, restrict_ground_eq]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
he : M.Nonloop e
⊢ h.repFun e ∈ ⇑h.repFun '' {e | M.Nonloop e}
Theorem: Matroid.IsSimplification.repFun_apply_mem_ground
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
he : M.Nonloop e
⊢ h.repFun e ∈ ⇑h.repFun '' {e | M.Nonloop e}
Tactic:
exact mem_image_of_mem h.repFun he
Proof state after:
no goals
Theorem: Matroid.IsSimplification.simple
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ N.Simple
Tactic:
obtain ⟨f, rfl⟩ := h
Proof state after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (M ↾ ⇑f '' {e | M.Nonloop e}).Simple
Theorem: Matroid.IsSimplification.simple
Proof state before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (M ↾ ⇑f '' {e | M.Nonloop e}).Simple
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall]
Proof state after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (M ↾ ⇑f '' {e | M.Nonloop e}).Loopless ∧ ∀ (e f_1 : α), (M ↾ ⇑f '' {e | M.Nonloop e}).Parallel e f_1 → e = f_1
Theorem: Matroid.IsSimplification.simple
Proof state before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (M ↾ ⇑f '' {e | M.Nonloop e}).Loopless ∧ ∀ (e f_1 : α), (M ↾ ⇑f '' {e | M.Nonloop e}).Parallel e f_1 → e = f_1
Tactic:
simp only [restrict_parallel_iff, mem_image, mem_setOf_eq, and_imp, forall_exists_index,
  loopless_iff_forall_nonloop, restrict_ground_eq, mem_image, mem_setOf_eq, restrict_nonloop_iff,
  forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
Proof state after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (∀ (a : α), M.Nonloop a → M.Nonloop (f a) ∧ ∃ x, M.Nonloop x ∧ f x = f a) ∧
    ∀ (e f_1 : α), M.Parallel e f_1 → ∀ (x : α), M.Nonloop x → f x = e → ∀ (x : α), M.Nonloop x → f x = f_1 → e = f_1
Theorem: Matroid.IsSimplification.simple
Proof state before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (∀ (a : α), M.Nonloop a → M.Nonloop (f a) ∧ ∃ x, M.Nonloop x ∧ f x = f a) ∧
    ∀ (e f_1 : α), M.Parallel e f_1 → ∀ (x : α), M.Nonloop x → f x = e → ∀ (x : α), M.Nonloop x → f x = f_1 → e = f_1
Tactic:
refine ⟨fun x hx ↦ ⟨f.apply_mem hx, ⟨x, hx, rfl⟩⟩, ?_⟩
Proof state after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ ∀ (e f_1 : α), M.Parallel e f_1 → ∀ (x : α), M.Nonloop x → f x = e → ∀ (x : α), M.Nonloop x → f x = f_1 → e = f_1
Theorem: Matroid.IsSimplification.simple
Proof state before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ ∀ (e f_1 : α), M.Parallel e f_1 → ∀ (x : α), M.Nonloop x → f x = e → ∀ (x : α), M.Nonloop x → f x = f_1 → e = f_1
Tactic:
rintro _ _ hxy x - rfl y - rfl
Proof state after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x✝ y✝ : α
f : M.parallelClasses.RepFun
x y : α
hxy : M.Parallel (f x) (f y)
⊢ f x = f y
Theorem: Matroid.IsSimplification.simple
Proof state before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x✝ y✝ : α
f : M.parallelClasses.RepFun
x y : α
hxy : M.Parallel (f x) (f y)
⊢ f x = f y
Tactic:
simpa using f.apply_eq_apply hxy
Proof state after:
no goals
Theorem: Matroid.Simple.exists_subset_isSimplification
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
⊢ ∃ N, N.IsSimplification M ∧ X ⊆ N.E
Tactic:
obtain ⟨f, hf⟩ := M.parallelClasses.exists_extend_partial_repFun'
  (fun _ _ ↦ hX.eq_of_parallel_of_mem)
Proof state after:
case intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
f : M.parallelClasses.RepFun
hf : EqOn (⇑f) id X
⊢ ∃ N, N.IsSimplification M ∧ X ⊆ N.E
Theorem: Matroid.Simple.exists_subset_isSimplification
Proof state before:
case intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
f : M.parallelClasses.RepFun
hf : EqOn (⇑f) id X
⊢ ∃ N, N.IsSimplification M ∧ X ⊆ N.E
Tactic:
refine ⟨_, ⟨f,rfl⟩, ?_⟩
Proof state after:
case intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
f : M.parallelClasses.RepFun
hf : EqOn (⇑f) id X
⊢ X ⊆ (M ↾ ⇑f '' {e | M.Nonloop e}).E
Theorem: Matroid.Simple.exists_subset_isSimplification
Proof state before:
case intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
f : M.parallelClasses.RepFun
hf : EqOn (⇑f) id X
⊢ X ⊆ (M ↾ ⇑f '' {e | M.Nonloop e}).E
Tactic:
rw [← image_id X, ← hf.image_eq]
Proof state after:
case intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
f : M.parallelClasses.RepFun
hf : EqOn (⇑f) id X
⊢ ⇑f '' X ⊆ (M ↾ ⇑f '' {e | M.Nonloop e}).E
Theorem: Matroid.Simple.exists_subset_isSimplification
Proof state before:
case intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
f : M.parallelClasses.RepFun
hf : EqOn (⇑f) id X
⊢ ⇑f '' X ⊆ (M ↾ ⇑f '' {e | M.Nonloop e}).E
Tactic:
exact image_subset f hX.subset_nonloops
Proof state after:
no goals
Theorem: Matroid.IsSimplification.restriction
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ N ≤r M
Tactic:
obtain ⟨f, rfl⟩ := h
Proof state after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ M ↾ ⇑f '' {e | M.Nonloop e} ≤r M
Theorem: Matroid.IsSimplification.restriction
Proof state before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ M ↾ ⇑f '' {e | M.Nonloop e} ≤r M
Tactic:
refine restrict_restriction _ _ ?_
Proof state after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ ⇑f '' {e | M.Nonloop e} ⊆ M.E
Theorem: Matroid.IsSimplification.restriction
Proof state before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ ⇑f '' {e | M.Nonloop e} ⊆ M.E
Tactic:
rintro _ ⟨x,hx,rfl⟩
Proof state after:
case intro.intro.intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x✝ y : α
f : M.parallelClasses.RepFun
x : α
hx : x ∈ {e | M.Nonloop e}
⊢ f x ∈ M.E
Theorem: Matroid.IsSimplification.restriction
Proof state before:
case intro.intro.intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x✝ y : α
f : M.parallelClasses.RepFun
x : α
hx : x ∈ {e | M.Nonloop e}
⊢ f x ∈ M.E
Tactic:
exact Nonloop.mem_ground <| f.apply_mem hx
Proof state after:
no goals
Theorem: Matroid.Simple.exists_restriction_isSimplification_of_restriction
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
hN : N.Simple
h : N ≤r M
⊢ ∃ M', M'.IsSimplification M ∧ N ≤r M'
Tactic:
obtain ⟨R, -, rfl⟩ := h.exists_eq_restrict
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
⊢ ∃ M', M'.IsSimplification M ∧ M ↾ R ≤r M'
Theorem: Matroid.Simple.exists_restriction_isSimplification_of_restriction
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
⊢ ∃ M', M'.IsSimplification M ∧ M ↾ R ≤r M'
Tactic:
obtain ⟨M', hM', hRM'⟩ := hN.exists_subset_isSimplification
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
M' : Matroid α
hM' : M'.IsSimplification M
hRM' : R ⊆ M'.E
⊢ ∃ M', M'.IsSimplification M ∧ M ↾ R ≤r M'
Theorem: Matroid.Simple.exists_restriction_isSimplification_of_restriction
Proof state before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
M' : Matroid α
hM' : M'.IsSimplification M
hRM' : R ⊆ M'.E
⊢ ∃ M', M'.IsSimplification M ∧ M ↾ R ≤r M'
Tactic:
refine ⟨M', hM', ?_⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
M' : Matroid α
hM' : M'.IsSimplification M
hRM' : R ⊆ M'.E
⊢ M ↾ R ≤r M'
Theorem: Matroid.Simple.exists_restriction_isSimplification_of_restriction
Proof state before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
M' : Matroid α
hM' : M'.IsSimplification M
hRM' : R ⊆ M'.E
⊢ M ↾ R ≤r M'
Tactic:
obtain ⟨R', -, rfl⟩ := hM'.restriction.exists_eq_restrict
Proof state after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
R' : Set α
hM' : (M ↾ R').IsSimplification M
hRM' : R ⊆ (M ↾ R').E
⊢ M ↾ R ≤r M ↾ R'
Theorem: Matroid.Simple.exists_restriction_isSimplification_of_restriction
Proof state before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
R' : Set α
hM' : (M ↾ R').IsSimplification M
hRM' : R ⊆ (M ↾ R').E
⊢ M ↾ R ≤r M ↾ R'
Tactic:
exact ⟨R, hRM', by rw [restrict_restrict_eq _ (show R ⊆ R' from hRM')]⟩
Proof state after:
no goals
Theorem: Matroid.Simple.exists_restriction_isSimplification_of_restriction
Proof state before:
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
R' : Set α
hM' : (M ↾ R').IsSimplification M
hRM' : R ⊆ (M ↾ R').E
⊢ M ↾ R = M ↾ R' ↾ R
Tactic:
rw [restrict_restrict_eq _ (show R ⊆ R' from hRM')]
Proof state after:
no goals
Theorem: Matroid.IsSimplification.repFun_injOn
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ InjOn (⇑h.repFun) N.E
Tactic:
apply Simple.repFun_injOn
Proof state after:
case h
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ (M ↾ N.E).Simple
Theorem: Matroid.IsSimplification.repFun_injOn
Proof state before:
case h
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ (M ↾ N.E).Simple
Tactic:
rw [h.restriction.eq_restrict]
Proof state after:
case h
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ N.Simple
Theorem: Matroid.IsSimplification.repFun_injOn
Proof state before:
case h
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ N.Simple
Tactic:
exact h.simple
Proof state after:
no goals
Theorem: Matroid.IsSimplification.eq_self_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ N = M ↔ M.Simple
Tactic:
refine ⟨fun h' ↦ h' ▸ h.simple, fun h' ↦ ?_⟩
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
h' : M.Simple
⊢ N = M
Theorem: Matroid.IsSimplification.eq_self_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
h' : M.Simple
⊢ N = M
Tactic:
obtain ⟨f, rfl⟩ := h
Proof state after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
h' : M.Simple
f : M.parallelClasses.RepFun
⊢ M ↾ ⇑f '' {e | M.Nonloop e} = M
Theorem: Matroid.IsSimplification.eq_self_iff
Proof state before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
h' : M.Simple
f : M.parallelClasses.RepFun
⊢ M ↾ ⇑f '' {e | M.Nonloop e} = M
Tactic:
rw [restrict_eq_self_iff, f.coeFun_eq_id_of_eq_discrete M.parallelClasses_eq_discrete, image_id,
  Loopless.ground_eq]
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 : α
⊢ N.IsSimplification M ↔ N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
Tactic:
refine ⟨fun h ↦ ⟨h.simple.loopless, h.restriction, fun e he ↦ ?_⟩, fun ⟨h, hr, h'⟩ ↦ ?_⟩
Proof state after:
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

case 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
h' : ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
⊢ N.IsSimplification M
Theorem: Matroid.isSimplification_iff
Proof state before:
case 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
h' : ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
⊢ N.IsSimplification M
Tactic:
choose f hf using h'
Proof state after:
case 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
⊢ N.IsSimplification M
Theorem: Matroid.isSimplification_iff
Proof state before:
case 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
⊢ N.IsSimplification M
Tactic:
refine ⟨Partition.RepFun.mk (fun x ↦ if hx : M.Nonloop x then f hx else x) ?_ ?_ ?_, ?_⟩
Proof state after:
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

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)

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

case refine_2.refine_4
α : 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
⊢ N =
    M ↾
      ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ?refine_2.refine_1,
            rel_apply_of_mem := ?refine_2.refine_2, apply_eq_of_rel := ?refine_2.refine_3 } ''
        {e | M.Nonloop e}
Theorem: Matroid.isSimplification_iff
Proof state before:
case refine_2.refine_4
α : 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
⊢ N =
    M ↾
      ⇑{ 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:
convert hr.eq_restrict.symm
Proof state after:
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