mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
⊢ ∃ j g,
    LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
let fs : ∀ a : α, j0 ⟶ j a := fun a => (hj0 (hj a)).some

Goal state after:
case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a ↦ ⋯.some
⊢ ∃ j g,
    LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))
x : ↑↑b
this : f ↑↑x = Fiber.image (f ∘ fun x ↦ ↑x) b
⊢ ↑↑x ∈ ↑(Fiber.mk f ↑(Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b))

Tactic:
Fiber.mem_iff_eq_image,

Goal state after:
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))
x : ↑↑b
this : f ↑↑x = Fiber.image (f ∘ fun x ↦ ↑x) b
⊢ f ↑↑x = Fiber.image f (Fiber.mk f ↑(Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b))
Module: Mathlib.Topology.Category.CompHausLike.Cartesian

Goal state before:
pp: case fst
P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop × ↑Y.toTop)
x✝¹ : BinaryFan X Y
x✝ : x✝¹.pt ⟶ of P (↑X.toTop × ↑Y.toTop)
h₁ : x✝ ≫ ofHom P { toFun := Prod.fst, continuous_toFun := ⋯ } = x✝¹.fst
h₂ : x✝ ≫ ofHom P { toFun := Prod.snd, continuous_toFun := ⋯ } = x✝¹.snd
x : ↑x✝¹.pt.toTop
⊢ ((ConcreteCategory.hom x✝) x).1 =
    ((ConcreteCategory.hom
          (ofHom P
            { toFun := fun x ↦ ((ConcreteCategory.hom x✝¹.fst) x, (ConcreteCategory.hom x✝¹.snd) x),
              continuous_toFun := ⋯ }))
        x).1

pp: case snd
P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop × ↑Y.toTop)
x✝¹ : BinaryFan X Y
x✝ : x✝¹.pt ⟶ of P (↑X.toTop × ↑Y.toTop)
h₁ : x✝ ≫ ofHom P { toFun := Prod.fst, continuous_toFun := ⋯ } = x✝¹.fst
h₂ : x✝ ≫ ofHom P { toFun := Prod.snd, continuous_toFun := ⋯ } = x✝¹.snd
x : ↑x✝¹.pt.toTop
⊢ ((ConcreteCategory.hom x✝) x).2 =
    ((ConcreteCategory.hom
          (ofHom P
            { toFun := fun x ↦ ((ConcreteCategory.hom x✝¹.fst) x, (ConcreteCategory.hom x✝¹.snd) x),
              continuous_toFun := ⋯ }))
        x).2

Tactic:
exacts [ConcreteCategory.congr_hom h₁ _, ConcreteCategory.congr_hom h₂ _]

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Cartesian

Goal state before:
pp: case inl
P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop ⊕ ↑Y.toTop)
x✝¹ : BinaryCofan X Y
x✝ : of P (↑X.toTop ⊕ ↑Y.toTop) ⟶ x✝¹.pt
h₁ : ofHom P { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ x✝ = x✝¹.inl
h₂ : ofHom P { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ x✝ = x✝¹.inr
val✝ : ↑X.toTop
⊢ (ConcreteCategory.hom x✝) (Sum.inl val✝) =
    (ConcreteCategory.hom
        (ofHom P
          { toFun := Sum.elim ⇑(ConcreteCategory.hom x✝¹.inl) ⇑(ConcreteCategory.hom x✝¹.inr), continuous_toFun := ⋯ }))
      (Sum.inl val✝)

pp: case inr
P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop ⊕ ↑Y.toTop)
x✝¹ : BinaryCofan X Y
x✝ : of P (↑X.toTop ⊕ ↑Y.toTop) ⟶ x✝¹.pt
h₁ : ofHom P { toFun := Sum.inl, continuous_toFun := ⋯ } ≫ x✝ = x✝¹.inl
h₂ : ofHom P { toFun := Sum.inr, continuous_toFun := ⋯ } ≫ x✝ = x✝¹.inr
val✝ : ↑Y.toTop
⊢ (ConcreteCategory.hom x✝) (Sum.inr val✝) =
    (ConcreteCategory.hom
        (ofHom P
          { toFun := Sum.elim ⇑(ConcreteCategory.hom x✝¹.inl) ⇑(ConcreteCategory.hom x✝¹.inr), continuous_toFun := ⋯ }))
      (Sum.inr val✝)

Tactic:
exacts [ConcreteCategory.congr_hom h₁ _, ConcreteCategory.congr_hom h₂ _]

Goal state after:
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
⊢ ∀ (xj : (fun X ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))),
    (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i))) fi =
        (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op j))) xj →
      ∃ k f g,
        (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map f)) fi =
          (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map g)) xj

Tactic:
(fj : LocallyConstant _ _)

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
⊢ (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i))) fi =
      (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op j))) fj →
    ∃ k f g,
      (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map f)) fi =
        (ConcreteCategory.hom (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map g)) fj
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)
f : LocallyConstant (↑c.pt.toTop) X
⊢ ∃ i xi, f = (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi

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

Goal state after:
case refine_1
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
f : LocallyConstant (↑c.pt.toTop) X
j : ℕᵒᵖ
h : ∃ g, f = LocallyConstant.comap (TopCat.Hom.hom ((lightToProfinite.mapCone c).π.app j).hom) g
⊢ ∃ i xi, f = (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi
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
⊢ ∀ (xj : (fun X ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))),
    (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i))) fi =
        (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op j))) xj →
      ∃ k f g,
        (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f)) fi =
          (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g)) xj

Tactic:
(fj : LocallyConstant _ _)

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
⊢ (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i))) fi =
      (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op j))) fj →
    ∃ k f g,
      (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f)) fi =
        (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g)) fj
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
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).obj P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e

Tactic:
refine ⟨S', π, hπ, (μIso (free R) _ _).hom ≫ 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
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 ≫ g') ≫ e
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
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ g = g' ≫ e

Tactic:
refine ⟨S', π, hπ, (μIso (free R) _ _).hom ≫ 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
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 ≫ g') ≫ e
Module: Mathlib.Control.Bitraversable.Lemmas

Goal state before:
pp: t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ α₂ β : Type u
f : α₀ → F α₁
f' : α₁ → G α₂
x : t α₀ β
⊢ bitraverse (Comp.mk ∘ map f' ∘ f) (Comp.mk ∘ map pure ∘ pure) x = tfst (Comp.mk ∘ map f' ∘ f) x

Tactic:
simp only [Function.comp_def, tfst, map_pure, Pure.pure]

Goal state after:
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
hk : Nat.find h' = k + ↑Upto.zero
⊢ Part.fix f x = Fix.approx f k.succ x

Tactic:
revert hk

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero → Part.fix f x = Fix.approx f k.succ x
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{?u.3} 0
β : TypeVec.{?u.6} 0
i : Fin2 0
⊢ α i → β i

Tactic:
apply Fin2.elim0 i

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

Goal state before:
pp: 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)).2 = x
x : T
⊢ (¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x) ↔
    ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun ⟨n, hn, hn'⟩ ↦ ?_⟩

Goal state after:
case refine_1
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)).2 = x
x : T
x✝ : ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
h₁ : ¬(π x).2 = none
h₂ : ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
⊢ ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i

case refine_2
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)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = ↑n
⊢ ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ Pairwise (fun l₁ l₂ ↦ ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) L ↔
    Pairwise (fun a b ↦ a.keys.Disjoint b.keys) L

Tactic:
simp [keys, disjoint_iff_ne, Sigma.forall]

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

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

Tactic:
by
  induction l with
  | nil => grind
  | cons s _ _ => by_cases s.fst = a <;> grind

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

Goal state before:
pp: case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
⊢ (if True then ∅ else s) = (image (const β✝) s).sup fun f ↦ image f ∅

Tactic:
image_empty,

Goal state after:
case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
⊢ (if True then ∅ else s) = (image (const β✝) s).sup fun f ↦ ∅
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
t : Finset β✝
⊢ ∅ = (image (const α✝ id) ∅).sup fun f ↦ image f t

Tactic:
image_empty,

Goal state after:
case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
t : Finset β✝
⊢ ∅ = ∅.sup fun f ↦ image f t
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : a = ah
h₂ : a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

Tactic:
subst h₁ h₂

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a' : α
tl : List (Sigma β)
h : a' ≠ a'
ih : dlookup a' (kerase a' tl) = dlookup a' tl
bh : β a'
⊢ dlookup a' (kerase a' (⟨a', bh⟩ :: tl)) = dlookup a' (⟨a', bh⟩ :: tl)
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ f.toAList.keys.toFinset ↔ f x ≠ 0

Tactic:
toAList_keys_toFinset,

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ f.support ↔ f x ≠ 0
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 g : α →₀ N
a : α
⊢ a ∈ f.neLocus g ↔ f a ≠ g a

Tactic:
simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff,
    and_iff_right_iff_imp] using Ne.ne_or_ne _

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₃
⊢ x ⊗ y ⊗ z ≍ x ⊗ (y ⊗ z)

Tactic:
by simp [cast_heq, mul_assoc0, assocLeft]

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

Goal state before:
pp: case ofNat
a✝ : ℕ
⊢ a✝.bodd = (ofNat a✝).bodd

Tactic:
simp [bodd]

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

Goal state before:
pp: case negSucc
a✝ : ℕ
⊢ (↑(a✝ + 1)).bodd = -[a✝+1].bodd

Tactic:
simp [bodd]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: case h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∀ b ∈ (Finset.range d).attach, b ≠ ⟨i, ⋯⟩ → (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

Tactic:
intro (b : { x // x ∈ Finset.range d })

Goal state after:
case h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : ↥(Finset.range d)
⊢ b ∈ (Finset.range d).attach → b ≠ ⟨i, ⋯⟩ → (if i = ↑b then x.slice ↑b ⋯ else 0) = 0
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (bit b -[n+1]).testBit m.succ = -[n+1].testBit m

Tactic:
dsimp only [testBit]
    simp only [bit_negSucc]
    cases b <;> simp only [Bool.not_false, Bool.not_true, Nat.testBit_bit_succ]

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

Goal state before:
pp: n m : ℕ
hnm : n < m
⊢ filter (fun x ↦ decide (x < n + 1)) (Ico n m) = [n]

Tactic:
have r : min m (n + 1) = n + 1 := (@inf_eq_right _ _ m (n + 1)).mpr hnm

Goal state after:
n m : ℕ
hnm : n < m
r : min m (n + 1) = n + 1
⊢ filter (fun x ↦ decide (x < n + 1)) (Ico n m) = [n]
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
⊢ Shortlex r (s ++ t₁) (s ++ t₂)

Tactic:
rcases shortlex_def.mp h with h1 | h2
  · apply of_length_lt
    rw [List.length_append, List.length_append]
    lia
  cases s with
  | nil =>
    rw [List.nil_append, List.nil_append]
    exact h
  | cons head tail =>
    apply of_lex
    · simp only [List.cons_append, List.length_cons, List.length_append,
      add_left_inj, add_right_inj]
      exact h2.1
    exact List.Lex.append_left r h2.2 (head :: tail)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: l : Type u_1
m : Type u_2
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m m A
k : ℕ
⊢ mulRightLinearMap l R a ^ 0 = mulRightLinearMap l R (a ^ 0)

Tactic:
by rw [pow_zero, pow_zero, mulRightLinearMap_one, Module.End.one_eq_id]

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ Y₂ + X₂ = Z₁ + X₁

Tactic:
rwa [eq_comm]

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

Goal state before:
pp: case intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M : Multiset α
hM : Acc OneStep M
⊢ Acc OneStep (a ::ₘ M)

Tactic:
induction hM with | _ M hM ihM

Goal state after:
case intro.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
⊢ Acc OneStep (a ::ₘ M)
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: q : ℚ≥0
⊢ ⌊q⌋₊ = q.num / q.den

Tactic:
← Int.natCast_inj,

Goal state after:
q : ℚ≥0
⊢ ↑⌊q⌋₊ = ↑(q.num / q.den)
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: p q : ℚ
hq : 0 ≤ q
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat

Tactic:
div_eq_inv_mul,

Goal state after:
p q : ℚ
hq : 0 ≤ q
⊢ (q⁻¹ * p).toNNRat = p.toNNRat / q.toNNRat
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: p q : ℚ
hq : 0 ≤ q
⊢ (q⁻¹ * p).toNNRat = p.toNNRat / q.toNNRat

Tactic:
div_eq_inv_mul,

Goal state after:
p q : ℚ
hq : 0 ≤ q
⊢ (q⁻¹ * p).toNNRat = q.toNNRat⁻¹ * p.toNNRat
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
n p : ℕ
hp : IsNilpotent ↑p
h : p.Coprime n
⊢ IsUnit ↑n

Tactic:
obtain ⟨m, hm⟩ := hp

Goal state after:
A : Type u_1
inst✝ : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : ↑p ^ m = 0
⊢ IsUnit ↑n
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: i j : ℕ
⊢ i.dist j = max i j - min i j

Tactic:
cases le_total i j <;> simp [Nat.dist, *]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

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

Tactic:
exact hl'.sum_fib_lt (by simpa)

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ p ^ (multiplicity p n + 1) ∣ n

Tactic:
nth_rw 2 [hm]

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ p ^ (multiplicity p n + 1) ∣ p ^ multiplicity p n * m
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
⊢ nth p n = 0 ↔ p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ n

Tactic:
by
  refine ⟨fun h => ?_, ?_⟩
  · simp only [or_iff_not_imp_right, not_exists, not_le]
    exact fun hn => ⟨h ▸ nth_mem _ hn, nonpos_iff_eq_zero.1 <| h ▸ le_nth hn⟩
  · rintro (⟨h₀, rfl⟩ | ⟨hf, hle⟩)
    exacts [nth_zero_of_zero h₀, nth_of_card_le hf hle]

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

Goal state before:
pp: case zero
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hn : ∀ (hf : (Set.ofPred p).Finite), 0 < #hf.toFinset
⊢ f 0 ≤ nth p 0

Tactic:
rw [Nat.nth_zero]

Goal state after:
case zero
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hn : ∀ (hf : (Set.ofPred p).Finite), 0 < #hf.toFinset
⊢ f 0 ≤ sInf (Set.ofPred p)
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rx : α
rr : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
rlx : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
exact node 3 (ι x) rlx ι rx

Goal state after:
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α

Tactic:
exact node 3 (ι x) rlx ι rx

Goal state after: