mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
this : #s ≤ Fintype.card α / 2
⊢ ∀ (t₁ : Finset α),
    (∀ {t₂ : Finset α},
        #t₂ ≤ Fintype.card α / 2 →
          t₁ ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting) →
      #t₁ ≤ Fintype.card α / 2 → (↑t₁).Intersecting → ∃ t, t₁ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting

Tactic:
rintro s ih _hcard hs

Goal state after:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
⊢ ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
⊢ ∃ a ∉ t,
    #s = #(insert a t) ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))

Tactic:
have hcard : #s = #(insert j t) := by
    rw [card_insert_of_notMem ‹j ∉ t›, ← ‹_ = #t›, card_erase_add_one (min'_mem _ _)]

Goal state after:
case mpr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
⊢ ∃ a ∉ t,
    #s = #(insert a t) ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : x ∈ s
_s' : Set α
hs' : _s' ∈ c
⊢ x ∈ _s' → y ∈ _s'

Tactic:
hx'

Goal state after:
case mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : x ∈ s
_s' : Set α
hs' : _s' ∈ c
hx' : x ∈ _s'
⊢ y ∈ _s'
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case left.a.a
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
a b : α
h_eq : {x | r x a} = {x | r x b}
⊢ a ∈ {x | r x b}

Tactic:
rw [← h_eq]

Goal state after:
case left.a.a
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
a b : α
h_eq : {x | r x a} = {x | r x b}
⊢ a ∈ {x | r x a}
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G = ⊥ ∧ ¬G.Colorable 0 ↔ G = ⊥ ∧ ¬IsEmpty V

Tactic:
colorable_zero_iff

Goal state after:
V : Type u
G : SimpleGraph V
⊢ G = ⊥ ∧ ¬IsEmpty V ↔ G = ⊥ ∧ ¬IsEmpty V
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
⊢ ¬(G.deleteEdges {s(y, x)}).Reachable u x

Tactic:
· rintro ⟨p⟩
    obtain ⟨hx₂, -, hy₂⟩ : G.Adj x p.penultimate ∧ _ ∧ ¬p.penultimate = y := by
      simpa using p.reverse.adj_snd (not_nil_of_ne ‹_›)
    exact hy₂ <| hx hx₂ hxy

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
⊢ ¬(G.deleteEdges {s(y, x)}).Reachable v x

Tactic:
· rintro ⟨p⟩
    obtain ⟨hx₂, -, hy₂⟩ : G.Adj x p.penultimate ∧ _ ∧ ¬p.penultimate = y := by
      simpa using p.reverse.adj_snd (not_nil_of_ne ‹_›)
    exact hy₂ <| hx hx₂ hxy

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet v)
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ Disjoint (G.neighborSet v) ↑s

Tactic:
exact isBipartiteWith_neighborSet_disjoint h hv

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
⊢ w ∈ {w | (between s sᶜ G).Adj v w} ∪ s

Tactic:
Set.mem_union,

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
⊢ w ∈ {w | (between s sᶜ G).Adj v w} ∨ w ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
⊢ v ∈ {w_1 | (between s sᶜ G).Adj w w_1} ∪ sᶜ

Tactic:
Set.mem_union,

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
⊢ v ∈ {w_1 | (between s sᶜ G).Adj w w_1} ∨ v ∈ sᶜ
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ (∀ ⦃v_1 : V⦄,
      v_1 ∈ w.toSubgraph.verts → ∀ ⦃w_1 : V⦄, w_1 ∈ w.toSubgraph.verts → G.Adj v_1 w_1 → w.toSubgraph.Adj v_1 w_1) ↔
    ∀ ⦃e : Sym2 V⦄, ¬w.IsChord e

Tactic:
IsChord,

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ (∀ ⦃v_1 : V⦄,
      v_1 ∈ w.toSubgraph.verts → ∀ ⦃w_1 : V⦄, w_1 ∈ w.toSubgraph.verts → G.Adj v_1 w_1 → w.toSubgraph.Adj v_1 w_1) ↔
    ∀ ⦃e : Sym2 V⦄, ¬(e ∈ G.edgeSet ∧ e ∉ w.edges ∧ Sym2.lift ⟨fun v_1 w_1 ↦ v_1 ∈ w.support ∧ w_1 ∈ w.support, ⋯⟩ e)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s✝ t✝ s t : Finset α
⊢ image (⇑{ toFun := ⇑liftLatticeHom, inj' := ⋯ }) (s \\ t) =
    image (⇑{ toFun := ⇑liftLatticeHom, inj' := ⋯ }) s \\ image (⇑{ toFun := ⇑liftLatticeHom, inj' := ⋯ }) t

Tactic:
exact image_image₂_distrib fun a b ↦ rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ : α
b : β
a₂ : α
⊢ (G □ H).Adj (a₁, b) (a₂, b) ↔ G.Adj a₁ a₂

Tactic:
by
  simp only [boxProd_adj, and_true, SimpleGraph.irrefl, false_and, or_false]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
let w_app := (wG.boxProdLeft _ _).append (wH.boxProdRight _ _)

Goal state after:
case neg
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl.inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
v₁ : V
w₂ : W
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inl v₁) (Sum.inr w₂)

pp: case inr.inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ : W
v₂ : V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inl v₂)

pp: case inr.inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ w₂ : W
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inr w₂)

Tactic:
· exact (hG ..).sum_sup_edge (hH ..)

Goal state after:
case inr.inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ : W
v₂ : V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inl v₂)

case inr.inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ w₂ : W
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inr w₂)
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_2
V : Type u_1
G H : SimpleGraph V
hHG : H ≤ G
hH : H.IsAcyclic
c : Set (SimpleGraph V)
hcs : c ⊆ {H | H ≤ G ∧ H.IsAcyclic}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : SimpleGraph V
hy : y ∈ c
⊢ (sSup c).IsAcyclic

Tactic:
exact isAcyclic_sSup_of_isAcyclic_directedOn c (by grind) hc.directedOn

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

Goal state before:
pp: case mpr.refine_2
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
⊢ ∀ (u v : V) (x y : G.Path u v), x = y

Tactic:
rintro v w ⟨p, hp⟩ ⟨q, hq⟩

Goal state after:
case mpr.refine_2
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
v w : V
p : G.Walk v w
hp : p.IsPath
q : G.Walk v w
hq : q.IsPath
⊢ ⟨p, hp⟩ = ⟨q, hq⟩
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case refine_2
n r : ℕ
⊢ r = 0 ∨ n ≤ r → ∀ (x x_1 : Fin n), ↑x % r = ↑x_1 % r ↔ x = x_1

Tactic:
rintro (rfl | h) a b

Goal state after:
case refine_2.inl
n : ℕ
a b : Fin n
⊢ ↑a % 0 = ↑b % 0 ↔ a = b

case refine_2.inr
n r : ℕ
h : n ≤ r
a b : Fin n
⊢ ↑a % r = ↑b % r ↔ a = b
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ Function.Injective fun v ↦ ⟨↑v, ⋯⟩

Tactic:
by
    rintro v w
    rw [Fin.mk.injEq]
    exact Fin.ext

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
⊢ False

Tactic:
have h' : G.chromaticNumber ≤ 2 := Order.le_of_lt_add_one <| not_le.mp h

Goal state after:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Finite V
inst✝ : Nontrivial V
hconn : G.Connected
⊢ ∃ v, (induce {v}ᶜ G).Connected

Tactic:
by
  obtain ⟨T, _, T_isTree⟩ := hconn.exists_isTree_le
  have ⟨hT, _⟩ := T_isTree
  have := Fintype.ofFinite V
  classical
  obtain ⟨v, hv⟩ := T_isTree.exists_vert_degree_one_of_nontrivial
  exact ⟨v, (hT.induce_compl_singleton_of_degree_eq_one hv).mono (by tauto)⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
⊢ G.dist u v ≠ G.dist u w

Tactic:
obtain ⟨p, hp, hp'⟩ := hreach.exists_path_of_dist

Goal state after:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
⊢ G.dist u v ≠ G.dist u w
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
⊢ False

Tactic:
obtain ⟨x, -, y, -, hn, he⟩ :=
    exists_ne_map_eq_of_card_lt_of_maps_to l.1 fun a _ ↦ fp.part_mem.2 (mem_univ a)

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
z : Finset V
zc : #z = r
⊢ ∃ x ∈ ↑z, ∃ y ∈ ↑z, x ≠ y ∧ ¬G.Adj x y

Tactic:
h.not_adj_iff_part_eq

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
z : Finset V
zc : #z = r
⊢ ∃ x ∈ ↑z, ∃ y ∈ ↑z, x ≠ y ∧ h.finpartition.part x = h.finpartition.part y
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case e'_4
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
cf : G.CliqueFree r
⊢ ¬G.Adj x y

Tactic:
h.not_adj_iff_part_eq

Goal state after:
case e'_4
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
cf : G.CliqueFree r
⊢ h.finpartition.part x = h.finpartition.part y
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case inj'
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := ⋯
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := ⋯
⊢ Injective fun x ↦
    match x with
    | (i, j) => ↑((fₜ (fᵣ i)) j)

Tactic:
intro (i₁, j₁) (i₂, j₂) heq

Goal state after:
case inj'
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
heq :
  (fun x ↦
        match x with
        | (i, j) => ↑((fₜ (fᵣ i)) j))
      (i₁, j₁) =
    (fun x ↦
        match x with
        | (i, j) => ↑((fₜ (fᵣ i)) j))
      (i₂, j₂)
⊢ (i₁, j₁) = (i₂, j₂)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : Finite α
inst✝ : Nontrivial α
⊢ G.Connected ↔ G.diam ≠ 0

Tactic:
rw [connected_iff_ediam_ne_top, not_iff_not, diam_eq_zero_iff_ediam_eq_top]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
cf : Fintype.card V = 0
⊢ #G.edgeFinset ≤ (Fintype.card V).choose 2

Tactic:
exact card_edgeFinset_le_card_choose_two

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case refine_3
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ #↑(Subtype.val '' ⇑f ⁻¹' range Sum.inl) = #↑(Subtype.val '' ⇑f ⁻¹' range Sum.inr)

Tactic:
simp [mk_image_eq Subtype.val_injective]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
w✝² w✝¹ w✝ : α
s t : Finset α
hw : G.IsFiveWheelLike r (#(s ∩ t)) w✝² w✝¹ w✝ s t
P : ℕ → Prop := fun k ↦ ∃ v w₁ w₂ s t, G.IsFiveWheelLike r k v w₁ w₂ s t
hk : P #(s ∩ t)
⊢ ∃ k v w₁ w₂ s t, G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j

Tactic:
classical
  obtain ⟨_, _, _, _, _, hw⟩ := Nat.findGreatest_spec (hw.card_inter_lt_of_cliqueFree h.1).le hk
  exact ⟨_, _, _, _, _, _, hw, hw.card_inter_lt_of_cliqueFree h.1,
         fun _ hj _ _ _ _ _ hv ↦ hj.not_ge <| Nat.le_findGreatest
           (hv.card_inter_lt_of_cliqueFree h.1).le ⟨_, _, _, _, _, hv⟩⟩

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : MulZeroOneClass R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
e : Sym2 α
⊢ incMatrix R G a e * incMatrix R G b e = (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 e

Tactic:
simp [incMatrix_apply', Set.indicator_apply, ← ite_and, and_comm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type v
C : G.Coloring α
⊢ ∀ s ∈ C.colorClasses, IsAntichain G.Adj s

Tactic:
by
    rintro s ⟨c, rfl⟩
    apply C.isIndepSet_colorClass

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
hc : hf.toFinset.card ≤ n
⊢ G.Colorable n

Tactic:
have : Fintype P.parts := hf.fintype

Goal state after:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
hc : hf.toFinset.card ≤ n
this : Fintype ↑P.parts
⊢ G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
G' : SimpleGraph V
hG' : G'.IsAlternating M2.spanningCoe
hG'cyc : G'.IsCycles
hG'xb : ¬G'.Adj x b
hnG'ac : G'.Adj a c
hle : G' ≤ G ⊔ edge a c
this : M2.spanningCoe ∆ G' ≤ G
⊢ (toSubgraph (M2.spanningCoe ∆ G') this).IsPerfectMatching

Tactic:
apply hM2.symmDiff_of_isAlternating hG' hG'cyc

Goal state after:
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: m n : ℕ
⊢ m.psub n = none ↔ m < n

Tactic:
rcases s : psub m n
  · simp only [true_iff]
    refine lt_of_not_ge fun h => ?_
    obtain ⟨k, e⟩ := le.dest h
    injection s.symm.trans (psub_eq_some.2 <| (add_comm _ _).trans e)
  · grind [psub_eq_some]

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this✝ : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : x' ∈ {x, b}
hx'p : x' ∈ p'.support
htw : ∀ t ∈ {x, b}, t ∈ (p'.takeUntil x' hx'p).support → t = x'
this : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd
⊢ (p'.takeUntil x' hx'p).toSubgraph.Adj a c

Tactic:
rwa [Walk.snd_takeUntil, hp'.2.1] at this

Goal state after:
case refine_1.hsu
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this✝ : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : x' ∈ {x, b}
hx'p : x' ∈ p'.support
htw : ∀ t ∈ {x, b}, t ∈ (p'.takeUntil x' hx'p).support → t = x'
this : (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd
⊢ x' ≠ a
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Primrec f
hg : Primrec₂ g
hh : Primrec₂ h
a : α
⊢ (bif (encode (f a)).bodd then Option.map (h a) (decode (encode (f a)).div2)
    else Option.map (g a) (decode (encode (f a)).div2)) =
    some (Sum.casesOn (f a) (g a) (h a))

Tactic:
rcases f a with b | c

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Primrec f
hg : Primrec₂ g
hh : Primrec₂ h
a : α
b : β
⊢ (bif (encode (Sum.inl b)).bodd then Option.map (h a) (decode (encode (Sum.inl b)).div2)
    else Option.map (g a) (decode (encode (Sum.inl b)).div2)) =
    some (Sum.casesOn (Sum.inl b) (g a) (h a))

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Primrec f
hg : Primrec₂ g
hh : Primrec₂ h
a : α
c : γ
⊢ (bif (encode (Sum.inr c)).bodd then Option.map (h a) (decode (encode (Sum.inr c)).div2)
    else Option.map (g a) (decode (encode (Sum.inr c)).div2)) =
    some (Sum.casesOn (Sum.inr c) (g a) (h a))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Nat.Partrec ↑f✝
pg : Nat.Partrec ↑g✝
⊢ Nat.Partrec ↑(unpaired fun z n ↦ Nat.rec (f✝ z) (fun y IH ↦ g✝ (Nat.pair z (Nat.pair y IH))) n)

Tactic:
refine (pf.prec pg).of_eq_tot fun n => ?_
    simp only [unpaired, PFun.coe_val, bind_eq_bind]
    induction n.unpair.2 with
    | zero => simp
    | succ m IH =>
      simp only [mem_bind_iff, mem_some_iff]
      exact ⟨_, IH, rfl⟩

Goal state after: