mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: case inl
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e✝ : β
x✝ y✝ : α'
f : α → α'
G : Graph α β
e : β
x y : α
hxy : G.IsLink e x y
w : α
hzw : G.IsLink e x w
⊢ f x = f x ∨ f x = f w

pp: case inr
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e✝ : β
x✝ y✝ : α'
f : α → α'
G : Graph α β
e : β
x y : α
hxy : G.IsLink e x y
z : α
hzw : G.IsLink e z x
⊢ f x = f z ∨ f x = f x

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e✝ : β
x✝ y✝ : α'
f : α → α'
G : Graph α β
e : β
x y : α
hxy : G.IsLink e x y
w : α
hzw : G.IsLink e x w
⊢ f x = f x ∨ f x = f w

case inr
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e✝ : β
x✝ y✝ : α'
f : α → α'
G : Graph α β
e : β
x y : α
hxy : G.IsLink e x y
z : α
hzw : G.IsLink e z x
⊢ f x = f z ∨ f x = f x
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e : β
x y : α'
f : α → α'
G : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x y v w : α'⦄, Relation.Map (G.IsLink e) f f x y → Relation.Map (G.IsLink e) f f v w → x = v ∨ x = w

Tactic:
by
    rintro e - - - - ⟨x, y, hxy, rfl, rfl⟩ ⟨z, w, hzw, rfl, rfl⟩
    obtain rfl | rfl := hxy.left_eq_or_eq hzw <;> simp

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
x y : α'
f : α → α'
⊢ (map f G).Adj x y ↔ Relation.Map G.Adj f f x y

Tactic:
by
  simp only [Adj, map_isLink, map_apply]
  tauto

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

Goal state before:
pp: case hV
α : Type u_1
β : Type u_4
G : Graph α β
a : α
⊢ a ∈ V(map id G) ↔ a ∈ V(G)

pp: case h
α : Type u_1
β : Type u_4
G : Graph α β
a : β
b c : α
⊢ (map id G).IsLink a b c ↔ G.IsLink a b c

Tactic:
<;>

Goal state after:
case hV
α : Type u_1
β : Type u_4
G : Graph α β
a : α
⊢ a ∈ V(map id G) ↔ a ∈ V(G)

case h
α : Type u_1
β : Type u_4
G : Graph α β
a : β
b c : α
⊢ (map id G).IsLink a b c ↔ G.IsLink a b c
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: case hV
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
a : α''
⊢ a ∈ V(map f' (map f G)) ↔ a ∈ V(map (f' ∘ f) G)

pp: case h
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
a : β
b c : α''
⊢ (map f' (map f G)).IsLink a b c ↔ (map (f' ∘ f) G).IsLink a b c

Tactic:
<;>

Goal state after:
case hV
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
a : α''
⊢ a ∈ V(map f' (map f G)) ↔ a ∈ V(map (f' ∘ f) G)

case h
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
a : β
b c : α''
⊢ (map f' (map f G)).IsLink a b c ↔ (map (f' ∘ f) G).IsLink a b c
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: case refine_1
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
x✝³ : β
x✝² x✝¹ : α'
x✝ : (map f G).IsLink x✝³ x✝² x✝¹
w✝¹ w✝ : α
hvw : G.IsLink x✝³ w✝¹ w✝
left✝ : f w✝¹ = x✝²
right✝ : f w✝ = x✝¹
⊢ (map g G).IsLink x✝³ x✝² x✝¹

pp: case refine_2
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
x✝³ : β
x✝² x✝¹ : α'
x✝ : (map g G).IsLink x✝³ x✝² x✝¹
w✝¹ w✝ : α
hvw : G.IsLink x✝³ w✝¹ w✝
left✝ : g w✝¹ = x✝²
right✝ : g w✝ = x✝¹
⊢ (map f G).IsLink x✝³ x✝² x✝¹

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
x✝³ : β
x✝² x✝¹ : α'
x✝ : (map f G).IsLink x✝³ x✝² x✝¹
w✝¹ w✝ : α
hvw : G.IsLink x✝³ w✝¹ w✝
left✝ : f w✝¹ = x✝²
right✝ : f w✝ = x✝¹
⊢ (map g G).IsLink x✝³ x✝² x✝¹

case refine_2
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
x✝³ : β
x✝² x✝¹ : α'
x✝ : (map g G).IsLink x✝³ x✝² x✝¹
w✝¹ w✝ : α
hvw : G.IsLink x✝³ w✝¹ w✝
left✝ : g w✝¹ = x✝²
right✝ : g w✝ = x✝¹
⊢ (map f G).IsLink x✝³ x✝² x✝¹
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: case map_rel_iff'.refine_1
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
h : G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)
⊢ (ofSimpleGraph G).Adj ↑a✝ ↑b✝

pp: case map_rel_iff'.refine_2
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
x✝ : (ofSimpleGraph G).toSimpleGraph.Adj a✝ b✝
left✝ : a✝ ≠ b✝
h : (ofSimpleGraph G).Adj ↑a✝ ↑b✝
⊢ G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)

Tactic:
<;>

Goal state after:
case map_rel_iff'.refine_1
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
h : G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)
⊢ (ofSimpleGraph G).Adj ↑a✝ ↑b✝

case map_rel_iff'.refine_2
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
x✝ : (ofSimpleGraph G).toSimpleGraph.Adj a✝ b✝
left✝ : a✝ ≠ b✝
h : (ofSimpleGraph G).Adj ↑a✝ ↑b✝
⊢ G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: case map_rel_iff'.refine_1
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
⊢ G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝) → (ofSimpleGraph G).Adj ↑a✝ ↑b✝

pp: case map_rel_iff'.refine_2
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
x✝ : (ofSimpleGraph G).toSimpleGraph.Adj a✝ b✝
left✝ : a✝ ≠ b✝
⊢ (ofSimpleGraph G).Adj ↑a✝ ↑b✝ → G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)

Tactic:
<;>

Goal state after:
case map_rel_iff'.refine_1
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
⊢ G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝) → (ofSimpleGraph G).Adj ↑a✝ ↑b✝

case map_rel_iff'.refine_2
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
x✝ : (ofSimpleGraph G).toSimpleGraph.Adj a✝ b✝
left✝ : a✝ ≠ b✝
⊢ (ofSimpleGraph G).Adj ↑a✝ ↑b✝ → G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: case map_rel_iff'.refine_1
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
⊢ G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝) → G.Adj ↑a✝ ↑b✝

pp: case map_rel_iff'.refine_2
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
x✝ : (ofSimpleGraph G).toSimpleGraph.Adj a✝ b✝
left✝ : a✝ ≠ b✝
⊢ G.Adj ↑a✝ ↑b✝ → G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)

Tactic:
<;>

Goal state after:
case map_rel_iff'.refine_1
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
⊢ G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝) → G.Adj ↑a✝ ↑b✝

case map_rel_iff'.refine_2
α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
a✝ b✝ : ↑V(ofSimpleGraph G)
x✝ : (ofSimpleGraph G).toSimpleGraph.Adj a✝ b✝
left✝ : a✝ ≠ b✝
⊢ G.Adj ↑a✝ ↑b✝ → G.Adj ((Equiv.Set.univ α) a✝) ((Equiv.Set.univ α) b✝)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inl.inl
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
val✝ : α
hm : m.idxFun i = Sum.inl val✝
⊢ Sum.inl a = Sum.inl val✝

pp: case inl.inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
val✝ : η
hm : m.idxFun i = Sum.inr val✝
⊢ Sum.inl a = Sum.inr val✝

Tactic:
<;>

Goal state after:
case inl.inl
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
val✝ : α
hm : m.idxFun i = Sum.inl val✝
⊢ Sum.inl a = Sum.inl val✝

case inl.inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
val✝ : η
hm : m.idxFun i = Sum.inr val✝
⊢ Sum.inl a = Sum.inr val✝
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inl
η✝ : 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 : ι
val✝ : α
h : l.idxFun i = Sum.inl val✝
⊢ Sum.inl val✝ = Sum.inr (eη.symm e) ↔ Sum.map (⇑eα) (⇑eη) (l.idxFun (eι.symm (eι i))) = Sum.inr e

pp: case inr
η✝ : 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 : ι
val✝ : η
h : l.idxFun i = Sum.inr val✝
⊢ Sum.inr val✝ = Sum.inr (eη.symm e) ↔ Sum.map (⇑eα) (⇑eη) (l.idxFun (eι.symm (eι i))) = Sum.inr e

Tactic:
<;>

Goal state after:
case inl
η✝ : 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 : ι
val✝ : α
h : l.idxFun i = Sum.inl val✝
⊢ Sum.inl val✝ = Sum.inr (eη.symm e) ↔ Sum.map (⇑eα) (⇑eη) (l.idxFun (eι.symm (eι i))) = Sum.inr e

case inr
η✝ : 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 : ι
val✝ : η
h : l.idxFun i = Sum.inr val✝
⊢ Sum.inr val✝ = Sum.inr (eη.symm e) ↔ Sum.map (⇑eα) (⇑eη) (l.idxFun (eι.symm (eι i))) = Sum.inr e
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inl
η : 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 : ι'
val✝ : α
h : l.idxFun (eι.symm i) = Sum.inl val✝
⊢ ↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))

pp: case inr
η : 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 : ι'
val✝ : η
h : l.idxFun (eι.symm i) = Sum.inr val✝
⊢ ↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))

Tactic:
<;>

Goal state after:
case inl
η : 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 : ι'
val✝ : α
h : l.idxFun (eι.symm i) = Sum.inl val✝
⊢ ↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))

case inr
η : 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 : ι'
val✝ : η
h : l.idxFun (eι.symm i) = Sum.inr val✝
⊢ ↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: case vertexSet
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
H : Hypergraph α
x✝ : γ
⊢ x✝ ∈ V((H.image f).image g) ↔ x✝ ∈ V(H.image (g ∘ f))

pp: case edgeSet
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
H : Hypergraph α
x✝ : Set γ
⊢ x✝ ∈ E((H.image f).image g) ↔ x✝ ∈ E(H.image (g ∘ f))

Tactic:
<;>

Goal state after:
case vertexSet
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
H : Hypergraph α
x✝ : γ
⊢ x✝ ∈ V((H.image f).image g) ↔ x✝ ∈ V(H.image (g ∘ f))

case edgeSet
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
H : Hypergraph α
x✝ : Set γ
⊢ x✝ ∈ E((H.image f).image g) ↔ x✝ ∈ E(H.image (g ∘ f))
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_1.none
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : l.idxFun i = some a
hi : m.idxFun i = none
⊢ none = some a

pp: case refine_1.some
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : l.idxFun i = some a
val✝ : α
hi : m.idxFun i = some val✝
⊢ some val✝ = some a

Tactic:
<;>

Goal state after:
case refine_1.none
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : l.idxFun i = some a
hi : m.idxFun i = none
⊢ none = some a

case refine_1.some
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : l.idxFun i = some a
val✝ : α
hi : m.idxFun i = some val✝
⊢ some val✝ = some a
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_2.none
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : m.idxFun i = some a
hi : l.idxFun i = none
⊢ none = some a

pp: case refine_2.some
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : m.idxFun i = some a
val✝ : α
hi : l.idxFun i = some val✝
⊢ some val✝ = some a

Tactic:
<;>

Goal state after:
case refine_2.none
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : m.idxFun i = some a
hi : l.idxFun i = none
⊢ none = some a

case refine_2.some
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : m.idxFun i = some a
val✝ : α
hi : l.idxFun i = some val✝
⊢ some val✝ = some a
Module: Mathlib.Combinatorics.HalesJewett

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

pp: case some
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
val✝ : α
h : l.idxFun i = some val✝
⊢ ↑l.toSubspaceUnit a i = ↑l (a ()) i

Tactic:
<;>

Goal state after:
case none
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
h : l.idxFun i = none
⊢ ↑l.toSubspaceUnit a i = ↑l (a ()) i

case some
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
val✝ : α
h : l.idxFun i = some val✝
⊢ ↑l.toSubspaceUnit a i = ↑l (a ()) i
Module: Mathlib.Combinatorics.HalesJewett

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

pp: case some
η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
val✝ : η → α
h : l.idxFun ie.1 = some val✝
⊢ ↑l.toSubspace a ie = ↑l a ie.1 ie.2

Tactic:
<;>

Goal state after:
case none
η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
h : l.idxFun ie.1 = none
⊢ ↑l.toSubspace a ie = ↑l a ie.1 ie.2

case some
η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
val✝ : η → α
h : l.idxFun ie.1 = some val✝
⊢ ↑l.toSubspace a ie = ↑l a ie.1 ie.2
Module: Mathlib.Combinatorics.HalesJewett

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

pp: case inr
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
val✝ : ι'
⊢ ↑(vertical v l) x (Sum.inr val✝) = Sum.elim v (↑l x) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
val✝ : ι
⊢ ↑(vertical v l) x (Sum.inl val✝) = Sum.elim v (↑l x) (Sum.inl val✝)

case inr
α : Type u_5
ι : Type u_6
ι' : Type u_7
v : ι → α
l : Line α ι'
x : α
val✝ : ι'
⊢ ↑(vertical v l) x (Sum.inr val✝) = Sum.elim v (↑l x) (Sum.inr val✝)
Module: Mathlib.Combinatorics.HalesJewett

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

pp: case inr
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
val✝ : ι'
⊢ ↑(l.horizontal v) x (Sum.inr val✝) = Sum.elim (↑l x) v (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
val✝ : ι
⊢ ↑(l.horizontal v) x (Sum.inl val✝) = Sum.elim (↑l x) v (Sum.inl val✝)

case inr
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
val✝ : ι'
⊢ ↑(l.horizontal v) x (Sum.inr val✝) = Sum.elim (↑l x) v (Sum.inr val✝)
Module: Mathlib.Combinatorics.HalesJewett

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

pp: case inr
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
val✝ : ι'
⊢ ↑(l.prod l') x (Sum.inr val✝) = Sum.elim (↑l x) (↑l' x) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
val✝ : ι
⊢ ↑(l.prod l') x (Sum.inl val✝) = Sum.elim (↑l x) (↑l' x) (Sum.inl val✝)

case inr
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
val✝ : ι'
⊢ ↑(l.prod l') x (Sum.inr val✝) = Sum.elim (↑l x) (↑l' x) (Sum.inr val✝)
Module: Mathlib.Combinatorics.HalesJewett

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

Tactic:
by
    -- This deals with the degenerate case where `α` is empty.
    intro κ _
    by_cases h : Nonempty κ
    · refine ⟨Unit, inferInstance, fun C => ⟨default, Classical.arbitrary _, PEmpty.rec⟩⟩
    · exact ⟨Empty, inferInstance, fun C => (h ⟨C (Empty.rec)⟩).elim⟩

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case refine_2.htd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ ∀ (i : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (i + 1) a)} ⊆ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}

Tactic:
intro n U hU
      filter_upwards [hU]
      rw [← Stream'.drop_drop, ← Stream'.tail_eq_drop]
      exact FP.tail _

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:
obtain ⟨ι, _inst, hι⟩ := key (Fintype.card κ + 1)
      refine ⟨ι, _inst, fun C => (hι C).resolve_left ?_⟩
      rintro ⟨s, sr⟩
      apply Nat.not_succ_le_self (Fintype.card κ)
      rw [← Nat.add_one, ← sr, ← Multiset.card_map, ← Finset.card_mk]
      exact Finset.card_le_univ ⟨_, s.distinct_colors⟩

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
hx : x ∈ s
⊢ ↑({ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
            invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
            left_inv := ⋯, right_inv := ⋯ }
          x) <
      #s →
    x ∈ s

pp: case neg
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
hx : x ∉ s
⊢ ↑({ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
            invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
            left_inv := ⋯, right_inv := ⋯ }
          x) <
      #s →
    x ∈ s

Tactic:
<;>

Goal state after:
case pos
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
hx : x ∈ s
⊢ ↑({ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
            invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
            left_inv := ⋯, right_inv := ⋯ }
          x) <
      #s →
    x ∈ s

case neg
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
hx : x ∉ s
⊢ ↑({ toFun := fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s),
            invFun := fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩),
            left_inv := ⋯, right_inv := ⋯ }
          x) <
      #s →
    x ∈ s
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

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

Tactic:
← dual_ground,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
⊢ (M✶ ＼ (C ∩ M✶.E))✶ = M ／ C
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ M✶.Spanning (M.E \ I)

Tactic:
← dual_ground,

Goal state after:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ M✶.Spanning (M✶.E \ I)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : j = i
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)

Tactic:
apply le_trans degree_mul_le

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : j = i
⊢ m.toSyn (m.degree (b j) + m.degree ((Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∃ i, m.degree (b i) = 0
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
obtain ⟨i, hb0⟩ := hb'
    use Finsupp.single i ((hb i).unit⁻¹ • f), 0
    constructor
    · simp only [Finsupp.linearCombination_single, smul_eq_mul, add_zero]
      simp only [smul_mul_assoc, ← smul_eq_iff_eq_inv_smul, Units.smul_isUnit]
      nth_rewrite 2 [eq_C_of_degree_eq_zero hb0]
      rw [mul_comm, smul_eq_C_mul]
    constructor
    · intro j
      by_cases hj : j = i
      · apply le_trans degree_mul_le
        simp only [hj, hb0, Finsupp.single_eq_same, zero_add]
        apply le_of_eq
        simp only [EmbeddingLike.apply_eq_iff_eq]
        apply degree_smul_of_isRegular (Units.isRegular _)
      · simp only [Finsupp.single_eq_of_ne hj, mul_zero, degree_zero, map_zero]
        apply bot_le
    · simp

Goal state after: