mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: case g
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) := ⋯
s : Cone (empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ s.pt.left ⟶ (asEmptyCone x).pt.left

Tactic:
change op (unop _) ⟶ op (⟨_, H⟩ : Opens _)

Goal state after:
case g
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) := CostructuredArrow.mk (homOfLE ⋯).op
s : Cone (empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ op (unop s.pt.1) ⟶ op { carrier := ⇑(ConcreteCategory.hom f) '' ↑U, is_open' := H }
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ h.functor.IsContinuous (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y)

Tactic:
apply Functor.isContinuous_of_coverPreserving
  · exact h.compatiblePreserving
  · exact h.isOpenMap.coverPreserving

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
h : F.IsSheafPreservesLimitPairwiseIntersections
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (Functor.mapCone F (Pairwise.cocone U).op))

Tactic:
have := h U

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
h : F.IsSheafPreservesLimitPairwiseIntersections
ι : Type w
U : ι → Opens ↑X
this : PreservesLimit (Pairwise.diagram U).op F
⊢ Nonempty (IsLimit (Functor.mapCone F (Pairwise.cocone U).op))
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ ⋯.some.lift
        { pt := s.pt,
          π :=
            {
              app := fun X_1 ↦
                Opposite.casesOn X_1 fun unop ↦
                  Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd)
                    fun a a_1 ↦
                    ULift.casesOn a fun down ↦
                      WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op),
              naturality := ⋯ } } ≫
      F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    s.snd

Tactic:
exact
    (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <|
      op <| Pairwise.single <| ULift.up WalkingPair.right

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r : ↑(RingCat.FilteredColimits.colimit R)
⊢ ∀ (a : (j : C) × (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a • 0 = 0

Tactic:
by
    rintro ⟨U, a⟩
    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ (𝟙 _) (rightToMax _ _) ?_
    dsimp
    simp only [map_zero, smul_zero]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S✝
inst✝⁹ : Ring R
inst✝⁸ : Ring S✝
A : Type u_3
inst✝⁷ : AddCommGroup A
inst✝⁶ : Module R A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsModuleTopology R A
B : Type u_4
inst✝³ : AddCommGroup B
inst✝² : Module R B
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S✝ B'
S : Submodule R A
⊢ QuotientModule.Quotient.topologicalSpace S = moduleTopology R (A ⧸ S)

Tactic:
have := toContinuousAdd R A

Goal state after:
R : Type u_1
S✝ : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S✝
inst✝⁹ : Ring R
inst✝⁸ : Ring S✝
A : Type u_3
inst✝⁷ : AddCommGroup A
inst✝⁶ : Module R A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsModuleTopology R A
B : Type u_4
inst✝³ : AddCommGroup B
inst✝² : Module R B
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S✝ B'
S : Submodule R A
this : ContinuousAdd A
⊢ QuotientModule.Quotient.topologicalSpace S = moduleTopology R (A ⧸ S)
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
c : Cone F
hc : IsLimit c
⊢ IsIso (c.π.app i₀)

Tactic:
simp only [← IsLimit.conePointUniqueUpToIso_hom_comp hc h.isLimitCone i₀,
    cone_π_app, coneπApp_eq_id, cone_pt, comp_id]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map β = F.map α ≫ 𝟙 (F.obj j')

Tactic:
comp_id,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map β = F.map α
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
s : Cocone F
m : h.cocone.pt ⟶ s.pt
hm : ∀ (j : J), h.cocone.ι.app j ≫ m = s.ι.app j
⊢ m = s.ι.app i₀

Tactic:
simp only [← hm i₀, cocone_ι_app, coconeιApp_eq_id, id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : ι × ι → J₁
b : (i : ι × ι) → l ⟶ m i
hb : ∀ (a_1 b_1 : ι), f a_1 ≫ a ≫ F.map (b (a_1, b_1)) = f b_1 ≫ a ≫ F.map (b (a_1, b_1))
n : J₁
c : (i : ι × ι) → m i ⟶ n
d : l ⟶ n
hn : ∀ (i : ι × ι), b i ≫ c i = d
i₀ : ι := Classical.arbitrary ι
i : ι
⊢ f i ≫ a ≫ F.map (b (i₀, i)) ≫ F.map (c (i₀, i)) = f i₀ ≫ a ≫ F.map (b (i₀, i)) ≫ F.map (c (i₀, i))

Tactic:
reassoc_of% (hb i₀ i)

Goal state after:
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : ι × ι → J₁
b : (i : ι × ι) → l ⟶ m i
hb : ∀ (a_1 b_1 : ι), f a_1 ≫ a ≫ F.map (b (a_1, b_1)) = f b_1 ≫ a ≫ F.map (b (a_1, b_1))
n : J₁
c : (i : ι × ι) → m i ⟶ n
d : l ⟶ n
hn : ∀ (i : ι × ι), b i ≫ c i = d
i₀ : ι := Classical.arbitrary ι
i : ι
⊢ f i ≫ a ≫ F.map (b (i₀, i)) ≫ F.map (c (i₀, i)) = f i ≫ a ≫ F.map (b (i₀, i)) ≫ F.map (c (i₀, i))
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
⊢ ∃ k hik hjk, a ≫ F.map hik = b ≫ F.map hjk

Tactic:
refine ⟨c'.pt, c'.ι.app (.left (.inl .unit)), c'.ι.app (.left (.inr .unit)), ?_⟩

Goal state after:
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
⊢ a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ()))) =
    b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ())))
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
j : Fin n → J
x : (i : Fin n) → (fun X ↦ X) ((F ⋙ forget CommRingCat).obj (j i))
h :
  ∀ (i : Fin n),
    (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app (j i))) (x i) =
      (ConcreteCategory.hom (π ≫ g)) (MvPolynomial.X i)
this : ∃ i, ∀ (a : Fin n), Nonempty (j a ⟶ i)
⊢ ∃ i, Nonempty ((a : Fin n) → j a ⟶ i)

Tactic:
simpa [← exists_true_iff_nonempty, Classical.skolem, -exists_const_iff] using! this

Goal state after:
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring A
f : R →+* A
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP A q
⊢ ↑p = 0

Tactic:
← map_natCast f p,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring A
f : R →+* A
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP A q
⊢ f ↑p = 0
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
f : L →ₐ[K] L'
a₁✝ a₂✝ : IntermediateField K L
h : (map f a₁✝).toSubalgebra = (map f a₂✝).toSubalgebra
⊢ a₁✝ = a₂✝

Tactic:
toSubalgebra_map,

Goal state after:
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
f : L →ₐ[K] L'
a₁✝ a₂✝ : IntermediateField K L
h : Subalgebra.map f a₁✝.toSubalgebra = (map f a₂✝).toSubalgebra
⊢ a₁✝ = a₂✝
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
f : L →ₐ[K] L'
a₁✝ a₂✝ : IntermediateField K L
h : Subalgebra.map f a₁✝.toSubalgebra = (map f a₂✝).toSubalgebra
⊢ a₁✝ = a₂✝

Tactic:
toSubalgebra_map,

Goal state after:
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
f : L →ₐ[K] L'
a₁✝ a₂✝ : IntermediateField K L
h : Subalgebra.map f a₁✝.toSubalgebra = Subalgebra.map f a₂✝.toSubalgebra
⊢ a₁✝ = a₂✝
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: F : Type u_4
inst✝⁴ : Field F
E : Type u_5
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
⊢ (f.comp L.val).fieldRange.toSubalgebra = (map f L).toSubalgebra

Tactic:
toSubalgebra_map,

Goal state after:
F : Type u_4
inst✝⁴ : Field F
E : Type u_5
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
⊢ (f.comp L.val).fieldRange.toSubalgebra = Subalgebra.map f L.toSubalgebra
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ Nonempty (Algebra ℚ R) ↔ ∀ p > 0, ¬MixedCharZero R p

Tactic:
rw [← EqualCharZero.iff_not_mixedCharZero]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ Nonempty (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : f b = none
⊢ corec f b = nil

Tactic:
apply destruct_eq_none
  simp [h]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a ∈ s

Tactic:
rw [get_succ, tail_cons] at h

Goal state after:
case succ
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = s.get n'
⊢ a ∈ s
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
x : α
s : Seq α
⊢ (cons x s).Terminates ↔ s.Terminates

Tactic:
constructor <;> intro ⟨n, h⟩
  · exact ⟨n, cons_terminatedAt_succ_iff.mp (terminated_stable _ (Nat.le_succ _) h)⟩
  · exact ⟨n + 1, cons_terminatedAt_succ_iff.mpr h⟩

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
h : s.Terminates
a : α
p : s ~> a
⊢ a ∈ s

Tactic:
obtain ⟨a', h⟩ := h

Goal state after:
α : Type u
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a ∈ s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case a.succ
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (s.think.val (n + 1)).isSome = true
⊢ (s.val n).isSome = true

Tactic:
apply this

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ s.inits.get n = take n.succ s

Tactic:
induction n generalizing s with
  | zero => rfl
  | succ n ih => rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ s.bind (pure ∘ f)

Tactic:
apply mem_bind m

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ (pure ∘ f) a
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ nil.drop n = nil

Tactic:
by
  induction n with
  | zero => simp [drop]
  | succ m ih => simp [← dropn_tail, ih]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case inr
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = (s.set n x).get? m
h_nm : n ≠ m
⊢ p y

Tactic:
get?_set_of_ne _ _ h_nm.symm

Goal state after:
case inr
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = s.get? m
h_nm : n ≠ m
⊢ p y
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
five_le_n : 5 ≤ n
⊢ n ≤ fib n

Tactic:
induction five_le_n with

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

Goal state before:
pp: case inr
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred.succ + m)) = (fib m).gcd (fib n.pred.succ)

Tactic:
succ_eq_add_one

Goal state after:
case inr
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + 1))
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
⊢ (g.squashGCF (n + 1)).s.get? m = g.s.get? m

Tactic:
simp only [squashGCF, squashSeq_nth_of_lt m_lt_n]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case succ.succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)

Tactic:
have m'_lt_n : m'' + 1 < n' + 1 := m_le_n
            have succ_m''th_contsAux_eq := IH (m'' + 1) (lt_add_one (m'' + 1)) m'_lt_n.le
            have : m'' < m'' + 2 := lt_add_of_pos_right m'' zero_lt_two
            have m''th_contsAux_eq := IH m'' this (le_trans this.le m_le_n)
            have : (squashGCF g (n' + 1)).s.get? m'' = g.s.get? m'' :=
              squashGCF_nth_of_lt (Nat.succ_lt_succ_iff.mp m'_lt_n)
            simp [contsAux, succ_m''th_contsAux_eq, m''th_contsAux_eq, this]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Idempotents

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
x : R
i : I
⊢ ↑(((decompose V) x) i) = ↑((x • (decompose V) 1) i)

Tactic:
← decompose_smul,

Goal state after:
R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
x : R
i : I
⊢ ↑(((decompose V) x) i) = ↑(((decompose V) (x • 1)) i)
Module: Mathlib.Algebra.DirectSum.Idempotents

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
x : R
i : I
⊢ ↑(((decompose V) x) i) = x * idempotent V i

Tactic:
by
  rw [← smul_eq_mul (a := x), idempotent, ← Submodule.coe_smul, ← smul_apply, ← decompose_smul,
    smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.b ^ 2 * φ P.c ^ 2 - 4 * φ P.a * φ P.c ^ 3 - 4 * φ P.b ^ 3 * φ P.d - 27 * φ P.a ^ 2 * φ P.d ^ 2 +
      18 * φ P.a * φ P.b * φ P.c * φ P.d =
    (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2

Tactic:
rw [b_eq_three_roots ha h3, c_eq_three_roots ha h3, d_eq_three_roots ha h3]

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (φ P.a * -(x + y + z)) ^ 2 * (φ P.a * (x * y + x * z + y * z)) ^ 2 -
            4 * φ P.a * (φ P.a * (x * y + x * z + y * z)) ^ 3 -
          4 * (φ P.a * -(x + y + z)) ^ 3 * (φ P.a * -(x * y * z)) -
        27 * φ P.a ^ 2 * (φ P.a * -(x * y * z)) ^ 2 +
      18 * φ P.a * (φ P.a * -(x + y + z)) * (φ P.a * (x * y + x * z + y * z)) * (φ P.a * -(x * y * z)) =
    (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
w✝ x✝ y✝ z✝ : R
h₁ : ∀ (i j : n), c (single i j w✝) (single i j x✝)
h₂ : ∀ (i j : n), c (single i j y✝) (single i j z✝)
i j : n
⊢ c (single i j (w✝ * y✝)) (single i j (x✝ * z✝))

Tactic:
simpa using c.mul (h₁ i i) (h₂ i j)

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

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
⊢ r ∈ ↑(equivMatrix.symm I) → r ∈ {x | ∃ N ∈ I, N i j = x}

Tactic:
intro h
    exact ⟨single i j r, by simpa using! h i j, by simp⟩

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

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
⊢ I ≤ J → matrix n I ≤ matrix n J

Tactic:
· intro IJ M MI i j
      exact IJ <| MI i j

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
⊢ (trace R M) f = ((toMatrix b b) f).trace

Tactic:
classical
  rw [trace_eq_matrix_trace_of_finset R b.reindexFinsetRange, ← traceAux_def, ← traceAux_def,
    traceAux_eq R b b.reindexFinsetRange]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R M
⊢ trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquivOfBasis b).symm

Tactic:
simp [LinearEquiv.eq_comp_toLinearMap_symm, trace_eq_contract_of_basis b]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
l : ℕ
⊢ ((LinearMap.restrict f hfp - LinearMap.restrict (μ • 1) ⋯) ^ l).ker = Submodule.comap p.subtype ((f - μ • 1) ^ l).ker

Tactic:
LinearMap.restrict_sub hfp,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
l : ℕ
⊢ ((f - μ • 1).restrict ⋯ ^ l).ker = Submodule.comap p.subtype ((f - μ • 1) ^ l).ker
Module: Mathlib.Algebra.Field.NegOnePow

Goal state before:
pp: K : Type u_1
n : ℤ
inst✝ : DivisionRing K
⊢ ↑↑n.negOnePow = (-1) ^ n

Tactic:
rcases even_or_odd' n with ⟨k, rfl | rfl⟩

Goal state after:
case inl
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k).negOnePow = (-1) ^ (2 * k)

case inr
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = (-1) ^ (2 * k + 1)
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
f : α → β
x✝ : FreeSemigroup α
x : α
y : FreeSemigroup α
hx : ((map f) (of x)).length = (of x).length
hy : ((map f) y).length = y.length
⊢ ((map f) (of x * y)).length = (of x * y).length

Tactic:
simp only [map_mul, length_mul, *]

Goal state after: