mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : FaithfullyFlat R S
inst✝⁴ : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
hf : Function.Injective ⇑f
this : Flat R (S ⊗[R] M)
⊢ Function.Injective ⇑(LinearMap.lTensor M f)

Tactic:
← FaithfullyFlat.lTensor_injective_iff_injective R S

Goal state after:
R : Type u
M : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : FaithfullyFlat R S
inst✝⁴ : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
hf : Function.Injective ⇑f
this : Flat R (S ⊗[R] M)
⊢ Function.Injective ⇑(LinearMap.lTensor S (LinearMap.lTensor M f))
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ r • ((algebraMap R S) r ⊗ₜ[R] t * x) = r • r • (1 ⊗ₜ[R] t * x)

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ r • ((r • 1) ⊗ₜ[R] t * x) = r • r • (1 ⊗ₜ[R] t * x)
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
T : Type u_3
inst✝⁴ : CommRing T
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
⊢ (Algebra.TensorProduct.map f (AlgHom.id R T)).SurjectiveOnStalks

Tactic:
by
  let := f.toRingHom.toAlgebra
  have := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm
  change (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T)).SurjectiveOnStalks
  convert_to ((Algebra.TensorProduct.cancelBaseChange R S S S' T).toAlgHom.comp
    Algebra.TensorProduct.includeRight).SurjectiveOnStalks
  · congr; ext; simp
  exact (Algebra.TensorProduct.cancelBaseChange R S S S' T).toRingEquiv.surjectiveOnStalks.comp
    Hf.baseChange'

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
I : Ideal R
inst✝ : I.IsPrime
x : I.ResidueField
⊢ ∃ x_1, x * (algebraMap (R ⧸ I) I.ResidueField) ↑x_1.2 = (algebraMap (R ⧸ I) I.ResidueField) x_1.1

Tactic:
obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq I.primeCompl x
    refine ⟨⟨Ideal.Quotient.mk _ x, ⟨Ideal.Quotient.mk _ s, ?_⟩⟩, ?_⟩
    · rwa [mem_nonZeroDivisors_iff_ne_zero, ne_eq, Ideal.Quotient.eq_zero_iff_mem]
    · simp [IsScalarTower.algebraMap_eq R (Localization.AtPrime I) I.ResidueField, ← map_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).2 * (↑b).2 + ((↑a).1 * ((↑a).2 * (↑c).2) + (↑a).2 * (↑a).2 * ((↑b).1 * (↑c).2)) =
    (↑a).2 * (↑b).2 + (↑a).2 * ((↑b).1 * (↑c).2)

Tactic:
(IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).2 * (↑b).2 + ((↑a).1 * ((↑a).2 * (↑c).2) + (↑a).2 * ((↑b).1 * (↑c).2)) =
    (↑a).2 * (↑b).2 + (↑a).2 * ((↑b).1 * (↑c).2)
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b a : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).2 + (↑a).1 * (↑a).1 = 1

Tactic:
(IsIdempotentElem.of_mul_add a.2.1 a.2.2).1.eq,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b a : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).2 + (↑a).1 = 1
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b a : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ 1 = (↑a).1 + (↑a).2 * (↑a).2

Tactic:
(IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b a : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ 1 = (↑a).1 + (↑a).2
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mpr.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
⊢ ∀ ⦃y : Ideal A⦄, (fun q ↦ q.IsPrime ∧ Ideal.map (algebraMap R A) J ≤ q) y → y ≤ p → p ≤ y

Tactic:
intro I

Goal state after:
case mpr.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
I : Ideal A
⊢ (fun q ↦ q.IsPrime ∧ Ideal.map (algebraMap R A) J ≤ q) I → I ≤ p → p ≤ I
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this✝ : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
this : Ideal.under R J ≠ ⊤
⊢ Ideal.under R J ≤ q

Tactic:
rw [ne_eq, Ideal.comap_eq_top_iff, ← ne_eq, ← disjoint_under_iff q.primeCompl A J] at this

Goal state after:
case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this✝ : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
this : Disjoint ↑q.primeCompl ↑(Ideal.under R J)
⊢ Ideal.under R J ≤ q
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : x ∉ range ⇑(algebraMap R K)
⊢ ¬∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯

Tactic:
hlocal

Goal state after:
case mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : x ∉ range ⇑(algebraMap R K)
hlocal : ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
⊢ False
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Function.Surjective ⇑↑(MaximalSpectrum.toPiLocalization ((i : ι) → R i))

Tactic:
← piLocalizationToMaximal_comp_toPiLocalization

Goal state after:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Function.Surjective ⇑↑((piLocalizationToMaximal ((i : ι) → R i)).comp (toPiLocalization ((i : ι) → R i)))
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
this : Z ∪ (frontier (U ∩ Z))ᶜ = univ
⊢ IsOpen[inst✝] (U ∪ (frontier (U ∩ Z))ᶜ)

Tactic:
exact hU.union isClosed_frontier.isOpen_compl

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: 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
H : ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)), 𝓝 x = Filter.comap Subtype.val (Filter.comap f (𝓝 ((f ∘ Subtype.val) x)))
x : α
i : ι
hi : f x ∈ U i
⊢ 𝓝 x = Filter.comap f (𝓝 (f x))

Tactic:
simpa [← ((h.1 _ (U i).2).isOpenEmbedding_subtypeVal).map_nhds_eq ⟨x, hi⟩, H i ⟨x, hi⟩,
      subtype_coe_map_comap] using preimage_mem_comap ((U i).2.mem_nhds hi)

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
⊢ ∀ (s : Set (CofiniteTopology α)) (f : Ultrafilter (CofiniteTopology α)),
    s ∈ ↑f → ∃ x ∈ s, ↑f ≤ pure x ∨ ↑f ≤ Filter.cofinite

Tactic:
intro s

Goal state after:
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
⊢ ∀ (f : Ultrafilter (CofiniteTopology α)), s ∈ ↑f → ∃ x ∈ s, ↑f ≤ pure x ∨ ↑f ≤ Filter.cofinite
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
⊢ ∀ (x : Closeds α),
    (∀ y < x, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S) →
      ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ x = sSup S

Tactic:
intro s

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
⊢ (∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S) →
    ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
by
  apply wellFounded_lt.induction s; clear s
  intro s H
  rcases eq_or_ne s ⊥ with rfl | h₀
  · use ∅; simp
  · by_cases h₁ : IsPreirreducible (s : Set α)
    · replace h₁ : IsIrreducible (s : Set α) := ⟨Closeds.coe_nonempty.2 h₀, h₁⟩
      use {s}; simp [h₁]
    · simp only [isPreirreducible_iff_isClosed_union_isClosed, not_forall, not_or] at h₁
      obtain ⟨z₁, z₂, hz₁, hz₂, h, hz₁', hz₂'⟩ := h₁
      lift z₁ to Closeds α using hz₁
      lift z₂ to Closeds α using hz₂
      rcases H (s ⊓ z₁) (inf_lt_left.2 hz₁') with ⟨S₁, hSf₁, hS₁, h₁⟩
      rcases H (s ⊓ z₂) (inf_lt_left.2 hz₂') with ⟨S₂, hSf₂, hS₂, h₂⟩
      refine ⟨S₁ ∪ S₂, hSf₁.union hSf₂, Set.union_subset_iff.2 ⟨hS₁, hS₂⟩, ?_⟩
      rwa [sSup_union, ← h₁, ← h₂, ← inf_sup_left, left_eq_inf]

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 : Set X⦄,
    (∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ s ⊆ W ∧ W ⊆ U) →
      (∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ t ⊆ W ∧ W ⊆ U) → ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ s ∪ t ⊆ W ∧ W ⊆ U

Tactic:
intro s

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 : Set X
⊢ ∀ ⦃t : Set X⦄,
    (∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ s ⊆ W ∧ W ⊆ U) →
      (∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ t ⊆ W ∧ 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 γ
f : α ≃ₜ β
s : Compacts α
⊢ Compacts.map ⇑f.symm ⋯ (Compacts.map ⇑f ⋯ s) = s

Tactic:
ext1
    simp only [coe_map, ← image_comp, f.symm_comp_self, image_id]

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
M N : ModuleCat A
g : M ⟶ N
h : Function.Bijective ⇑(ConcreteCategory.hom ((extendScalars f).map g))
algInst✝ : Algebra A B := f.toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat A B
⊢ Function.Bijective ⇑(ConcreteCategory.hom g)

Tactic:
replace h : Function.Bijective (LinearMap.lTensor B g.hom) := h

Goal state after:
A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
M N : ModuleCat A
g : M ⟶ N
algInst✝ : Algebra A B := f.toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat A B
h : Function.Bijective ⇑(LinearMap.lTensor B (Hom.hom g))
⊢ Function.Bijective ⇑(ConcreteCategory.hom g)
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: case neg
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
h : ¬p = q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
have := Q.over_def q

Goal state after:
case neg
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
h : ¬p = q
this : q = under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
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.of (S ⊗[R] S) ⟶ CommRingCat.of (T ⊗[R] A)

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.of S ⟶ CommRingCat.of (T ⊗[S] A)

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)
⊢ IsPushout ?m.67 (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom) ?m.69

Tactic:
· exact CommRingCat.ofHom
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T)
      (IsScalarTower.toAlgHom R S A)).toRingHom

Goal state after:
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.of S ⟶ CommRingCat.of (T ⊗[S] A)

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)
⊢ IsPushout
    (CommRingCat.ofHom
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A)).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom) ?m.69
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:
simp only [leibniz, *]

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
f : R
p : PrimeSpectrum R
h : (basicOpen f).carrier = {p}
r : R
hr : ∀ m ∈ Submonoid.powers f, m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint ↑q ↑(Submonoid.powers f)
this : { asIdeal := q, isPrime := prime } = p
⊢ r ∉ { asIdeal := q, isPrime := prime }.asIdeal.primeCompl

Tactic:
exact not_not.mpr (q.span_singleton_le_iff_mem.mp le)

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ Nat.find ?hc ≤ n

Tactic:
apply Nat.find_min'

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
⊢ zpowers g = ⊤

Tactic:
by
  subst h
  have := (zpowers g).eq_bot_or_eq_top_of_prime_card
  rwa [zpowers_eq_bot, or_iff_right hg] at this

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
⊢ (∀ (g : G), g ^ n = 1) → exponent G ∣ n

Tactic:
intro hG

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ Nat.card ↥⊤ = Nat.card α

Tactic:
card_top

Goal state after:
α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ Nat.card α = Nat.card α
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
⊢ Function.Surjective ⇑(MaximalSpectrum.toPiLocalization R)

Tactic:
← piLocalizationToMaximal_comp_toPiLocalization

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
⊢ Function.Surjective ⇑((piLocalizationToMaximal R).comp (toPiLocalization R))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
simp_rw [← isMax_iff, StableUnderSpecialization, ← le_iff_specializes, Set.mem_singleton_iff,
    @forall_comm _ (_ = _), forall_eq]

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ (a : PrimeSpectrum R), x ≤ a → a = x) ↔ IsMax x
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ n.gcd (Fintype.card α) * m / m ≤ n

Tactic:
Nat.mul_div_cancel _ hm0

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ n.gcd (Fintype.card α) ≤ n
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h✝ : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
h : b.coeff 0 = 1
this : b.natTrailingDegree = 0
⊢ b.reverse.Monic

Tactic:
rw [Monic.def, reverse_leadingCoeff, trailingCoeff, this, h]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ Nat.card (G ⧸ center G) ∣ p

Tactic:
rw [← mul_dvd_mul_iff_left (NeZero.ne p), ← sq, ← hG, ← (center G).card_mul_index]

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ p * Nat.card (G ⧸ center G) ∣ Nat.card ↥(center G) * (center G).index
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n✝ : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n✝
inst✝ : AddCommMonoid M
n : ℕ
h : ∀ (x : M), (n + 1) • x = 0
h_mod : ∀ (c : ℕ) (x : M), (c % (n + 1)) • x = c • x
this : n + 1 ≠ 0
⊢ Module (ZMod (n + 1)) M

Tactic:
exact {
    smul := fun (c : Fin _) x ↦ c.val • x
    smul_zero := fun _ ↦ nsmul_zero _
    zero_smul := fun _ ↦ zero_nsmul _
    smul_add := fun _ _ _ ↦ nsmul_add _ _ _
    one_smul := fun _ ↦ (h_mod _ _).trans <| one_nsmul _
    add_smul := fun _ _ _ ↦ (h_mod _ _).trans <| add_nsmul _ _ _
    mul_smul := fun _ _ _ ↦ (h_mod _ _).trans <| mul_nsmul' _ _ _
  }

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
p : Ideal R
hp : p.IsPrime
hinj : Function.Injective ⇑(algebraMap R S)
⊢ ∃ a, comap (algebraMap R S) a = { asIdeal := p, isPrime := hp }

Tactic:
obtain ⟨Q, _, hQ, rfl⟩ := Ideal.exists_ideal_over_prime_of_isIntegral p (⊥ : Ideal S)
    (by simp [Ideal.comap_bot_of_injective (algebraMap R S) hinj])

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
hinj : Function.Injective ⇑(algebraMap R S)
Q : Ideal S
left✝ : Q ≥ ⊥
hQ : Q.IsPrime
hp : (Ideal.comap (algebraMap R S) Q).IsPrime
⊢ ∃ a, comap (algebraMap R S) a = { asIdeal := Ideal.comap (algebraMap R S) Q, isPrime := hp }
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ Set.EqOn ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) id (irreducibleComponents (PrimeSpectrum R))

Tactic:
intro s

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ s ∈ irreducibleComponents (PrimeSpectrum R) → ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) s = id s
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ Nat.card ↥(centralizer {g}) = Nat.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
by
  rw [centralizer_eq_comap_stabilizer]; rfl

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
⊢ x ^ n = f b

Tactic:
simpa [Subtype.ext_iff] using hn

Goal state after: