mathlib-initiative/mathlib-tactics huggingface dataset:
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 : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pushoutComp._auto_1
⊢ P.HasPushoutsAlong fg

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this :
  CreatesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
⊢ PreservesLimit (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)

Tactic:
by

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 : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pushoutComp._auto_1
this : P.HasPushoutsAlong fg
⊢ P.IsStableUnderCobaseChangeAlong fg

Tactic:
by

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
⊢ tensorKerInv S M f ∘ₗ tensorKer S M f = id

Tactic:
by

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
⊢ P.HasPushoutsAlong fg

Tactic:
by

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

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
⊢ tensorEqLocus S M f g ∘ₗ tensorEqLocusInv S M f g = id

Tactic:
by

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
g : X ⟶ Y
h : f = g
⊢ P.HasPushoutsAlong g

Tactic:
by

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
g : X ⟶ Y
h : f = g
this : P.HasPushoutsAlong g
⊢ P.IsStableUnderCobaseChangeAlong g

Tactic:
by

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
⊢ tensorEqLocusInv S M f g ∘ₗ tensorEqLocus S M f g = id

Tactic:
by

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
g : X ⟶ Y
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
h : f = g
A : P.Under Q X
⊢ P.HasPushoutsAlong g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this✝ :
  CreatesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
this :
  PreservesLimit (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ S)

Tactic:
by

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 : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
g : X ⟶ Y
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
h : f = g
A : P.Under Q X
⊢ pushout.inl A.hom f ≫ ((pushoutCongr h).hom.app A).right = pushout.inl A.hom g

Tactic:
by

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

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
⊢ PreservesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ f)

Tactic:
by

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

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

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

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
⊢ Function.Exact ⇑0 ⇑(rTensor P K.subtype)

Tactic:
by

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

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
⊢ Q (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯)

Tactic:
by

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
⊢ Function.Injective ⇑(lTensor A g)

Tactic:
by

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 P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
⊢ ↥(lTensor A f).ker ≃ₗ[R] A ⊗[R] ↥f.ker

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
t : ℕ
inst✝¹ : Invertible ↑t
inst✝ : Nontrivial R
⊢ ¬ringChar R ∣ t

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
n : ℕ
this : ↑(↑n * n.gcdA p + ↑p * n.gcdB p) = ↑↑(n.gcd p)
⊢ ↑n * ↑(n.gcdA p) = ↑(n.gcd p)

Tactic:
by

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

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

Tactic:
by

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

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 * ↑(n.gcdA p) = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
n : ℕ
inst✝ : Invertible ↑n
h : n.Coprime p
⊢ ⅟↑n = ↑(n.gcdA p)

Tactic:
by

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

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

Tactic:
by

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

Tactic:
by

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 B : P.Under Q Y
g : A ⟶ B
⊢ (map Q hPf ⋙ pushout P Q f).map g ≫ Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj B).right)) B.hom ⋯) ⋯ ⋯ =
    Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯) ⋯ ⋯ ≫ (𝟭 (P.Under Q Y)).map g

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
⊢ 2 ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
⊢ 3 ≠ 0

Tactic:
by

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)
⊢ (tensorEqualizerAux S T f g) (x * y) = (tensorEqualizerAux S T f g) x * (tensorEqualizerAux S T f g) y

Tactic:
by

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 = r ^ n * a

Tactic:
by

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
⊢ IsUnit ↑a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : ℕ
hchar : CharP R p
htorsion : ∃ x, Ideal.torsionOf R M x = ⊥
n : ℕ
⊢ ↑n = ↑n • 1

Tactic:
by

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
a_unit : IsUnit ↑a
⊢ ↑(r ^ n) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : ℕ
hchar : CharP R p
htorsion : ∃ x, Ideal.torsionOf R M x = ⊥
n : ℕ
exact : ↑n = ↑n • 1
h : ∀ (x : M), (↑n • 1) x = 0 x
x : M
hx : Ideal.torsionOf R M x = ⊥
⊢ ↑n = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : ℕ
hchar : CharP R p
htorsion : ∃ x, Ideal.torsionOf R M x = ⊥
n : ℕ
⊢ ↑n = 0 ↔ p ∣ n

Tactic:
by

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
a_unit : IsUnit ↑a
rn_cast_zero : ↑(r ^ n) = 0
q_eq_rn : q = r ^ n
n_zero : n = 0
⊢ q = 1

Tactic:
by

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 = 0 ∨ IsPrimePow q

Tactic:
by

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)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] ↥(RingHom.ker (algebraMap S T)) :=
  LinearEquiv.restrictScalars R ((IsScalarTower.toAlgHom R S T).toLinearMap.kerLTensorEquivOfSurjective h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (algebraMap S T))) A).symm ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (algebraMap S T))) ↑ePp.symm) ≪≫ₗ
    LinearEquiv.restrictScalars R (_root_.TensorProduct.comm S (↥(RingHom.ker (algebraMap S T))) (A ⊗[R] S))
r' : A ⊗[R] S
x : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))
⊢ (↑e₄'.symm).toFun (r' • x) = (RingHom.id (A ⊗[R] S)) r' • (↑e₄'.symm).toFun x

Tactic:
by

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

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
⊢ ↑x = 0

Tactic:
by

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)
⊢ r ≠ 0

Tactic:
by

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

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

Tactic:
by

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'
S : IntermediateField K L
⊢ Function.Injective fun S ↦ S.carrier

Tactic:
by

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
x : L
hx : x ∈ S
⊢ -x ∈ S

Tactic:
by

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

Goal state after: