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

Goal state before:
pp: S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x✝ : Option Γ'
⊢ Λ'.Supports S ((fun s ↦ (if s = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) k) (unrev q)) x✝)

Tactic:
dsimp only

Goal state after:
S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x✝ : Option Γ'
⊢ Λ'.Supports S ((if x✝ = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) k) (unrev q))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type ?u.19} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
R : ∀ {α : Type ?u.21} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
s : Option Γ'
⊢ (fun s ↦ bif natEnd (s.getD default) then Λ'.ret a✝ else Λ'.clear natEnd main (trNormal a✝¹ (Cont'.fix a✝¹ a✝))) s ∈ S

Tactic:
dsimp only

Goal state after:
case fix
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type ?u.19} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
R : ∀ {α : Type ?u.21} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
s : Option Γ'
⊢ (bif natEnd (s.getD default) then Λ'.ret a✝ else Λ'.clear natEnd main (trNormal a✝¹ (Cont'.fix a✝¹ a✝))) ∈ S
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)
X : Type (max u w)
⊢ Presheaf.IsSheaf (coherentTopology (CompHausLike P)) (functorToPresheaves.obj X)

Tactic:
rw [Presheaf.isSheaf_of_iso_iff (functorToPresheavesIso P hs 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)
X : Type (max u w)
⊢ Presheaf.IsSheaf (coherentTopology (CompHausLike P)) (TopCat.toSheafCompHausLike P (TopCat.discrete.obj X) hs).obj
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 Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
this✝ : Preregular (CompHausLike P)
S : (CompHausLike P)ᵒᵖ
f : LocallyConstant (↑(unop S).toTop) (X.obj.obj (op (of P PUnit.{u + 1})))
a : Fiber ⇑(map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f)
b :
  Fiber
    ⇑(comap (TopCat.Hom.hom (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
        f)
this :
  (ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))
      (f (preimage (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1})))) ∘ ⇑f) a)) =
    Fiber.image (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1})))) ∘ ⇑f) a
⊢ (ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))
        (f
          ↑(preimage
              (⇑f ∘
                ⇑(TopologicalSpace.Fiber.sigmaIncl ((ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1})))).1 ∘ ⇑f)
                    a))
              b)) =
      Fiber.image (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1})))) ∘ ⇑f) a ↔
    ↑(preimage
          (⇑(comap
              (TopCat.Hom.hom (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
              f))
          b) ∈
      ↑a

Tactic:
exact (mem_iff_eq_image (g.hom.app _ ∘ f) _ _).symm

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

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop × ↑Y.toTop)
⊢ ∀ (s : BinaryFan X Y),
    ofHom P
          { toFun := fun x ↦ ((ConcreteCategory.hom s.fst) x, (ConcreteCategory.hom s.snd) x), continuous_toFun := ⋯ } ≫
        ofHom P { toFun := Prod.fst, continuous_toFun := ⋯ } =
      s.fst

Tactic:
rfl_cat

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

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop × ↑Y.toTop)
⊢ ∀ (s : BinaryFan X Y),
    ofHom P
          { toFun := fun x ↦ ((ConcreteCategory.hom s.fst) x, (ConcreteCategory.hom s.snd) x), continuous_toFun := ⋯ } ≫
        ofHom P { toFun := Prod.snd, continuous_toFun := ⋯ } =
      s.snd

Tactic:
rfl_cat

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

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop ⊕ ↑Y.toTop)
⊢ ∀ (s : BinaryCofan X Y),
    ofHom P { toFun := Sum.inl, continuous_toFun := ⋯ } ≫
        ofHom P
          { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
      s.inl

Tactic:
rfl_cat

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

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop ⊕ ↑Y.toTop)
⊢ ∀ (s : BinaryCofan X Y),
    ofHom P { toFun := Sum.inr, continuous_toFun := ⋯ } ≫
        ofHom P
          { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
      s.inr

Tactic:
rfl_cat

Goal state after:
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: case e_4
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ Comp.instApplicativeComp = inst✝¹

Tactic:
apply Comp.applicative_comp_id

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Prod

Tactic:
constructor <;> intros <;> casesm _ × _ <;>
    simp [bitraverse, Prod.bitraverse, functor_norm] <;> rfl

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

Goal state before:
pp: p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property✝ : ∀ (j : ℕ), j < b → ¬p j
⊢ a > b ↔ x - a < x - b

Tactic:
rw [tsub_lt_tsub_iff_left_of_le (le_of_not_gt fun h' => ha _ h' h)]

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: n : ℕ
⊢ last.rev = fz

Tactic:
induction n

Goal state after:
case zero
⊢ last.rev = fz

case succ
n✝ : ℕ
a✝ : last.rev = fz
⊢ last.rev = fz
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: case fz
n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
⊢ fz ∈ Finset.cons fz (Finset.map { toFun := fs, inj' := ⋯ } elems) ⋯

Tactic:
simp [compl]

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: case fs
n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
i : Fin2 n
⊢ i.fs ∈ Finset.cons fz (Finset.map { toFun := fs, inj' := ⋯ } elems) ⋯

Tactic:
simp [compl]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
n : ℕ
α : TypeVec.{u_1} n
⊢ (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)

Tactic:
induction n

Goal state after:
case zero
β : Type u_1
α : TypeVec.{u_1} 0
⊢ (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)

case succ
β : Type u_1
n✝ : ℕ
a✝ : ∀ (α : TypeVec.{u_1} n✝), (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)
α : TypeVec.{u_1} (n✝ + 1)
⊢ (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: 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' ▷ ℕ∪{∞})
n : ↑ℕ∪{∞}.toTop
⊢ (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π =
    lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
        (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
      y' ▷ ℕ∪{∞}

Tactic:
apply CartesianMonoidalCategory.hom_ext<;> ext x

Goal state after:
case h_fst
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' ▷ ℕ∪{∞})
n : ↑ℕ∪{∞}.toTop
x : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop
⊢ (ConcreteCategory.hom (((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ fst S ℕ∪{∞})) x =
    (ConcreteCategory.hom
        ((lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
              (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
            y' ▷ ℕ∪{∞}) ≫
          fst S ℕ∪{∞}))
      x

case h_snd
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' ▷ ℕ∪{∞})
n : ↑ℕ∪{∞}.toTop
x : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop
⊢ (ConcreteCategory.hom (((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ snd S ℕ∪{∞})) x =
    (ConcreteCategory.hom
        ((lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
              (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
            y' ▷ ℕ∪{∞}) ≫
          snd S ℕ∪{∞}))
      x
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
f : Filter α
F : f.Realizer
⊢ f ≠ ⊥ ↔ ∀ (a : F.σ), (F.F.f a).Nonempty

Tactic:
not_iff_comm,

Goal state after:
α : Type u_1
f : Filter α
F : f.Realizer
⊢ (¬∀ (a : F.σ), (F.F.f a).Nonempty) ↔ f = ⊥
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ l.length / 2 ≤ count b l

Tactic:
rw [Nat.div_le_iff_le_mul_add_pred two_pos, ← tsub_le_iff_right]

Goal state after:
l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ l.length - (2 - 1) ≤ 2 * count b l
Module: Mathlib.Data.DFinsupp.Interval

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

Tactic:
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]

Goal state after:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: case cons
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
⊢ ⨅ i, ∑ a ∈ Finset.cons a s ha, f i a = ∑ a ∈ Finset.cons a s ha, ⨅ i, f i a

Tactic:
simp only [Finset.sum_cons, ← ih]

Goal state after:
case cons
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
⊢ ⨅ i, f i a + ∑ a ∈ s, f i a = (⨅ i, f i a) + ⨅ i, ∑ a ∈ s, f i a
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
⊢ InternallyProjective ((free R).obj ℕ∪{∞}.toCondensed)

Tactic:
rw [free_lightProfinite_internallyProjective_iff_tensor_condition' R ℕ∪{∞}]

Goal state after:
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
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
γ : Type u_1
s : AList β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ ⟦s⟧.liftOn f H = f s

Tactic:
cases s
  rfl

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

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

Tactic:
induction x using Quotient.inductionOn
  simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map]
  rw [Traversable.map_traverse']
  simp only [fmap_def, Function.comp_apply, Functor.map_map, List.map_eq_map, map_coe]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
l : List (Sigma β)
⊢ (kerase a (s :: tail✝)).kunion (kerase a l) = kerase a ((s :: tail✝).kunion l)

Tactic:
by_cases h : a = s.1 <;> simp [h, kerase_comm a s.1 l, kunion_kerase]

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⟩ ∈ l.entries ∧ decide (b ≠ 0) = true) ↔ (lookup a l).getD 0 ≠ 0

Tactic:
← mem_lookup_iff

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : f a = 0
this : lookup a f.toAList = none
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
simp [h, this]

Goal state after:
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (Disjoint on Finsupp.support) s
⊢ s.sum.support = (map Finsupp.support s).sup

Tactic:
induction s using Quot.inductionOn with | _ a
   =>  _ 

Goal state after:
case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a : List (ι →₀ M)
hs : Pairwise (Disjoint on Finsupp.support) (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).support =
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).sup
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 (f + g) = g.support

Tactic:
neLocus_self_add_right

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ g.support = g.support
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: case pos
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k✝ : κ
f : ι k✝ →₀ M
k : κ
i : ι k
h : ⟨k, i⟩.fst = k✝
⊢ f.embSigma ⟨k, i⟩ = f (h ▸ ⟨k, i⟩.snd)

pp: case neg
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k✝ : κ
f : ι k✝ →₀ M
k : κ
i : ι k
h : ¬⟨k, i⟩.fst = k✝
⊢ f.embSigma ⟨k, i⟩ = 0

Tactic:
· subst h
    simp only [embSigma, Embedding.sigmaMk]
    apply embDomain_apply_self

Goal state after:
case neg
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k✝ : κ
f : ι k✝ →₀ M
k : κ
i : ι k
h : ¬⟨k, i⟩.fst = k✝
⊢ f.embSigma ⟨k, i⟩ = 0
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: n : ℕ
⊢ (bif (↑n).bodd then 1 else 0) + 2 * (↑n).div2 = ↑n

Tactic:
by
    rw [show (cond (bodd n) 1 0 : ℤ) = (cond (bodd n) 1 0 : ℕ) by cases bodd n <;> rfl]
    exact congr_arg ofNat n.bodd_add_div2

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

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a ^ 2 ≤ b ^ 2

Tactic:
by
  rw [sq, sq]
  exact natAbs_le_iff_mul_self_le

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

Goal state before:
pp: ⊢ bitwise xor = Int.xor

Tactic:
by
  funext m n
  rcases m with m | m <;> rcases n with n | n <;> try {rfl}
    <;> simp only [bitwise, natBitwise, Bool.not_false, Bool.bne_eq_xor,
      cond_false, cond_true, negSucc.injEq, Bool.false_xor,
      Bool.true_xor, Bool.not_true,
      Int.xor, HXor.hXor, XorOp.xor, Nat.xor] <;> simp

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

Goal state before:
pp: case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false true then -[Nat.bitwise (fun x y ↦ !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise (fun x y ↦ !f x !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f x !y) m n))

Tactic:
by_cases h : f false true <;> simp +decide [h]

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

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).ldiff (bit b n) = bit (a && !b) (m.ldiff n)

Tactic:
rw [← bitwise_diff, bitwise_bit]

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

Goal state before:
pp: a b r : ℤ
hr : 0 < r
v : ℤ
⊢ ↑(#({x ∈ Ioc a b | x ≡ v [ZMOD r]})) = max (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) 0

Tactic:
by
  simp [Ioc_filter_modEq_eq, Ioc_filter_dvd_eq, hr]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ (l ++ l.reverse).reverse = l ++ l.reverse

Tactic:
rw [reverse_append, reverse_reverse]

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

Goal state before:
pp: case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = true
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l b (a :: g) gs)

Tactic:
refine IH hgs' hgs fun m hm ↦ ?_
      obtain ⟨ha, _, H⟩ := hga m hm
      refine ⟨ha, append_ne_nil_of_right_ne_nil _ (cons_ne_nil _ _), ?_⟩
      rwa [reverse_cons, head_append_of_ne_nil]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ ha hb, r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
x : List α
hx : x ∈ l
right✝ : x ≠ []
w✝¹ : a ≠ []
w✝ : l.head ⋯ ≠ []
H : r (a.getLast w✝¹) ((l.head ⋯).head w✝) = false
⊢ r (a.getLast ⋯) (l.flatten.head ⋯) = false

Tactic:
head_flatten_eq_head_head

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ ha hb, r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
x : List α
hx : x ∈ l
right✝ : x ≠ []
w✝¹ : a ≠ []
w✝ : l.head ⋯ ≠ []
H : r (a.getLast w✝¹) ((l.head ⋯).head w✝) = false
⊢ r (a.getLast ⋯) ((l.head ⋯).head ?cons.hl') = false

case cons.hl'
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ ha hb, r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
x : List α
hx : x ∈ l
right✝ : x ≠ []
w✝¹ : a ≠ []
w✝ : l.head ⋯ ≠ []
H : r (a.getLast w✝¹) ((l.head ⋯).head w✝) = false
⊢ l.head ⋯ ≠ []
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: case h2
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ snd (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) i✝ j✝ =
    (fst (of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) *
          snd (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j)) +
        snd (of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) *
          fst (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j)))
      i✝ j✝

Tactic:
simp only [mul_apply, snd_sum, DualNumber.snd_mul, snd_mk, of_apply, fst_mk, add_apply]

Goal state after:
case h2
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ ∑ x, (fst (A i✝ x) * snd (B x j✝) + snd (A i✝ x) * fst (B x j✝)) =
    ∑ x, fst (A i✝ x) * snd (B x j✝) + ∑ x, snd (A i✝ x) * fst (B x j✝)
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case refine_4
α : 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 : α), y ∈ Y₁ + (Y₂ - Z₁) → ∃ z, z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z

Tactic:
simp only [mem_add, or_imp, forall_and]

Goal state after:
case refine_4
α : 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
⊢ (∀ (x : α), x ∈ Y₁ → ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z) ∧
    ∀ (x : α), x ∈ Y₂ - Z₁ → ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z