mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring 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✝¹ : Ring R
inst✝ : CharP R 2
a b : R
⊢ a + b = 0 ↔ 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✝⁹ : 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
c : StarSubalgebra R C
⊢ (starLift f).range ≤ c ↔ StarAlgebra.adjoin R ↑(NonUnitalStarAlgHom.range f) ≤ c

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
hf : Pairwise (IsCoprime on I)
x : (i : ι) → R ⧸ I i
⊢ ∃ r, ∀ (i : ι), (Quotient.mk (I i)) r = x 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)
x : ι → R
⊢ ∃ r, ∀ (i : ι), r - x i ∈ I 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
n : ℤ
⊢ ↑n = if Even n then 0 else 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✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : Semiring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
⊢ (unitization s).range = StarAlgebra.adjoin R ↑s

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✝⁶ : StarRing R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
h1 : 1 ∉ s
x✝ : ↥s
⊢ (unitization s) ↑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
⊢ Set.range Int.cast = {0, 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✝⁶ : StarRing R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R ↑s) :=
  (unitization s).codRestrict (StarAlgebra.adjoin R ↑s) ⋯
x✝ : ↥s
⊢ ((StarAlgebra.adjoin R ↑s).subtype.comp starAlgHom) ↑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
n : ℤ
⊢ ↑n = ↑(n % 2)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
x y : R
⊢ (x + y) ^ 2 = x ^ 2 + y ^ 2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
x y : R
⊢ (x + y) * (x + y) = x * x + y * y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
l : List R
⊢ l.sum * l.sum = (List.map (fun x ↦ x * x) l).sum

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
l : Multiset R
⊢ l.sum * l.sum = (Multiset.map (fun x ↦ x * x) l).sum

Tactic:
by

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
s : Finset ι
f : ι → R
⊢ (∑ i ∈ s, f i) * ∑ i ∈ s, f i = ∑ i ∈ s, f i * f i

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R 2
inst✝ : NoZeroDivisors R
⊢ Function.Injective fun x ↦ x ^ 2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ -1 = 1 ↔ ringChar R = 2

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✝⁶ : StarRing R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R ↑s) :=
  (unitization s).codRestrict (StarAlgebra.adjoin R ↑s) ⋯
⊢ Function.Bijective ⇑starAlgHom

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
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
⊢ Pairwise (IsCoprime on f)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: a b : ℕ
⊢ Prime (a * b) ↔ Prime a ∧ b = 1 ∨ Prime b ∧ a = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: a b : ℕ
a1 : a ≠ 1
b1 : b ≠ 1
⊢ ¬Prime (a * b)

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
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
hf : Pairwise (IsCoprime on f)
⊢ I ⊓ J = ⨅ i, f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ p = a → a ∣ p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p ↔ p = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
h : p % 2 = 0
⊢ ¬2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
⊢ 5 ≤ p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ ¬Prime n ↔ ∃ a b, a < n ∧ b < n ∧ a * b = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
⊢ a ∣ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ Even p ↔ p = 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ Odd p ↔ 3 ≤ p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
h2 : p ≠ 2
n : ℕ
hn : p = 2 * n + 1
⊢ p - 1 = n + n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p % 2 = 1 ↔ p ≠ 2

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ (fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = factor ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: m n : ℕ
⊢ ¬m.Coprime n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
p : ℕ
hp : Prime p
hn : p ∣ n
hm : p ∣ m
⊢ 0 < m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ n.Coprime m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p m n : ℕ
pp : Prime p
Hm : ¬p ∣ m
Hn : ¬p ∣ n
⊢ ¬(p ∣ m ∨ p ∣ n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: n : ℕ
⊢ Coprime 2 n ↔ Odd n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
⊢ a ^ k = p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p a k : ℕ
hp : Prime p
⊢ a ^ k = p ↔ a = p ∧ k = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ (snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = factor ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
⊢ p ∣ x * y

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ (fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime) = factor ⋯

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ (snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime) = factor ⋯

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
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ ∀ (r : R₁) (x : A ⧸ I), ((mk I).comp (algebraMap R₁ A)) r * x = x * ((mk I).comp (algebraMap R₁ A)) r

Tactic:
by

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

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
h : I = ⊥
⊢ ker (mk I) = ⊥

Tactic:
by

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

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ Bijective ⇑(mk I) ↔ I = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
⊢ factorₐ R ⋯ = AlgHom.id R (A ⧸ I)

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
inst✝⁵ : CommSemiring R₁
inst✝⁴ : Ring A
inst✝³ : Algebra R₁ A
I J : Ideal A
inst✝² : I.IsTwoSided
inst✝¹ : J.IsTwoSided
hIJ : I ≤ J
K : Ideal A
inst✝ : K.IsTwoSided
hJK : J ≤ K
⊢ ((factorₐ R₁ hJK).comp (factorₐ R₁ hIJ)).comp (mkₐ R₁ I) = (factorₐ R₁ ⋯).comp (mkₐ R₁ I)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
⊢ x = p ∧ y = p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
⊢ p = a * y

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
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Semiring B
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : I.IsTwoSided
f : A →ₐ[R₁] B
hI : ∀ a ∈ I, f a = 0
r : R₁
⊢ (↑↑(lift I (↑f) hI)).toFun ((algebraMap R₁ (A ⧸ I)) r) = (algebraMap R₁ B) r

Tactic:
by

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

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ A ∙ 1 = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_5
inst✝ : CommRing R
a : R
I : Ideal R
⊢ a • ⊤ = R ∙ Submodule.Quotient.mk a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
⊢ x * y = p ^ 2 ↔ x = p ∧ y = p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
pp : Prime p
i : ℕ
⊢ p.Coprime i ∨ p ∣ i

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
x : A ⧸ ker f
⊢ f.kerLift (r • x) = r • f.kerLift x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
pp : Prime p
m i : ℕ
⊢ i ∣ p ^ m ↔ ∃ k, k ≤ m ∧ i = p ^ k

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
a : A
⊢ (kerLiftAlg f) ((Quotient.mk (ker f)) a) = f a

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
hf : Surjective ⇑f
a : A
⊢ (quotientKerAlgEquivOfSurjective hf).symm (f a) = (Quotient.mk (ker f)) a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: a p k : ℕ
pp : Prime p
h₁ : ¬a ∣ p ^ k
h₂ : a ∣ p ^ (k + 1)
⊢ a = p ^ (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: ⊢ 0 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: ⊢ 1 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 1

Tactic:
simp [Nat.not_prime_one]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: ⊢ 1 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: n : ℕ
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: n : ℕ
⊢ n = 1 ↔ ∀ (p : ℕ), Prime p → ¬p ∣ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
⊢ p ^ (k + l) * p ∣ m * n

Tactic:
by

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

Goal state before:
pp: R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Surjective ⇑f
g : A →ₐ[R] C
H : ker f.toRingHom ≤ ker g.toRingHom
x : A
⊢ (f.liftOfSurjective hf g H) (f x) = g x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
⊢ p ∣ m * n / (p ^ k * p ^ l)

Tactic:
by

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

Goal state before:
pp: R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Surjective ⇑f
g : A →ₐ[R] C
H : ker f.toRingHom ≤ ker g.toRingHom
⊢ (f.liftOfSurjective hf g H).comp f = g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
⊢ p ∣ m / p ^ k * (n / p ^ l)

Tactic:
by

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

Goal state before:
pp: R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Surjective ⇑f
g : A →ₐ[R] C
H : ker f.toRingHom ≤ ker g.toRingHom
hg : Surjective ⇑g
⊢ Surjective (⇑(f.liftOfSurjective hf g H) ∘ ⇑f)

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✝
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
S : Type v
inst✝² : Ring S
I : Ideal R
J : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R →+* S
hIJ : I ≤ comap f J
x✝ : R
ha : x✝ ∈ I
⊢ ((Quotient.mk J).comp f) x✝ = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S : Type v
inst✝² : Ring S
J : Ideal R
I : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
x : R
⊢ ((quotientMap I f H).comp (Quotient.mk J)) x = ((Quotient.mk I).comp f) x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
this : p ^ k * p ∣ m ∨ p ^ l * p ∣ n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n

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
inst✝ : J.IsTwoSided
⊢ ker (quotientMap (map (Quotient.mk I) J) (Quotient.mk I) ⋯) = map (Quotient.mk J) I

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✝
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
S : Type v
inst✝² : Ring S
I : Ideal R
J : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R ≃+* S
hIJ : J = map (↑f) I
⊢ LeftInverse (⇑(quotientMap I ↑f.symm ⋯)) (↑↑(quotientMap J ↑f ⋯)).toFun

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✝
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
S : Type v
inst✝² : Ring S
I : Ideal R
J : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R ≃+* S
hIJ : J = map (↑f) I
⊢ RightInverse (⇑(quotientMap I ↑f.symm ⋯)) (↑↑(quotientMap J ↑f ⋯)).toFun

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : Type u_1
s : Multiset α
l l' : List α
h : l ~ l'
⊢ ↑l.permutations = ↑l'.permutations

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : Type u_1
l : Finset α
⊢ l.val.lists.Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
⊢ l ∈ s.lists ↔ s = ⟦l⟧

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S : Type v
inst✝² : Ring S
J : Ideal R
I : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
⊢ Injective ⇑(quotientMap I f H)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S : Type v
inst✝² : Ring S
J : Ideal R
I : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
hf : Surjective ⇑f
x✝ : S ⧸ I
x : S
hx : (Quotient.mk I) x = x✝
y : R
hy : f y = x
⊢ (quotientMap I f H) ((Quotient.mk J) y) = x✝

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
S : Type v
inst✝³ : Ring S
R' : Type u_5
S' : Type u_6
inst✝² : Ring R'
inst✝¹ : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst✝ : I.IsTwoSided
⊢ let leq := ⋯;
  (quotientMap I g' ⋯).comp (quotientMap (comap g' I) f ⋯) = (quotientMap I f' ⋯).comp (quotientMap (comap f' I) g leq)

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
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : Ring A
inst✝⁵ : Algebra R₁ A
inst✝⁴ : Algebra R₂ A
inst✝³ : Ring B
inst✝² : Algebra R₁ B
I : Ideal A
J : Ideal B
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : A →ₐ[R₁] B
hIJ : I ≤ comap f J
r : R₁
⊢ (↑↑(quotientMap J (↑f) hIJ)).toFun ((algebraMap R₁ (A ⧸ I)) r) = (algebraMap R₁ (B ⧸ J)) r

Tactic:
by

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

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Ring B
inst✝² : Algebra R₁ B
I : Ideal A
J : Ideal B
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : A →ₐ[R₁] B
H : I ≤ comap f J
x : A
⊢ ((quotientMapₐ J f H).comp (Quotient.mkₐ R₁ I)) x = ((Quotient.mkₐ R₁ J).comp f) x

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
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : Ring A
inst✝⁵ : Algebra R₁ A
inst✝⁴ : Algebra R₂ A
inst✝³ : Ring B
inst✝² : Algebra R₁ B
I : Ideal A
J : Ideal B
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : A ≃ₐ[R₁] B
hIJ : J = map (↑f) I
r : R₁
⊢ (I.quotientEquiv J f.toRingEquiv hIJ).toFun ((algebraMap R₁ (A ⧸ I)) r) = (algebraMap R₁ (B ⧸ J)) r

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
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : Ring A
inst✝⁵ : Algebra R₁ A
inst✝⁴ : Algebra R₂ A
inst✝³ : Ring B
inst✝² : Algebra R₁ B
I : Ideal A
J : Ideal B
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : A ≃ₐ[R₁] B
hIJ : J = map (↑f) I
⊢ I = map (↑f.symm) J

Tactic:
by

Goal state after: