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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
⊢ 𝒜.shatterer.Shatters s ↔ 𝒜.Shatters s

Tactic:
simp_rw [← mem_shatterer, shatterer_idem]

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

Goal state before:
pp: V : Type u
s : Set (Sym2 V)
⊢ (fromEdgeSet s).Reachable = Relation.ReflTransGen (Sym2.ToRel s)

Tactic:
reachable_eq_reflTransGen,

Goal state after:
V : Type u
s : Set (Sym2 V)
⊢ Relation.ReflTransGen (fromEdgeSet s).Adj = Relation.ReflTransGen (Sym2.ToRel s)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
⊢ v ∈ H.verts

Tactic:
let rec aux {v' : V} (hv' : v' ∈ H.verts) (p : G.Walk v' v) : v ∈ H.verts := by
    by_cases hnp : p.Nil
    · exact hnp.eq ▸ hv'
    exact aux (H.edge_vert (h _ hv' _ (Walk.adj_snd hnp)).symm) p.tail
  termination_by p.length
  decreasing_by {
    rw [← Walk.length_tail_add_one hnp]
    lia
  }

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
⊢ v ∈ H.verts
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
m : ℕ
⊢ m < k → m < n

Tactic:
apply forall_lt_iff_le.2 hkn

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
⊢ G.chromaticNumber ≤ ↑(card V)

Tactic:
rw [← chromaticNumber_top]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
⊢ G.chromaticNumber ≤ ⊤.chromaticNumber
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
⊢ G.neighborSet v ⊆ t

Tactic:
by
  rw [isBipartiteWith_neighborSet h hv]
  exact Set.sep_subset t (G.Adj v ·)

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet v)
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ {w ∈ t | G.Adj v w} ⊆ t

Tactic:
exact filter_subset (G.Adj v ·) t

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst✝ : Fintype ↑(G.neighborSet u)
h : G.IsEdgeReachable k u v
huv : u ≠ v
⊢ k ≤ G.degree u

Tactic:
by_contra! hh
  rw [← card_incidenceSet_eq_degree, ← ENat.natCast_lt_natCast, Set.coe_fintypeCard] at hh
  obtain ⟨w, _⟩ := h hh |>.exists_isPath
  simpa using w.adj_snd <| mt Walk.Nil.eq huv

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
hG : G.IsBipartiteWith s t
⊢ G.edgeSet.encard ≤ s.encard * t.encard

Tactic:
classical
  grw [hG.edgeSetEmbeddingCompleteBipartiteGraph.encard_le]
  simp [encard_edgeSet_completeBipartiteGraph]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(G.neighborSet x.1)
inst✝ : Fintype ↑(H.neighborSet x.2)
y : α × β
⊢ G.Adj x.1 y.1 ∧ y.2 = x.2 ∨ y.1 = x.1 ∧ H.Adj x.2 y.2 ↔ (G □ H).Adj x ((Equiv.refl (α × β)) y)

Tactic:
Equiv.refl_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(G.neighborSet x.1)
inst✝ : Fintype ↑(H.neighborSet x.2)
y : α × β
⊢ G.Adj x.1 y.1 ∧ y.2 = x.2 ∨ y.1 = x.1 ∧ H.Adj x.2 y.2 ↔ (G □ H).Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ (pathGraph n).Adj u v ↔ ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u

Tactic:
simp [pathGraph, hasse]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
S : Set (Set V)
Sn : S.Nonempty
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
⊢ (induce (⋃₀ S) G).Connected

Tactic:
by
  obtain ⟨s, sS⟩ := Sn
  obtain ⟨v, vs⟩ := (Sc sS).nonempty
  apply G.induce_connected_of_patches _ (Set.subset_sUnion_of_mem sS vs)
  rintro w hw
  simp only [Set.mem_sUnion] at hw
  obtain ⟨t, tS, wt⟩ := hw
  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.Connectivity.Subgraph

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ ∃ a ∈ t, v ∈ (Nonempty.some ⋯).support

Tactic:
exact ⟨v, vt, Walk.end_mem_support _⟩

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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ : ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
i j : V ⊕ V
i' : V
hi' : i' ∈ left
hi : Sum.inl i' = i
j' : V
hj' : j' ∈ right
hj : Sum.inr j' = j
⊢ G.bipartiteDoubleCover.Adj i j

Tactic:
simpa [← hi, ← hj] using h hi' hj'

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

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

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

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : AddZeroClass α
inst✝¹ : One α
H : SimpleGraph V
inst✝ : DecidableRel H.Adj
h : IsCompl G H
⊢ adjMatrix α G + adjMatrix α H = adjMatrix α G + adjMatrix α Gᶜ

Tactic:
by have := h.compl_eq; subst this; congr

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

Goal state before:
pp: 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
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
this : (f x).takeUntil y hy = cons h nil
⊢ False

Tactic:
← take_spec _ hy

Goal state after:
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
x y : V
h : G.Adj x y
hy : y ∈ (f x).support
h' : (((f x).takeUntil y hy).append ((f x).dropUntil y hy)).length ≤ (f y).length
this : (f x).takeUntil y hy = cons h nil
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
⊢ ∃ H x, H.IsTuranMaximal r

Tactic:
by
  simpa [IsTuranMaximal, exists_isExtremal_iff_exists] using ⟨⊥, cliqueFree_bot (by lia)⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsTree ↔ Nonempty V ∧ Maximal IsAcyclic G

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨_, h⟩ ↦ G.maximal_isAcyclic_iff_isTree.mp h⟩
  have := h.nonempty
  exact ⟨this, G.maximal_isAcyclic_iff_isTree.mpr h⟩

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

Goal state before:
pp: n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ (cycleGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩

Tactic:
simp [cycleGraph_adj', Fin.sub_val_of_le]

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

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
x : V
hx : x ∈ s
h : G.connectedComponentMk x ∈ C
⊢ ∀ y ∈ s, G.connectedComponentMk y = G.connectedComponentMk x → y = x

Tactic:
exact fun y hy hyx ↦ hrep.2.1 hy hx hyx

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

Goal state before:
pp: case inr.a
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
this : w % r = x % r
⊢ w = x

Tactic:
rwa [Nat.mod_eq_of_lt mw.1, Nat.mod_eq_of_lt mx.1] at this

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

Goal state before:
pp: case neg.refine_2.refine_3
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
⊢ #s = t ∧ ∀ a ∈ K.parts, #a = t

Tactic:
exact ⟨hs, fun p ↦ K.card_mem_parts⟩

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
K L : Finset V
h : K ⊆ L
v : V
vL : v ∉ ↑L
vK : v ∉ ↑K
Cinf : (G.componentComplMk vK).supp.Infinite
⊢ ∃ D, hom h D = G.componentComplMk vK

Tactic:
exact ⟨componentComplMk _ vL, rfl⟩

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) +
      ∑ i, ∑ j, if G.Adj j i then x i * x i - x i * x j else 0) /
    2

Tactic:
enter [1, 2]; rw [Finset.sum_comm]

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
| ∑ y, ∑ x_1, if G.Adj y x_1 then x x_1 * x x_1 - x x_1 * x y else 0
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: case refine_2
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✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
x : V → R
⊢ 0 ≤ x ⬝ᵥ lapMatrix R G *ᵥ x

Tactic:
← toLinearMap₂'_apply',

Goal state after:
case refine_2
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✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
x : V → R
⊢ 0 ≤ (((toLinearMap₂' R) (lapMatrix R G)) x) x
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
⊢ c.toSimpleGraph.spanningCoe.IsCycles

Tactic:
intro v ⟨w, hw⟩
  rw [mem_neighborSet, c.adj_spanningCoe_toSimpleGraph] at hw
  rw [← h ⟨w, hw.2⟩]
  congr 1
  ext w'
  simp only [mem_neighborSet, c.adj_spanningCoe_toSimpleGraph, hw, true_and]

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

Goal state before:
pp: case succ
α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn (n + 1) 1 fun n ↦ Nat.casesOn (encode (decode n)) 0 fun n ↦ n.succ.succ) = encode (decode (n + 1))

Tactic:
rw [decode_option_succ]
        cases H : @decode α _ n <;> simp [H]

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

Goal state before:
pp: ⊢ Primrec₂ Nat.pair

Tactic:
simp [Primrec₂, Primrec]; constructor

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ encode
      (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) n)) =
    encode (decode n)

Tactic:
apply Nat.case_strong_induction_on n

Goal state after:
case hz
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := ⋯
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ encode
      (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) 0)) =
    encode (decode 0)

case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := ⋯
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ m ≤ n,
        encode
            (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
              (ofNat (List ℕ) m)) =
          encode (decode m)) →
      encode
          (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) (n + 1))) =
        encode (decode (n + 1))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
f : α → ℕ
h₂ : PrimrecRel fun a b ↦ f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
⊢ Primrec f

Tactic:
refine (nat_findGreatest pg h₂).of_eq fun n => ?_

Goal state after:
α : Type u_1
inst✝ : Primcodable α
f : α → ℕ
h₂ : PrimrecRel fun a b ↦ f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
n : α
⊢ Nat.findGreatest (fun b ↦ f n = b) (g n) = f n
Module: Mathlib.Computability.Partrec

Goal state before:
pp: this : Primrec₂ fun n m ↦ if n = m.succ then 0 else 1
n : ℕ
⊢ (Nat.rfind fun n_1 ↦
      (fun m ↦ decide (m = 0)) <$> ↑(unpaired fun n m ↦ if n = m.succ then 0 else 1) (Nat.pair n n_1)) =
    ↑n.ppred

Tactic:
cases n
    · exact eq_none_iff.2 (by simp)
    · exact eq_some_iff.2 (by simp; lia)

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
⊢ (Nat.rfind fun n_1 ↦
      (fun m ↦ decide (m = 0)) <$>
        (↑(decode (Nat.pair n n_1))).bind fun a ↦
          Part.map encode ((fun a ↦ Part.map (fun b ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2)) a)) =
    (↑(decode n)).bind fun a ↦ Part.map encode ((fun a ↦ Nat.rfind (p a)) a)

Tactic:
by
    rcases e : decode (α := α) n <;> simp [e, Nat.rfind_zero_none, map_map, map_id']

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

Goal state before:
pp: f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ ↑⌈-logb 2 (x / x₀)⌉₊ ≤ 1 + ↑⌊-logb 2 (x / x₀)⌋₊

Tactic:
rw [add_comm]; exact_mod_cast Nat.ceil_le_floor_add_one _

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
⊢ 0 < b (max_bi b)

Tactic:
by have := R.b_pos (max_bi b); linarith

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

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

Tactic:
match lt_trichotomy c₁ c₂ with
  | .inl hlt => -- c₁ < c₂
    left
    filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg
    have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by
      rw [Set.mem_Icc]
      exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
    have hu := hx (3 / 4 * x) h'
    have hu := Set.nonempty_of_mem hu
    rw [Set.nonempty_Icc] at hu
    have hu' : 0 ≤ (c₂ - c₁) * f x := by linarith
    exact nonneg_of_mul_nonneg_right hu' (by linarith)
  | .inr (.inr hgt) => -- c₂ < c₁
    right
    filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg
    have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by
      rw [Set.mem_Icc]
      exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
    have hu := hx (3 / 4 * x) h'
    have hu := Set.nonempty_of_mem hu
    rw [Set.nonempty_Icc] at hu
    have hu' : (c₁ - c₂) * f x ≤ 0 := by linarith
    exact nonpos_of_mul_nonpos_right hu' (by linarith)
  | .inr (.inl heq) => -- c₁ = c₂
    have hmain : ∃ c, ∀ᶠ x in atTop, f x = c := by
      simp only [heq, Set.Icc_self, Set.mem_singleton_iff] at h
      rw [eventually_atTop] at h
      obtain ⟨n₀, hn₀⟩ := h
      refine ⟨f (max n₀ 2), ?_⟩
      rw [eventually_atTop]
      refine ⟨max n₀ 2, ?_⟩
      refine Real.induction_Ico_mul _ 2 (by norm_num) (by positivity) ?base ?step
      case base => grind
      case step =>
        intro n _ _ z _
        have le_2n : max n₀ 2 ≤ (2 : ℝ) ^ n * max n₀ 2 := by
          simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]
        have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) := by
          grind [mul_assoc]
        grind
    obtain ⟨c, hc⟩ := hmain
    cases le_or_gt 0 c with
    | inl hpos =>
      exact Or.inl <| by filter_upwards [hc] with _ hc; simpa only [hc]
    | inr hneg =>
      right
      filter_upwards [hc] with x hc
      exact le_of_lt <| by simpa only [hc]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
a k : ℕ
⊢ (cf.prec cg).eval (Nat.pair a k.succ) = do
    let ih ← (cf.prec cg).eval (Nat.pair a k)
    cg.eval (Nat.pair a (Nat.pair k ih))

Tactic:
rw [eval, Nat.unpaired, Part.bind_eq_bind, Nat.unpair_pair]
  simp

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case inr
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
this :
  ∀ (n m : Fin (Fintype.card σ + 1)),
    n ≠ m →
      M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x) →
        ↑n ≤ ↑m →
          ∃ q a b c,
            x = a ++ b ++ c ∧
              a.length + b.length ≤ Fintype.card σ ∧
                b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
hle : ¬↑n ≤ ↑m
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t

pp: α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t

Tactic:
· exact this m n hneq.symm heq.symm (le_of_not_ge hle)

Goal state after:
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if (if a = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if b = true then 2 * n + 1 else 2 * n else 0
    else
      if (if b = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if a = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if a = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if b = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2)) =
    if f a b = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
cases a <;> cases b <;> simp

Goal state after:
case false.false
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if m = 0 then if f false true = true then 2 * n else 0
    else
      if n = 0 then if f true false = true then 2 * m else 0
      else if f false false = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    if f false false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

case false.true
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if m = 0 then if f false true = true then 2 * n + 1 else 0
    else
      if f false true = true then bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) + 1
      else bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2)) =
    if f false true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

case true.false
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if n = 0 then if f true false = true then 2 * m + 1 else 0
    else
      if f true false = true then bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n + 1
      else bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n) =
    if f true false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

case true.true
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if f true true = true then
      bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + 1
    else bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2)) =
    if f true true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ (replicate n none).reduceOption = []

Tactic:
dsimp [reduceOption]
  rw [filterMap_replicate_of_none (id_def _)]

Goal state after: