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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
⊢ ∃ u, G.IsTutteViolator u

Tactic:
classical
  cases nonempty_fintype V
  -- It suffices to consider the edge-maximal case
  obtain ⟨Gmax, hSubgraph, hMatchingFree, hMaximal⟩ := exists_maximal_isMatchingFree h
  refine ⟨Gmax.universalVerts, .mono hSubgraph ?_⟩
  by_contra! hc
  simp only [IsTutteViolator, Set.ncard_eq_toFinset_card', Set.toFinset_card] at hc
  by_cases! h' : ∀ (K : ConnectedComponent Gmax.deleteUniversalVerts.coe),
      Gmax.deleteUniversalVerts.coe.IsClique K.supp
  · -- Deleting universal vertices splits the graph into cliques
    rw [Fintype.card_eq_nat_card] at hc
    simp_rw [Fintype.card_eq_nat_card, Nat.card_coe_set_eq] at hc
    push Not at hc
    obtain ⟨M, hM⟩ := Subgraph.IsPerfectMatching.exists_of_isClique_supp hvEven
      (by simpa [IsTutteViolator] using hc) h'
    exact hMatchingFree M hM
  · -- Deleting universal vertices does not result in only cliques
    obtain ⟨K, hK⟩ := h'
    obtain ⟨x, y, hxy⟩ := (not_isClique_iff _).mp hK
    obtain ⟨p, hp⟩ := Reachable.exists_path_of_dist (K.connected_toSimpleGraph x y)
    obtain ⟨x, a, b, hxa, hxb, hnadjxb, hnxb⟩ := Walk.exists_adj_adj_not_adj_ne hp.2
      (p.reachable.one_lt_dist_of_ne_of_not_adj hxy.1 hxy.2)
    simp only [ConnectedComponent.toSimpleGraph, deleteUniversalVerts, universalVerts,
      Subgraph.verts_top, comap_adj, Function.Embedding.coe_subtype,
      Subgraph.coe_adj, Subgraph.induce_adj, Subtype.coe_prop, Subgraph.top_adj, true_and]
      at hxa hxb hnadjxb
    obtain ⟨c, hc⟩ : ∃ (c : V), (a : V) ≠ c ∧ ¬ Gmax.Adj a c := by
      simpa [universalVerts, IsUniversal] using a.1.2.2
    have hbnec : b.val.val ≠ c := by rintro rfl; exact hc.2 hxb
    obtain ⟨_, hG1⟩ := hMaximal _ <| left_lt_sup.mpr (by
      rw [edge_le_iff (v := x.1.1) (w := b.1.1)]
      simp [hnadjxb, Subtype.val_injective.ne <| Subtype.val_injective.ne hnxb])
    obtain ⟨_, hG2⟩ := hMaximal _ <| left_lt_sup.mpr (by
      rwa [edge_le_iff (v := a.1.1) (w := c), not_or])
    have hcnex : x.val.val ≠ c := by rintro rfl; exact hc.2 hxa.symm
    obtain ⟨Mcon, hMcon⟩ := tutte_exists_isPerfectMatching_of_near_matchings hxa
      hxb hnadjxb (fun hadj ↦ hc.2 hadj) (by lia) hcnex hc.1 hbnec hG1 hG2
    exact hMatchingFree Mcon hMcon

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

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

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

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

Goal state before:
pp: x : ℝ
⊢ deriv ε x = -x⁻¹ / log x ^ 2

Tactic:
simp [deriv_smoothingFn]

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

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

Tactic:
have C_pos : 0 ≤ C := by grind [inv_pos]

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
⊢ f x + g x ≥ f x - ‖g x‖

Tactic:
by
                rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le (g x)

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
⊢ 1 / 2 * ‖f u‖ = 1 / 2 * f u

Tactic:
congr; simp only [norm_eq_abs, abs_eq_self, hfu_nonneg]

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
hfg₃ : ‖g u‖ ≤ 1 / 2 * f u
⊢ f u + g u ≤ f u + ‖g u‖

Tactic:
by gcongr; exact le_norm_self (g u)

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
hfg₃ : ‖g u‖ ≤ 1 / 2 * f u
⊢ f u + g u ≤ 3 * c₂ * (f x + g x)

Tactic:
calc _ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
           _ ≤ f u + 1 / 2 * f u := by gcongr
           _ = 3 / 2 * f u := by ring
           _ ≤ 3 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
           _ = 3 * c₂ * (1 / 2 * f x) := by ring
           _ ≤ 3 * c₂ * (f x + g x) := by gcongr

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

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

Tactic:
have C_pos : 0 ≤ C := by grind [inv_pos]

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
⊢ f x + g x ≥ f x - ‖g x‖

Tactic:
by
                rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le (g x)

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ f u + g u ≤ f u + ‖g u‖

Tactic:
by gcongr; exact le_norm_self (g u)

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

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

Tactic:
by simp [Num.ofNat']

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₁ s₂ : σ
x' : List (Option α)
hs₁ : s₁ ∈ M.start
hs₂ : s₂ ∈ M.accept
h : x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
⊢ x ∈ M.accepts

Tactic:
have := M.mem_evalFrom_iff_exists.mpr ⟨_, hs₁, M.mem_evalFrom_iff_exists_path.mpr ⟨_, h⟩⟩

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₁ s₂ : σ
x' : List (Option α)
hs₁ : s₁ ∈ M.start
hs₂ : s₂ ∈ M.accept
h : x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
this : s₂ ∈ M.evalFrom M.start x
⊢ x ∈ M.accepts
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: p : PosNum
⊢ (↑p.pred').succ = ↑(pos p)

Tactic:
rw [PosNum.pred'_to_nat, Nat.succ_pred_eq_of_pos (PosNum.to_nat_pos _)]

Goal state after:
p : PosNum
⊢ ↑p = ↑(pos p)
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: n : ℕ
f : ℕ →. ℕ
g : List.Vector ℕ n → ℕ
hf : Partrec' fun v ↦ f v.head
hg : Partrec' ↑g
⊢ Partrec' fun v ↦ f (g v)

Tactic:
simpa using hf.comp' (Partrec'.cons hg Partrec'.nil)

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_1.some.inl
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝¹ : b ∈ eval f a✝
a : σ
h✝ : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
h : Sum.inl b ∈ Part.some ((f a).elim (Sum.inl a) Sum.inr)
⊢ Reaches f a b ∧ f b = none

Tactic:
rw [e] at h

Goal state after:
case refine_1.some.inl
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝¹ : b ∈ eval f a✝
a : σ
h✝ : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
h : Sum.inl b ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
⊢ Reaches f a b ∧ f b = none
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_1.some.inr
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝¹ : b ∈ eval f a✝
a : σ
h✝ : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
w✝ : σ
h : Sum.inr w✝ ∈ Part.some ((f a).elim (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) w✝
⊢ Reaches f a b ∧ f b = none

Tactic:
rw [e] at h

Goal state after:
case refine_1.some.inr
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝¹ : b ∈ eval f a✝
a : σ
h✝ : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
w✝ : σ
h : Sum.inr w✝ ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s ↦ Part.some ((f s).elim (Sum.inl s) Sum.inr)) w✝
⊢ Reaches f a b ∧ f b = none
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₂
⊢ ∃ b₁, tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁

Tactic:
refine ⟨_, cc, mem_eval.2 ⟨ac, ?_⟩⟩

Goal state after:
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₂
⊢ f₁ c₁ = none
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth 0 = if 0 = n + 1 then f (L.nth 0) else L.nth 0

Tactic:
rw [if_neg (Nat.succ_ne_zero _).symm]
      simp only [ListBlank.nth_zero, ListBlank.head_cons, ListBlank.modifyNth]

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: O : Set (ℕ →. ℕ)
⊢ ∀ g ∈ O, RecursiveIn O g

Tactic:
intro g hg

Goal state after:
O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ RecursiveIn O g
Module: Mathlib.Computability.Reduce

Goal state before:
pp: d₁ d₂ d₃ : ManyOneDegree
⊢ d₁ ≤ d₂ → d₂ ≤ d₃ → d₁ ≤ d₃

Tactic:
by
  induction d₁ using ManyOneDegree.ind_on
  induction d₂ using ManyOneDegree.ind_on
  induction d₃ using ManyOneDegree.ind_on
  apply ManyOneReducible.trans

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

Goal state before:
pp: case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a✝ : Dir
q : Stmt Γ Λ σ
IH : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q → (stepAux q v T).l ∈ Finset.insertNone S
v : σ
T : Tape Γ
hs : SupportsStmt S (move a✝ q)
⊢ (stepAux (move a✝ q) v T).l ∈ Finset.insertNone S

Tactic:
exact IH _ _ hs

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

Goal state before:
pp: case write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a✝ : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q → (stepAux q v T).l ∈ Finset.insertNone S
v : σ
T : Tape Γ
hs : SupportsStmt S (write a✝ q)
⊢ (stepAux (write a✝ q) v T).l ∈ Finset.insertNone S

Tactic:
exact IH _ _ hs

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

Goal state before:
pp: case load
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a✝ : Γ → σ → σ
q : Stmt Γ Λ σ
IH : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q → (stepAux q v T).l ∈ Finset.insertNone S
v : σ
T : Tape Γ
hs : SupportsStmt S (load a✝ q)
⊢ (stepAux (load a✝ q) v T).l ∈ Finset.insertNone S

Tactic:
exact IH _ _ hs

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

Goal state before:
pp: case load
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a✝¹ : σ → σ
a✝ : Stmt Γ Λ σ
IH : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S a✝ → (stepAux a✝ v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (load a✝¹ a✝)
⊢ (stepAux (load a✝¹ a✝) v T).l ∈ Finset.insertNone S

Tactic:
exact IH _ _ hs

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

Goal state before:
pp: case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
k✝ : K
a✝¹ : σ → Γ k✝
a✝ : Stmt Γ Λ σ
IH : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S a✝ → (stepAux a✝ v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (push k✝ a✝¹ a✝)
⊢ (stepAux (push k✝ a✝¹ a✝) v T).l ∈ Finset.insertNone S

Tactic:
exact IH _ _ hs

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

Goal state before:
pp: case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
IH : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S a✝ → (stepAux a✝ v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (peek k✝ a✝¹ a✝)
⊢ (stepAux (peek k✝ a✝¹ a✝) v T).l ∈ Finset.insertNone S

Tactic:
exact IH _ _ hs

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

Goal state before:
pp: case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
IH : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S a✝ → (stepAux a✝ v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (pop k✝ a✝¹ a✝)
⊢ (stepAux (pop k✝ a✝¹ a✝) v T).l ∈ Finset.insertNone S

Tactic:
exact IH _ _ hs

Goal state after:
Module: Mathlib.Computability.RegularExpressions

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

Tactic:
rw [plus_def, add_rmatch_iff, ih₁, ih₂]

Goal state after:
case plus
α : Type u_1
inst✝ : DecidableEq α
a✝¹ a✝ : RegularExpression α
ih₁ : ∀ (x : List α), a✝¹.rmatch x = true ↔ x ∈ a✝¹.matches'
ih₂ : ∀ (x : List α), a✝.rmatch x = true ↔ x ∈ a✝.matches'
x : List α
⊢ x ∈ a✝¹.matches' ∨ x ∈ a✝.matches' ↔ x ∈ (a✝¹ + a✝).matches'
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hf : ∃ c, ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v
hg : ∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> ((Vector.mOfFn fun i ↦ g i v) >>= f)

Tactic:
rsuffices ⟨cg, hg⟩ :
    ∃ c : Code, ∀ v : List.Vector ℕ m,
      c.eval v.1 = Subtype.val <$> List.Vector.mOfFn fun i => g i v

Goal state after:
m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hf : ∃ c, ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg : ∀ (v : List.Vector ℕ m), cg.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
⊢ ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> ((Vector.mOfFn fun i ↦ g i v) >>= f)

m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hf : ∃ c, ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v
hg : ∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
⊢ IsOpenEmbedding
    (⇑(homeoOfIso ((colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X))) ∘
      ⇑(ConcreteCategory.hom (Sigma.ι X a)))

Tactic:
convert! finiteCoproduct.isOpenEmbedding_ι X a

Goal state after:
case e'_5
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
e_2✝ : ↑(finiteCoproduct.cofan X).pt.toTop = (fun X ↦ ↑X.toTop) (finiteCoproduct X)
⊢ ⇑(homeoOfIso ((colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X))) ∘
      ⇑(ConcreteCategory.hom (Sigma.ι X a)) =
    ⇑(ConcreteCategory.hom (finiteCoproduct.ι X a))
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case some
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
b : ?m.88
c : ?m.103 b
r : Reaches (TM1.step (tr M)) (?m.104 b) (?m.105 b)
⊢ match TM2.step M { l := some l, var := v, stk := S } with
  | some b₁ =>
    ∃ b₂,
      TrCfg b₁ b₂ ∧
        Reaches₁ (TM1.step (tr M)) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } b₂
  | none => TM1.step (tr M) { l := Option.map normal (some l), var := v, Tape := Tape.mk' ∅ (addBottom L) } = none

Tactic:
exact ⟨b, c, TransGen.head' rfl r⟩

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

Goal state before:
pp: case halt
v : List ℕ
⊢ eval step (stepRet Cont.halt v) = pure (Cfg.halt v)

Tactic:
exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)

Goal state after: