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

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
hG : G.IsAcyclic
verts : G.ConnectedComponent → V
h : ∀ (C : G.ConnectedComponent), verts C ∈ C
⊢ ∀ {a b : V},
    G.Adj a b →
      (completeGraph (Fin 2)).Adj
        (let u := verts (G.connectedComponentMk a);
        ⟨G.dist u a % 2, ⋯⟩)
        (let u := verts (G.connectedComponentMk b);
        ⟨G.dist u b % 2, ⋯⟩)

Tactic:
by
    intro u v hadj
    have := ConnectedComponent.sound hadj.reachable
    have := hG.dist_eq_dist_add_one_of_adj_of_reachable _ hadj <| ConnectedComponent.exact <| h _
    grind [top_adj]

Goal state after:
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
⊢ ∀ ⦃x : Finset V⦄, True → ¬G.IsNClique r x

Tactic:
forall_true_left,

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
⊢ ∀ ⦃x : Finset V⦄, ¬G.IsNClique r x
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
h : IsEmpty α
⊢ G.radius ≠ 0

Tactic:
simp [radius]

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

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
⊢ ⊤.radius = 1

Tactic:
simp [radius]

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

Goal state before:
pp: V : Type
G : SimpleGraph V
inst✝ : Finite V
⊢ ∀ (a : ↑G.end), False

Tactic:
rintro ⟨s, _⟩

Goal state after:
V : Type
G : SimpleGraph V
inst✝ : Finite V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
property✝ : s ∈ G.end
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: case hm
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
v : Fin (n + 1)
⊢ v ∈ univ → ↑(#(bipartiteAbove (fun v e ↦ v ∉ e) G.edgeFinset v)) ≤ extremalNumber n H

Tactic:
hv

Goal state after:
case hm
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
v : Fin (n + 1)
hv : v ∈ univ
⊢ ↑(#(bipartiteAbove (fun v e ↦ v ∉ e) G.edgeFinset v)) ≤ extremalNumber n H
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case inl
α : Type u_1
s : Set α
hs : s.Infinite
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard

Tactic:
hs.ncard

Goal state after:
case inl
α : Type u_1
s : Set α
hs : s.Infinite
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = 0
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
p : Finset (Fin n)
hp : p ∈ K.parts
⊢ t ≤ t'

Tactic:
exact ht_lt_t'.le

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
⊢ v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts → ∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w

Tactic:
hv

Goal state after:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
hv : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
⊢ ∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
⊢ ¬G.Colorable (r + 1)

Tactic:
intro ⟨C⟩

Goal state after:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
⊢ v ∈ (M ⊔ M').verts → ∃! w, (M ⊔ M').Adj v w

Tactic:
hv

Goal state after:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
⊢ ∃! w, (M ⊔ M').Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun i j ↦ Disjoint (f i).support (f j).support
v : V
⊢ v ∈ (⨆ i, f i).verts → ∃! w, (⨆ i, f i).Adj v w

Tactic:
hv

Goal state after:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun i j ↦ Disjoint (f i).support (f j).support
v : V
hv : v ∈ (⨆ i, f i).verts
⊢ ∃! w, (⨆ i, f i).Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
⊢ v✝ ∈ (G.subgraphOfAdj h).verts → ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1

Tactic:
hv

Goal state after:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
hv : v✝ ∈ (G.subgraphOfAdj h).verts
⊢ ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
⊢ v✝ ∈ (Subgraph.coeSubgraph M).verts → ∃! w, (Subgraph.coeSubgraph M).Adj v✝ w

Tactic:
hv

Goal state after:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
⊢ ∃! w, (Subgraph.coeSubgraph M).Adj v✝ w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h
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
⊢ v ∈ s ∨ v ∈ t → ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

Tactic:
hv

Goal state after:
case h
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
hv : v ∈ s ∨ v ∈ t
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
c : G.ConnectedComponent
v✝ : V
⊢ v✝ ∈ (M.induce (M.verts ∩ c.supp)).verts → ∃! w, (M.induce (M.verts ∩ c.supp)).Adj v✝ w

Tactic:
hv

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
c : G.ConnectedComponent
v✝ : V
hv : v✝ ∈ (M.induce (M.verts ∩ c.supp)).verts
⊢ ∃! w, (M.induce (M.verts ∩ c.supp)).Adj v✝ w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
hM : M.IsPerfectMatching
c : ↑(⊤.deleteVerts u).coe.oddComponents
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ (↑c).supp
v : V
⊢ v ∈ (M.induce (Subtype.val '' (↑c).supp)).verts → ∃! w, (M.induce (Subtype.val '' (↑c).supp)).Adj v w

Tactic:
hv

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
hM : M.IsPerfectMatching
c : ↑(⊤.deleteVerts u).coe.oddComponents
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ (↑c).supp
v : V
hv : v ∈ (M.induce (Subtype.val '' (↑c).supp)).verts
⊢ ∃! w, (M.induce (Subtype.val '' (↑c).supp)).Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
⊢ (p.toSubgraph.spanningCoe.neighborSet v).Nonempty → (p.toSubgraph.spanningCoe.neighborSet v).ncard = 2

Tactic:
hv

Goal state after:
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hv : (p.toSubgraph.spanningCoe.neighborSet v).Nonempty
⊢ (p.toSubgraph.spanningCoe.neighborSet v).ncard = 2
Module: Mathlib.Combinatorics.SimpleGraph.Star

Goal state before:
pp: V : Type u_1
r : V
⊢ (starGraph r).IsAcyclic

Tactic:
refine isAcyclic_iff_forall_adj_isBridge.mpr fun v w hadj ↦ ?_

Goal state after:
V : Type u_1
r v w : V
hadj : (starGraph r).Adj v w
⊢ (starGraph r).IsBridge s(v, w)
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
⊢ v ∈ p.toSubgraph.verts → ∀ (w : V), G.Adj v w → p.toSubgraph.Adj v w

Tactic:
hv

Goal state after:
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), G.Adj v w → p.toSubgraph.Adj v w
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)
hn : ¬H.IsCompleteMultipartite
k : ℕ
w✝⁴ w✝³ w✝² : α
w✝¹ w✝ : Finset α
hw : H.IsFiveWheelLike (r + 1) k w✝⁴ w✝³ w✝² w✝¹ w✝
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
⊢ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) * (2 * r + 2 + k + 3) * (3 * r + 4).succ ≤
    (3 * r + 2) * ‖α‖ * (2 * r + 2 + k + 2).succ

Tactic:
apply (Nat.mul_le_mul_right _ (Nat.div_mul_le_self ..)).trans

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
k : ℕ
w✝⁴ w✝³ w✝² : α
w✝¹ w✝ : Finset α
hw : H.IsFiveWheelLike (r + 1) k w✝⁴ w✝³ w✝² w✝¹ w✝
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
⊢ (2 * (r + 1) + k) * ‖α‖ * (3 * r + 4).succ ≤ (3 * r + 2) * ‖α‖ * (2 * r + 2 + k + 2).succ
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ≃g H
c : Set W
h : G.IsVertexCover (⇑f ⁻¹' c)
⊢ H.IsVertexCover c

Tactic:
simpa [← RelIso.image_eq_preimage_symm, Set.image_preimage_eq _ f.surjective]
      using h.preimage f.symm

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
⊢ M2.IsMatching

Tactic:
refine .iSup hcomplMatch_match fun i j hij ↦ (?_ : Disjoint _ _)

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
i j : G.deleteUniversalVerts.coe.ConnectedComponent
hij : i ≠ j
⊢ Disjoint (complMatch i).support (complMatch j).support
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
⊢ v ∈ Set.univ \ G.universalVerts → v ∈ M1.verts ∪ M2.verts

Tactic:
hv

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
hv : v ∈ Set.univ \ G.universalVerts
⊢ v ∈ M1.verts ∪ M2.verts
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case intro.refine_2
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val✝ : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
⊢ (M ⊔ M').IsSpanning

Tactic:
rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
    exact M.verts.union_compl_self

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

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

Tactic:
cases psub m n

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.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
a : ℕ × ℕ
⊢ (fun x1 x2 ↦ x1 ≤ x2) a.1 a.2 ∧ swap (fun x1 x2 ↦ x1 ≤ x2) a.1 a.2 ↔ (fun a b ↦ a = b) a.1 a.2

Tactic:
by simp [le_antisymm_iff]

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

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
inst✝ : Finite α
f : α → σ
l : List α
left✝ : l.Nodup
m : ∀ (x : α), x ∈ l
this : DecidableEq α
a : α
⊢ (List.map f l)[List.idxOf a l]? = some (f a)

Tactic:
List.getElem?_map,

Goal state after:
α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
inst✝ : Finite α
f : α → σ
l : List α
left✝ : l.Nodup
m : ∀ (x : α), x ∈ l
this : DecidableEq α
a : α
⊢ Option.map f l[List.idxOf a l]? = some (f a)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case zero
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
k : ℕ
kn : n ≤ k + 0
⊢ Acc (lbp p) k

Tactic:
refine ⟨_, fun y r => ?_⟩; rcases r with ⟨rfl, a⟩

Goal state after:
case zero
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
k : ℕ
kn : n ≤ k + 0
a : ∀ k_1 ≤ k, false ∈ p k_1
⊢ Acc (lbp p) (k + 1)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case succ
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
⊢ Acc (lbp p) k

Tactic:
refine ⟨_, fun y r => ?_⟩; rcases r with ⟨rfl, a⟩

Goal state after:
case succ
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
a : ∀ k_1 ≤ k, false ∈ p k_1
⊢ Acc (lbp p) (k + 1)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
⊢ Primrec Subtype.val

Tactic:
by
  let := Primcodable.subtype hp
  refine (Primcodable.prim (Subtype p)).of_eq fun n => ?_
  rcases @decode (Subtype p) _ n with (_ | ⟨a, h⟩) <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hf : PrimrecPred p
⊢ Primrec₂ fun a ↦ Option.guard fun x ↦ decide (p x)

Tactic:
simp only [Primrec₂, Option.guard, decide_eq_true_eq]

Goal state after:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hf : PrimrecPred p
⊢ Primrec fun p_1 ↦ if p p_1.2 then some p_1.2 else none
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case prec.succ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Nat.Partrec ↑f✝
pg : Nat.Partrec ↑g✝
n m : ℕ
IH :
  Nat.rec (f✝ (unpair n).1) (fun y IH ↦ g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) m ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH ↦ IH.bind fun i ↦ Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) m
⊢ Nat.rec (f✝ (unpair n).1) (fun y IH ↦ g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) (m + 1) ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH ↦ IH.bind fun i ↦ Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) (m + 1)

Tactic:
simp only [mem_bind_iff, mem_some_iff]

Goal state after:
case prec.succ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Nat.Partrec ↑f✝
pg : Nat.Partrec ↑g✝
n m : ℕ
IH :
  Nat.rec (f✝ (unpair n).1) (fun y IH ↦ g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) m ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH ↦ IH.bind fun i ↦ Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) m
⊢ ∃
    a ∈
      Nat.rec (Part.some (f✝ (unpair n).1))
        (fun y IH ↦ IH.bind fun i ↦ Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) m,
    g✝
        (Nat.pair (unpair n).1
          (Nat.pair m (Nat.rec (f✝ (unpair n).1) (fun y IH ↦ g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) m))) =
      g✝ (Nat.pair (unpair n).1 (Nat.pair m a))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_2
α : 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 : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
⊢ ∀ (k : ℕ), Sum.inr a₁ ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

Tactic:
apply @PFun.fixInduction _ _ _ _ _ _ h₁

Goal state after:
case refine_2
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α := ⋯
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
⊢ ∀ (a' : α),
    b ∈ f.fix a' →
      (∀ (a'' : α),
          Sum.inr a'' ∈ f a' →
            ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m) →
        ∀ (k : ℕ), Sum.inr a' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case comp
n : ℕ
f✝¹ : List.Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
hf : Primrec' fun v ↦ f✝ v.head
hg : Primrec' fun v ↦ g✝ v.head
⊢ Primrec' fun v ↦ (fun n ↦ f✝ (g✝ n)) v.head

Tactic:
exact hf.comp₁ _ hg

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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
⊢ False

Tactic:
rw [Fintype.card_eq_nat_card] at hc

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Nat.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
⊢ False
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ ↑n ^ p a b * ↑n * (c₂ * g ↑n / ↑n ^ (p a b + 1)) = c₂ * (↑n ^ (p a b + 1) / ↑n ^ (p a b + 1)) * g ↑n

Tactic:
by
        rw [← Real.rpow_add_one (by positivity) (p a b)]; ring

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_2
c : Code
⊢ Nat.Partrec c.eval

Tactic:
induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'

Goal state after: