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

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

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

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✝ : 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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
refine ⟨fun hf ↦ ?_, fun hf ↦ .comp hf (.of_bijective hg)⟩

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
⊢ f.Flat
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:
simp

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
x✝ : R
⊢ f x✝ = ((f.comp e.toRingHom).comp e.symm.toRingHom) x✝

Tactic:
simp

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

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

Goal state before:
pp: case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
h✝ : b.factorization p ≤ a.factorization p
⊢ p ^ n * 1 = p ^ n

Tactic:
simp

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

Goal state before:
pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
h✝ : ¬b.factorization p ≤ a.factorization p
⊢ 1 * p ^ n = p ^ n

Tactic:
simp

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:
rw [← isOpen_compl_iff, isOpen_iff, compl_compl]

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

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

Goal state before:
pp: case refine_4.h₀
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)
x✝ : ↑(CommRingCat.of S)
⊢ (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          pushout.map (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S))
              (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
              (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A))
              (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)) (𝟙 (CommRingCat.of R)) ⋯ ⋯ ≫
            (pushout.congrHom ⋯ ⋯ ≪≫ ⋯.isoPushout.symm).hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          ⋯.isoPushout.symm.hom ≫
            CommRingCat.ofHom
              (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A)).toRingHom))
      x✝

Tactic:
simp

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

Goal state before:
pp: case h₁
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)
x✝ : ↑(CommRingCat.of S)
⊢ (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          pushout.map (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S))
              (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
              (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A))
              (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)) (𝟙 (CommRingCat.of R)) ⋯ ⋯ ≫
            (pushout.congrHom ⋯ ⋯ ≪≫ ⋯.isoPushout.symm).hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          ⋯.isoPushout.symm.hom ≫
            CommRingCat.ofHom
              (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A)).toRingHom))
      x✝

Tactic:
simp

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

Goal state before:
pp: case refine_5.h₀
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)
x✝ : ↑(CommRingCat.of S)
⊢ (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ (Iso.refl (CommRingCat.of S)).hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          ⋯.isoPushout.symm.hom ≫ CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom))
      x✝

Tactic:
simp

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

Goal state before:
pp: case h₁
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)
x✝ : ↑(CommRingCat.of S)
⊢ (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ (Iso.refl (CommRingCat.of S)).hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          ⋯.isoPushout.symm.hom ≫ CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom))
      x✝

Tactic:
simp

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

Goal state before:
pp: case succ.inl
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
ihn : D (a ^ 0) = 0 • a ^ (0 - 1) • D a
⊢ D (a ^ (0 + 1)) = (0 + 1) • a ^ (0 + 1 - 1) • D a

Tactic:
simp

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

Goal state before:
pp: case C
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
x : A
a✝ : R
⊢ D ((aeval x) (C a✝)) = (aeval x) (derivative (C a✝)) • D x

Tactic:
simp

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

Goal state before:
pp: case refine_6.h₀
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)
x✝ : ↑(CommRingCat.of T)
⊢ (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
            (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) ≫
          pushout.map (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
              (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A))
              (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)) (𝟙 (CommRingCat.of T))
              (𝟙 (CommRingCat.of A)) (CommRingCat.ofHom (algebraMap R S)) ⋯ ⋯ ≫
            ⋯.isoPushout.symm.hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
            (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) ≫
          (pushout.congrHom ⋯ ⋯ ≪≫ ⋯.isoPushout.symm).hom ≫
            CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom))
      x✝

Tactic:
simp

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

Goal state before:
pp: case h₁
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)
x✝ : ↑(CommRingCat.of A)
⊢ (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
            (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) ≫
          pushout.map (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
              (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A))
              (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)) (𝟙 (CommRingCat.of T))
              (𝟙 (CommRingCat.of A)) (CommRingCat.ofHom (algebraMap R S)) ⋯ ⋯ ≫
            ⋯.isoPushout.symm.hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
            (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) ≫
          (pushout.congrHom ⋯ ⋯ ≪≫ ⋯.isoPushout.symm).hom ≫
            CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom))
      x✝

Tactic:
simp

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

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

Goal state before:
pp: case refine_7
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)
x✝ : ↑(CommRingCat.of S)
⊢ (CommRingCat.Hom.hom
        ((CommRingCat.ofHom (algebraMap S T) ≫
            pushout.inl (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A))) ≫
          ⋯.isoPushout.symm.hom))
      x✝ =
    (CommRingCat.Hom.hom
        ((Iso.refl (CommRingCat.of S)).hom ≫
          CommRingCat.ofHom (Algebra.TensorProduct.includeLeft.comp (algebraMap S T))))
      x✝

Tactic:
simp

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
e : R ≃+* S
x✝ : PrimeSpectrum R
⊢ comap ((↑e.symm).comp ↑e) x✝ = x✝

Tactic:
simp

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
e : R ≃+* S
x✝ : PrimeSpectrum S
⊢ comap ((↑e).comp ↑e.symm) x✝ = x✝

Tactic:
simp

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
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M
d : Derivation R B M
⊢ (↑d ∘ₗ (IsScalarTower.toAlgHom R A B).toLinearMap) 1 = 0

Tactic:
simp

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
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M
d : Derivation R B M
a b : A
⊢ (↑d ∘ₗ (IsScalarTower.toAlgHom R A B).toLinearMap) (a * b) =
    a • (↑d ∘ₗ (IsScalarTower.toAlgHom R A B).toLinearMap) b + b • (↑d ∘ₗ (IsScalarTower.toAlgHom R A B).toLinearMap) a

Tactic:
simp

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
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
p : Ideal S
hp : p.IsPrime
eq : p✝.asIdeal = ⊤.prod p
⊢ (0, 1) ∈ RingHom.ker (RingHom.fst R S)

Tactic:
simp

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
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
p : Ideal R
hp : p.IsPrime
eq : p✝.asIdeal = p.prod ⊤
⊢ (1, 0) ∈ RingHom.ker (RingHom.snd R S)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ ↑(basicOpen 1) = ↑⊤

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ ↑(basicOpen 0) = ↑⊥

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv₁ f_inv₂ : M → A
hf₁ : Function.RightInverse f_inv₁ ⇑f
hf₂ : Function.RightInverse f_inv₂ ⇑f
x✝¹ : Derivation R A A
x✝ : ∀ (x : A), f x = 0 → f (x✝¹ x) = 0
x : A
⊢ (liftOfRightInverse hf₁ x✝) (f x) = (liftOfRightInverse hf₂ x✝) (f x)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
hf : Function.Surjective ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : A
⊢ (liftOfSurjective hf hd) (f x) = f (d x)

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
⊢ D 0⁻¹ = -0⁻¹ ^ 2 • D 0

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u
inst✝ : CommSemiring R
r : R
⊢ basicOpen r ≤ basicOpen (r ^ 0)

Tactic:
simp

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

Goal state before:
pp: case succ
R : Type u
inst✝ : CommSemiring R
r : R
n✝ : ℕ
⊢ basicOpen r ≤ basicOpen (r ^ (n✝ + 1))

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ ⨆ i ∈ s, basicOpen i = ⊤ ↔ ⨆ i, basicOpen ↑i = ⊤

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
⊢ ↑(RingHom.ker (Pi.evalRingHom R i)) ⊆ ↑p.asIdeal

Tactic:
SetLike.coe_subset_coe

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
⊢ RingHom.ker (Pi.evalRingHom R i) ≤ p.asIdeal
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inl
G : Type u
inst✝ : Monoid G
⊢ exponent G ∣ 0 ↔ ∀ (g : G), g ^ 0 = 1

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
q : PrimeSpectrum (R i)
hp : comap (Pi.evalRingHom R i) q ∈ ↑(basicOpen (Pi.single i f))
x✝ : (i : ι) → R i
⊢ x✝ ∈ (comap (Pi.evalRingHom R i) q).asIdeal ↔ x✝ ∈ (comap (Pi.evalRingHom R i) q).asIdeal

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ (n % exponent G) = 1

Tactic:
← pow_eq_mod_exponent

Goal state after:
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ n = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case ofNat
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ∃ x ∈ H, x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk✝ : (fun x ↦ g ^ x) (Int.ofNat k) = x
hk : g ^ Int.ofNat k = x
⊢ x ∈ H

Tactic:
exact hx₁

Goal state after: