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

Goal state before:
pp: case cons
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : codeSupp (f.cons fs) k ⊆ S
⊢ codeSupp f (Cont'.cons₁ fs k) ⊆ S

Tactic:
codeSupp_cons

Goal state after:
case cons
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : trStmts₁ (trNormal (f.cons fs) k) ∪ codeSupp f (Cont'.cons₁ fs k) ⊆ S
⊢ codeSupp f (Cont'.cons₁ fs k) ⊆ S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case comp
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H' : contSupp (Cont'.comp f k) ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S

Tactic:
contSupp_comp

Goal state after:
case comp
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
H' : codeSupp f k ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: X : LightCondSet
tfae_1_iff_2 : LightCondensed.IsDiscrete X ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ (LightCondensed.discrete (Type u)).essImage X
⊢ [LightCondensed.IsDiscrete X, IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X),
      (LightCondensed.discrete (Type u)).essImage X, functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      ∀ (S : LightProfinite), Nonempty (IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE

Tactic:
tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _ LightProfinite.isTerminalPUnit adjunction X

Goal state after:
X : LightCondSet
tfae_1_iff_2 : LightCondensed.IsDiscrete X ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ (LightCondensed.discrete (Type u)).essImage X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
⊢ [LightCondensed.IsDiscrete X, IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X),
      (LightCondensed.discrete (Type u)).essImage X, functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      ∀ (S : LightProfinite), Nonempty (IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ (isoLocallyConstantOfIsColimit X hX).inv = counitApp X

Tactic:
by
  dsimp [isoLocallyConstantOfIsColimit]
  simp only [Category.assoc]
  rw [Iso.inv_comp_eq]
  ext S : 2
  apply colimit.hom_ext
  intro ⟨Y, _, g⟩
  suffices _ ≫ (isoFinYonedaComponents _ _).inv ≫ X.map g =
    (locallyConstantPresheaf _).map g ≫ counitAppApp (Opposite.unop S) X by
      simpa [locallyConstantIsoFinYoneda, isoFinYoneda, counitApp]
  erw [(counitApp.{u, u} X).naturality]
  simp only [← Category.assoc, op_obj, functorToPresheaves_obj_obj]
  congr
  ext f
  apply presheaf_ext.{u, u} (X := X) (Y := X) (f := f)
  intro x
  dsimp [toLightProfinite_obj]
  rw [incl_of_counitAppApp]
  simp only [counitAppAppImage]
  have : Finite (fiber.{u, u} f x) :=
    Finite.of_injective (sigmaIncl.{u, u} f x).1 Subtype.val_injective
  apply injective_of_mono (isoFinYonedaComponents X (fiber.{u, u} f x)).hom
  ext y
  simp only [toLightProfinite_obj, isoFinYonedaComponents_hom, TypeCat.hom_ofHom,
    TypeCat.Fun.coe_mk, ← map_comp_apply, ← op_comp]
  rw [show (LightProfinite.of PUnit.{u + 1}).const y ≫
    IsTerminal.from _ (fiber.{u, u} f x) = 𝟙 _ from rfl]
  simpa [← dsimp% isoFinYonedaComponents_inv_comp X _ (sigmaIncl.{u, u} f x),
    ← isoFinYonedaComponents_hom_apply, -isoFinYonedaComponents_hom] using! x.map_eq_image f y

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

Goal state before:
pp: 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
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P ⊗ S'.toCondensed) ⟶ A
hh : (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ (μIso (free R) P S.toCondensed).inv ≫ g = g' ≫ e
⊢ (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g =
    (μIso (free R) P S'.toCondensed).hom ≫
      (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ (μIso (free R) P S.toCondensed).inv ≫ g

Tactic:
← assoc,

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
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (P ⊗ S'.toCondensed) ⟶ A
hh : (free R).map (P ◁ lightProfiniteToLightCondSet.map π) ≫ (μIso (free R) P S.toCondensed).inv ≫ g = g' ≫ e
⊢ (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g =
    ((μIso (free R) P S'.toCondensed).hom ≫ (free R).map (P ◁ lightProfiniteToLightCondSet.map π)) ≫
      (μIso (free R) P S.toCondensed).inv ≫ g
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: 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
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S'.toCondensed ⊗ P) ⟶ A
hh : (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ (μIso (free R) S.toCondensed P).inv ≫ g = g' ≫ e
⊢ (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ g =
    (μIso (free R) S'.toCondensed P).hom ≫
      (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ (μIso (free R) S.toCondensed P).inv ≫ g

Tactic:
← assoc,

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
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S'.toCondensed ⊗ P) ⟶ A
hh : (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ (μIso (free R) S.toCondensed P).inv ≫ g = g' ≫ e
⊢ (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ g =
    ((μIso (free R) S'.toCondensed P).hom ≫ (free R).map (lightProfiniteToLightCondSet.map π ▷ P)) ≫
      (μIso (free R) S.toCondensed P).inv ≫ g
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
⊢ ∃ h, f ≫ h = g

Tactic:
have h_comm (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)) (h_down :
        f ≫ k = g ≫ lightToProfinite.map (S.proj n)) : f ≫ k =
          g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n) := by
      rw [h_down, ← Functor.map_comp, ← S.proj_comp_transitionMap n]

Goal state after:
S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
⊢ ∃ h, f ≫ h = g
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ X : CondensedSet
S : CompHausᵒᵖ
x : X.obj.obj S
⊢ Continuous fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x

Tactic:
by
        suffices ∀ (i : (T : CompHaus.{u}) × X.obj.obj ⟨T⟩),
          Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩
        rw [← continuous_sigma_iff]
        apply continuous_coinduced_rng

Goal state after:
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
rr : β → β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }) i.fs
⊢ ofRepeat (α.RelLast' rr i.fs (prod.mk i.fs (↑x).1 (↑x).2)) = ((↑x).1 = (↑x).2)

Tactic:
repeatEq_iff_eq

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }) i.fs
⊢ ((↑x).1 = (↑x).2) = ((↑x).1 = (↑x).2)
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
rr : β → β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // α.RelLast rr p_1.1 p_1.2 }) i.fs
⊢ ((↑x).1 = (↑x).2) = ofRepeat (α.RelLast' rr i.fs (prod.mk i.fs (↑x).1 (↑x).2))

Tactic:
repeatEq_iff_eq

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // α.RelLast rr p_1.1 p_1.2 }) i.fs
⊢ ((↑x).1 = (↑x).2) = ((↑x).1 = (↑x).2)
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
h₁ : (approx (⇑f) (Nat.find h₀) a).Dom
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a

Tactic:
rw [dom_iff_mem] at h₁

Goal state after:
case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
h₁ : ∃ y, y ∈ approx (⇑f) (Nat.find h₀) a
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
⊢ toSubtype p ⊚ ofSubtype p = id

Tactic:
by
  ext i x
  induction i <;> simp only [id, toSubtype, comp, ofSubtype] at *
  simp [*]

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

Goal state before:
pp: case pos
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : (π t).2 = none
⊢ ∃ a, coverToFun (fibreIncl π σ) (π_r π σ) a = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩

pp: case neg
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : ¬(π t).2 = none
⊢ ∃ a, coverToFun (fibreIncl π σ) (π_r π σ) a = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩

Tactic:
· exact ⟨Sum.inr ⟨(⟨⟨t, ht⟩, by grind⟩, ⟨⟨t', ht'⟩, by grind⟩), by grind⟩, by grind⟩

Goal state after:
case neg
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : ¬(π t).2 = none
⊢ ∃ a, coverToFun (fibreIncl π σ) (π_r π σ) a = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
f : Filter α
F : f.Realizer
a : Set α
⊢ a ∈ f ↔ ∃ b, F.F.f b ⊆ a

Tactic:
cases F; subst f; rfl

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

Goal state before:
pp: α : Type u_1
f : Filter α
F : f.Realizer
⊢ (∃ x, ¬(F.F.f x).Nonempty) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ⊆ Realizer.bot.F.f b

Tactic:
simp only [Set.not_nonempty_iff_eq_empty]

Goal state after:
α : Type u_1
f : Filter α
F : f.Realizer
⊢ (∃ x, F.F.f x = ∅) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ⊆ Realizer.bot.F.f b
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: case cons
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
⊢ (⨆ i, f a i) + ⨆ i, ∑ a ∈ s, f a i = ⨆ i, f a i + ∑ a ∈ s, f a i

Tactic:
refine iSup_add_iSup fun i j ↦ (hf i j).imp fun k hk ↦ ?_

Goal state after:
case cons
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ f a i + ∑ a ∈ s, f a j ≤ f a k + ∑ a ∈ s, f a k
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u_1
inst✝³ : FinEnum α✝
β : α✝ → Type u_2
inst✝² : (a : α✝) → FinEnum (β a)
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : ¬p
⊢ ∀ (x : (hp : p) → α hp), x ∈ [fun hp' ↦ ⋯.elim]

Tactic:
by simp [funext_iff, hp]

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

Goal state before:
pp: case pos
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
this✝¹ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
this : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p

Tactic:
have hc := Limits.isColimitOfPreserves (free R) hπ'.isColimit

Goal state after:
case pos
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
this✝¹ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
this : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
hα : Nat.card α ≤ 2
⊢ Nat.card (Perm α) ∣ 2

Tactic:
simpa [card_perm] using factorial_dvd_factorial hα

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ b ∈ dlookup a l

Tactic:
obtain ⟨b', h'⟩ := Option.isSome_iff_exists.mp (dlookup_isSome.mpr (mem_keys_of_mem h))

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
b' : β ⟨a, b⟩.fst
h' : dlookup ⟨a, b⟩.fst l = some b'
⊢ b ∈ dlookup a l
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ map Sigma.fst (eraseP (fun s ↦ decide (a = s.fst)) l) = (map Sigma.fst l).erase a

Tactic:
erase_eq_eraseP,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ map Sigma.fst (eraseP (fun s ↦ decide (a = s.fst)) l) = eraseP (fun x ↦ a == x) (map Sigma.fst l)
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a)
hg : g = update f i ((f i).erase x)
hx' : x ∉ g i
⊢ f = update f i (insert x (update f i ((f i).erase x) i))

Tactic:
update_self,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a)
hg : g = update f i ((f i).erase x)
hx' : x ∉ g i
⊢ f = update f i (insert x ((f i).erase x))
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
hr : r i x ((update g i (insert x (g i)) i).erase x)
hg : g = update f i ((f i).erase x)
hx' : x ∉ g i
⊢ f = update f i (insert x (update f i ((f i).erase x) i))

Tactic:
update_self,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
hr : r i x ((update g i (insert x (g i)) i).erase x)
hg : g = update f i ((f i).erase x)
hx' : x ∉ g i
⊢ f = update f i (insert x ((f i).erase x))
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x ((update g i (insert x (g i)) i).erase x)
hg : g = update f i ((f i).erase x)
hx' : x ∉ g i
⊢ f = update f i (insert x (update f i ((f i).erase x) i))

Tactic:
update_self,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x ((update g i (insert x (g i)) i).erase x)
hg : g = update f i ((f i).erase x)
hx' : x ∉ g i
⊢ f = update f i (insert x ((f i).erase x))