mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ (↑{ index := index, groupElts := groupElts }).Finite ↔
    (↑(↑ps { index := index, groupElts := groupElts }.index)).Finite

Tactic:
simp only [coeSet]

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ (Quotient.liftOn' groupElts (fun g ↦ g • ↑(↑ps index)) ⋯).Finite ↔ (↑(↑ps index)).Finite
Module: Mathlib.Combinatorics.Young.SemistandardTableau

Goal state before:
pp: μ : YoungDiagram
T T' : SemistandardYoungTableau μ
h : T.entry = T'.entry
⊢ T = T'

Tactic:
by
    cases T
    cases T'
    congr

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec 0
      (fun n_1 n_ih ↦
        Nat.rec (encode (Option.map f (decode n_1)))
          (fun y IH ↦
            encode
              (Option.map (fun p ↦ g p.1 p.2)
                ((decode n_1).bind fun a ↦ Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode (some a)) =
    encode ((some a).bind fun a ↦ some (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) (Nat.unpair n).2))

Tactic:
simp only [Nat.pred_eq_sub_one, encode_some, Nat.succ_eq_add_one, encodek, Option.map_some,
        Option.bind_some, Option.map_map]

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec (encode (f a) + 1)
      (fun y IH ↦ encode (Option.map ((fun p ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1))))
      (Nat.unpair n).2 =
    encode (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) (Nat.unpair n).2) + 1
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α := ⋯
hF : Primrec₂ F
this : Primrec fun p ↦ Sum.casesOn (F p.1 p.2) (fun x ↦ none) some
l : List α
n : ℕ
⊢ l[n]? = Sum.rec (fun val ↦ none) (fun val ↦ some val) (F l n)

Tactic:
induction l generalizing n with
    | nil => rfl
    | cons a l IH =>
      rcases n with - | n
      · dsimp [F]
        clear IH
        induction l <;> simp_all
      · simpa using! IH ..

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : DecidableEq α
a : α
p : α × β
ps : List (α × β)
ih :
  (List.recOn (a, ps).2 none fun b l IH ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps
⊢ (bif a == p.1 then some p.2 else List.lookup a ps) =
    match a == p.1 with
    | true => some p.2
    | false => List.lookup a ps

Tactic:
cases ha : a == p.1

Goal state after:
case cons.false
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : DecidableEq α
a : α
p : α × β
ps : List (α × β)
ih :
  (List.recOn (a, ps).2 none fun b l IH ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps
ha : (a == p.1) = false
⊢ (bif false then some p.2 else List.lookup a ps) =
    match false with
    | true => some p.2
    | false => List.lookup a ps

case cons.true
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : DecidableEq α
a : α
p : α × β
ps : List (α × β)
ih :
  (List.recOn (a, ps).2 none fun b l IH ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps
ha : (a == p.1) = true
⊢ (bif true then some p.2 else List.lookup a ps) =
    match true with
    | true => some p.2
    | false => List.lookup a ps
Module: Mathlib.Computability.Partrec

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

Tactic:
injection mem_unique h₁ (rfind_min hm h)

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
⊢ Computable₂ fun a n ↦ (decode n).bind (f a)

Tactic:
have :
      Partrec fun a : α × ℕ =>
        (encode (decode (α := β) a.2)).casesOn (some Option.none)
          fun n => Part.map (f a.1) (decode (α := β) n) :=
      Partrec.nat_casesOn_right
        (h := fun (a : α × ℕ) (n : ℕ) ↦ map (fun b ↦ f a.1 b) (Part.ofOption (decode n)))
        (Primrec.encdec.to_comp.comp snd) (const Option.none)
        ((ofOption (Computable.decode.comp snd)).map (hf.comp (fst.comp <| fst.comp fst) snd).to₂)
    refine this.of_eq fun a => ?_
    simp; cases decode (α := β) a.2 <;> simp [encodek]

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

Goal state before:
pp: H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n
⊢ Primrec' fun v ↦ v.head.sqrt

Tactic:
simp only [H, succ_eq_add_one]
    have :=
      @prec' 1 _ _
        (fun v => by
          have x := v.head; have y := v.tail.head
          exact if x.succ < y.succ * y.succ then y else y.succ)
        head (const 0) ?_
    · exact this
    have x1 : @Primrec' 3 fun v => v.head.succ := succ.comp₁ _ head
    have y1 : @Primrec' 3 fun v => v.tail.head.succ := succ.comp₁ _ (tail head)
    exact if_lt x1 (mul.comp₂ _ y1 y1) (tail head) y1

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: c : Code
⊢ ofNatCode c.encodeCode = c

Tactic:
induction c

Goal state after:
case zero
⊢ ofNatCode zero.encodeCode = zero

case succ
⊢ ofNatCode succ.encodeCode = succ

case left
⊢ ofNatCode left.encodeCode = left

case right
⊢ ofNatCode right.encodeCode = right

case pair
a✝¹ a✝ : Code
a_ih✝¹ : ofNatCode a✝¹.encodeCode = a✝¹
a_ih✝ : ofNatCode a✝.encodeCode = a✝
⊢ ofNatCode (a✝¹.pair a✝).encodeCode = a✝¹.pair a✝

case comp
a✝¹ a✝ : Code
a_ih✝¹ : ofNatCode a✝¹.encodeCode = a✝¹
a_ih✝ : ofNatCode a✝.encodeCode = a✝
⊢ ofNatCode (a✝¹.comp a✝).encodeCode = a✝¹.comp a✝

case prec
a✝¹ a✝ : Code
a_ih✝¹ : ofNatCode a✝¹.encodeCode = a✝¹
a_ih✝ : ofNatCode a✝.encodeCode = a✝
⊢ ofNatCode (a✝¹.prec a✝).encodeCode = a✝¹.prec a✝

case rfind'
a✝ : Code
a_ih✝ : ofNatCode a✝.encodeCode = a✝
⊢ ofNatCode a✝.rfind'.encodeCode = a✝.rfind'
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_2.inr
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂ : b ∈ f.fix a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ f.fix a₃
n : ℕ
hn₁ : Sum.inl b ∈ F a n
hn₂ : ∀ m < n, k.succ ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer),
      the `clear_value F` was not required here. -/

Goal state after:
case refine_2.inr
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂ : b ∈ f.fix a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ f.fix a₃
n : ℕ
hn₁ : Sum.inl b ∈ F a n
hn₂ : ∀ m < n, k.succ ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
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
n : ℕ
hn : ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2
i : α
h₁ : 0 ≤ b i
⊢ b i * ↑n ≤ ↑n / log ↑n ^ 2 + ↑(r i n)

Tactic:
← sub_le_iff_le_add

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2
i : α
h₁ : 0 ≤ b i
⊢ b i * ↑n - ↑(r i n) ≤ ↑n / log ↑n ^ 2
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
gt_zero : 0 < b (min_bi b)
⊢ b (min_bi b) / 2 < b (min_bi b)

Tactic:
by aesop (add safe apply div_two_lt_of_pos)

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

Goal state before:
pp: x : ℝ
hx : x * 1 = 0
⊢ -x * log x ^ 2 = 0

Tactic:
rw [mul_one] at hx

Goal state after:
x : ℝ
hx : x = 0
⊢ -x * log x ^ 2 = 0
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 : α
x✝ : ℕ
⊢ -log (b i) / (log ↑x✝ * log ↑x✝) = -log (b i) / log ↑x✝ ^ 2

Tactic:
congr 1

Goal state after:
case e_a
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x✝ : ℕ
⊢ log ↑x✝ * log ↑x✝ = log ↑x✝ ^ 2
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 : α
x✝ : i ∈ univ
⊢ Continuous fun p ↦ a i

Tactic:
by fun_prop

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
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)‖
h_main : (fun n ↦ q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
h₁ : q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)
⊢ q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) + q ↑(r i n)

Tactic:
← sub_le_iff_le_add

Goal state after:
α : 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)‖
h_main : (fun n ↦ q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
h₁ : q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)
⊢ q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
Module: Mathlib.Computability.DFA

Goal state before:
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
⊢ M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
    M.evalFrom s (List.take (↑n) (List.take (↑m) x))

Tactic:
List.take_take,

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
⊢ M.evalFrom (M.evalFrom s (List.take (min ↑n ↑m) x)) (List.drop (↑n) (List.take (↑m) x)) =
    M.evalFrom s (List.take (min ↑n ↑m) x)
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
⊢ (M1.union M2).accepts = M1.accepts + M2.accepts

Tactic:
by
  simp [accepts]

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
⊢ (M1.inter M2).accepts = M1.accepts ⊓ M2.accepts

Tactic:
by
  simp [accepts]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
k₁ : ℕ
⊢ ∀ {c' : Code} {n : ℕ},
    Nat.pair k₁ (encode c') < Nat.pair k (encode c) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode c))))
          (k₁, c') n =
        evaln k₁ c' n

Tactic:
c₁

Goal state after:
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
k₁ : ℕ
c₁ : Code
⊢ ∀ {n : ℕ},
    Nat.pair k₁ (encode c₁) < Nat.pair k (encode c) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode c))))
          (k₁, c₁) n =
        evaln k₁ c₁ n
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
k₁ : ℕ
c₁ : Code
⊢ ∀ {n : ℕ},
    Nat.pair k₁ (encode c₁) < Nat.pair k (encode c) →
      lup
          (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode c))))
          (k₁, c₁) n =
        evaln k₁ c₁ n

Tactic:
n₁

Goal state after:
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
k₁ : ℕ
c₁ : Code
n₁ : ℕ
⊢ Nat.pair k₁ (encode c₁) < Nat.pair k (encode c) →
    lup
        (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair k (encode c))))
        (k₁, c₁) n₁ =
      evaln k₁ c₁ n₁
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ b = true

Tactic:
revert h
        cases b <;> simp

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

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hpos : ∀ᶠ (x : ℝ) in atTop, 0 < f x
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_pos : 0 < f x
hf_pos₂ : ∀ (y : ℝ), b * id x ≤ y → 0 < f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ (c₁ * f x) ^ p = c₁ ^ p * f x ^ p

Tactic:
← mul_rpow (le_of_lt hc₁_mem) (le_of_lt hf_pos)

Goal state after:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hpos : ∀ᶠ (x : ℝ) in atTop, 0 < f x
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_pos : 0 < f x
hf_pos₂ : ∀ (y : ℝ), b * id x ≤ y → 0 < f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ (c₁ * f x) ^ p = (c₁ * f x) ^ p
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case one
⊢ (if [] = [] then PosNum.one else (decodePosNum []).bit1) = PosNum.one

Tactic:
| one =>

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

Goal state before:
pp: case one
⊢ ∀ (n : PosNum), (one.cmp n).swap = n.cmp one

Tactic:
| one =>

Goal state after:
case one
⊢ ∀ (n : PosNum), (one.cmp n).swap = n.cmp one
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mpr
α : Type u_1
l : List (Option α)
a : α
⊢ (∃ m n, l = replicate m none ++ some a :: replicate n none) → filterMap id l = [a]

Tactic:
intro ⟨_, _, h⟩
    simp only [h, filterMap_append, filterMap_cons_some, filterMap_replicate_of_none, id_eq,
      nil_append, Option.some.injEq]

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

Goal state before:
pp: α : Type u_1
l : List (Option α)
l'₁ l'₂ : List α
⊢ l.reduceOption = l'₁ ++ l'₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.reduceOption = l'₁ ∧ l₂.reduceOption = l'₂

Tactic:
by
  dsimp [reduceOption]
  exact filterMap_eq_append_iff

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

Goal state before:
pp: case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a < ↑b + ↑b

pp: case eq
a b : PosNum
this : a = b
⊢ a.bit0 = b.bit0

pp: case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a

Tactic:
· exact Nat.add_lt_add this this

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ a.bit0 = b.bit0

case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a

Tactic:
· exact Nat.add_lt_add this this

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

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

Tactic:
by
    dsimp [cmp]
    have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
    · exact Nat.add_lt_add this this
    · rw [this]
    · exact Nat.add_lt_add this this

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

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ ↑a + ↑a < ↑b + ↑b + 1

Tactic:
rw [this]
      apply Nat.lt_succ_self

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

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑a + ↑a + 1

Tactic:
rw [this]
      apply Nat.lt_succ_self

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case cons
α : Type u
σ : Type v
M : NFA α σ
x : α
xs : List α
ih :
  ∀ {S S' : Set σ},
    Disjoint S (List.foldl M.reverse.stepSet S' xs) → Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S xs)
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet S' (x :: xs))
⊢ Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S (x :: xs))

Tactic:
List.foldl_cons

Goal state after:
case cons
α : Type u
σ : Type v
M : NFA α σ
x : α
xs : List α
ih :
  ∀ {S S' : Set σ},
    Disjoint S (List.foldl M.reverse.stepSet S' xs) → Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S xs)
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet (M.reverse.stepSet S' x) xs)
⊢ Disjoint S' (List.foldr (fun x y ↦ M.stepSet y x) S (x :: xs))
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: 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‖)
⊢ c₁ * ‖g u‖ ≤ f u

Tactic:
← Real.norm_of_nonneg (hf_pos u hu.1)

Goal state after:
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‖)
⊢ c₁ * ‖g u‖ ≤ ‖f u‖
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
n : PosNum
⊢ 1 ≤ ↑n

Tactic:
by
  rw [← cast_to_nat, ← Nat.cast_one, Nat.cast_le (α := α)]; apply to_nat_pos

Goal state after: