mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
⊢ IsConstructible s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (↑(U i) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set ↑↑(U i)
hVx : V ∈ 𝓝 ⟨x, hi⟩
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (V ↓∩ ↑(U i) ↓∩ s)
⊢ MapsTo Subtype.val V ↑V

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (↑(U i) ↓∩ s)
⊢ IsLocallyConstructible s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (s ∩ ↑(U i))
i : ι
⊢ IsLocallyConstructible (↑(U i) ↓∩ s)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).FaithfullyFlat ↔ Module.FaithfullyFlat R S

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FaithfullyFlat
⊢ f.Flat

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ f.FaithfullyFlat ↔ f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ FaithfullyFlat = fun f ↦ f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)

Tactic:
by

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

Goal state before:
pp: ⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
p : PrimeSpectrum R
x✝ : R
⊢ (RingEquiv.ofBijective f hf) (((↑(RingEquiv.ofBijective f hf).symm).comp f) x✝) =
    (RingEquiv.ofBijective f hf) ((id R) x✝)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
p : PrimeSpectrum R
⊢ (↑(RingEquiv.ofBijective f hf).symm).comp f = id R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ f.FaithfullyFlat

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FaithfullyFlat
⊢ Function.Injective ⇑f

Tactic:
by

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

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.Flat
⊢ PreservesFiniteLimits (tensorLeft ((restrictScalars f).obj (of B B)))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.Flat
⊢ PreservesFiniteLimits (extendScalars f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
⊢ (extendScalars f).ReflectsIsomorphisms

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
⊢ ComonadicLeftAdjoint (extendScalars f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p q : Ideal R
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : Q.LiesOver q
hle : p ≤ q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p q : Ideal R
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : Q.LiesOver q
hpq : p < q
⊢ ∃ P < Q, P.IsPrime ∧ P.LiesOver p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
⊢ l.toList[0] = PrimeSpectrum.comap (algebraMap R S) (RelSeries.toList L)[0]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
⊢ (RelSeries.head L).asIdeal.LiesOver l.head.asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
this : (RelSeries.head L).asIdeal.LiesOver l.head.asIdeal
Q : Ideal S
Qlt : Q < (RelSeries.head L).asIdeal
hQ : Q.IsPrime
Qlo : Q.LiesOver q.asIdeal
⊢ List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.cons L { asIdeal := Q, isPrime := hQ } Qlt).toList =
    (l.cons q lt).toList

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : LTSeries (PrimeSpectrum R)
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver (RelSeries.last l).asIdeal
⊢ ∃ L,
    L.length = l.length ∧
      RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
        List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = RelSeries.toList l

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ HasGoingDown R S ↔ GeneralizingMap (PrimeSpectrum.comap (algebraMap R S))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingDown R S
inst✝ : HasGoingDown S T
⊢ HasGoingDown R T

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this✝ : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime✝ } =
    { asIdeal := pl, isPrime := ⋯ }
this : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
⊢ Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl = pl

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ IsLocalHom (algebraMap (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Flat R S
⊢ HasGoingDown R S

Tactic:
by

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

Goal state before:
pp: 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
f₁ f₂ : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x : A
⊢ (f₁.toLinearMap - f₂.toLinearMap) x ∈ Submodule.restrictScalars R I

Tactic:
by

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

Goal state before:
pp: 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
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
⊢ (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp (IsScalarTower.toAlgHom R A B)

Tactic:
by

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

Goal state before:
pp: 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
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
F : A →ₗ[R] ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
⊢ (f x - (algebraMap A B) x) * (f y - (algebraMap A B) y) = 0

Tactic:
by

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

Goal state before:
pp: 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
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
⊢ Derivation R A ↥I

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
⊢ (algebraMap R S).Flat ↔ Module.Flat R S

Tactic:
by

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

Goal state before:
pp: 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
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
⊢ ↑(f 1) + (algebraMap A B) 1 = 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
hf : f.Flat
hg : g.Flat
⊢ (g.comp 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
hf : Function.Bijective ⇑f
⊢ f.Flat

Tactic:
by

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

Goal state before:
pp: ⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Flat

Tactic:
by

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

Goal state before:
pp: ⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Flat

Tactic:
by

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

Goal state before:
pp: 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
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
x y : A
⊢ ↑(f x) * ↑(f y) = 0

Tactic:
by

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

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Flat

Tactic:
by

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

Goal state before:
pp: 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
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
x y : A
⊢ ↑(f (x * y)) + (algebraMap A B) (x * y) = (↑(f x) + (algebraMap A B) x) * (↑(f y) + (algebraMap A B) y)

Tactic:
by

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

Goal state before:
pp: ⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ Flat

Tactic:
by

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

Goal state before:
pp: 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
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
r : R
⊢ ↑(f ((algebraMap R A) r)) + (algebraMap A B) ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
by

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

Goal state before:
pp: 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
⊢ (Ideal.Quotient.mk I) ((liftOfDerivationToSquareZero I hI d) x) = (algebraMap A (B ⧸ I)) x

Tactic:
by

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

Goal state before:
pp: 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
d : Derivation R A ↥I
x : A
⊢ (Ideal.Quotient.mk I) ↑(d x) + (algebraMap A (B ⧸ I)) x = (algebraMap A (B ⧸ I)) x

Tactic:
by

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

Goal state before:
pp: ⊢ OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ Flat

Tactic:
by

Goal state after:
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:
· rintro ⟨f, hf⟩; ext x; exact sub_add_cancel (f x) (algebraMap A B x)

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

Goal state before:
pp: 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
⊢ Derivation R A ↥I ≃ { f // (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I) }

Tactic:
by

Goal state after:
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 b : Additive G}, (MulEquiv.toAdditive ↑e).toFun a ≤ (MulEquiv.toAdditive ↑e).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✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o Additive H
⊢ ∀ {a b : G}, (MulEquiv.toAdditive.symm ↑e).toFun a ≤ (MulEquiv.toAdditive.symm ↑e).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✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : G ≃*o H
⊢ (fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
by

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

Goal state before:
pp: ⊢ OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ 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✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o Additive H
⊢ (fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, 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✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃+o H
⊢ ∀ {a b : Multiplicative G}, (AddEquiv.toMultiplicative ↑e).toFun a ≤ (AddEquiv.toMultiplicative ↑e).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✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o Multiplicative H
⊢ ∀ {a b : G}, (AddEquiv.toMultiplicative.symm ↑e).toFun a ≤ (AddEquiv.toMultiplicative.symm ↑e).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✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃+o H
⊢ (fun e ↦ { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicative ↑e, 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✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o Multiplicative H
⊢ (fun e ↦ { toMulEquiv := AddEquiv.toMultiplicative ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ }) e) =
    e

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
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
Q : Ideal R
inst✝ : Q.IsPrime
hQP : Q = Ideal.comap f P
⊢ (Localization.localRingHom Q P f hQP).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✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o H
⊢ ∀ {a b : G},
    (AddEquiv.toMultiplicativeRight e.toAddEquiv).toFun a ≤ (AddEquiv.toMultiplicativeRight 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✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃*o Multiplicative H
⊢ ∀ {a b : Additive G},
    (MulEquiv.toAdditiveLeft e.toMulEquiv).toFun a ≤ (MulEquiv.toAdditiveLeft 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
f : R →+* S
hf : f.Flat
⊢ GeneralizingMap (comap f)

Tactic:
by

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

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
hR : IsField R
f : R →+* S
⊢ 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✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃*o Multiplicative H
⊢ (fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeRight e.toAddEquiv, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveLeft e.toMulEquiv, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
by

Goal state after: