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

Goal state before:
pp: case neg.convert_8
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
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.fix f k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
    s'
⊢ Option.elim'
    (update (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail main = (trNat v.headI).tail ∧
      trList v.tail = [])
    (fun a ↦
      natEnd a = true ∧
        update (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail main =
          (trNat v.headI).tail ++ a :: trList v.tail)
    (some Γ'.cons)

Tactic:
exact ⟨rfl, this.2⟩

Goal state after:
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
w✝¹ : ↑(Set.range f)
val✝¹ : S
hx✝ : val✝¹ ∈ ↑⟨(fun x ↦ f ⁻¹' {↑x}) w✝¹, ⋯⟩
hx : f val✝¹ ∈ {↑w✝¹}
w✝ : ↑(Set.range f)
val✝ : S
hy✝ : val✝ ∈ ↑⟨(fun x ↦ f ⁻¹' {↑x}) w✝, ⋯⟩
hy : f val✝ ∈ {↑w✝}
h : val✝¹ = val✝
⊢ ⟨⟨(fun x ↦ f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx✝⟩⟩.fst = ⟨⟨(fun x ↦ f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy✝⟩⟩.fst

Tactic:
Set.mem_singleton_iff

Goal state after:
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
w✝¹ : ↑(Set.range f)
val✝¹ : S
hx✝ : val✝¹ ∈ ↑⟨(fun x ↦ f ⁻¹' {↑x}) w✝¹, ⋯⟩
hx : f val✝¹ = ↑w✝¹
w✝ : ↑(Set.range f)
val✝ : S
hy✝ : val✝ ∈ ↑⟨(fun x ↦ f ⁻¹' {↑x}) w✝, ⋯⟩
hy : f val✝ = ↑w✝
h : val✝¹ = val✝
⊢ ⟨⟨(fun x ↦ f ⁻¹' {↑x}) w✝¹, ⋯⟩, ⟨val✝¹, hx✝⟩⟩.fst = ⟨⟨(fun x ↦ f ⁻¹' {↑x}) w✝, ⋯⟩, ⟨val✝, hy✝⟩⟩.fst
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✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)
⊢ counitAppAppImage (comap (TopCat.Hom.hom g.unop.hom) f) a =
    (ConcreteCategory.hom (Y.map (componentHom f g.unop a).op))
      (counitAppAppImage f
        (Fiber.mk (⇑f) ((ConcreteCategory.hom g.unop) (preimage (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a))))

Tactic:
simp only [counitAppAppImage, ← Functor.map_comp_apply, ← op_comp]

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✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)
⊢ (ConcreteCategory.hom (Y.map (isTerminalPUnit.from (fiber (comap (TopCat.Hom.hom g.unop.hom) f) a)).op))
      (Fiber.image (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a) =
    (ConcreteCategory.hom
        (Y.map
          (componentHom f g.unop a ≫
              isTerminalPUnit.from
                (fiber f
                  (Fiber.mk (⇑f)
                    ((ConcreteCategory.hom g.unop) (preimage (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a))))).op))
      (Fiber.image (⇑f)
        (Fiber.mk (⇑f) ((ConcreteCategory.hom g.unop) (preimage (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a))))
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
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ (lightProfiniteToLightCondSet.map π ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv (lightProfiniteToLightCondSet.obj S) Y) p).hom =
    ((coherentTopology LightProfinite).yonedaEquiv.symm
        ((ConcreteCategory.hom
            ((((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p).hom.app (Opposite.op T)))
          (Quiver.Hom.unop (Opposite.op π)))).hom

Tactic:
← GrothendieckTopology.yonedaEquiv_symm_naturality_right

Goal state after:
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
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ (lightProfiniteToLightCondSet.map π ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv (lightProfiniteToLightCondSet.obj S) Y) p).hom =
    ((coherentTopology LightProfinite).yonedaEquiv.symm (Quiver.Hom.unop (Opposite.op π)) ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p).hom
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case e_a
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj
      (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
this : Finite ↑(fiber f x).toTop
y : ↑(fiber f x).toTop
⊢ (ConcreteCategory.hom (X.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) y ≫ sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (LightProfinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom
        (X.map
          (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) y ≫ CompHausLike.isTerminalPUnit.from (fiber f x)).op))
      (Function.Fiber.image (⇑f) x)

Tactic:
show (LightProfinite.of PUnit.{u + 1}).const y ≫
    IsTerminal.from _ (fiber.{u, u} f x) = 𝟙 _ from rfl

Goal state after:
case e_a
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj
      (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
this : Finite ↑(fiber f x).toTop
y : ↑(fiber f x).toTop
⊢ (ConcreteCategory.hom (X.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) y ≫ sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (LightProfinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (𝟙 (LightProfinite.of PUnit.{u + 1})).op)) (Function.Fiber.image (⇑f) x)
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case succ.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j : ℕ
ih : j + 1 ≤ j → approx (⇑f) (j + 1) ≤ approx (⇑f) j
⊢ approx (⇑f) (j + 1) ≤ approx (⇑f) (j + 1)

pp: case succ.step
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih : i ≤ j → approx (⇑f) i ≤ approx (⇑f) j
a✝ : i.le j
⊢ approx (⇑f) i ≤ approx (⇑f) (j + 1)

Tactic:
· exact le_rfl

Goal state after:
case succ.step
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih : i ≤ j → approx (⇑f) i ≤ approx (⇑f) j
a✝ : i.le j
⊢ approx (⇑f) i ≤ approx (⇑f) (j + 1)
Module: Mathlib.Control.Monad.Writer

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ γ✝ : Type u
x✝² : WriterT ω M α✝
x✝¹ : α✝ → WriterT ω M β✝
x✝ : β✝ → WriterT ω M γ✝
⊢ x✝² >>= x✝¹ >>= x✝ = x✝² >>= fun x ↦ x✝¹ x >>= x✝

Tactic:
by ext; simp [mul_assoc]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1
f : β nilFun
g : Fin2.elim0 ⟹ Fin2.elim0
this : g = nilFun
⊢ β g

Tactic:
rwa [this]

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)
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
case : i ≤ j
⊢ y = b

Tactic:
replace hh := approx_mono f case _ _ hh

Goal state after:
α✝ : Type u_1
β✝ : α✝ → Type u_2
f✝ : ((a : α✝) → Part (β✝ a)) →o (a : α✝) → Part (β✝ a)
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i j : ℕ
h₁ : y ∈ approx (⇑f) j a
case : i ≤ j
hh : b ∈ approx (⇑f) j a
⊢ y = b
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u} n
i : Fin2 n
x : α i
⊢ (subtypeVal α.repeatEq ⊚ diagSub) i x = prod.diag i x

Tactic:
induction i with
  | fz => simp only [comp, subtypeVal, diagSub, prod.diag]
  | fs _ i_ih => apply @i_ih (drop α)

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
⊢ (monotoneUncurry α β γ) (ωSup c) = ωSup (c.map (monotoneUncurry α β γ))

Tactic:
ext ⟨x, y⟩

Goal state after:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ (monotoneUncurry α β γ) (ωSup c) ⟨x, y⟩ = ωSup (c.map (monotoneUncurry α β γ)) ⟨x, y⟩
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: 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
⊢ Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))

Tactic:
CompHausLike.mono_iff_injective

Goal state after:
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
⊢ Function.Injective ⇑(ConcreteCategory.hom (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞})))
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case pos
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

Tactic:
rw [h']
    simp only [take, update_self]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case refine_2
α : Type u
β : α → Type v
γ : Type ?u.32
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ s.entries.NodupKeys →
    (Quotient.liftOn s.entries (fun l ↦ { Dom := l.NodupKeys, get := fun nd ↦ f { entries := l, nodupKeys := nd } })
        ⋯).Dom

Tactic:
rcases s.entries with ⟨l⟩

Goal state after:
case refine_2.mk
α : Type u
β : α → Type v
γ : Type ?u.32
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
x✝ : Multiset (Sigma β)
l : List (Sigma β)
⊢ Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) l) →
    (Quotient.liftOn (Quot.mk (⇑(isSetoid (Sigma β))) l)
        (fun l ↦ { Dom := l.NodupKeys, get := fun nd ↦ f { entries := l, nodupKeys := nd } }) ⋯).Dom
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

Tactic:
simp only [ne_eq, h, not_false_iff, lookupAll_cons_ne]
      exact (lookupAll_sublist a l).cons _

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ replace a b ⟦s⟧ = ⟦AList.replace a b s⟧

Tactic:
simp [replace]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝), (x✝³ && f x✝² x✝¹ && f x✝ b₂) = (x✝³ && f x✝ b₂ && f x✝² x✝¹)

Tactic:
simp_rw [Bool.and_assoc, Bool.and_comm, imp_true_iff]

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

Tactic:
by_cases e : a = hd.1

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys
e : a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys
e : ¬a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
Module: Mathlib.Data.Finset.PiInduction

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

Tactic:
apply notMem_erase

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : (b, m) ∈ f.graph.toList
n : M
hc : (b, n) ∈ f.graph.toList
⊢ (b, m) = (b, n)

Tactic:
rw [Finset.mem_toList, Finsupp.mem_graph_iff] at hb hc

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : f (b, m).1 = (b, m).2 ∧ (b, m).2 ≠ 0
n : M
hc : f (b, n).1 = (b, n).2 ∧ (b, n).2 ≠ 0
⊢ (b, m) = (b, n)
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
m : M
⊢ (insert a m l).lookupFinsupp = l.lookupFinsupp.update a m

Tactic:
by
  ext b
  by_cases h : b = a <;> simp [h]

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:
by
  induction s using Quot.inductionOn with | _ a
  obtain ⟨l, hl, hd⟩ := hs
  suffices a.Pairwise (_root_.Disjoint on Finsupp.support) by
    convert! List.support_sum_eq a this
    simp only [quot_mk_to_coe'', map_coe, sup_coe,
      Finset.sup_eq_union, Finset.bot_eq_empty, List.foldr_map]
  simp only [Multiset.quot_mk_to_coe'', Multiset.coe_eq_coe] at hl
  exact hl.symm.pairwise hd fun h ↦ _root_.Disjoint.symm h

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

Goal state before:
pp: α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝ : Semiring β
r : β
f : α → β
m : α →₀ β
⊢ (r • f) • m = r • f • m

Tactic:
by ext; simp [mul_assoc]

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

Goal state before:
pp: case mpr
a b r q : ℤ
h : b ≠ 0
⊢ r + b * q = a ∧ 0 ≤ r ∧ r < |b| → a / b = q ∧ a % b = r

Tactic:
intro ⟨rfl, hz, hb⟩

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

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

Tactic:
Ioc_filter_dvd_eq _ _ hr,

Goal state after:
a b r : ℤ
hr : 0 < r
⊢ ↑(#(map { toFun := fun x ↦ x * r, inj' := ⋯ } (Ioc ⌊↑a / ↑r⌋ ⌊↑b / ↑r⌋))) = max (⌊↑b / ↑r⌋ - ⌊↑a / ↑r⌋) 0
Module: Mathlib.Data.List.Indexes

Goal state before:
pp: case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
⊢ (do
      f arr.size head
      mapIdxMAux' f (arr.size + 1) tail) =
    do
    let x ← f arr.size head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)

Tactic:
generalize (f (Array.size arr) head) = head

Goal state after:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
⊢ (do
      head
      mapIdxMAux' f (arr.size + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝¹ = n✝

Tactic:
refine IH hx.right ?_ ?_ h

Goal state after:
case cons.succ.succ.refine_1
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝¹ ∈ {n | n ≤ tl.length}

case cons.succ.succ.refine_2
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝ ∈ {n | n ≤ tl.length}
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : 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₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)

Tactic:
refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩

Goal state after:
case refine_1
α : 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
⊢ Z₂ + (Z₁ - Y₂) ≠ ∅

case refine_2
α : 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₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))

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
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))

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
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N P : Multiset α
⊢ M.IsDershowitzMannaLT N → N.IsDershowitzMannaLT P → M.IsDershowitzMannaLT P

Tactic:
rintro ⟨X₁, Y₁, Z₁, -, rfl, rfl, hYZ₁⟩ ⟨X₂, Y₂, Z₂, hZ₂, hXZXY, rfl, hYZ₂⟩
  rw [add_comm X₁, add_comm X₂] at hXZXY
  refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
  · simpa [-not_and, not_and_or] using .inl hZ₂
  · rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]
  · rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]
    rwa [eq_comm]
  simp only [mem_add, or_imp, forall_and]
  refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
    by_cases z_in : z ∈ Y₂
    · obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
      exact ⟨w, .inl hw, hyz.trans hzw⟩
    · exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy
    exact ⟨z, .inl hz, hyz⟩

Goal state after: