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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
⊢ #K.parts + 1 = #K'.parts

Tactic:
K.card_parts.resolve_right ht,

Goal state after:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
⊢ r + 1 = #K'.parts
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
L : Set V
C : G.ComponentCompl L
⊢ ConnectedComponent.map Hom.id C = C

Tactic:
ConnectedComponent.map_id

Goal state after:
V : Type u
G : SimpleGraph V
L : Set V
C : G.ComponentCompl L
⊢ C = C
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
Ddis : Disjoint ↑(K ∪ Cfin.toFinset) ↑D := ComponentCompl.disjoint_right D
⊢ False

Tactic:
simp_rw [Finset.coe_union, Set.Finite.coe_toFinset, Set.disjoint_union_left,
        Set.disjoint_iff] at Ddis

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
Ddis : ↑K ∩ ↑D ⊆ ∅ ∧ C.supp ∩ ↑D ⊆ ∅
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ (↑n - 1) * (↑n / 2) * ↑(#G.edgeFinset) ≤ (↑n + 1) * ↑n / 2 * ↑(extremalNumber n H)

Tactic:
mul_comm _ (n / 2 : ℝ),

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑n / 2 * (↑n - 1) * ↑(#G.edgeFinset) ≤ (↑n + 1) * ↑n / 2 * ↑(extremalNumber n H)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑n / 2 * (↑(#G.edgeFinset) * (↑n - 1)) ≤ (↑n + 1) * (↑n / 2) * ↑(extremalNumber n H)

Tactic:
mul_comm _ (n / 2 : ℝ),

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑n / 2 * (↑(#G.edgeFinset) * (↑n - 1)) ≤ ↑n / 2 * (↑n + 1) * ↑(extremalNumber n H)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) - ↑(#(filter K t)) * (↑(#K.verts) - (↑t' - ↑t)) +
      ↑(#(filter K t)) * ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)

Tactic:
mul_sub (#(filter K t) : ℝ) _ _,

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) - (↑(#(filter K t)) * ↑(#K.verts) - ↑(#(filter K t)) * (↑t' - ↑t)) +
      ↑(#(filter K t)) * ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
s : Finset ↑p₁
this : (↑(Finset.image Subtype.val s)).ncard ≤ (⋃ x ∈ ↑(Finset.image Subtype.val s), G.neighborSet x).ncard
⊢ s.card ≤ (s.biUnion fun x ↦ G.neighborFinset ↑x).card

Tactic:
Set.ncard_coe_finset,

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
s : Finset ↑p₁
this : (Finset.image Subtype.val s).card ≤ (⋃ x ∈ ↑(Finset.image Subtype.val s), G.neighborSet x).ncard
⊢ s.card ≤ (s.biUnion fun x ↦ G.neighborFinset ↑x).card
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
⊢ p₁ ∪ p₂ = Set.univ

Tactic:
obtain ⟨f, _, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun x ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ s
    simpa [← Set.ncard_coe_finset, neighborFinset_def]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
left✝ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
⊢ p₁ ∪ p₂ = Set.univ
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
⊢ #s = r

Tactic:
by
  simp [← Nat.succ_inj, ← hw.isNClique_left.2, hw.notMem_left]

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

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun i j ↦ Disjoint (f i).support (f j).support
v : V
hv : v ∈ (⨆ i, f i).verts
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun w ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun w ↦ (f i).Adj v w) y → y = w
y : V
hy : (⨆ i, f i).Adj v y
⊢ y = w

Tactic:
obtain ⟨i', hi'⟩ := iSup_adj.mp hy

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun i j ↦ Disjoint (f i).support (f j).support
v : V
hv : v ∈ (⨆ i, f i).verts
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun w ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun w ↦ (f i).Adj v w) y → y = w
y : V
hy : (⨆ i, f i).Adj v y
i' : ι
hi' : (f i').Adj v y
⊢ y = w
Module: Mathlib.Combinatorics.SimpleGraph.Partition

Goal state before:
pp: V : Type u
G : SimpleGraph V
P : G.Partition
v : V
⊢ v ∈ P.partOfVertex v

Tactic:
obtain ⟨⟨_, h⟩, _⟩ := (P.isPartition.2 v).choose_spec

Goal state after:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
right✝ : ∀ (y : Set V), (fun b ↦ b ∈ P.parts ∧ v ∈ b) y → y = Exists.choose ⋯
left✝ : Exists.choose ⋯ ∈ P.parts
h : v ∈ Exists.choose ⋯
⊢ v ∈ P.partOfVertex v
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ ν : YoungDiagram
h : (fun y ↦ ↑y.cells) μ = (fun y ↦ ↑y.cells) ν
⊢ μ = ν

Tactic:
rwa [YoungDiagram.ext_iff, ← Finset.coe_inj]

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

Goal state before:
pp: μ ν : YoungDiagram
⊢ IsLowerSet (↑μ.cells ∪ ↑ν.cells)

Tactic:
exact μ.isLowerSet.union ν.isLowerSet

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

Goal state before:
pp: μ : YoungDiagram
i : ℕ
⊢ μ.row i = {i} ×ˢ Finset.range (μ.rowLen i)

Tactic:
ext ⟨a, b⟩
  simp only [Finset.mem_product, Finset.mem_singleton, Finset.mem_range, mem_row_iff,
    mem_iff_lt_rowLen, and_comm, and_congr_right_iff]
  rintro rfl
  rfl

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case succ
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
⊢ Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ h a (n + 1 - 1)) (n + 1) =
    Nat.rec (Part.some (g a)) (fun n n_ih ↦ h a n) (n + 1)

Tactic:
· refine ext fun b => ⟨fun H => ?_, fun H => ?_⟩
      · rcases mem_bind_iff.1 H with ⟨c, _, h₂⟩
        exact h₂
      · have : ∀ m, (Nat.rec (motive := fun _ => Part σ)
            (Part.some (g a)) (fun y IH => IH.bind fun _ => h a n) m).Dom := by
          intro m
          induction m <;> simp [*, H.fst]
        exact ⟨⟨this n, H.fst⟩, H.snd⟩

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

Goal state before:
pp: v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec 0 (fun y IH ↦ v.tail.head + IH) v.head = v.head * v.tail.head

Tactic:
induction v.head <;> simp [*, Nat.succ_mul]

Goal state after:
case succ
v : List.Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
a✝ : Nat.rec 0 (fun y IH ↦ v.tail.head + IH) n✝ = n✝ * v.tail.head
⊢ v.tail.head + n✝ * v.tail.head = n✝ * v.tail.head + v.tail.head
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec 0 (fun y IH ↦ (y ::ᵥ IH ::ᵥ v.tail).tail.tail.head + (y ::ᵥ IH ::ᵥ v.tail).tail.head) v.head =
    v.head * v.tail.head

Tactic:
by
    simp; induction v.head <;> simp [*, Nat.succ_mul]; rw [add_comm]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack (m + 1) (n₁ + 1) < ack (m + 1) (n₂ + 1)

Tactic:
rw [ack_succ_succ, ack_succ_succ]

Goal state after:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack (m₁ + 1) (n + 1) < ack (m₂ + 1) (n + 1)

Tactic:
rw [ack_succ_succ, ack_succ_succ]

Goal state after:
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack (m + 1) (n + 1)

Tactic:
· rw [ack_succ_succ]
    apply ack_mono_right m (le_trans _ <| add_add_one_le_ack _ n)
    lia

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ (ack (m + 1) (n + 1) + 1) ^ 2 ≤ ack (m + 1 + 3) (n + 1)

Tactic:
rw [ack_succ_succ, ack_succ_succ]

Goal state after:
m n : ℕ
⊢ (ack m (ack (m + 1) n) + 1) ^ 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)

Tactic:
filter_upwards [hg', (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hfg, hfg]
    with x hx₁ hx₂ hx₃

Goal state after:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
x : ℝ
hx₁ : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
hx₂ : ∀ (y : ℝ), b * id x ≤ y → f y = g y
hx₃ : f x = g x
⊢ ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ (fun n ↦ ↑n * (log ↑n ^ 2)⁻¹) =o[atTop] fun n ↦ ↑n * 1⁻¹

Tactic:
refine IsBigO.mul_isLittleO (isBigO_refl _ _) ?_
      refine IsLittleO.inv_rev ?_ (by simp)
      calc
        _ = (fun (_ : ℕ) => ((1 : ℝ) ^ 2)) := by simp
        _ =o[atTop] (fun (n : ℕ) => (log n) ^ 2) :=
          IsLittleO.pow (IsLittleO.natCast_atTop <| isLittleO_const_log_atTop) (by norm_num)

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

Goal state before:
pp: h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < 1 + ε x

Tactic:
filter_upwards [h₁ (by simp : (0 : ℝ) < 1 / 2), eventually_gt_atTop 1] with x _ hx'

Goal state after:
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
x : ℝ
a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖
hx' : 1 < x
⊢ 0 < 1 + ε x
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)
⊢ (deriv fun x ↦ (fun z ↦ z ^ p a b) x * (fun z ↦ 1 + ε z) x) =ᶠ[atTop] fun x ↦
    deriv (fun z ↦ z ^ p a b) x * (1 + ε x) + x ^ p a b * deriv (fun z ↦ 1 + ε z) x

Tactic:
by
        filter_upwards [eventually_ne_atTop 0, eventually_gt_atTop 1] with x hx hx'
        rw [deriv_fun_mul] <;> aesop

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case neg.succ
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : ¬m = 0
y : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + ((unpair n).2 + 1)))
hy₂ : ∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + ((unpair n).2 + 1))), ¬a = 0
h₂ : evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some (y + ((unpair n).2 + 1))
i : ℕ
im : i + 1 < y + 1
z : ℕ
hz : z ∈ cf.eval (Nat.pair (unpair n).1 (i + ((unpair n).2 + 1)))
z0 : ¬z = 0
⊢ ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (i + 1 + (unpair n).2)), ¬a = 0

Tactic:
exact ⟨z, by simpa [add_comm, add_left_comm] using hz, z0⟩

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

Tactic:
← evalFrom_of_append,

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

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

Tactic:
← evalFrom_of_append,

Goal state after:
case right
α : 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
hq :
  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))
⊢ M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x)))
      (List.drop (↑n) (List.take (↑m) x) ++ List.drop (↑m) x) =
    t
Module: Mathlib.Computability.DFA

Goal state before:
pp: case right
α : 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
hq :
  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))
⊢ M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x)))
      (List.drop (↑n) (List.take (↑m) x) ++ List.drop (↑m) x) =
    t

Tactic:
← evalFrom_of_append,

Goal state after:
case right
α : 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
hq :
  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))
⊢ M.evalFrom s (List.take (↑n) (List.take (↑m) x) ++ (List.drop (↑n) (List.take (↑m) x) ++ List.drop (↑m) x)) = t
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif false then Num.bit1 else Num.bit0) (ofNat' n + 1) = (bif true then Num.bit1 else Num.bit0) (ofNat' n) + 1

Tactic:
simp only [cond, add_one, bit1_succ]

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: f : ℕ →. ℕ
h : Partrec fun v ↦ f v.head
v : ℕ
⊢ f (ofFn fun i ↦ id v).head = f v

Tactic:
simp only [id, head_ofFn]

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
⊢ append (l₁ ++ l₂) l₃ = append l₁ (append l₂ l₃)

Tactic:
refine l₃.induction_on fun l ↦ ?_

Goal state after:
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
l : List Γ
⊢ append (l₁ ++ l₂) (mk l) = append l₁ (append l₂ (mk l))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L R : ListBlank Γ
this :
  ∀ (f : List.Vector Bool n → Stmt Bool (Λ' ?m.41 ?m.42 σ) σ),
    stepAux (readAux n f) v (trTape' enc0 L R) =
      stepAux (f (enc R.head)) v (trTape' enc0 (ListBlank.cons R.head L) R.tail)
⊢ stepAux (read dec f) v (trTape' enc0 L R) = stepAux (f R.head) v (trTape' enc0 L R)

Tactic:
rw [read, this, stepAux_move, encdec, trTape'_move_left enc0]

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L R : ListBlank Γ
this :
  ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux n f) v (trTape' enc0 L R) =
      stepAux (f (enc R.head)) v (trTape' enc0 (ListBlank.cons R.head L) R.tail)
⊢ stepAux (f R.head) v
      (trTape' enc0 (ListBlank.cons R.head L).tail (ListBlank.cons (ListBlank.cons R.head L).head R.tail)) =
    stepAux (f R.head) v (trTape' enc0 L R)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
⊢ L.nth n k = S.reverse[n]?

Tactic:
by
  rw [← proj_map_nth, hL, ← List.map_reverse, ListBlank.nth_mk,
    List.getI_eq_getElem?_getD, List.getElem?_map]
  cases S.reverse[n]? <;> rfl

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

Goal state before:
pp: case zero
n : ℕ
⊢ zero.testBit n = (↑zero).testBit n

Tactic:
dsimp only [testBit]

Goal state after:
case zero
n : ℕ
⊢ false = (↑zero).testBit n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos
n : ℕ
m : PosNum
⊢ (pos m).testBit n = (↑(pos m)).testBit n

Tactic:
dsimp only [testBit]

Goal state after:
case pos
n : ℕ
m : PosNum
⊢ m.testBit n = (↑(pos m)).testBit n
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = (S k).length
h : i < (S k).length
⊢ (List.map some (S k)).reverse.getI i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

Tactic:
rw [List.getI_append]

Goal state after:
case neg.inl.h
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = (S k).length
h : i < (S k).length
⊢ i < (List.map some (S k)).reverse.length
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = tl.length
h : i < tl.length
⊢ ((List.map some tl).reverse ++ [some hd]).getI i = (List.map some tl).reverse.getI i

Tactic:
rw [List.getI_append]

Goal state after:
case neg.inl.h
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h✝ : ¬i = tl.length
h : i < tl.length
⊢ i < (List.map some tl).reverse.length
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
this✝ : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
this : i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
⊢ (ConcreteCategory.hom (π q.fst)) q.snd =
    (ConcreteCategory.hom (i.inv ≫ Sigma.desc π)) ((ConcreteCategory.hom i.hom) t)

Tactic:
by
      rw [this]; rfl

Goal state after: