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

Goal state before:
pp: case refine_2
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
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ eval a (map (algebraMap S A) (map (integralClosure R S).toSubring.subtype p)) = 0

Tactic:
map_toSubring,

Goal state after:
case refine_2
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
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ eval a (map (algebraMap S A) (r • p✝)) = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hIM : I ≤ M
⊢ (zeroLocus ↑I).Nonempty

Tactic:
exact ⟨⟨M, hM.isPrime⟩, hIM⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (Set R)
⊢ zeroLocus (⋃ s' ∈ s, s') = ⋂ s' ∈ s, zeroLocus s'

Tactic:
by simp only [zeroLocus_iUnion]

Goal state after:
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
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.lTensor M f = 0
n : N
m : M
⊢ (TensorProduct.comm R N' M) (((AlgebraTensorModule.curry (LinearMap.rTensor M f)) n) m) =
    (TensorProduct.comm R N' M) (((AlgebraTensorModule.curry 0) n) m)

Tactic:
by simpa using congr($h (m ⊗ₜ n))

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

Goal state before:
pp: case mpr
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
⊢ (∀ (x : K), IsAlgebraic R x) → ∀ (x : S), IsAlgebraic R x

Tactic:
intro h x
    obtain ⟨f, hf₁, hf₂⟩ := h (algebraMap S K x)
    use f, hf₁
    rw [Polynomial.aeval_algebraMap_apply] at hf₂
    exact
      (injective_iff_map_eq_zero (algebraMap S K)).1 (FaithfulSMul.algebraMap_injective _ _) _
        hf₂

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

Goal state before:
pp: case neg
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 S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rs) (↥Rts) A
this✝¹ : Nontrivial ↥Rs
this✝ : Nontrivial S
this : IsDomain ↥Rt
x : S
hs : x ∈ s
ht : x ∉ t
⊢ IsAlgebraic (↥Rt) x

Tactic:
exact alg _ ⟨hs, ht⟩

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) ↔
    ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x

Tactic:
constructor
  · intro H y
    obtain ⟨a, ha⟩ := H (IsLocalization.mk' _ y (1 : P.primeCompl))
    obtain ⟨a, t, rfl⟩ := IsLocalization.exists_mk'_eq (P.comap f).primeCompl a
    rw [Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq,
      Submonoid.coe_one, one_mul, IsLocalization.eq_iff_exists P.primeCompl] at ha
    obtain ⟨c, hc⟩ := ha
    simp only [← mul_assoc] at hc
    exact ⟨_, _, _, c.2, t.2, hc.symm⟩
  · refine fun H y ↦ Localization.ind (fun ⟨y, t, h⟩ ↦ ?_) y
    simp only
    obtain ⟨yx, ys, yc, hyc, hy, ey⟩ := H y
    obtain ⟨tx, ts, yt, hyt, ht, et⟩ := H t
    refine ⟨Localization.mk (yx * ts) ⟨ys * tx, Submonoid.mul_mem _ hy ?_⟩, ?_⟩
    · exact fun H ↦ mul_mem (P.primeCompl.mul_mem hyt ht) h (et ▸ Ideal.mul_mem_left _ yt H)
    · simp only [Localization.mk_eq_mk', Localization.localRingHom_mk', map_mul f,
        IsLocalization.mk'_eq_iff_eq, IsLocalization.eq_iff_exists P.primeCompl]
      refine ⟨⟨yc, hyc⟩ * ⟨yt, hyt⟩, ?_⟩
      simp only [Submonoid.coe_mul]
      convert! congr($(ey.symm) * $(et)) using 1 <;> ring

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case add
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
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)

Tactic:
rw [this, ← one_mul (1 : S), ← Algebra.TensorProduct.tmul_mul_tmul, mul_add, mul_comm (_ ⊗ₜ _),
      mul_assoc, e₁, Algebra.TensorProduct.tmul_mul_tmul, one_mul, smul_mul_assoc,
      ← TensorProduct.smul_tmul, mul_comm (_ ⊗ₜ _), mul_assoc, e₂,
      Algebra.TensorProduct.tmul_mul_tmul, one_mul, smul_mul_assoc, ← TensorProduct.smul_tmul,
      TensorProduct.add_tmul, mul_comm t₁ t₂]

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

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

Tactic:
rw [add_comm, a.2.2]

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

Goal state before:
pp: case refine_1
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 s : R
hs : s ∈ I.primeCompl
⊢ (Ideal.Quotient.mk I) s ≠ 0

Tactic:
ne_eq,

Goal state after:
case refine_1
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 s : R
hs : s ∈ I.primeCompl
⊢ ¬(Ideal.Quotient.mk I) s = 0
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
⊢ ∀ b ∈ {J | map (algebraMap R (Localization.AtPrime p)) I ≤ J ∧ J.IsPrime},
    map (algebraMap R (Localization.AtPrime p)) p ≤ b

Tactic:
rintro q ⟨hq', hq⟩

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : map (algebraMap R (Localization.AtPrime p)) I ≤ q
hq : q.IsPrime
⊢ map (algebraMap R (Localization.AtPrime p)) p ≤ q
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := { bot := { asIdeal := ⊥, isPrime := inst✝ }, bot_le := ⋯ }
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      (PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩ ≠ ⊥ → ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal.IsMaximal) ↔
    ∀ (I : Ideal R), I.IsPrime → I ≠ ⊥ → I.IsMaximal

Tactic:
ne_eq,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := { bot := { asIdeal := ⊥, isPrime := inst✝ }, bot_le := ⋯ }
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      ¬(PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩ = ⊥ →
        ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal.IsMaximal) ↔
    ∀ (I : Ideal R), I.IsPrime → ¬I = ⊥ → I.IsMaximal
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) ∈ I

Tactic:
have : (x * (t.1 * b.1)) ^ (n + 1) = (t.1 ^ n * b.1 ^ n * x * t.1) * a := by
      rw [mul_assoc, ← ht]; ring

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this✝ : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
this : (x * (↑t * ↑b)) ^ (n + 1) = ↑t ^ n * ↑b ^ n * x * ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) ∈ I
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I x : Ideal R
hx : x ∈ (I ⊔ RingHom.ker f).minimalPrimes
⊢ (comap f ∘ map f) x = id x

Tactic:
exact (Ideal.comap_map_of_surjective f hf _).trans (sup_eq_left.mpr <| le_sup_right.trans hx.le)

Goal state after:
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:
ne_eq,

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 : ¬Ideal.under R J = ⊤
⊢ Ideal.under R J ≤ q
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))
⊢ ∀ (x : ↑(f ⁻¹' s)),
    𝓝 x = comap (Subtype.val ∘ MapsTo.restrict f (f ⁻¹' s) s ⋯) (𝓝 ((Subtype.val ∘ MapsTo.restrict f (f ⁻¹' s) s ⋯) x))

Tactic:
MapsTo.coe_restrict,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))
⊢ ∀ (x : ↑(f ⁻¹' s)), 𝓝 x = comap ((f ⁻¹' s).domRestrict f) (𝓝 ((f ⁻¹' s).domRestrict f x))
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ⋃ i ∈ {s | s ∈ SetLike.coe '' B ∧ s ⊆ ↑U}, i = ⋃ i ∈ {V | V ∈ B ∧ V ≤ U}, ↑i

Tactic:
iUnion,

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

Goal state before:
pp: 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))

Tactic:
exact fun H i ↦ H.inter (U i).isOpen

Goal state after:
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 ∘ MapsTo.restrict f (f ⁻¹' (U i).carrier) (U i).carrier ⋯)
          (𝓝 ((Subtype.val ∘ MapsTo.restrict f (f ⁻¹' (U i).carrier) (U i).carrier ⋯) x))

Tactic:
MapsTo.coe_restrict,

Goal state after:
α : 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 ((f ⁻¹' (U i).carrier).domRestrict f) (𝓝 ((f ⁻¹' (U i).carrier).domRestrict f x))
Module: Mathlib.Topology.Sets.Opens

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

Tactic:
simp only [IsBasis] at H ⊢

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
⊢ IsTopologicalBasis (SetLike.coe '' {x | ∃ U ∈ B, { carrier := f ⁻¹' ↑U, is_open' := ⋯ } = x})
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst✝¹] (f '' ↑A) = closure[inst✝¹] (f '' ↑B)
⊢ ↑A = ↑B

Tactic:
← A.isClosed.closure_eq,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst✝¹] (f '' ↑A) = closure[inst✝¹] (f '' ↑B)
⊢ closure[inst✝] ↑A = ↑B
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst✝¹] (f '' ↑A) = closure[inst✝¹] (f '' ↑B)
⊢ f ⁻¹' closure[inst✝¹] (f '' ↑B) = ↑B

Tactic:
← hf.closure_eq_preimage_closure_image,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst✝¹] (f '' ↑A) = closure[inst✝¹] (f '' ↑B)
⊢ closure[inst✝] ↑B = ↑B
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset (↑s × ↑s)
⊢ ∀ (hx : (∅.sup fun x ↦ ↑x.1 \ ↑x.2) ∈ closure s), p (∅.sup fun x ↦ ↑x.1 \ ↑x.2) hx

Tactic:
simpa using sdiff _ bot_mem _ bot_mem

Goal state after:
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
⊢ IsQuasiSeparated (f '' s)

Tactic:
by
  intro U V hU hU' hU'' hV hV' hV''
  convert!
    (H (f ⁻¹' U) (f ⁻¹' V) ?_ (h.continuous.1 _ hU') ?_ ?_ (h.continuous.1 _ hV') ?_).image
      h.continuous
  · symm
    rw [← Set.preimage_inter, Set.image_preimage_eq_inter_range, Set.inter_eq_left]
    exact Set.inter_subset_left.trans (hU.trans (Set.image_subset_range _ _))
  · intro x hx
    rw [← h.injective.injOn.mem_image_iff (Set.subset_univ _) trivial]
    exact hU hx
  · rw [h.isCompact_iff]
    convert! hU''
    rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]
    exact hU.trans (Set.image_subset_range _ _)
  · intro x hx
    rw [← h.injective.injOn.mem_image_iff (Set.subset_univ _) trivial]
    exact hV hx
  · rw [h.isCompact_iff]
    convert! hV''
    rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]
    exact hV.trans (Set.image_subset_range _ _)

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s)

Tactic:
refine ⟨fun hs => hs.image_of_isEmbedding h.isEmbedding, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
⊢ IsQuasiSeparated (f '' s) → IsQuasiSeparated s
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
⊢ I ≠ ⊤ ↔ ⊤ ∉ I

Tactic:
ne_eq,

Goal state after:
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
⊢ ¬I = ⊤ ↔ ⊤ ∉ I
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
⊢ IsCompact (⋂₀ s)

Tactic:
wlog h : ∀ t ∈ s, IsOpen t
  · let a := { t ∈ s | IsOpen t }
    let b := { t ∈ s | IsClosed t }
    have heq : s = a ∪ b := subset_antisymm (by grind) (by grind)
    rw [heq, Set.sInter_union]
    simp only [not_forall] at h
    obtain ⟨t, ht, hno⟩ := h
    obtain (ha | ha) := a.eq_empty_or_nonempty
    · simp only [ha, Set.sInter_empty, Set.univ_inter]
      exact IsCompact.of_isClosed_subset (hc _ ht) (isClosed_sInter (by grind)) (by grind)
    · apply IsCompact.inter_right
      · apply this (hf.subset (by grind)) ha <;> grind
      · exact isClosed_sInter (by grind)
  revert hne
  induction s, hf using Set.Finite.induction_on with
  | empty => simp
  | insert ha hs ih =>
    rename_i s
    obtain (rfl | hne) := s.eq_empty_or_nonempty
    · grind
    · grind [IsCompact.inter_of_isOpen, hs.isOpen_sInter, Set.sInter_insert]

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case compl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (f '' sᶜ)

Tactic:
rw [← range_sdiff_image hfopen.injective]
    exact (hfcomp.isConstructible hfopen.isOpen_range).sdiff hs'

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}
⊢ f ∈ p.asIdeal.primeCompl

Tactic:
by apply h ▸ Set.mem_singleton p

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Simple

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ⇑f
H : Subgroup H✝
iH : H.Normal
⊢ H = ⊥ ∨ H = ⊤

Tactic:
refine (iH.comap f).eq_bot_or_eq_top.imp (fun h => ?_) fun h => ?_
    · rw [← map_bot f, ← h, map_comap_eq_self_of_surjective hf]
    · rw [← comap_top f] at h
      exact comap_injective hf h

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

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

Tactic:
← Subgroup.inv_mem_iff H

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

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
⊢ IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k

Tactic:
isPGroup_iff_orderOf_dvd_pow,

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
⊢ (∀ (g : G), ∃ k, orderOf g ∣ p ^ k) ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : 1 < Nat.card ↑(fixedPoints G α)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b

Tactic:
rw [Finite.one_lt_card_iff_nontrivial] at hα

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : Nontrivial ↑(fixedPoints G α)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ Ideal.span (↑I ∪ ↑J) = ⊤

Tactic:
rw [Ideal.span_union, Ideal.span_eq, Ideal.span_eq, ← zeroLocus_empty_iff_eq_top,
        zeroLocus_sup, hI', hJ', Set.compl_inter_self]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : Nat.card ↥H = 0
⊢ P ≤ H ∨ Disjoint H P

Tactic:
rw [h1, Nat.coprime_zero_left, Subgroup.index_eq_one] at h_cop
    rw [h_cop]
    exact Or.inl le_top

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

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
⊢ #{a | orderOf a = d} = φ d

Tactic:
induction d using Nat.strong_induction_on with

Goal state after:
case h
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
⊢ #{a | orderOf a = d} = φ d
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Nontrivial G
inst✝ : FG G
⊢ rank G ≠ 0

Tactic:
ne_eq,

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Nontrivial G
inst✝ : FG G
⊢ ¬rank G = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ zeroLocus ↑I ∈ irreducibleComponents (PrimeSpectrum R) ↔ I.radical ∈ minimalPrimes R

Tactic:
← vanishingIdeal_zeroLocus_eq_radical

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ zeroLocus ↑I ∈ irreducibleComponents (PrimeSpectrum R) ↔ vanishingIdeal (zeroLocus ↑I) ∈ minimalPrimes R