mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
⊢ IsAlgebraic R (a * b)

Tactic:
have ⟨ra, a0, int_a⟩ := ha.exists_integral_multiple
  have ⟨rb, b0, int_b⟩ := hb.exists_integral_multiple
  refine IsAlgebraic.iff_exists_smul_integral.mpr ⟨_, mul_ne_zero a0 b0, ?_⟩
  simp_rw [Algebra.smul_def, map_mul, mul_mul_mul_comm, ← Algebra.smul_def]
  exact int_a.mul int_b

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case mp
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ IsIntegral (FractionRing R) ((algebraMap S K) a / (algebraMap S K) b)

Tactic:
rw [div_eq_mul_inv]

Goal state after:
case mp
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ IsIntegral (FractionRing R) ((algebraMap S K) a * ((algebraMap S K) b)⁻¹)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
a : A
inst✝ : Algebra.IsIntegral R S
ha : ¬Transcendental S a
⊢ ¬Transcendental R a

Tactic:
Transcendental,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
a : A
inst✝ : Algebra.IsIntegral R S
ha : ¬¬IsAlgebraic S a
⊢ ¬¬IsAlgebraic R a
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
a : A
inst✝ : Algebra.IsAlgebraic R S
ha : ¬Transcendental S a
⊢ ¬Transcendental R a

Tactic:
Transcendental,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
a : A
inst✝ : Algebra.IsAlgebraic R S
ha : ¬¬IsAlgebraic S a
⊢ ¬¬IsAlgebraic R a
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝¹ : IsDomain S
inst✝ : FaithfulSMul R S
σ : Type u
⊢ Module.rank (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) = lift.{u, u_2} (Module.rank R S)

Tactic:
have := IsDomain.of_faithfulSMul R S
  rw [rank_fractionRing, rank_mvPolynomial_mvPolynomial]

Goal state after:
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
⊢ 1 ⊗ₜ[R] (r • t) * (algebraMap S (S ⊗[R] T)) ((algebraMap R S) r) * x = 1 ⊗ₜ[R] (r • t) * (algebraMap S (S ⊗[R] T)) a

Tactic:
simp only [tmul_smul, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self,
      RingHomCompTriple.comp_apply, Algebra.smul_mul_assoc, Algebra.TensorProduct.tmul_mul_tmul,
      one_mul, mul_one, id_apply, ← e]

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 • ((algebraMap R S) r ⊗ₜ[R] t * x) = r • r • (1 ⊗ₜ[R] t * x)
Module: Mathlib.RingTheory.Localization.AsSubring

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
x✝ : K
⊢ x✝ ∈ {x | ∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩} ↔
    x✝ ∈ ↑(mapToFractionRing K S (Localization S) hS).range

Tactic:
symm

Goal state after:
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
x✝ : K
⊢ x✝ ∈ ↑(mapToFractionRing K S (Localization S) hS).range ↔
    x✝ ∈ {x | ∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩}
Module: Mathlib.RingTheory.Localization.AsSubring

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : K
⊢ x✝ ∈ {x | ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹} ↔
    x✝ ∈ ↑(mapToFractionRing K S (Localization S) hS).range

Tactic:
symm

Goal state after:
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : K
⊢ x✝ ∈ ↑(mapToFractionRing K S (Localization S) hS).range ↔
    x✝ ∈ {x | ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹}
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ (∃ y ∉ I.radical, x * y ∈ I.radical) → ∃ i, I.IsMinimalPrime i ∧ x ∈ i

Tactic:
rintro ⟨y, hy, hx⟩

Goal state after:
case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
⊢ ∃ i, I.IsMinimalPrime i ∧ x ∈ i
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mpr.refine_1
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
⊢ p.IsPrime

Tactic:
rw [IsLocalization.isPrime_iff_isPrime_disjoint S A, IsLocalization.disjoint_under_iff S]
      refine ⟨hp.isPrime, ?_⟩
      rintro rfl
      exact hp.isPrime.ne_top rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: 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 A
⊢ (Ideal.comap (algebraMap R A) J).minimalPrimes =
    Ideal.comap (algebraMap R A) '' Ideal.under R ⁻¹' (Ideal.under R J).minimalPrimes

Tactic:
refine (Set.image_preimage_eq_iff.mpr ?_).symm

Goal state after:
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 A
⊢ (Ideal.comap (algebraMap R A) J).minimalPrimes ⊆ Set.range (Ideal.comap (algebraMap R A))
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case refine_1
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
i : Y
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ i ∈ ↑(Finset.image f' t), b i

Tactic:
simpa using subset_iUnion₂ (s := fun i _ => b (f' i)) i hi

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝¹ : TopologicalSpace X
u : ι → Opens X
hu : iSup u = ⊤
inst✝ : CompactSpace X
⊢ ∃ s, IsOpenCover fun i ↦ u ↑i

Tactic:
eq_top_iff,

Goal state after:
ι : Type u_1
X : Type u_3
inst✝¹ : TopologicalSpace X
u : ι → Opens X
hu : ⊤ ≤ iSup u
inst✝ : CompactSpace X
⊢ ∃ s, IsOpenCover fun i ↦ u ↑i
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case h_option
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type u_5
inst✝¹ : Finite ι
α✝ : Type u_5
inst✝ : Fintype α✝
ih : ∀ (U : α✝ → Opens α), ↑(⨅ i, U i) = ⋂ i, ↑(U i)
U : Option α✝ → Opens α
⊢ ↑(⨅ i, U i) = ⋂ i, ↑(U i)

Tactic:
rw [iInf_option, Set.iInter_option, Opens.coe_inf, ih]

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
x : α
⊢ (∃ W, ↑(W ⊓ U) ⊆ ↑V ∧ x ∈ W) ↔ ∃ t ⊆ ↑V ∪ (↑U)ᶜ, IsOpen[inst✝] t ∧ x ∈ t

Tactic:
coe_inf,

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
x : α
⊢ (∃ W, ↑W ∩ ↑U ⊆ ↑V ∧ x ∈ W) ↔ ∃ t ⊆ ↑V ∪ (↑U)ᶜ, IsOpen[inst✝] t ∧ x ∈ t
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[instTopologicalSpaceSubtype] (coborder s ↓∩ s)

Tactic:
isClosed_preimage_val,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s ∩ closure[inst✝] (coborder s ∩ s) ⊆ s
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ↑U = ↑(sSup {V | V ∈ B ∧ V ≤ U})

Tactic:
coe_sSup,

Goal state after:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ↑U = ⋃ i ∈ {V | V ∈ B ∧ V ≤ U}, ↑i
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
hU' : ↑s ⊆ ⋃ i, U i
t : Finset ι
ht : s ≤ t.sup fun i ↦ { carrier := U i, is_open' := ⋯ }
⊢ t.sup (SetLike.coe ∘ fun i ↦ { carrier := U i, is_open' := ⋯ }) ⊆ ⋃ i ∈ t, U i

Tactic:
Finset.sup_eq_iSup

Goal state after:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
hU' : ↑s ⊆ ⋃ i, U i
t : Finset ι
ht : s ≤ t.sup fun i ↦ { carrier := U i, is_open' := ⋯ }
⊢ ⨆ a ∈ t, (SetLike.coe ∘ fun i ↦ { carrier := U i, is_open' := ⋯ }) a ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case e_a
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ univ = ⋃ i, {x | x ∈ U i}

Tactic:
exact hU.iSup_set_eq_univ.symm

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: case refine_3
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝ : Finset (↑s × ↑s)
x✝² : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝¹ : ∃ t_1, (t.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t_1.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝ : (x, y) ∉ t
tc : Finset (↑s × ↑s)
eq : (t.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
refine tc.induction ⟨∅, by simp⟩ fun ⟨z, w⟩ tc _ ⟨t, eq⟩ ↦ ?_

Goal state after:
case refine_3
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝¹ : Finset (↑s × ↑s)
x✝⁵ : ↑s × ↑s
t✝ : Finset (↑s × ↑s)
x✝⁴ : ∃ t, (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝³ : (x, y) ∉ t✝
tc✝ : Finset (↑s × ↑s)
eq✝ : (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc✝.sup fun x ↦ ↑x.1 \ ↑x.2
x✝² : ↑s × ↑s
tc : Finset (↑s × ↑s)
x✝¹ : ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
z w : ↑s
x✝ : (z, w) ∉ tc
t : Finset (↑s × ↑s)
eq : ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ∃ t, ((↑x \ ↑y)ᶜ ⊓ (insert (z, w) tc).sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ U ∩ V = f '' (f ⁻¹' U ∩ f ⁻¹' V)

Tactic:
symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ f '' (f ⁻¹' U ∩ f ⁻¹' V) = U ∩ V
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : PartialOrder P
inst✝ : OrderTop P
a : P
⊢ (principal a).IsProper ↔ a ≠ ⊤

Tactic:
rw [isProper_iff_top_notMem, mem_principal, top_le_iff]

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S✝ S : Set (Ideal P)
s : Ideal P
hs : s ∈ S
⊢ ⋂ s ∈ S, ↑s ⊆ ↑s

Tactic:
exact biInter_subset_of_mem hs

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed[inst✝²] S✝
⊢ ∃ x, IsGenericPoint x S✝

Tactic:
by
    have hS'' := hS.image f hf.continuous.continuousOn
    obtain ⟨x, hx⟩ := QuasiSober.sober hS''.closure isClosed_closure
    obtain ⟨T, hT, rfl⟩ := hf.isInducing.isClosed_iff.mp hS'
    rw [image_preimage_eq_inter_range] at hx hS''
    have hxT : x ∈ T := by
      rw [← hT.closure_eq]
      exact closure_mono inter_subset_left hx.mem
    obtain ⟨y, rfl⟩ : x ∈ range f := by
      rw [hx.mem_open_set_iff hf.isOpen_range]
      refine Nonempty.mono ?_ hS''.1
      simpa using subset_closure
    use y
    change _ = _
    rw [hf.isEmbedding.closure_eq_preimage_closure_image, image_singleton, show _ = _ from hx]
    apply image_injective.mpr hf.injective
    ext z
    simp only [image_preimage_eq_inter_range, mem_inter_iff, and_congr_left_iff]
    exact fun hy => ⟨fun h => hT.closure_eq ▸ closure_mono inter_subset_left h,
      fun h => subset_closure ⟨h, hy⟩⟩

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)
h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)
V₁ V₂ : Set X
ho₁ : IsOpen[inst✝] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst✝] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
x : X
hx₁ : x ∈ V₁
hx₂ : x ∈ V₂
i : ι
hi : i ∈ t
hxi : x ∈ (U i).carrier
⊢ x ∈ ↑(U i) ∩ V₁ ∩ (↑(U i) ∩ V₂)

Tactic:
by simpa [*]

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
  refine ⟨fun d => ⟨liftOfDerivationToSquareZero I hI d, ?_⟩, fun f =>
    (derivationToSquareZeroOfLift I hI f.1 f.2 :), ?_, ?_⟩
  · ext x; exact liftOfDerivationToSquareZero_mk_apply I hI d x
  · intro d; ext x; exact add_sub_cancel_right (d x : B) (algebraMap A B x)
  · rintro ⟨f, hf⟩; ext x; exact sub_add_cancel (f x) (algebraMap A B x)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
⊢ ((Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)).Flat

Tactic:
refine RingHom.Flat.comp ?_ ?_

Goal state after:
case refine_1
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)
⊢ (↑(Algebra.TensorProduct.map (AlgHom.id S A) g)).Flat

case refine_2
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)
⊢ (Algebra.TensorProduct.map f (AlgHom.id R D)).Flat
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case pos
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime 1

Tactic:
simp only [coprime_one_right_eq_true, coprime_one_left_eq_true]

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

Goal state before:
pp: case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : ¬b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime (q ^ (a.lcm b).factorization q)

Tactic:
simp only [coprime_one_right_eq_true, coprime_one_left_eq_true]

Goal state after:
case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : ¬b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime (q ^ (a.lcm b).factorization q)
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case pos
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : ¬b.factorization p ≤ a.factorization p
h✝ : b.factorization q ≤ a.factorization q
⊢ Coprime 1 1

Tactic:
simp only [coprime_one_right_eq_true, coprime_one_left_eq_true]

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

Goal state before:
pp: case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : ¬b.factorization p ≤ a.factorization p
h✝ : ¬b.factorization q ≤ a.factorization q
⊢ Coprime 1 (q ^ (a.lcm b).factorization q)

Tactic:
simp only [coprime_one_right_eq_true, coprime_one_left_eq_true]

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

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

Tactic:
(gc R).u_l_u_eq_u,

Goal state after:
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
I : Set R
hI : closure t = zeroLocus I
⊢ I ⊆ ↑(vanishingIdeal t) ∧ t ⊆ zeroLocus ↑(vanishingIdeal t)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

pp: case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I.radical = J.radical → zeroLocus ↑I = zeroLocus ↑J

Tactic:
· intro h; simp_rw [← vanishingIdeal_zeroLocus_eq_radical, h]

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I.radical = J.radical → zeroLocus ↑I = zeroLocus ↑J
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T) = CommRingCat.ofHom (algebraMap R T)

Tactic:
simp [IsScalarTower.algebraMap_eq R S T]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h :
  Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) p.asIdeal) =
    Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) q.asIdeal)
⊢ p = q

Tactic:
rw [IsLocalization.map_under M S, IsLocalization.map_under M S] at h

Goal state after:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h : p.asIdeal = q.asIdeal
⊢ p = q
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
⊢ #{a | a ^ n = 1} ≤ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset

Tactic:
by
      gcongr
      intro x hx
      let ⟨m, hm⟩ := show x ∈ Submonoid.powers g from mem_powers_iff_mem_zpowers.2 <| hg x
      refine Set.mem_toFinset.2 ⟨(m / (Fintype.card α / Nat.gcd n (Fintype.card α)) : ℕ), ?_⟩
      dsimp only at ⊢ hm
      rw [zpow_natCast, ← pow_mul, Nat.mul_div_cancel_left', hm]
      refine Nat.dvd_of_mul_dvd_mul_right (gcd_pos_of_pos_left (Fintype.card α) hn0) ?_
      conv_lhs =>
        rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ← Nat.card_eq_fintype_card,
          ← orderOf_eq_card_of_forall_mem_zpowers hg]
      exact orderOf_dvd_of_pow_eq_one <| by simpa [pow_mul, hm] using (mem_filter.1 hx).2

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
⊢ zeroLocus {e} = ↑(basicOpen f)

Tactic:
by
  rw [basicOpen_eq_zeroLocus_of_mul_add f e] <;> simp only [mul, add, mul_comm, add_comm]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_2
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ orderOf g ∣ Finset.univ.lcm orderOf

Tactic:
lcm_orderOf_eq_exponent

Goal state after:
case refine_2
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ orderOf g ∣ exponent G