mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a + -a ≡ b + -b [ZMOD n]

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
m : ℕ
h : a ≡ b [ZMOD n]
⊢ a ^ m ≡ b ^ m [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b m : ℤ
h : a ≡ b [ZMOD m * n]
⊢ a ≡ b [ZMOD n]

Tactic:
by

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

Goal state before:
pp: m a b c : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
⊢ a ≡ b [ZMOD m / ↑(m.gcd c)]

Tactic:
by

Goal state after:
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:
by

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

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

Goal state before:
pp: m a b c : ℤ
hc : c ≠ 0
⊢ c * a ≡ c * b [ZMOD c * m] → a ≡ b [ZMOD m]

Tactic:
by

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

Goal state before:
pp: m a b c : ℤ
hc : c ≠ 0
⊢ a * c ≡ b * c [ZMOD m * c] → a ≡ b [ZMOD m]

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ n ∣ a ↔ n ∣ b

Tactic:
by

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

Goal state before:
pp: a : ℤ
⊢ |a| ≡ a [ZMOD 2]

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ n ≡ 0 [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
⊢ a ≡ b [ZMOD |n|] ↔ a ≡ b [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
⊢ a ≡ b [ZMOD ↑n.natAbs] ↔ a ≡ b [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
⊢ a + b ≡ a [ZMOD n] ↔ n ∣ b

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
⊢ a + b ≡ b [ZMOD n] ↔ n ∣ a

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
⊢ a ≡ a + b [ZMOD n] ↔ n ∣ b

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
⊢ b ≡ a + b [ZMOD n] ↔ n ∣ a

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
⊢ a + n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
⊢ n + a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
⊢ a ≡ b + n [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
⊢ a ≡ n + b [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b c : ℤ
⊢ a + b * n ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b c : ℤ
⊢ b * n + a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b c : ℤ
⊢ a ≡ b + c * n [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b c : ℤ
⊢ a ≡ b * n + c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b c : ℤ
⊢ a + n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b c : ℤ
⊢ n * b + a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b c : ℤ
⊢ a ≡ b + n * c [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b c : ℤ
⊢ a ≡ n * b + c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
⊢ a - n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b c : ℤ
⊢ a - n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
⊢ a ≡ b - n [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a b c : ℤ
⊢ a ≡ b - n * c [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by

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

Goal state before:
pp: a b : ℤ
⊢ a ≡ b [ZMOD 0] ↔ a = b

Tactic:
by

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

Goal state before:
pp: n a : ℤ
⊢ n + a ≡ a [ZMOD n]

Tactic:
by

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

Goal state before:
pp: n a : ℤ
⊢ a + n ≡ a [ZMOD n]

Tactic:
by

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

Goal state before:
pp: a b m n : ℤ
⊢ a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD ↑(m.lcm n)]

Tactic:
by

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

Goal state before:
pp: a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
⊢ a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n]

Tactic:
by

Goal state after:
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 : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
⊢ Function.Injective ⇑(Ideal.Quotient.lift I f H)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
a : R
⊢ a ∈ ker f → f a = 0

Tactic:
by

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

Goal state before:
pp: a b : ℕ
⊢ ↑a * a.gcdA b ≡ ↑(a.gcd b) [ZMOD ↑b]

Tactic:
by

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

Goal state before:
pp: a t n : ℤ
⊢ a + n * t ≡ a [ZMOD n]

Tactic:
by

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ ↑a * a.gcdA b ≡ ↑a * a.gcdA b + ↑b * a.gcdB b [ZMOD ↑b]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
g : S → R
hf : Function.RightInverse g ⇑f
⊢ Function.LeftInverse (⇑(Ideal.Quotient.mk (ker f)) ∘ g) ⇑f.kerLift

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
x : R
⊢ (quotientKerEquivOfSurjective hf).symm (f x) = (Ideal.Quotient.mk (ker f)) x

Tactic:
by

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ ↑a * a.gcdA b + ↑b * a.gcdB b ≡ 1 [ZMOD ↑b]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: 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
x : A
⊢ (lift f).toRingHom ↑x = f x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
⊢ (quotientKerEquivOfSurjective hf).symm.toRingHom.comp f = Ideal.Quotient.mk (ker f)

Tactic:
by

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

Goal state before:
pp: a b : ℤ
hb : 0 < b
⊢ a % b < b

Tactic:
by

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

Goal state before:
pp: a b : ℤ
hb : 0 < b
⊢ a % b ≡ a [ZMOD b]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ ker (Quotient.mk I) = I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ≤ J
⊢ map (Quotient.mk J) I = ⊥

Tactic:
by

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

Goal state before:
pp: a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑z.natAbs < b ∧ ↑z.natAbs ≡ a [ZMOD b]

Tactic:
by

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

Goal state before:
pp: n a b : ℤ
h : a / n = b / n
⊢ a ≡ b [ZMOD n] ↔ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: 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
⊢ (lift f).range ≤ S ↔ NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: 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
c : Subalgebra R C
⊢ (lift f).range ≤ c ↔ Algebra.adjoin R ↑(NonUnitalAlgHom.range f) ≤ c

Tactic:
by

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

Goal state before:
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:
Nat.modEq_iff_dvd' hle

Goal state after:
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 : p ∣ b - a
hle : a ≤ b
⊢ ↑a = ↑b
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
⊢ ↑a = ↑b

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
⊢ (unitization s).range = Algebra.adjoin R ↑s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℤ
⊢ ↑a = ↑b ↔ a ≡ b [ZMOD ↑p]

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
⊢ InjOn Int.cast (Ico 0 ↑p)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ 2 = ↑2

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ 2 ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : AddMonoidWithOne S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP S q
⊢ ∀ (x : ℕ), ↑x = 0 ↔ p.lcm q ∣ x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : AddMonoidWithOne S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP S p
⊢ CharP (R × S) p

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ InjOn Int.cast {0, 1, -1}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : CharZero R
p : ℕ
hp : Nat.Prime p
⊢ ↑p ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
⊢ ExpChar (R × S) p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
α : Type u_2
inst✝² : Semiring α
inst✝¹ : IsLeftCancelAdd α
n : ℕ
inst✝ : CharP α n
a b : ℕ
⊢ OfNat.ofNat a = OfNat.ofNat b ↔ a % n = b % n

Tactic:
by

Goal state after:
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 : ∀ a ∈ I, f a = 0
⊢ Injective ⇑(Quotient.lift I f H) ↔ ker f = I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
ι : Type u_1
I : ι → Ideal R
inst✝ : ∀ (i : ι), (I i).IsTwoSided
⊢ ker (RingHom.pi fun i ↦ Quotient.mk (I i)) = ⨅ i, I i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
⊢ ⊥.IsMaximal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
x : R
⊢ (Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J ⊔ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
hIJ : I ≤ J
x : R
⊢ (Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
F : Type w
inst✝² : Ring R
inst✝¹ : Semiring S
ι : Type u_1
I : ι → Ideal R
inst✝ : ∀ (i : ι), (I i).IsTwoSided
⊢ ∀ a ∈ ⨅ i, I i, (RingHom.pi fun i ↦ Quotient.mk (I i)) a = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
ι : Type u_1
I : ι → Ideal R
inst✝ : ∀ (i : ι), (I i).IsTwoSided
⊢ Injective ⇑(quotientInfToPiQuotient I)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i j : ι
hj : j ∈ {i}ᶜ
⊢ i ≠ j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: 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
⊢ Function.Injective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i : ι
⊢ ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : Field R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
⊢ Function.Injective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
he : e ∈ ⨅ j ∈ {i}ᶜ, I j
hue : u + e = 1
⊢ ∀ (j : ι), j ≠ i → e ∈ I j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
x✝ : ↥s
⊢ (unitization s) ↑x✝ = ↑x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
algHom : Unitization R ↥s →ₐ[R] ↥(Algebra.adjoin R ↑s) := (unitization s).codRestrict (Algebra.adjoin R ↑s) ⋯
x✝ : ↥s
⊢ ((Algebra.adjoin R ↑s).val.comp algHom) ↑x✝ = ↑x✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
⊢ ∀ (i : ι), ∃ e, (Quotient.mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) e = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
x : ℤˣ
⊢ x ∈ {1, -1}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
⊢ Nat.card αˣ = Nat.card α - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : Finite α
⊢ Nat.card α = Nat.card αˣ + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
algHom : Unitization R ↥s →ₐ[R] ↥(Algebra.adjoin R ↑s) := (unitization s).codRestrict (Algebra.adjoin R ↑s) ⋯
⊢ Function.Bijective ⇑algHom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card αˣ = card α - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card α = card αˣ + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
⊢ (unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
⊢ (unitization s).range = subalgebraOfSubring (Subring.closure ↑s)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
⊢ ↑n = 0 ↔ 2 ∣ n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ 2 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
n : ℕ
⊢ ↑n = if Even n then 0 else 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ Set.range Nat.cast = {0, 1}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
n : ℕ
⊢ ↑n = ↑(n % 2)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ 37 = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
x : R
⊢ x + x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : (starLift f).range ≤ S
x : A
⊢ (↑(starLift f)).toRingHom ↑x = f x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
x : R
⊢ 2 • x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
a b : R
⊢ a + (a + b) = b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
a b : R
⊢ a + b + b = a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x : R
⊢ -x = x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x y : R
⊢ x - y = x + y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
a b c : R
⊢ a + b = c ↔ a = c + b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
⊢ (starLift f).range ≤ S ↔ NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
⊢ Surjective ⇑(quotientInfToPiQuotient I)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
a b c : R
⊢ a = b + c ↔ a + c = b

Tactic:
by

Goal state after: