mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case inr
Γ : Type ?u.6
inst✝ : Inhabited Γ
α : Sort ?u.10
l : ListBlank Γ
f : List Γ → α
H : ∀ (a b : List Γ), BlankExtends a b → f a = f b
a b : List Γ
h : BlankExtends b a
⊢ f a = f b

Tactic:
exact (H _ _ h).symm

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case tail
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
IH : ∃ c₁ c₂, Reaches f₂ b✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
⊢ ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
rcases IH with ⟨e₁, e₂, ce, ee, ae⟩

Goal state after:
case tail
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
e₂ : σ₂
ce : Reaches f₂ b✝ e₂
ee : tr e₁ e₂
ae : Reaches f₁ a₁ e₁
⊢ ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
⊢ (∀ (i_1 : ℕ), L₁.nth i_1 = L₂.nth i_1) → L₁ = L₂

Tactic:
refine ListBlank.induction_on L₁ fun l₁ ↦ ListBlank.induction_on L₂ fun l₂ H ↦ ?_
  wlog h : l₁.length ≤ l₂.length
  · cases le_total l₁.length l₂.length <;> [skip; symm] <;> apply this <;> try assumption
    intro
    rw [H]
  refine Quotient.sound' (Or.inl ⟨l₂.length - l₁.length, ?_⟩)
  refine List.ext_getElem ?_ fun i h h₂ ↦ Eq.symm ?_
  · simp only [Nat.add_sub_cancel' h, List.length_append, List.length_replicate]
  simp only [ListBlank.nth_mk] at H
  rcases lt_or_ge i l₁.length with h' | h'
  · simp [h', List.getElem_append h₂, ← List.getI_eq_getElem _ h, ← List.getI_eq_getElem _ h', H]
  · rw [List.getElem_append_right h', List.getElem_replicate,
      ← List.getI_eq_default _ h', H, List.getI_eq_getElem _ h]

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n i : ℕ
L : ListBlank Γ
⊢ (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i

Tactic:
induction n generalizing i L with
  | zero =>
    cases i <;> simp only [ListBlank.nth_zero, if_true, ListBlank.head_cons, ListBlank.modifyNth,
      ListBlank.nth_succ, if_false, ListBlank.tail_cons, reduceCtorEq]
  | succ n IH =>
    cases i
    · rw [if_neg (Nat.succ_ne_zero _).symm]
      simp only [ListBlank.nth_zero, ListBlank.head_cons, ListBlank.modifyNth]
    · simp only [IH, ListBlank.modifyNth, ListBlank.nth_succ, ListBlank.tail_cons, Nat.succ.injEq]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f l).head = f.f l.head

Tactic:
rw [← ListBlank.cons_head_tail l]
  induction l using Quotient.inductionOn'
  rfl

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f l).tail = map f l.tail

Tactic:
rw [← ListBlank.cons_head_tail l]
  induction l using Quotient.inductionOn'
  rfl

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case nil.mp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
⊢ P.matchEpsilon = true ∧ Q.matchEpsilon = true

Tactic:
rwa [Bool.and_eq_true_iff] at h

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case pos.mp
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨ (Q.deriv a).rmatch x = true →
    ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

pp: case pos.mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
⊢ (∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true) →
    (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨ (Q.deriv a).rmatch x = true

Tactic:
· rintro (⟨t, u, _⟩ | h)
        · exact ⟨a :: t, u, by tauto⟩
        · exact ⟨[], a :: x, rfl, hepsilon, h⟩

Goal state after:
case pos.mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
⊢ (∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true) →
    (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨ (Q.deriv a).rmatch x = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
l₁ : List Bool
⊢ ∀ {l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) =
        Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)

Tactic:
l₂

Goal state after:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
l₁ l₂ : List Bool
⊢ (enc a).toList = l₁.reverseAux l₂ →
    (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) =
      Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
l₁ : List Bool
⊢ ∀ (l₂ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')

Tactic:
l₂

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
l₁ l₂ : List Bool
⊢ ∀ (l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case cons.cons
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
b : Bool
l₂' : List Bool
e : l₂'.length = l₂.length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
List.reverseAux,

Goal state after:
case cons.cons
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
b : Bool
l₂' : List Bool
e : l₂'.length = l₂.length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux (a :: l₁)) L') R')
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: ⊢ zero'.eval = fun v ↦ pure (0 :: v)

Tactic:
by simp [eval]

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

Goal state before:
pp: ⊢ succ.eval = fun v ↦ pure [v.headI.succ]

Tactic:
by simp [eval]

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

Goal state before:
pp: ⊢ tail.eval = fun v ↦ pure v.tail

Tactic:
by simp [eval]

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

Goal state before:
pp: f fs : Code
⊢ (f.cons fs).eval = fun v ↦ do
    let n ← f.eval v
    let ns ← fs.eval v
    pure (n.headI :: ns)

Tactic:
by simp [eval]

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

Goal state before:
pp: f g : Code
⊢ (f.comp g).eval = fun v ↦ g.eval v >>= f.eval

Tactic:
by simp [eval]

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

Goal state before:
pp: k k' : Cont
v : List ℕ
⊢ (k.then k').eval v = k.eval v >>= k'.eval

Tactic:
induction k generalizing v with
  | halt => simp only [Cont.eval, Cont.then, pure_bind]
  | cons₁ => simp only [Cont.eval, Cont.then, bind_assoc, *]
  | cons₂ => simp only [Cont.eval, Cont.then, *]
  | comp _ _ k_ih => simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]
  | fix _ _ k_ih =>
    simp only [Cont.eval, Cont.then, *]
    split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]

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

Goal state before:
pp: 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 : Λ
N : TM2.Stmt Γ Λ σ
⊢ ∃ b, TrCfg (TM2.stepAux N v S) b ∧ Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal N) v (Tape.mk' ∅ (addBottom L))) b

Tactic:
induction N using stmtStRec generalizing v S L hT with

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

Goal state before:
pp: case nil.cons.true
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e₁ : some a = o
e₂ : Sk = L₂
⊢ ReflTransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some q, var := o, stk := update S k Sk } { l := some q, var := o, stk := update S k L₂ }

Tactic:
e₂

Goal state after:
case nil.cons.true
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e₁ : some a = o
e₂ : Sk = L₂
⊢ ReflTransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some q, var := o, stk := update S k L₂ } { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
⊢ Continuous f → Surjective f → ∃ h, Continuous h ∧ f ∘ h = φ

Tactic:
f_cont

Goal state after:
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
⊢ Surjective f → ∃ h, Continuous h ∧ f ∘ h = φ
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case zero
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trNum Num.zero ++ [Γ'.cons]) [] c d }
    { l := some q, var := none, stk := elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d }

Tactic:
refine TransGen.head rfl ?_
    simp only [Option.mem_def]
    convert! unrev_ok using 1
    simp only [elim_update_rev, elim_rev, elim_main, List.reverseAux_nil, elim_update_main]
    rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case empty
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
S : Set (Set ↑(F.obj j))
P : J → Set ↑(F.obj j)
he : Set.univ ∈ S
⊢ (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ ∅, P e ∈ S) → ⋂ e ∈ ∅, P e ∈ S

Tactic:
_hh

Goal state after:
case empty
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
S : Set (Set ↑(F.obj j))
P : J → Set ↑(F.obj j)
he : Set.univ ∈ S
_hh : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
⊢ (∀ e ∈ ∅, P e ∈ S) → ⋂ e ∈ ∅, P e ∈ S
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
hff : ∀ (a : α), ∃ j g, ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
⊢ ∃ j g,
    LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
choose j g h using hff

Goal state after:
case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
⊢ ∃ j g,
    LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Module: Mathlib.Logic.Function.FiberPartition

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : Y → Z
g : X → Y
a : Fiber (f ∘ g)
⊢ image (f ∘ g) a = image f (mk f (g (preimage (f ∘ g) a)))

Tactic:
rw [← map_preimage_eq_image_map _ _ a, mk_image]

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Sequence

Goal state before:
pp: case refine_2
⊢ IsClosedMap ⇑natUnionInftyEmbedding

Tactic:
· exact fun _ hC => (hC.isCompact.image natUnionInftyEmbedding.continuous).isClosed

Goal state after:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
⊢ SeqContinuous (topCatAdjunctionCounitEquiv X).invFun

Tactic:
unfold SeqContinuous

Goal state after:
X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
⊢ ∀ ⦃x : ℕ → ↑X⦄ ⦃p : ↑X⦄,
    Filter.Tendsto x Filter.atTop (nhds p) →
      Filter.Tendsto ((topCatAdjunctionCounitEquiv X).invFun ∘ x) Filter.atTop
        (nhds ((topCatAdjunctionCounitEquiv X).invFun p))
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m α
x✝ : β
⊢ (⇑(foldrM.ofFreeMonoid f) ∘ FreeMonoid.of) x✝ = (foldrM.mk ∘ f) x✝

Tactic:
simp [(· ∘ ·), foldrM.ofFreeMonoid, foldrM.mk, Function.flip_def]

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : OptionT m α) (next : Label ω (OptionT m) γ → α → OptionT m ω),
    (callCC fun f ↦ cmd >>= next f) = do
      let x ← cmd
      callCC fun f ↦ next f x

Tactic:
by
    refine fun _ _ => OptionT.ext ?_
    simpa [callCC, Option.elimM, callCC_bind_right] using
      bind_congr fun | some _ => rfl | none => by simp [@callCC_dummy m _]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec.{u_1} n✝} (a : α a✝) (b : β a✝), prod.fst a✝ (prod.mk a✝ a b) = a
α β : TypeVec.{u_1} (n✝ + 1)
a : α a✝.fs
b : β a✝.fs
⊢ prod.fst a✝.fs (prod.mk a✝.fs a b) = a

Tactic:
| fs _ i_ih =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec.{u_1} n✝} (a : α a✝) (b : β a✝), prod.snd a✝ (prod.mk a✝ a b) = b
α β : TypeVec.{u_1} (n✝ + 1)
a : α a✝.fs
b : β a✝.fs
⊢ prod.snd a✝.fs (prod.mk a✝.fs a b) = b

Tactic:
| fs _ i_ih =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α α' β β' : TypeVec.{u_1} n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.fst ⊚ (f ⊗' g)) a✝ = (f ⊚ prod.fst) a✝
α α' β β' : TypeVec.{u_1} (n✝ + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.fst ⊚ (f ⊗' g)) a✝.fs = (f ⊚ prod.fst) a✝.fs

Tactic:
| fs _ i_ih =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α α' β β' : TypeVec.{u_1} n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.snd ⊚ (f ⊗' g)) a✝ = (g ⊚ prod.snd) a✝
α α' β β' : TypeVec.{u_1} (n✝ + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) a✝.fs = (g ⊚ prod.snd) a✝.fs

Tactic:
| fs _ i_ih =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝}, (prod.fst ⊚ prod.diag) a✝ = id a✝
α : TypeVec.{u_1} (n✝ + 1)
⊢ (prod.fst ⊚ prod.diag) a✝.fs = id a✝.fs

Tactic:
| fs _ i_ih =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝}, (prod.snd ⊚ prod.diag) a✝ = id a✝
α : TypeVec.{u_1} (n✝ + 1)
⊢ (prod.snd ⊚ prod.diag) a✝.fs = id a✝.fs

Tactic:
| fs _ i_ih =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝} {x y : α a✝}, ofRepeat (α.repeatEq a✝ (prod.mk a✝ x y)) ↔ x = y
α : TypeVec.{u_1} (n✝ + 1)
x y : α a✝.fs
⊢ ofRepeat (α.repeatEq a✝.fs (prod.mk a✝.fs x y)) ↔ x = y

Tactic:
| fs _ i_ih =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u} n✝} (x : α a✝), (subtypeVal α.repeatEq ⊚ diagSub) a✝ x = prod.diag a✝ x
α : TypeVec.{u} (n✝ + 1)
x : α a✝.fs
⊢ (subtypeVal α.repeatEq ⊚ diagSub) a✝.fs x = prod.diag a✝.fs x

Tactic:
| fs _ i_ih =>

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n✝¹ n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec.{u} n✝} (a : (α ⊗ β) a✝), (id ⊗' id) a✝ a = id a✝ a
α✝ β✝ : TypeVec.{u} (n✝ + 1)
a : (α✝ ⊗ β✝) a✝.fs
⊢ (id ⊗' id) a✝.fs a = id a✝.fs a

Tactic:
| fs _ i_ih =>

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ g.toFun i = 0 }
i : ι
h : i ∉ ↑fs + ↑gs
⊢ Icc (f i) (g i) = 0

Tactic:
by
        have hf : f i = 0 := (fs.prop i).resolve_left
            (Multiset.notMem_mono (Multiset.Le.subset <| Multiset.le_add_right _ _) h)
        have hg : g i = 0 := (gs.prop i).resolve_left
            (Multiset.notMem_mono (Multiset.Le.subset <| Multiset.le_add_left _ _) h)
        simp_rw [hf, hg]
        exact Icc_self _

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
a b : α
ab : b ∈ pure a
c : α
ac : c ∈ pure a
⊢ b = c

Tactic:
by
    rw [mem_pure] at ab ac
    rwa [← ac] at ab

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
⊢ take m h (update v (castLE h i) x) = update (take m h v) i x

Tactic:
ext j
  by_cases h' : j = i
  · rw [h']
    simp only [take, update_self]
  · have : castLE h j ≠ castLE h i := by simp [h']
    simp only [take, update_of_ne h', update_of_ne this]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ a' ≠ ⟨a, b⟩.fst

Tactic:
exact h.symm

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ s₄ : AList β
p₁₂ : s₁.entries ~ s₂.entries
p₃₄ : s₃.entries ~ s₄.entries
⊢ (s₁ ∪ s₃).entries ~ (s₂ ∪ s₄).entries

Tactic:
simp [p₁₂.kunion s₃.nodupKeys p₃₄]

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

Goal state before:
pp: α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
l : List ((_ : α) × β)
nd : l.NodupKeys
⊢ (map (Sigma.map f fun x ↦ id) l).NodupKeys

Tactic:
induction l with
  | nil => exact nodupKeys_nil
  | cons hd tl ih =>
    simp only [map_cons, nodupKeys_cons] at nd ⊢
    exact ⟨mt (fun h => by
      simp only [keys, map_map] at h ⊢
      obtain ⟨x, hm, he⟩ := mem_map.mp h
      exact mem_map.mpr ⟨x, hm, hf he⟩) nd.1, ih nd.2⟩

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

Tactic:
subst h
      simp only [lookupAll_cons_eq, List.map]
      exact (lookupAll_sublist a l).cons_cons _

Goal state after: