mathlib-initiative/mathlib-tactics huggingface dataset:
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 b : Multiplicative G},
    (AddEquiv.toMultiplicativeLeft e.toAddEquiv).toFun a ≤ (AddEquiv.toMultiplicativeLeft e.toAddEquiv).toFun b ↔ a ≤ b

Tactic:
by

Goal state after:
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 b : G}, (MulEquiv.toAdditiveRight e.toMulEquiv).toFun a ≤ (MulEquiv.toAdditiveRight e.toMulEquiv).toFun b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: 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
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 D
inst✝ : Algebra R D
f : B →ₐ[R] D
hf : f.Flat
⊢ (Algebra.TensorProduct.lTensor A f).Flat

Tactic:
by

Goal state after:
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
⊢ (fun e ↦ { toAddEquiv := MulEquiv.toAdditiveRight e.toMulEquiv, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeLeft e.toAddEquiv, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
by

Goal state after:
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
⊢ (fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeLeft e.toAddEquiv, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveRight e.toMulEquiv, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Aut

Goal state before:
pp: n : ℕ
f : AddAut (ZMod n)
x : ZMod n
⊢ f 1 * x = f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Aut

Goal state before:
pp: n : ℕ
h : ∀ (f : AddAut (ZMod n)) (x : ZMod n), f 1 * x = f x
g : AddAut (ZMod n)
⊢ (fun x ↦ AddAut.mulLeft (Additive.toMul x)) ((fun f ↦ Additive.ofMul (Units.mkOfMulEqOne (f 1) ((-f) 1) ⋯)) g) = g

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Aut

Goal state before:
pp: n : ℕ
h : ∀ (f : AddAut (ZMod n)) (x : ZMod n), f 1 * x = f x
x : Additive (ZMod n)ˣ
⊢ (fun f ↦ Additive.ofMul (Units.mkOfMulEqOne (f 1) ((-f) 1) ⋯)) ((fun x ↦ AddAut.mulLeft (Additive.toMul x)) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.ZMod.Aut

Goal state before:
pp: n : ℕ
h : ∀ (f : AddAut (ZMod n)) (x : ZMod n), f 1 * x = f x
f g : AddAut (ZMod n)
⊢ Additive.ofMul (Units.mkOfMulEqOne ((f + g) 1) ((-(f + g)) 1) ⋯) =
    Additive.ofMul (Units.mkOfMulEqOne (f 1) ((-f) 1) ⋯) + Additive.ofMul (Units.mkOfMulEqOne (g 1) ((-g) 1) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: 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
⊢ Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: 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)
⊢ AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D)) =
    (↑(Algebra.TensorProduct.comm R D C)).comp
      ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑(Algebra.TensorProduct.comm R A D))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: 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
⊢ (Algebra.TensorProduct.map f g).Flat

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: b : ℕ
⊢ factorizationLCMLeft 0 b = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a : ℕ
⊢ a.factorizationLCMLeft 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: b : ℕ
⊢ factorizationLCMRight 0 b = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a : ℕ
⊢ a.factorizationLCMRight 0 = 1

Tactic:
by

Goal state after:
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
⊢ f = e.symm.toRingHom.comp (e.toRingHom.comp f)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
⊢ 0 < a.factorizationLCMLeft b

Tactic:
by

Goal state after:
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
⊢ (g.comp f).Flat ↔ f.Flat

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
⊢ 0 < a.factorizationLCMRight b

Tactic:
by

Goal state after:
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
⊢ f = (f.comp e.toRingHom).comp e.symm.toRingHom

Tactic:
by

Goal state after:
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
⊢ (f.comp g).Flat ↔ f.Flat

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Flat

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf : Function.Injective ⇑(ConcreteCategory.hom f)
hg : (Hom.hom g).Flat
⊢ Function.Injective ⇑(ConcreteCategory.hom (pushout.inr f g))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
⊢ (a.factorizationLCMLeft b).Coprime (a.factorizationLCMRight b)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ zeroLocus Set.univ = ∅

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf : (Hom.hom f).Flat
hg : Function.Injective ⇑(ConcreteCategory.hom g)
⊢ Function.Injective ⇑(ConcreteCategory.hom (pushout.inl f g))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: ⊢ flat.IsStableUnderCobaseChange

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ ∀ A ⊆ Set.range zeroLocus, ⋂₀ A ∈ Set.range zeroLocus

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ ∀ A ∈ Set.range zeroLocus, ∀ B ∈ Set.range zeroLocus, A ∪ B ∈ Set.range zeroLocus

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b * a.factorizationLCMRight b = a.lcm b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ IsClosed (zeroLocus s)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
rcases isClosed_iff_zeroLocus (closure t) |>.mp isClosed_closure with ⟨I, hI⟩
  rw [subset_antisymm_iff, (isClosed_zeroLocus _).closure_subset_iff, hI,
      subset_zeroLocus_iff_subset_vanishingIdeal, (gc R).u_l_u_eq_u,
      ← subset_zeroLocus_iff_subset_vanishingIdeal, ← hI]
  exact ⟨subset_closure, subset_zeroLocus_vanishingIdeal t⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ closure {x} = zeroLocus ↑x.asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsClosed {x} ↔ x.asIdeal.IsMaximal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (vanishingIdeal s).IsRadical

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ s ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
hs : IsClosed s
ht : IsClosed t
⊢ s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
⊢ ¬{ asIdeal := ⊥, isPrime := ⋯ }.asIdeal ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
⊢ a.factorizationLCMLeft b ∣ a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
by

Goal state after:
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.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T) = CommRingCat.ofHom (algebraMap R T)

Tactic:
by

Goal state after:
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:
exact sup_le (not_le.1 le).le le_rfl

Goal state after:
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.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A) = CommRingCat.ofHom (algebraMap R A)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
⊢ a.factorizationLCMRight b ∣ b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsIrreducible (zeroLocus ↑I) ↔ I.IsPrime

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsIrreducible s ↔ (vanishingIdeal s).IsPrime

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s} = {P | P.IsPrime}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ IrreducibleSpace (PrimeSpectrum R) ↔ (nilradical R).IsPrime

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : IsDomain R
⊢ IrreducibleSpace (PrimeSpectrum R)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
⊢ IsGenericPoint { asIdeal := vanishingIdeal S, isPrime := ⋯ } S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
ι✝ : Type u
S : ι✝ → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι✝), IsClosed (S i)
I : ι✝ → Ideal R
hI : ∀ (i : ι✝), S i = zeroLocus ↑(I i)
S_empty : ⋂ i, zeroLocus ↑(I i) = ∅
⊢ ∃ u, ⋂ i ∈ u, zeroLocus ↑(I i) = ∅

Tactic:
← zeroLocus_iSup,

Goal state after:
R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
ι✝ : Type u
S : ι✝ → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι✝), IsClosed (S i)
I : ι✝ → Ideal R
hI : ∀ (i : ι✝), S i = zeroLocus ↑(I i)
S_empty : zeroLocus ↑(⨆ i, I i) = ∅
⊢ ∃ u, zeroLocus ↑(⨆ i ∈ u, I i) = ∅
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: 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
D1 D2 : Derivation R A M
h : (fun D ↦ D.toFun) D1 = (fun D ↦ D.toFun) D2
⊢ D1 = D2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ CompactSpace (PrimeSpectrum R)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
r : R
⊢ D ((algebraMap R A) r) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
n : ℕ
⊢ D ↑n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Peel

Goal state before:
pp: p q r : Prop
h : r → p → q
⊢ r ∧ p → r ∧ q

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Peel

Goal state before:
pp: α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x ↔ q x
⊢ (∀ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, q x

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Peel

Goal state before:
pp: α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x ↔ q x
⊢ (∃ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, q x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
le : sInf {I | I.IsMaximal} ≤ nilradical R
I : Ideal R
hI : I.IsPrime
⊢ I.IsMaximal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ a * a ^ (n - 1) = a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ DiscreteTopology (PrimeSpectrum R) ↔ Finite ↑{I | I.IsMaximal} ∧ sInf {I | I.IsMaximal} ≤ nilradical R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ Continuous (comap f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Function.Injective (comap (algebraMap R S))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
P : R[X]
x : A
⊢ D ((aeval x) P) = (aeval x) (derivative P) • D x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D1 D2 : Derivation R A M
s : Set A
h : Set.EqOn (⇑D1) (⇑D2) s
x✝² : A
hx✝ : x✝² ∈ ↑(adjoin R s)
x y : A
x✝¹ : x ∈ adjoin R s
x✝ : y ∈ adjoin R s
hx : D1 x = D2 x
hy : D1 y = D2 y
⊢ D1 (x + y) = D2 (x + y)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D1 D2 : Derivation R A M
s : Set A
h : Set.EqOn (⇑D1) (⇑D2) s
x✝² : A
hx✝ : x✝² ∈ ↑(adjoin R s)
x y : A
x✝¹ : x ∈ adjoin R s
x✝ : y ∈ adjoin R s
hx : D1 x = D2 x
hy : D1 y = D2 y
⊢ D1 (x * y) = D2 (x * y)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D1 D2 : Derivation R A M
s : Set A
h : Set.EqOn (⇑D1) (⇑D2) s
x✝² : A
hx✝ : x✝² ∈ ↑(adjoin R s)
x y : A
x✝¹ : x ∈ adjoin R s
x✝ : y ∈ adjoin R s
hx : D1 x = D2 x
hy : D1 y = D2 y
⊢ D1 (x * y) = D2 (x * y)

Tactic:
by simp only [leibniz, *]

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: 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 b : A
⊢ 0 (a * b) = a • 0 b + b • 0 a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: 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
D1 D2 : Derivation R A M
⊢ (↑D1 + ↑D2) 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Set.range (comap (algebraMap R S)) = {p | Disjoint ↑M ↑p.asIdeal}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: 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
D1 D2 : Derivation R A M
a b : A
⊢ (↑D1 + ↑D2) (a * b) = a • (↑D1 + ↑D2) b + b • (↑D1 + ↑D2) a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: 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
S : Type u_5
T : Type u_6
inst✝⁷ : Monoid S
inst✝⁶ : DistribMulAction S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : SMulCommClass S A M
inst✝³ : Monoid T
inst✝² : DistribMulAction T M
inst✝¹ : SMulCommClass R T M
inst✝ : SMulCommClass T A M
r : S
D : Derivation R A M
⊢ (r • ↑D) 1 = 0

Tactic:
by

Goal state after: