mathlib-initiative/mathlib-tactics huggingface dataset:
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 s : ↑(RingCat.FilteredColimits.colimit R)
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
⊢ ∀ (a b : (j : C) × (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j)
    (c : (j : C) × (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj j),
    (Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a +
          Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b) •
        Quot.mk
          (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel c =
      Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a •
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
            c +
        Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b •
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel c

Tactic:
by
    rintro ⟨U₁, a₁⟩ ⟨U₂, a₂⟩ ⟨V, b⟩
    obtain ⟨s, α, β, h₁, h₂, h₃, h₄⟩ := crown₄
      (rightToMax U₁ V ≫ leftToMax (max U₁ V) (max U₂ V)) (rightToMax (max U₁ U₂) V)
      (rightToMax U₂ V ≫ rightToMax (max U₁ V) (max U₂ V)) (rightToMax (max U₁ U₂) V)
      (leftToMax U₁ V ≫ leftToMax (max U₁ V) (max U₂ V))
      (leftToMax U₁ U₂ ≫ leftToMax (max U₁ U₂) V)
      (leftToMax U₂ V ≫ rightToMax (max U₁ V) (max U₂ V))
      (rightToMax U₁ U₂ ≫ leftToMax (max U₁ U₂) V)
    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ β α ?_
    dsimp
    simp only [add_smul, map_add, ← ConcreteCategory.comp_apply, ← Functor.map_comp, *]

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 : CokernelCofork φ
m : (CokernelCofork.ofπ (cokerπ φ) ⋯).pt ⟶ s.pt
h : cokerπ φ ≫ m = Cofork.π s
⊢ m = ofHom { toLinearMap := (↑(Hom.hom φ)).range.liftQ ↑(Hom.hom (Cofork.π s)) ⋯, cont := ⋯ }

Tactic:
← cancel_epi (cokerπ φ),

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
s : CokernelCofork φ
m : (CokernelCofork.ofπ (cokerπ φ) ⋯).pt ⟶ s.pt
h : cokerπ φ ≫ m = Cofork.π s
⊢ cokerπ φ ≫ m = cokerπ φ ≫ ofHom { toLinearMap := (↑(Hom.hom φ)).range.liftQ ↑(Hom.hom (Cofork.π s)) ⋯, cont := ⋯ }
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
⊢ PreservesFilteredColimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1} (Under.forget X)

Tactic:
by
  refine ⟨fun J hJ hJ' ↦ ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨.ofExistsUnique fun s ↦ ?_⟩⟩⟩⟩
  obtain i := Nonempty.some ((inferInstance : Nonempty J))
  let s' : Cocone F := ⟨Under.mk ((F.obj i).hom ≫ s.ι.app i), fun j ↦ Under.homMk (s.ι.app j) (by
    obtain ⟨k, hik, hjk, -⟩ := IsFilteredOrEmpty.cocone_objs i j
    simp only [Functor.const_obj_obj, Under.mk_right, Under.mk_hom,
      ← s.w hjk, ← s.w hik]
    simp), fun j k e ↦ by ext; simpa using s.w e⟩
  refine ⟨(hc.desc s').right, fun j ↦ congr($(hc.fac s' j).right), fun f hf ↦ ?_⟩
  dsimp at hf
  exact congr($(hc.uniq s' (Under.homMk f (by simp [s', ← hf]))
    fun j ↦ Under.UnderMorphism.ext (hf j)).right)

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

Goal state before:
pp: S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²² : Semiring R
inst✝²¹ : Semiring S
inst✝²⁰ : AddCommMonoid V
inst✝¹⁹ : Module R V
inst✝¹⁸ : TopologicalSpace V
inst✝¹⁷ : Module S V
inst✝¹⁶ : ContinuousConstSMul S V
inst✝¹⁵ : AddCommMonoid W
inst✝¹⁴ : Module R W
inst✝¹³ : TopologicalSpace W
inst✝¹² : Module S W
inst✝¹¹ : ContinuousConstSMul S W
inst✝¹⁰ : AddCommMonoid G
inst✝⁹ : Module R G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module S G
inst✝⁶ : ContinuousConstSMul S G
inst✝⁵ : SMulCommClass R S W
inst✝⁴ : SMul S R
inst✝³ : IsScalarTower S R V
inst✝² : IsScalarTower S R W
inst✝¹ : SMulCommClass R S V
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
x✝ : G
⊢ ((α • e).trans f) x✝ = (α • e.trans f) x✝

Tactic:
simp [LinearMapClass.map_smul_of_tower f]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
⊢ Finite (Arrow C) ↔ Nonempty (FinCategory C)

Tactic:
constructor
  · intro
    refine ⟨?_, fun a b ↦ ?_⟩
    · have := Finite.of_injective (fun (a : C) ↦ Arrow.mk (𝟙 a))
        (fun _ _ ↦ congr_arg Comma.left)
      apply Fintype.ofFinite
    · have := Finite.of_injective (fun (f : a ⟶ b) ↦ Arrow.mk f)
        (fun f g h ↦ by
          change (Arrow.mk f).hom = (Arrow.mk g).hom
          congr)
      apply Fintype.ofFinite
  · rintro ⟨_⟩
    have := Fintype.ofEquiv _ (Arrow.equivSigma C).symm
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, u} C
x✝ : Arrow (Shrink.{w, u} C)
⊢ ((Shrink.equivalence C).functor.mapArrow.obj ((Shrink.equivalence C).inverse.mapArrow.obj x✝)).hom =
    eqToHom ⋯ ≫ x✝.hom ≫ eqToHom ⋯

Tactic:
by simp; rfl

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
s : Cone F
m : s.pt ⟶ h.cone.pt
hm : ∀ (j : J), m ≫ h.cone.π.app j = s.π.app j
⊢ m = s.π.app i₀

Tactic:
simp only [← hm i₀, cone_π_app, coneπApp_eq_id, cone_pt, comp_id]

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

Goal state before:
pp: case h₁
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 := ⋯
D : MulticospanIndex J' J := ⋯
c' : Cocone D.multicospan
⊢ (CommRingCat.Hom.hom (a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ()))))).comp (CommRingCat.Hom.hom f) =
    (CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))).comp (CommRingCat.Hom.hom f)

Tactic:
rw [← CommRingCat.hom_comp, ← CommRingCat.hom_comp, reassoc_of% ha, reassoc_of% hb]
    simp [← α.naturality]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
N : Type u_4
inst✝³ : Semiring N
inst✝² : Algebra R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : ι → R
⊢ (piScalarRight R S N ι).symm ((algebraMap (ι → R) (ι → N)) x) = 1 ⊗ₜ[R] x

Tactic:
simp [Algebra.algebraMap_eq_smul_one, Pi.smul_def', LinearEquiv.symm_apply_eq,
    piScalarRight_apply, piScalarRightHom_tmul]

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

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
i j : J
f₁ : (F ⋙ coyoneda.obj (Opposite.op S)).obj i
⊢ ∀ (xj : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj j)),
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) f₁ =
        (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) f₁ =
          (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) xj

Tactic:
f₂

Goal state after:
case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
i j : J
f₁ : (F ⋙ coyoneda.obj (Opposite.op S)).obj i
f₂ : (F ⋙ coyoneda.obj (Opposite.op S)).obj j
⊢ (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) f₁ =
      (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) f₂ →
    ∃ k f g,
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) f₁ =
        (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) f₂
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesColimitsOfShape J L
inst✝ : HasColimitsOfShape J A
c : (D : J ⥤ T) → [HasColimit D] → Cocone D
hc : (D : J ⥤ T) → [inst : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasColimit D] {X : T} (s : D ⟶ (Functor.const J).obj X),
    (∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : (MorphismProperty.costructuredArrowObj L P).ColimitOfShape J Y
hd : IsColimit ((proj L X ⋙ L).mapCocone d.cocone) := isColimitOfPreserves (proj L X ⋙ L) d.isColimit
⊢ MorphismProperty.costructuredArrowObj L P Y

Tactic:
have heq : Y.hom = hd.desc { pt := X, ι := { app j := (d.diag.obj j).hom } } := by
      refine hd.hom_ext fun j ↦ ?_
      simp only [IsColimit.fac]
      simp

Goal state after:
T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesColimitsOfShape J L
inst✝ : HasColimitsOfShape J A
c : (D : J ⥤ T) → [HasColimit D] → Cocone D
hc : (D : J ⥤ T) → [inst : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasColimit D] {X : T} (s : D ⟶ (Functor.const J).obj X),
    (∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : (MorphismProperty.costructuredArrowObj L P).ColimitOfShape J Y
hd : IsColimit ((proj L X ⋙ L).mapCocone d.cocone) := isColimitOfPreserves (proj L X ⋙ L) d.isColimit
heq : Y.hom = hd.desc { pt := X, ι := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } }
⊢ MorphismProperty.costructuredArrowObj L P Y
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
⊢ hc.lift (pullbackConeEquivBinaryFan.inverse.obj s) ≫ (Over.mk (c.fst ≫ f)).hom = s.pt.hom

Tactic:
by
      simpa using! s.fst.w

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

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X✝ : T
inst✝³ : HasPullbacks T
inst✝² : P.IsMultiplicative
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
X Y : T
f : X ⟶ Y
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J (pullback P ⊤ f)

Tactic:
have : PreservesLimitsOfShape J
        (MorphismProperty.Over.pullback P ⊤ f ⋙ MorphismProperty.Over.forget _ _ _) :=
      inferInstanceAs <| PreservesLimitsOfShape J <|
        Over.forget _ _ _ ⋙ CategoryTheory.Over.pullback f

Goal state after:
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X✝ : T
inst✝³ : HasPullbacks T
inst✝² : P.IsMultiplicative
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
X Y : T
f : X ⟶ Y
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this : PreservesLimitsOfShape J (pullback P ⊤ f ⋙ Over.forget P ⊤ X)
⊢ PreservesLimitsOfShape J (pullback P ⊤ f)
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : NonAssocSemiring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this : Nontrivial R
⊢ CharP A p

Tactic:
have H := (CharP.char_is_prime_or_zero R p).resolve_right hp

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : NonAssocSemiring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this : Nontrivial R
H : Nat.Prime p
⊢ CharP A p
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
D : WalkingParallelPair ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
this :
  CreatesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
⊢ HasLimit D

Tactic:
exact hasLimit_of_created D (Under.forget _ _ R)

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Module.Flat R M
⊢ ∀ (x : ↥(((AlgebraTensorModule.lTensor S M) f).eqLocus ((AlgebraTensorModule.lTensor S M) g))),
    (((AlgebraTensorModule.lTensor S M) f).eqLocus ((AlgebraTensorModule.lTensor S M) g)).subtype x ∈
      ((AlgebraTensorModule.lTensor S M) (f.eqLocus g).subtype).range

Tactic:
by simp [Module.Flat.eqLocus_lTensor_eq]

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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
n : ℕ
h : n.Coprime p
⊢ ↑(n.gcdA p) * ↑n = 1

Tactic:
by rw [CharP.natCast_gcdA_mul_intCast_eq_gcd, h, Nat.cast_one]

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

Goal state before:
pp: ι : Type u
hi : Nonempty ι
R : Type v
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
x : ℕ
i : ι
h : ↑x = 0
j : ι
⊢ (Pi.evalRingHom (fun x ↦ R) j) ↑x = 0

Tactic:
map_natCast,

Goal state after:
ι : Type u
hi : Nonempty ι
R : Type v
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
x : ℕ
i : ι
h : ↑x = 0
j : ι
⊢ ↑x = 0
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → ∀ p > 0, MixedCharZero R p → P

Tactic:
· intro h q q_pos q_mixedChar
    rcases q_mixedChar.charP_quotient with ⟨I, hI_ne_top, _⟩
    -- Krull's Thm: There exists a prime ideal `P` such that `I ≤ P`
    rcases Ideal.exists_le_maximal I hI_ne_top with ⟨M, hM_max, h_IM⟩
    let r := ringChar (R ⧸ M)
    have r_pos : r ≠ 0 := by
      have q_zero :=
        congr_arg (Ideal.Quotient.factor h_IM) (CharP.cast_eq_zero (R ⧸ I) q)
      simp only [map_natCast, map_zero] at q_zero
      apply ne_zero_of_dvd_ne_zero (ne_of_gt q_pos)
      exact (CharP.cast_eq_zero_iff (R ⧸ M) r q).mp q_zero
    have r_prime : Nat.Prime r :=
      or_iff_not_imp_right.1 (CharP.char_is_prime_or_zero (R ⧸ M) r) r_pos
    apply h r r_prime
    have : CharZero R := q_mixedChar.toCharZero
    exact ⟨⟨M, hM_max.ne_top, ringChar.of_eq rfl⟩⟩

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
S : Subsemiring R
x : ℕ
h : ↑x = 0
⊢ S.subtype ↑x = 0

Tactic:
map_natCast,

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
S : Subsemiring R
x : ℕ
h : ↑x = 0
⊢ ↑x = 0
Module: Mathlib.Algebra.CharP.Subring

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
S : Subring R
x : ℕ
h : ↑x = 0
⊢ S.subtype ↑x = 0

Tactic:
map_natCast,

Goal state after:
R : Type u
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
S : Subring R
x : ℕ
h : ↑x = 0
⊢ ↑x = 0
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z : FreeCommRing ((i : ι) × G i)
⊢ (of G f (Classical.arbitrary ι)) (-1) =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      (-1)

Tactic:
by simp; rfl

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

Goal state before:
pp: case right
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail

Tactic:
exact ⟨tail s₂, by rw [interleave_eq, even_cons_cons, tail_cons]⟩

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

Goal state before:
pp: α : Type u
s : Stream' α
⊢ s.inits.tail = initsCore [s.head, s.tail.head] s.tail.tail

Tactic:
unfold inits

Goal state after:
α : Type u
s : Stream' α
⊢ (initsCore [s.head] s.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail
Module: Mathlib.Data.Seq.Basic

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

Tactic:
| cons _ u =>

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
x : FreeCommRing ((i : ι) × G i)
hx :
  x ∈
    {a |
      (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
        (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
          (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
            ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}
⊢ (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) x = 0

Tactic:
rcases hx with (⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩)

Goal state after:
case inl
ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
i j : ι
hij : i ≤ j
x : G i
⊢ (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) (FreeCommRing.of ⟨j, f i j hij x⟩ - FreeCommRing.of ⟨i, x⟩) = 0

case inr.inl
ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
i : ι
⊢ (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) (FreeCommRing.of ⟨i, 1⟩ - 1) = 0

case inr.inr.inl
ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
i : ι
x y : G i
⊢ (FreeCommRing.lift fun x ↦ (g x.fst) x.snd)
      (FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩)) =
    0

case inr.inr.inr
ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
i : ι
x y : G i
⊢ (FreeCommRing.lift fun x ↦ (g x.fst) x.snd)
      (FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩) =
    0
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f✝ : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f✝ i j hij x) = (g i) x
f'✝ f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i j : ι
h : i ≤ j
⊢ ((g₂ j).comp (g₁ j)).comp (f i j h) = (f'' i j h).comp ((g₂ i).comp (g₁ i))

Tactic:
by
      rw [RingHom.comp_assoc, hg₁ i, ← RingHom.comp_assoc, hg₂ i, RingHom.comp_assoc]

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
x : α
n : ℕ
hx : some x = tl.get? n
⊢ R hd x

Tactic:
simpa [← hx] using h 0 (n + 1) (by lia)

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq1 α
f : α → Seq1 β
g : β → Seq1 γ
⊢ (s.bind f).bind g = s.bind fun x ↦ (f x).bind g

Tactic:
obtain ⟨a, s⟩ := s
  simp only [bind, map_pair, map_join]
  rw [← map_comp]
  simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl]
  rw [map_comp _ join]
  generalize Seq.map (map g ∘ f) s = SS
  rcases map g (f a) with ⟨⟨a, s⟩, S⟩
  induction s using recOn with | nil => ?_ | cons x s_1 => ?_ <;>
  induction S using recOn with | nil => simp | cons x_1 s_2 => ?_
  · obtain ⟨x, t⟩ := x_1
    cases t <;> simp
  · obtain ⟨y, t⟩ := x_1; simp

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

Goal state before:
pp: K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminatedAt_succ_n : s.get? (n + 1) = none
⊢ squashSeq s n = s

Tactic:
cases s_nth_eq : s.get? n <;> simp only [*, squashSeq]

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

Goal state before:
pp: case some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val✝
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n :=
      s.ge_stable n.le_succ s_succ_nth_eq
    simp [*, squashSeq, m_lt_n.ne]

Goal state after: