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

Goal state before:
pp: case h.inr
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
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
v x : V
hx₁ : x ∈ p₁
hx₂ : f ⟨x, hx₁⟩ = v
⊢ ∃! w, if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False

Tactic:
· use x
    have := hx₂ ▸ this ⟨x, hx₁⟩
    simp only [this, ↓reduceDIte, hx₁, hx₂, dite_else_false, forall_exists_index, true_and]
    exact fun _ _ k ↦ Subtype.ext_iff.mp <| hf₁ (hx₂ ▸ k)

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

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
a✝ b✝ : ↑G.edgeSet
⊢ ¬⟨Sym2.map ⇑f ↑a✝, ⋯⟩ = ⟨Sym2.map ⇑f ↑b✝, ⋯⟩ ↔ ¬a✝ = b✝

Tactic:
rw [Subtype.mk.injEq, Subtype.mk.injEq]

Goal state after:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
a✝ b✝ : ↑G.edgeSet
⊢ ¬Sym2.map ⇑f ↑a✝ = Sym2.map ⇑f ↑b✝ ↔ ¬↑a✝ = ↑b✝
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
w : V
hcyc : G.IsCycles
_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath
a✝² :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y _x →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
v : V
p✝ : (p : G.Walk v w) ×' p.IsPath
a✝¹ :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y ⟨v, p✝⟩ →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
p : G.Walk v w
hp : p.IsPath
a✝ :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y ⟨v, ⟨p, hp⟩⟩ →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
h✝ : (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
left✝ : p.snd ≠ w' ∧ G.Adj v w'
hwu : ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this✝ : (G \ p.toSubgraph.spanningCoe).Adj w' v
this : Fintype V
⊢ Nat.card V + 1 - (Walk.cons ⋯ p).length < Nat.card V + 1 - p.length

Tactic:
simp_wf

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
w : V
hcyc : G.IsCycles
_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath
a✝² :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y _x →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
v : V
p✝ : (p : G.Walk v w) ×' p.IsPath
a✝¹ :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y ⟨v, p✝⟩ →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
p : G.Walk v w
hp : p.IsPath
a✝ :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y ⟨v, ⟨p, hp⟩⟩ →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
h✝ : (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
left✝ : p.snd ≠ w' ∧ G.Adj v w'
hwu : ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this✝ : (G \ p.toSubgraph.spanningCoe).Adj w' v
this : Fintype V
⊢ Fintype.card V - p.length < Fintype.card V + 1 - p.length
Module: Mathlib.Combinatorics.SimpleGraph.Partition

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

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

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
P : G.Partition
v✝ w✝ : V
hvw : G.Adj v✝ w✝
⊢ ⟨P.partOfVertex v✝, ⋯⟩ ≠ ⟨P.partOfVertex w✝, ⋯⟩

Tactic:
Ne,

Goal state after:
V : Type u
G : SimpleGraph V
P : G.Partition
v✝ w✝ : V
hvw : G.Adj v✝ w✝
⊢ ¬⟨P.partOfVertex v✝, ⋯⟩ = ⟨P.partOfVertex w✝, ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
⊢ fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe

Tactic:
simp only [Walk.toSubgraph, singletonSubgraph_le_iff, subgraphOfAdj_verts, Set.mem_insert_iff,
      Set.mem_singleton_iff, or_true, sup_of_le_left]

Goal state after:
V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
⊢ fromEdgeSet {s(v, w)} = (G.subgraphOfAdj hadj).spanningCoe
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
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ 2 * k

Tactic:
apply le_trans (card_commonNeighbors_le_degree_left _ _ _)

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ G.degree v ≤ 2 * k
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case refine_4
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
p₁✝ p₂✝ : Finset (Fin n)
v₁ v₂ : Fin n
p₁ : Finset (Fin n)
hp₁ : p₁ ∈ K.parts
hv₁ : v₁ ∈ ↑(y p₁ ⋯)
hyp₁ : y p₁ ⋯ = p₁✝
hy₁' : y p₁ hp₁ ⊆ p₁ ∧ #(y p₁ hp₁) = t
p₂ : Finset (Fin n)
hp₂ : p₂ ∈ K.parts
hne : y p₁ ⋯ ≠ y p₂ ⋯
hv₂ : v₂ ∈ ↑(y p₂ ⋯)
hyp₂ : y p₂ ⋯ = p₂✝
hy₂' : y p₂ hp₂ ⊆ p₂ ∧ #(y p₂ hp₂) = t
heq : p₁ = p₂
⊢ False

Tactic:
simp [← heq] at hne

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

Goal state before:
pp: case hi.some.some.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n✝ n : ℕ
IH✝ :
  ∀ m ≤ n,
    encode
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) m)) =
      encode (decode m)
a : α
val✝¹ : List ℕ
val✝ : List α
IH : encode (some val✝¹) = encode (some val✝)
⊢ encode (Option.map (List.cons (encode a)) (some val✝¹)) = encode (Option.map (List.cons a) (some val✝))

Tactic:
exact congr_arg (fun k => (Nat.pair (encode a) k).succ.succ) (Nat.succ.inj IH)

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
⊢ ∀ (m k : ℕ), n ≤ k + m → Acc (lbp p) k

Tactic:
intro m k kn

Goal state after:
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m k : ℕ
kn : n ≤ k + m
⊢ Acc (lbp p) k
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: n₁ n₂ : ℕ
h : Code.const (n₁ + 1) = Code.const (n₂ + 1)
⊢ n₁ + 1 = n₂ + 1

Tactic:
by
    dsimp [Nat.Partrec.Code.const] at h
    injection h with h₁ h₂
    simp only [const_inj h₂]

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
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
⊢ ↑n ^ p a b * ↑n * (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1)) ≤ ↑n ^ p a b * ↑n * (c₂ * g ↑n / (c₁ * ↑n) ^ (p a b + 1))

Tactic:
gcongr; exact hn₁ i

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
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t

Tactic:
obtain ⟨n, m, hneq, heq⟩ :=
    Fintype.exists_ne_map_eq_of_card_lt
      (fun n : Fin (Fintype.card σ + 1) => M.evalFrom s (x.take n)) (by simp)

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)
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
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
⊢ T =O[atTop] asympBound g a b

Tactic:
calc T
    _ =O[atTop] (fun n => (1 - ε n) * asympBound g a b n) := by
      exact R.T_isBigO_smoothingFn_mul_asympBound
    _ =O[atTop] (fun n => 1 * asympBound g a b n) := by
      refine IsBigO.mul (isBigO_const_of_tendsto (y := 1) ?_ one_ne_zero) (isBigO_refl _ _)
      rw [← Function.comp_def (fun n => 1 - ε n) Nat.cast]
      exact Tendsto.comp isEquivalent_one_sub_smoothingFn_one.tendsto_const
        tendsto_natCast_atTop_atTop
    _ = asympBound g a b := by simp

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

Goal state before:
pp: m k : ℕ
⊢ shiftLeft' true m (k + 1) + 1 = (m + 1) * 2 ^ (k + 1)

Tactic:
by
    rw [shiftLeft', bit_val, Bool.toNat_true, Nat.add_assoc, ← Nat.mul_add_one,
      shiftLeft'_true_eq_mul_pow m k, Nat.mul_left_comm, Nat.mul_comm 2, Nat.pow_succ]

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

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 1
⊢ (n + 1) % 2 = 0

Tactic:
rw [add_mod, ← @mod_mod_of_dvd _ 4 n <| by simp, ← Fin.val_ofNat 4, h]

Goal state after:
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 1
⊢ (↑1 % 2 + 1 % 2) % 2 = 0
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length ≠ l.length ↔ none ∈ l

Tactic:
Ne,

Goal state after:
α : Type u_1
l : List (Option α)
⊢ ¬l.reduceOption.length = l.length ↔ none ∈ l
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
p : Prop
x : List α
⊢ x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p

Tactic:
induction x generalizing S with
  | nil => simp only [nil_mem_acceptsFrom, mem_ofPred_eq]; tauto
  | cons a x ih =>
    have h : M.stepSet {s ∈ S | p} a = {s ∈ M.stepSet S a | p} := by
      ext s; simp only [stepSet, mem_ofPred_eq, mem_iUnion, exists_prop]; tauto
    simp [h, ih]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
s✝ t✝ : σ
x✝ : List α
p : Nonempty (M.Path s✝ t✝ x✝)
t s s' : σ
a : α
x : List α
h₁ : s' ∈ M.step s a
h₂ : M.Path s' t x
⊢ ∃ t_1 ∈ M.step s a, t ∈ M.evalFrom {t_1} x

Tactic:
exact ⟨s', h₁, mem_evalFrom_iff_nonempty_path.2 ⟨h₂⟩⟩

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a ≤ b ∨ b ≤ a

Tactic:
intro a b
    transfer_rw
    apply le_total

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
n : PosNum
⊢ ↑(n + 1) = ↑n + 1

Tactic:
cast_add,

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
n : PosNum
⊢ ↑n + ↑1 = ↑n + 1
Module: Mathlib.Computability.Halting

Goal state before:
pp: C : Set (ℕ →. ℕ)
h : ComputablePred fun c ↦ c.eval ∈ C
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
⊢ g ∈ C

Tactic:
by
  obtain ⟨_, h⟩ := h
  obtain ⟨c, e⟩ :=
    fixed_point₂
      (Partrec.cond (h.comp fst) ((Partrec.nat_iff.2 hg).comp snd).to₂
          ((Partrec.nat_iff.2 hf).comp snd).to₂).to₂
  simp only [Bool.cond_decide] at e
  by_cases H : eval c ∈ C <;> simp_all

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
n : Num
⊢ ↑(n.bit0 + 1) = 2 * ↑n + 1

Tactic:
cast_add,

Goal state after:
α : Type u_1
inst✝ : NonAssocSemiring α
n : Num
⊢ ↑n.bit0 + ↑1 = 2 * ↑n + 1
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
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
h : x ∈ f a ∨ x ∈ g a
this : (k a).Dom
⊢ x ∈ k a

Tactic:
refine ⟨this, ?_⟩

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
h : x ∈ f a ∨ x ∈ g a
this : (k a).Dom
⊢ (k a).get this = x
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
⊢ Computable fun x ↦ Nat.find ⋯

Tactic:
have h : Partrec (fun x ↦ Nat.rfind fun n => Part.some (decide (P x n))) :=
    Partrec.rfind hP_comp.decide.partrec
  refine h.of_eq_tot fun x ↦ ?_
  simp +contextual [Nat.find_spec]

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

Goal state before:
pp: ι : Type u_1
Γ : ι → Type u_2
inst✝ : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ (ListBlank.map (proj i) L).nth n = L.nth n i

Tactic:
rw [ListBlank.nth_map]

Goal state after:
ι : Type u_1
Γ : ι → Type u_2
inst✝ : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ (proj i).f (L.nth n) = L.nth n i
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
c' : Cfg Γ Λ
h₁ : c' ∈ step M { q := q, Tape := T }
h₂ : { q := q, Tape := T }.q ∈ S
⊢ c'.q ∈ S

Tactic:
rcases Option.map_eq_some_iff.1 h₁ with ⟨⟨q', a⟩, h, rfl⟩

Goal state after:
Γ : Type u_1
Λ : Type u_2
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
h₂ : { q := q, Tape := T }.q ∈ S
q' : Λ
a : Stmt Γ
h : M q T.head = some (q', a)
h₁ :
  (match (q', a) with
    | (q', a) =>
      { q := q',
        Tape :=
          match a with
          | Stmt.move d => Tape.move d T
          | Stmt.write a => Tape.write a T }) ∈
    step M { q := q, Tape := T }
⊢ (match (q', a) with
      | (q', a) =>
        { q := q',
          Tape :=
            match a with
            | Stmt.move d => Tape.move d T
            | Stmt.write a => Tape.write a T }).q ∈
    S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
l : Γ → σ → Λ
hs : ∀ (a : Γ) (v : σ), l a v ∈ S
h : q₁ = goto l
⊢ SupportsStmt S q₁

Tactic:
subst h; exact hs

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

Goal state before:
pp: case right.some.some.move.refl
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
d : Dir
h₂ : some (TM1.Stmt.move d val✝) ∈ TM1.stmts M S
hs : TM1.SupportsStmt S (TM1.Stmt.move d val✝)
a_ih✝ :
  ∀ (v : σ),
    some val✝ ∈ TM1.stmts M S →
      some (trAux M a val✝ v) = some ((some val✝, v'), move d) → TM1.SupportsStmt S val✝ → some val✝ ∈ TM1.stmts M S
⊢ val✝ ∈ insert (TM1.Stmt.move d val✝) (TM1.stmts₁ val✝)

Tactic:
exact Finset.mem_insert_of_mem TM1.stmts₁_self

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

Goal state before:
pp: case right.some.some.write.refl
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
b : Γ → σ → Γ
h₂ : some (TM1.Stmt.write b val✝) ∈ TM1.stmts M S
hs : TM1.SupportsStmt S (TM1.Stmt.write b val✝)
a_ih✝ :
  ∀ (v : σ),
    some val✝ ∈ TM1.stmts M S →
      some (trAux M a val✝ v) = some ((some val✝, v'), write (b a v')) →
        TM1.SupportsStmt S val✝ → some val✝ ∈ TM1.stmts M S
⊢ val✝ ∈ insert (TM1.Stmt.write b val✝) (TM1.stmts₁ val✝)

Tactic:
exact Finset.mem_insert_of_mem TM1.stmts₁_self

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

Goal state before:
pp: case right.some.some.load
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
b : Γ → σ → σ
q : TM1.Stmt Γ Λ σ
IH :
  ∀ (v : σ),
    some q ∈ TM1.stmts M S →
      some (trAux M a q v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.load b q) ∈ TM1.stmts M S
h₁ : some (trAux M a (TM1.Stmt.load b q) v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.load b q)
⊢ q ∈ insert (TM1.Stmt.load b q) (TM1.stmts₁ q)

Tactic:
exact Finset.mem_insert_of_mem TM1.stmts₁_self

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

Goal state before:
pp: case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
l : σ → Λ
hs : ∀ (v : σ), l v ∈ S
h : q₁ = goto l
⊢ SupportsStmt S q₁

Tactic:
subst h; exact hs

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

Goal state before:
pp: case pop.cons
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
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k (hd :: tl).tail k_1)).reverse) ∧
      (bif ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L))).head.1 then
          TM1.stepAux q (f v none) ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))
        else
          TM1.stepAux q
            (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
            (Tape.write
              ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.1,
                update
                  (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k
                  none)
              (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))))) =
        TM1.stepAux q (f v (hd :: tl).head?)
          ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom L')))

Tactic:
· refine
        ⟨_, fun k' ↦ ?_, by
          erw [List.length_cons, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_succ_fst,
            cond_false, iterate_succ', Function.comp, Tape.move_right_left, Tape.move_right_n_head,
            Tape.mk'_nth_nat, Tape.write_move_right_n fun a : Γ' K Γ ↦ (a.1, update a.2 k none),
            addBottom_modifyNth fun a ↦ update a k none, addBottom_nth_snd,
            stk_nth_val _ (hL k), e,
            show (List.cons hd tl).reverse[tl.length]? = some hd by
              rw [List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length],
            List.head?, List.tail]⟩
      refine ListBlank.ext fun i ↦ ?_
      rw [ListBlank.nth_map, ListBlank.nth_modifyNth, proj, PointedMap.mk_val]
      by_cases h' : k' = k
      · subst k'
        split_ifs with h <;> simp only [Function.update_self, ListBlank.nth_mk, List.tail]
        · rw [List.getI_eq_default]
          · rfl
          rw [h, List.length_reverse, List.length_map]
        rw [← proj_map_nth, hL, ListBlank.nth_mk, e, List.map, List.reverse_cons]
        rcases lt_or_gt_of_ne h with h | h
        · rw [List.getI_append]
          simpa only [List.length_map, List.length_reverse] using h
        · rw [List.getI_eq_default, List.getI_eq_default] <;>
            simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse,
              List.length_append, List.length_map]
      · split_ifs <;> rw [Function.update_of_ne h', ← proj_map_nth, hL]
        rw [Function.update_of_ne h']

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos.refine_3
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ X ⁻¹' {a})

pp: case pos.refine_4
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ IsClosed (↑c ∩ X ⁻¹' {a})

Tactic:
all_goals exact (C_sub c.mem).left.inter <| (T1Space.t1 a).preimage X_cont

Goal state after: