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

Goal state before:
pp: case pos.refine_1
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
⊢ Directed (fun x1 x2 ↦ x1 ⊇ x2) fun i ↦ ↑i ∩ X ⁻¹' {a}

Tactic:
replace C_chain : IsChain (· ⊇ ·) C := C_chain.symm

Goal state after:
case pos.refine_1
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
hC : Nonempty ↑C
a : A
C_chain : IsChain (fun x1 x2 ↦ x1 ⊇ x2) C
⊢ Directed (fun x1 x2 ↦ x1 ⊇ x2) fun i ↦ ↑i ∩ X ⁻¹' {a}
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X Y : Stonean
f : X ⟶ Y
h : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
⊢ False

Tactic:
classical
  let g : Y ⟶ mkFinite (ULift (Fin 2)) := ConcreteCategory.ofHom
    ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩
  let h : Y ⟶ mkFinite (ULift (Fin 2)) := ConcreteCategory.ofHom ⟨fun _ => ⟨1⟩, continuous_const⟩
  have H : h = g := by
    rw [← cancel_epi f]
    ext x
    apply ULift.ext -- why is `ext` not doing this automatically?
    change 1 = ite _ _ _ -- why is `dsimp` not getting me here?
    rw [if_neg]
    refine mt (hVU ·) ?_ -- what would be an idiomatic tactic for this step?
    simpa only [U, Set.mem_compl_iff, Set.mem_range, not_exists, not_forall, not_not]
      using! exists_apply_eq_apply f x
  apply_fun fun e => (e y).down at H
  change 1 = ite _ _ _ at H -- why is `dsimp at H` not getting me here?
  rw [if_pos hyV] at H
  exact one_ne_zero H

Goal state after:
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
inst✝ : CompactSpace X
W : Clopens (X × Y)
U : X × Y → Clopens X
hxU : ∀ x ∈ W, x.1 ∈ U x
V : X × Y → Clopens Y
hxV : ∀ x ∈ W, x.2 ∈ V x
hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, ↑(U x) ×ˢ ↑(V x)
⊢ ∃ I, W = I.sup fun i ↦ i.1 ×ˢ i.2

Tactic:
classical
  use I.image fun x ↦ (U x, V x)
  rw [Finset.sup_image]
  refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)
  · rcases Set.mem_iUnion₂.1 (hWI hx) with ⟨i, hi, hxi⟩
    exact SetLike.le_def.1 (Finset.le_sup hi) hxi
  · exact hUV _ <| hIW _ hx

Goal state after:
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
inst✝² : CompactSpace X
inst✝¹ : Finite (Clopens X)
inst✝ : Finite (Clopens Y)
⊢ Finite (Clopens (X × Y))

Tactic:
cases nonempty_fintype (Clopens X)

Goal state after:
case intro
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : CompactSpace Y
inst✝² : CompactSpace X
inst✝¹ : Finite (Clopens X)
inst✝ : Finite (Clopens Y)
val✝ : Fintype (Clopens X)
⊢ Finite (Clopens (X × Y))
Module: Mathlib.Topology.Category.LightProfinite.EffectiveEpi

Goal state before:
pp: ⊢ Preregular LightProfinite

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

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

Goal state before:
pp: case neg
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₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
⊢ ∃ b₂,
    TrCfg (stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.fix f k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.fix f k)) }
        b₂

Tactic:
obtain ⟨s', h₁, h₂⟩ := trNormal_respects f (Cont.fix f k) v.tail (some Γ'.cons)
      refine ⟨_, h₁, TransGen.head rfl <| TransGen.trans ?_ h₂⟩
      rw [trCont, tr]; simp only [pop', TM2.stepAux, elim_main, this.1]
      convert! clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _) using 2
      · simp
        convert! rfl
      · exact fun x h => trNat_natEnd _ _ (List.tail_subset _ h)
      · exact ⟨rfl, this.2⟩

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
let S := f.discreteQuotient

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
h : ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))
⊢ Condensed.IsDiscrete ((Condensed.forget R).obj M)

Tactic:
((CondensedSet.isDiscrete_tfae _).out 0 6 :)

Goal state after:
R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
h : ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))
⊢ ∀ (S : Profinite),
    Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ ((Condensed.forget R).obj M).obj).mapCocone S.asLimitCone.op))
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
tfae_7_to_1 :
  (∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))) →
    Condensed.IsDiscrete M
h : Condensed.IsDiscrete ((Condensed.forget R).obj M)
S : Profinite
⊢ Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))

Tactic:
((CondensedSet.isDiscrete_tfae _).out 0 6 :)

Goal state after:
R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
tfae_7_to_1 :
  (∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))) →
    Condensed.IsDiscrete M
h :
  ∀ (S : Profinite),
    Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ ((Condensed.forget R).obj M).obj).mapCocone S.asLimitCone.op))
S : Profinite
⊢ Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
⊢ ∀ (X : Type (max u w)),
    (functor P hs).map ((unit P hs).app X) ≫ (counit P hs).app ((functor P hs).obj X) = 𝟙 ((functor P hs).obj X)

Tactic:
intro X

Goal state after:
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
⊢ (functor P hs).map ((unit P hs).app X) ≫ (counit P hs).app ((functor P hs).obj X) = 𝟙 ((functor P hs).obj X)
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
⊢ ∀ (X : Sequential), IsIso (sequentialAdjunction.counit.app X)

Tactic:
intro X

Goal state after:
X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : Sequential
⊢ IsIso (sequentialAdjunction.counit.app X)
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_1
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ ∀ (x : ((locallyConstantPresheaf X).mapCocone c.op).pt),
    ∃ i xi, x = (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi

Tactic:
intro (f : LocallyConstant c.pt X)
    obtain ⟨j, h⟩ := Profinite.exists_locallyConstant.{_, 0} (lightToProfinite.mapCone c)
      (isLimitOfPreserves lightToProfinite hc) f
    exact ⟨⟨j⟩, h⟩

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
⊢ ∃ T π g, Epi π ∧ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p = g ≫ f

Tactic:
have : Epi ((LightCondensed.forget _).map f) := inferInstance
  rw [LightCondSet.epi_iff_locallySurjective_on_lightProfinite] at this
  obtain ⟨T, π, hπ, x, hx⟩ := this S <| (coherentTopology LightProfinite).yonedaEquiv <|
    (LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y p
  refine ⟨T, π, ((LightCondensed.freeForgetAdjunction R).homEquiv T.toCondensed X).symm
    ((coherentTopology LightProfinite).yonedaEquiv.symm x),
    (LightProfinite.epi_iff_surjective π).mpr hπ, ?_⟩
  rw [Functor.comp_map, ← Adjunction.homEquiv_naturality_left_square_iff
    (LightCondensed.freeForgetAdjunction R), Sheaf.hom_ext_iff, Equiv.apply_symm_apply,
    GrothendieckTopology.yonedaEquiv_symm_naturality_right, hx,
    GrothendieckTopology.map_yonedaEquiv', ← GrothendieckTopology.yonedaEquiv_symm_naturality_right]
  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)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (μIso (free R) _ _).hom ≫ g', ?_⟩
    rw [assoc, ← hh, ← assoc, ← assoc]
    -- Generated by `simp? [← μ_natural_left]`
    -- Leaving it unsqueezed is too slow.
    simp only [comp_obj, Functor.comp_map, μIso_hom, ← μ_natural_left, μIso_inv, assoc, μ_δ,
      comp_id]

Goal state after:
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X : CondensedSet
⊢ ∀ (X : CompactlyGenerated), IsIso (compactlyGeneratedAdjunction.counit.app X)

Tactic:
intro X

Goal state after:
X✝ : CondensedSet
X : CompactlyGenerated
⊢ IsIso (compactlyGeneratedAdjunction.counit.app X)
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
xs : List α
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) xs) = xs

Tactic:
induction xs with
  | nil => rfl
  | cons _ _ ih => (conv_rhs => rw [← ih]); rfl

Goal state after:
Module: Mathlib.Control.LawfulFix

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

Tactic:
by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom

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 ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

case neg
α : 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
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
x : β
α : TypeVec.{u_2} 0
⊢ TypeVec.const x α = nilFun

Tactic:
ext i : 1; cases i

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → Lattice (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(uIcc f g) = ∏ i ∈ f.support ∪ g.support, #(uIcc (f i) (g i))

Tactic:
rw [← support_inf_union_support_sup]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → Lattice (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(uIcc f g) = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, #(uIcc (f i) (g i))
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ q.liftOn id p ∈ q

Tactic:
liftOn_ofMem q _ _ a h

Goal state after:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ id a ∈ q
Module: Mathlib.Condensed.Light.Sequence

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

Tactic:
intro X

Goal state after:
R : Type
inst✝ : CommRing R
X : LightCondMod R
⊢ ∀ {B : LightCondMod R} (e : X ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ ℕ∪{∞})) ≫ g = g' ≫ e
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case zero
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
⊢ take (Nat.succ 0) h v 0 = snoc (take 0 ⋯ v) (v ⟨0, h⟩) 0

Tactic:
simp [take, snoc, castLE]

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

Goal state before:
pp: α : Type u_1
f : α → Option α
l : List α
⊢ (lookmap f l).length = l.length

Tactic:
rw [← length_map, lookmap_map_eq _ fun _ => (), length_map]; simp

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s✝ : Finmap β
s : AList β
⊢ (erase a (erase a' ⟦s⟧)).entries = (erase a' (erase a ⟦s⟧)).entries

Tactic:
by simp only [AList.erase_erase, erase_toFinmap]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
this : l'.NodupKeys
⊢ (foldr (fun x ↦ kinsert x.fst x.snd) l' l).NodupKeys

Tactic:
induction l with
  | nil => apply this
  | cons x xs l_ih =>
    cases x
    simp only [foldr_cons, kinsert_def, nodupKeys_cons]
    constructor
    · simp only [keys_kerase]
      apply l_ih.not_mem_erase
    · exact l_ih.kerase _

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

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ image (fun p ↦ p.1 * p.2) (image Subtype.val (m.divisors ×ˢ n.divisors).attach) =
    map { toFun := fun p ↦ (↑p).1 * (↑p).2, inj' := ⋯ } (m.divisors ×ˢ n.divisors).attach

Tactic:
rw [Finset.map_eq_image, Finset.image_image]; rfl

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 : α
⊢ (∃ b, ⟨a, b⟩ ∈ filter (fun x ↦ decide (x.snd ≠ 0)) l.entries) ↔ (lookup a l).getD 0 ≠ 0

Tactic:
List.mem_filter,

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
⊢ (∃ b, ⟨a, b⟩ ∈ l.entries ∧ decide (b ≠ 0) = true) ↔ (lookup a l).getD 0 ≠ 0
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f : ι k →₀ M
i : ι k
⊢ f.embSigma ⟨k, i⟩ = f i

Tactic:
embSigma

Goal state after:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f : ι k →₀ M
i : ι k
⊢ (embDomain (Embedding.sigmaMk k) f) ⟨k, i⟩ = f i
Module: Mathlib.Data.Holor

Goal state before:
pp: case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
hid' : ⟨i, ⋯⟩ ∉ (Finset.range d).attach
⊢ False

Tactic:
exact absurd (Finset.mem_attach _ _) hid'

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
this : CPRankMax (m + n + 1) (x₁ + (x₂ + y))
⊢ CPRankMax (m + 1 + n) (x₁ + x₂ + y)

Tactic:
simpa only [add_comm, add_assoc, add_left_comm] using this

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

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

Tactic:
by
  rw [← abs_eq_iff_mul_self_eq, abs_eq_natAbs, abs_eq_natAbs]
  exact Int.natCast_inj.symm

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

Goal state before:
pp: m n k : ℕ
⊢ ↑m >>> (↑n + ↑k) = ↑(m >>> n >>> k)

Tactic:
← Int.natCast_add,

Goal state after:
m n k : ℕ
⊢ ↑m >>> ↑(n + k) = ↑(m >>> n >>> k)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n k : ℕ
⊢ -[m+1] >>> (↑n + ↑k) = -[m >>> n >>> k+1]

Tactic:
← Int.natCast_add,

Goal state after:
m n k : ℕ
⊢ -[m+1] >>> ↑(n + k) = -[m >>> n >>> k+1]
Module: Mathlib.Data.List.DropRight

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

Tactic:
if_pos h

Goal state after:
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ rdropWhile p l = rdropWhile p l
Module: Mathlib.Data.List.DropRight

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

Tactic:
if_pos h

Goal state after:
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ rtakeWhile p l ++ [x] = rtakeWhile p l ++ [x]
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
h : Ico n m = []
⊢ [].length = 0

Tactic:
List.length

Goal state after:
n m : ℕ
h : Ico n m = []
⊢ 0 = 0
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: α : Type u_1
l : List α
x : α
hx : ¬x ∈ l
⊢ Set.InjOn (fun k ↦ l.insertIdx k x) {n | n ≤ l.length}

Tactic:
intro n hn m hm h

Goal state after:
α : Type u_1
l : List α
x : α
hx : ¬x ∈ l
n : ℕ
hn : n ∈ {n | n ≤ l.length}
m : ℕ
hm : m ∈ {n | n ≤ l.length}
h : (fun k ↦ l.insertIdx k x) n = (fun k ↦ l.insertIdx k x) m
⊢ n = m
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case inr
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n (min m l)

Tactic:
rw [min_eq_right hlm, filter_lt_of_ge hlm]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Trichotomous r
⊢ Function.Injective fun a ↦ (a.length, a)

Tactic:
simp [Function.Injective]

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

Goal state before:
pp: α : Type u_1
q k : ℕ
w : List α
per_q : w.HasPeriod q
per_plus : w.HasPeriod (k + q)
⊢ (drop q w).HasPeriod k

Tactic:
rw [hasPeriod_iff_getElem?] at per_plus per_q ⊢

Goal state after:
α : Type u_1
q k : ℕ
w : List α
per_q : ∀ i < w.length - q, w[i]? = w[i + q]?
per_plus : ∀ i < w.length - (k + q), w[i]? = w[i + (k + q)]?
⊢ ∀ i < (drop q w).length - k, (drop q w)[i]? = (drop q w)[i + k]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
a : α
m : List α
ha : ∀ (x : α), x ∈ l.getLast? → r x a = false
⊢ splitBy r (l ++ a :: m) = splitBy r l ++ splitBy r (a :: m)

Tactic:
apply splitBy_append
  simpa

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
v₁ : n₁ → R
v₂ : n₂ → R
⊢ A₁.fromCols A₂ *ᵥ Sum.elim v₁ v₂ = A₁ *ᵥ v₁ + A₂ *ᵥ v₂

Tactic:
by
  ext
  simp [Matrix.mulVec, fromCols]

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Semiring R
⊢ fromCols 0 0 = 0

Tactic:
ext _ (_ | _) <;> simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
⊢ (A₁.fromRows A₂)ᴴ = A₁ᴴ.fromCols A₂ᴴ

Tactic:
ext _ (_ | _) <;> simp

Goal state after:
Module: Mathlib.Data.Nat.Cast.SetInterval

Goal state before:
pp: a : ℕ
⊢ Nat.cast '' Iic a = Icc 0 ↑a

Tactic:
← Icc_bot,

Goal state after:
a : ℕ
⊢ Nat.cast '' Icc ⊥ a = Icc 0 ↑a
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum < fib n

Tactic:
calc
      fib a + (map fib l).sum < fib a + fib (a - 1) := by gcongr; exact sum_fib_lt hl.2 this
      _ ≤ fib n := by
        rw [add_comm, ← fib_add_one (hl.1.2.trans_lt' zero_lt_two).ne']; exact fib_mono (hn _ rfl)

Goal state after: