mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ ¬G.Adj s t ↔ h.finpartition.part s = h.finpartition.part t

Tactic:
change h.setoid.r s t ↔ _
  rw [← Finpartition.mem_part_ofSetoid_iff_rel]
  let fp := h.finpartition
  change t ∈ fp.part s ↔ fp.part s = fp.part t
  rw [fp.mem_part_iff_part_eq_part (mem_univ t) (mem_univ s), eq_comm]

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

Goal state before:
pp: case e_a
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ {t | ¬G.Adj s t} = h.finpartition.part s

Tactic:
ext

Goal state after:
case e_a
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ {t | ¬G.Adj s t} ↔ a✝ ∈ h.finpartition.part s
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
⊢ G.IsCompleteMultipartite ↔ ∃ ι V, ∃ (_ : ∀ (i : ι), Nonempty (V i)), Nonempty (G ≃g completeMultipartiteGraph V)

Tactic:
constructor

Goal state after:
case mp
α : Type u
G : SimpleGraph α
⊢ G.IsCompleteMultipartite → ∃ ι V, ∃ (_ : ∀ (i : ι), Nonempty (V i)), Nonempty (G ≃g completeMultipartiteGraph V)

case mpr
α : Type u
G : SimpleGraph α
⊢ (∃ ι V, ∃ (_ : ∀ (i : ι), Nonempty (V i)), Nonempty (G ≃g completeMultipartiteGraph V)) → G.IsCompleteMultipartite
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
T : SimpleGraph V
left✝ : T ≤ G
T_isTree : T.IsTree
hT : T.Connected
isAcyclic✝ : T.IsAcyclic
this : Fintype V
⊢ ∃ v, (induce {v}ᶜ G).Connected

Tactic:
obtain ⟨v, hv⟩ := T_isTree.exists_vert_degree_one_of_nontrivial

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Finite V
inst✝ : Nontrivial V
hconn : G.Connected
T : SimpleGraph V
left✝ : T ≤ G
T_isTree : T.IsTree
hT : T.Connected
isAcyclic✝ : T.IsAcyclic
this : Fintype V
v : V
hv : T.degree v = 1
⊢ ∃ v, (induce {v}ᶜ G).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ G.Reachable u v ↔ ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ G.Reachable u v → ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty

case mpr
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ (∃ n, (G.finsetWalkLength (↑n) u v).Nonempty) → G.Reachable u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝⁴ : DecidableEq V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
inst✝¹ : Fintype ↑c'.supp
inst✝ : DecidablePred fun c ↦ c.supp ⊆ c'.supp
x : G.ConnectedComponent
x✝¹ : x ∈ ↑{c | c.supp ⊆ c'.supp}
y : G.ConnectedComponent
x✝ : y ∈ ↑{c | c.supp ⊆ c'.supp}
hxy : x ≠ y
⊢ (Disjoint on fun c ↦ c.supp.toFinset) x y

Tactic:
by simpa using pairwise_disjoint_supp_connectedComponent _ hxy

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

Goal state before:
pp: r t : ℕ
v : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).neighborSet v = {v.1}ᶜ ×ˢ Set.univ

Tactic:
ext

Goal state after:
r t : ℕ
v x✝ : Fin r × Fin t
⊢ x✝ ∈ (completeEquipartiteGraph r t).neighborSet v ↔ x✝ ∈ {v.1}ᶜ ×ˢ Set.univ
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
v : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).neighborFinset v = {v.1}ᶜ ×ˢ univ

Tactic:
ext

Goal state after:
r t : ℕ
v a✝ : Fin r × Fin t
⊢ a✝ ∈ (completeEquipartiteGraph r t).neighborFinset v ↔ a✝ ∈ {v.1}ᶜ ×ˢ univ
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd G.oddComponents.ncard ↔ Odd #(univ.biUnion fun x ↦ x.supp.toFinset)

Tactic:
rw [Finset.card_biUnion
    (fun x _ y _ hxy ↦ Set.disjoint_toFinset.mpr (pairwise_disjoint_supp_connectedComponent _ hxy))]

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd G.oddComponents.ncard ↔ Odd (∑ u, #u.supp.toFinset)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u ≤ 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u ≤ 1 → ∀ (v : α), u ≠ v → G.Adj u v

case mpr
α : Type u_1
G : SimpleGraph α
u : α
⊢ (∀ (v : α), u ≠ v → G.Adj u v) → G.eccent u ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: 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

Tactic:
constructor

Goal state after:
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

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.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
⊢ C.supp.Infinite ↔ ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
⊢ C.supp.Infinite → ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C

case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
⊢ (∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C) → C.supp.Infinite
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K L M : Set V
x✝ : (Finset V)ᵒᵖ
⊢ ↾ComponentCompl.hom ⋯ = 𝟙 (G.ComponentCompl ↑(Opposite.unop x✝))

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
K L M : Set V
x✝² : (Finset V)ᵒᵖ
x✝¹ : G.ComponentCompl ↑(Opposite.unop x✝²)
x✝ : V
⊢ x✝ ∈ ((ConcreteCategory.hom (↾ComponentCompl.hom ⋯)).toFun x✝¹).supp ↔
    x✝ ∈ ((ConcreteCategory.hom (𝟙 (G.ComponentCompl ↑(Opposite.unop x✝²)))).toFun x✝¹).supp
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r✝ r : ℕ
h : Maximal (fun H ↦ H.CliqueFree (r + 1 + 1)) G
hc : G.Colorable (r + 1)
⊢ G.IsCompleteMultipartite

Tactic:
contrapose hc

Goal state after:
α : Type u_1
G : SimpleGraph α
r✝ r : ℕ
h : Maximal (fun H ↦ H.CliqueFree (r + 1 + 1)) G
hc : ¬G.IsCompleteMultipartite
⊢ ¬G.Colorable (r + 1)
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
⊢ (M ⊔ M').IsMatching

Tactic:
by
  intro v hv
  have aux {N N' : Subgraph G} (hN : N.IsMatching) (hd : Disjoint N.support N'.support)
    (hmN : v ∈ N.verts) : ∃! w, (N ⊔ N').Adj v w := by
    obtain ⟨w, hw⟩ := hN hmN
    use w
    refine ⟨sup_adj.mpr (.inl hw.1), ?_⟩
    intro y hy
    cases hy with
    | inl h => exact hw.2 y h
    | inr h =>
      rw [Set.disjoint_left] at hd
      simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, h⟩] using @hd v
  cases Set.mem_or_mem_of_mem_union hv with
  | inl hmM => exact aux hM hd hmM
  | inr hmM' =>
    rw [sup_comm]
    exact aux hM' (Disjoint.symm hd) hmM'

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
P : G.Partition
v✝ w✝ : V
hvw : G.Adj v✝ w✝
⊢ ⟨P.partOfVertex v✝, ⋯⟩ ≠ ⟨P.partOfVertex w✝, ⋯⟩

Tactic:
by
    rw [Ne, Subtype.mk_eq_mk]
    exact P.partOfVertex_ne_of_adj hvw

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Partitionable n ↔ G.Colorable n

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Partitionable n → G.Colorable n

case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n → G.Partitionable n
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝ : Fintype V
ℓ : ℕ
v w : V
x✝ : v ≠ w
⊢ filter (Membership.mem (⊥.commonNeighbors v w)) univ = ∅

Tactic:
ext

Goal state after:
V : Type u
inst✝ : Fintype V
ℓ : ℕ
v w : V
x✝ : v ≠ w
a✝ : V
⊢ a✝ ∈ filter (Membership.mem (⊥.commonNeighbors v w)) univ ↔ a✝ ∈ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.IsEulerian ↔ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

Tactic:
constructor

Goal state after:
case mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.IsEulerian → p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

case mpr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ (p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges) → p.IsEulerian
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
⊢ ∃ M, M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts

Tactic:
by
  have hrep := ConnectedComponent.Represents.image_out G.deleteUniversalVerts.coe.oddComponents
  -- First we match one node from each odd component to a universal vertex
  obtain ⟨t, ht, M1, hM1⟩ := Subgraph.IsMatching.exists_of_universalVerts
      (disjoint_image_val_universalVerts _).symm (by
        simp only [IsTutteViolator, not_lt] at h
        rwa [Set.ncard_image_of_injective _ Subtype.val_injective, hrep.ncard_eq])
  -- Then we match all other nodes in components internally
  have exists_complMatch (K : G.deleteUniversalVerts.coe.ConnectedComponent) :
      ∃ M : Subgraph G, M.verts = Subtype.val '' K.supp \ M1.verts ∧ M.IsMatching := by
    have : G.IsClique (Subtype.val '' K.supp \ M1.verts) :=
      ((h' K).of_induce).subset Set.sdiff_subset
    rw [← this.even_iff_exists_isMatching (Set.toFinite _), hM1.1]
    exact even_ncard_image_val_supp_sdiff_image_val_rep_union _ ht hrep
  choose complMatch hcomplMatch_compl hcomplMatch_match using exists_complMatch
  let M2 : Subgraph G := ⨆ K, complMatch K
  have hM2 : M2.IsMatching := by
    refine .iSup hcomplMatch_match fun i j hij ↦ (?_ : Disjoint _ _)
    rw [(hcomplMatch_match i).support_eq_verts, hcomplMatch_compl i,
        (hcomplMatch_match j).support_eq_verts, hcomplMatch_compl j]
    exact Set.disjoint_of_subset Set.sdiff_subset Set.sdiff_subset <|
      Set.disjoint_image_of_injective Subtype.val_injective <|
        SimpleGraph.pairwise_disjoint_supp_connectedComponent _ hij
  have disjointM12 : Disjoint M1.support M2.support := by
    rw [hM1.2.support_eq_verts, hM2.support_eq_verts, Subgraph.verts_iSup,
      Set.disjoint_iUnion_right]
    exact fun K ↦ hcomplMatch_compl K ▸ Set.disjoint_sdiff_right
  -- The only vertices left are indeed contained in universalVerts
  have : (M1.verts ∪ M2.verts)ᶜ ⊆ G.universalVerts := by
    rw [Set.compl_subset_comm, Set.compl_eq_univ_sdiff]
    intro v hv
    by_cases h : v ∈ M1.verts
    · exact M1.verts.mem_union_left _ h
    right
    simp only [Subgraph.verts_iSup, Set.mem_iUnion, M2,
      hcomplMatch_compl]
    use G.deleteUniversalVerts.coe.connectedComponentMk ⟨v, hv⟩
    aesop
  exact ⟨M1 ⊔ M2, hM1.2.sup hM2 disjointM12, this⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hodd : Odd (Nat.card V)
⊢ G.IsTutteViolator ∅

Tactic:
rw [IsTutteViolator, Set.ncard_empty]
  exact ((odd_ncard_oddComponents _).mpr <| by simpa using hodd).pos

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

Goal state before:
pp: ⊢ ↑⊥ = ∅

Tactic:
ext

Goal state after:
x✝ : ℕ × ℕ
⊢ x✝ ∈ ↑⊥ ↔ x✝ ∈ ∅
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ ν : YoungDiagram
⊢ μ.transpose = ν ↔ μ = ν.transpose

Tactic:
constructor

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

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

Goal state before:
pp: case refine_2
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
i₁ : ιₚ
g₁ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index ∧
    ∃ g, ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
⊢ { index := i₁, groupElts := g₁ } = { index := i₁, groupElts := g₂ }

Tactic:
ext

Goal state after:
case refine_2.index
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
i₁ : ιₚ
g₁ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index ∧
    ∃ g, ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
⊢ { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index

case refine_2.groupElts
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
i₁ : ιₚ
g₁ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index ∧
    ∃ g, ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
⊢ { index := i₁, groupElts := g₁ }.groupElts ≍ { index := i₁, groupElts := g₂ }.groupElts
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: m : ℕ
⊢ ppred 0 = some m ↔ m.succ = 0

Tactic:
constructor

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

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

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

Tactic:
constructor

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

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

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

Tactic:
constructor

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

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

Goal state before:
pp: ⊢ Nat.Primrec fun n ↦ n + 1

Tactic:
constructor

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
⊢ (Primrec fun a ↦ ↑(f a)) ↔ Primrec f

Tactic:
refine ⟨fun h => ?_, fun hf => subtype_val.comp hf⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a ↦ ↑(f a)
⊢ Primrec f
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case zero
n : ℕ
f✝ : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v ↦ (fun x ↦ 0) v.head

Tactic:
exact const 0

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ (fun n ↦ ↑n * 1⁻¹) = fun n ↦ ↑n

Tactic:
ext

Goal state after:
x✝ : ℕ
⊢ ↑x✝ * 1⁻¹ = ↑x✝
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
⊢ ∃ u, G.IsTutteViolator u

Tactic:
by_cases hvOdd : Odd (Nat.card V)

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvOdd : Odd (Nat.card V)
⊢ ∃ u, G.IsTutteViolator u

case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvOdd : ¬Odd (Nat.card V)
⊢ ∃ u, G.IsTutteViolator u
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ p * z ^ (p - 1) * 1) = fun z ↦ p * z ^ (p - 1)

Tactic:
ext

Goal state after:
p : ℝ
hp : p ≠ 0
x✝ : ℝ
⊢ p * x✝ ^ (p - 1) * 1 = p * x✝ ^ (p - 1)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ z ^ (p - 1) / 1) = fun z ↦ z ^ (p - 1)

Tactic:
ext

Goal state after:
p : ℝ
hp : p ≠ 0
x✝ : ℝ
⊢ x✝ ^ (p - 1) / 1 = x✝ ^ (p - 1)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
⊢ (fun x ↦ x ^ (p a b - 1) * 1) = fun x ↦ x ^ (p a b - 1)

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x✝ : ℝ
⊢ x✝ ^ (p a b - 1) * 1 = x✝ ^ (p a b - 1)
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
i : α
⊢ (fun n ↦ (log ↑n - log (b i) - log ↑n) / ((log (b i) + log ↑n) * log ↑n)) = fun n ↦
    -log (b i) / ((log (b i) + log ↑n) * log ↑n)

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x✝ : ℕ
⊢ (log ↑x✝ - log (b i) - log ↑x✝) / ((log (b i) + log ↑x✝) * log ↑x✝) = -log (b i) / ((log (b i) + log ↑x✝) * log ↑x✝)
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
i : α
⊢ (fun n ↦ log (b i) + log ↑n) = fun n ↦ log ↑n + log (b i)

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x✝ : ℕ
⊢ log (b i) + log ↑x✝ = log ↑x✝ + log (b i)
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
i : α
⊢ (fun n ↦ -log (b i) / (log ↑n * log ↑n)) = fun n ↦ -log (b i) / log ↑n ^ 2

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x✝ : ℕ
⊢ -log (b i) / (log ↑x✝ * log ↑x✝) = -log (b i) / log ↑x✝ ^ 2
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ (b : ℝ), n₀ ≤ b → ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
a✝² : n ≥ 1
a✝¹ : ∀ z ∈ Set.Ico (max n₀ 2) (2 ^ n * max n₀ 2), f z = f (max n₀ 2)
z : ℝ
a✝ : z ∈ Set.Ico (2 ^ n * max n₀ 2) (2 ^ (n + 1) * max n₀ 2)
⊢ max n₀ 2 ≤ 2 ^ n * max n₀ 2

Tactic:
simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case neg.inr
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x ≤ 0) ∧ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0

Tactic:
exact ⟨h', h⟩

Goal state after:
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
⊢ (fun x ↦ x ^ (p a b - 1) * 1) = fun x ↦ x ^ (p a b - 1)

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x✝ : ℝ
⊢ x✝ ^ (p a b - 1) * 1 = x✝ ^ (p a b - 1)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, 0 < (1 - ε ↑n) * asympBound g a b n

pp: case refine_3
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀,
      ∀ᶠ (n : ℕ) in atTop,
        ∀ C ≥ C₀,
          (∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)) → T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)

Tactic:
· filter_upwards [R.eventually_asympBound_pos, eventually_one_sub_smoothingFn_pos] with n hn hn₂
    positivity

Goal state after:
case refine_3
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀,
      ∀ᶠ (n : ℕ) in atTop,
        ∀ C ≥ C₀,
          (∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)) → T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)