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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ ¬(G □ H).Reachable x y ↔ ¬G.Reachable x.1 y.1 ∨ ¬H.Reachable x.2 y.2

Tactic:
reachable_boxProd,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ ¬(G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2) ↔ ¬G.Reachable x.1 y.1 ∨ ¬H.Reachable x.2 y.2
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
sintert : (s ∩ t).Nonempty
⊢ (⊤.induce (s ∪ t)).Connected

Tactic:
preconnected_induce_iff

Goal state after:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : (⊤.induce s).Preconnected
tconn : (⊤.induce t).Preconnected
sintert : (s ∩ t).Nonempty
⊢ (⊤.induce (s ∪ t)).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (⊤.induce (s ∪ t)).Connected

Tactic:
preconnected_induce_iff

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Preconnected
tconn : (⊤.induce t).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (⊤.induce (s ∪ t)).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ val✝ : V
huv : (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inl val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝))

Tactic:
simp_all [cG.valid, cH.valid]

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

Goal state before:
pp: case inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ : V
val✝ : W
huv : (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inr val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝))

Tactic:
simp_all [cG.valid, cH.valid]

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

Goal state before:
pp: case inr.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ : W
val✝ : V
huv : (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inl val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝))

Tactic:
simp_all [cG.valid, cH.valid]

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

Goal state before:
pp: case inr.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ val✝ : W
huv : (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝))

Tactic:
simp_all [cG.valid, cH.valid]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
t : Set V
tS : t ∈ S
wt : w ∈ t
⊢ ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩

Tactic:
refine ⟨s ∪ t, Set.union_subset (Set.subset_sUnion_of_mem sS) (Set.subset_sUnion_of_mem tS),
          Or.inl vs, Or.inr wt,
          induce_union_connected (Sc sS).preconnected (Sc tS).preconnected (Snd sS tS) _ _⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
V : Type u_3
inst✝ : DecidableEq V
G : SimpleGraph V
u v✝ : V
w : G.Walk u v✝
hw : w.IsPath
v : ↑w.toSubgraph.verts
⊢ List.idxOf (↑v) w.support < w.length + 1

Tactic:
grind [w.mem_verts_toSubgraph]

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

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
s : Set G
⊢ circulantGraph s = circulantGraph (s \ {0})

Tactic:
ext (u v : G)

Goal state after:
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
⊢ (circulantGraph s).Adj u v ↔ (circulantGraph (s \ {0})).Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
⊢ a = b

Tactic:
· have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b :=
        congrArg (·.snd) h
      have h3 := congrArg length (hf' _ ((f _).tail.copy h1 rfl) ?_)
      · rw [length_copy, ← add_left_inj 1,
          length_tail_add_one (not_nil_of_ne (by simpa using ha))] at h3
        lia
      · simp only [isPath_copy]
        exact (hf _).tail

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

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
this : (α : Type u_1) → [Finite α] → Fintype α
T : SimpleGraph V
hle : T ≤ G
hT : T.IsTree
⊢ T.edgeFinset.card ≤ Fintype.card ↑G.edgeSet

Tactic:
← edgeFinset_card

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
this : (α : Type u_1) → [Finite α] → Fintype α
T : SimpleGraph V
hle : T ≤ G
hT : T.IsTree
⊢ T.edgeFinset.card ≤ G.edgeFinset.card
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 u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
l2 : (G.replaceVertex s t).degree u = G.degree u - 1
⊢ ∃ w, G.Adj u w

Tactic:
use t, h.symm

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| r * t

Tactic:
rw [← Nat.sub_one_add_one_eq_of_pos v.2.pos, Nat.mul_add_one, mul_comm r (t - 1)]

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| (t - 1) * r + r
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case inj'.inr
α : 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
hne✝ : i₁ = i₂ → j₁ ≠ j₂
hne : i₁ ≠ i₂
⊢ ↑((fₜ (fᵣ i₁)) j₁) ≠ ↑((fₜ (fᵣ i₂)) j₂)

Tactic:
refine (K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop).ne
        exact Subtype.ext_iff.ne.mp <| fᵣ.injective.ne hne

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
⊢ Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t) ↔ ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s

Tactic:
refine ⟨fun ⟨K'⟩ ↦ ?_, fun ⟨K, s, hs, hadj⟩ ↦ ?_⟩

Goal state after:
case neg.refine_1
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
⊢ ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s

case neg.refine_2
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
s : Finset V
nhs_mem : s ∉ K.parts
hs : insert s K.parts = K'.parts
⊢ s ∈ K'.parts

Tactic:
simp [← hs]

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

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
⊢ zarankiewicz m n s t =
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
let e₂ := completeBipartiteGraphCongr
    (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)

Goal state after:
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
⊢ zarankiewicz m n s t =
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
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:
· obtain ⟨H, _, maxH⟩ := exists_isTuranMaximal (V := V) hr
    convert! maxH.2 cf
    rw [((isTuranMaximal_iff_nonempty_iso_turanGraph hr).mp maxH).some.card_edgeFinset_eq,
      card_edgeFinset_turanGraph]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : ι → Set α
⊢ (⋃ i, s i).ncard ≤ ∑ i, (s i).ncard

Tactic:
by
  simpa using Finset.univ.set_ncard_biUnion_le s

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

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

Tactic:
| inr =>

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

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ ((∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
        ∑ y, ∑ x_1, if G.Adj y x_1 then x x_1 * x x_1 - x x_1 * x y else 0) /
      2 =
    (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
← sum_add_distrib,

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ (∑ x_1,
        ∑ x_2,
          ((if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
            if G.Adj x_1 x_2 then x x_2 * x x_2 - x x_2 * x x_1 else 0)) /
      2 =
    (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : u ≠ v
hs : s(v, u) ∉ p.edges
c : (completeGraph V).Walk v v := cons ⋯ (Walk.mapLe ⋯ p)
this : p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe
⊢ c.IsCycle

Tactic:
by simp [Walk.cons_isCycle_iff, c, hp, hs]

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

Goal state before:
pp: μ : YoungDiagram
j : ℕ
⊢ μ.colLen j = (μ.col j).card

Tactic:
by
  simp [col_eq_prod]

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
pt : PlacedTile ps
a b : G
r : a⁻¹ * b ∈ Subgroup.map (MulAction.stabilizer G ↑(↑ps pt.index)).subtype (↑ps pt.index).symmetries
⊢ { index := pt.index, groupElts := ↑(g * a) } = { index := pt.index, groupElts := ↑(g * b) }

Tactic:
refine PlacedTile.ext rfl ?_

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
pt : PlacedTile ps
a b : G
r : a⁻¹ * b ∈ Subgroup.map (MulAction.stabilizer G ↑(↑ps pt.index)).subtype (↑ps pt.index).symmetries
⊢ { index := pt.index, groupElts := ↑(g * a) }.groupElts ≍ { index := pt.index, groupElts := ↑(g * b) }.groupElts
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 : α × β → σ
⊢ Primrec₂ (Function.curry f) ↔ Primrec f

Tactic:
rw [← uncurry, Function.uncurry_curry]

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
⊢ Primrec₂ fun p ↦ encode

Tactic:
exact encode_iff.mpr snd

Goal state after:
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
  refine (Nat.Primrec.pred.comp hf).of_eq fun n => ?_
  generalize hx : @decode α _ n = x
  cases x <;> simp

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

Goal state before:
pp: β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
i : ℕ
hi : i ≤ m b + 1
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph : ∀ {bs bs' : List β}, bs' ⊆ bs → mapGraph (List.map (fun x ↦ (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph (graph b i) (l b')))) (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
⊢ graph b i = List.map (fun x ↦ (x, f x)) (bindList b (m b + 1 - i))

Tactic:
induction i with

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

Goal state before:
pp: f : ℕ → ℕ → ℕ
hf : Primrec' fun v ↦ f v.head v.tail.head
n : ℕ
g h : List.Vector ℕ n → ℕ
hg : Primrec' g
hh : Primrec' h
⊢ Primrec' fun v ↦ f (g v) (h v)

Tactic:
by
  simpa using hf.comp' (hg.cons <| hh.cons Primrec'.nil)

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : 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
this :
  ∀ (a' : α),
    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
⊢ Sum.inr a ∈ F a 0

Tactic:
by simp [F]

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

Goal state before:
pp: f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
left✝ : c₁ > 0
c₂ : ℝ
hc₂ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c₂ * f x

Tactic:
filter_upwards [h]

Goal state after:
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
left✝ : c₁ > 0
c₂ : ℝ
hc₂ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, f u ≤ c₂ * f a
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
hc₁ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c₁ * f x ≤ f u

Tactic:
filter_upwards [h]

Goal state after:
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
hc₁ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, c₁ * f a ≤ f u
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:

Tactic:
(b i : ℝ) * n - r i n
    _ = ‖b i * n‖ - ‖(r i n : ℝ)‖ := by
      simp only [norm_mul, RCLike.norm_natCast, Real.norm_of_nonneg h₁]
    _ ≤ ‖(b i * n : ℝ) - r i n‖ := norm_sub_norm_le _ _
    _ = ‖(r i n : ℝ) - b i * n‖ := norm_sub_rev _ _
    _ ≤ n / log n ^ 2 := hn i

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
hvOdd : Odd (Nat.card V)
⊢ ∃ u, G.IsTutteViolator u

Tactic:
exact ⟨∅, .empty hvOdd⟩

Goal state after:
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 : α
h : Tendsto (fun n ↦ log (b i * ↑n)) atTop atTop
⊢ ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * ↑x)

Tactic:
exact h.eventually_gt_atTop 0

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

Goal state before:
pp: x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ DifferentiableAt ℝ ε x

Tactic:
change DifferentiableAt ℝ (fun z => 1 / log z) x

Goal state after:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ DifferentiableAt ℝ (fun z ↦ 1 / log z) x
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)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ 0 ≤ ε (b i * ↑n) - ε ↑n

Tactic:
refine sub_nonneg_of_le <|
            (strictAntiOn_smoothingFn.le_iff_ge ?n_gt_one ?bn_gt_one).mpr ?le

Goal state after:
case n_gt_one
α : 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)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ ↑n ∈ Set.Ioi 1

case bn_gt_one
α : 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)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ b i * ↑n ∈ Set.Ioi 1

case le
α : 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)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ b i * ↑n ≤ ↑n
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)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ b i * ↑n ∈ Set.Ioi 1

Tactic:
calc 1 = b i * (b i)⁻¹ := by rw [mul_inv_cancel₀ (by positivity)]
              _ ≤ b i * ⌈(b i)⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
              _ < b i * n := by gcongr

Goal state after:
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
⊢ Tendsto (fun p ↦ ∑ i, a i * b i ^ p) atTop (𝓝 0)

Tactic:
by
  have h₁ : Finset.univ.sum (fun _ : α => (0 : ℝ)) = 0 := by simp
  rw [← h₁]
  refine tendsto_finsetSum (univ : Finset α) (fun i _ => ?_)
  rw [← mul_zero (a i)]
  refine Tendsto.mul (by simp) <| tendsto_rpow_atTop_of_base_lt_one _ ?_ (R.b_lt_one i)
  have := R.b_pos i
  linarith

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

Goal state before:
pp: f : ℝ → ℝ
hf✝ : GrowsPolynomially f
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₁ * (-f) x) (c₂ * (-f) x)

Tactic:
refine ⟨c₂, hc₂_mem, c₁, hc₁_mem, ?_⟩

Goal state after:
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₂ * (-f) x) (c₁ * (-f) x)