mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.succ.bit1
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit1) >>> (n + 1)

pp: case pos.succ.bit0
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit0) >>> (n + 1)

Tactic:
· trans
    · apply IH
    change Nat.shiftRight m n = Nat.shiftRight (m + m + 1) (n + 1)
    rw [add_comm n 1, @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]
    apply congr_arg fun x => Nat.shiftRight x n
    simp [-add_assoc, Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, hdiv2]

Goal state after:
case pos.succ.bit0
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit0) >>> (n + 1)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.refine_1
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
e : M q T.head = some (q', s)
⊢ { l := some (Λ'.act s q'), var := (), Tape := T } ∈ TM1.step (tr M) { l := some (Λ'.normal q), var := (), Tape := T }

Tactic:
grind [TM1.step, TM1.stepAux, tr]

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

Goal state before:
pp: case some.refine_2
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
this :
  TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
e : M q T.head = some (q', s)
⊢ ReflTransGen (fun a b ↦ b ∈ TM1.step (tr M) a)
    { l := some (Λ'.normal q'), var := (),
      Tape :=
        match s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
    {
      l :=
        match
          match
            M q'
              (match s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T).head with
          | some val => true
          | none => false with
        | true => some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }

Tactic:
grind [TM1.step, TM1.stepAux, tr]

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst✝³] ↑s
hdir : Directed GE.ge fun s ↦ ↑s
⊢ ∃ s, ↑s ⊆ U

Tactic:
have h_nhds : ∀ y ∈ ⋂ s : N, s.val, U ∈ 𝓝 y := fun y y_in => by
        rw [hx, mem_singleton_iff] at y_in
        rwa [y_in]

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst✝³] ↑s
hdir : Directed GE.ge fun s ↦ ↑s
h_nhds : ∀ y ∈ ⋂ s, ↑s, U ∈ 𝓝 y
⊢ ∃ s, ↑s ⊆ U
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case case
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step (Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) v.headI) = do
    let v ← Nat.rec (f.eval v.tail) (fun y x ↦ g.eval (y :: v.tail)) v.headI
    eval step (Cfg.ret k v)

Tactic:
cases v.headI <;> simp only [Nat.rec_zero, Part.bind_eq_bind] <;> [apply IHf; apply IHg]

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

Goal state before:
pp: case e'_2
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a.succ = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) [] c d }
    { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
⊢ elim (trPosNum a.succ ++ [Γ'.cons]) [] c d =
    update (update (elim (l₂' ++ [Γ'.cons]) l₁' c d) rev []) main
      ((elim (l₂' ++ [Γ'.cons]) l₁' c d rev).reverseAux (elim (l₂' ++ [Γ'.cons]) l₁' c d main))

Tactic:
simp [e, List.reverseAux_eq]

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

Goal state before:
pp: case e'_2
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum a) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d }
    { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ elim (trPosNum a ++ Γ'.cons :: trList v) [] c d =
    update (update (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d) rev []) main
      ((elim (l₂' ++ Γ'.cons :: trList v) l₁' c d rev).reverseAux (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d main))

Tactic:
simp [e, List.reverseAux_eq]

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A : DiscreteQuotient X
B B' : DiscreteQuotient Y
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
⊢ ofLE h (map f cond a) = map f ⋯ a

Tactic:
rcases a with ⟨⟩

Goal state after:
case mk
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A : DiscreteQuotient X
B B' : DiscreteQuotient Y
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
a✝ : X
⊢ ofLE h (map f cond (Quot.mk (⇑A.toSetoid) a✝)) = map f ⋯ (Quot.mk (⇑A.toSetoid) a✝)
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
S : Cone F
x✝ : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = S.π.app j
⊢ x✝ =
    ConcreteCategory.ofHom
      (TopCat.Hom.hom
        ((CompHaus.limitConeIsLimit (F ⋙ lightProfiniteToCompHaus)).lift (lightProfiniteToCompHaus.mapCone S)).hom)

Tactic:
apply lightProfiniteToCompHaus.map_injective
    apply (CompHaus.limitConeIsLimit.{v, u} _).uniq (lightProfiniteToCompHaus.mapCone S)
    intro j
    simp [← h]
    rfl

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.AsLimit

Goal state before:
pp: S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ ⇑(ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(ConcreteCategory.hom (S.proj m)) =
    ⇑(ConcreteCategory.hom (S.proj n))

Tactic:
by
  rw [← S.proj_comp_transitionMapLE h]
  rfl

Goal state after:
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
⊢ IsIso ((LightCondensed.forget R).map ((discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj M)))

Tactic:
dsimp [LightCondensed.forget, discreteUnderlyingAdj]

Goal state after:
P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
⊢ IsIso
    ((sheafCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).map
      ((constantSheafAdj (coherentTopology LightProfinite) (ModuleCat R) isTerminalPUnit).counit.app
        ((functor R).obj M)))
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondMod R
x✝ : InternallyProjective P
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : P ⊗ (free R).obj S.toCondensed ⟶ B
h : isInternallyProjective P
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : ↑((P ⟹ A).obj.obj (Opposite.op S'))
hh :
  (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S'))) g' =
    (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op π))) ((ihomPoints R P B S).symm g)
⊢ P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = (ihomPoints R P A S') g' ≫ e

Tactic:
rw [ihom_map_val_app] at hh

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondMod R
x✝ : InternallyProjective P
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : P ⊗ (free R).obj S.toCondensed ⟶ B
h : isInternallyProjective P
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : ↑((P ⟹ A).obj.obj (Opposite.op S'))
hh :
  (ihomPoints R P B S').symm ((ihomPoints R P A S') g' ≫ e) =
    (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op π))) ((ihomPoints R P B S).symm g)
⊢ P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = (ihomPoints R P A S') g' ≫ e
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ sequence (Comp.mk <$> x) = Comp.mk (sequence <$> sequence x)

Tactic:
simp only [sequence, traverse_map, id_comp]; rw [← comp_traverse]; simp [map_id]

Goal state after:
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 (α ::: β)
⊢ f' rr n α ⊚ g' rr n α = TypeVec.id

Tactic:
ext i ⟨x, _⟩ : 2
    cases i <;> rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f = g

Tactic:
refine funext (fun x => ?_)
  cases x
  · apply h₁
  · apply congr_fun h₀

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ n : ℕ
β : (v : TypeVec.{?u.30} (n + 1)) → (v' : TypeVec.{?u.32} (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.30) →
    (t' : Type ?u.32) →
      (f : t → t') →
        (v : TypeVec.{?u.30} n) → (v' : TypeVec.{?u.32} n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
v : TypeVec.{?u.30} (n + 1)
v' : TypeVec.{?u.32} (n + 1)
fs : v.drop ::: v.last ⟹ v'.drop ::: v'.last
⊢ β (v.drop ::: v.last) (v'.drop ::: v'.last) (splitFun (dropFun fs) (lastFun fs))

Tactic:
apply F

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ n : ℕ
t : Type u_1
t' : Type u_2
v : TypeVec.{u_1} n
v' : TypeVec.{u_2} n
β : v ::: t ⟹ v' ::: t' → Sort u_3
F : (f : t → t') → (fs : v ⟹ v') → β (fs ::: f)
fs : v ::: t ⟹ v' ::: t'
⊢ β (splitFun (dropFun fs) (lastFun fs))

Tactic:
apply F

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr
α : 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
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
⊢ y = b

Tactic:
rcases le_total i j with H | H <;> [skip; symm] <;> apply_assumption <;> assumption

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

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
x✝⁴ : ApplicativeTransformation F✝ G✝
x✝³ x✝² : Type u
x✝¹ : x✝³ → F✝ x✝²
x✝ : t' x✝³
⊢ (fun {α} ↦ x✝⁴.app α) (Equiv.traverse eqv x✝¹ x✝) = traverse ((fun {α} ↦ x✝⁴.app α) ∘ x✝¹) x✝

Tactic:
Equiv.naturality,

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
x✝⁴ : ApplicativeTransformation F✝ G✝
x✝³ x✝² : Type u
x✝¹ : x✝³ → F✝ x✝²
x✝ : t' x✝³
⊢ Equiv.traverse eqv ((fun {α} ↦ x✝⁴.app α) ∘ x✝¹) x✝ = traverse ((fun {α} ↦ x✝⁴.app α) ∘ x✝¹) x✝
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: case h
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
a✝ : List α
⊢ traverse h (map g ⟦a✝⟧) = traverse (h ∘ g) ⟦a✝⟧

Tactic:
simp only [traverse, quot_mk_to_coe, map_coe, lift_coe, Function.comp_apply]

Goal state after:
case h
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
a✝ : List α
⊢ ofList <$> Traversable.traverse h (List.map g a✝) = ofList <$> Traversable.traverse (h ∘ g) a✝
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ s.biUnion ((fun f ↦ image f t) ∘ Prod.mk) = t.biUnion ((fun f ↦ image f s) ∘ fun b a ↦ (a, b))

Tactic:
change (s.biUnion fun a => t.image fun b => (a, b))
        = t.biUnion fun b => s.image fun a => (a, b)

Goal state after:
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ (s.biUnion fun a ↦ image (fun b ↦ (a, b)) t) = t.biUnion fun b ↦ image (fun a ↦ (a, b)) s
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ (s.biUnion fun a ↦ image (fun b ↦ (a, b)) t) = s ×ˢ t

Tactic:
product_eq_biUnion

Goal state after:
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ (s.biUnion fun a ↦ image (fun b ↦ (a, b)) t) = s.biUnion fun a ↦ image (fun b ↦ (a, b)) t
Module: Mathlib.Data.List.Sigma

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

Tactic:
apply this

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ dlookup a l.dedupKeys = dlookup a l

Tactic:
by
  induction l with
  | nil => rfl
  | cons l_hd _ l_ih =>
    obtain ⟨a', b⟩ := l_hd
    by_cases h : a = a'
    · subst a'
      rw [dedupKeys_cons, dlookup_kinsert, dlookup_cons_eq]
    · rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne]
      exact h

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ f.graph.toList.Nodup

Tactic:
apply Finset.nodup_toList

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)
⊢ s.sum.support ⊆ (map Finsupp.support s).sup

Tactic:
induction s using Quot.inductionOn

Goal state after:
case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a✝ : List (ι →₀ M)
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a✝)).support ⊆
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a✝)).sup
Module: Mathlib.Data.Finsupp.Sigma

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

Tactic:
simp [split_apply]

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₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.take.take * (y t.take.drop * z t.drop) = cast ⋯ (fun t ↦ x t.take * (y t.drop.take * z t.drop.drop)) t

Tactic:
← HolorIndex.take_take,

Goal state after:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.assocRight.take * (y t.take.drop * z t.drop) = cast ⋯ (fun t ↦ x t.take * (y t.drop.take * z t.drop.drop)) t
Module: Mathlib.Data.Holor

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

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

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| = r

Tactic:
emod_eq_of_lt hz hb

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

Goal state before:
pp: a b r v x : ℤ
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔ x ∈ map { toFun := fun x ↦ x + v, inj' := ⋯ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})

Tactic:
simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]

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

Goal state before:
pp: case neg
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
hp : ¬p hd = true
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true

Tactic:
· simp [hp]

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

Goal state before:
pp: case append_singleton.succ
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n✝ : ℕ
⊢ take ((xs ++ [x]).length - (n✝ + 1)) (xs ++ [x]) = (drop (n✝ + 1) (xs ++ [x]).reverse).reverse

Tactic:
simp [take_append, IH]

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ l.rdrop n = (drop n l.reverse).reverse

Tactic:
by
  rw [rdrop]
  induction l using List.reverseRecOn generalizing n with
  | nil => simp
  | append_singleton xs x IH =>
    cases n
    · simp [take_length_add_append]
    · simp [take_append, IH]

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

Goal state before:
pp: n m : ℕ
hnm : n < m
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico n m
⊢ decide (x✝¹ ≤ n) = decide (x✝¹ < n + 1)

Tactic:
by
    simpa using Nat.lt_succ_iff.symm

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

Goal state before:
pp: case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : (head :: tail).length = n.succ
⊢ Acc (Shortlex r) (head :: tail)

Tactic:
rw [List.length_cons, add_left_inj] at len_a

Goal state after:
case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
⊢ Acc (Shortlex r) (head :: tail)
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ (v ++ w)[j + u.length - u.length]? = v[j]?

pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ u.length ≤ j + u.length

Tactic:
Nat.add_sub_cancel,

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ (v ++ w)[j]? = v[j]?

α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ u.length ≤ j + u.length
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2
α : 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 = false
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l b [] ((a :: g).reverse :: gs))

Tactic:
apply IH
      · simpa using hgs'
      · rw [reverse_cons]
        apply isChain_cons.2 ⟨hga, hgs⟩
      · simpa

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

Goal state before:
pp: R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (of fun i j ↦ fst ((algebraMap R (Matrix n n (DualNumber R))) r i j),
      of fun i j ↦ snd ((algebraMap R (Matrix n n (DualNumber R))) r i j)) =
    (algebraMap R (DualNumber (Matrix n n R))) r

Tactic:
algebraMap_eq_inl',

Goal state after:
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (of fun i j ↦ fst ((algebraMap R (Matrix n n (DualNumber R))) r i j),
      of fun i j ↦ snd ((algebraMap R (Matrix n n (DualNumber R))) r i j)) =
    inl ((algebraMap R (Matrix n n R)) r)
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
⊢ ↑(↑(p ^ m) * (p ^ m).gcdA n + ↑n * (p ^ m).gcdB n) = ↑↑((p ^ m).gcd n)

Tactic:
Nat.gcd_eq_gcd_ab

Goal state after:
A : Type u_1
inst✝ : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : ↑p ^ m = 0
⊢ ↑(↑(p ^ m) * (p ^ m).gcdA n + ↑n * (p ^ m).gcdB n) = ↑(↑(p ^ m) * (p ^ m).gcdA n + ↑n * (p ^ m).gcdB n)
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a n : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k ↦ p ^ ((k + n - 1) / n)) =
    if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
split_ifs with h <;>
    simp [Finsupp.ceilDiv_def, prod_mapRange_index pow_zero, Nat.ceilDiv_eq_add_pred_div]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inr.inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
← factorization_le_iff_dvd ha (pow_ne_zero _ hb),

Goal state after:
case inr.inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization ≤ (b ^ n).factorization ↔ n.ceilRoot a ∣ b