internlm/Lean-Github huggingface dataset:
Theorem: Matroid.rFin.union_of_contract
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).rFin X
hC : M.rFin C
⊢ (M ／ C).er X + M.er C < ⊤
Tactic:
rw [← er_ne_top_iff] at hC hX
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).er X ≠ ⊤
hC : M.er C ≠ ⊤
⊢ (M ／ C).er X + M.er C < ⊤
Theorem: Matroid.rFin.union_of_contract
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).er X ≠ ⊤
hC : M.er C ≠ ⊤
⊢ (M ／ C).er X + M.er C < ⊤
Tactic:
rw [lt_top_iff_ne_top, Ne, WithTop.add_eq_top, not_or]
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).er X ≠ ⊤
hC : M.er C ≠ ⊤
⊢ ¬(M ／ C).er X = ⊤ ∧ ¬M.er C = ⊤
Theorem: Matroid.rFin.union_of_contract
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).er X ≠ ⊤
hC : M.er C ≠ ⊤
⊢ ¬(M ／ C).er X = ⊤ ∧ ¬M.er C = ⊤
Tactic:
exact ⟨hX, hC⟩
Proof state after:
no goals
Theorem: Matroid.rFin.contract_rFin_of_subset_union
Proof state before:
α : Type u_1
M N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
h : M.rFin Z
X C : Set α
hX : X ⊆ M.cl (Z ∪ C)
⊢ X \ C ⊆ (M ／ C).cl Z
Tactic:
rw [contract_cl_eq]
Proof state after:
α : Type u_1
M N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
h : M.rFin Z
X C : Set α
hX : X ⊆ M.cl (Z ∪ C)
⊢ X \ C ⊆ M.cl (Z ∪ C) \ C
Theorem: Matroid.rFin.contract_rFin_of_subset_union
Proof state before:
α : Type u_1
M N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
h : M.rFin Z
X C : Set α
hX : X ⊆ M.cl (Z ∪ C)
⊢ X \ C ⊆ M.cl (Z ∪ C) \ C
Tactic:
exact diff_subset_diff_left hX
Proof state after:
no goals
Theorem: Matroid.Minor.erk_le
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
⊢ N.erk ≤ M.erk
Tactic:
obtain ⟨C, D, -, -, -, rfl⟩ := h
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
I J C✝ D✝ X Y Z : Set α
e f : α
C D : Set α
⊢ (M ／ C ＼ D).erk ≤ M.erk
Theorem: Matroid.Minor.erk_le
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
I J C✝ D✝ X Y Z : Set α
e f : α
C D : Set α
⊢ (M ／ C ＼ D).erk ≤ M.erk
Tactic:
rw [← er_univ_eq, ← er_univ_eq, delete_er_eq']
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
I J C✝ D✝ X Y Z : Set α
e f : α
C D : Set α
⊢ (M ／ C).er (univ \ D) ≤ M.er univ
Theorem: Matroid.Minor.erk_le
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
I J C✝ D✝ X Y Z : Set α
e f : α
C D : Set α
⊢ (M ／ C).er (univ \ D) ≤ M.er univ
Tactic:
exact (M.er_contract_le_er _ _).trans (M.er_mono diff_subset)
Proof state after:
no goals
Theorem: Matroid.Minor.rk_le
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
⊢ N.rk ≤ M.rk
Tactic:
have hle := h.erk_le
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : N.erk ≤ M.erk
⊢ N.rk ≤ M.rk
Theorem: Matroid.Minor.rk_le
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : N.erk ≤ M.erk
⊢ N.rk ≤ M.rk
Tactic:
have := h.finiteRk
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : N.erk ≤ M.erk
this : N.FiniteRk
⊢ N.rk ≤ M.rk
Theorem: Matroid.Minor.rk_le
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : N.erk ≤ M.erk
this : N.FiniteRk
⊢ N.rk ≤ M.rk
Tactic:
rw [← M.coe_rk_eq, ← N.coe_rk_eq] at hle
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : ↑N.rk ≤ ↑M.rk
this : N.FiniteRk
⊢ N.rk ≤ M.rk
Theorem: Matroid.Minor.rk_le
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
h : N ≤m M
inst✝ : M.FiniteRk
hle : ↑N.rk ≤ ↑M.rk
this : N.FiniteRk
⊢ N.rk ≤ M.rk
Tactic:
exact WithTop.coe_le_coe.1 hle
Proof state after:
no goals
Theorem: Matroid.delete_r_eq'
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
D X : Set α
⊢ (M ＼ D).r X = M.r (X \ D)
Tactic:
rw [r, r, delete_er_eq']
Proof state after:
no goals
Theorem: Matroid.delete_r_eq_of_disjoint
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hDX : Disjoint X D
⊢ (M ＼ D).r X = M.r X
Tactic:
rw [delete_r_eq', hDX.sdiff_eq_left]
Proof state after:
no goals
Theorem: Matroid.delete_elem_r_eq
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
heX : e ∉ X
⊢ (M ＼ e).r X = M.r X
Tactic:
rw [deleteElem, delete_r_eq', diff_singleton_eq_self heX]
Proof state after:
no goals
Theorem: Matroid.restrict_r_eq'
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
M : Matroid α
R X : Set α
⊢ (M ↾ R).r X = M.r (X ∩ R)
Tactic:
rw [r, restrict_er_eq', r]
Proof state after:
no goals
Theorem: Matroid.restrict_r_eq
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
R : Set α
hXR : X ⊆ R
⊢ (M ↾ R).r X = M.r X
Tactic:
rw [r, M.restrict_er_eq hXR, r]
Proof state after:
no goals
Theorem: Matroid.contract_r_add_eq
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
inst✝ : M.FiniteRk
C X : Set α
⊢ (M ／ C).r X + M.r C = M.r (X ∪ C)
Tactic:
simp_rw [← Nat.cast_inj (R := ℕ∞), Nat.cast_add, coe_r_eq, ← relRank_add_er_eq, relRank]
Proof state after:
no goals
Theorem: Matroid.contract_r_cast_int_Eq
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
inst✝ : M.FiniteRk
C X : Set α
⊢ ↑((M ／ C).r X) = ↑(M.r (X ∪ C)) - ↑(M.r C)
Tactic:
rw [← contract_r_add_eq]
Proof state after:
α : Type u_1
M✝ N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
inst✝ : M.FiniteRk
C X : Set α
⊢ ↑((M ／ C).r X) = ↑((M ／ C).r X + M.r C) - ↑(M.r C)
Theorem: Matroid.contract_r_cast_int_Eq
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
inst✝ : M.FiniteRk
C X : Set α
⊢ ↑((M ／ C).r X) = ↑((M ／ C).r X + M.r C) - ↑(M.r C)
Tactic:
exact eq_sub_of_add_eq rfl
Proof state after:
no goals
Theorem: Matroid.Nonloop.contract_r_add_one_eq
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
inst✝ : M.FiniteRk
he : M.Nonloop e
⊢ (M ／ e).r X + 1 = M.r (insert e X)
Tactic:
rw [← union_singleton, ← contract_r_add_eq, he.r_eq, contract_elem]
Proof state after:
no goals
Theorem: Matroid.Nonloop.contract_r_cast_int_eq
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
inst✝ : M.FiniteRk
he : M.Nonloop e
⊢ ↑((M ／ e).r X) = ↑(M.r (insert e X)) - 1
Tactic:
rw [← he.contract_r_add_one_eq]
Proof state after:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
inst✝ : M.FiniteRk
he : M.Nonloop e
⊢ ↑((M ／ e).r X) = ↑((M ／ e).r X + 1) - 1
Theorem: Matroid.Nonloop.contract_r_cast_int_eq
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
inst✝ : M.FiniteRk
he : M.Nonloop e
⊢ ↑((M ／ e).r X) = ↑((M ／ e).r X + 1) - 1
Tactic:
exact eq_sub_of_add_eq rfl
Proof state after:
no goals
Theorem: vecMul_eq_sum
Proof state before:
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : Semiring R
inst✝ : Fintype m
M : Matrix m n R
x : m → R
⊢ x ᵥ* M = ∑ i : m, x i • M i
Tactic:
ext j
Proof state after:
case h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : Semiring R
inst✝ : Fintype m
M : Matrix m n R
x : m → R
j : n
⊢ (x ᵥ* M) j = (∑ i : m, x i • M i) j
Theorem: vecMul_eq_sum
Proof state before:
case h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : Semiring R
inst✝ : Fintype m
M : Matrix m n R
x : m → R
j : n
⊢ (x ᵥ* M) j = (∑ i : m, x i • M i) j
Tactic:
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
Proof state after:
case h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : Semiring R
inst✝ : Fintype m
M : Matrix m n R
x : m → R
j : n
⊢ (x ᵥ* M) j = ∑ x_1 : m, x x_1 * M x_1 j
Theorem: vecMul_eq_sum
Proof state before:
case h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : Semiring R
inst✝ : Fintype m
M : Matrix m n R
x : m → R
j : n
⊢ (x ᵥ* M) j = ∑ x_1 : m, x x_1 * M x_1 j
Tactic:
rfl
Proof state after:
no goals
Theorem: Matrix.vecMulLinear_injective_iff
Proof state before:
R✝ : Type u_1
m : Type u_2
n : Type u_3
inst✝² : Semiring R✝
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Fintype m
M : Matrix m n R
⊢ Function.Injective ⇑M.vecMulLinear ↔ LinearIndependent R fun i => M i
Tactic:
rw [← vecMul_injective_iff]
Proof state after:
R✝ : Type u_1
m : Type u_2
n : Type u_3
inst✝² : Semiring R✝
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Fintype m
M : Matrix m n R
⊢ Function.Injective ⇑M.vecMulLinear ↔ Function.Injective fun v => v ᵥ* fun i => M i
Theorem: Matrix.vecMulLinear_injective_iff
Proof state before:
R✝ : Type u_1
m : Type u_2
n : Type u_3
inst✝² : Semiring R✝
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Fintype m
M : Matrix m n R
⊢ Function.Injective ⇑M.vecMulLinear ↔ Function.Injective fun v => v ᵥ* fun i => M i
Tactic:
rfl
Proof state after:
no goals
Theorem: mulVec_eq_sum
Proof state before:
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : CommRing R
M✝ : Matrix m n R
inst✝ : Fintype n
M : Matrix m n R
x : n → R
⊢ M *ᵥ x = ∑ i : n, x i • fun x => M x i
Tactic:
ext j
Proof state after:
case h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : CommRing R
M✝ : Matrix m n R
inst✝ : Fintype n
M : Matrix m n R
x : n → R
j : m
⊢ (M *ᵥ x) j = (∑ i : n, x i • fun x => M x i) j
Theorem: mulVec_eq_sum
Proof state before:
case h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : CommRing R
M✝ : Matrix m n R
inst✝ : Fintype n
M : Matrix m n R
x : n → R
j : m
⊢ (M *ᵥ x) j = (∑ i : n, x i • fun x => M x i) j
Tactic:
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, mul_comm]
Proof state after:
case h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : CommRing R
M✝ : Matrix m n R
inst✝ : Fintype n
M : Matrix m n R
x : n → R
j : m
⊢ (M *ᵥ x) j = ∑ x_1 : n, M j x_1 * x x_1
Theorem: mulVec_eq_sum
Proof state before:
case h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : CommRing R
M✝ : Matrix m n R
inst✝ : Fintype n
M : Matrix m n R
x : n → R
j : m
⊢ (M *ᵥ x) j = ∑ x_1 : n, M j x_1 * x x_1
Tactic:
rfl
Proof state after:
no goals
Theorem: Matrix.mulVecLin_injective_iff
Proof state before:
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : CommRing R
M : Matrix m n R
inst✝ : Fintype n
⊢ Function.Injective ⇑M.mulVecLin ↔ LinearIndependent R fun i => Mᵀ i
Tactic:
rw [← vecMulLinear_transpose, vecMulLinear_injective_iff]
Proof state after:
no goals
Theorem: mem_maximals_iff_forall_insert
Proof state before:
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
s : Set α
⊢ s ∈ maximals (fun x x_1 => x ⊆ x_1) {t | P t} ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)
Tactic:
simp only [mem_maximals_iff, mem_setOf_eq, and_congr_right_iff]
Proof state after:
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
s : Set α
⊢ P s → ((∀ ⦃y : Set α⦄, P y → s ⊆ y → s = y) ↔ ∀ x ∉ s, ¬P (insert x s))
Theorem: mem_maximals_iff_forall_insert
Proof state before:
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
s : Set α
⊢ P s → ((∀ ⦃y : Set α⦄, P y → s ⊆ y → s = y) ↔ ∀ x ∉ s, ¬P (insert x s))
Tactic:
refine fun _ ↦ ⟨fun h x hx hxs ↦ hx ?_, fun h t ht hst ↦ hst.antisymm fun x hxt ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → s ⊆ y → s = y
x : α
hx : x ∉ s
hxs : P (insert x s)
⊢ x ∈ s

case refine_2
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
s : Set α
x✝ : P s
h : ∀ x ∉ s, ¬P (insert x s)
t : Set α
ht : P t
hst : s ⊆ t
x : α
hxt : x ∈ t
⊢ x ∈ s
Theorem: mem_maximals_iff_forall_insert
Proof state before:
case refine_2
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
s : Set α
x✝ : P s
h : ∀ x ∉ s, ¬P (insert x s)
t : Set α
ht : P t
hst : s ⊆ t
x : α
hxt : x ∈ t
⊢ x ∈ s
Tactic:
exact by_contra fun hxs ↦ h x hxs (hP ht (insert_subset hxt hst))
Proof state after:
no goals
Theorem: mem_maximals_iff_forall_insert
Proof state before:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → s ⊆ y → s = y
x : α
hx : x ∉ s
hxs : P (insert x s)
⊢ x ∈ s
Tactic:
rw [h hxs (subset_insert _ _)]
Proof state after:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → s ⊆ y → s = y
x : α
hx : x ∉ s
hxs : P (insert x s)
⊢ x ∈ insert x s
Theorem: mem_maximals_iff_forall_insert
Proof state before:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → s ⊆ y → s = y
x : α
hx : x ∉ s
hxs : P (insert x s)
⊢ x ∈ insert x s
Tactic:
apply mem_insert
Proof state after:
no goals
Theorem: mem_minimals_iff_forall_diff_singleton
Proof state before:
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
⊢ s ∈ minimals (fun x x_1 => x ⊆ x_1) {t | P t} ↔ P s ∧ ∀ x ∈ s, ¬P (s \ {x})
Tactic:
simp only [mem_minimals_iff, mem_setOf_eq, and_congr_right_iff]
Proof state after:
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
⊢ P s → ((∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y) ↔ ∀ x ∈ s, ¬P (s \ {x}))
Theorem: mem_minimals_iff_forall_diff_singleton
Proof state before:
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
⊢ P s → ((∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y) ↔ ∀ x ∈ s, ¬P (s \ {x}))
Tactic:
refine fun _ ↦ ⟨fun h x hx hxs ↦ ?_, fun h t ht hst ↦ Eq.symm <| hst.antisymm (fun x hxs ↦ ?_)⟩
Proof state after:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y
x : α
hx : x ∈ s
hxs : P (s \ {x})
⊢ False

case refine_2
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ x ∈ s, ¬P (s \ {x})
t : Set α
ht : P t
hst : t ⊆ s
x : α
hxs : x ∈ s
⊢ x ∈ t
Theorem: mem_minimals_iff_forall_diff_singleton
Proof state before:
case refine_2
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ x ∈ s, ¬P (s \ {x})
t : Set α
ht : P t
hst : t ⊆ s
x : α
hxs : x ∈ s
⊢ x ∈ t
Tactic:
exact by_contra fun hxt ↦ h x hxs (hP ht (subset_diff_singleton hst hxt))
Proof state after:
no goals
Theorem: mem_minimals_iff_forall_diff_singleton
Proof state before:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y
x : α
hx : x ∈ s
hxs : P (s \ {x})
⊢ False
Tactic:
rw [(h hxs diff_subset)] at hx
Proof state after:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y
x : α
hx : x ∈ s \ {x}
hxs : P (s \ {x})
⊢ False
Theorem: mem_minimals_iff_forall_diff_singleton
Proof state before:
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y
x : α
hx : x ∈ s \ {x}
hxs : P (s \ {x})
⊢ False
Tactic:
simp at hx
Proof state after:
no goals
Theorem: Matroid.IsoRestr.exists_restr_iso
Proof state before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
I : Set ↑N.E
⊢ N.Indep ↑I ↔ (M ↾ range (val ∘ ⇑i)).Indep ↑(⇑(Equiv.ofInjective (fun y => (val ∘ ⇑i) y) ⋯) '' I)
Tactic:
simp only [← i.indep_image_iff, restrict_ground_eq, comp_apply, Equiv.ofInjective_apply,
  restrict_indep_iff, image_subset_iff, Subtype.coe_preimage_self, subset_univ, and_true]
Proof state after:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
I : Set ↑N.E
⊢ M.Indep ↑(⇑i '' I) ↔ M.Indep ((fun a => ↑a) '' ((fun a => (Equiv.ofInjective (fun y => ↑(i y)) ⋯) a) '' I))
Theorem: Matroid.IsoRestr.exists_restr_iso
Proof state before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
I : Set ↑N.E
⊢ M.Indep ↑(⇑i '' I) ↔ M.Indep ((fun a => ↑a) '' ((fun a => (Equiv.ofInjective (fun y => ↑(i y)) ⋯) a) '' I))
Tactic:
simp only [image_image]
Proof state after:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
I : Set ↑N.E
⊢ M.Indep ((fun x => ↑(i x)) '' I) ↔ M.Indep ((fun x => ↑((Equiv.ofInjective (fun y => ↑(i y)) ⋯) x)) '' I)
Theorem: Matroid.IsoRestr.exists_restr_iso
Proof state before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
I : Set ↑N.E
⊢ M.Indep ((fun x => ↑(i x)) '' I) ↔ M.Indep ((fun x => ↑((Equiv.ofInjective (fun y => ↑(i y)) ⋯) x)) '' I)
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.IsoRestr.exists_restr_iso
Proof state before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
⊢ range (val ∘ ⇑i) ⊆ M.E
Tactic:
simp [range_comp]
Proof state after:
no goals
Theorem: Matroid.IsoMinor.exists_iso
Proof state before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
⊢ ∃ M₀, ∃ (hM₀ : M₀ ≤m M), ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x
Tactic:
obtain ⟨M₀, hM₀, hE, h⟩ := i.exists_minor
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
⊢ ∃ M₀, ∃ (hM₀ : M₀ ≤m M), ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x
Theorem: Matroid.IsoMinor.exists_iso
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
⊢ ∃ M₀, ∃ (hM₀ : M₀ ≤m M), ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x
Tactic:
refine ⟨M₀, hM₀,  ?_⟩
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
⊢ ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x
Theorem: Matroid.IsoMinor.exists_iso
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
⊢ ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x
Tactic:
let e := Equiv.ofInjective _ (Subtype.val_injective.comp (EmbeddingLike.injective i))
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
e : ↑N.E ≃ ↑(range (val ∘ ⇑i)) := Equiv.ofInjective (val ∘ ⇑i) ⋯
⊢ ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x
Theorem: Matroid.IsoMinor.exists_iso
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
e : ↑N.E ≃ ↑(range (val ∘ ⇑i)) := Equiv.ofInjective (val ∘ ⇑i) ⋯
⊢ ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x
Tactic:
exact ⟨Iso.mk (e.trans (Equiv.setCongr (by simp [hE, range_comp])))
  fun _ ↦ by simp [h, image_image, e], fun ⟨x,hx⟩ ↦ rfl⟩
Proof state after:
no goals
Theorem: Matroid.IsoMinor.exists_iso
Proof state before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
e : ↑N.E ≃ ↑(range (val ∘ ⇑i)) := Equiv.ofInjective (val ∘ ⇑i) ⋯
⊢ range (val ∘ ⇑i) = M₀.E
Tactic:
simp [hE, range_comp]
Proof state after:
no goals
Theorem: Matroid.IsoMinor.exists_iso
Proof state before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
e : ↑N.E ≃ ↑(range (val ∘ ⇑i)) := Equiv.ofInjective (val ∘ ⇑i) ⋯
x✝ : Set ↑N.E
⊢ N.Indep ↑x✝ ↔ M₀.Indep ↑(⇑(e.trans (Equiv.setCongr ⋯)) '' x✝)
Tactic:
simp [h, image_image, e]
Proof state after:
no goals
Theorem: Matroid.IsoMinor.erk_le
Proof state before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
e : N ≤i M
⊢ N.erk ≤ M.erk
Tactic:
obtain ⟨M₀, hM₀, i, -⟩ := e.exists_iso
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
e : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
i : N ≂ M₀
⊢ N.erk ≤ M.erk
Theorem: Matroid.IsoMinor.erk_le
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
e : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
i : N ≂ M₀
⊢ N.erk ≤ M.erk
Tactic:
exact i.erk_eq.trans_le hM₀.erk_le
Proof state after:
no goals
Theorem: Matroid.IsoMinor.rk_le
Proof state before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
e : N ≤i M
inst✝ : M.FiniteRk
⊢ N.rk ≤ M.rk
Tactic:
obtain ⟨M₀, hM₀, i, -⟩ := e.exists_iso
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
e : N ≤i M
inst✝ : M.FiniteRk
M₀ : Matroid α
hM₀ : M₀ ≤m M
i : N ≂ M₀
⊢ N.rk ≤ M.rk
Theorem: Matroid.IsoMinor.rk_le
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
e : N ≤i M
inst✝ : M.FiniteRk
M₀ : Matroid α
hM₀ : M₀ ≤m M
i : N ≂ M₀
⊢ N.rk ≤ M.rk
Tactic:
exact i.rk_eq.trans_le hM₀.rk_le
Proof state after:
no goals
Theorem: biUnion_insert_eq
Proof state before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
X : Set α
hX : X.Nonempty
Y : Set α
⊢ ⋃ x ∈ X, insert x Y = X ∪ Y
Tactic:
have := hX.to_subtype
Proof state after:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
X : Set α
hX : X.Nonempty
Y : Set α
this : Nonempty ↑X
⊢ ⋃ x ∈ X, insert x Y = X ∪ Y
Theorem: biUnion_insert_eq
Proof state before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
X : Set α
hX : X.Nonempty
Y : Set α
this : Nonempty ↑X
⊢ ⋃ x ∈ X, insert x Y = X ∪ Y
Tactic:
simp_rw [← singleton_union, biUnion_eq_iUnion, ← iUnion_union, iUnion_singleton_eq_range,
  Subtype.range_coe_subtype, setOf_mem_eq]
Proof state after:
no goals
Theorem: Equiv.exists_bijOn
Proof state before:
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
⊢ ∃ f, BijOn f s t ∧ ∀ (x : ↑s), ↑(e x) = f ↑x
Tactic:
use fun x ↦ if hx : x ∈ s then e ⟨x,hx⟩ else Classical.arbitrary β
Proof state after:
case h
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
⊢ BijOn (fun x => if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) s t ∧
    ∀ (x : ↑s), ↑(e x) = if hx : ↑x ∈ s then ↑(e ⟨↑x, hx⟩) else Classical.arbitrary β
Theorem: Equiv.exists_bijOn
Proof state before:
case h
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
⊢ BijOn (fun x => if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) s t ∧
    ∀ (x : ↑s), ↑(e x) = if hx : ↑x ∈ s then ↑(e ⟨↑x, hx⟩) else Classical.arbitrary β
Tactic:
refine ⟨BijOn.mk (fun x hx ↦ ?_) (fun x hx y hy hxy ↦ ?_) (fun y hy ↦ ⟨e.symm ⟨y, hy⟩, by simp⟩),
  by simp⟩
Proof state after:
case h.refine_1
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
⊢ (if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) ∈ t

case h.refine_2
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy :
  (if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) =
    if hx : y ∈ s then ↑(e ⟨y, hx⟩) else Classical.arbitrary β
⊢ x = y