mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
K✝ : J ⥤ CostructuredArrow K B
c✝ : Cone K✝
hc : IsLimit c✝
x✝¹ : Cone (K✝ ⋙ proj K B)
x✝ : J
⊢ (proj K B).map (hc.lift (CreatesConnected.raiseCone x✝¹) ≫ c✝.π.app x✝) = x✝¹.π.app x✝

Tactic:
hc.fac,

Goal state after:
J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
K✝ : J ⥤ CostructuredArrow K B
c✝ : Cone K✝
hc : IsLimit c✝
x✝¹ : Cone (K✝ ⋙ proj K B)
x✝ : J
⊢ (proj K B).map ((CreatesConnected.raiseCone x✝¹).π.app x✝) = x✝¹.π.app x✝
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ ((overEquiv Y₁) (pullback f S)).arrows g ↔ (pullback (Over.Hom.left f) ((overEquiv Y₂) S)).arrows g

Tactic:
dsimp [overEquiv, Presieve.functorPushforward]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1) ↔
    ∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
m : Mono 0
h : IsIso 0
j : 0 ≫ i.hom ≠ 0
⊢ False

Tactic:
simp at j

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
⊢ HasBinaryProducts α

Tactic:
have : ∀ x y : α, HasLimit (pair x y) := by
    let := hasFiniteLimits_of_hasFiniteLimits_of_size.{u} α
    infer_instance
  apply hasBinaryProducts_of_hasLimit_pair

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

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

Tactic:
exact h.compatiblePreserving

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

Goal state before:
pp: case single.pair
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ List.IsChain Zag
    [{ left := { as := PUnit.unit }, right := single i, hom := a },
      { left := { as := PUnit.unit }, right := Pairwise.pair i' i, hom := ObjectProperty.homMk (homOfLE ⋯) },
      { left := { as := PUnit.unit }, right := single i', hom := ObjectProperty.homMk (homOfLE ⋯) },
      { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }]

Tactic:
exact
          List.IsChain.cons_cons
            (Or.inr
              ⟨{  left := 𝟙 _
                  right := right i' i }⟩)
            (List.IsChain.cons_cons
              (Or.inl
                ⟨{  left := 𝟙 _
                    right := left i' i }⟩)
              (List.IsChain.cons_cons
                (Or.inr
                  ⟨{  left := 𝟙 _
                      right := left i' j' }⟩)
                (List.IsChain.singleton _)))

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

Goal state before:
pp: case refine_2
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)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ ∀ ⦃X_1 Y : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ⦄ (f : X_1 ⟶ Y),
    (((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).map f ≫
        Opposite.casesOn Y 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)) =
      (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)) ≫
        ((Pairwise.diagram ι).op ⋙ F.presheaf).map f

Tactic:
rintro ⟨i⟩ ⟨j⟩ f

Goal state after:
case refine_2
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)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
i j : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)
f : op i ⟶ op j
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).map f ≫
      Opposite.casesOn (op j) 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)) =
    (Opposite.casesOn (op i) 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)) ≫
      ((Pairwise.diagram ι).op ⋙ F.presheaf).map f
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
⊢ closure[Pi.topologicalSpace] ↑(⨆ i, map (LinearMap.single R M i) (s i)) = Set.univ.pi fun i ↦ closure[inst✝¹ i] ↑(s i)

Tactic:
rw [← closure_pi_set]
  refine (closure_mono ?_).antisymm <| closure_minimal ?_ isClosed_closure
  · exact SetLike.coe_mono <| iSup_map_single_le
  · simp only [Set.subset_def, mem_closure_iff]
    intro x hx U hU hxU
    rcases isOpen_pi_iff.mp hU x hxU with ⟨t, V, hV, hVU⟩
    refine ⟨∑ i ∈ t, Pi.single i (x i), hVU ?_, ?_⟩
    · simp_all [Finset.sum_pi_single]
    · exact sum_mem fun i hi ↦ mem_iSup_of_mem i <| mem_map_of_mem <| hx _ <| Set.mem_univ _

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
t : CC (G.obj.obj (op U))
x : ↑X
hx : x ∈ U
s₀ : CC ((stalkFunctor C x).obj F.obj)
hs₀ : (ConcreteCategory.hom ((stalkFunctor C x).map f.hom)) s₀ = (ConcreteCategory.hom (G.presheaf.germ U x hx)) t
⊢ ∃ V, ∃ (_ : x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t

Tactic:
obtain ⟨V₁, hxV₁, s₁, rfl⟩ := F.presheaf.exists_germ_eq s₀

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
t : CC (G.obj.obj (op U))
x : ↑X
hx : x ∈ U
V₁ : Opens ↑X
hxV₁ : x ∈ V₁
s₁ : ToType (F.presheaf.obj (op V₁))
hs₀ :
  (ConcreteCategory.hom ((stalkFunctor C x).map f.hom)) ((ConcreteCategory.hom (F.presheaf.germ V₁ x hxV₁)) s₁) =
    (ConcreteCategory.hom (G.presheaf.germ U x hx)) t
⊢ ∃ V, ∃ (_ : x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ ↑T⁻¹ (↑T x) = x

Tactic:
by rw [← mul_apply_eq_comp, Units.inv_mul, one_apply_eq_self]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
hF' : Topology.IsEmbedding ⇑(ConcreteCategory.hom F)
⊢ IsHomeomorph ⇑(ConcreteCategory.hom ((forget₂ (TopModuleCat R) TopCat).map F))

Tactic:
isHomeomorph_iff_isEmbedding_surjective

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
hF' : Topology.IsEmbedding ⇑(ConcreteCategory.hom F)
⊢ Topology.IsEmbedding ⇑(ConcreteCategory.hom ((forget₂ (TopModuleCat R) TopCat).map F)) ∧
    Function.Surjective ⇑(ConcreteCategory.hom ((forget₂ (TopModuleCat R) TopCat).map F))
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case mp
J : Type u
inst✝ : Category.{v, u} J
a✝ : IsCardinalFiltered J Cardinal.aleph0
⊢ IsFiltered J

Tactic:
exact isFiltered_of_isCardinalFiltered J Cardinal.aleph0

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

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
j₀ : J
A : Type w
x✝ : SmallCategory A
F : A ⥤ Under j₀
hA : HasCardinalLT (Arrow A) κ
this : IsFiltered J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
x : A → (j₀ ⟶ IsFiltered.max j₀ c.pt) := fun a ↦ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
hκ' : HasCardinalLT A κ
a : A
⊢ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ' =
    (((Functor.const A).obj (Under.mk (toCoeq x hκ'))).obj a).hom

Tactic:
simpa [x] using coeq_condition x hκ' a

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
s : S
x : N
⊢ (toSpanSingleton R N (s • x)).compLeft ι = (RingHom.id S) s • (toSpanSingleton R N x).compLeft ι

Tactic:
ext i j
    dsimp only [coe_comp, coe_single, Function.comp_apply, compLeft_apply, toSpanSingleton_apply,
      RingHom.id_apply, smul_apply, Pi.smul_apply]
    rw [← IsScalarTower.smul_assoc, _root_.Algebra.smul_def, mul_comm, mul_smul]
    simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_1
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 π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
⊢ ↑s ⊆ ↑(ker (CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none))))

Tactic:
intro r hr

Goal state after:
case refine_1
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 π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
r : ↑P
hr : r ∈ ↑s
⊢ r ∈ ↑(ker (CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none))))
Module: Mathlib.Algebra.CharP.CharAndCard

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R

Tactic:
have hch := CharP.cast_eq_zero R (ringChar R)
  have hp : p.Prime := Fact.out
  constructor
  · rintro h₁ ⟨q, hq⟩
    rcases IsUnit.exists_left_inv h₁ with ⟨a, ha⟩
    have h₃ : ¬ringChar R ∣ q := by
      rintro ⟨r, hr⟩
      rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq
      nth_rw 1 [← mul_one (ringChar R)] at hq
      exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩
    simp_all only [ne_eq]
    grind [ringChar.dvd]
  · intro h
    rcases (hp.coprime_iff_not_dvd.mpr h).isCoprime with ⟨a, b, hab⟩
    apply_fun ((↑) : ℤ → R) at hab
    push_cast at hab
    rw [hch, mul_zero, add_zero, mul_comm] at hab
    exact .of_mul_eq_one a hab

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

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
hp : Nat.Prime p
n : ℕ
⊢ IsUnit ↑↑n ↔ ¬↑p ∣ ↑n

Tactic:
simp [CharP.isUnit_natCast_iff hp, Int.ofNat_dvd]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
g : ↑a ∈ nonunits R
⊢ False

Tactic:
rw [← IsLocalRing.mem_maximalIdeal] at g

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
g : ↑a ∈ IsLocalRing.maximalIdeal R
⊢ False
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
i : ℕ
⊢ (s.head :: s.tail) i = s i

Tactic:
cases i

Goal state after:
case zero
α : Type u
s : Stream' α
⊢ (s.head :: s.tail) 0 = s 0

case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ (s.head :: s.tail) (n✝ + 1) = s (n✝ + 1)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
n : ℕ
⊢ s.get n = t.get n

Tactic:
by rw [← get_succ_cons n _ x, h, get_succ_cons]

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

Goal state before:
pp: case zero
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
o : α ⊕ β
⊢ Stream'.corec' (Corec.f f) o 0 = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd 0 = some a'

Tactic:
change (Corec.f f o).1 = some a' → (Corec.f f (Corec.f f o).2).1 = some a'
    rcases o with _ | b <;> intro h
    · exact h
    unfold Corec.f at *; split <;> simp_all

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

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
⊢ s.Results a n

Tactic:
by
    let ⟨n', r, e⟩ := of_results_think h
    injection e with h'; rwa [h']

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
g : GenContFract K
n : ℕ
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.nums n * g.dens (n + 1) - g.dens n * g.nums (n + 1) = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
· exact determinant_aux <| Or.inr <| not_terminatedAt_n

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Seq α
⊢ (map f s).Terminates ↔ s.Terminates

Tactic:
by
  simp [Terminates]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
gp_n : Pair K
s_nth_eq : (of v).s.get? n = some gp_n
⊢ ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ ↑ifp.b = gp_n.b

Tactic:
obtain ⟨ifp, stream_succ_nth_eq, rfl⟩ :
      ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ Pair.mk 1 (ifp.b : K) = gp_n := by
    unfold of IntFractPair.seq1 at s_nth_eq
    simpa using s_nth_eq

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
s_nth_eq : (of v).s.get? n = some { a := 1, b := ↑ifp.b }
⊢ ∃ ifp_1, IntFractPair.stream v (n + 1) = some ifp_1 ∧ ↑ifp_1.b = { a := 1, b := ↑ifp.b }.b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ (s.drop n).head = s.get? n

Tactic:
induction n generalizing s with
  | zero => rfl
  | succ n IH => rw [← get?_tail, ← dropn_tail]; apply IH

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

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
x : α
s : Seq α
⊢ ((cons x s).drop (n + 1)).length' = (cons x s).length' - ↑(n + 1)

Tactic:
| cons x s =>

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

Goal state before:
pp: case bisim.nil.cons.cons
α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x✝ x : α
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join)
    (nil.append (Seq.cons ((x✝, Seq.cons x s), S) SS).join.join).destruct
    (nil.append (Seq.map join (Seq.cons ((x✝, Seq.cons x s), S) SS)).join).destruct

Tactic:
| cons x s =>

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:
pp: K : Type u_1
v : K
inst✝⁶ : Field K
inst✝⁵ : LinearOrder K
inst✝⁴ : IsStrictOrderedRing K
inst✝³ : FloorRing K
inst✝² : Archimedean K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
⊢ Filter.Tendsto (of v).convs Filter.atTop (𝓝 v)

Tactic:
simpa [LinearOrderedAddCommGroup.tendsto_nhds, abs_sub_comm] using of_convergence_epsilon v

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
ifp_n ifp_succ_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
this : ↑⌊ifp_n.fr⁻¹⌋ ≤ ifp_n.fr⁻¹
⊢ ↑ifp_succ_n.b ≤ ifp_n.fr⁻¹

Tactic:
by
    obtain ⟨_, ifp_n_fr⟩ := ifp_n
    have : ifp_n_fr ≠ 0 := by
      intro h
      simp [h, IntFractPair.stream, nth_stream_eq] at succ_nth_stream_eq
    have : IntFractPair.of ifp_n_fr⁻¹ = ifp_succ_n := by
      simpa [this, IntFractPair.stream, nth_stream_eq, Option.coe_def] using succ_nth_stream_eq
    rwa [← this]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 1
⊢ P.toPoly.Monic

Tactic:
nontriviality R
  rw [Monic, leadingCoeff_of_b_ne_zero ha (hb ▸ one_ne_zero), hb]

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.discr = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2

Tactic:
simp only [discr, RingHom.map_add, map_sub, map_mul, map_pow, map_ofNat]

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.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
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Subsingleton R
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0

pp: case inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0

Tactic:
· exact ⟨_, Subsingleton.elim _ _, rfl, Subsingleton.elim _ _⟩

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0