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

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
⊢ G ≤ SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph (Fin m) (Fin n)) ∧
    K.Free (SimpleGraph.map (⇑e₁.toEmbedding) G)

Tactic:
refine ⟨fun _ _ hadj ↦ ?_, ?_⟩

Goal state after:
case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
x✝¹ x✝ : V ⊕ W
hadj : G.Adj x✝¹ x✝
⊢ (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph (Fin m) (Fin n))).Adj x✝¹ x✝

case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
⊢ K.Free (SimpleGraph.map (⇑e₁.toEmbedding) G)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Fintype V
inst✝⁵ : Fintype W
inst✝⁴ : Fintype α
inst✝³ : Fintype β
R : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : R
h : 0 ≤ x
⊢ x < ↑(zarankiewicz m n s t) ↔
    ∃ G x_1, G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ x < ↑(#G.edgeFinset)

Tactic:
simp_rw [← Nat.floor_lt h]

Goal state after:
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Fintype V
inst✝⁵ : Fintype W
inst✝⁴ : Fintype α
inst✝³ : Fintype β
R : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : R
h : 0 ≤ x
⊢ ⌊x⌋₊ < zarankiewicz m n s t ↔
    ∃ G x_1, G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ ⌊x⌋₊ < #G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : 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)
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
a : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
b : α
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
⊢ ∃ a b c d,
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s

Tactic:
obtain ⟨c, hc, hcj⟩ := hw.isNClique_left.exists_not_adj_of_cliqueFree_succ hcf x

Goal state after:
α : 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)
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
a : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
b : α
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
c : α
hc : c ∈ insert v s
hcj : ¬G.Adj x c
⊢ ∃ a b c d,
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
h✝ : Nonempty α
x✝ : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
this : Injective fun x ↦ p.support.get x
⊢ Fin p.support.length ≃ α

Tactic:
refine (Fintype.equivFinOfCardEq ?_).symm

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
h✝ : Nonempty α
x✝ : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
this : Injective fun x ↦ p.support.get x
⊢ Fintype.card α = p.support.length
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
hy : v ∈ s
⊢ ↑(f ⟨v, hy⟩) = ↑(f.symm ⟨v, hr⟩)

pp: case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
y : V
hy : y ∈ s
hr : ↑(f ⟨y, hy⟩) ∈ t
⊢ y = ↑(f.symm ⟨↑(f ⟨y, hy⟩), hr⟩)

Tactic:
· exact (h.ne_of_mem hy hr rfl).elim

Goal state after:
case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
y : V
hy : y ∈ s
hr : ↑(f ⟨y, hy⟩) ∈ t
⊢ y = ↑(f.symm ⟨↑(f ⟨y, hy⟩), hr⟩)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case pos
α : 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
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
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₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj v y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj v z}) ≤ 2
haj : ¬G.Adj v a
hbj : ¬G.Adj v b
hcj : ¬G.Adj v a
hdj : ¬G.Adj v b
hax : v = a
⊢ False

pp: case neg
α : 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
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
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₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj v y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj v z}) ≤ 2
haj : ¬G.Adj v a
hbj : ¬G.Adj v b
hcj : ¬G.Adj v a
hdj : ¬G.Adj v b
hax : ¬v = a
⊢ False

Tactic:
· grind

Goal state after:
case neg
α : 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
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
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₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj v y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj v z}) ≤ 2
haj : ¬G.Adj v a
hbj : ¬G.Adj v b
hcj : ¬G.Adj v a
hdj : ¬G.Adj v b
hax : ¬v = a
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : NonAssocSemiring R
v : V
vec : V → R
⊢ ((diagonal fun x ↦ ↑(G.degree x)) *ᵥ vec) v = ↑(G.degree v) * vec v

Tactic:
mulVec_diagonal

Goal state after:
V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : NonAssocSemiring R
v : V
vec : V → R
⊢ ↑(G.degree v) * vec v = ↑(G.degree v) * vec v
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case pos
α : 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
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
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₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj w₁ y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj w₁ z}) ≤ 2
haj : ¬G.Adj w₁ a
hbj : ¬G.Adj w₁ b
hcj : ¬G.Adj w₁ a
hdj : ¬G.Adj w₁ b
hax : w₁ = a
⊢ False

pp: case neg
α : 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
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
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₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj w₁ y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj w₁ z}) ≤ 2
haj : ¬G.Adj w₁ a
hbj : ¬G.Adj w₁ b
hcj : ¬G.Adj w₁ a
hdj : ¬G.Adj w₁ b
hax : ¬w₁ = a
⊢ False

Tactic:
· grind

Goal state after:
case neg
α : 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
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
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₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj w₁ y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj w₁ z}) ≤ 2
haj : ¬G.Adj w₁ a
hbj : ¬G.Adj w₁ b
hcj : ¬G.Adj w₁ a
hdj : ¬G.Adj w₁ b
hax : ¬w₁ = a
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case pos
α : 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
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
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₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj w₂ y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj w₂ z}) ≤ 2
haj : ¬G.Adj w₂ a
hbj : ¬G.Adj w₂ b
hcj : ¬G.Adj w₂ a
hdj : ¬G.Adj w₂ b
hbx : w₂ = b
⊢ False

pp: case neg
α : 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
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
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₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj w₂ y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj w₂ z}) ≤ 2
haj : ¬G.Adj w₂ a
hbj : ¬G.Adj w₂ b
hcj : ¬G.Adj w₂ a
hdj : ¬G.Adj w₂ b
hbx : ¬w₂ = b
⊢ False

Tactic:
· grind

Goal state after:
case neg
α : 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
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
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₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj w₂ y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj w₂ z}) ≤ 2
haj : ¬G.Adj w₂ a
hbj : ¬G.Adj w₂ b
hcj : ¬G.Adj w₂ a
hdj : ¬G.Adj w₂ b
hbx : ¬w₂ = b
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.LineGraph

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
e : ↑G.edgeSet
⊢ Sym2.map ⇑f ↑e ∈ G'.edgeSet

Tactic:
rcases e with ⟨⟨⟩, h⟩

Goal state after:
case mk
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
val✝ : Sym2 V
a✝ : V × V
h : Quot.mk (Sym2.Rel V) a✝ ∈ G.edgeSet
⊢ Sym2.map ⇑f ↑⟨Quot.mk (Sym2.Rel V) a✝, h⟩ ∈ G'.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Partition

Goal state before:
pp: V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
⊢ False

Tactic:
have hw := P.mem_partOfVertex w

Goal state after:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
hw : w ∈ P.partOfVertex w
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v✝ : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv✝ : v✝ ∈ c.supp
w✝ : V
hw : w✝ ∈ G.neighborSet v✝
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v✝, w✝) ∈ p.edges
hvp : v✝ ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
⊢ Nonempty (↑(G.neighborSet v) ≃ ↑(p.toSubgraph.neighborSet v))

Tactic:
rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        h this, hp.1.ncard_neighborSet_toSubgraph_eq_two (p.mem_verts_toSubgraph.mp hv)]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w w' : V
hww' : w ≠ w'
hvw : H.spanningCoe.Adj v w
hvv' : H.spanningCoe.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
simp only [Subgraph.spanningCoe_adj] at hvw hvv'

Goal state after:
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w w' : V
hww' : w ≠ w'
hvw : H.Adj v w
hvv' : H.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case neg.inr.inl.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'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
hrr1 : v = x
hrr2 : w = u
⊢ G'.Adj v w'

Tactic:
· grind

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case neg.inr.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'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
· grind

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inl
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
y : V
hl : M.Adj v y ∧ ¬G'.Adj v y
⊢ y = w'

pp: case h.inr
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
⊢ y = w'

Tactic:
· grind

Goal state after:
case h.inr
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
⊢ y = w'
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inl
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
y : V
hl : M.Adj v y ∧ ¬G'.Adj v y
⊢ y = w

pp: case h.inr
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
⊢ y = w

Tactic:
· exact hw.2 _ hl.1

Goal state after:
case h.inr
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
⊢ y = w
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
h : ¬decide (x = u✝ ∨ x = v✝) = true
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 0) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Tactic:
· grind

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : 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
hk : s ∩ t = ∅
x✝ : α
⊢ x✝ ∈ X

Tactic:
by simp [X, hk]

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

Goal state before:
pp: μ : YoungDiagram
j : ℕ
⊢ ∃ i, (i, j) ∉ μ.cells

Tactic:
convert! μ.transpose.exists_notMem_row j using 1

Goal state after:
μ : YoungDiagram
j : ℕ
⊢ (fun i ↦ (i, j) ∉ μ.cells) = fun j_1 ↦ (j, j_1) ∉ μ.transpose
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ μ.colLen j2 ≤ μ.colLen j1

Tactic:
convert! μ.transpose.rowLen_anti j1 j2 hj using 1

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.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 ιₚ
pt : PlacedTile ps
a b : G
r :
  (QuotientGroup.leftRel (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt.index)).subtype (↑ps pt.index).symmetries)) a b
⊢ a • ↑(↑ps pt.index) = b • ↑(↑ps pt.index)

Tactic:
rw [QuotientGroup.leftRel_eq] at r
      rw [eq_comm, ← inv_smul_eq_iff, smul_smul, ← MulAction.mem_stabilizer_iff]
      exact SetLike.le_def.1 (Subgroup.map_subtype_le _) r

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a ↦ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
⊢ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a))) =
    some (List.casesOn (f a) (g a) fun b l ↦ h a (b, l))

Tactic:
rcases f a with - | ⟨b, l⟩

Goal state after:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a ↦ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
⊢ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode [])) =
    some (List.casesOn [] (g a) fun b l ↦ h a (b, l))

case cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a ↦ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
b : β
l : List β
⊢ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (b :: l))) =
    some (List.casesOn (b :: l) (g a) fun b l ↦ h a (b, l))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case inr.inl
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
h₃ : m = n
⊢ (p m).Dom

Tactic:
h₃

Goal state after:
case inr.inl
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
h₃ : m = n
⊢ (p n).Dom
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_1
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n
⊢ b ∈ f.fix a

Tactic:
rcases h with ⟨n, ⟨_x, h₁⟩, h₂⟩

Goal state after:
case refine_1
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
⊢ b ∈ f.fix a