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
inst✝ : Module.Flat R M
x : ↥(((AlgebraTensorModule.lTensor S M) f).eqLocus ((AlgebraTensorModule.lTensor S M) g))
⊢ ((AlgebraTensorModule.lTensor S M) (f.eqLocus g).subtype) ((tensorEqLocusInv S M f g) x) = ↑x

Tactic:
]

Goal state after:
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 g).subtype) ((tensorEqLocusInv S M f g) x) = ↑x
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
    (parallelPair
      ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
        WalkingParallelPairHom.left)
      ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
        WalkingParallelPairHom.right))
    (R.tensorProd S)

Tactic:
]

Goal state after:
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
    (parallelPair
      ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
        WalkingParallelPairHom.left)
      ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
        WalkingParallelPairHom.right))
    (R.tensorProd S)
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.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R ⋙
      CategoryTheory.Under.pushout f)

Tactic:
]

Goal state after:
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.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R ⋙
      CategoryTheory.Under.pushout f)
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
this : Function.Exact ⇑0 ⇑(lTensor A g)
⊢ Function.Injective ⇑(lTensor A g)

Tactic:
]

Goal state after:
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
this : Function.Exact ⇑0 ⇑(lTensor A g)
⊢ Function.Injective ⇑(lTensor A g)
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.subtype).range = (lTensor A f.ker.subtype).range

Tactic:
]

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
⊢ ↑t ≠ 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : Ring R
t : ℕ
inst✝¹ : Invertible ↑t
inst✝ : Nontrivial R
⊢ ↑t ≠ 0
Module: Mathlib.Algebra.CharP.Invertible

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

Tactic:
]

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
⊢ 1 = 1

Tactic:
]

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
this : Nontrivial R
⊢ ¬↑n = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
n : ℕ
hp : Nat.Prime p
h : IsUnit ↑n
this : Nontrivial R
⊢ ¬↑n = 0
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:
]

Goal state after:
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)
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 = q

Tactic:
]

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

Goal state before:
pp: case inl
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
⊢ IsPrimePow q

Tactic:
]

Goal state after:
case inl
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
⊢ IsPrimePow q
Module: Mathlib.Algebra.CharP.LocalRing

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
g : ↑a ∈ IsLocalRing.maximalIdeal R
a_cast_zero : ↑a = 0
⊢ False
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
⊢ 0 = 0

Tactic:
]

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
⊢ (∀ (x : M), (↑n • 1) x = 0 x) ↔ ↑n = 0

Tactic:
]

Goal state after:
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
⊢ (∀ (x : M), (↑n • 1) x = 0 x) ↔ ↑n = 0
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case tmul.tmul.tmul
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))
y : ↥(RingHom.ker (algebraMap S T))
x : A
z : S
r : A
s : S
⊢ e₄'.symm ((r ⊗ₜ[R] s • x ⊗ₜ[R] z) ⊗ₜ[S] y) = r ⊗ₜ[R] s • e₄'.symm (x ⊗ₜ[R] z ⊗ₜ[S] y)

Tactic:
]

Goal state after:
case tmul.tmul.tmul
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))
y : ↥(RingHom.ker (algebraMap S T))
x : A
z : S
r : A
s : S
⊢ e₄'.symm ((r ⊗ₜ[R] s • x ⊗ₜ[R] z) ⊗ₜ[S] y) = r ⊗ₜ[R] s • e₄'.symm (x ⊗ₜ[R] z ⊗ₜ[S] y)
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case tmul.tmul.tmul
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))
y : ↥(RingHom.ker (algebraMap S T))
x : A
z : S
r : A
s : S
⊢ (r * x) ⊗ₜ[R] (s * (z * ↑y)) = (r * x) ⊗ₜ[R] (s * (z * ↑y))

Tactic:
]

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 : ι
⊢ 0 = 0

Tactic:
]

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

Tactic:
]

Goal state after:
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
⊢ ↑p = 0

Tactic:
]

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.Subring

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

Tactic:
]

Goal state after:
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
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case pos
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
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
hx0 : x = 0
⊢ 0 ∈ S

Tactic:
]

Goal state after:
case pos
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
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
hx0 : x = 0
⊢ 0 ∈ S
Module: Mathlib.Algebra.CharP.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ (Ideal.Quotient.mk I) ↑x = 0 ↔ ↑x = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ (Ideal.Quotient.mk I) ↑x = 0 ↔ ↑x = 0
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: case neg
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
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
y : ↥S
hy : x⁻¹ = ↑y
⊢ x⁻¹ ∈ S

Tactic:
]

Goal state after:
case neg
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
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
y : ↥S
hy : x⁻¹ = ↑y
⊢ x⁻¹ ∈ S
Module: Mathlib.Algebra.CharZero.AddMonoidHom

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : AddCommMonoidWithOne M
inst✝¹ : AddCommMonoidWithOne N
inst✝ : CharZero M
e : M →+ N
he : e 1 = 1
he' : Function.Injective ⇑e
n m : ℕ
h : n = m
⊢ n = m

Tactic:
]

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : AddCommMonoidWithOne M
inst✝¹ : AddCommMonoidWithOne N
inst✝ : CharZero M
e : M →+ N
he : e 1 = 1
he' : Function.Injective ⇑e
n m : ℕ
h : n = m
⊢ n = m
Module: Mathlib.Algebra.CharP.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x ∈ I ↔ ↑x = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x ∈ I ↔ ↑x = 0
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
⊢ I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
hI

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ CharZero (R ⧸ I)
Module: Mathlib.Algebra.CharP.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
x✝ : CharP (R ⧸ I) n
x : ℕ
hx : ↑x ∈ I
⊢ ↑x = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
x✝ : CharP (R ⧸ I) n
x : ℕ
hx : ↑x ∈ I
⊢ ↑x = 0
Module: Mathlib.Algebra.CharP.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ (∀ (x : ℕ), ↑x ∈ I → ↑x = 0) ↔ Ideal.comap (Nat.castRingHom R) I ≤ Ideal.comap (Nat.castRingHom R) ⊥

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ (∀ (x : ℕ), ↑x ∈ I → ↑x = 0) ↔ Ideal.comap (Nat.castRingHom R) I ≤ Ideal.comap (Nat.castRingHom R) ⊥