mathlib-initiative/mathlib-tactics huggingface dataset:
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
m : M
r : R
x : ↥(f.eqLocus g)
⊢ ⟨m ⊗ₜ[R] ↑(r • x), ⋯⟩ = (RingHom.id R) r • ⟨m ⊗ₜ[R] ↑x, ⋯⟩

Tactic:
simp

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
m : M
a : ↥f.ker
⊢ m ⊗ₜ[R] ↑a ∈ ((AlgebraTensorModule.lTensor S M) f).ker

Tactic:
simp

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
m : M
r : R
x : ↥f.ker
⊢ ⟨m ⊗ₜ[R] ↑(r • x), ⋯⟩ = (RingHom.id R) r • ⟨m ⊗ₜ[R] ↑x, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: case h₀
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A B : P.Over Q X
g : A ⟶ B
⊢ ((𝟭 (P.Over Q X)).map g ≫ Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj B).left) B.hom ⋯) ⋯ ⋯).left ≫
      pullback.fst ((map Q hPf).obj B).hom f =
    (Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj A).left) A.hom ⋯) ⋯ ⋯ ≫
          (map Q hPf ⋙ pullback P Q f).map g).left ≫
      pullback.fst ((map Q hPf).obj B).hom f

Tactic:
simp

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

Goal state before:
pp: case h₁
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A B : P.Over Q X
g : A ⟶ B
⊢ ((𝟭 (P.Over Q X)).map g ≫ Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj B).left) B.hom ⋯) ⋯ ⋯).left ≫
      pullback.snd ((map Q hPf).obj B).hom f =
    (Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj A).left) A.hom ⋯) ⋯ ⋯ ≫
          (map Q hPf ⋙ pullback P Q f).map g).left ≫
      pullback.snd ((map Q hPf).obj B).hom f

Tactic:
simp

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

Goal state before:
pp: case h_map
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
X Y Z : T
inst✝ : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
U V : P.Under Q Z
k : U ⟶ V
⊢ ((map Q ⋯).map k).right = (eqToHom ⋯ ≫ (map Q hg ⋙ map Q hf).map k ≫ eqToHom ⋯).right

Tactic:
simp

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

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
A B : P.Under Q X
g : A ⟶ B
⊢ (Under.mk Q (pushout.inr A.hom f) ⋯).hom ≫ pushout.desc (g.right ≫ pushout.inl B.hom f) (pushout.inr B.hom f) ⋯ =
    (Under.mk Q (pushout.inr B.hom f) ⋯).hom

Tactic:
simp

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

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
A B : P.Under Q X
g : A ⟶ B
⊢ B.hom = A.hom ≫ g.right

Tactic:
simp

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

Goal state before:
pp: case h₀
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
X✝ Y✝ Z✝ : P.Under Q X
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ pushout.inl X✝.hom f ≫
      (Under.homMk (pushout.desc ((x✝¹ ≫ x✝).right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right =
    pushout.inl X✝.hom f ≫
      (Under.homMk (pushout.desc (x✝¹.right ≫ pushout.inl Y✝.hom f) (pushout.inr Y✝.hom f) ⋯) ⋯ ⋯ ≫
          Under.homMk (pushout.desc (x✝.right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right

Tactic:
simp

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

Goal state before:
pp: case h₁
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
X✝ Y✝ Z✝ : P.Under Q X
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ pushout.inr X✝.hom f ≫
      (Under.homMk (pushout.desc ((x✝¹ ≫ x✝).right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right =
    pushout.inr X✝.hom f ≫
      (Under.homMk (pushout.desc (x✝¹.right ≫ pushout.inl Y✝.hom f) (pushout.inr Y✝.hom f) ⋯) ⋯ ⋯ ≫
          Under.homMk (pushout.desc (x✝.right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right

Tactic:
simp

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).ker
⊢ ↑((tensorKer S M f ∘ₗ tensorKerInv S M f) x) = ↑(id x)

Tactic:
simp

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
m : M
x : ↥f.ker
⊢ (lTensor M f.ker.subtype) (((AlgebraTensorModule.curry (tensorKerInv S M f ∘ₗ tensorKer S M f)) m) x) =
    (lTensor M f.ker.subtype) (((AlgebraTensorModule.curry id) m) x)

Tactic:
simp

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

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X✝ Y Z : T
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderCobaseChangeAlong f
inst✝⁴ : P.IsStableUnderCobaseChangeAlong g
inst✝³ : P.HasPushoutsAlong f
inst✝² : P.HasPushoutsAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderCobaseChange
fg : X✝ ⟶ Z
hfg : fg = f ≫ g
this✝ : P.HasPushoutsAlong fg
X : P.Under Q X✝
this : HasPushout X.hom fg
⊢ ((pushout P Q fg).obj X).hom ≫ (pushout.congrHom ⋯ hfg ≪≫ (pushoutLeftPushoutInrIso X.hom f g).symm).hom =
    ((pushout P Q f ⋙ pushout P Q g).obj X).hom

Tactic:
simp

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))
⊢ ↑((tensorEqLocus S M f g ∘ₗ tensorEqLocusInv S M f g) x✝) = ↑(id x✝)

Tactic:
simp

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
m : M
x : ↥(f.eqLocus g)
⊢ (lTensor M (f.eqLocus g).subtype)
      (((AlgebraTensorModule.curry (tensorEqLocusInv S M f g ∘ₗ tensorEqLocus S M f g)) m) x) =
    (lTensor M (f.eqLocus g).subtype) (((AlgebraTensorModule.curry id) m) x)

Tactic:
simp

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

Goal state before:
pp: T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A : P.Under Q Y
⊢ ((map Q hPf).obj A).hom ≫ 𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right) = f ≫ A.hom

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_4
P : Type u_5
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
g : M →ₗ[R] N
hg : Function.Injective ⇑g
H : Function.Exact ⇑g ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
Q : Type (max u_1 u_6) := A →₀ R
π : Q →ₗ[R] A := Finsupp.linearCombination R fun a ↦ a
hπ : Function.Surjective ⇑π
K : Submodule R Q := π.ker
⊢ lTensor Q g ∘ₗ rTensor M K.subtype = rTensor N K.subtype ∘ₗ lTensor (↥K) g

Tactic:
simp

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

Goal state before:
pp: T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A : P.Under Q Y
⊢ ((map Q hPf ⋙ pushout P Q f).obj A).hom ≫ pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯ =
    ((𝟭 (P.Under Q Y)).obj A).hom

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_4
P : Type u_5
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
g : M →ₗ[R] N
hg : Function.Injective ⇑g
H : Function.Exact ⇑g ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
Q : Type (max u_1 u_6) := A →₀ R
π : Q →ₗ[R] A := Finsupp.linearCombination R fun a ↦ a
hπ : Function.Surjective ⇑π
K : Submodule R Q := π.ker
⊢ lTensor Q f ∘ₗ rTensor N K.subtype = rTensor P K.subtype ∘ₗ lTensor (↥K) f

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_4
P : Type u_5
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
g : M →ₗ[R] N
hg : Function.Injective ⇑g
H : Function.Exact ⇑g ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
Q : Type (max u_1 u_6) := A →₀ R
π : Q →ₗ[R] A := Finsupp.linearCombination R fun a ↦ a
hπ : Function.Surjective ⇑π
K : Submodule R Q := π.ker
⊢ lTensor A g ∘ₗ rTensor M π = rTensor N π ∘ₗ lTensor Q g

Tactic:
simp

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

Goal state before:
pp: case h₀
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A B : P.Under Q Y
g : A ⟶ B
⊢ pushout.inl ((map Q hPf).obj A).hom f ≫
      ((map Q hPf ⋙ pushout P Q f).map g ≫
          Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj B).right)) B.hom ⋯) ⋯ ⋯).right =
    pushout.inl ((map Q hPf).obj A).hom f ≫
      (Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯) ⋯ ⋯ ≫ (𝟭 (P.Under Q Y)).map g).right

Tactic:
simp

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

Goal state before:
pp: case h₁
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A B : P.Under Q Y
g : A ⟶ B
⊢ pushout.inr ((map Q hPf).obj A).hom f ≫
      ((map Q hPf ⋙ pushout P Q f).map g ≫
          Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj B).right)) B.hom ⋯) ⋯ ⋯).right =
    pushout.inr ((map Q hPf).obj A).hom f ≫
      (Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯) ⋯ ⋯ ≫ (𝟭 (P.Under Q Y)).map g).right

Tactic:
simp

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
x y : T ⊗[R] ↥(f.equalizer g)
⊢ (Algebra.TensorProduct.map (AlgHom.id S T) (f.equalizer g).val) (x * y) =
    ↑((tensorEqualizerAux S T f g) x * (tensorEqualizerAux S T f g) y)

Tactic:
simp

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

Goal state before:
pp: 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)
q_zero : ↑q = 0
⊢ r ≠ 0

Tactic:
apply ne_zero_of_dvd_ne_zero (ne_of_gt q_pos)

Goal state after:
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 : ℕ := ⋯
q_zero : ↑q = 0
⊢ r ∣ q
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'
S : IntermediateField K L
toSubsemiring✝¹ : Subsemiring L
algebraMap_mem'✝¹ : ∀ (r : K), (algebraMap K L) r ∈ toSubsemiring✝¹.carrier
inv_mem'✝¹ :
  ∀ x ∈ { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ }.carrier,
    x⁻¹ ∈ { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ }.carrier
toSubsemiring✝ : Subsemiring L
algebraMap_mem'✝ : ∀ (r : K), (algebraMap K L) r ∈ toSubsemiring✝.carrier
inv_mem'✝ :
  ∀ x ∈ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }.carrier,
    x⁻¹ ∈ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }.carrier
⊢ (fun S ↦ S.carrier)
        { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹, inv_mem' := inv_mem'✝¹ } =
      (fun S ↦ S.carrier)
        { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝, inv_mem' := inv_mem'✝ } →
    { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹, inv_mem' := inv_mem'✝¹ } =
      { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝, inv_mem' := inv_mem'✝ }

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
n : ℕ
⊢ ↑n ∈ S

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
I : Ideal R
inst✝ : CharP (R ⧸ I) p
⊢ (Quotient.mk I) ↑p = 0

Tactic:
simp

Goal state after:
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'
inst✝¹ : Algebra L L'
inst✝ : IsScalarTower K L L'
x✝ : L'
⊢ x✝ ∈ ↑(toAlgHom K L L').fieldRange ↔ x✝ ∈ Set.range ⇑(algebraMap L L')

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑0 = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑(Rat.num 1) /ₚ ↑(Rat.pnatDen 1) = 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑(a.num * b.num * ↑(a * b).den) = ↑a.num * ↑b.num * ↑(a * b).den

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑((a.num * ↑b.den + b.num * ↑a.den) * ↑(a + b).den) = (↑a.num * ↑b.den + ↑b.num * ↑a.den) * ↑(a + b).den

Tactic:
simp

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

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
v : Seq1 α
H : s.destruct = some v
⊢ motive s

Tactic:
· obtain ⟨a, s'⟩ := v
    rw [destruct_eq_cons H]
    apply cons

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u
a : Stream' α
n : ℕ
⊢ (drop n a).head = a.get n

Tactic:
simp

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

Goal state before:
pp: case cons.cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝¹ : α
s✝¹ : Seq α
x✝ : α
s✝ : Seq α
⊢ R (cons x✝¹ s✝¹) (cons x✝ s✝) →
    BisimO R (cons x✝¹ s✝¹).destruct (cons x✝ s✝).destruct →
      (cons x✝¹ s✝¹).head = (cons x✝ s✝).head ∧ R (cons x✝¹ s✝¹).tail (cons x✝ s✝).tail

Tactic:
simp

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

Goal state after:
ι : 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)
⊢ -1 = -1
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁.tail ⋈ s₂.tail).get (2 * n + 1) = s₂.get n.succ

Tactic:
get_interleave_right n (tail s₁) (tail s₂)

Goal state after:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ s₂.tail.get n = s₂.get n.succ
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ none = none ↔ none.isNone = true

Tactic:
simp

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

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
val✝ : α
⊢ some val✝ = none ↔ (some val✝).isNone = true

Tactic:
simp

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

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
h : s.TerminatedAt 0
n : ℕ
a✝ : α
⊢ none = some a✝ ↔ nil.get? n = some a✝

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u
a : α
l : List α
⊢ (↑(a :: l)).get? 0 = (cons a ↑l).get? 0

Tactic:
simp

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

Goal state before:
pp: case succ
α : Type u
a : α
l : List α
n : ℕ
⊢ (↑(a :: l)).get? (n + 1) = (cons a ↑l).get? (n + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ENatToNat

Goal state before:
pp: case top
⊢ ¬⊤ < ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ENatToNat

Goal state before:
pp: case coe
a✝ : ℕ
⊢ ¬⊤ < ↑a✝

Tactic:
simp

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

Goal state before:
pp: case cons.zero
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
h : 0 < (b :: x).length
⊢ (b :: x ++ₛ a).get 0 = (b :: x)[0]

Tactic:
simp

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

Goal state before:
pp: α : Type u
s : Stream' α
⊢ [s.head] ++ₛ s.tail = s

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u
xs : Stream' α
⊢ (take 0 xs).dropLast = take (0 - 1) xs

Tactic:
simp

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

Goal state before:
pp: case a
α : Type u
s : Computation α
h : s.Terminates
⊢ (s.think.val s.think.length).isSome = true → s.length + 1 ≤ s.think.length

Tactic:
rcases length (think s) with - | n

Goal state after:
case a.zero
α : Type u
s : Computation α
h : s.Terminates
⊢ (s.think.val 0).isSome = true → s.length + 1 ≤ 0

case a.succ
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
⊢ (s.think.val (n + 1)).isSome = true → s.length + 1 ≤ n + 1
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case hl
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ (List.map f (take n a)).length = (take n (map f a)).length

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ ∀ (i : ℕ) (h₁ : i < (List.map f (take n a)).length) (h₂ : i < (take n (map f a)).length),
    (List.map f (take n a))[i] = (take n (map f a))[i]

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u
m n : ℕ
a : Stream' α
⊢ ∀ (i : ℕ) (h₁ : i < (take n (drop m a)).length) (h₂ : i < (List.drop m (take (m + n) a)).length),
    (take n (drop m a))[i] = (List.drop m (take (m + n) a))[i]

Tactic:
simp

Goal state after: