mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous[inst✝¹, instTopologicalSpaceProd] fun y ↦ (a.1, y)
V : Set Y := {y | (a.1, y) ∈ W}
hV : IsCompact V
U : Set X := {x | MapsTo (Prod.mk x) V ↑W}
hUV : U ×ˢ V ⊆ ↑W
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Tactic:
exact ⟨⟨U, (ContinuousMap.isClopen_setOfPred_mapsTo hV W.2).preimage
    (ContinuousMap.id (X × Y)).curry.2⟩, by simp [U, V, MapsTo], ⟨V, W.2.preimage hp⟩, h, hUV⟩

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

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
⊢ ∀ (i j : J) (f : i ⟶ j),
    ∀ V ∈ {W | IsClopen W}, ⇑(ConcreteCategory.hom ((F ⋙ toTopCat).map f)) ⁻¹' V ∈ {W | IsClopen W}

Tactic:
rintro i j f V (hV : IsClopen _)
    refine ⟨hV.1.preimage ?_, hV.2.preimage ?_⟩ <;> fun_prop

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

Goal state before:
pp: case nil
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
s : Option Γ'
⊢ if [].headI = 0 then natEnd ((trList []).head?.getD default) = true ∧ (trList []).tail = trList [].tail
  else
    natEnd ((trList []).head?.getD default) = false ∧
      (trList []).tail = (trNat [].headI).tail ++ Γ'.cons :: trList [].tail

pp: case cons
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
s : Option Γ'
n : ℕ
tail✝ : List ℕ
⊢ if (n :: tail✝).headI = 0 then
    natEnd ((trList (n :: tail✝)).head?.getD default) = true ∧ (trList (n :: tail✝)).tail = trList (n :: tail✝).tail
  else
    natEnd ((trList (n :: tail✝)).head?.getD default) = false ∧
      (trList (n :: tail✝)).tail = (trNat (n :: tail✝).headI).tail ++ Γ'.cons :: trList (n :: tail✝).tail

Tactic:
· exact ⟨rfl, rfl⟩

Goal state after:
case cons
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
s : Option Γ'
n : ℕ
tail✝ : List ℕ
⊢ if (n :: tail✝).headI = 0 then
    natEnd ((trList (n :: tail✝)).head?.getD default) = true ∧ (trList (n :: tail✝)).tail = trList (n :: tail✝).tail
  else
    natEnd ((trList (n :: tail✝)).head?.getD default) = false ∧
      (trList (n :: tail✝)).tail = (trNat (n :: tail✝).headI).tail ++ Γ'.cons :: trList (n :: tail✝).tail
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: X : LightCondSet
h : (S : LightProfinite) → IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ LocallyConstant.functor.essImage X

Tactic:
let i : X.obj ≅ (LightCondSet.LocallyConstant.functor.obj _).obj :=
    LightCondensed.isoLocallyConstantOfIsColimit _ h

Goal state after:
X : LightCondSet
h : (S : LightProfinite) → IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone))
i : X.obj ≅ (LocallyConstant.functor.obj (X.obj.obj (toLightProfinite.op.obj (Opposite.op (of PUnit.{u + 1}))))).obj :=
  LightCondensed.isoLocallyConstantOfIsColimit X.obj h
⊢ LocallyConstant.functor.essImage X
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_6_to_1 :
  (∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    LightCondensed.IsDiscrete M
⊢ [LightCondensed.IsDiscrete M, IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (LightCondensed.discrete (ModuleCat R)).essImage M, (functor R).essImage M,
      IsIso ((LocallyConstant.adjunction R).counit.app M),
      ∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE

Tactic:
tfae_have 1 → 6 := by
    intro h S
    rw [isDiscrete_iff_isDiscrete_forget, ((LightCondSet.isDiscrete_tfae _).out 0 5 :)] at h
    let : ReflectsFilteredColimitsOfSize.{0, 0} (forget (ModuleCat R)) :=
      reflectsFilteredColimitsOfSize_shrink.{0, u, 0, u} _
    exact ⟨isColimitOfReflects (forget (ModuleCat R)) (h S).some⟩

Goal state after:
R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_6_to_1 :
  (∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    LightCondensed.IsDiscrete M
tfae_1_to_6 :
  LightCondensed.IsDiscrete M →
    ∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))
⊢ [LightCondensed.IsDiscrete M, IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (LightCondensed.discrete (ModuleCat R)).essImage M, (functor R).essImage M,
      IsIso ((LocallyConstant.adjunction R).counit.app M),
      ∀ (S : LightProfinite), Nonempty (IsColimit (M.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE
Module: Mathlib.Topology.Category.Sequential

Goal state before:
pp: X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : SequentialSpace X✝
X Y : Sequential
f : ↑X.toTop ≃ₜ ↑Y.toTop
⊢ InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f, continuous_toFun := ⋯ }) ≫
      InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ }) =
    𝟙 X

Tactic:
ext x
    exact f.symm_apply_apply x

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
s : Cocone ((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X)
n : ℕᵒᵖ
f : LocallyConstant (↑(toLightProfinite.obj (F.obj n)).toTop) X
⊢ (ConcreteCategory.hom ((isColimitLocallyConstantPresheaf c X hc).desc s))
      (LocallyConstant.comap (TopCat.Hom.hom (c.π.app n).hom) f) =
    (ConcreteCategory.hom (s.ι.app (Opposite.op n))) f

Tactic:
change ((((locallyConstantPresheaf X).mapCocone c.op).ι.app ⟨n⟩) ≫
    (isColimitLocallyConstantPresheaf c X hc).desc s) _ = _
  rw [(isColimitLocallyConstantPresheaf c X hc).fac]

Goal state after:
Module: Mathlib.Topology.Category.CompactlyGenerated

Goal state before:
pp: X✝ : Type w
inst✝¹ : TopologicalSpace X✝
inst✝ : UCompactlyGeneratedSpace X✝
X Y : CompactlyGenerated
f : ↑X.toTop ≃ₜ ↑Y.toTop
⊢ ofHom { toFun := ⇑f, continuous_toFun := ⋯ } ≫ ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ } = 𝟙 X

Tactic:
ext x
    exact f.symm_apply_apply x

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondSet
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (P ⊗ S.toCondensed) ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj P ⊗ (free R).obj S.toCondensed ⟶ B
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e

Tactic:
specialize h e S ((μIso (free R) _ _).inv ≫ g)

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj P ⊗ (free R).obj S.toCondensed ⟶ B
h :
  ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ (μIso (free R) P S.toCondensed).inv ≫ g = g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: case refine_3
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
h_glue : ∀ (i j : S), ∀ x ∈ C i, x ∈ C j → i = j
x : X
⊢ (liftCover C (fun i x ↦ i) h_glue C_cover_univ ∘ f) x = g x

Tactic:
simp [liftCover_of_mem <| Z_subset_C (g x) (by simpa [mem_image] using ⟨x, rfl, rfl⟩)]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondSet
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (S.toCondensed ⊗ P) ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj S.toCondensed ⊗ (free R).obj P ⟶ B
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ g = g' ≫ e

Tactic:
specialize h e S ((μIso (free R) _ _).inv ≫ g)

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj S.toCondensed ⊗ (free R).obj P ⟶ B
h :
  ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ (μIso (free R) S.toCondensed P).inv ≫ g = g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ g = g' ≫ e
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // ofRepeat (α.PredLast' pp i p_1) }) i.fs
⊢ ofRepeat (α.PredLast' pp i.fs ↑x) = α.PredLast pp ↑x

Tactic:
by grind [PredLast]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

Tactic:
simp only [Part.fix_def f h₀]

Goal state after:
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a ↔ ∃ i, b ∈ approx (⇑f) i a
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ ?m.39

pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ ?m.39 ≤ approx (⇑f) i.succ x

pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part (β x)

Tactic:
· apply hx

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ approx (⇑f) i x ≤ approx (⇑f) i.succ x
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
h : ∞ ∈ {↑i}
⊢ IsCompact (OnePoint.some ⁻¹' {↑i})ᶜ

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : f.Realizer
E : F.σ ≃ τ
x✝¹ : Set α
x✝ : x✝¹ ∈ (CFilter.ofEquiv E F.F).toFilter.sets
s : τ
h : (CFilter.ofEquiv E F.F).f s ⊆ x✝¹
⊢ F.F.f (E.symm s) ⊆ x✝¹

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
a : α
s✝ : Set α
x✝ : ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s✝
s : F.σ
h : a ∈ F.F.f s ∧ F.F.f s ⊆ s✝
⊢ a ∈ (Ctop.ofEquiv E F.F).f (E s) ∧ (Ctop.ofEquiv E F.F).f (E s) ⊆ s✝

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
a : α
s : Set α
x✝ : ∃ b, a ∈ (Ctop.ofEquiv E F.F).f b ∧ (Ctop.ofEquiv E F.F).f b ⊆ s
t : τ
h : a ∈ (Ctop.ofEquiv E F.F).f t ∧ (Ctop.ofEquiv E F.F).f t ⊆ s
⊢ a ∈ F.F.f (E.symm t) ∧ F.F.f (E.symm t) ⊆ s

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β✝ : α → Type v
β : Type ?u.23
inst✝¹ : FinEnum α
inst✝ : FinEnum β
x : α × β
⊢ x ∈ toList α ×ˢ toList β

Tactic:
by cases x; simp

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ s.max' hs < t.min' ht

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
ht : ¬t.Nonempty
p : α
hp : s.max' hs < p
⊢ (∀ x ∈ s, x < p) ∧ ∀ y ∈ t, p < y

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : t.Nonempty
p : α
hp : p < t.min' ht
⊢ (∀ x ∈ s, x < p) ∧ ∀ y ∈ t, p < y

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : ¬t.Nonempty
p : α
⊢ (∀ x ∈ s, x < p) ∧ ∀ y ∈ t, p < y

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: α : Type u_1
x : Multiset α
⊢ traverse pure x = pure x

Tactic:
induction x using Quotient.inductionOn

Goal state after:
case h
α : Type u_1
a✝ : List α
⊢ traverse pure ⟦a✝⟧ = pure ⟦a✝⟧
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) x = Comp.mk (traverse h <$> traverse g x)

Tactic:
induction x using Quotient.inductionOn

Goal state after:
case h
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
a✝ : List α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) ⟦a✝⟧ = Comp.mk (traverse h <$> traverse g ⟦a✝⟧)
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case h_fst
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
x : ↑(S' ⊗ ℕ∪{∞}).toTop
⊢ (ConcreteCategory.hom
        ((ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ } ≫ π') ≫ fst S' ℕ∪{∞}))
      x =
    (ConcreteCategory.hom (𝟙 (S' ⊗ ℕ∪{∞}) ≫ fst S' ℕ∪{∞})) x

pp: case h_snd
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
x : ↑(S' ⊗ ℕ∪{∞}).toTop
⊢ (ConcreteCategory.hom
        ((ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ } ≫ π') ≫ snd S' ℕ∪{∞}))
      x =
    (ConcreteCategory.hom (𝟙 (S' ⊗ ℕ∪{∞}) ≫ snd S' ℕ∪{∞})) x

Tactic:
all_goals exact h.elim x

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
⊢ Functor.map h <$> traverse g x = traverse (Functor.map h ∘ g) x

Tactic:
induction x using Quotient.inductionOn

Goal state after:
case h
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
a✝ : List α
⊢ Functor.map h <$> traverse g ⟦a✝⟧ = traverse (Functor.map h ∘ g) ⟦a✝⟧
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
⊢ traverse h (map g x) = traverse (h ∘ g) x

Tactic:
induction x using Quotient.inductionOn

Goal state after:
case h
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
a✝ : List α
⊢ traverse h (map g ⟦a✝⟧) = traverse (h ∘ g) ⟦a✝⟧
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
⊢ (fun {α} ↦ eta.app α) (traverse f x) = traverse ((fun {α} ↦ eta.app α) ∘ f) x

Tactic:
induction x using Quotient.inductionOn

Goal state after:
case h
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
a✝ : List α
⊢ (fun {α} ↦ eta.app α) (traverse f ⟦a✝⟧) = traverse ((fun {α} ↦ eta.app α) ∘ f) ⟦a✝⟧
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ kextract a (⟨a', b⟩ :: l) = (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))

Tactic:
by
    simp only [kextract]; split_ifs with h
    · subst a'
      simp [kerase]
    · simp [Ne.symm h, kextract_eq_dlookup_kerase a l, kerase]

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✝ : Zero N
f : α →₀ N
⊢ f.neLocus 0 = f.support

Tactic:
ext
  rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.assocRight.take * (y t.assocRight.drop.take * z t.assocRight.drop.drop) =
    cast ⋯ (fun t ↦ x t.take * (y t.drop.take * z t.drop.drop)) t

Tactic:
cast_type

Goal state after:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.assocRight.take * (y t.assocRight.drop.take * z t.assocRight.drop.drop) =
    (fun t ↦ x (cast ⋯ t).take * (y (cast ⋯ t).drop.take * z (cast ⋯ t).drop.drop)) t

case eq
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃
Module: Mathlib.Data.Int.NatPrime

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ k.natAbs

Tactic:
apply @Nat.Prime.dvd_of_dvd_pow _ _ 2 hp

Goal state after:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ k.natAbs ^ 2
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a : α
⊢ (fun x ↦ a ^^^ x) = id ↔ a = 0

Tactic:
xor_left_eq_id_iff

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a : α
⊢ a = 0 ↔ a = 0
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m x✝ : ℕ
⊢ Nat.shiftLeft' false m x✝ = m * 2 ^ x✝

Tactic:
by simp [Nat.shiftLeft_eq]

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

Goal state before:
pp: n : ℕ
⊢ Nat.shiftLeft' false 1 n = 2 ^ n

Tactic:
by simp [Nat.shiftLeft_eq]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ dropWhile (fun x ↦ !p x) l ≠ []

Tactic:
by simpa using h

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ rtakeWhile p (l ++ [x]) = rtakeWhile p l ++ [x]

Tactic:
rw [rtakeWhile_concat, if_pos h]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ dropWhile p l ≠ []

Tactic:
by simpa using h

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

Goal state before:
pp: case refine_1
α : Type u_1
L : List (List α)
f : List α
h : f ∈ L.sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L

Tactic:
induction L generalizing f
    · cases mem_singleton.1 h
      exact Forall₂.nil
    simp only [sections, mem_flatMap, mem_map] at h
    rcases h with ⟨_, _, _, _, rfl⟩
    simp only [*, forall₂_cons, true_and]

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

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l : List α
h : m ∈ splitBy r l
x✝ : m = []
⊢ False

Tactic:
by simp_all

Goal state after: