mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf✝ : f✝ ∈ Ideal.map C I
f : MvPolynomial σ R
hf : f ∈ ⇑C '' ↑I
n : σ →₀ ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : ¬n = 0
⊢ (if 0 = n then x else 0) ∈ I

Tactic:
·

Goal state after:
case neg
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf✝ : f✝ ∈ Ideal.map C I
f : MvPolynomial σ R
hf : f ∈ ⇑C '' ↑I
n : σ →₀ ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : ¬n = 0
⊢ (if 0 = n then x else 0) ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_2
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (m : σ →₀ ℕ), coeff m 0 ∈ I

pp: case mp.refine_3
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (x y : MvPolynomial σ R),
    x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
      y ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
        (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → (∀ (m : σ →₀ ℕ), coeff m y ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (x + y) ∈ I

pp: case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (a x : MvPolynomial σ R),
    x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
      (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (a • x) ∈ I

Tactic:
·

Goal state after:
case mp.refine_2
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (m : σ →₀ ℕ), coeff m 0 ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_3
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (x y : MvPolynomial σ R),
    x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
      y ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
        (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → (∀ (m : σ →₀ ℕ), coeff m y ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (x + y) ∈ I

pp: case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (a x : MvPolynomial σ R),
    x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
      (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (a • x) ∈ I

Tactic:
·

Goal state after:
case mp.refine_3
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (x y : MvPolynomial σ R),
    x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
      y ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
        (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → (∀ (m : σ →₀ ℕ), coeff m y ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (x + y) ∈ I
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_2.mem.inr
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x : ↥N
j : Fin k
⊢ f (nj j) ∈ M'

Tactic:
·

Goal state after:
case refine_2.mem.inr
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x : ↥N
j : Fin k
⊢ f (nj j) ∈ M'
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (a x : MvPolynomial σ R),
    x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
      (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (a • x) ∈ I

Tactic:
·

Goal state after:
case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (a x : MvPolynomial σ R),
    x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
      (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (a • x) ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m f ∈ I) → f ∈ Ideal.map C I

Tactic:
·

Goal state after:
case mpr
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m f ∈ I) → f ∈ Ideal.map C I
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ -b - -a = -(b - a)

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case inl
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ c * a ≡ c * b [ZMOD c * n]

pp: case inr.inl
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 * a ≡ 0 * b [ZMOD 0 * n]

pp: case inr.inr
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : 0 < c
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
·

Goal state after:
case inl
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ c * a ≡ c * b [ZMOD c * n]
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case inr.inl
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 * a ≡ 0 * b [ZMOD 0 * n]

pp: case inr.inr
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : 0 < c
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
·

Goal state after:
case inr.inl
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 * a ≡ 0 * b [ZMOD 0 * n]
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case inr.inr
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : 0 < c
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
·

Goal state after:
case inr.inr
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : 0 < c
⊢ c * a ≡ c * b [ZMOD c * n]
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
⊢ d - c = b + d - (a + c) - (b - a)

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case refine_1
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑d ∣ c / ↑d * (b - a)

pp: case refine_2
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ (m / ↑(m.gcd c)).gcd (c / ↑d) = 1

Tactic:
·

Goal state after:
case refine_1
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑d ∣ c / ↑d * (b - a)
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case refine_2
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ (m / ↑(m.gcd c)).gcd (c / ↑d) = 1

Tactic:
·

Goal state after:
case refine_2
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ (m / ↑(m.gcd c)).gcd (c / ↑d) = 1
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: m a b c : ℤ
hm : 0 < m
h : c * a ≡ c * b [ZMOD m]
⊢ a * c ≡ b * c [ZMOD m]

Tactic:
simpa [mul_comm] using h

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a ≡ b [ZMOD m]

Tactic:
convert! h.mul_left'

Goal state after:
case e'_1
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ m = ?m.24 * (m / c)

case e'_2
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a = ?m.24 * (a / c)

case e'_3
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ b = ?m.24 * (b / c)

m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ ℤ
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : (lift f).range ≤ S
⊢ NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra

pp: case refine_2
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
⊢ (lift f).range ≤ S

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : (lift f).range ≤ S
⊢ NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
⊢ (lift f).range ≤ S

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
⊢ (lift f).range ≤ S
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
⊢ x ∈ ker (Quotient.lift I f H) → x ∈ map (Quotient.mk I) (ker f)

pp: case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
⊢ x ∈ map (Quotient.mk I) (ker f) → x ∈ ker (Quotient.lift I f H)

Tactic:
·

Goal state after:
case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
⊢ x ∈ ker (Quotient.lift I f H) → x ∈ map (Quotient.mk I) (ker f)
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
this : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ}, a ≡ b [MOD p] → a ≤ b → ↑a = ↑b
hle : ¬a ≤ b
⊢ ↑a = ↑b

pp: R✝ : Type u_1
inst✝² : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
hle : a ≤ b
⊢ ↑a = ↑b

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
this : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ}, a ≡ b [MOD p] → a ≤ b → ↑a = ↑b
hle : ¬a ≤ b
⊢ ↑a = ↑b
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsRightCancelAdd R],
    a ≤ b → (↑a = ↑b ↔ a ≡ b [MOD p])
hle : ¬a ≤ b
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]

pp: R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsRightCancelAdd R],
    a ≤ b → (↑a = ↑b ↔ a ≡ b [MOD p])
hle : ¬a ≤ b
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
⊢ x ∈ map (Quotient.mk I) (ker f) → x ∈ ker (Quotient.lift I f H)

Tactic:
·

Goal state after:
case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
⊢ x ∈ map (Quotient.mk I) (ker f) → x ∈ ker (Quotient.lift I f H)
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
q : ℕ
hq : Nat.Prime q
inst✝ : CharP R 1
hneq : 1 ≠ q
h : 1 ∣ q
⊢ False

pp: case inr
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h✝ : p ∣ q
h : p = q
⊢ False

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
q : ℕ
hq : Nat.Prime q
inst✝ : CharP R 1
hneq : 1 ≠ q
h : 1 ∣ q
⊢ False
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h✝ : p ∣ q
h : p = q
⊢ False

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h✝ : p ∣ q
h : p = q
⊢ False
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)

Tactic:
apply Ideal.ext
  intro x
  constructor
  · intro hx
    obtain ⟨y, hy⟩ := Quotient.mk_surjective x
    rw [mem_ker, ← hy, Ideal.Quotient.lift_mk, ← mem_ker] at hx
    rw [← hy, mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective]
    exact ⟨y, hx, rfl⟩
  · intro hx
    rw [mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective] at hx
    obtain ⟨y, hy⟩ := hx
    rw [mem_ker, ← hy.right, Ideal.Quotient.lift_mk]
    exact hy.left

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

Goal state before:
pp: case inr.inl.inr.inr
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : 1 = -1
⊢ 1 = -1

pp: case inr.inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : -1 = 1
⊢ -1 = 1

Tactic:
·

Goal state after:
case inr.inl.inr.inr
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : 1 = -1
⊢ 1 = -1
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case inr.inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : -1 = 1
⊢ -1 = 1

Tactic:
·

Goal state after:
case inr.inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : -1 = 1
⊢ -1 = 1
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝⁴ : AddMonoidWithOne R
S : Type u_2
inst✝³ : Semiring S
inst✝² : CharZero R
inst✝¹ : ExpChar R 1
inst✝ : ExpChar S 1
⊢ ExpChar (R × S) 1

pp: case prime
R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
hp : Nat.Prime p
hchar✝ : CharP R p
⊢ ExpChar (R × S) p

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝⁴ : AddMonoidWithOne R
S : Type u_2
inst✝³ : Semiring S
inst✝² : CharZero R
inst✝¹ : ExpChar R 1
inst✝ : ExpChar S 1
⊢ ExpChar (R × S) 1
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case prime.zero
R : Type u_1
inst✝⁴ : AddMonoidWithOne R
S : Type u_2
inst✝³ : Semiring S
inst✝² : CharZero S
inst✝¹ : ExpChar R 1
inst✝ : ExpChar S 1
hp : Nat.Prime 1
hchar✝ : CharP R 1
⊢ ExpChar (R × S) 1

pp: case prime.prime
R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
hp : Nat.Prime p
hchar✝¹ : CharP R p
hprime✝ : Nat.Prime p
hchar✝ : CharP S p
⊢ ExpChar (R × S) p

Tactic:
·

Goal state after:
case prime.zero
R : Type u_1
inst✝⁴ : AddMonoidWithOne R
S : Type u_2
inst✝³ : Semiring S
inst✝² : CharZero S
inst✝¹ : ExpChar R 1
inst✝ : ExpChar S 1
hp : Nat.Prime 1
hchar✝ : CharP R 1
⊢ ExpChar (R × S) 1
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case prime.prime
R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
hp : Nat.Prime p
hchar✝¹ : CharP R p
hprime✝ : Nat.Prime p
hchar✝ : CharP S p
⊢ ExpChar (R × S) p

Tactic:
·

Goal state after:
case prime.prime
R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
hp : Nat.Prime p
hchar✝¹ : CharP R p
hprime✝ : Nat.Prime p
hchar✝ : CharP S p
⊢ ExpChar (R × S) p
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker f ≤ I → ker f = I

pp: case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker f = I → ker f ≤ I

Tactic:
·

Goal state after:
case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker f ≤ I → ker f = I
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker f = I → ker f ≤ I

Tactic:
·

Goal state after:
case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker f = I → ker f ≤ I
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case pos
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : r = 0
⊢ Unitization.inl r = -↑a

pp: case neg
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : ¬r = 0
⊢ Unitization.inl r = -↑a

Tactic:
·

Goal state after:
case pos
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : r = 0
⊢ Unitization.inl r = -↑a
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case pos.fst
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : r = 0
⊢ (Unitization.inl r).toProd.1 = (-↑a).toProd.1

pp: case pos.snd
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : r = 0
⊢ ↑(Unitization.inl r).toProd.2 = ↑(-↑a).toProd.2

Tactic:
·

Goal state after:
case pos.fst
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : r = 0
⊢ (Unitization.inl r).toProd.1 = (-↑a).toProd.1
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case pos.snd
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : r = 0
⊢ ↑(Unitization.inl r).toProd.2 = ↑(-↑a).toProd.2

Tactic:
·

Goal state after:
case pos.snd
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : r = 0
⊢ ↑(Unitization.inl r).toProd.2 = ↑(-↑a).toProd.2
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case neg
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : ¬r = 0
⊢ Unitization.inl r = -↑a

Tactic:
·

Goal state after:
case neg
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : ¬r = 0
⊢ Unitization.inl r = -↑a