mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_2
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : I
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toProfinite.obj (F.obj k)).toTop
x : ↑(((const I).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
⊢ fi ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toProfinite).map ki)) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toProfinite).map kj)) x)

Tactic:
have h := LocallyConstant.congr_fun h x

Goal state after:
case refine_2
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h✝¹ :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : I
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toProfinite.obj (F.obj k)).toTop
x : ↑(((const I).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toProfinite).map ki)) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toProfinite).map kj)) x)
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
⊢ fi ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toLightProfinite).map ki)) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toLightProfinite).map kj)) x)

Tactic:
have h := LocallyConstant.congr_fun h x

Goal state after:
case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h✝¹ :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
h :
  (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi) x =
    (LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj) x
⊢ fi ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toLightProfinite).map ki)) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toLightProfinite).map kj)) x)
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ X : CondensedSet
⊢ ∀ {Y : Type (u + 1)} [tY : TopologicalSpace Y] (f : ↑X.toTopCat → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, ↑X.toTopCat)), Continuous (f ∘ ⇑g)) → Continuous f

Tactic:
intro Y _ f h

Goal state after:
X✝ X : CondensedSet
Y : Type (u + 1)
tY✝ : TopologicalSpace Y
f : ↑X.toTopCat → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, ↑X.toTopCat)), Continuous (f ∘ ⇑g)
⊢ Continuous f
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
⊢ (fun i t ↦ (↑t).1) <$$> u✝ = x ∧ (fun i t ↦ (↑t).2) <$$> u✝ = y ↔
    (fun i x ↦ (↑(f' rr n α i x)).1) <$$> u✝ = x ∧ (fun i x ↦ (↑(f' rr n α i x)).2) <$$> u✝ = y

Tactic:
apply iff_of_eq

Goal state after:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
⊢ ((fun i t ↦ (↑t).1) <$$> u✝ = x ∧ (fun i t ↦ (↑t).2) <$$> u✝ = y) =
    ((fun i x ↦ (↑(f' rr n α i x)).1) <$$> u✝ = x ∧ (fun i x ↦ (↑(f' rr n α i x)).2) <$$> u✝ = y)
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : f.Realizer
x✝ : Set β
⊢ (∃ b, F.F.f b ⊆ m ⁻¹' x✝) ↔ m ⁻¹' x✝ ∈ f

Tactic:
F.mem_sets

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : f.Realizer
x✝ : Set β
⊢ (∃ b, F.F.f b ⊆ m ⁻¹' x✝) ↔ ∃ b, F.F.f b ⊆ m ⁻¹' x✝
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
⊢ ∃ S' T' y' π' g',
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧ Epi (cover π')

Tactic:
let S'π (n : ℕ∪{∞}) : LightProfinite.of (S' π) ⟶ LightProfinite.fibre n (π ≫ snd _ _) :=
    ⟨TopCat.ofHom {
      toFun x := x.val n,
      continuous_toFun := by refine (continuous_apply _).comp ?_; fun_prop }⟩

Goal state after:
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
⊢ ∃ S' T' y' π' g',
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧ Epi (cover π')
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → Filter β
G : (i : α) → (m i).Realizer
x✝ : Set β
σ✝ : Type ?u.147
F : CFilter (Set α) σ✝
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | ⟨s, f⟩ => ⋃ i, ⋃ (h : i ∈ { σ := σ✝, F := F, eq := ⋯ }.F.f s), (G i).F.f (f i h),
            pt := ⟨{ σ := σ✝, F := F, eq := ⋯ }.F.pt, fun i x ↦ (G i).F.pt⟩,
            inf := fun x x_1 ↦
              match x with
              | ⟨a, f⟩ =>
                match x_1 with
                | ⟨b, f'⟩ => ⟨{ σ := σ✝, F := F, eq := ⋯ }.F.inf a b, fun i h ↦ (G i).F.inf (f i ⋯) (f' i ⋯)⟩,
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (F.toFilter.bind m).sets

Tactic:
simp only [CFilter.toFilter, iUnion_subset_iff, Sigma.exists, Filter.mem_sets, mem_bind]

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → Filter β
G : (i : α) → (m i).Realizer
x✝ : Set β
σ✝ : Type ?u.147
F : CFilter (Set α) σ✝
⊢ x✝ ∈ {a | ∃ a_1 b, ∀ (i : α) (i_1 : i ∈ F.f a_1), (G i).F.f (b i i_1) ⊆ a} ↔
    ∃ t ∈ { sets := {a | ∃ b, F.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }, ∀ x ∈ t, x✝ ∈ m x
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i) →
    ∃ a ∈ s.pi t, { toFun := fun f ↦ DFinsupp.mk s fun i ↦ f ↑i ⋯, inj' := ⋯ } a = f

Tactic:
refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
⊢ ({ toFun := fun f ↦ DFinsupp.mk s fun i ↦ f ↑i ⋯, inj' := ⋯ } fun i x ↦ f i) = f
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
b : Bool
⊢ count (!b) l + count b l = l.length

Tactic:
by
  have := length_eq_countP_add_countP (l := l) (· == !b)
  aesop (add simp this)

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ ∏ i ∈ f.support, #(f i) = f.prod fun i ↦ ↑(#(f i))

Tactic:
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.natCast_apply, Nat.cast_id]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ toDFinsupp (replicate n a) = DFinsupp.single a n

Tactic:
by
  ext i
  dsimp [toDFinsupp]
  simp [count_replicate]

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

Goal state before:
pp: case refine_1
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this✝ : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop :=
  fun n ↦
    ⇑(ConcreteCategory.hom
        (pullback.lift π (y' ▷ ℕ∪{∞}) (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
          (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
            (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n))
          ⋯))
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
hσ' :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).2 = x
this : CompactSpace ↑(fibres (⇑(ConcreteCategory.hom π')) σ')
⊢ Epi π'

Tactic:
dsimp [π']

Goal state after:
case refine_1
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this✝ : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop :=
  fun n ↦
    ⇑(ConcreteCategory.hom
        (pullback.lift π (y' ▷ ℕ∪{∞}) (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
          (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
            (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n))
          ⋯))
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
hσ' :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).2 = x
this : CompactSpace ↑(fibres (⇑(ConcreteCategory.hom π')) σ')
⊢ Epi (pullback.snd π (y' ▷ ℕ∪{∞}))
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
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p

Tactic:
obtain ⟨r_inf, hr⟩ := Injective.factors (𝟙 _) (LightProfinite.fibreIncl ∞ (π' ≫ snd _ _))

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' ℕ∪{∞}))
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : ¬a' = x.fst
h' : a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : ¬a' = x.fst
h' : ¬a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Tactic:
· subst a
      simp [kerase_cons_eq rfl, kerase_cons_ne (Ne.symm h)]

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : ¬a' = x.fst
h' : ¬a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
h : sizeOf xs.dedupKeys ≤ sizeOf xs
⊢ sizeOf (x :: xs).dedupKeys ≤ sizeOf (x :: xs)

Tactic:
| cons x xs h =>

Goal state after:
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)
⊢ 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)
⊢ x ∉ (f i).erase x
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
l : List (ι →₀ M)
x : ι
⊢ x ∈ foldr (fun x1 x2 ↦ x1.support ∪ x2) ∅ l ↔ ∃ f ∈ l, f x ≠ 0

Tactic:
induction l with
  | nil => simp
  | cons hd tl IH =>
    simp only [foldr, Finset.mem_union, Finsupp.mem_support_iff, ne_eq, IH,
      mem_cons, exists_eq_or_imp]

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 - g).support

Tactic:
rw [← neLocus_add_right _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]

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

Goal state before:
pp: case mpr.right
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) % b = r

Tactic:
add_mul_emod_self_left,

Goal state after:
case mpr.right
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ r % b = r
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ -1 * ↑r < -↑(v % r) ∧ -↑(v % r) ≤ 0 * ↑r

Tactic:
neg_one_mul,

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ -↑r < -↑(v % r) ∧ -↑(v % r) ≤ 0 * ↑r
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: α : Type u_1
l : List α
p : l.Palindrome
⊢ l.reverse = l

Tactic:
by
  induction p <;> try (exact rfl)
  simpa

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

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h1 : s₁.length < s₂.length
⊢ Shortlex r s₁ (s₂ ++ t)

pp: case inr
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
⊢ Shortlex r s₁ (s₂ ++ t)

Tactic:
· apply of_length_lt
    rw [List.length_append]
    lia

Goal state after:
case inr
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
⊢ Shortlex r s₁ (s₂ ++ t)
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inr.cons
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
head : α
tail : List α
⊢ s₁.length < (s₂ ++ head :: tail).length

Tactic:
List.length_append,

Goal state after:
case inr.cons
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
head : α
tail : List α
⊢ s₁.length < s₂.length + (head :: tail).length
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
n : ℕ
⊢ (n :: sz).splitLengths l = take n l :: sz.splitLengths (drop n l)

Tactic:
simp [splitLengths]

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

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h1 : t₁.length < t₂.length
⊢ (s ++ t₁).length < (s ++ t₂).length

Tactic:
List.length_append,

Goal state after:
case inl
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h1 : t₁.length < t₂.length
⊢ s.length + t₁.length < (s ++ t₂).length
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
m : ℕ
⊢ IsNat r m → IsNat ⌈r⌉₊ m

Tactic:
rintro ⟨⟨⟩⟩
  exact ⟨by simp⟩

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
m : ℕ
⊢ IsInt r (Int.negOfNat m) → IsNat ⌈r⌉₊ 0

Tactic:
rintro ⟨⟨⟩⟩
  exact ⟨by simp⟩

Goal state after:
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
⊢ (List.map s l).prod ≠ 0

Tactic:
simp only [ne_eq, List.prod_eq_zero_iff, List.mem_map, not_exists, not_and]

Goal state after:
case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
⊢ ∀ x ∈ l, ¬s x = 0
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : ↑p ^ m = 0
⊢ IsUnit ↑n

Tactic:
suffices ∃ a b : A, p ^ m * a + n * b = 1 by
    obtain ⟨a, b, h⟩ := this
    refine .of_mul_eq_one b ?_
    simpa [hm] using h

Goal state after:
A : Type u_1
inst✝ : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : ↑p ^ m = 0
⊢ ∃ a b, ↑p ^ m * a + ↑n * b = 1
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
| (∑ i ∈ range (n % p + 1),
        ∑ j ∈ range (n / p + 1), X ^ i * ↑((n % p).choose i) * (X ^ (p * j) * ↑((n / p).choose j))).coeff
    k

Tactic:
enter [

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
| (∑ i ∈ range (n % p + 1),
        ∑ j ∈ range (n / p + 1), X ^ i * ↑((n % p).choose i) * (X ^ (p * j) * ↑((n / p).choose j))).coeff
    k
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
⊢ k % p = x₁ ∧ k / p = x₂

pp: case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k % p = x₁ ∧ k / p = x₂
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2

Tactic:
· simp only [mem_product, mem_range] at hx
      have h' : x₁ < p := lt_of_lt_of_le hx.left <| mod_lt _ Fin.pos'
      rw [h, add_mul_mod_self_left, add_mul_div_left _ _ Fin.pos', eq_comm (b := x₂)]
      exact ⟨mod_eq_of_lt h', right_eq_add.mpr (div_eq_of_lt h')⟩

Goal state after:
case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k % p = x₁ ∧ k / p = x₂
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (n - fib n.greatestFib).greatestFib ≤ n.greatestFib - 2

Tactic:
rw [← Nat.lt_succ_iff, greatestFib_lt, tsub_lt_iff_right n.fib_greatestFib_le, Nat.sub_succ,
    succ_pred, ← fib_add_one]

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n < fib (n.greatestFib + 1)

n : ℕ
hn : n ≠ 0
⊢ n.greatestFib ≠ 0

n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
hn : k ∉ Set.range fun x ↦ x + m
⊢ False

Tactic:
Set.mem_range,

Goal state after:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
hn : ¬∃ y, y + m = k
⊢ False
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a : PosNum
⊢ (a + a).pred'.toZNumNeg = (neg a).bit1

Tactic:
a.bit0_of_bit0

Goal state after:
a : PosNum
⊢ a.bit0.pred'.toZNumNeg = (neg a).bit1