mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hbx : x = b
⊢ w₂ ≠ x

pp: case neg
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hbx : ¬x = b
⊢ w₂ ≠ x

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hbx : x = b
⊢ w₂ ≠ x

case neg
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hbx : ¬x = b
⊢ w₂ ≠ x
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case neg.inl
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvv' : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
hl : G.Adj v w
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

pp: case neg.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvv' : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
<;>

Goal state after:
case neg.inl
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvv' : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
hl : G.Adj v w
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

case neg.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvv' : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case inl
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v u : V
ha : v ≠ u ∧ ¬G.Adj v u
hne : v ≠ u
⊢ ¬G.Adj v u ∧ ¬G.Adj u u

pp: case inr
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
w u : V
ha : u ≠ w ∧ ¬G.Adj u w
hne : u ≠ w
⊢ ¬G.Adj u u ∧ ¬G.Adj w u

Tactic:
<;>

Goal state after:
case inl
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v u : V
ha : v ≠ u ∧ ¬G.Adj v u
hne : v ≠ u
⊢ ¬G.Adj v u ∧ ¬G.Adj u u

case inr
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
w u : V
ha : u ≠ w ∧ ¬G.Adj u w
hne : u ≠ w
⊢ ¬G.Adj u u ∧ ¬G.Adj w u
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case pos
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : G.Adj v w
⊢ ↑(Fintype.card ↑(G.commonNeighbors v w)) =
    (k • 0 + ℓ • if G.Adj v w then 1 else 0) + μ • if ¬False ∧ ¬G.Adj v w then 1 else 0

pp: case neg
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : ¬G.Adj v w
⊢ ↑(Fintype.card ↑(G.commonNeighbors v w)) =
    (k • 0 + ℓ • if G.Adj v w then 1 else 0) + μ • if ¬False ∧ ¬G.Adj v w then 1 else 0

Tactic:
<;>

Goal state after:
case pos
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : G.Adj v w
⊢ ↑(Fintype.card ↑(G.commonNeighbors v w)) =
    (k • 0 + ℓ • if G.Adj v w then 1 else 0) + μ • if ¬False ∧ ¬G.Adj v w then 1 else 0

case neg
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : ¬G.Adj v w
⊢ ↑(Fintype.card ↑(G.commonNeighbors v w)) =
    (k • 0 + ℓ • if G.Adj v w then 1 else 0) + μ • if ¬False ∧ ¬G.Adj v w then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case h
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
i : α
a✝ : i ∈ W
⊢ G.minDegree ≤ G.degree i

pp: case h₁
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := ⋯
W : Finset α := ⋯
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
x : α
a✝ : x ∈ s ∩ t
⊢ G.minDegree ≤ G.degree x

Tactic:
<;>

Goal state after:
case h
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
i : α
a✝ : i ∈ W
⊢ G.minDegree ≤ G.degree i

case h₁
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := ⋯
W : Finset α := ⋯
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
x : α
a✝ : x ∈ s ∩ t
⊢ G.minDegree ≤ G.degree x
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
he : e ∈ p.edges
⊢ List.count e p.edges ≤ 1

pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
he : e ∉ p.edges
⊢ List.count e p.edges ≤ 1

Tactic:
· exact (h e (edges_subset_edgeSet _ he)).le

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
he : e ∉ p.edges
⊢ List.count e p.edges ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r✝ : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun H ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
⊢ False

Tactic:
have hn : ¬ H.IsCompleteMultipartite := fun hc ↦ hnotcol <| hc.colorable_of_cliqueFree hmcf.1

Goal state after:
α : Type u_1
G : SimpleGraph α
r✝ : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun H ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this✝ : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
this : 1 < (Set.univ \ t).encard
a b : V
left✝¹ : a ∈ Set.univ \ t
left✝ : b ∈ Set.univ \ t
hne : a ≠ b
⊢ (completeGraph V).Adj a b

Tactic:
by simp [hne]

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: case mp
μ ν : YoungDiagram
⊢ μ.transpose = ν → μ = ν.transpose

pp: case mpr
μ ν : YoungDiagram
⊢ μ = ν.transpose → μ.transpose = ν

Tactic:
<;>

Goal state after:
case mp
μ ν : YoungDiagram
⊢ μ.transpose = ν → μ = ν.transpose

case mpr
μ ν : YoungDiagram
⊢ μ = ν.transpose → μ.transpose = ν
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: case e'_3
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ μ.colLen j2 = μ.transpose.rowLen j2

pp: case e'_4
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ μ.colLen j1 = μ.transpose.rowLen j1

Tactic:
<;>

Goal state after:
case e'_3
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ μ.colLen j2 = μ.transpose.rowLen j2

case e'_4
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ μ.colLen j1 = μ.transpose.rowLen j1
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: case nil
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens [] ↔ ∃ (h : c.1 < [].length), c.2 < [][c.1]

pp: case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens (head✝ :: tail✝) ↔ ∃ (h : c.1 < (head✝ :: tail✝).length), c.2 < (head✝ :: tail✝)[c.1]

Tactic:
<;>

Goal state after:
case nil
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens [] ↔ ∃ (h : c.1 < [].length), c.2 < [][c.1]

case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens (head✝ :: tail✝) ↔ ∃ (h : c.1 < (head✝ :: tail✝).length), c.2 < (head✝ :: tail✝)[c.1]
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: case cons.zero
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
snd✝ : ℕ
⊢ (0, snd✝) ∈
      {0} ×ˢ Finset.range head✝ ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail✝) ↔
    ∃ (h : (0, snd✝).1 < (head✝ :: tail✝).length), (0, snd✝).2 < (head✝ :: tail✝)[(0, snd✝).1]

pp: case cons.succ
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
snd✝ n✝ : ℕ
⊢ (n✝ + 1, snd✝) ∈
      {0} ×ˢ Finset.range head✝ ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail✝) ↔
    ∃ (h : (n✝ + 1, snd✝).1 < (head✝ :: tail✝).length), (n✝ + 1, snd✝).2 < (head✝ :: tail✝)[(n✝ + 1, snd✝).1]

Tactic:
<;>

Goal state after:
case cons.zero
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
snd✝ : ℕ
⊢ (0, snd✝) ∈
      {0} ×ˢ Finset.range head✝ ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail✝) ↔
    ∃ (h : (0, snd✝).1 < (head✝ :: tail✝).length), (0, snd✝).2 < (head✝ :: tail✝)[(0, snd✝).1]

case cons.succ
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
snd✝ n✝ : ℕ
⊢ (n✝ + 1, snd✝) ∈
      {0} ×ˢ Finset.range head✝ ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail✝) ↔
    ∃ (h : (n✝ + 1, snd✝).1 < (head✝ :: tail✝).length), (n✝ + 1, snd✝).2 < (head✝ :: tail✝)[(n✝ + 1, snd✝).1]
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ x ∈ g • pt ↔ g⁻¹ • x ∈ pt

Tactic:
by
  simp_rw [← mem_coe, coe_smul, Set.mem_smul_set_iff_inv_smul_mem]

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case zero
⊢ Nat.casesOn 0 0 id = Nat.pred 0

pp: case succ
n✝ : ℕ
⊢ Nat.casesOn (n✝ + 1) 0 id = (n✝ + 1).pred

Tactic:
<;>

Goal state after:
case zero
⊢ Nat.casesOn 0 0 id = Nat.pred 0

case succ
n✝ : ℕ
⊢ Nat.casesOn (n✝ + 1) 0 id = (n✝ + 1).pred
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case zero
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH + 1) 0 = (unpair p).1 + 0

pp: case succ
p n✝ : ℕ
a✝ : Nat.rec (unpair p).1 (fun y IH ↦ IH + 1) n✝ = (unpair p).1 + n✝
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH + 1) (n✝ + 1) = (unpair p).1 + (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH + 1) 0 = (unpair p).1 + 0

case succ
p n✝ : ℕ
a✝ : Nat.rec (unpair p).1 (fun y IH ↦ IH + 1) n✝ = (unpair p).1 + n✝
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH + 1) (n✝ + 1) = (unpair p).1 + (n✝ + 1)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case zero
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) 0 = (unpair p).1 - 0

pp: case succ
p n✝ : ℕ
a✝ : Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) n✝ = (unpair p).1 - n✝
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) (n✝ + 1) = (unpair p).1 - (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) 0 = (unpair p).1 - 0

case succ
p n✝ : ℕ
a✝ : Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) n✝ = (unpair p).1 - n✝
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) (n✝ + 1) = (unpair p).1 - (n✝ + 1)
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case zero
⊢ pred 0 = (ppred 0).getD 0

pp: case succ
n✝ : ℕ
⊢ (n✝ + 1).pred = (n✝ + 1).ppred.getD 0

Tactic:
<;>

Goal state after:
case zero
⊢ pred 0 = (ppred 0).getD 0

case succ
n✝ : ℕ
⊢ (n✝ + 1).pred = (n✝ + 1).ppred.getD 0
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case none
m n : ℕ
⊢ (none.getD 0).ppred.getD 0 = (none >>= ppred).getD 0

pp: case some
m n val✝ : ℕ
⊢ ((some val✝).getD 0).ppred.getD 0 = (some val✝ >>= ppred).getD 0

Tactic:
<;>

Goal state after:
case none
m n : ℕ
⊢ (none.getD 0).ppred.getD 0 = (none >>= ppred).getD 0

case some
m n val✝ : ℕ
⊢ ((some val✝).getD 0).ppred.getD 0 = (some val✝ >>= ppred).getD 0
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mp
m : ℕ
⊢ ppred 0 = some m → m.succ = 0

pp: case mpr
m : ℕ
⊢ m.succ = 0 → ppred 0 = some m

Tactic:
<;>

Goal state after:
case mp
m : ℕ
⊢ ppred 0 = some m → m.succ = 0

case mpr
m : ℕ
⊢ m.succ = 0 → ppred 0 = some m
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mp
m : ℕ
h : ppred 0 = some m
⊢ m.succ = 0

pp: case mpr
m : ℕ
h : m.succ = 0
⊢ ppred 0 = some m

Tactic:
<;>

Goal state after:
case mp
m : ℕ
h : ppred 0 = some m
⊢ m.succ = 0

case mpr
m : ℕ
h : m.succ = 0
⊢ ppred 0 = some m
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mp
m n : ℕ
⊢ (n + 1).ppred = some m → m.succ = n + 1

pp: case mpr
m n : ℕ
⊢ m.succ = n + 1 → (n + 1).ppred = some m

Tactic:
<;>

Goal state after:
case mp
m n : ℕ
⊢ (n + 1).ppred = some m → m.succ = n + 1

case mpr
m n : ℕ
⊢ m.succ = n + 1 → (n + 1).ppred = some m
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mp
m n : ℕ
h : (n + 1).ppred = some m
⊢ m.succ = n + 1

pp: case mpr
m n : ℕ
h : m.succ = n + 1
⊢ (n + 1).ppred = some m

Tactic:
<;>

Goal state after:
case mp
m n : ℕ
h : (n + 1).ppred = some m
⊢ m.succ = n + 1

case mpr
m n : ℕ
h : m.succ = n + 1
⊢ (n + 1).ppred = some m
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mp
m n : ℕ
val_eq✝ : n = m
⊢ m.succ = n + 1

pp: case mpr
m n : ℕ
n_eq✝ : m = n
⊢ (n + 1).ppred = some m

Tactic:
<;>

Goal state after:
case mp
m n : ℕ
val_eq✝ : n = m
⊢ m.succ = n + 1

case mpr
m n : ℕ
n_eq✝ : m = n
⊢ (n + 1).ppred = some m
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mp
n : ℕ
⊢ n.succ = n + 1

pp: case mpr
n : ℕ
⊢ (n + 1).ppred = some n

Tactic:
<;>

Goal state after:
case mp
n : ℕ
⊢ n.succ = n + 1

case mpr
n : ℕ
⊢ (n + 1).ppred = some n
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mp
n : ℕ
⊢ (n + 1).ppred = none → n + 1 = 0

pp: case mpr
n : ℕ
⊢ n + 1 = 0 → (n + 1).ppred = none

Tactic:
<;>

Goal state after:
case mp
n : ℕ
⊢ (n + 1).ppred = none → n + 1 = 0

case mpr
n : ℕ
⊢ n + 1 = 0 → (n + 1).ppred = none
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mp
n : ℕ
a✝ : (n + 1).ppred = none
⊢ n + 1 = 0

pp: case mpr
n : ℕ
a✝ : n + 1 = 0
⊢ (n + 1).ppred = none

Tactic:
<;>

Goal state after:
case mp
n : ℕ
a✝ : (n + 1).ppred = none
⊢ n + 1 = 0

case mpr
n : ℕ
a✝ : n + 1 = 0
⊢ (n + 1).ppred = none
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case zero
p : ℕ
⊢ Nat.rec 0 (fun y IH ↦ (unpair p).1 + IH) 0 = (unpair p).1 * 0

pp: case succ
p n✝ : ℕ
a✝ : Nat.rec 0 (fun y IH ↦ (unpair p).1 + IH) n✝ = (unpair p).1 * n✝
⊢ Nat.rec 0 (fun y IH ↦ (unpair p).1 + IH) (n✝ + 1) = (unpair p).1 * (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
p : ℕ
⊢ Nat.rec 0 (fun y IH ↦ (unpair p).1 + IH) 0 = (unpair p).1 * 0

case succ
p n✝ : ℕ
a✝ : Nat.rec 0 (fun y IH ↦ (unpair p).1 + IH) n✝ = (unpair p).1 * n✝
⊢ Nat.rec 0 (fun y IH ↦ (unpair p).1 + IH) (n✝ + 1) = (unpair p).1 * (n✝ + 1)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case zero
p : ℕ
⊢ Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) 0 = (unpair p).1 ^ 0

pp: case succ
p n✝ : ℕ
a✝ : Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) n✝ = (unpair p).1 ^ n✝
⊢ Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) (n✝ + 1) = (unpair p).1 ^ (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
p : ℕ
⊢ Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) 0 = (unpair p).1 ^ 0

case succ
p n✝ : ℕ
a✝ : Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) n✝ = (unpair p).1 ^ n✝
⊢ Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) (n✝ + 1) = (unpair p).1 ^ (n✝ + 1)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode none = encode (Option.map (⇑e.symm) none)

pp: case some
α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
val✝ : α
⊢ encode (some val✝) = encode (Option.map (⇑e.symm) (some val✝))

Tactic:
<;>

Goal state after:
case none
α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
⊢ encode none = encode (Option.map (⇑e.symm) none)

case some
α : Type ?u.4
β : Type ?u.9
inst✝ : Primcodable α
e : β ≃ α
n : ℕ
val✝ : α
⊢ encode (some val✝) = encode (Option.map (⇑e.symm) (some val✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case zero
⊢ (Nat.casesOn 0 1 fun x ↦ 0) = encode (decode 0)

pp: case succ
n✝ : ℕ
⊢ (Nat.casesOn (n✝ + 1) 1 fun x ↦ 0) = encode (decode (n✝ + 1))

Tactic:
<;>

Goal state after:
case zero
⊢ (Nat.casesOn 0 1 fun x ↦ 0) = encode (decode 0)

case succ
n✝ : ℕ
⊢ (Nat.casesOn (n✝ + 1) 1 fun x ↦ 0) = encode (decode (n✝ + 1))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case succ.none
α : Type u_1
h : Primcodable α
n : ℕ
H : decode n = none
⊢ (Nat.casesOn (n + 1) 1 fun n ↦ Nat.casesOn (encode (decode n)) 0 fun n ↦ n.succ.succ) = encode (Option.map some none)

pp: case succ.some
α : Type u_1
h : Primcodable α
n : ℕ
val✝ : α
H : decode n = some val✝
⊢ (Nat.casesOn (n + 1) 1 fun n ↦ Nat.casesOn (encode (decode n)) 0 fun n ↦ n.succ.succ) =
    encode (Option.map some (some val✝))

Tactic:
<;>

Goal state after:
case succ.none
α : Type u_1
h : Primcodable α
n : ℕ
H : decode n = none
⊢ (Nat.casesOn (n + 1) 1 fun n ↦ Nat.casesOn (encode (decode n)) 0 fun n ↦ n.succ.succ) = encode (Option.map some none)

case succ.some
α : Type u_1
h : Primcodable α
n : ℕ
val✝ : α
H : decode n = some val✝
⊢ (Nat.casesOn (n + 1) 1 fun n ↦ Nat.casesOn (encode (decode n)) 0 fun n ↦ n.succ.succ) =
    encode (Option.map some (some val✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: n✝ n : ℕ
⊢ (Nat.casesOn (n + 2) 1 fun x ↦ Nat.casesOn x 2 fun x ↦ 0) = encode none

pp: case h
n✝ n : ℕ
⊢ 2 ≤ n + 2

Tactic:
<;>

Goal state after:
n✝ n : ℕ
⊢ (Nat.casesOn (n + 2) 1 fun x ↦ Nat.casesOn x 2 fun x ↦ 0) = encode none

case h
n✝ n : ℕ
⊢ 2 ≤ n + 2
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ encode none = encode (Option.map encode none)

pp: case some
α : Type u_1
inst✝ : Primcodable α
n : ℕ
val✝ : α
⊢ encode (some val✝) = encode (Option.map encode (some val✝))

Tactic:
<;>

Goal state after:
case none
α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ encode none = encode (Option.map encode none)

case some
α : Type u_1
inst✝ : Primcodable α
n : ℕ
val✝ : α
⊢ encode (some val✝) = encode (Option.map encode (some val✝))