mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f : α → β
hd : Option α
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
⊢ (map (Option.map f) (hd :: tl)).reduceOption = map f (hd :: tl).reduceOption

Tactic:
cases hd

Goal state after:
case cons.none
α : Type u_1
β : Type u_2
f : α → β
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
⊢ (map (Option.map f) (none :: tl)).reduceOption = map f (none :: tl).reduceOption

case cons.some
α : Type u_1
β : Type u_2
f : α → β
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
val✝ : α
⊢ (map (Option.map f) (some val✝ :: tl)).reduceOption = map f (some val✝ :: tl).reduceOption
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case cons
α : Type u_1
hd : Option α
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
⊢ (hd :: tl).reduceOption.length = (filter Option.isSome (hd :: tl)).length

Tactic:
cases hd

Goal state after:
case cons.none
α : Type u_1
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
⊢ (none :: tl).reduceOption.length = (filter Option.isSome (none :: tl)).length

case cons.some
α : Type u_1
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
val✝ : α
⊢ (some val✝ :: tl).reduceOption.length = (filter Option.isSome (some val✝ :: tl)).length
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case cons
α : Type u_1
hd : Option α
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
⊢ ((hd :: tl).concat x).reduceOption = (hd :: tl).reduceOption ++ x.toList

Tactic:
cases hd

Goal state after:
case cons.none
α : Type u_1
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
⊢ ((none :: tl).concat x).reduceOption = (none :: tl).reduceOption ++ x.toList

case cons.some
α : Type u_1
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
val✝ : α
⊢ ((some val✝ :: tl).concat x).reduceOption = (some val✝ :: tl).reduceOption ++ x.toList
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ ↑0 = 0

Tactic:
cast_zero

Goal state after:
⊢ 0 = 0
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : l₁.length ≤ l₂.length
e : l₁.length + i = l₂.length + j
⊢ j ≤ i

Tactic:
rwa [← Nat.add_le_add_iff_left, e, Nat.add_le_add_iff_right]

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

Goal state before:
pp: case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ SupportsStmt S (readAux (i + 1) f)

Tactic:
constructor <;> apply IH <;> intro <;> apply hf

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

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

Tactic:
conv => rhs; rw [← addBottom_map L, ListBlank.nth_map]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
x : List α
IH :
  ∀ (t : List α),
    t.length < x.length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
⊢ (∃ S, x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true) → P.star.rmatch x = true

Tactic:
rintro ⟨S, hsum, helem⟩
      rcases x with - | ⟨a, x⟩
      · rfl
      · rw [rmatch, deriv, mul_rmatch_iff]
        rcases S with - | ⟨t', U⟩
        · exact ⟨[], [], by tauto⟩
        · obtain - | ⟨b, t⟩ := t'
          · simp only [forall_eq_or_imp, List.mem_cons] at helem
            simp only [not_true, Ne, false_and] at helem
          simp only [List.flatten_cons, List.cons_append, List.cons_eq_cons] at hsum
          refine ⟨t, U.flatten, hsum.2, ?_, ?_⟩
          · specialize helem (b :: t) (by simp)
            rw [rmatch] at helem
            convert! helem.2
            exact hsum.1
          · grind

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

Goal state before:
pp: case zero
n : ℕ
⊢ false = Nat.testBit 0 n

Tactic:
Nat.zero_testBit

Goal state after:
case zero
n : ℕ
⊢ false = false
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P
inst✝ : HasExplicitPullbacksOfInclusions P
⊢ ∀ {X Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), PreservesLimit (cospan coprod.inl f) (compHausLikeToTop P)

Tactic:
intro X Y Z f
      infer_instance

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.EffectiveEpi

Goal state before:
pp: P : TopCat → Prop
inst✝ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
X Y Z : CompHausLike P
f : X ⟶ Y
π : Z ⟶ Y
hπ : EffectiveEpi π
y : ↑X.toTop
z : ↑Z.toTop
hz : (ConcreteCategory.hom π) z = (ConcreteCategory.hom f) y
⊢ ∃ a, (ConcreteCategory.hom (pullback.fst f π)) a = y

Tactic:
exact ⟨⟨(y, z), hz.symm⟩, rfl⟩

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 Γ Λ σ
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
c₁ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
h₁ : c₁ ∈ eval (TM1.step (tr M)) (TM1.init (trInit k L))
H₁ : c₁.Tape.right₀ ∈ TM1.eval (tr M) (trInit k L)
q✝ : Option Λ
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
h₂ : { l := q✝, var := v✝, stk := S✝ } ∈ eval (TM2.step M) (TM2.init k L)
H₂ : { l := q✝, var := v✝, stk := S✝ }.stk k ∈ TM2.eval M k L
h₃ :
  { l := Option.map normal q✝, var := v✝, Tape := Tape.mk' ∅ (addBottom L') } ∈
    eval (TM1.step (tr M)) (TM1.init (trInit k L))
⊢ ∃ S L',
    addBottom L' = c₁.Tape.right₀ ∧
      (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧
        S k = { l := q✝, var := v✝, stk := S✝ }.stk k

Tactic:
cases Part.mem_unique h₁ h₃

Goal state after:
case refl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
q✝ : Option Λ
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
h₂ : { l := q✝, var := v✝, stk := S✝ } ∈ eval (TM2.step M) (TM2.init k L)
H₂ : { l := q✝, var := v✝, stk := S✝ }.stk k ∈ TM2.eval M k L
h₃ :
  { l := Option.map normal q✝, var := v✝, Tape := Tape.mk' ∅ (addBottom L') } ∈
    eval (TM1.step (tr M)) (TM1.init (trInit k L))
h₁ :
  { l := Option.map normal q✝, var := v✝, Tape := Tape.mk' ∅ (addBottom L') } ∈
    eval (TM1.step (tr M)) (TM1.init (trInit k L))
H₁ :
  { l := Option.map normal q✝, var := v✝, Tape := Tape.mk' ∅ (addBottom L') }.Tape.right₀ ∈ TM1.eval (tr M) (trInit k L)
⊢ ∃ S L'_1,
    addBottom L'_1 = { l := Option.map normal q✝, var := v✝, Tape := Tape.mk' ∅ (addBottom L') }.Tape.right₀ ∧
      (∀ (k : K), ListBlank.map (proj k) L'_1 = ListBlank.mk (List.map some (S k)).reverse) ∧
        S k = { l := q✝, var := v✝, stk := S✝ }.stk k
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Profinite
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj
              { toTop := (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop, is_compact := ⋯, is_hausdorff := ⋯,
                prop := ⋯ }).map
          f ≫
        InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app Y).hom =
      InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app X).hom ≫ F.map f

Tactic:
by
      intro j k f
      ext ⟨g, p⟩
      exact (p f).symm

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

Goal state before:
pp: k : Cont
v : List ℕ
⊢ eval step (stepRet k v) = Cfg.halt <$> k.eval v

Tactic:
induction k generalizing v with
  | halt =>
    simp only [Cont.eval, map_pure]
    exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)
  | cons₁ fs as k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IH, bind_pure_comp]
  | cons₂ ns k IH => rw [Cont.eval, stepRet]; exact IH
  | comp f k IH =>
    rw [Cont.eval, stepRet, code_is_ok]
    simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [IH, bind_pure_comp]
  | fix f k IH =>
    rw [Cont.eval, stepRet]; simp only
    split_ifs; · exact IH
    simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)]
    congr; funext; rw [bind_pure_comp, ← IH]
    exact reaches_eval (ReflTransGen.single rfl)

Goal state after:
Module: Mathlib.Topology.Category.Profinite.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
⊢ [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b].TFAE

Tactic:
tfae_have 3 ↔ 1 := by
    erw [((CompHaus.effectiveEpiFamily_tfae
      (fun a ↦ profiniteToCompHaus.obj (X a)) (fun a ↦ profiniteToCompHaus.map (π a))).out 2 0 :)]
    exact ⟨fun h ↦ profiniteToCompHaus.finite_effectiveEpiFamily_of_map _ _ h,
      fun _ ↦ inferInstance⟩

Goal state after:
α : Type
inst✝ : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_iff_1 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) ↔ EffectiveEpiFamily X π
⊢ [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b].TFAE
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case h_option
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
⊢ ∃ C,
    (∀ (i : Option I), IsClopen (C i)) ∧
      (∀ (i : Option I), Z i ⊆ C i) ∧ (∀ (i : Option I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C

Tactic:
| @h_option I _ IH =>

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
⊢ x = y

Tactic:
rw [← mem_singleton_iff, ← connectedComponent_eq_singleton, connectedComponent_eq_iInter_isClopen,
    mem_iInter]
  rintro ⟨U, hU1, hU2⟩
  exact (Quotient.exact' (h (ofIsClopen hU1))).mpr hU2

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

Goal state before:
pp: ⊢ Preregular LightProfinite

Tactic:
apply CompHausLike.preregular
  intro _ _ f
  exact (effectiveEpi_iff_surjective f).mp

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj
              { toTop := (CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop, is_compact := ⋯,
                is_hausdorff := ⋯, prop := ⋯ }).map
          f ≫
        ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app Y).hom) =
      ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app X).hom) ≫
        F.map f

Tactic:
by
      intro j k f
      ext ⟨g, p⟩
      exact (p f).symm

Goal state after:
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y), hxy⟩)
ha' :
  a ((ConcreteCategory.hom (G.map (pullback.fst π π))) xy) = a ((ConcreteCategory.hom (G.map (pullback.snd π π))) xy)
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
⊢ ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.snd (G.map π) (G.map π))) y

Tactic:
simp only [← PreservesPullback.iso_inv_snd]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y), hxy⟩)
ha' :
  a ((ConcreteCategory.hom (G.map (pullback.fst π π))) xy) = a ((ConcreteCategory.hom (G.map (pullback.snd π π))) xy)
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
⊢ ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom ((PreservesPullback.iso G π π).inv ≫ G.map (pullback.snd π π))) y
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
⊢ Injective ⇑(sigmaIsoHom f)

Tactic:
rintro ⟨⟨_, _, rfl⟩, ⟨_, hx⟩⟩ ⟨⟨_, _, rfl⟩, ⟨_, hy⟩⟩ h
  refine Sigma.subtype_ext ?_ h
  simp only [sigmaIsoHom_apply] at h
  rw [Set.mem_preimage, Set.mem_singleton_iff] at hx hy
  simp [← hx, ← hy, h]

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

Goal state before:
pp: S : LightProfinite
x✝ : ℕᵒᵖ
⊢ S.asLimitConeAux.π.app x✝ =
    (lightToProfiniteFullyFaithful.preimageIso ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).hom ≫
      S.asLimitCone.π.app x✝

Tactic:
← @Iso.inv_comp_eq

Goal state after:
S : LightProfinite
x✝ : ℕᵒᵖ
⊢ (lightToProfiniteFullyFaithful.preimageIso ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).inv ≫
      S.asLimitConeAux.π.app x✝ =
    S.asLimitCone.π.app x✝
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: S : Finset Λ'
c : Code
k : Cont'
H : codeSupp c k ⊆ S
⊢ Supports (codeSupp' c k) S

Tactic:
by
  induction c generalizing k with
  | cons f fs IHf IHfs =>
    have H' := H; simp only [codeSupp_cons, Finset.union_subset_iff] at H'
    refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => ?_
    refine supports_union.2 ⟨IHf H'.2, ?_⟩
    refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun h => ?_
    · simp only [codeSupp, Finset.union_subset_iff, contSupp] at h H ⊢
      exact ⟨h.2.2.1, h.2.2.2, H.2⟩
    refine supports_union.2 ⟨IHfs ?_, ?_⟩
    · rw [codeSupp, contSupp_cons₁] at H'
      exact Finset.union_subset_right (Finset.union_subset_right H'.2)
    exact
      trStmts₁_supports (head_supports <| Finset.union_subset_right H)
        (Finset.union_subset_right h)
  | comp f g IHf IHg =>
    have H' := H; rw [codeSupp_comp] at H'; have H' := Finset.union_subset_right H'
    refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => ?_
    refine supports_union.2 ⟨IHg H', ?_⟩
    refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun _ => ?_
    · simp only [codeSupp', codeSupp, Finset.union_subset_iff] at h H ⊢
      exact ⟨h.2.2, H.2⟩
    exact IHf (Finset.union_subset_right H')
  | case f g IHf IHg =>
    have H' := H; simp only [codeSupp_case, Finset.union_subset_iff] at H'
    refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun _ => ?_
    exact supports_union.2 ⟨IHf H'.2.1, IHg H'.2.2⟩
  | fix f IHf =>
    have H' := H; simp only [codeSupp_fix, Finset.union_subset_iff] at H'
    refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => ?_
    refine supports_union.2 ⟨IHf H'.2, ?_⟩
    refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun _ => ?_
    · simp only [codeSupp', codeSupp, Finset.union_subset_iff, contSupp, trStmts₁,
        Finset.insert_subset_iff] at h H ⊢
      exact ⟨h.1, ⟨H.1.1, h⟩, H.2⟩
    exact supports_singleton.2 (ret_supports <| Finset.union_subset_right H)
  | _ => exact trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) H)

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
f : Except ε α✝
⊢ Except.map (⇑e.symm) (Except.map (⇑e) f) = f

Tactic:
cases f

Goal state after:
case error
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : ε
⊢ Except.map (⇑e.symm) (Except.map (⇑e) (error a✝)) = error a✝

case ok
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : α✝
⊢ Except.map (⇑e.symm) (Except.map (⇑e) (ok a✝)) = ok a✝
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
f : Except ε β✝
⊢ Except.map (⇑e) (Except.map (⇑e.symm) f) = f

Tactic:
cases f

Goal state after:
case error
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : ε
⊢ Except.map (⇑e) (Except.map (⇑e.symm) (error a✝)) = error a✝

case ok
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : β✝
⊢ Except.map (⇑e) (Except.map (⇑e.symm) (ok a✝)) = ok a✝
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
f : Option α✝
⊢ Option.map (⇑e.symm) (Option.map (⇑e) f) = f

Tactic:
cases f

Goal state after:
case none
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
⊢ Option.map (⇑e.symm) (Option.map (⇑e) none) = none

case some
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
val✝ : α✝
⊢ Option.map (⇑e.symm) (Option.map (⇑e) (some val✝)) = some val✝
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
f : Option β✝
⊢ Option.map (⇑e) (Option.map (⇑e.symm) f) = f

Tactic:
cases f

Goal state after:
case none
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
⊢ Option.map (⇑e) (Option.map (⇑e.symm) none) = none

case some
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
val✝ : β✝
⊢ Option.map (⇑e) (Option.map (⇑e.symm) (some val✝)) = some val✝
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ { toFun := approx ⇑f, monotone' := ⋯ } (n✝ + 1) ≤ X

Tactic:
trans f X
    · apply f.monotone i_ih
    · apply hX

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p Fin2.fz
⊢ (toSubtype p ⊚ ofSubtype p) Fin2.fz x = id Fin2.fz x

Tactic:
simp only [id, toSubtype, comp, ofSubtype] at *

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : Subtype_ p a✝), (toSubtype p ⊚ ofSubtype p) a✝ x = id a✝ x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p a✝.fs
⊢ (toSubtype p ⊚ ofSubtype p) a✝.fs x = id a✝.fs x

Tactic:
simp only [id, toSubtype, comp, ofSubtype] at *

Goal state after:
case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : Subtype_ p a✝), toSubtype p a✝ (ofSubtype p a✝ x) = x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p a✝.fs
⊢ toSubtype (dropFun p) a✝ (ofSubtype (dropFun p) a✝ x) = x
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) 1 = (fun i ↦ if i = 0 then a else b) j
hi : ¬i = 0
hj : ¬j = 0
⊢ 1 = j

Tactic:
· rw [eq_one_of_ne_zero j hj]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih : hd.fst ∈ tl.keys → ∃ b l₁ l₂, ¬hd.fst ∈ l₁.keys ∧ tl = l₁ ++ ⟨hd.fst, b⟩ :: l₂ ∧ kerase hd.fst tl = l₁ ++ l₂
h : hd.fst ∈ (hd :: tl).keys
⊢ hd :: tl = [] ++ ⟨hd.fst, hd.snd⟩ :: tl

Tactic:
cases hd

Goal state after:
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
tl : List (Sigma β)
fst✝ : α
snd✝ : β fst✝
ih :
  ⟨fst✝, snd✝⟩.fst ∈ tl.keys →
    ∃ b l₁ l₂,
      ¬⟨fst✝, snd✝⟩.fst ∈ l₁.keys ∧ tl = l₁ ++ ⟨⟨fst✝, snd✝⟩.fst, b⟩ :: l₂ ∧ kerase ⟨fst✝, snd✝⟩.fst tl = l₁ ++ l₂
h : ⟨fst✝, snd✝⟩.fst ∈ (⟨fst✝, snd✝⟩ :: tl).keys
⊢ ⟨fst✝, snd✝⟩ :: tl = [] ++ ⟨⟨fst✝, snd✝⟩.fst, ⟨fst✝, snd✝⟩.snd⟩ :: tl
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
t : Finset β✝
⊢ ∅ = ∅.sup fun f ↦ image f t

Tactic:
sup_empty,

Goal state after:
case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
t : Finset β✝
⊢ ∅ = ⊥