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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
⊢ cycleGraph n ⊑ G ↔ ∃ v p, p.IsCycle ∧ p.length = n

Tactic:
refine ⟨fun ⟨h⟩ ↦ ?_, fun h' ↦ ?_⟩
  · have : n = n - 3 + 3 := by lia
    rw [this] at h
    refine ⟨h.toHom ⟨0, by lia⟩, Walk.map h.toHom <| cycleGraph.cycle (n - 3), ?_, ?_⟩
    · exact (isCycle_map_iff_of_injective h.injective).mpr cycleGraph.isCycle_cycle
    · simp [cycleGraph.length_cycle, ← this]
  · obtain ⟨a, p, hp₁, hp₂⟩ := h'
    refine ⟨⟨⟨fun n ↦ p.support[n.succ]'(?_), ?_⟩, ?_⟩⟩
    · grind [hp₁.three_le_length, length_tail_add_one, not_nil_iff_lt_length]
    · intro ⟨x, hx⟩ ⟨y, hy⟩ hab
      have hne : x ≠ y := fun _ ↦ by simp_all
      wlog hle : x > y
      · exact this hn a p hp₁ hp₂ y hy x hx hab.symm hne.symm (by lia) |>.symm
      rcases cycleGraph_adj'.mp hab with hab | hab
      · simp_rw [show x = y + 1 by grind [Fin.sub_val_of_le]]
        exact p.isChain_adj_support.getElem _ _ |>.symm
      · rw [Fin.coe_sub_iff_lt.mpr hle] at hab
        simp_rw [show x = n - 1 by lia, show y = 0 by lia, Fin.succ_mk, show n - 1 + 1 = n by lia]
        simp [← hp₂, p.adj_snd hp₁.not_nil]
    · have hlen : p.tail.support.length = n := by
        grind [length_tail_add_one, not_nil_iff_lt_length]
      have (m : Fin n) : p.support[m.succ]'(by grind) = p.tail.support[m] := by
        simp [p.support_tail_of_not_nil hp₁.not_nil]
      simp_rw [this]
      have := IsPath.mk' <| (support_tail_of_not_nil _ hp₁.not_nil) ▸ hp₁.support_nodup
      exact hlen ▸ (isPath_iff_injective_get_support _ |>.mp this)

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : extremalNumber (Fintype.card V) H < #G.edgeFinset
⊢ H ⊑ G

Tactic:
contrapose h

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ¬H ⊑ G
⊢ ¬extremalNumber (Fintype.card V) H < #G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h✝ : n₁ = n₂
e : H₁ ≃g H₂
G : SimpleGraph (Fin n₂)
inst✝ : DecidableRel G.Adj
h : H₁.Free G
⊢ H₂.Free G

Tactic:
contrapose h

Goal state after:
case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h✝ : n₁ = n₂
e : H₁ ≃g H₂
G : SimpleGraph (Fin n₂)
inst✝ : DecidableRel G.Adj
h : H₂ ⊑ G
⊢ H₁ ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h✝ : n₁ = n₂
e : H₂ ≃g H₁
G : SimpleGraph (Fin n₂)
inst✝ : DecidableRel G.Adj
h : H₂.Free G
⊢ H₁.Free G

Tactic:
contrapose h

Goal state after:
case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h✝ : n₁ = n₂
e : H₂ ≃g H₁
G : SimpleGraph (Fin n₂)
inst✝ : DecidableRel G.Adj
h : H₁ ⊑ G
⊢ H₂ ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : H.Free G
v : V
⊢ H.Free (induce {v}ᶜ G)

Tactic:
contrapose h

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
h : H ⊑ induce {v}ᶜ G
⊢ H ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ ∑ x ∈ G.neighborFinset u, ↑(#(G.finsetWalkLength n x v)) =
    ↑(#(univ.biUnion fun w ↦ Finset.map { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑w) v)))

Tactic:
rw [Finset.card_biUnion]

Goal state after:
case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ ∑ x ∈ G.neighborFinset u, ↑(#(G.finsetWalkLength n x v)) =
    ↑(∑ u_1, #(Finset.map { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑u_1) v)))

case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ (↑univ).PairwiseDisjoint fun w ↦
    Finset.map { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑w) v)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
h : ¬G.IsCompleteMultipartite
⊢ ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂

Tactic:
apply mt IsTrans.mk at h

Goal state after:
α : Type u
G : SimpleGraph α
h : ¬∀ (a b c : α), ¬G.Adj a b → ¬G.Adj b c → ¬G.Adj a c
⊢ ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁✝ a₂✝ : Fin 3
a✝ :
  (fun x ↦
        match x with
        | 0 => w₁
        | 1 => v
        | 2 => w₂)
      a₁✝ =
    (fun x ↦
        match x with
        | 0 => w₁
        | 1 => v
        | 2 => w₂)
      a₂✝
⊢ a₁✝ = a₂✝

Tactic:
have := h.ne_fst

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁✝ a₂✝ : Fin 3
a✝ :
  (fun x ↦
        match x with
        | 0 => w₁
        | 1 => v
        | 2 => w₂)
      a₁✝ =
    (fun x ↦
        match x with
        | 0 => w₁
        | 1 => v
        | 2 => w₂)
      a₂✝
this : v ≠ w₁
⊢ a₁✝ = a₂✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
e : (pathGraph 3)ᶜ ↪g G
h : G.IsCompleteMultipartite
⊢ False

Tactic:
have h0 : ¬ G.Adj (e 0) (e 1) := by simp [pathGraph_adj]

Goal state after:
α : Type u
G : SimpleGraph α
e : (pathGraph 3)ᶜ ↪g G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj (e 0) (e 1)
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
β : Type u_1
H : SimpleGraph β
f : H ↪g G
h : G.IsCompleteMultipartite
⊢ H.IsCompleteMultipartite

Tactic:
contrapose h

Goal state after:
α : Type u
G : SimpleGraph α
β : Type u_1
H : SimpleGraph β
f : H ↪g G
h : ¬H.IsCompleteMultipartite
⊢ ¬G.IsCompleteMultipartite
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd (Fintype.card ↑{c | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp}) ↔
    Odd #({x ∈ {c | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)})

Tactic:
Fintype.card_ofFinset

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd #({a ∈ G.oddComponents.toFinset | (fun c ↦ c.supp ⊆ c'.supp) a}) ↔
    Odd #({x ∈ {c | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)})
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
i₁ i₂ : Fin r
h :
  ∀ (a : V),
    a ∈ map { toFun := fun j ↦ f (i₁, j), inj' := ⋯ } univ ↔ a ∈ map { toFun := fun j ↦ f (i₂, j), inj' := ⋯ } univ
this : NeZero t
⊢ ∃ j, f (i₁, j) = f (i₂, 0)

Tactic:
simpa using h <| f (i₂, 0)

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

Goal state before:
pp: case h
α : Type u_1
G : SimpleGraph α
x✝ : Nonempty α ∧ Subsingleton α
left✝ : Nonempty α
right✝ : Subsingleton α
⊢ G.eccent Classical.ofNonempty = 0

Tactic:
simpa [eccent] using Subsingleton.elim _

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ hom h C = D → ∃ x ∈ ↑C, x ∈ ↑D

pp: case mpr
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ (∃ x ∈ ↑C, x ∈ ↑D) → hom h C = D

Tactic:
· rintro rfl
    refine C.ind fun x xnL => ?_
    exact ⟨x, ⟨xnL, rfl⟩, ⟨fun xK => xnL (h xK), rfl⟩⟩

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ (∃ x ∈ ↑C, x ∈ ↑D) → hom h C = D
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 : G.CliqueFree (0 + 1)
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % 0) ^ 2) * (0 - 1) / (2 * 0) + (n % 0).choose 2

pp: case inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
· rw [cliqueFree_one, ← Fintype.card_eq_zero_iff] at cf
    simp_rw [zero_tsub, mul_zero, Nat.mod_zero, Nat.div_zero, zero_add]
    exact card_edgeFinset_le_card_choose_two

Goal state after:
case inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
ha : M.Adj v w
⊢ h.toEdge ⟨v, ⋯⟩ = h.toEdge ⟨w, ⋯⟩

Tactic:
rw [h.toEdge_eq_of_adj ha, h.toEdge_eq_of_adj ha.symm, Subtype.mk_eq_mk, Sym2.eq_swap]

Goal state after:
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)
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, G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))

Tactic:
obtain ⟨a, b, c, d, ha, haj, hb, hbj, hc, hcj, hd, hdj, hab, had, hbc, hat, hbs⟩ :=
    hw.exist_not_adj_of_adj_inter hcf hW

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)
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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
⊢ ∃ a b, G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case inr
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
⊢ completeEquipartiteGraph (r + 1) t ⊑ G

Tactic:
have hrε_lt_1 : r * ε < 1 := by
      have hδ_lt_card : (G.minDegree : ℝ) < (n : ℝ) := by
        conv_rhs =>
          rw [← Fintype.card_fin n]
        exact_mod_cast G.minDegree_lt_card
      contrapose! hδ_lt_card with h1_le_rε
      rw [← div_le_iff₀' (by positivity), ← sub_nonpos,
        ← le_sub_self_iff 1, ← sub_add] at h1_le_rε
      exact hδ.trans' (le_mul_of_one_le_left n.cast_nonneg h1_le_rε)

Goal state after:
case inr
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
⊢ completeEquipartiteGraph (r + 1) t ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
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:
exact hbj <| hw.isNClique_snd_right.1 (mem_insert_self ..) (mem_insert_of_mem hbt) hbx

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

Goal state before:
pp: case cons
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 : p.IsTrail → (Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝)
ht : (cons huv p).IsTrail
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) (cons huv p).edges) ↔ u✝ ≠ w✝ → x ≠ u✝ ∧ x ≠ w✝

Tactic:
| cons huv p ih =>

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

Goal state before:
pp: case inr.convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
x : V
⊢ x ∈ {x | ¬u = v ∧ (¬x = u → x = v)} ↔ x ∈ {u, v}

Tactic:
simp [hn, imp_iff_not_or]

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

Goal state before:
pp: case refine_2
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
hadj : s(x, a) ∈ p.toSubgraph.edgeSet
⊢ False

Tactic:
Subgraph.mem_edgeSet

Goal state after:
case refine_2
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
hadj : p.toSubgraph.Adj x a
⊢ False
Module: Mathlib.Combinatorics.Young.YoungDiagram

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

Tactic:
induction w generalizing c <;> rw [YoungDiagram.cellsOfRowLens]

Goal state after:
case nil
c : ℕ × ℕ
⊢ c ∈ ∅ ↔ ∃ (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 ∈
      {0} ×ˢ Finset.range head✝ ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail✝) ↔
    ∃ (h : c.1 < (head✝ :: tail✝).length), c.2 < (head✝ :: tail✝)[c.1]
Module: Mathlib.Combinatorics.Young.SemistandardTableau

Goal state before:
pp: case inr
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 < i2
⊢ T i1 j ≤ T i2 j

Tactic:
· exact le_of_lt (T.col_strict h cell)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
a : Option α
b : Option β
⊢ Option.map (fun p ↦ f p.1 p.2) (a.bind fun a ↦ Option.map (Prod.mk a) b) = a.bind fun a ↦ Option.map (f a) b

Tactic:
cases a

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
b : Option β
⊢ Option.map (fun p ↦ f p.1 p.2) (none.bind fun a ↦ Option.map (Prod.mk a) b) = none.bind fun a ↦ Option.map (f a) b

case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
b : Option β
val✝ : α
⊢ Option.map (fun p ↦ f p.1 p.2) ((some val✝).bind fun a ↦ Option.map (Prod.mk a) b) =
    (some val✝).bind fun a ↦ Option.map (f a) b
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
f : Bool → Bool → α
x✝ : Bool × Bool
a b : Bool
⊢ (bif (a, b).1 then f true (a, b).2 else f false (a, b).2) = f (a, b).1 (a, b).2

Tactic:
cases a

Goal state after:
case false
α : Type u_1
inst✝ : Primcodable α
f : Bool → Bool → α
x✝ : Bool × Bool
b : Bool
⊢ (bif (false, b).1 then f true (false, b).2 else f false (false, b).2) = f (false, b).1 (false, b).2

case true
α : Type u_1
inst✝ : Primcodable α
f : Bool → Bool → α
x✝ : Bool × Bool
b : Bool
⊢ (bif (true, b).1 then f true (true, b).2 else f false (true, b).2) = f (true, b).1 (true, b).2
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
d : α
⊢ Primrec₂ fun l n ↦ l[n]?.getD d

Tactic:
exact option_getD.comp₂ list_getElem? (const _)

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

Goal state before:
pp: case some
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n ↦ (decode n).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a
n : ℕ
a : α
⊢ encode (if decide (p a) = true then some a else none) = encode (if h : p a then some ⟨a, h⟩ else none)

Tactic:
by_cases h : p a

Goal state after:
case pos
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n ↦ (decode n).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a
n : ℕ
a : α
h : p a
⊢ encode (if decide (p a) = true then some a else none) = encode (if h : p a then some ⟨a, h⟩ else none)

case neg
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n ↦ (decode n).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a
n : ℕ
a : α
h : ¬p a
⊢ encode (if decide (p a) = true then some a else none) = encode (if h : p a then some ⟨a, h⟩ else none)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
⊢ Primrec f → Primrec fun a ↦ (f a).get ⋯

Tactic:
intro hf

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
⊢ Primrec fun a ↦ (f a).get ⋯
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case false.inr
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
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
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h✝ : n ≤ m
h : n = m
⊢ false ∈ p n

Tactic:
rw [h]
          exact ⟨_, e⟩

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

Goal state before:
pp: v : List.Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH ↦ y) v.head = v.head - 1

Tactic:
cases v.head

Goal state after:
case zero
v : List.Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH ↦ y) 0 = 0 - 1

case succ
v : List.Vector ℕ (Nat.succ 0)
n✝ : ℕ
⊢ Nat.rec 0 (fun y IH ↦ y) (n✝ + 1) = n✝ + 1 - 1
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case zero
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec 0 (fun y IH ↦ v.tail.head + IH) 0 = 0 * v.tail.head

Tactic:
simp [*, Nat.succ_mul]

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

Goal state before:
pp: case succ
v : List.Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
a✝ : Nat.rec 0 (fun y IH ↦ v.tail.head + IH) n✝ = n✝ * v.tail.head
⊢ Nat.rec 0 (fun y IH ↦ v.tail.head + IH) (n✝ + 1) = (n✝ + 1) * v.tail.head

Tactic:
simp [*, Nat.succ_mul]

Goal state after:
case succ
v : List.Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
a✝ : Nat.rec 0 (fun y IH ↦ v.tail.head + IH) n✝ = n✝ * v.tail.head
⊢ v.tail.head + n✝ * v.tail.head = n✝ * v.tail.head + v.tail.head
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: n : ℕ
m : ℕ := n.div2.div2
⊢ m < n + 4

Tactic:
by
      simp only [m, div2_val]
      exact
        lt_of_le_of_lt (le_trans (Nat.div_le_self _ _) (Nat.div_le_self _ _))
          (Nat.succ_le_succ (Nat.le_add_right _ _))

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

Goal state before:
pp: case neg
n : ℕ
IH : Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
h : ¬n + 1 < (n.sqrt + 1) * (n.sqrt + 1)
⊢ n.sqrt + 1 = (n + 1).sqrt

Tactic:
exact Nat.eq_sqrt.2
        ⟨not_lt.1 h, Nat.sqrt_lt.1 <| Nat.lt_succ_iff.2 <| Nat.sqrt_succ_le_succ_sqrt _⟩

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m : ℕ
⊢ 0 < ack (m + 1) 0

Tactic:
ack_succ_zero

Goal state after:
m : ℕ
⊢ 0 < ack m 1
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m : ℕ
⊢ 1 < ack (m + 1 + 1) 0

Tactic:
ack_succ_zero

Goal state after:
m : ℕ
⊢ 1 < ack (m + 1) 1
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m : ℕ
⊢ (ack m 1 + 1) ^ 2 ≤ ack (m + 1 + 3) 0

Tactic:
ack_succ_zero

Goal state after:
m : ℕ
⊢ (ack m 1 + 1) ^ 2 ≤ ack (m + 3) 1