mathlib-initiative/mathlib-tactics huggingface dataset:
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 : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * ↑n)
h_log_pos : 0 < log ↑n
⊢ log ↑n ≠ 0

Tactic:
aesop

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

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

Tactic:
aesop

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

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

Tactic:
aesop

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

Goal state before:
pp: case hab
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
hu' : u ∈ Set.Icc (r i n) n
⊢ ↑u ∈ Set.Icc (c₁ * ↑n) ↑n

Tactic:
rw [Set.mem_Icc]

Goal state after:
case hab
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
hu' : u ∈ Set.Icc (r i n) n
⊢ c₁ * ↑n ≤ ↑u ∧ ↑u ≤ ↑n
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case h₂
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
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, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
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)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ |g u| ≤ c₄ * |g x|

Tactic:
exact (hg u hu).2

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

Goal state before:
pp: case hab
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
u : ℕ
hu : r i n ≤ u ∧ u < n
hu' : u ∈ Set.Icc (r i n) n
⊢ ↑u ∈ Set.Icc (c₁ * ↑n) ↑n

Tactic:
rw [Set.mem_Icc]

Goal state after:
case hab
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
u : ℕ
hu : r i n ≤ u ∧ u < n
hu' : u ∈ Set.Icc (r i n) n
⊢ c₁ * ↑n ≤ ↑u ∧ ↑u ≤ ↑n
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case h₂
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
hf'✝ : 0 ≤ᶠ[atTop] f
hg'✝ : 0 ≤ᶠ[atTop] g
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₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y
hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
fx_nonneg : 0 ≤ f x
gx_nonneg : 0 ≤ g x
⊢ g u ≤ c₄ * g x

Tactic:
exact (hg u hu).2

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

Goal state before:
pp: case hab
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
hu' : u ∈ Set.Icc (r i n) n
⊢ ↑u ∈ Set.Icc (c₁ * ↑n) ↑n

Tactic:
rw [Set.mem_Icc]

Goal state after:
case hab
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
u : ℕ
hu : r i n ≤ u ∧ u < n
hu' : u ∈ Set.Icc (r i n) n
⊢ c₁ * ↑n ≤ ↑u ∧ ↑u ≤ ↑n
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a n ↦
              Nat.casesOn n (evaln (k + 1) cf a) fun y ↦ do
                let i ← evaln k (cf.prec cg) (Nat.pair a y)
                evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x
n✝ : ℕ
a✝ :
  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)))
        n✝ =
      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)))
        n✝ =
      some x
⊢ ∀ (x_1 : ℕ),
    evaln k (cf.prec cg) (Nat.pair (unpair n).1 n✝) = some x_1 →
      evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ x_1)) = some x →
        ∃ a,
          evaln k₂ (cf.prec cg) (Nat.pair (unpair n).1 n✝) = some a ∧
            evaln (k₂ + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ a)) = some x

Tactic:
exact fun y h₁ h₂ => ⟨y, evaln_mono hl' h₁, hg _ _ h₂⟩

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

Goal state before:
pp: case hab
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
u : ℕ
hu : r i n ≤ u ∧ u < n
hu' : u ∈ Set.Icc (r i n) n
⊢ ↑u ∈ Set.Icc (c₁ * ↑n) ↑n

Tactic:
rw [Set.mem_Icc]

Goal state after:
case hab
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
u : ℕ
hu : r i n ≤ u ∧ u < n
hu' : u ∈ Set.Icc (r i n) n
⊢ c₁ * ↑n ≤ ↑u ∧ ↑u ≤ ↑n
Module: Mathlib.Computability.Language

Goal state before:
pp: case a
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
x : List α
hx : x ∈ l
⊢ x ∈ m∗ * n

Tactic:
induction hlen : x.length using Nat.strong_induction_on generalizing x with | _ _ ih
       =>  _ 

Goal state after:
case a.h
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
n✝ : ℕ
ih : ∀ m_1 < n✝, ∀ ⦃x : List α⦄, x ∈ l → x.length = m_1 → x ∈ m∗ * n
x : List α
hx : x ∈ l
hlen : x.length = n✝
⊢ x ∈ m∗ * n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ ↑(a + b) + 1 + (↑(a + b) + 1) = ↑a + ↑a + 1 + (↑b + ↑b + 1)

Tactic:
add_to_nat a b

Goal state after:
a b : PosNum
⊢ ↑a + ↑b + 1 + (↑a + ↑b + 1) = ↑a + ↑a + 1 + (↑b + ↑b + 1)
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List (Option α)
f : α → β
⊢ (map (Option.map f) l).reduceOption = map f l.reduceOption

Tactic:
induction l with
  | nil => simp only [reduceOption_nil, map_nil]
  | cons hd tl hl =>
    cases hd <;> simpa [Option.map_some, map, eq_self_iff_true, reduceOption_cons_of_some] using hl

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) (a.cmp b)

Tactic:
cases cmp a b

Goal state after:
case lt
a b : PosNum
⊢ Ordering.casesOn Ordering.lt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) Ordering.lt

case eq
a b : PosNum
⊢ Ordering.casesOn Ordering.eq (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) Ordering.eq

case gt
a b : PosNum
⊢ Ordering.casesOn Ordering.gt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (a.cmp b))

Tactic:
cases cmp a b

Goal state after:
case lt
a b : PosNum
⊢ Ordering.casesOn Ordering.lt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt Ordering.lt)

case eq
a b : PosNum
⊢ Ordering.casesOn Ordering.eq (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt Ordering.eq)

case gt
a b : PosNum
⊢ Ordering.casesOn Ordering.gt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt Ordering.gt)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (a.cmp b))

Tactic:
cases cmp a b

Goal state after:
case lt
a b : PosNum
⊢ Ordering.casesOn Ordering.lt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt Ordering.lt)

case eq
a b : PosNum
⊢ Ordering.casesOn Ordering.eq (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt Ordering.eq)

case gt
a b : PosNum
⊢ Ordering.casesOn Ordering.gt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt Ordering.gt)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) (a.cmp b)

Tactic:
cases cmp a b

Goal state after:
case lt
a b : PosNum
⊢ Ordering.casesOn Ordering.lt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) Ordering.lt

case eq
a b : PosNum
⊢ Ordering.casesOn Ordering.eq (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) Ordering.eq

case gt
a b : PosNum
⊢ Ordering.casesOn Ordering.gt (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ ofNat' 0 = 0

Tactic:
simp [Num.ofNat']

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Tactic:
by
    have := PosNum.cmp_to_nat a b; revert this; dsimp [cmp]; cases PosNum.cmp a b
    exacts [id, congr_arg pos, id]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ n.natSize = (↑n).size

Tactic:
rw [← size_eq_natSize, size_to_nat]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : Num
⊢ n.natSize = (↑n).size

Tactic:
rw [← size_eq_natSize, size_to_nat]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero.pos
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)
n : PosNum
⊢ ↑(bif g false true then pos n else 0) = if g false true = true then ↑(pos n) else 0

Tactic:
cases g false true

Goal state after:
case zero.pos.false
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)
n : PosNum
⊢ ↑(bif false then pos n else 0) = if false = true then ↑(pos n) else 0

case zero.pos.true
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)
n : PosNum
⊢ ↑(bif true then pos n else 0) = if true = true then ↑(pos n) else 0
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 : ℕ →. ℕ
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' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this : (∃ a_1 ∈ f a, encode a_1 = n) ∨ ∃ a_1 ∈ g a, encode a_1 = n
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
obtain ⟨a', ha, rfl⟩ | ⟨a', ha, rfl⟩ := this <;> simp only [encodek, Option.some_inj] at hx <;>
      rw [hx] at ha

Goal state after:
case inl
α : 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' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x a' : σ
ha : x ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a

case inr
α : 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' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
x a' : σ
ha : x ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
pF : Nat.Partrec f
⊢ Nat.RecursiveIn O f

Tactic:
by
  induction pF with
  | zero | succ | left | right => constructor
  | pair _ _ ih₁ ih₂ => exact .pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact .comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact .prec ih₁ ih₂
  | rfind _ ih => exact .rfind ih

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : 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 α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ a = b

Tactic:
exact h.1

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : 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 α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ a = b

Tactic:
exact h.1

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case prim.get.refine_2
n✝² : ℕ
f : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i✝ : Fin n✝
n : ℕ
i : Fin n
IH : ∃ c, ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> (↑fun v ↦ v.get i) v
⊢ ∃ c, ∀ (v : List.Vector ℕ n.succ), c.eval ↑v = pure <$> (↑fun v ↦ v.get i.succ) v

Tactic:
obtain ⟨c, h⟩ := IH
        exact ⟨c.comp tail, fun v => by simpa [← Vector.get_tail, Bind.bind] using h v.tail⟩

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a : Z ⟶ X
b : Z ⟶ Y
z : ↑Z.toTop
w : (ConcreteCategory.hom (a ≫ f)) z = (ConcreteCategory.hom (b ≫ g)) z
⊢ ((ConcreteCategory.hom a) z, (ConcreteCategory.hom b) z) ∈
    {xy | (ConcreteCategory.hom f) xy.1 = (ConcreteCategory.hom g) xy.2}

Tactic:
exact w

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
this : ∀ C ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun x ↦ x ∈ S) E
E_closed : IsClosed E
E_surj : X '' E = univ
E₀ : Set ↑E
E₀_min : E₀ ≠ univ
E₀_closed : IsClosed E₀
⊢ E.domRestrict X '' E₀ ≠ univ

Tactic:
contrapose E₀_min

Goal state after:
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
this : ∀ C ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun x ↦ x ∈ S) E
E_closed : IsClosed E
E_surj : X '' E = univ
E₀ : Set ↑E
E₀_closed : IsClosed E₀
E₀_min : E.domRestrict X '' E₀ = univ
⊢ E₀ = univ