mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
hq : p.primesOver S = {q}
inst✝ : Algebra.IsIntegral R S
x : S
hx : x ∉ q
this : ∀ r ∉ p, ∀ (c : S), c * x ≠ (algebraMap R S) r
⊢ False

Tactic:
obtain ⟨Q, hQ, hxQ, hQp⟩ := Ideal.exists_le_prime_disjoint (.span {x})
    (Algebra.algebraMapSubmonoid _ p.primeCompl)
    (by simpa [Set.disjoint_iff_forall_ne, Ideal.mem_span_singleton',
      Algebra.algebraMapSubmonoid, @forall_comm S])

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
hq : p.primesOver S = {q}
inst✝ : Algebra.IsIntegral R S
x : S
hx : x ∉ q
this : ∀ r ∉ p, ∀ (c : S), c * x ≠ (algebraMap R S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint ↑Q ↑(Algebra.algebraMapSubmonoid S p.primeCompl)
⊢ False
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
y : N1 ⊗[R] M
hy : (LinearMap.rTensor M l12) y = x ⊗ₜ[R] m
⊢ (LinearMap.rTensor M l23.ker.subtype)
      ((TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id)
        ((LinearMap.rTensor M
            (LinearMap.codRestrict (Submodule.inclusion complex).range
              (Submodule.inclusion complex ∘ₗ l12.rangeRestrict) ⋯))
          y)) =
    (LinearMap.rTensor M l12) y

Tactic:
← LinearMap.comp_apply,

Goal state after:
case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
y : N1 ⊗[R] M
hy : (LinearMap.rTensor M l12) y = x ⊗ₜ[R] m
⊢ (LinearMap.rTensor M l23.ker.subtype ∘ₗ TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id)
      ((LinearMap.rTensor M
          (LinearMap.codRestrict (Submodule.inclusion complex).range (Submodule.inclusion complex ∘ₗ l12.rangeRestrict)
            ⋯))
        y) =
    (LinearMap.rTensor M l12) y
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
y : N1 ⊗[R] M
hy : (LinearMap.rTensor M l12) y = x ⊗ₜ[R] m
⊢ (LinearMap.rTensor M (l23.ker.subtype ∘ₗ (Submodule.inclusion complex).range.subtype))
      ((LinearMap.rTensor M
          (LinearMap.codRestrict (Submodule.inclusion complex).range (Submodule.inclusion complex ∘ₗ l12.rangeRestrict)
            ⋯))
        y) =
    (LinearMap.rTensor M l12) y

Tactic:
← LinearMap.comp_apply,

Goal state after:
case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
y : N1 ⊗[R] M
hy : (LinearMap.rTensor M l12) y = x ⊗ₜ[R] m
⊢ (LinearMap.rTensor M (l23.ker.subtype ∘ₗ (Submodule.inclusion complex).range.subtype) ∘ₗ
        LinearMap.rTensor M
          (LinearMap.codRestrict (Submodule.inclusion complex).range (Submodule.inclusion complex ∘ₗ l12.rangeRestrict)
            ⋯))
      y =
    (LinearMap.rTensor M l12) y
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
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Surjective ⇑f

Tactic:
← LinearMap.exact_zero_iff_surjective (M ⊗[R] Unit),

Goal state after:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑(LinearMap.lTensor M f) ⇑0 ↔ Function.Surjective ⇑f
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_3
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst✝¹² : CommRing Rf
inst✝¹¹ : CommRing Sf
inst✝¹⁰ : Algebra R Rf
inst✝⁹ : Algebra S Sf
inst✝⁸ : Algebra Rf Sf
inst✝⁷ : Algebra R Sf
inst✝⁶ : IsScalarTower R S Sf
inst✝⁵ : IsScalarTower R Rf Sf
M : Submonoid R
inst✝⁴ : IsLocalization M Rf
inst✝³ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst✝² : Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst✝¹ : IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst✝ : IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
⊢ ∀ {x y : ↥(integralClosure R S)},
    (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) x =
        (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) y →
      ∃ c, ↑c * x = ↑c * y

Tactic:
· rintro ⟨a, ha⟩ ⟨b, hb⟩ e
    have := congr(algebraMap _ Sf $e)
    have : algebraMap S Sf a = algebraMap S Sf b := by
      simpa only [← IsScalarTower.algebraMap_apply] using! this
    obtain ⟨⟨_, m, hm, rfl⟩, h⟩ :=
      (IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S M) _).mp this
    refine ⟨⟨_, m, hm, rfl⟩, FaithfulSMul.algebraMap_injective (integralClosure R S) S ?_⟩
    simpa only [← IsScalarTower.algebraMap_apply]

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'
hf : LinearMap.lTensor M f = 0
⊢ f = 0

Tactic:
have := lTensor_reflects_exact R M f LinearMap.id (by
      rw [LinearMap.exact_iff, hf, LinearMap.range_zero, LinearMap.ker_eq_bot]
      apply Module.Flat.lTensor_preserves_injective_linearMap
      exact fun _ _ h => h)
    ext x; simpa using this (f x)

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ R ∙ x * y ≤ M

Tactic:
span_singleton_le_iff_mem

Goal state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ x * y ∈ M
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst✝ : NoZeroDivisors S
h : Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic R[X] S[X]

Tactic:
have := h.noZeroDivisors _ (map_zero _) (map_mul _); infer_instance

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

Goal state before:
pp: case pos
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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst✝ : NoZeroDivisors S
h : Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)

Tactic:
have := h.noZeroDivisors _ (map_zero _) (map_mul _); infer_instance

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

Goal state before:
pp: case h.refine_1
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ A ∙ x * y ≤ M

Tactic:
span_singleton_le_iff_mem

Goal state after:
case h.refine_1
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ x * y ∈ M
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
inst✝¹ : I.IsPrime
J : Ideal S
inst✝ : J.IsPrime
f : R →+* S
hf : I = comap f J
r : R
⊢ (map I J f hf) ((algebraMap R I.ResidueField) r) = (algebraMap S J.ResidueField) (f r)

Tactic:
rw [IsScalarTower.algebraMap_apply R (Localization.AtPrime I)]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
inst✝¹ : I.IsPrime
J : Ideal S
inst✝ : J.IsPrime
f : R →+* S
hf : I = comap f J
r : R
⊢ (map I J f hf) ((algebraMap (Localization.AtPrime I) I.ResidueField) ((algebraMap R (Localization.AtPrime I)) r)) =
    (algebraMap S J.ResidueField) (f r)
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
⊢ KrullDimLE 0 R

Tactic:
rwa [Ring.krullDimLE_zero_iff]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
⊢ comap f '' zeroLocus ↑I = zeroLocus ↑(Ideal.comap f I)

Tactic:
simp only [Set.ext_iff, Set.mem_image, mem_zeroLocus, SetLike.coe_subset_coe]

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
⊢ ∀ (x : PrimeSpectrum R), (∃ x_1, I ≤ x_1.asIdeal ∧ comap f x_1 = x) ↔ Ideal.comap f I ≤ x.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ x' - (x' - x) ∈ p.asIdeal

Tactic:
refine p.asIdeal.sub_mem hx' (hp ?_)

Goal state after:
case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ x' - x ∈ ker f
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: 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
⊢ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
obtain ⟨t, ht⟩ :=
    hUc.elim_finite_subcover (b ∘ f') (fun i => hb.isOpen (Set.mem_range_self _)) (by rw [e])

Goal state after:
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
⊢ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
Us : Set (Opens α)
x : α
⊢ x ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u

Tactic:
by
  simp_rw [sSup_eq_iSup, mem_iSup, exists_prop]

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s = univ ↔ IsClosed[inst✝] s

Tactic:
by
  simp [coborder, sdiff_eq_empty, closure_subset_iff_isClosed]

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U : Opens α
⊢ U ≠ ⊥ ↔ (↑U).Nonempty

Tactic:
Ne,

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
U : Opens α
⊢ ¬U = ⊥ ↔ (↑U).Nonempty
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
t : Set ↑(f ⁻¹' s)
this :
  ∀ (u : Set α),
    IsOpen[inst✝¹] u → Subtype.val ⁻¹' u = t → ∃ v, IsOpen[inst✝] v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t
⊢ IsOpen[instTopologicalSpaceSubtype] t → IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f '' t)

Tactic:
by
      simpa [isOpen_induced_iff]

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

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
B : (i : ι) → Set (Opens (α i))
hB : ∀ (i : ι), IsBasis (B i)
⊢ IsBasis (⋃ i, (fun U ↦ { carrier := Sigma.mk i '' U.carrier, is_open' := ⋯ }) '' B i)

Tactic:
by
  convert! TopologicalSpace.IsTopologicalBasis.sigma hB
  simp only [IsBasis, Set.image_iUnion, ← Set.image_comp]
  simp

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ DenseRange f ↔ ∀ (i : ι), DenseRange ((U i).carrier.restrictPreimage f)

Tactic:
simp_rw [denseRange_iff_closure_range, Set.range_restrictPreimage,
    ← (U _).2.isOpenEmbedding_subtypeVal.isOpenMap.preimage_closure_eq_closure_preimage
      continuous_subtype_val]
  simp only [Opens.carrier_eq_coe, SetLike.coe_sort_coe, preimage_eq_univ_iff,
    Subtype.range_coe_subtype, SetLike.mem_coe]
  rw [← iUnion_subset_iff, ← Set.univ_subset_iff, iff_iff_eq]
  congr 1
  exact hU.iSup_set_eq_univ.symm

Goal state after:
Module: Mathlib.Order.Ideal

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

Tactic:
top_mem_iff_eq_top

Goal state after:
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
⊢ ¬I = ⊤ ↔ ¬I = ⊤
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
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)

Tactic:
Module.FaithfullyFlat.lTensor_bijective_iff_bijective

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 ⇑(Hom.hom g)
⊢ Function.Bijective ⇑(ConcreteCategory.hom g)
Module: Mathlib.RingTheory.Ideal.GoingDown

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

Tactic:
use Q

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

Goal state before:
pp: case h₁
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ zeroLocus ↑I ≠ ∅ ↔ I ≠ ⊤

Tactic:
Ne,

Goal state after:
case h₁
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ ¬zeroLocus ↑I = ∅ ↔ I ≠ ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
⊢ (range (comap (algebraMap R[X] (Away c)[X])))ᶜ = range (comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Tactic:
let := (mapRingHom (algebraMap R (Away c))).toAlgebra

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
this : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
⊢ (range (comap (algebraMap R[X] (Away c)[X])))ᶜ = range (comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
hG : exponent G = p
g : G
hg : g ≠ 1
⊢ orderOf g = p

Tactic:
Ne,

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
hG : exponent G = p
g : G
hg : ¬g = 1
⊢ orderOf g = p
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : exponent G ≠ 0 ↔ (Set.range orderOf).Finite
⊢ exponent G = 0 ↔ (Set.range orderOf).Infinite

Tactic:
Ne,

Goal state after:
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : ¬exponent G = 0 ↔ (Set.range orderOf).Finite
⊢ exponent G = 0 ↔ (Set.range orderOf).Infinite
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ zpowers g
a b : ZMod (Nat.card G)
h : g ^ a.val = g ^ b.val
⊢ a = b

Tactic:
pow_eq_pow_iff_modEq,

Goal state after:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ zpowers g
a b : ZMod (Nat.card G)
h : a.val ≡ b.val [MOD orderOf g]
⊢ a = b
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_3
inst✝ : MulAction G α
this : Finite α
hpα : Nat.card ↑(fixedPoints G α) = 0
⊢ p ∣ Nat.card α

Tactic:
rw [← Nat.modEq_zero_iff_dvd, ← hpα]

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst✝ : MulAction G α
this : Finite α
hpα : Nat.card ↑(fixedPoints G α) = 0
⊢ Nat.card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h : p ∣ (↑P).index
⊢ False

Tactic:
rw [P.index_eq_card] at h

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h : p ∣ Nat.card (G ⧸ ↑P)
⊢ False
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
⊢ ∃ H, Nat.card ↥H = p ^ n

Tactic:
have : Fact p.Prime := ⟨hp⟩
  have : Finite G := Nat.finite_of_card_ne_zero <| by linarith [Nat.one_le_pow n p hp.pos]
  obtain ⟨m, hm⟩ := h.exists_card_eq
  refine exists_subgroup_card_pow_prime _ ?_
  rw [hm] at hn ⊢
  exact pow_dvd_pow _ <| (Nat.pow_le_pow_iff_right hp.one_lt).1 hn

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
Q : Sylow p G
x✝ : G
h1 : P = Q
x : G
h2 : P = default
⊢ Q = default

Tactic:
← h1,

Goal state after:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
Q : Sylow p G
x✝ : G
h1 : P = Q
x : G
h2 : P = default
⊢ P = default
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case inr
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer ↑P ≤ K
⊢ normalizer ↑↑P = ⊤

Tactic:
have := hnc _ hK

Goal state after:
case inr
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer ↑P ≤ K
this : K.Normal
⊢ normalizer ↑↑P = ⊤
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
f : R[X]
m : AEval R M a
⊢ (of R M a).symm ((r • f) • m) = (of R M a).symm (r • f • m)

Tactic:
rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul]

Goal state after: