mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x ↦ x * m) '' N = N

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
⊢ (ofSimpleGraph G).toSimpleGraph ≃g G

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x ↦ x * m) '' N = N
⊢ N ∩ {m' | m' * m = m} = N

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
⊢ ∃ m, m * m = m

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
⊢ ∃ m ∈ s, m * m = m

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
⊢ Injective toFun

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
l : Subspace η α ι
x : η → α
i : ι
a : α
h : l.idxFun i = Sum.inl a
⊢ ↑l x i = a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
l : Subspace η α ι
x : η → α
i : ι
e : η
h : l.idxFun i = Sum.inr e
⊢ ↑l x i = x e

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η✝ : Type u_1
α✝ : Type u_2
ι✝ : Type u_3
κ✝ : Type u_4
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l✝ : Subspace η α ι
x : η → α
i✝ : ι
a : α
e✝ : η
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
e : η'
i : ι
⊢ l.idxFun i = Sum.inr (eη.symm e) ↔ Sum.map (⇑eα) (⇑eη) (l.idxFun (eι.symm (eι i))) = Sum.inr e

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
x : η' → α'
i : ι'
⊢ ↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type ?u.3
inst✝ : Semigroup M
U V W : Ultrafilter M
p : M → Prop
⊢ (∀ᶠ (x : M) in ↑(U * V * W), p x) ↔ ∀ᶠ (x : M) in ↑(U * (V * W)), p x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
e e' : Set α
H : Hypergraph α
he : e ∈ E(H)
he' : e' ∈ E(H)
⊢ e = e' ↔ ∀ x ∈ V(H), x ∈ e ↔ x ∈ e'

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
x y : α
H : Hypergraph α
h : H.Adj x y
⊢ H.Adj y x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι' → α') → κ
c : κ
⊢ ∀ (a : η' → α'),
    (C fun x ↦ eα (Sum.elim id (⇑eα.symm ∘ a ∘ ⇑eη) (l.idxFun (eι.symm x)))) = c ↔
      C (⇑eα ∘ ↑l ((eη.arrowCongr eα).symm a) ∘ ⇑eι.symm) = c

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
e f : Set α
H : Hypergraph α
h : H.EAdj e f
⊢ ∃ x ∈ V(H), x ∈ e ∧ x ∈ f

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι' → α') → κ
⊢ IsMono C (l.reindex eη eα eι) ↔ IsMono (fun x ↦ C (⇑eα ∘ x ∘ ⇑eι.symm)) l

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
e f : Set α
H : Hypergraph α
h : H.EAdj e f
⊢ H.EAdj f e

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
e e' f✝ : Set α
H✝ H : Hypergraph α
f : α → β
⊢ ∀ ⦃e : Set β⦄, e ∈ image f '' E(H) → e ⊆ f '' V(H)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι → α) → κ
hl : IsMono C l
⊢ IsMono (fun x ↦ C (⇑eα.symm ∘ x ∘ ⇑eι)) (l.reindex eη eα eι)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
H : Hypergraph α
⊢ (H.image f).image g = H.image (g ∘ f)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
H : Hypergraph α
⊢ ⋃₀ E(H) = V(H) ↔ ∀ x ∈ V(H), ¬H.IsIsolated x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
e : Set α
H : Hypergraph α
⊢ H.IsLoop e ↔ e ∈ E(H) ∧ e.ncard = 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
x y : α✝
e e' f : Set α✝
H : Hypergraph α✝
α : Type u_4
⊢ ∀ ⦃e : Set α⦄, e ∈ ∅ → e ⊆ ∅

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
H : Hypergraph α
⊢ H ≠ ⊥ ↔ H.IsNonempty

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
H : Hypergraph α
⊢ V(H) = ∅ ∧ E(H) = ∅ ∨ V(H).Nonempty ∨ E(H).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
m : M
hm : m ∈ FP a
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
H : Hypergraph α
⊢ H = ⊥ ∨ H.IsNonempty

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
e e' f✝ : Set α
H : Hypergraph α
f : Set α
⊢ ∀ ⦃e : Set α⦄, e ∈ ∅ → e ⊆ f

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
⊢ Injective toFun

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
f : Set α
hf : f.Nonempty
⊢ (Hypergraph.trivialOn f).IsTrivial

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
H : Hypergraph α
h : H.IsTrivial
⊢ H.IsNonempty

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
l✝ : Line α ι
i✝ : ι
a x : α
l : Line α ι
x✝ : Unit
i : ι
hi : l.idxFun i = none
⊢ (l.idxFun i).elim (Sum.inr ()) Sum.inl = Sum.inr x✝

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
e : Set α
H : Hypergraph α
h : H.IsTrivial
⊢ e ∉ E(H)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x y : α
e e' f✝ : Set α
H : Hypergraph α
f : Set α
⊢ ∀ ⦃e : Set α⦄, e ∈ 𝒫 f → e ⊆ f

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
e f : Set α
⊢ e ∈ E(completeOn f) ↔ e ⊆ f

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
⊢ ↑l.toSubspaceUnit a = ↑l (a ())

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
e : Set α
H : Hypergraph α
h : H.IsComplete
⊢ e ∈ E(H) ↔ e ⊆ V(H)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_2
ι : Type u_3
κ : Type u_4
l : Line α ι
C : (ι → α) → κ
⊢ Subspace.IsMono C l.toSubspaceUnit ↔ IsMono C l

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
l✝ : Line α ι
i✝ : ι
a x : α
l : Line (η → α) ι
e : η
i : ι
hi : l.idxFun i = none
⊢ ((l.idxFun (i, e).1).elim (Sum.inr (i, e).2) fun f ↦ Sum.inl (f (i, e).2)) = Sum.inr e

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
H : Hypergraph α
h : H.IsComplete
⊢ ¬H.IsTrivial

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
⊢ ↑l.toSubspace a ie = ↑l a ie.1 ie.2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
l : Line (η → α) ι
C : (ι × η → α) → κ
⊢ Subspace.IsMono C l.toSubspace ↔
    IsMono
      (fun x ↦
        C fun x_1 ↦
          match x_1 with
          | (i, e) => x i e)
      l

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α✝ : Type u_2
ι✝ : Type u_3
κ✝ : Type u_4
l : Line α✝ ι✝
i : ι✝
a x : α✝
α : Type ?u.18
ι : Type ?u.23
κ : Type ?u.22
C : (ι → Option α) → κ
⊢ Inhabited (ColorFocused C)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α✝ : Type u_2
ι✝ : Type u_3
κ : Type u_4
l✝ : Line α✝ ι✝
i : ι✝
a x : α✝
α : Type ?u.19
α' : Type ?u.22
ι : Type ?u.18
f : α → α'
l : Line α ι
⊢ Option.map f (l.idxFun ⋯.choose) = none

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
ι : Type u_6
l : Line α ι
x : α
i : ι
h : l.idxFun i = none
⊢ ↑l x i = x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_2
ι : Type u_3
l : Line α ι
i : ι
a x : α
h : l.idxFun i = some a
⊢ ↑l x i = a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
α' : Type u_6
ι : Type u_7
f : α → α'
l : Line α ι
x : α
⊢ ↑(map f l) (f x) = f ∘ ↑l x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
⊢ ↑(vertical v l) x = Sum.elim v (↑l x)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
⊢ ↑(l.horizontal v) x = Sum.elim (↑l x) v

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
⊢ ↑(l.prod l') x = Sum.elim (↑l x) (↑l' x)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
ι : Type u_6
inst✝ : Nonempty ι
x : α
⊢ ↑(diagonal α ι) x = fun x_1 ↦ x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α α' : Type u
e : α ≃ α'
κ : Type (max v u)
x✝¹ : Finite κ
ι : Type
x✝ : Fintype ι
h : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (ι → α') → κ
l : Line α ι
c : κ
lc : ∀ (x : α), (fun v ↦ C (⇑e ∘ v)) (↑l x) = c
x : α
⊢ C (↑(map (⇑e) l) (e x)) = c

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: ⊢ ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ l, IsMono C l

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ＼ (M.E \ R) = M ↾ R

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M N : Matroid α
hNM : N ≤r M
⊢ N = M ＼ (M.E \ N.E)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M N : Matroid α
⊢ (∃ D ⊆ M.E, N = M ＼ D) → N ≤r M

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
⊢ M ＼ D = M ↔ Disjoint D M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ M ＼ {e} = M

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ ＼ D₂ = M ＼ (D₁ ∪ D₂)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ ＼ D₂ = M ＼ D₂ ＼ D₁

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
⊢ M ＼ (D ∩ M.E) = M ＼ D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : D₁ ∩ M.E = D₂ ∩ M.E
⊢ M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ = M ＼ D₂ ↔ D₁ ∩ M.E = D₂ ∩ M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ＼ ∅ = M

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ ＼ D₂ = M ＼ D₁ ＼ (D₂ \ D₁)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
s : Set M
hs : s ∈ U
⊢ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s} ∈ ↑U

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M N : Matroid α
X : Set α
h : N ≤r M
hX : Disjoint X N.E
⊢ N ≤r M ＼ X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
key : ∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M N : Matroid α
e : α
h : N ≤r M
he : e ∉ N.E
⊢ Disjoint {e} N.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D : Set α
⊢ (M ＼ D).Indep I ↔ M.Indep I ∧ Disjoint I D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
I : Set α
⊢ (M ＼ {e}).Indep I ↔ M.Indep I ∧ e ∉ I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
this : ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
⊢ FP (Stream'.corec elem succ ⟨s₀, sU⟩) ⊆ s₀

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ (M ＼ D).Dep X ↔ M.Dep X ∧ Disjoint X D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
B D : Set α
⊢ (M ＼ D).IsBase B ↔ M.IsBasis B (M.E \ D)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
⊢ (M ＼ D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
⊢ (M ＼ D).IsBasis' I X ↔ M.IsBasis' I (X \ D)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
h : M.IsBasis I X
hX : Disjoint X D
⊢ (M ＼ D).IsBasis I X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBase B ∧ Disjoint B D
⊢ B ⊆ M.E \ D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
⊢ (M ＼ D).IsBase B ↔ M.IsBase B ∧ Disjoint B D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
inst✝ : M.RankPos
hD : M.Coindep D
⊢ (M ＼ D).RankPos

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D S : Set α
hD : M.Coindep D
⊢ (M ＼ D).Spanning S ↔ M.Spanning S ∧ Disjoint S D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ (M ＼ D).IsLoop e ↔ M.IsLoop e ∧ e ∉ D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
⊢ (∃ l, IsMono C' l) → ∃ l, IsMono C l

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ (M ＼ D).IsNonloop e ↔ M.IsNonloop e ∧ e ∉ D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ↾ M.E \ M.loops = M ↾ {e | M.IsNonloop e}

Tactic:
compl_loops_eq

Goal state after:
α : Type u_1
M : Matroid α
⊢ M ↾ {e | M.IsNonloop e} = M ↾ {e | M.IsNonloop e}
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ＼ M.loops = M.removeLoops

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D C : Set α
⊢ (M ＼ D).IsCircuit C ↔ M.IsCircuit C ∧ Disjoint C D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ (M ＼ D).closure X = M.closure (X \ D) \ D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
hXD : Disjoint X D
⊢ (M ＼ D).closure X = M.closure X \ D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
⊢ (M ＼ D).loops = M.loops \ D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
e : α
M : Matroid α
D : Set α
⊢ (M ＼ D).IsColoop e ↔ e ∉ M.closure ((M.E \ D) \ {e}) ∧ e ∈ M.E ∧ e ∉ D

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
⊢ ∃ a, FP a ⊆ s₀

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
⊢ FP (Stream'.drop n a) ⊆ FP a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i : ℕ
⊢ a.get i ∈ FP a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ FP (Stream'.drop i a).tail (a.get j)

Tactic:
rcases Nat.exists_eq_add_of_le (Nat.succ_le_of_lt ij) with ⟨d, hd⟩

Goal state after:
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = i.succ + d
⊢ FP (Stream'.drop i a).tail (a.get j)
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s : Finset X
inst✝ : DecidableEq X
⊢ f ∈ prefixed s ↔ f.IsPrefix s

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : ↥s
⊢ ↑(↑f ↑x) < Fintype.card ↥s

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ a.get i * a.get j ∈ FP a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : Fin (Fintype.card ↥s)
⊢ Fintype.card ↥s ≤ Fintype.card X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : Fin (Fintype.card ↥s)
⊢ (Equiv.symm ↑f) ⟨↑n, ⋯⟩ ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : ↥s
⊢ (fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n, ⋯⟩, ⋯⟩) ((fun x ↦ ⟨↑(↑f ↑x), ⋯⟩) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : Fin (Fintype.card ↥s)
⊢ (fun x ↦ ⟨↑(↑f ↑x), ⋯⟩) ((fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n, ⋯⟩, ⋯⟩) n) = n

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : ↥sᶜ
⊢ ↑(↑f ↑x) - #s < Fintype.card ↥sᶜ

Tactic:
by

Goal state after: