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

Goal state before:
pp: case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ x✝ : V
w✝¹ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ = x✝³
w✝ : Fin r
h₂ : map { toFun := fun j ↦ f (w✝, j), inj' := ⋯ } univ = x✝²
h₁' : x✝¹ ∈ (fun j ↦ f (w✝¹, j)) '' ↑univ
h₂' : x✝ ∈ (fun j ↦ f (w✝, j)) '' ↑univ
⊢ G.Adj x✝¹ x✝

Tactic:
coe_univ,

Goal state after:
case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ x✝ : V
w✝¹ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ = x✝³
w✝ : Fin r
h₂ : map { toFun := fun j ↦ f (w✝, j), inj' := ⋯ } univ = x✝²
h₁' : x✝¹ ∈ (fun j ↦ f (w✝¹, j)) '' Set.univ
h₂' : x✝ ∈ (fun j ↦ f (w✝, j)) '' Set.univ
⊢ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
G' : G.Finsubgraphᵒᵖ
this : Fintype ↑(↑(Opposite.unop G')).verts
⊢ Fintype ((G.finsubgraphHomFunctor F).obj G')

Tactic:
haveI : Fintype (↥G'.unop.val.verts → W) := by classical exact Pi.instFintype

Goal state after:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝¹ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
G' : G.Finsubgraphᵒᵖ
this✝ : Fintype ↑(↑(Opposite.unop G')).verts
this : Fintype (↑(↑(Opposite.unop G')).verts → W)
⊢ Fintype ((G.finsubgraphHomFunctor F).obj G')
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
⊢ BddBelow {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}

Tactic:
refine ⟨0, fun x ⟨_, _, hx⟩ ↦ ?_⟩

Goal state after:
W : Type u_1
H : SimpleGraph W
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
w✝ : ℕ
left✝ : w✝ ∈ Set.Ici 2
hx : ↑(extremalNumber w✝ H) / ↑(w✝.choose 2) = x
⊢ 0 ≤ x
Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
⊢ Nonempty (G →g F)

Tactic:
cases nonempty_fintype W
  -- Establish the required interface instances.
  have : ∀ G' : G.Finsubgraphᵒᵖ, Nonempty ((finsubgraphHomFunctor G F).obj G') := fun G' =>
    ⟨h G'.unop G'.unop.property⟩
  have : ∀ G' : G.Finsubgraphᵒᵖ, Fintype ((finsubgraphHomFunctor G F).obj G') := by
    intro G'
    haveI : Fintype (G'.unop.val.verts : Type u) := G'.unop.property.fintype
    haveI : Fintype (↥G'.unop.val.verts → W) := by classical exact Pi.instFintype
    exact Fintype.ofInjective (fun f => f.toFun) RelHom.coe_fn_injective
  -- Use compactness to obtain a section.
  obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (finsubgraphHomFunctor G F)
  refine ⟨⟨fun v => ?_, ?_⟩⟩
  · -- Map each vertex using the homomorphism provided for its singleton subgraph.
    exact
      (u (Opposite.op (singletonFinsubgraph v))).toFun
        ⟨v, by
          unfold singletonFinsubgraph
          simp⟩
  · -- Prove that the above mapping preserves adjacency.
    intro v v' e
    simp only
    /- The homomorphism for each edge's singleton subgraph agrees with those for its source and
        target vertices. -/
    have hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v) :=
      Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_left)
    have hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v') :=
      Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_right)
    rw [← hu hv, ← hu hv']
    -- Porting note: was `apply Hom.map_adj`
    apply Hom.map_adj (u _) ?_
    -- `v` and `v'` are definitionally adjacent in `finsubgraphOfAdj e`
    simp [finsubgraphOfAdj]

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
x : ℕ
⊢ zarankiewicz m n s t ≤ x ↔
    ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst : DecidableRel G.Adj],
      G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → #G.edgeFinset ≤ x

Tactic:
simp_rw [zarankiewicz_of_fintypeCard_eq hm hn hs ht,
    Finset.sup_le_iff, mem_filter, mem_univ, true_and]

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
x : ℕ
⊢ (∀ (b : SimpleGraph (V ⊕ W)),
      b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b → #b.edgeFinset ≤ x) ↔
    ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst : DecidableRel G.Adj],
      G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → #G.edgeFinset ≤ x
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
⊢ ∃ a w, w.IsCycle ∧ G.egirth = ↑w.length

Tactic:
← egirth_eq_top,

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
h : ¬G.egirth = ⊤
⊢ ∃ a w, w.IsCycle ∧ G.egirth = ↑w.length
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
⊢ Even s.ncard ↔ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
use exists_union_disjoint_cardinal_eq_of_even

Goal state after:
case mpr
α : Type u_1
s : Set α
⊢ (∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u) → Even s.ncard
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)
⊢ ∀ a ∈ K.parts, (powersetCard t a).Nonempty

Tactic:
powersetCard_nonempty

Goal state after:
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)
⊢ ∀ a ∈ K.parts, t ≤ #a
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
i j : ℕ
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
W X : Finset α
hx : ∀ x ∈ X, i ≤ #({z ∈ W | ¬G.Adj x z})
hxc : ∀ y ∈ Xᶜ, j ≤ #({z ∈ W | ¬G.Adj y z})
⊢ ∀ (x y : α), x ∈ W ∧ y ∈ G.neighborFinset x ↔ x ∈ G.neighborFinset y ∩ W ∧ y ∈ univ

Tactic:
simp [and_comm, adj_comm]

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

Goal state before:
pp: case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
a b : α
h : ¬a = b
h' : G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1

Tactic:
exact G.incMatrix_mul_transpose_apply_of_adj h'

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

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ {w} ∪ {v} ⊆ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

Tactic:
· intro u
    simp only [mem_union, mem_compl, mem_neighborFinset, mem_inter, mem_singleton]
    rintro (rfl | rfl) <;> simpa [adj_comm] using ha.2

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

Goal state before:
pp: μ : YoungDiagram
i : ℕ
⊢ ∃ j, (i, j) ∉ μ

Tactic:
by
  obtain ⟨j, hj⟩ :=
    Infinite.exists_notMem_finset
      (μ.cells.preimage (Prod.mk i) fun _ _ _ _ h => by
        cases h
        rfl)
  rw [Finset.mem_preimage] at hj
  exact ⟨j, hj⟩

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

Goal state before:
pp: case pos
m n : ℕ
h : n ≤ m
⊢ some (m - n) = m.psub n

Tactic:
exact (psub_eq_sub h).symm

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

Goal state before:
pp: ⊢ Primrec₂ fun x1 x2 ↦ x1 / x2

Tactic:
by
  refine of_graph ⟨_, fst, fun p => Nat.div_le_self _ _⟩ ?_
  have : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) => (a.2 = 0 ∧ b = 0) ∨
      (0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2) :=
    PrimrecPred.or
      (.and (const 0 |> Primrec.eq.comp (fst |> snd.comp)) (const 0 |> Primrec.eq.comp snd))
      (.and (nat_lt.comp (const 0) (fst |> snd.comp)) <|
          .and (nat_le.comp (nat_mul.comp snd (fst |> snd.comp)) (fst |> fst.comp))
          (nat_lt.comp (fst.comp fst) (nat_mul.comp (Primrec.succ.comp snd) (snd.comp fst))))
  refine this.of_eq ?_
  rintro ⟨a, k⟩ q
  if H : k = 0 then simp [H, eq_comm]
  else
    have : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k := by
      rw [le_antisymm_iff, ← (@Nat.lt_succ_iff _ q), Nat.le_div_iff_mul_le (Nat.pos_of_ne_zero H),
          Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero H)]
    simpa [H, zero_lt_iff, eq_comm (b := q)]

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

Goal state before:
pp: n : ℕ
⊢ Nat.rec [] (fun n_1 IH ↦ (n, n_1, IH).2.2 ++ [(n, n_1, IH).2.1]) (id n) = List.range n

Tactic:
by
    simp; induction n <;> simp [*, List.range_succ]

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

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x'✝ x' c' : V
hc : c' ≠ a
w : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
hx' : x'✝ ∈ {x, x'}
p : cycles.Walk a x'✝
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
hadj : p.toSubgraph.Adj c' x'
hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x'
hw : ∀ (y : V), (fun w ↦ M1.Adj x' w) y → y = w
⊢ p.toSubgraph.Adj x x'

Tactic:
rw [hw _ hM1xb.symm, ← hw _ hl.1.symm]

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x'✝ x' c' : V
hc : c' ≠ a
w : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
hx' : x'✝ ∈ {x, x'}
p : cycles.Walk a x'✝
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
hadj : p.toSubgraph.Adj c' x'
hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x'
hw : ∀ (y : V), (fun w ↦ M1.Adj x' w) y → y = w
⊢ p.toSubgraph.Adj c' x'
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)
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x

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

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)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c₂ * f x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

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

Tactic:
obtain ⟨n₀, hn₀⟩ := h

Goal state after:
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
⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, f x = c
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

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

Tactic:
case le => calc b i * n
            _ ≤ 1 * n := by have := R.b_lt_one i; gcongr
            _ = n := by rw [one_mul]

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)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)

Tactic:
exact hx u hu

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

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

Tactic:
case le => calc b i * n
            _ ≤ 1 * n := by have := R.b_lt_one i; gcongr
            _ = n := by rw [one_mul]

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
⊢ 1 / 2 * ‖f x‖ = 1 / 2 * f x

Tactic:
by congr; exact norm_of_nonneg (hf₂ _ hbx)

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.refine_1
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x →
      x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m
x y : ℕ
h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y
h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x
⊢ Nat.rec (evaln (k + 1) cf (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      m =
    some y

pp: case succ.refine_2
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x →
      x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m
x y : ℕ
h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y
h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x
⊢ x ∈ cg.eval (Nat.pair (unpair n).1 (Nat.pair m y))

Tactic:
· have := evaln_mono k.le_succ h₁
          simp [evaln, Option.bind_eq_some_iff] at this
          exact this.2

Goal state after:
case succ.refine_2
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x →
      x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m
x y : ℕ
h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y
h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x
⊢ x ∈ cg.eval (Nat.pair (unpair n).1 (Nat.pair m y))
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: case succ
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
⊢ (shiftLeft' b m n).size.succ = m.size + (n + 1)

Tactic:
Nat.add_succ

Goal state after:
case succ
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.inl
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
⊢ c ^^^ a < b

Tactic:
hca

Goal state after:
case inr.inl
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
⊢ b ^^^ v < b
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
a : α
h : ∃ l₁ a_1 l₂, l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : Option α), x ∈ l₁ → id x = none) ∧ id a_1 = some a ∧ filterMap id l₂ = []
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Tactic:
obtain ⟨l₁, _, l₂, h, hl₁, ⟨⟩, hl₂⟩ := h

Goal state after:
case mp
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none
hl₂ : filterMap id l₂ = []
h : l = l₁ ++ some a :: l₂
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s t : σ
x✝ : List α
a : α
x : List α
h : t ∈ M.evalFrom {s} (a :: x)
⊢ ∃ s' ∈ M.step s a, t ∈ M.evalFrom {s'} x

Tactic:
evalFrom_cons,

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
s t : σ
x✝ : List α
a : α
x : List α
h : t ∈ M.evalFrom (M.stepSet {s} a) x
⊢ ∃ s' ∈ M.step s a, t ∈ M.evalFrom {s'} x
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s✝ t✝ : σ
x✝ : List α
p : Nonempty (M.Path s✝ t✝ x✝)
t s s' : σ
a : α
x : List α
h₁ : s' ∈ M.step s a
h₂ : M.Path s' t x
⊢ t ∈ M.evalFrom {s} (a :: x)

Tactic:
evalFrom_cons,

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
s✝ t✝ : σ
x✝ : List α
p : Nonempty (M.Path s✝ t✝ x✝)
t s s' : σ
a : α
x : List α
h₁ : s' ∈ M.step s a
h₂ : M.Path s' t x
⊢ t ∈ M.evalFrom (M.stepSet {s} a) x
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : Num
h : m.toZNum = n.toZNum
⊢ m = n

Tactic:
by cases m <;> cases n <;> cases h <;> rfl

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
⊢ ∃ k, Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Tactic:
let ⟨k, hk, H⟩ := Nat.Partrec.merge' (bind_decode₂_iff.1 hf) (bind_decode₂_iff.1 hg)

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
⊢ ∃ k, Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
L R : ListBlank Γ
n : ℕ
⊢ (mk' L R).nth ↑n = R.nth n

Tactic:
by
  rw [← Tape.right₀_nth, Tape.mk'_right₀]

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : α → Prop
q : β → Prop
⊢ Quotient.mk'' (toNat p) = Quotient.mk'' (toNat q) ↔ ManyOneEquiv p q

Tactic:
Quotient.eq''

Goal state after:
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : α → Prop
q : β → Prop
⊢ { r := ManyOneEquiv, iseqv := _proof_1 } (toNat p) (toNat q) ↔ ManyOneEquiv p q
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : α → Prop
q : β → Prop
⊢ of p = of q ↔ ManyOneEquiv p q

Tactic:
rw [of, of, Quotient.eq'']
  simp

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
⊢ (P * Q).rmatch [] = true ↔ ∃ t u, [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
rw [rmatch]; simp only [matchEpsilon]
    constructor
    · intro h
      refine ⟨[], [], rfl, ?_⟩
      rw [rmatch, rmatch]
      rwa [Bool.and_eq_true_iff] at h
    · rintro ⟨t, u, h₁, h₂⟩
      obtain ⟨rfl, rfl⟩ := List.append_eq_nil_iff.1 h₁.symm
      repeat rw [rmatch] at h₂
      simp [h₂]

Goal state after: