mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_2
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
⊢ Function.LeftInverse (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩

pp: case refine_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
⊢ Function.RightInverse (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) fun d ↦
    ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩

Tactic:
·

Goal state after:
case refine_2
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
⊢ Function.LeftInverse (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
⊢ Function.RightInverse (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) fun d ↦
    ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩

Tactic:
·

Goal state after:
case refine_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
⊢ Function.RightInverse (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) fun d ↦
    ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := ⋯
⊢ ∀ (P : Ideal S) [inst : P.IsMaximal], Module.Flat R (Localization.AtPrime P)

Tactic:
intro P _

Goal state after:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
P : Ideal S
inst✝ : P.IsMaximal
⊢ Module.Flat R (Localization.AtPrime P)
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
⊢ (↑(Algebra.TensorProduct.map (AlgHom.id S A) g)).Flat

pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
⊢ (Algebra.TensorProduct.map f (AlgHom.id R D)).Flat

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
⊢ (↑(Algebra.TensorProduct.map (AlgHom.id S A) g)).Flat
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
⊢ (Algebra.TensorProduct.map f (AlgHom.id R D)).Flat

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
⊢ (Algebra.TensorProduct.map f (AlgHom.id R D)).Flat
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case pos
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
h : b.factorization p ≤ a.factorization p
⊢ False

pp: case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
h : ¬b.factorization p ≤ a.factorization p
⊢ False

Tactic:
·

Goal state after:
case pos
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
h : b.factorization p ≤ a.factorization p
⊢ False
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
h : ¬b.factorization p ≤ a.factorization p
⊢ False

Tactic:
·

Goal state after:
case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
h : ¬b.factorization p ≤ a.factorization p
⊢ False
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case pos
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) = 0
h : b.factorization p ≤ a.factorization p
⊢ False

pp: case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) = 0
h : ¬b.factorization p ≤ a.factorization p
⊢ False

Tactic:
·

Goal state after:
case pos
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) = 0
h : b.factorization p ≤ a.factorization p
⊢ False
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) = 0
h : ¬b.factorization p ≤ a.factorization p
⊢ False

Tactic:
·

Goal state after:
case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) = 0
h : ¬b.factorization p ≤ a.factorization p
⊢ False
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : (ulift.{u₁, u₂, u_1, u_2} f).Flat
⊢ f.Flat

pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Flat
⊢ (ulift.{u₁, u₂, u_1, u_2} f).Flat

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : (ulift.{u₁, u₂, u_1, u_2} f).Flat
⊢ f.Flat
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Flat
⊢ (ulift.{u₁, u₂, u_1, u_2} f).Flat

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Flat
⊢ (ulift.{u₁, u₂, u_1, u_2} f).Flat
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inl
b : ℕ
⊢ factorizationLCMLeft 0 b ∣ 0

pp: case inr
a b : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMLeft b ∣ a

Tactic:
·

Goal state after:
case inl
b : ℕ
⊢ factorizationLCMLeft 0 b ∣ 0
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inl
a : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMLeft 0 ∣ a

pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ a

Tactic:
·

Goal state after:
case inr.inl
a : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMLeft 0 ∣ a
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ CommRingCat.of (S ⊗[R] S) ⟶ CommRingCat.of (T ⊗[R] A)

pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ CommRingCat.of S ⟶ CommRingCat.of (T ⊗[S] A)

pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ IsPushout ?m.67 (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom) ?m.69

Tactic:
·

Goal state after:
R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ CommRingCat.of (S ⊗[R] S) ⟶ CommRingCat.of (T ⊗[R] A)
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ ∏ x ∈ (a.lcm b).factorization.support, x ^ a.factorization x

pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization.support ⊆ (a.lcm b).factorization.support

pp: case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1

Tactic:
·

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ ∏ x ∈ (a.lcm b).factorization.support, x ^ a.factorization x
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ CommRingCat.of S ⟶ CommRingCat.of (T ⊗[S] A)

pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ IsPushout
    (CommRingCat.ofHom
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A)).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom) ?m.69

Tactic:
·

Goal state after:
R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ CommRingCat.of S ⟶ CommRingCat.of (T ⊗[S] A)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
I : Set R
hI : closure t = zeroLocus I
⊢ zeroLocus ↑(vanishingIdeal t) = closure t

Tactic:
subset_antisymm_iff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
I : Set R
hI : closure t = zeroLocus I
⊢ zeroLocus ↑(vanishingIdeal t) ⊆ closure t ∧ closure t ⊆ zeroLocus ↑(vanishingIdeal t)
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ p ^ (a.lcm b).factorization p ∣ p ^ a.factorization p

pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ 1 ∣ p ^ a.factorization p

Tactic:
·

Goal state after:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ p ^ (a.lcm b).factorization p ∣ p ^ a.factorization p
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ IsPushout
    (CommRingCat.ofHom
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A)).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.includeLeft.comp (algebraMap S T)))

Tactic:
·

Goal state after:
R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ IsPushout
    (CommRingCat.ofHom
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A)).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.includeLeft.comp (algebraMap S T)))
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ 1 ∣ p ^ a.factorization p

Tactic:
·

Goal state after:
case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ 1 ∣ p ^ a.factorization p
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : zeroLocus ↑x.asIdeal ⊆ {x}
⊢ x.asIdeal.IsMaximal

pp: case mpr
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : x.asIdeal.IsMaximal
⊢ zeroLocus ↑x.asIdeal ⊆ {x}

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : zeroLocus ↑x.asIdeal ⊆ {x}
⊢ x.asIdeal.IsMaximal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : x.asIdeal.IsMaximal
⊢ zeroLocus ↑x.asIdeal ⊆ {x}

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : x.asIdeal.IsMaximal
⊢ zeroLocus ↑x.asIdeal ⊆ {x}
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ zeroLocus ↑I = zeroLocus ↑J → I.radical = J.radical

pp: case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I.radical = J.radical → zeroLocus ↑I = zeroLocus ↑J

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ zeroLocus ↑I = zeroLocus ↑J → I.radical = J.radical
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization.support ⊆ (a.lcm b).factorization.support

pp: case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1

Tactic:
·

Goal state after:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization.support ⊆ (a.lcm b).factorization.support
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I.radical = J.radical → zeroLocus ↑I = zeroLocus ↑J

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I.radical = J.radical → zeroLocus ↑I = zeroLocus ↑J
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
⊢ T1Space (PrimeSpectrum R) → IsField R

pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
⊢ T1Space (PrimeSpectrum R)

Tactic:
·

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
⊢ T1Space (PrimeSpectrum R) → IsField R
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
⊢ T1Space (PrimeSpectrum R)

Tactic:
·

Goal state after:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
⊢ T1Space (PrimeSpectrum R)
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1

Tactic:
·

Goal state after:
case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
⊢ x.asIdeal.IsMaximal

pp: case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : ¬x.asIdeal = ⊥
⊢ x.asIdeal.IsMaximal

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
⊢ x.asIdeal.IsMaximal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : ¬x.asIdeal = ⊥
⊢ x.asIdeal.IsMaximal

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : ¬x.asIdeal = ⊥
⊢ x.asIdeal.IsMaximal
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inl
b : ℕ
⊢ factorizationLCMRight 0 b ∣ b

pp: case inr
a b : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMRight b ∣ b

Tactic:
·

Goal state after:
case inl
b : ℕ
⊢ factorizationLCMRight 0 b ∣ b
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inl
a : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMRight 0 ∣ 0

pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMRight b ∣ b

Tactic:
·

Goal state after:
case inr.inl
a : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMRight 0 ∣ 0
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case h₁
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (zeroLocus ↑I).Nonempty ↔ I ≠ ⊤

pp: case h₂
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsPreirreducible (zeroLocus ↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
·

Goal state after:
case h₁
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (zeroLocus ↑I).Nonempty ↔ I ≠ ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case h₂
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsPreirreducible (zeroLocus ↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
·

Goal state after:
case h₂
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsPreirreducible (zeroLocus ↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsPreirreducible (zeroLocus ↑I) ↔
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y

pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) ↔
    ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
·

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsPreirreducible (zeroLocus ↑I) ↔
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMRight b ∣ ∏ x ∈ (a.lcm b).factorization.support, x ^ b.factorization x

pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ b.factorization.support ⊆ (a.lcm b).factorization.support

pp: case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1

Tactic:
·

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMRight b ∣ ∏ x ∈ (a.lcm b).factorization.support, x ^ b.factorization x