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

Goal state before:
pp: case mp.halt
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
v'' : List ℕ
h₁ : v'' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v'')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v'')
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
cases Part.mem_unique h₂ (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)

Goal state after:
case mp.halt.refl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
⊢ False

Tactic:
have hyU : y ∈ U := by
      refine Set.mem_compl ?_
      rintro ⟨y', hy'⟩
      exact hy y' hy'

Goal state after:
case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
⊢ False
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this✝ : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
⊢ (Z₁ ∪ Z₂) ∩ (Z₁ ∩ Z₂) = ∅

Tactic:
hZ₁₂.inter_eq,

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this✝ : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
⊢ (Z₁ ∪ Z₂) ∩ ∅ = ∅
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 φ
f_cont : Continuous f
⊢ Surjective f → ∃ h, Continuous h ∧ f ∘ h = φ

Tactic:
f_surj

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
f_surj : Surjective f
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
Module: Mathlib.Topology.Category.Stonean.Limits

Goal state before:
pp: X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Set ↑(⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
hU : IsOpen U
h : IsClopen (⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
⊢ IsOpen ((fun a ↦ ↑a) ⁻¹' closure (Subtype.val '' U))

Tactic:
exact isOpen_induced (ExtremallyDisconnected.open_closure _
      (h.2.isOpenEmbedding_subtypeVal.isOpenMap U hU))

Goal state after:
Module: Mathlib.Topology.Category.Stonean.Limits

Goal state before:
pp: X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : ExtremallyDisconnected ↑(⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
e : ↑(⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f)) ≃ₜ
  { p // (ConcreteCategory.hom i) p.1 = (ConcreteCategory.hom f) p.2 } :=
  (TopCat.pullbackHomeoPreimage ⇑(ConcreteCategory.hom i) ⋯ ⇑(ConcreteCategory.hom f) ⋯).symm
⊢ ↑{xy | (ConcreteCategory.hom f) xy.1 = (ConcreteCategory.hom i) xy.2} ≃ₜ
    ↑{xy | (ConcreteCategory.hom i) xy.1 = (ConcreteCategory.hom f) xy.2}

Tactic:
exact TopCat.homeoOfIso
      ((TopCat.pullbackIsoProdSubtype f.hom i.hom).symm ≪≫ pullbackSymmetry _ _ ≪≫
        (TopCat.pullbackIsoProdSubtype i.hom f.hom))

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

Goal state before:
pp: q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
⊢ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) [] c d }
    { l := some q, var := none, stk := elim (trPosNum a.succ ++ [Γ'.cons]) [] c d }

Tactic:
obtain ⟨l₁', l₂', s', e, h⟩ := this []

Goal state after:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
l₁' l₂' : List Γ'
s' : Option Γ'
e : [].reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) [] c d }
    { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
⊢ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) [] c d }
    { l := some q, var := none, stk := elim (trPosNum a.succ ++ [Γ'.cons]) [] c d }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d }
    { l := some q₂, var := none, stk := elim (trPosNum a ++ Γ'.cons :: trList v) [] c d }

Tactic:
obtain ⟨l₁', l₂', s', e, h⟩ := this []

Goal state after:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
l₁' l₂' : List Γ'
s' : Option Γ'
e : [].reverseAux (trPosNum a) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d }
    { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d }
    { l := some q₂, var := none, stk := elim (trPosNum a ++ Γ'.cons :: trList v) [] c d }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case e'_1.e'_7
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
a_ih✝ :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal fs (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
c : Cfg'
h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.cons₁ fs v k))), var := none,
      stk := elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k)) }
    c
⊢ elim ((trList v).reverse.reverseAux []) [] []
      ((trList v).reverse.reverseAux ((some Γ'.consₗ).getD default :: trContStack k)) =
    elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))

Tactic:
simp [List.reverseAux_eq, trContStack]

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
toSetoid✝¹ : Setoid X
isOpen_setOfPred_rel✝¹ : ∀ (x : X), IsOpen[inst✝¹] (ofPred (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOfPred_rel✝ : ∀ (x : X), IsOpen[inst✝¹] (ofPred (toSetoid✝ x))
h :
  (fun x ↦
        match x with
        | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes)
      { toSetoid := toSetoid✝¹, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝¹ } =
    (fun x ↦
        match x with
        | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes)
      { toSetoid := toSetoid✝, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝ }
⊢ toSetoid✝¹ = toSetoid✝

Tactic:
rw [Setoid.classes_inj]

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
toSetoid✝¹ : Setoid X
isOpen_setOfPred_rel✝¹ : ∀ (x : X), IsOpen[inst✝¹] (ofPred (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOfPred_rel✝ : ∀ (x : X), IsOpen[inst✝¹] (ofPred (toSetoid✝ x))
h :
  (fun x ↦
        match x with
        | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes)
      { toSetoid := toSetoid✝¹, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝¹ } =
    (fun x ↦
        match x with
        | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes)
      { toSetoid := toSetoid✝, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝ }
⊢ toSetoid✝¹.classes = toSetoid✝.classes
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case insert
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))
a : J
E : Finset J
_ha : a ∉ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S → (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ E, P e ∈ S) → ⋂ e ∈ E, P e ∈ S
hh2 : J → Set ↑(F.obj j)
hh3 : Set.univ ∈ S
hh4 : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
hh5 : ∀ e ∈ insert a E, hh2 e ∈ S
⊢ ⋂ e ∈ insert a E, hh2 e ∈ S

Tactic:
rw [Finset.set_biInter_insert]

Goal state after:
case insert
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))
a : J
E : Finset J
_ha : a ∉ E
hh1 :
  ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S → (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ E, P e ∈ S) → ⋂ e ∈ E, P e ∈ S
hh2 : J → Set ↑(F.obj j)
hh3 : Set.univ ∈ S
hh4 : ∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S
hh5 : ∀ e ∈ insert a E, hh2 e ∈ S
⊢ hh2 a ∩ ⋂ x ∈ E, hh2 x ∈ S
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: case mp
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
⊢ False

Tactic:
have hyU : y ∈ U := by
      refine Set.mem_compl ?_
      rintro ⟨y', hy'⟩
      exact hy y' hy'

Goal state after:
case mp
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
⊢ False
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: case refine_2
S : LightDiagram
⊢ (n : ℕ) × LocallyConstant (↑((S.diagram ⋙ toProfinite).obj (op n)).toTop) (Fin 2) →
    LocallyConstant (↑S.cone.pt.toTop) (Fin 2)

pp: case refine_3
S : LightDiagram
⊢ Function.Surjective ?refine_2

Tactic:
· exact fun a ↦ a.snd.comap (S.cone.π.app ⟨a.fst⟩).hom.hom

Goal state after:
case refine_3
S : LightDiagram
⊢ Function.Surjective fun a ↦ LocallyConstant.comap (TopCat.Hom.hom (S.cone.π.app (op a.fst)).hom) a.snd
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: X✝ Y✝ : LightDiagram
f : X✝ ⟶ Y✝
⊢ InducedCategory.homMk (InducedCategory.homMk f.hom.hom) ≫
      lightDiagramToProfinite.preimage (𝟙 (of ↑Y✝.cone.pt.toTop).toLightDiagram.toProfinite) =
    lightDiagramToProfinite.preimage (𝟙 (of ↑X✝.cone.pt.toTop).toLightDiagram.toProfinite) ≫ f

Tactic:
apply lightDiagramToProfinite.map_injective

Goal state after:
X✝ Y✝ : LightDiagram
f : X✝ ⟶ Y✝
⊢ lightDiagramToProfinite.map
      (InducedCategory.homMk (InducedCategory.homMk f.hom.hom) ≫
        lightDiagramToProfinite.preimage (𝟙 (of ↑Y✝.cone.pt.toTop).toLightDiagram.toProfinite)) =
    lightDiagramToProfinite.map
      (lightDiagramToProfinite.preimage (𝟙 (of ↑X✝.cone.pt.toTop).toLightDiagram.toProfinite) ≫ f)
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ traverse (Comp.mk ∘ map x✝² ∘ x✝¹) x✝ = Comp.mk (traverse x✝² <$> traverse x✝¹ x✝)

Tactic:
rw [h₂, Equiv.comp_traverse, h₂]

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Comp.mk (Equiv.traverse eqv x✝² <$> Equiv.traverse eqv x✝¹ x✝) = Comp.mk (Equiv.traverse eqv x✝² <$> traverse x✝¹ x✝)
Module: Mathlib.Data.Fin.FlagRange

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun x1 x2 ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
⊢ x ∈ range f

Tactic:
mem_range

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun x1 x2 ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
⊢ ∃ y, f y = x
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case neg
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
hi : ¬i = 0
⊢ ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
        ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e))
      i =
    e i

Tactic:
· simp [Fin.eq_one_of_ne_zero i hi]

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

Goal state before:
pp: n : ℕ
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
i : Fin (List.take m (List.ofFn v)).length
⊢ (List.take m (List.ofFn v)).get i = (take m h v ∘ Fin.cast ⋯) i

Tactic:
simp [castLE]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
⊢ True

Tactic:
induction l

Goal state after:
case H0
α : Type u
β : α → Type v
inst✝ : DecidableEq α
⊢ True

case IH
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a✝² : α
b✝ : β a✝²
l✝ : AList β
a✝¹ : ¬a✝² ∈ l✝
a✝ : True
⊢ True
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
l : List ((a : α) × β a)
⊢ (map (Sigma.map id f) l).keys = l.keys

Tactic:
induction l

Goal state after:
case nil
α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
⊢ (map (Sigma.map id f) []).keys = [].keys

case cons
α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : (map (Sigma.map id f) tail✝).keys = tail✝.keys
⊢ (map (Sigma.map id f) (head✝ :: tail✝)).keys = (head✝ :: tail✝).keys
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: case cons
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
a✝ : l₁ ~ l₂
h : ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₂
⊢ ofList <$> Traversable.traverse f (x :: l₁) = ofList <$> Traversable.traverse f (x :: l₂)

Tactic:
have :
      Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₁ =
        Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₂ := by
      rw [h]

Goal state after:
case cons
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
a✝ : l₁ ~ l₂
h : ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₂
this : cons <$> f x <*> ofList <$> Traversable.traverse f l₁ = cons <$> f x <*> ofList <$> Traversable.traverse f l₂
⊢ ofList <$> Traversable.traverse f (x :: l₁) = ofList <$> Traversable.traverse f (x :: l₂)
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
⊢ ⟦s₁⟧.Disjoint ⟦s₂⟧ → ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₂⟧ ∪ ⟦s₁⟧

Tactic:
by
    intro h
    simp only [AList.toFinmap_eq, union_toFinmap, AList.union_comm_of_disjoint h]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h : ¬a ∈ (head✝ :: l₁).keys
⊢ kerase a (head✝ :: l₁ ++ l₂) = head✝ :: l₁ ++ kerase a l₂

Tactic:
by
    simp only [keys_cons, mem_cons, not_or] at h
    simp [h.1, kerase_append_right h.2]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
⊢ a ∈ (filter (fun x ↦ decide (x.snd ≠ 0)) l.entries).keys.toFinset ↔ (lookup a l).getD 0 ≠ 0

Tactic:
simp_rw [mem_toFinset, List.mem_keys, List.mem_filter, ← mem_lookup_iff]
      cases lookup a l <;> simp

Goal state after:
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ (-f).neLocus g = f.neLocus (-g)

Tactic:
by rw [← neLocus_neg_neg, neg_neg]

Goal state after:
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b

Tactic:
rw [← abs_le_iff_mul_self_le, abs_eq_natAbs, abs_eq_natAbs]

Goal state after:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ ↑a.natAbs ≤ ↑b.natAbs
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑r * ↑(b / r) + ↑(b % r) - ↑(v % r)) / ↑r⌉

Tactic:
← add_sub,

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑r * ↑(b / r) + (↑(b % r) - ↑(v % r))) / ↑r⌉
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
l : List α
⊢ foldl (flip cons) [] l = l.reverse

Tactic:
induction l

Goal state after:
case nil
α : Type u_1
l : List α
⊢ foldl (flip cons) [] [] = [].reverse

case cons
α : Type u_1
l : List α
head✝ : α
tail✝ : List α
tail_ih✝ : foldl (flip cons) [] tail✝ = tail✝.reverse
⊢ foldl (flip cons) [] (head✝ :: tail✝) = (head✝ :: tail✝).reverse
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
l : List α
a : α
f : α → α → α
inst✝ : Std.Associative f
ha : ∀ (x : α), f a x = f x a
⊢ foldl f a l = foldr f a l

Tactic:
induction l

Goal state after:
case nil
α : Type u_1
l : List α
a : α
f : α → α → α
inst✝ : Std.Associative f
ha : ∀ (x : α), f a x = f x a
⊢ foldl f a [] = foldr f a []

case cons
α : Type u_1
l : List α
a : α
f : α → α → α
inst✝ : Std.Associative f
ha : ∀ (x : α), f a x = f x a
head✝ : α
tail✝ : List α
tail_ih✝ : foldl f a tail✝ = foldr f a tail✝
⊢ foldl f a (head✝ :: tail✝) = foldr f a (head✝ :: tail✝)