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
d : Derivation R A ↥I
⊢ (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) ((fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩) d) = 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
d : Derivation R A ↥I
⊢ (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) ((fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩) d) = d
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
d : Derivation R A ↥I
x : A
⊢ ↑(((fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) ((fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩) d)) x) =
    ↑(d x)

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
d : Derivation R A ↥I
x : A
⊢ ↑(((fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) ((fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩) d)) x) =
    ↑(d x)
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
f : A →ₐ[R] B
hf : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
⊢ (fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩) ((fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) ⟨f, hf⟩) =
    ⟨f, hf⟩

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
f : A →ₐ[R] B
hf : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
⊢ (fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩) ((fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) ⟨f, hf⟩) =
    ⟨f, hf⟩
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
f : A →ₐ[R] B
hf : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x : A
⊢ ↑((fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩) ((fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) ⟨f, hf⟩)) x =
    ↑⟨f, hf⟩ x

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
f : A →ₐ[R] B
hf : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x : A
⊢ ↑((fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩) ((fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) ⟨f, hf⟩)) x =
    ↑⟨f, hf⟩ x
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : G ≃*o H
a✝ : G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ }) e))
      a✝ =
    e a✝

Tactic:
;

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : G ≃*o H
a✝ : G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ }) e))
      a✝ =
    e a✝
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o Additive H
a✝ : Additive G
⊢ Additive.toMul
      (((fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ })
          ((fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, map_le_map_iff' := ⋯ }) e))
        a✝) =
    Additive.toMul (e a✝)

Tactic:
;

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o Additive H
a✝ : Additive G
⊢ Additive.toMul
      (((fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ })
          ((fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, map_le_map_iff' := ⋯ }) e))
        a✝) =
    Additive.toMul (e a✝)
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃+o H
a✝ : G
⊢ ((fun e ↦ { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicative ↑e, map_le_map_iff' := ⋯ }) e))
      a✝ =
    e a✝

Tactic:
;

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃+o H
a✝ : G
⊢ ((fun e ↦ { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicative ↑e, map_le_map_iff' := ⋯ }) e))
      a✝ =
    e a✝
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o Multiplicative H
a✝ : Multiplicative G
⊢ Multiplicative.toAdd
      (((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicative ↑e, map_le_map_iff' := ⋯ })
          ((fun e ↦ { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ }) e))
        a✝) =
    Multiplicative.toAdd (e a✝)

Tactic:
;

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o Multiplicative H
a✝ : Multiplicative G
⊢ Multiplicative.toAdd
      (((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicative ↑e, map_le_map_iff' := ⋯ })
          ((fun e ↦ { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ }) e))
        a✝) =
    Multiplicative.toAdd (e a✝)
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o H
a✝ : Additive G
⊢ ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveLeft e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeRight e.toAddEquiv, map_le_map_iff' := ⋯ }) e))
      a✝ =
    e a✝

Tactic:
;

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o H
a✝ : Additive G
⊢ ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveLeft e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeRight e.toAddEquiv, map_le_map_iff' := ⋯ }) e))
      a✝ =
    e a✝
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃*o Multiplicative H
a✝ : G
⊢ Multiplicative.toAdd
      (((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeRight e.toAddEquiv, map_le_map_iff' := ⋯ })
          ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveLeft e.toMulEquiv, map_le_map_iff' := ⋯ }) e))
        a✝) =
    Multiplicative.toAdd (e a✝)

Tactic:
;

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃*o Multiplicative H
a✝ : G
⊢ Multiplicative.toAdd
      (((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeRight e.toAddEquiv, map_le_map_iff' := ⋯ })
          ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveLeft e.toMulEquiv, map_le_map_iff' := ⋯ }) e))
        a✝) =
    Multiplicative.toAdd (e a✝)
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : G ≃+o Additive H
a✝ : G
⊢ Additive.toMul
      (((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveRight e.toMulEquiv, map_le_map_iff' := ⋯ })
          ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeLeft e.toAddEquiv, map_le_map_iff' := ⋯ }) e))
        a✝) =
    Additive.toMul (e a✝)

Tactic:
;

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : G ≃+o Additive H
a✝ : G
⊢ Additive.toMul
      (((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveRight e.toMulEquiv, map_le_map_iff' := ⋯ })
          ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeLeft e.toAddEquiv, map_le_map_iff' := ⋯ }) e))
        a✝) =
    Additive.toMul (e a✝)
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o H
a✝ : Multiplicative G
⊢ ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeLeft e.toAddEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveRight e.toMulEquiv, map_le_map_iff' := ⋯ }) e))
      a✝ =
    e a✝

Tactic:
;

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o H
a✝ : Multiplicative G
⊢ ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeLeft e.toAddEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveRight e.toMulEquiv, map_le_map_iff' := ⋯ }) e))
      a✝ =
    e a✝
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑g
hf : (g.comp f).Flat
e : S ≃+* T := RingEquiv.ofBijective g hg
x✝ : R
⊢ f x✝ = (e.symm.toRingHom.comp (e.toRingHom.comp f)) x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑g
hf : (g.comp f).Flat
e : S ≃+* T := RingEquiv.ofBijective g hg
x✝ : R
⊢ f x✝ = (e.symm.toRingHom.comp (e.toRingHom.comp f)) x✝
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : T →+* R
hg : Function.Bijective ⇑g
hf : (f.comp g).Flat
e : T ≃+* R := RingEquiv.ofBijective g hg
x✝ : R
⊢ f x✝ = ((f.comp e.toRingHom).comp e.symm.toRingHom) x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : T →+* R
hg : Function.Bijective ⇑g
hf : (f.comp g).Flat
e : T ≃+* R := RingEquiv.ofBijective g hg
x✝ : R
⊢ f x✝ = ((f.comp e.toRingHom).comp e.symm.toRingHom) x✝
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
⊢ (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1).Coprime
    (if b.factorization q ≤ a.factorization q then 1 else q ^ (a.lcm b).factorization q)

Tactic:
;

Goal state after:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
⊢ (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1).Coprime
    (if b.factorization q ≤ a.factorization q then 1 else q ^ (a.lcm b).factorization q)
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : p = q
⊢ b.factorization q ≤ a.factorization q

Tactic:
;

Goal state after:
case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : p = q
⊢ b.factorization q ≤ a.factorization q
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case e_g
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (fun a_1 b_1 ↦
      (if b.factorization a_1 ≤ a.factorization a_1 then a_1 ^ b_1 else 1) *
        if b.factorization a_1 ≤ a.factorization a_1 then 1 else a_1 ^ b_1) =
    fun x1 x2 ↦ x1 ^ x2

Tactic:
;

Goal state after:
case e_g
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (fun a_1 b_1 ↦
      (if b.factorization a_1 ≤ a.factorization a_1 then a_1 ^ b_1 else 1) *
        if b.factorization a_1 ≤ a.factorization a_1 then 1 else a_1 ^ b_1) =
    fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case e_g
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
⊢ ((if b.factorization p ≤ a.factorization p then p ^ n else 1) *
      if b.factorization p ≤ a.factorization p then 1 else p ^ n) =
    p ^ n

Tactic:
;

Goal state after:
case e_g
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
⊢ ((if b.factorization p ≤ a.factorization p then p ^ n else 1) *
      if b.factorization p ≤ a.factorization p then 1 else p ^ n) =
    p ^ n
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
U : Set (PrimeSpectrum R)
⊢ IsOpen U ↔ ∃ s, zeroLocus s = Uᶜ

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
U : Set (PrimeSpectrum R)
⊢ IsOpen U ↔ ∃ s, zeroLocus s = Uᶜ
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1) i ((a.lcm b).factorization i) ∣
      i ^ a.factorization i

Tactic:
;

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1) i ((a.lcm b).factorization i) ∣
      i ^ a.factorization i
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1) p ((a.lcm b).factorization p) ∣
    p ^ a.factorization p

Tactic:
;

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1) p ((a.lcm b).factorization p) ∣
    p ^ a.factorization p
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) ∣ p ^ a.factorization p

Tactic:
;

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) ∣ p ^ a.factorization p
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.factorization ⊔ b.factorization) p ∣ 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.factorization ⊔ b.factorization) p ∣ p ^ a.factorization p
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
⊢ (a.factorization ⊔ b.factorization) 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
⊢ (a.factorization ⊔ b.factorization) p ≤ a.factorization p
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
;

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

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

Tactic:
;

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

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

Tactic:
;

Goal state after:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.factorization.support
⊢ p ∈ (a.lcm b).factorization.support
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : a.factorization p ≠ 0
⊢ (a.factorization ⊔ b.factorization) p ≠ 0

Tactic:
;

Goal state after:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : a.factorization p ≠ 0
⊢ (a.factorization ⊔ b.factorization) p ≠ 0
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
i✝ : ℕ
a✝ : 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✝ : i✝ ∈ (a.lcm b).factorization.support
⊢ i✝ ^ 0 = 1
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n) i ((a.lcm b).factorization i) ∣
      i ^ b.factorization i

Tactic:
;

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n) i ((a.lcm b).factorization i) ∣
      i ^ b.factorization i
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n) p ((a.lcm b).factorization p) ∣
    p ^ b.factorization p

Tactic:
;

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n) p ((a.lcm b).factorization p) ∣
    p ^ b.factorization p
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) ∣ p ^ b.factorization p

Tactic:
;

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) ∣ p ^ b.factorization p
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
⊢ p ^ (a.factorization ⊔ b.factorization) p ∣ p ^ b.factorization p

Tactic:
;

Goal state after:
case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ p ^ (a.factorization ⊔ b.factorization) p ∣ p ^ b.factorization p
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
⊢ (a.factorization ⊔ b.factorization) p ≤ b.factorization p

Tactic:
;

Goal state after:
case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ (a.factorization ⊔ b.factorization) p ≤ b.factorization p
Module: Mathlib.Data.Nat.Factorization.LCM

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

Tactic:
;

Goal state after:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ b.factorization.support
⊢ p ∈ (a.lcm b).factorization.support
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : b.factorization p ≠ 0
⊢ (a.factorization ⊔ b.factorization) p ≠ 0

Tactic:
;

Goal state after:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : b.factorization p ≠ 0
⊢ (a.factorization ⊔ b.factorization) p ≠ 0
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case mk
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : Module R M
D D1 D2✝ : Derivation R A M
r : R
a b : A
D2 : Derivation R A M
toLinearMap✝ : A →ₗ[R] M
map_one_eq_zero'✝ : toLinearMap✝ 1 = 0
leibniz'✝ : ∀ (a b : A), toLinearMap✝ (a * b) = a • toLinearMap✝ b + b • toLinearMap✝ a
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ } =
    (fun D ↦ D.toFun) D2
⊢ { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ } = D2

Tactic:
;

Goal state after:
case mk
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : Module R M
D D1 D2✝ : Derivation R A M
r : R
a b : A
D2 : Derivation R A M
toLinearMap✝ : A →ₗ[R] M
map_one_eq_zero'✝ : toLinearMap✝ 1 = 0
leibniz'✝ : ∀ (a b : A), toLinearMap✝ (a * b) = a • toLinearMap✝ b + b • toLinearMap✝ a
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ } =
    (fun D ↦ D.toFun) D2
⊢ { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ } = D2