mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: case refine_1
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 : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
⊢ ∀ (a : (j : C) × (R ⋙ forget RingCat).obj j) (b₁ b₂ : (j : C) × (M ⋙ forget Ab).obj j),
    (M ⋙ forget Ab).ColimitTypeRel b₁ b₂ →
      (M ⋙ forget Ab).ιColimitType (IsFiltered.max a.fst b₁.fst)
          ((ConcreteCategory.hom (R.map (leftToMax a.fst b₁.fst))) a.snd •
            (ConcreteCategory.hom (M.map (rightToMax a.fst b₁.fst))) b₁.snd) =
        (M ⋙ forget Ab).ιColimitType (IsFiltered.max a.fst b₂.fst)
          ((ConcreteCategory.hom (R.map (leftToMax a.fst b₂.fst))) a.snd •
            (ConcreteCategory.hom (M.map (rightToMax a.fst b₂.fst))) b₂.snd)

Tactic:
rintro ⟨U, a⟩ ⟨V₁, b₁⟩ ⟨V₂, b₂⟩ ⟨f : V₁ ⟶ V₂, rfl : b₂ = M.map _ b₁⟩

Goal state after:
case refine_1
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 : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
U : C
a : (R ⋙ forget RingCat).obj U
V₁ : C
b₁ : (M ⋙ forget Ab).obj V₁
V₂ : C
f : V₁ ⟶ V₂
⊢ (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨V₁, b₁⟩.snd) =
    (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst)))
          ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.snd)
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
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
V : C
b : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V
⊢ 0 •
      Quot.mk (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
        ⟨V, b⟩ =
    0

Tactic:
refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ (𝟙 _) (leftToMax _ _) ?_

Goal state after:
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
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
V : C
b : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V
⊢ (ConcreteCategory.hom ((M ⋙ forget Ab).map (𝟙 (IsFiltered.max ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.fst ⟨V, b⟩.fst))))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.fst ⟨V, b⟩.fst)))
          ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd) =
    (ConcreteCategory.hom ((M ⋙ forget Ab).map (leftToMax ⟨⋯.some, 0⟩.fst ⟨V, b⟩.fst))) ⟨⋯.some, 0⟩.snd
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✝ : Nontrivial M₁
e : 0 = 1
x : M₁
hx : x ≠ 0
⊢ x = 0

Tactic:
simpa using DFunLike.congr_fun e.symm x

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹⁸ : Semiring R
inst✝¹⁷ : Semiring S
inst✝¹⁶ : Semiring T
inst✝¹⁵ : Module R S
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : Module R M₂
inst✝¹² : Module S M₂
inst✝¹¹ : IsScalarTower R S M₂
inst✝¹⁰ : TopologicalSpace S
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : ContinuousSMul S M₂
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Module T M₂
inst✝² : ContinuousConstSMul T M₂
inst✝¹ : SMulCommClass R T M₂
inst✝ : SMulCommClass S T M₂
c : M →L[R] S
x y : M₂
⊢ c.smulRight (x + y) = c.smulRight x + c.smulRight y

Tactic:
ext e

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹⁸ : Semiring R
inst✝¹⁷ : Semiring S
inst✝¹⁶ : Semiring T
inst✝¹⁵ : Module R S
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : Module R M₂
inst✝¹² : Module S M₂
inst✝¹¹ : IsScalarTower R S M₂
inst✝¹⁰ : TopologicalSpace S
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : ContinuousSMul S M₂
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Module T M₂
inst✝² : ContinuousConstSMul T M₂
inst✝¹ : SMulCommClass R T M₂
inst✝ : SMulCommClass S T M₂
c : M →L[R] S
x y : M₂
e : M
⊢ (c.smulRight (x + y)) e = (c.smulRight x + c.smulRight y) e
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹⁸ : Semiring R
inst✝¹⁷ : Semiring S
inst✝¹⁶ : Semiring T
inst✝¹⁵ : Module R S
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : Module R M₂
inst✝¹² : Module S M₂
inst✝¹¹ : IsScalarTower R S M₂
inst✝¹⁰ : TopologicalSpace S
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : ContinuousSMul S M₂
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Module T M₂
inst✝² : ContinuousConstSMul T M₂
inst✝¹ : SMulCommClass R T M₂
inst✝ : SMulCommClass S T M₂
c : M →L[R] S
a : T
x : M₂
⊢ c.smulRight (a • x) = (RingHom.id T) a • c.smulRight x

Tactic:
ext e

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹⁸ : Semiring R
inst✝¹⁷ : Semiring S
inst✝¹⁶ : Semiring T
inst✝¹⁵ : Module R S
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : Module R M₂
inst✝¹² : Module S M₂
inst✝¹¹ : IsScalarTower R S M₂
inst✝¹⁰ : TopologicalSpace S
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : ContinuousSMul S M₂
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Module T M₂
inst✝² : ContinuousConstSMul T M₂
inst✝¹ : SMulCommClass R T M₂
inst✝ : SMulCommClass S T M₂
c : M →L[R] S
a : T
x : M₂
e : M
⊢ (c.smulRight (a • x)) e = ((RingHom.id T) a • c.smulRight x) e
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
⊢ f.IsInvertible → (↑e ∘SL f).IsInvertible

Tactic:
· rintro ⟨M, rfl⟩
    simp

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
⊢ f.IsInvertible → (f ∘SL ↑e).IsInvertible

Tactic:
· rintro ⟨M, rfl⟩
    simp

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

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

Tactic:
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

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 := IsFiltered.max i₀ j'
α : i₀ ⟶ i := leftToMax i₀ j'
β : j' ⟶ i := rightToMax i₀ j'
⊢ F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv = h.coconeιApp j

Tactic:
h.coconeιApp_eq j _ (φ ≫ β) α,

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 := IsFiltered.max i₀ j'
α : i₀ ⟶ i := leftToMax i₀ j'
β : j' ⟶ i := rightToMax i₀ j'
⊢ F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv = F.map (φ ≫ β) ≫ (h.isoMap α ⋯).inv
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: ι : Type u'
J : ι → Type u
inst✝³ : (i : ι) → Category.{v, u} (J i)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : ∀ (i : ι), IsCardinalFiltered (J i) κ
A✝ : Type w
inst✝ : SmallCategory A✝
F : A✝ ⥤ ((i : ι) → J i)
hC : HasCardinalLT (Arrow A✝) κ
c : (i : ι) → Cocone (F ⋙ Pi.eval J i) := fun i ↦ cocone (F ⋙ Pi.eval J i) hC
X Y : A✝
f : X ⟶ Y
i : ι
⊢ (F.map f ≫ fun i ↦ (c i).ι.app Y) i = ((fun i ↦ (c i).ι.app X) ≫ ((Functor.const A✝).obj fun i ↦ (c i).pt).map f) i

Tactic:
simpa using! (c i).ι.naturality f

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
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
f : ((coyoneda.obj (Opposite.op S)).mapCocone c).pt
i : J
g : S.right ⟶ (F ⋙ Under.forget R).obj i
h₁ : S.hom ≫ g = { app := fun i ↦ (F.obj i).hom, naturality := ⋯ }.app i
h₂ : Under.Hom.right f = g ≫ ((Under.forget R).mapCocone c).ι.app i
⊢ ∃ i xi, f = (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) xi

Tactic:
exact ⟨i, Under.homMk g h₁, Under.UnderMorphism.ext h₂⟩

Goal state after:
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 : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ m ≫ c.pt.hom = (pullbackConeEquivBinaryFan.functor.obj s).pt.hom

Tactic:
by
        simp [← hm₁, dsimp% c.fst.w]

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
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
⊢ ↥(RingHom.ker (TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T))) ≃ₗ[A ⊗[R] S]
    A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))

Tactic:
by
  let φ : A ⊗[R] S →ₐ[A] A ⊗[R] T :=
    Algebra.TensorProduct.map (.id _ _) (IsScalarTower.toAlgHom _ _ _)
  let ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
    { __ := Algebra.TensorProduct.comm _ _ _, commutes' _ := rfl }
  let e₃ : (RingHom.ker φ) ≃ₗ[R] A ⊗[R] (RingHom.ker (algebraMap S T)) :=
    (LinearMap.kerLTensorEquivOfSurjective (IsScalarTower.toAlgHom R S T).toLinearMap
      h₁ A).restrictScalars R
  let e₄' : (RingHom.ker φ) ≃ₗ[R] (A ⊗[R] S) ⊗[S] (RingHom.ker (algebraMap S T)) :=
    e₃ ≪≫ₗ _root_.TensorProduct.comm _ _ _ ≪≫ₗ
      (AlgebraTensorModule.cancelBaseChange _ _ S _ _).symm.restrictScalars R ≪≫ₗ
      (AlgebraTensorModule.congr (.refl S _) ePp.symm.toLinearEquiv).restrictScalars R ≪≫ₗ
      (_root_.TensorProduct.comm _ _ _).restrictScalars R
  let e₄ : (A ⊗[R] S) ⊗[S] (RingHom.ker (algebraMap S T)) ≃ₗ[A ⊗[R] S] (RingHom.ker φ) :=
    { __ := e₄'.symm, map_smul' r' x := by
        dsimp
        induction x with
        | zero => simp only [smul_zero, LinearEquiv.map_zero]
        | add x y _ _ => simp only [smul_add, LinearEquiv.map_add, *]
        | tmul x y =>
        induction x with
        | zero => simp only [zero_tmul, smul_zero, LinearEquiv.map_zero]
        | add x y _ _ => simp only [smul_add, add_tmul, LinearEquiv.map_add, *]
        | tmul x z =>
        induction r' with
        | zero => simp only [zero_smul, LinearEquiv.map_zero]
        | add x y _ _ => simp only [add_smul, LinearEquiv.map_add, *]
        | tmul r s =>
        rw [smul_tmul']
        ext1
        dsimp [e₄', ePp, φ]
        change ((r * x) ⊗ₜ[R] ((s * z) * y.1)) = (r ⊗ₜ[R] s) * (x ⊗ₜ[R] (z * y.1))
        rw [Algebra.TensorProduct.tmul_mul_tmul, mul_assoc] }
  exact e₄.symm

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ⋯
r_pos : r ≠ 0
r_prime : Nat.Prime r
⊢ MixedCharZero R r

Tactic:
have : CharZero R := q_mixedChar.toCharZero

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
r_pos : r ≠ 0
r_prime : Nat.Prime r
this : CharZero R
⊢ MixedCharZero R r
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ r ∣ p

Tactic:
rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ ↑p = 0
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ Ideal.span {↑↑n} = ⊤

Tactic:
apply not_imp_comm.mp (h.elim (Ideal.span {↑n}))

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ ¬CharZero (R ⧸ Ideal.span {↑↑n})
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ n • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p

Tactic:
rw [← natCast_zsmul r, zsmul_mem_zmultiples_iff_exists_sub_div (Int.natCast_ne_zero.mpr hn),
    Int.cast_natCast]
  rfl

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

Goal state before:
pp: α : Type u
β : Type v
g : α → β
f : α → α
a : α
⊢ corec g f a = g a :: corec g f (f a)

Tactic:
rw [corec_eq]

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

Goal state before:
pp: α : Type u
s s' : Computation α
⊢ s.destruct = Sum.inr s' → s = s'.think

Tactic:
by
  dsimp [destruct]
  rcases f0 : s.1 0 with - | a' <;> intro h
  · injection h with h'
    rw [← h']
    obtain ⟨f, al⟩ := s
    apply Subtype.ext
    dsimp [think, tail]
    rw [← f0]
    exact (Stream'.eta f).symm
  · contradiction

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

Goal state before:
pp: case inl
α : Type u
s₁✝ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
⊢ s₁ = nil ∧ s₁ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
cases s₁

Goal state after:
case inl.nil
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
⊢ nil = nil ∧ nil = nil ∨ ∃ x s₁' s₂', nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

case inl.cons
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
x✝ : α
s✝ : Seq α
⊢ cons x✝ s✝ = nil ∧ cons x✝ s✝ = nil ∨
    ∃ x s₁' s₂', cons x✝ s✝ = cons x s₁' ∧ cons x✝ s✝ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₁, s₂) =
    s₁.head :: s₂.head :: t

Tactic:
rw [corec_eq]

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (match (s₁, s₂) with
      | (s₁, snd) => s₁.head) ::
      corec
        (fun x ↦
          match x with
          | (s₁, snd) => s₁.head)
        (fun x ↦
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (match (s₁, s₂) with
        | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head :: corec (fun x ↦ x.fst.head) (fun x ↦ (x.snd, x.fst.tail)) (s₂, s₁.tail) = s₁.head :: s₂.head :: t

Tactic:
rw [corec_eq]

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head ::
      (s₂, s₁.tail).fst.head ::
        corec (fun x ↦ x.fst.head) (fun x ↦ (x.snd, x.fst.tail)) ((s₂, s₁.tail).snd, (s₂, s₁.tail).fst.tail) =
    s₁.head :: s₂.head :: t
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ (corec
        (fun x ↦
          match x with
          | (s₁, snd) => s₁.head)
        (fun x ↦
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (s₁, s₂)).tail =
    corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)

Tactic:
rw [corec_eq]

Goal state after:
α : Type u
s₁ s₂ : Stream' α
⊢ ((match (s₁, s₂) with
        | (s₁, snd) => s₁.head) ::
        corec
          (fun x ↦
            match x with
            | (s₁, snd) => s₁.head)
          (fun x ↦
            match x with
            | (s₁, s₂) => (s₂, s₁.tail))
          (match (s₁, s₂) with
          | (s₁, s₂) => (s₂, s₁.tail))).tail =
    corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case inr.inl
α : Type u
s₁✝ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
ih : motive s₁ s₁
⊢ s₁ = nil ∧ s₁ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
cases s₁

Goal state after:
case inr.inl.nil
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
ih : motive nil nil
⊢ nil = nil ∧ nil = nil ∨ ∃ x s₁' s₂', nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

case inr.inl.cons
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
x✝ : α
s✝ : Seq α
ih : motive (cons x✝ s✝) (cons x✝ s✝)
⊢ cons x✝ s✝ = nil ∧ cons x✝ s✝ = nil ∨
    ∃ x s₁' s₂', cons x✝ s✝ = cons x s₁' ∧ cons x✝ s✝ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ (corec head (fun s ↦ s.tail.tail) s).tail = corec head (fun s ↦ s.tail.tail) s.tail.tail

Tactic:
rw [corec_eq]

Goal state after:
α : Type u
s : Stream' α
⊢ (s.head :: corec head (fun s ↦ s.tail.tail) s.tail.tail).tail = corec head (fun s ↦ s.tail.tail) s.tail.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a₁ a₂ : α
s : Stream' α
⊢ corec head (fun s ↦ s.tail.tail) (a₁ :: a₂ :: s) = a₁ :: corec head (fun s ↦ s.tail.tail) s

Tactic:
rw [corec_eq]

Goal state after:
α : Type u
a₁ a₂ : α
s : Stream' α
⊢ (a₁ :: a₂ :: s).head :: corec head (fun s ↦ s.tail.tail) (a₁ :: a₂ :: s).tail.tail =
    a₁ :: corec head (fun s ↦ s.tail.tail) s
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
m n : ℕ
⊢ s.head :: List.take m (take n s.tail) = take (min (n + 1) (m + 1)) s

Tactic:
Nat.succ_min_succ,

Goal state after:
α : Type u
s : Stream' α
m n : ℕ
⊢ s.head :: List.take m (take n s.tail) = take (min n m).succ s
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
⊢ take (m + n) a = take m a ++ take n (drop m a)

Tactic:
apply append_left_injective _ _ (a.drop (m + n)) ((a.drop m).drop n)

Goal state after:
case h
α : Type u
m n : ℕ
a : Stream' α
⊢ take (m + n) a ++ₛ drop (m + n) a = take m a ++ take n (drop m a) ++ₛ drop n (drop m a)

case hl
α : Type u
m n : ℕ
a : Stream' α
⊢ (take (m + n) a).length = (take m a ++ take n (drop m a)).length
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case nil
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a' : α
⊢ corec Stream'.cycleF Stream'.cycleG (a', [], a, l) = [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
rw [corec_eq]

Goal state after:
case nil
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a' : α
⊢ Stream'.cycleF (a', [], a, l) :: corec Stream'.cycleF Stream'.cycleG (Stream'.cycleG (a', [], a, l)) =
    [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ corec id tail s.tail = s.tail :: corec id tail s.tail.tail

Tactic:
rw [corec_eq]

Goal state after:
α : Type u
s : Stream' α
⊢ id s.tail :: corec id tail s.tail.tail = s.tail :: corec id tail s.tail.tail