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

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

Tactic:
exact fun K ↦ hcomplMatch_compl K ▸ Set.disjoint_sdiff_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH ↦ List.casesOn IH.2 IH fun b l ↦ (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n ↦ (G a)^[n] (g a, f a)
hF : Primrec fun a ↦ (F a (encode (f a))).1
this : ∀ (a : α) (n : ℕ), F a n = (List.foldl (fun s b ↦ h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
a : α
⊢ (F a (encode (f a))).1 = List.foldl (fun s b ↦ h a (s, b)) (g a) (f a)

Tactic:
this,

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH ↦ List.casesOn IH.2 IH fun b l ↦ (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n ↦ (G a)^[n] (g a, f a)
hF : Primrec fun a ↦ (F a (encode (f a))).1
this : ∀ (a : α) (n : ℕ), F a n = (List.foldl (fun s b ↦ h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
a : α
⊢ (List.foldl (fun s b ↦ h a (s, b)) (g a) (List.take (encode (f a)) (f a)), List.drop (encode (f a)) (f a)).1 =
    List.foldl (fun s b ↦ h a (s, b)) (g a) (f a)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
⊢ n ∈ rfind p

Tactic:
rcases lt_trichotomy m n with (h | h | h)

Goal state after:
case inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m < n
⊢ n ∈ rfind p

case inr.inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m = n
⊢ n ∈ rfind p

case inr.inr
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : n < m
⊢ n ∈ rfind p
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case hc
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun z ↦ z ^ p) x

Tactic:
exact differentiableAt_rpow_const_of_ne _ (by positivity)

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

Goal state before:
pp: p : ℝ
⊢ (fun x ↦ p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2)) =ᶠ[atTop] fun x ↦
    p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / log x ^ 2

Tactic:
by
    filter_upwards [eventually_gt_atTop 0] with x hx
    rw [mul_div, ← Real.rpow_neg_one, ← Real.rpow_add (by positivity), sub_eq_add_neg]

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

Goal state before:
pp: case hc
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ x ^ p) x

Tactic:
exact differentiableAt_rpow_const_of_ne _ (by positivity)

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

Goal state before:
pp: b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ x) u ∈ Set.Icc (b * (fun x ↦ x) x) (c₂ * (fun x ↦ x) x)

Tactic:
refine ⟨1, by norm_num, ?_⟩

Goal state after:
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ x) u ∈ Set.Icc (b * (fun x ↦ x) x) (1 * (fun x ↦ x) x)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
⊢ (fun b ↦ succ.comp b)^[0] zero = Code.const 0

Tactic:
simp [*, Code.const, Function.iterate_succ', -Function.iterate_succ]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ
n✝ : ℕ
a✝ : (fun b ↦ succ.comp b)^[n✝] zero = Code.const n✝
⊢ (fun b ↦ succ.comp b)^[n✝ + 1] zero = Code.const (n✝ + 1)

Tactic:
simp [*, Code.const, Function.iterate_succ', -Function.iterate_succ]

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
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound1 : ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
h_smoothing_pos : 0 < 1 - ε ↑n
h_sumTransform : ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁⁻¹
h_ind : ∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ ∑ i, C * a i * (b i ^ p a b * (1 - ε ↑n) * (asympBound g a b n - sumTransform (p a b) g (r i n) n)) + g ↑n ≤
    ∑ i, C * a i * (b i ^ p a b * (1 - ε ↑n) * (asympBound g a b n - c₁ * g ↑n)) + g ↑n

Tactic:
gcongr with i
      · positivity [R.a_pos i]
      · positivity [R.b_pos i]
      · exact h_sumTransform i

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case rfind'
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
⊢ 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + (unpair n).2)) →
    (∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) →
      ∃ k, y + (unpair n).2 ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 (unpair n).2)

Tactic:
generalize n.unpair.2 = m

Goal state after:
case rfind'
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y m : ℕ
⊢ 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)) →
    (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
      ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
Module: Mathlib.Computability.Language

Goal state before:
pp: case mp
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ → ∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []

Tactic:
rintro ⟨S, rfl, h⟩

Goal state after:
case mp
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
⊢ ∃ S_1, S.flatten = S_1.flatten ∧ ∀ y ∈ S_1, y ∈ l ∧ y ≠ []
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
n x : ℕ
h : x = 0
⊢ (∃ x, n ≤ x) ∧ 0 = x

Tactic:
exact ⟨⟨_, le_rfl⟩, h.symm⟩

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ
n x : ℕ
h : x = n + 1
⊢ (∃ x, n ≤ x) ∧ n + 1 = x

Tactic:
exact ⟨⟨_, le_rfl⟩, h.symm⟩

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case left
n x : ℕ
h : x = (unpair n).1
⊢ (∃ x, n ≤ x) ∧ (unpair n).1 = x

Tactic:
exact ⟨⟨_, le_rfl⟩, h.symm⟩

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case right
n x : ℕ
h : x = (unpair n).2
⊢ (∃ x, n ≤ x) ∧ (unpair n).2 = x

Tactic:
exact ⟨⟨_, le_rfl⟩, h.symm⟩

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ ⨆ i, l ^ i

Tactic:
simp only [mem_kstar, mem_iSup, mem_pow]

Goal state after:
α : Type u_1
l : Language α
x : List α
⊢ (∃ L, x = L.flatten ∧ ∀ y ∈ L, y ∈ l) ↔ ∃ i S, x = S.flatten ∧ S.length = i ∧ ∀ y ∈ S, y ∈ l
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
⊢ reverse 1 = 1

Tactic:
simp [reverse, ← one_def]

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
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
h_exp : ⌈rexp 1⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁
h_ind : ∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
⊢ ∑ i, a i * (b i ^ p a b * (1 + ε ↑n) * (asympBound g a b n - sumTransform (p a b) g (r i n) n)) + C * g ↑n ≥
    ∑ i, a i * (b i ^ p a b * (1 + ε ↑n) * (asympBound g a b n - c₁ * g ↑n)) + C * g ↑n

Tactic:
gcongr with i
      · positivity [R.a_pos i]
      · positivity [R.b_pos i]
      · exact h_sumTransform i

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

Goal state before:
pp: case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun x ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 < f x
⊢ GrowsPolynomially fun x ↦ (f x)⁻¹

Tactic:
have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => |(f x)⁻¹| := by
          filter_upwards [hf'] with x hx₁
          rw [abs_of_nonneg (inv_nonneg_of_nonneg (le_of_lt hx₁))]
        rwa [iff_eventuallyEq hmain]

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
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
h_exp : ⌈rexp 1⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁
h_ind : ∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
this : 1 + ε ↑n < 2
⊢ c₁ * (1 + ε ↑n) ≤ C

Tactic:
this,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
h_exp : ⌈rexp 1⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁
h_ind : ∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
this : 1 + ε ↑n < 2
⊢ c₁ * 2 ≤ C
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: case pos.true
n : ℕ
h : ¬bit true 0 = 0
IH : shiftLeft' true 0 n ≠ 0 → (shiftLeft' true 0 n).size = size 0 + n
s0 : shiftLeft' true 0 n = 0
this : n = 0
⊢ (size 0).succ = (size 0 + n).succ

Tactic:
this,

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

Goal state before:
pp: case bit
b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
this : b = false
⊢ bit b n = 0

Tactic:
this,

Goal state after:
case bit
b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
this : b = false
⊢ bit false n = 0
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case pos
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn : b = false
hm : b' = true
this : n = m
⊢ bit false n < bit true m

Tactic:
this,

Goal state after:
case pos
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn : b = false
hm : b' = true
this : n = m
⊢ bit false m < bit true m
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
⊢ ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (1 / 2 * log x) (c₂ * log x)

Tactic:
refine ⟨1, by norm_num, ?_⟩

Goal state after:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (1 / 2 * log x) (1 * log x)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ log (b * x) ≤ log u

Tactic:
by gcongr; exact hu.1

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ (map (Option.map f) []).reduceOption = map f [].reduceOption

Tactic:
simp only [reduceOption_nil, map_nil]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
x : List α
⊢ x ∈ M.acceptsFrom (⋃ i, s i) ↔ x ∈ ⋃ i, M.acceptsFrom (s i)

Tactic:
simp only [acceptsFrom, evalFrom_iUnion, mem_iUnion]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
x : List α
⊢ x ∈ {x | ∃ s_1 ∈ M.accept, ∃ i, s_1 ∈ M.evalFrom (s i) x} ↔ x ∈ ⋃ i, {x | ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x}
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case hbc
f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound✝ : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
hg_bound : ∀ u ∈ Set.Icc (b * x) x, ‖g u‖ ∈ Set.Icc (c₃ * ‖g x‖) (c₄ * ‖g x‖)
⊢ ‖f x‖ ≤ c₂ * ‖g x‖

Tactic:
exact h_ub x hbx

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ b ∈ eval f a

Tactic:
· refine ReflTransGen.head_induction_on h₁ ?_ fun h _ IH ↦ ?_
    · refine PFun.mem_fix_iff.2 (Or.inl ?_)
      rw [h₂]
      apply Part.mem_some
    · refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH⟩)
      rw [h]
      apply Part.mem_some

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]

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
⊢ (P * Q).matchEpsilon = true ↔ ∃ t u, [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
⊢ (P * Q).rmatch (a :: x) = true ↔ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
rw [rmatch]

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
⊢ ((P * Q).deriv a).rmatch x = true ↔ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.one.bit1
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
n : PosNum
⊢ ↑(p 1 (PosNum.bit true n)) = Nat.bit (g true true) (bif g false true then ↑n else 0)

Tactic:
this,

Goal state after:
case pos.pos.one.bit1
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
n : PosNum
⊢ ↑(p 1 (PosNum.bit true n)) = Nat.bit (g true true) ↑(bif g false true then pos n else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.one.bit0
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
n : PosNum
⊢ ↑(p 1 (PosNum.bit false n)) = Nat.bit (g true false) (bif g false true then ↑n else 0)

Tactic:
this,

Goal state after:
case pos.pos.one.bit0
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
n : PosNum
⊢ ↑(p 1 (PosNum.bit false n)) = Nat.bit (g true false) ↑(bif g false true then pos n else 0)