mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring P
f : R →+* S
g : S →+* P
⊢ mapPiLocalization (g.comp f) = (mapPiLocalization g).comp (mapPiLocalization f)

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
P : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring P
f : R →+* S
g : S →+* P
x✝¹ : PiLocalization R
x✝ : PrimeSpectrum P
⊢ (mapPiLocalization (g.comp f)) x✝¹ x✝ = ((mapPiLocalization g).comp (mapPiLocalization f)) x✝¹ x✝
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B → ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ (∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U) → IsBasis B
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' closure[inst✝] s ⊆ closure[inst✝¹] (f ⁻¹' s)

Tactic:
exact hf.preimage_closure_subset_closure_preimage

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B → ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us

case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ (∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us) → IsBasis B
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ U Z, (∃ t, IsOpen[inst✝] t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed[inst✝] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z) ↔
    ∃ s', (∃ U Z, IsOpen[inst✝] U ∧ IsClosed[inst✝] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ U Z, (∃ t, IsOpen[inst✝] t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed[inst✝] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z) →
    ∃ s', (∃ U Z, IsOpen[inst✝] U ∧ IsClosed[inst✝] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s

case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ s', (∃ U Z, IsOpen[inst✝] U ∧ IsClosed[inst✝] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s) →
    ∃ U Z, (∃ t, IsOpen[inst✝] t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed[inst✝] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ IsOpen[inst✝] s ↔ ∀ (i : ι), IsOpen[inst✝] (s ∩ ↑(U i))

Tactic:
constructor

Goal state after:
case mp
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ IsOpen[inst✝] s → ∀ (i : ι), IsOpen[inst✝] (s ∩ ↑(U i))

case mpr
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ (∀ (i : ι), IsOpen[inst✝] (s ∩ ↑(U i))) → IsOpen[inst✝] s
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst✝] U
hZ : IsClosed[inst✝] Z
⊢ closure[inst✝] Z ∪ (frontier (U ∩ Z))ᶜ = univ

Tactic:
← compl_subset_iff_union,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst✝] U
hZ : IsClosed[inst✝] Z
⊢ (closure[inst✝] Z)ᶜ ⊆ (frontier (U ∩ Z))ᶜ
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ (∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))) ↔
    ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)), 𝓝 x = Filter.comap Subtype.val (Filter.comap f (𝓝 ((f ∘ Subtype.val) x)))

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ (∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))) →
    ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)), 𝓝 x = Filter.comap Subtype.val (Filter.comap f (𝓝 ((f ∘ Subtype.val) x)))

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ (∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)), 𝓝 x = Filter.comap Subtype.val (Filter.comap f (𝓝 ((f ∘ Subtype.val) x)))) →
    ∀ (x : α), 𝓝 x = Filter.comap f (𝓝 (f x))
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case e'_3
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ (range fun i ↦ (b i).carrier) = SetLike.coe '' range b

Tactic:
ext

Goal state after:
case e'_3
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U x✝ : Set α
⊢ (x✝ ∈ range fun i ↦ (b i).carrier) ↔ x✝ ∈ SetLike.coe '' range b
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L : BooleanSubalgebra α
M : BooleanSubalgebra β
e : β ≃o α
⊢ ↑(map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ } L) = ↑M ↔
    ↑L = ↑(map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ } M)

Tactic:
exact (Equiv.eq_image_iff_symm_image_eq _ _ _).symm

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L : BooleanSubalgebra α
M : BooleanSubalgebra β
e : β ≃o α
⊢ map
        (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        L =
      M ↔
    L =
      map
        (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        M

Tactic:
simp_rw [← coe_inj]; exact (Equiv.eq_image_iff_symm_image_eq _ _ _).symm

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Opens β)
H : IsTopologicalBasis (SetLike.coe '' B)
f : α → β
h : IsInducing f
⊢ SetLike.coe '' {x | ∃ U ∈ B, { carrier := f ⁻¹' ↑U, is_open' := ⋯ } = x} = preimage f '' SetLike.coe '' B

Tactic:
ext

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Opens β)
H : IsTopologicalBasis (SetLike.coe '' B)
f : α → β
h : IsInducing f
x✝ : Set α
⊢ x✝ ∈ SetLike.coe '' {x | ∃ U ∈ B, { carrier := f ⁻¹' ↑U, is_open' := ⋯ } = x} ↔ x✝ ∈ preimage f '' SetLike.coe '' B
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)
V : Set α
hV : IsOpen[inst✝¹] V
⊢ f '' V = f '' ⋃ i, V ∩ ↑(U i)

Tactic:
hU.iUnion_inter

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ WellFoundedGT (Opens α) ↔ ∀ (s : Opens α), IsCompact ↑s

Tactic:
CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ CompleteLattice.IsSupFiniteCompact (Opens α) ↔ ∀ (s : Opens α), IsCompact ↑s
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
⊢ ↑(⨅ i, s i) = ⋂ i, ↑(s i)

Tactic:
ext

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
x✝ : α
⊢ x✝ ∈ ↑(⨅ i, s i) ↔ x✝ ∈ ⋂ i, ↑(s i)
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Closeds α
⊢ IsAtom s ↔ ∃ x, s = {x}

Tactic:
by
  simp [← Closeds.isAtom_coe, Set.isAtom_iff, SetLike.ext_iff, Set.ext_iff]

Goal state after:
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
V : IrreducibleCloseds β
⊢ (fun V ↦ { carrier := f ⁻¹' ↑↑V, isIrreducible' := ⋯, isClosed' := ⋯ }) ((fun T ↦ ⟨map f ⋯ T, ⋯⟩) V) = V

Tactic:
ext

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
V : IrreducibleCloseds β
x✝ : β
⊢ x✝ ∈ ↑((fun V ↦ { carrier := f ⁻¹' ↑↑V, isIrreducible' := ⋯, isClosed' := ⋯ }) ((fun T ↦ ⟨map f ⋯ T, ⋯⟩) V)) ↔ x✝ ∈ ↑V
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
V : ↑{V | (f ⁻¹' ↑V).Nonempty}
⊢ (fun T ↦ ⟨map f ⋯ T, ⋯⟩) ((fun V ↦ { carrier := f ⁻¹' ↑↑V, isIrreducible' := ⋯, isClosed' := ⋯ }) V) = V

Tactic:
ext

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
V : ↑{V | (f ⁻¹' ↑V).Nonempty}
x✝ : α
⊢ x✝ ∈ ↑↑((fun T ↦ ⟨map f ⋯ T, ⋯⟩) ((fun V ↦ { carrier := f ⁻¹' ↑↑V, isIrreducible' := ⋯, isClosed' := ⋯ }) V)) ↔
    x✝ ∈ ↑↑V
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
⊢ ∃ o, IsOpen[inst✝¹] o ∧ o.Nonempty ∧ o ⊆ Z

Tactic:
have hα : (irreducibleComponents α).Finite := finite_irreducibleComponents
  have hZ := closure_sUnion_irreducibleComponents_sdiff_singleton hα Z H
  refine ⟨(⋃₀ (irreducibleComponents α \ {Z}))ᶜ, ?_, ?_, subset_closure.trans hZ.le⟩
  · rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]
    exact hα.sdiff.isClosed_biUnion fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1
  · contrapose! hZ
    rw [hZ, closure_empty, ← Set.nonempty_iff_empty_ne]
    exact H.1.nonempty

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
s t W₁ : Set X
Wc₁ : IsCompact W₁
Wo₁ : IsOpen[inst✝¹] W₁
hKW₁ : s ⊆ W₁
hWU₁ : W₁ ⊆ U
⊢ (∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ t ⊆ W ∧ W ⊆ U) → ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ s ∪ t ⊆ W ∧ W ⊆ U

Tactic:
⟨W₂, Wc₂, Wo₂, hKW₂, hWU₂⟩

Goal state after:
case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
s t W₁ : Set X
Wc₁ : IsCompact W₁
Wo₁ : IsOpen[inst✝¹] W₁
hKW₁ : s ⊆ W₁
hWU₁ : W₁ ⊆ U
W₂ : Set X
Wc₂ : IsCompact W₂
Wo₂ : IsOpen[inst✝¹] W₂
hKW₂ : t ⊆ W₂
hWU₂ : W₂ ⊆ U
⊢ ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ s ∪ t ⊆ W ∧ W ⊆ U
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : Nonempty α
⊢ Nontrivial (Compacts α)

Tactic:
constructor

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : Nonempty α
⊢ ∃ x y, x ≠ y
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : NonemptyCompacts α
⊢ NonemptyCompacts.map id ⋯ K = K

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
K : NonemptyCompacts α
x✝ : α
⊢ x✝ ∈ ↑(NonemptyCompacts.map id ⋯ K) ↔ x✝ ∈ ↑K
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → γ
g : α → β
hf : Continuous f
hg : Continuous g
K : NonemptyCompacts α
⊢ NonemptyCompacts.map (f ∘ g) ⋯ K = NonemptyCompacts.map f hf (NonemptyCompacts.map g hg K)

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → γ
g : α → β
hf : Continuous f
hg : Continuous g
K : NonemptyCompacts α
x✝ : γ
⊢ x✝ ∈ ↑(NonemptyCompacts.map (f ∘ g) ⋯ K) ↔ x✝ ∈ ↑(NonemptyCompacts.map f hf (NonemptyCompacts.map g hg K))
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
x : α
⊢ NonemptyCompacts.map f hf {x} = {f x}

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
x : α
x✝ : β
⊢ x✝ ∈ ↑(NonemptyCompacts.map f hf {x}) ↔ x✝ ∈ ↑{f x}
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝] U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst✝] V
htV : IsConstructible (V ↓∩ t)
⊢ (U ∩ V) ↓∩ (s ∪ t) = inclusion ⋯ ⁻¹' U ↓∩ s ∪ inclusion ⋯ ⁻¹' V ↓∩ t

Tactic:
ext

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝] U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst✝] V
htV : IsConstructible (V ↓∩ t)
x✝ : ↑(U ∩ V)
⊢ x✝ ∈ (U ∩ V) ↓∩ (s ∪ t) ↔ x✝ ∈ inclusion ⋯ ⁻¹' U ↓∩ s ∪ inclusion ⋯ ⁻¹' V ↓∩ t
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:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
x✝ : R →+* S
⊢ x✝.FaithfullyFlat ↔ x✝.Flat ∧ Function.Surjective (PrimeSpectrum.comap x✝)
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:
ext

Goal state after:
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).symm).comp f) x✝ = (id R) x✝
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:
constructor

Goal state after:
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.head.asIdeal = under R (RelSeries.head L).asIdeal
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_1
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)
⊢ (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp (IsScalarTower.toAlgHom R A B)

Tactic:
ext

Goal state after:
case refine_1
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✝ : A
⊢ ((Ideal.Quotient.mkₐ R I).comp f) x✝ = ((Ideal.Quotient.mkₐ R I).comp (IsScalarTower.toAlgHom R A B)) x✝
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
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)
⊢ (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) 1 = 0

Tactic:
ext

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
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)
⊢ ↑((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) 1) = ↑0
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
⊢ IsScalarTower.toAlgHom R A (B ⧸ I) = (Ideal.Quotient.mkₐ R I).comp (IsScalarTower.toAlgHom R A B)

Tactic:
ext

Goal state after:
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 x✝ : A
⊢ (IsScalarTower.toAlgHom R A (B ⧸ I)) x✝ = ((Ideal.Quotient.mkₐ R I).comp (IsScalarTower.toAlgHom R A B)) 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
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) ⋯
this : (f x - (algebraMap A B) x) * (f y - (algebraMap A B) y) = 0
⊢ (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) (x * y) =
    x • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) y +
      y • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) x

Tactic:
ext

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
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 := ⋯
this : (f x - (algebraMap A B) x) * (f y - (algebraMap A B) y) = 0
⊢ ↑((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) (x * y)) =
    ↑(x • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) y +
        y • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) x)
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case e'_5
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
algInst✝ : Algebra R S := ⋯
a✝ : ↑s
e_4✝ : OreLocalization.instAddCommMonoidOreLocalization = CommRing.toCommSemiring.toAddCommMonoid
⊢ OreLocalization.instModuleOfIsScalarTower = Algebra.toModule

Tactic:
ext

Goal state after:
case e'_5
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
a✝ : ↑s
e_4✝ : OreLocalization.instAddCommMonoidOreLocalization = CommRing.toCommSemiring.toAddCommMonoid
x✝¹ : R
x✝ : OreLocalization (Submonoid.powers ↑a✝) S
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ 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
⊢ (fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
ext

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
⊢ (fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
ext

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
⊢ (fun e ↦ { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicative ↑e, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
ext

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✝