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

Goal state before:
pp: case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : ¬G.Adj v w ∧ w ≠ v
⊢ #({a ∈ G.neighborFinset v | G.Adj a w}) = μ

Tactic:
adj_comm,

Goal state after:
case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : ¬G.Adj v w ∧ w ≠ v
⊢ #({x ∈ G.neighborFinset v | G.Adj w x}) = μ
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
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
⊢ ↑(Fintype.card ↑{p | p.length = 2}) =
    (k • 1 v w + ℓ • if G.Adj v w then 1 else 0) + μ • if v ≠ w ∧ ¬G.Adj v w then 1 else 0

Tactic:
@Fintype.card_congr _ _ (G.fintypeSetWalkLength v w 2) _
    (G.walkLengthTwoEquivCommonNeighbors v w)

Goal state after:
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
⊢ ↑(Fintype.card ↑(G.commonNeighbors v w)) =
    (k • 1 v w + ℓ • if G.Adj v w then 1 else 0) + μ • if v ≠ w ∧ ¬G.Adj v w then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r✝ : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
⊢ G.Colorable (r + 2)

Tactic:
classical
    -- There is an edge maximal `Kᵣ₊₃`-free supergraph `H` of `G`
    obtain ⟨H, hle, hmcf⟩ := @Finite.exists_le_maximal _ _ _ (fun H ↦ H.CliqueFree (r + 3)) G hf
    -- If `H` is `r + 2`-colorable then so is `G`
    apply Colorable.mono_left hle
    -- Suppose, for a contradiction, that `H` is not `r + 2`-colorable
    by_contra! hnotcol
    -- so `H` is not complete-multipartite
    have hn : ¬ H.IsCompleteMultipartite := fun hc ↦ hnotcol <| hc.colorable_of_cliqueFree hmcf.1
    -- Hence `H` contains `Wᵣ₊₁,ₖ` but not `Wᵣ₊₁,ₖ₊₁`, for some `k < r + 1`
    obtain ⟨k, _, _, _, _, _, hw, hlt, hm⟩ :=
      exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite hmcf hn
    -- But the minimum degree of `G`, and hence of `H`, is too large for it to be `Wᵣ₊₁,ₖ₊₁`-free,
    -- a contradiction.
    have hD := hw.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ hmcf.1 <| hm _ <| lt_add_one _
    have : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5) := by
      apply (Nat.le_div_iff_mul_le <| Nat.succ_pos _).2
              <| (mul_le_mul_iff_right₀ (_ + 2).succ_pos).1 _
      rw [← mul_assoc, mul_comm (2 * r + 2 + k + 3), mul_comm _ (_ * ‖α‖)]
      apply (Nat.mul_le_mul_right _ (Nat.div_mul_le_self ..)).trans
      nlinarith
    exact (hd.trans_le <| minDegree_le_minDegree hle).not_ge <| hD.trans <| this

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

Goal state before:
pp: μ : YoungDiagram
i✝ j1✝ j2✝ : ℕ
hj : j1✝ < j2✝
hcell : (i✝, j2✝) ∈ μ
⊢ (if (i✝, j1✝) ∈ μ then i✝ else 0) ≤ if (i✝, j2✝) ∈ μ then i✝ else 0

Tactic:
rw [if_pos hcell, if_pos (μ.up_left_mem (by rfl) (le_of_lt hj) hcell)]

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

Goal state before:
pp: p : ℕ × ℕ
⊢ (Nat.casesOn ((fun x1 x2 ↦ x1 - x2) p.1 p.2) true fun b ↦ false) = (fun a b ↦ decide (a ≤ b)) p.1 p.2

Tactic:
dsimp [swap]
    rcases e : p.1 - p.2 with - | n
    · simp [Nat.sub_eq_zero_iff_le.1 e]
    · simp [not_le.2 (Nat.lt_of_sub_eq_succ e)]

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ Primrec fun a ↦ (a.1 ::ᵥ a.2).toList

Tactic:
simpa using list_cons.comp fst (vector_toList_iff.2 snd)

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc✝ : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x✝ y : ↑K.supp
hxy : x✝ ≠ y ∧ ¬Gmax.deleteUniversalVerts.coe.Adj ↑x✝ ↑y
p : K.toSimpleGraph.Walk x✝ y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x✝ y
x a b : ↥K
hnxb : x ≠ b
hxa : Gmax.Adj ↑↑x ↑↑a
hxb : Gmax.Adj ↑↑a ↑↑b
hnadjxb : ¬Gmax.Adj ↑↑x ↑↑b
c : V
hc : ↑↑a ≠ c ∧ ¬Gmax.Adj (↑↑a) c
hbnec : ↑↑b ≠ c
w✝ : (Gmax ⊔ edge ↑↑x ↑↑b).Subgraph
hG1 : w✝.IsPerfectMatching
⊢ False

Tactic:
obtain ⟨_, hG2⟩ := hMaximal _ <| left_lt_sup.mpr (by
      rwa [edge_le_iff (v := a.1.1) (w := c), not_or])

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc✝ : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x✝ y : ↑K.supp
hxy : x✝ ≠ y ∧ ¬Gmax.deleteUniversalVerts.coe.Adj ↑x✝ ↑y
p : K.toSimpleGraph.Walk x✝ y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x✝ y
x a b : ↥K
hnxb : x ≠ b
hxa : Gmax.Adj ↑↑x ↑↑a
hxb : Gmax.Adj ↑↑a ↑↑b
hnadjxb : ¬Gmax.Adj ↑↑x ↑↑b
c : V
hc : ↑↑a ≠ c ∧ ¬Gmax.Adj (↑↑a) c
hbnec : ↑↑b ≠ c
w✝¹ : (Gmax ⊔ edge ↑↑x ↑↑b).Subgraph
hG1 : w✝¹.IsPerfectMatching
w✝ : (Gmax ⊔ edge (↑↑a) c).Subgraph
hG2 : w✝.IsPerfectMatching
⊢ False
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

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

pp: case hd
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun z ↦ 1 - ε z) x

Tactic:
· exact differentiableAt_rpow_const_of_ne _ (by positivity)

Goal state after:
case hd
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun z ↦ 1 - ε z) x
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

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

pp: case hd
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1 + ε x) x

Tactic:
· exact differentiableAt_rpow_const_of_ne _ (by positivity)

Goal state after:
case hd
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1 + ε x) x
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 - ε ↑n

Tactic:
by
  filter_upwards [eventually_one_sub_smoothingFn_pos] with n hn; exact le_of_lt hn

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

Goal state before:
pp: ⊢ (fun x ↦ x) =O[atTop] fun x ↦ x

Tactic:
aesop (add safe isBigO_refl)

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

Goal state before:
pp: ⊢ StrictMonoOn (fun x ↦ 1 - ε x) (Set.Ioi 1)

Tactic:
simp_rw [sub_eq_add_neg]
  exact StrictMonoOn.const_add (StrictAntiOn.neg <| strictAntiOn_smoothingFn) 1

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ (fun n ↦ 1 / log (b i * ↑n) - 1 / log ↑n) =ᶠ[atTop] fun n ↦ (log ↑n - log (b i * ↑n)) / (log (b i * ↑n) * log ↑n)

Tactic:
by
      filter_upwards [eventually_gt_atTop 1, R.eventually_log_b_mul_pos] with n hn hn'
      have h_log_pos : 0 < log n := Real.log_pos <| by simp_all
      simp only [one_div]
      rw [inv_sub_inv (by have := hn' i; positivity) (by aesop)]

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)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ b i * ↑n ≤ 1 * ↑n

Tactic:
have := R.b_lt_one i

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)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
this : b i < 1
⊢ b i * ↑n ≤ 1 * ↑n
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ GrowsPolynomially fun x ↦ |f x|

Tactic:
have hmain : -f =ᶠ[atTop] fun x => |f x| := by
      filter_upwards [hf'] with x hx
      simp only [Pi.neg_apply, abs_of_nonpos hx]
    rw [← iff_eventuallyEq hmain]
    exact hf.neg

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)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ b i * ↑n ≤ 1 * ↑n

Tactic:
have := R.b_lt_one i

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)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
this : b i < 1
⊢ b i * ↑n ≤ 1 * ↑n
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
a : ℕ
⊢ (cf.prec cg).eval (Nat.pair a 0) = cf.eval a

Tactic:
rw [eval, Nat.unpaired, Nat.unpair_pair]

Goal state after:
cf cg : Code
a : ℕ
⊢ Nat.rec (cf.eval (a, 0).1)
      (fun y IH ↦ do
        let i ← IH
        cg.eval (Nat.pair (a, 0).1 (Nat.pair y i)))
      (a, 0).2 =
    cf.eval a
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
hf' : 0 ≤ᶠ[atTop] f
hg' : 0 ≤ᶠ[atTop] g
⊢ GrowsPolynomially fun x ↦ f x + g x

Tactic:
by
  intro b hb
  have hf := hf b hb
  have hg := hg b hb
  obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf
  obtain ⟨c₃, hc₃_mem, c₄, _, hg⟩ := hg
  refine ⟨min c₁ c₃, by change 0 < min c₁ c₃; positivity, ?_⟩
  refine ⟨max c₂ c₄, by change 0 < max c₂ c₄; positivity, ?_⟩
  filter_upwards [hf, hg,
                  (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hf',
                  (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hg',
                  eventually_ge_atTop 0] with x hf hg hf' hg' hx_pos
  intro u hu
  have hbx : b * x ≤ x := calc
    b * x ≤ 1 * x := by gcongr; exact le_of_lt hb.2
        _ = x := by ring
  have fx_nonneg : 0 ≤ f x := hf' x hbx
  have gx_nonneg : 0 ≤ g x := hg' x hbx
  refine ⟨?lb, ?ub⟩
  case lb => calc
    min c₁ c₃ * (f x + g x) = min c₁ c₃ * f x + min c₁ c₃ * g x := by simp only [mul_add]
      _ ≤ c₁ * f x + c₃ * g x := by
              gcongr
              · exact min_le_left _ _
              · exact min_le_right _ _
      _ ≤ f u + g u := by
              gcongr
              · exact (hf u hu).1
              · exact (hg u hu).1
  case ub => calc
    max c₂ c₄ * (f x + g x) = max c₂ c₄ * f x + max c₂ c₄ * g x := by simp only [mul_add]
      _ ≥ c₂ * f x + c₄ * g x := by gcongr
                                    · exact le_max_left _ _
                                    · exact le_max_right _ _
      _ ≥ f u + g u := by gcongr
                          · exact (hf u hu).2
                          · exact (hg u hu).2

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

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

Tactic:
by
      cases hf_pos_or_neg with
      | inl hf' =>
        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]
      | inr hf' =>
        have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => -|(f x)⁻¹| := by
          filter_upwards [hf'] with x hx₁
          simp [abs_of_nonpos (inv_nonpos.mpr (le_of_lt hx₁))]
        rw [iff_eventuallyEq hmain]
        exact this.neg

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

Goal state before:
pp: f : Bool → Bool → Bool
⊢ bitwise f = fun n ↦
    binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
      (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) n

Tactic:
by
  funext x y
  induction x using binaryRec' generalizing y with
  | zero => simp only [bitwise_zero_left, binaryRec_zero, Bool.cond_eq_ite]
  | bit xb x hxb ih =>
    rw [← bit_ne_zero_iff] at hxb
    simp_rw [binaryRec_of_ne_zero _ _ hxb, bodd_bit, div2_bit, eq_rec_constant]
    induction y using binaryRec' with
    | zero => simp only [bitwise_zero_right, binaryRec_zero, Bool.cond_eq_ite]
    | bit yb y hyb =>
      rw [← bit_ne_zero_iff] at hyb
      simp_rw [binaryRec_of_ne_zero _ _ hyb, bitwise_of_ne_zero hxb hyb, bodd_bit, div2_bit,
        bit_div_two, eq_rec_constant, ih]

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 ∈ {x | ∃ s_1 ∈ M.accept, ∃ i, s_1 ∈ M.evalFrom (s i) x} ↔ ∃ i, x ∈ {x | ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x}

Tactic:
↑mem_ofPred_eq

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
x : List α
⊢ (∃ s_1 ∈ M.accept, ∃ i, s_1 ∈ M.evalFrom (s i) x) ↔ ∃ i, ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
x : α
⊢ x ∈ l.reduceOption ↔ some x ∈ l

Tactic:
by
  simp only [reduceOption, id, mem_filterMap, exists_eq_right]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
rw [← cast_to_nat, to_of_nat]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton.mp
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
⊢ (∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))) → ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

pp: case append_singleton.mpr
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
⊢ (∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x') → ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))

Tactic:
· intro ⟨t, ht, h⟩
      obtain ⟨x', _, _⟩ := ih.mp ht
      rw [mem_εClosure_iff_exists] at h
      simp_rw [mem_εClosure_iff_exists_path] at h
      obtain ⟨u, _, n, _⟩ := h
      use x' ++ some a :: List.replicate n none
      rw [List.reduceOption_append, List.reduceOption_cons_of_some,
        List.reduceOption_replicate_none, isPath_append]
      tauto

Goal state after:
case append_singleton.mpr
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
⊢ (∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x') → ∃ t ∈ M.evalFrom {s₁} x, s₂ ∈ M.εClosure (M.step t (some a))
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 :
  (n ∈ (↑(decode₂ α (encode a))).bind fun a ↦ Part.map encode (f a)) ∨
    n ∈ (↑(decode₂ α (encode a))).bind fun a ↦ Part.map encode (g a)
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
simp only [decode₂_encode, coe_some, bind_some, mem_map_iff] at this

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' : α → 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
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
P : α → ℕ → Prop
inst✝ : DecidableRel P
hP_comp : ComputablePred fun p ↦ P p.1 p.2
hP_ex : ∀ (x : α), ∃ n, P x n
h : Partrec fun x ↦ Nat.rfind fun n ↦ Part.some (decide (P x n))
x : α
⊢ Nat.find ⋯ ∈ Nat.rfind fun n ↦ Part.some (decide (P x n))

Tactic:
simp +contextual [Nat.find_spec]

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refl
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
⊢ f₁ c₁ = none

Tactic:
rcases hfc : f₁ c₁ with - | d₁

Goal state after:
case refl.none
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
hfc : f₁ c₁ = none
⊢ none = none

case refl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
d₁ : σ₁
hfc : f₁ c₁ = some d₁
⊢ some d₁ = none
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₁ : σ₁
⊢ (∀ ⦃a₂ : σ₂⦄,
      (fun a b ↦ tr a = b) a₁ a₂ →
        match f₁ a₁ with
        | some b₁ => ∃ b₂, (fun a b ↦ tr a = b) b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
        | none => f₂ a₂ = none) ↔
    FRespects f₂ tr (tr a₁) (f₁ a₁)

Tactic:
by
    cases f₁ a₁ <;> simp only [FRespects, exists_eq_left', forall_eq']

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (ListBlank.cons a R).tail.nth n = R.nth n

Tactic:
ListBlank.tail_cons

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ R.nth n = R.nth n
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ ((addBottom L).nth (n + 1)).1 = false

Tactic:
by
  rw [ListBlank.nth_succ, addBottom, ListBlank.tail_cons, ListBlank.nth_map]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case star
α : Type u_1
inst✝ : DecidableEq α
a✝ : RegularExpression α
ih : ∀ (x : List α), a✝.rmatch x = true ↔ x ∈ a✝.matches'
x : List α
⊢ a✝.star.rmatch x = true ↔ x ∈ a✝.star.matches'

Tactic:
| star _ ih =>

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

Goal state before:
pp: case gff
⊢ (false && false) = false

Tactic:
cases_type* Bool

Goal state after:
case gff
⊢ (false && false) = false
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f00
⊢ 0 &&& 0 = 0

Tactic:
cases_type* Bool

Goal state after:
case f00
⊢ 0 &&& 0 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n
n✝ : PosNum
⊢ 0 &&& pos n✝ = bif false && true then pos n✝ else 0

Tactic:
cases_type* Bool

Goal state after:
case f0n
n✝ : PosNum
⊢ 0 &&& pos n✝ = bif false && true then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0
n✝ : PosNum
⊢ pos n✝ &&& 0 = bif true && false then pos n✝ else 0

Tactic:
cases_type* Bool

Goal state after:
case fn0
n✝ : PosNum
⊢ pos n✝ &&& 0 = bif true && false then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn
m✝ n✝ : PosNum
⊢ pos m✝ &&& pos n✝ = m✝.land n✝

Tactic:
cases_type* Bool

Goal state after:
case fnn
m✝ n✝ : PosNum
⊢ pos m✝ &&& pos n✝ = m✝.land n✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0

Tactic:
cases_type* Bool

Goal state after:
case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit b✝ n✝) = bit (true && b✝) (bif false && true then pos n✝ else 0)

Tactic:
cases_type* Bool

Goal state after:
case p1b.false
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit false n✝) = bit (true && false) (bif false && true then pos n✝ else 0)

case p1b.true
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit true n✝) = bit (true && true) (bif false && true then pos n✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land 1 = bit (a✝ && true) (bif true && false then pos m✝ else 0)

Tactic:
cases_type* Bool

Goal state after:
case pb1.false
m✝ : PosNum
⊢ (PosNum.bit false m✝).land 1 = bit (false && true) (bif true && false then pos m✝ else 0)

case pb1.true
m✝ : PosNum
⊢ (PosNum.bit true m✝).land 1 = bit (true && true) (bif true && false then pos m✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land (PosNum.bit b✝ n✝) = bit (a✝ && b✝) (m✝.land n✝)

Tactic:
cases_type* Bool

Goal state after:
case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit false n✝) = bit (false && false) (m✝.land n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit true n✝) = bit (false && true) (m✝.land n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit false n✝) = bit (true && false) (m✝.land n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit true n✝) = bit (true && true) (m✝.land n✝)