mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
⊢ (((((compHom (D k)).comp Φ).comp (monomial m).toAddMonoidHom) r).comp (monomial n).toAddMonoidHom) s =
    ((((∑ x ∈ antidiagonal k, (compHom.comp ((compHom Φ) (D x.1))).flip (D x.2)).comp (monomial m).toAddMonoidHom)
            r).comp
        (monomial n).toAddMonoidHom)
      s

Tactic:
simp only [Φ, D, finsetSum_apply, coe_mulLeft, coe_comp, flip_apply, Function.comp_apply,
             hasseDeriv_monomial, LinearMap.toAddMonoidHom_coe, compHom_apply_apply,
             coe_mul, monomial_mul_monomial]

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
⊢ (monomial (m + n - k)) (↑((m + n).choose k) * (r * s)) =
    ∑ x ∈ antidiagonal k, (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s))
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
← mul_scaleRoots,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).scaleRoots r = r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ (C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod).roots = m

Tactic:
roots_C_mul _ hf0,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ (Multiset.map (fun x ↦ X - C x) m).prod.roots = m
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

pp: case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
· use integralNormalization p
    have : p ≠ 0 := fun h'' => by
      rw [h'', natDegree_zero] at h'
      exact Nat.not_succ_le_zero 0 h'
    use monic_integralNormalization this
    rw [integralNormalization_eval₂_leadingCoeff_mul h' f x, h, mul_zero]

Goal state after:
case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
⊢ f.IsIntegralElem (f p.leadingCoeff * x)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalization M S
R' : Type u_3
inst✝³ : CommRing R'
inst✝² : Algebra R R'
inst✝¹ : Algebra S R'
inst✝ : IsScalarTower R S R'
p : S[X]
x : R'
hx : (aeval x) p = 0
⊢ (aeval x) (integerNormalization M p) = 0

Tactic:
rwa [aeval_def, IsScalarTower.algebraMap_eq R S R', integerNormalization_eval₂_eq_zero]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this : g = C g.leadingCoeff * (Multiset.map (fun x ↦ X - C x) g.roots).prod
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (s ×ˢ g.roots)).prod = (Multiset.map (fun x ↦ eval x g) s).prod

Tactic:
hg.leadingCoeff,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this : g = C 1 * (Multiset.map (fun x ↦ X - C x) g.roots).prod
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (s ×ˢ g.roots)).prod = (Multiset.map (fun x ↦ eval x g) s).prod
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
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal
⊢ comap ((algebraMap S Sₚ).comp (algebraMap R S)) Qₚ = under R (comap (algebraMap Rₚ Sₚ) Qₚ)

Tactic:
← IsLocalization.map_comp (P := S) (Q := Sₚ) (g := algebraMap R S)
    (M := P.primeCompl) (T := Algebra.algebraMapSubmonoid S P.primeCompl) (S := Rₚ)
    (fun p hp => Algebra.mem_algebraMapSubmonoid_of_mem ⟨p, hp⟩)

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal
⊢ comap ((IsLocalization.map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)) Qₚ = under R (comap (algebraMap Rₚ Sₚ) Qₚ)
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
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FaithfulSMul R S
P : Ideal R
inst✝ : P.IsMaximal
⊢ ∃ Q, Q.IsMaximal ∧ Q.LiesOver P

Tactic:
liesOver_iff,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FaithfulSMul R S
P : Ideal R
inst✝ : P.IsMaximal
⊢ ∃ Q, Q.IsMaximal ∧ P = under R Q
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
h : Nontrivial R
⊢ Nonempty (PrimeSpectrum R)

Tactic:
obtain ⟨I, hI⟩ := Ideal.exists_maximal R

Goal state after:
case refine_2
R : Type u
inst✝ : CommSemiring R
h : Nontrivial R
I : Ideal R
hI : I.IsMaximal
⊢ Nonempty (PrimeSpectrum R)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asIdeal

Tactic:
rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_ofPred_eq]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q'.Monic

pp: case refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ eval₂ (algebraMap R S) t q' = 0

Tactic:
· refine monic_of_natDegree_le_of_coeff_eq_one (q.natDegree + N) ?_ ?_
    · refine natDegree_sum_le_of_forall_le _ _ fun i hi ↦ ?_
      grw [natDegree_mul_le, natDegree_pow_le, natDegree_X_le, natDegree_reflect_le]
      simp [max_eq_left (hN _), le_natDegree_of_mem_supp _ hi]
    · simp only [sum, finsetSum_coeff, coeff_X_pow_mul', coeff_reflect, q']
      rw [Finset.sum_eq_single q.natDegree]
      · simp [hqm.leadingCoeff]
      · intro i hi₁ hi₂
        have : N + i < q.natDegree + N :=
          add_comm N i ▸ add_lt_add_left ((le_natDegree_of_mem_supp _ hi₁).lt_of_ne hi₂) _
        simpa [(le_natDegree_of_mem_supp _ hi₁).trans, revAt, this.not_ge] using
          coeff_eq_zero_of_natDegree_lt (by grind)
      · simp +contextual

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ eval₂ (algebraMap R S) t q' = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
⊢ zeroLocus s = ∅

Tactic:
Set.eq_empty_iff_forall_notMem

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
⊢ ∀ (x : PrimeSpectrum R), x ∉ zeroLocus s
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
r : R
⊢ (∃ y ∈ vanishingIdeal t, ∃ z ∈ vanishingIdeal t', y + z = r) → ∀ x ∈ t ∩ t', r ∈ x.asIdeal

Tactic:
rintro ⟨f, hf, g, hg, rfl⟩ x ⟨hxt, hxt'⟩

Goal state after:
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : f ∈ vanishingIdeal t
g : R
hg : g ∈ vanishingIdeal t'
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal
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
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
⊢ Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A

Tactic:
by
  simp_rw [Algebra.isAlgebraic_def, Algebra.IsIntegral.isAlgebraic_iff R S]

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

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

Tactic:
rw [a.2.1, mul_comm, eq, b.2.1]

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 }
hac : a ≤ c
hbc : b ≤ c
⊢ (↑a).1 * (↑c).1 + (↑a).2 * ((↑b).1 * (↑c).1) = (↑a).1 + (↑a).2 * (↑b).1

Tactic:
rw [hac, hbc]

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 }
hab : a ≤ b
hac : a ≤ c
⊢ a ≤ (bᶜ ⊔ cᶜ)ᶜ

Tactic:
simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup, ← mul_assoc]

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 }
hab : a ≤ b
hac : a ≤ c
⊢ (↑a).1 * (↑b).1 * (↑c).1 = (↑a).1
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case a
ι : Type u_3
R : ι → Type u_4
inst✝² : (i : ι) → CommRing (R i)
inst✝¹ : _root_.Finite ι
S : Type u_5
inst✝ : CommRing S
f : S →+* (i : ι) → R i
⊢ Set.range (comap f) ⊆ ⋃ i, Set.range (comap f ∘ comap (Pi.evalRingHom R i))

Tactic:
rintro _ ⟨p, rfl⟩

Goal state after:
case a
ι : Type u_3
R : ι → Type u_4
inst✝² : (i : ι) → CommRing (R i)
inst✝¹ : _root_.Finite ι
S : Type u_5
inst✝ : CommRing S
f : S →+* (i : ι) → R i
p : PrimeSpectrum ((i : ι) → R i)
⊢ comap f p ∈ ⋃ i, Set.range (comap f ∘ comap (Pi.evalRingHom R i))
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
⊢ ∀ (a b : α), le (inf a b) a

Tactic:
intros; simp [eq_le, eq_inf]

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
⊢ ∀ (a b : α), le (inf a b) b

Tactic:
intros; simp [eq_le, eq_inf]

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
⊢ ∀ (a : α), ⊤ \ a = hnot a

Tactic:
by simp +instances [eq_le, eq_sdiff, eq_top, eq_hnot]

Goal state after:
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✝] (coborder (U ∩ Z))

Tactic:
rw [coborder_eq_union_frontier_compl, inter_union_distrib_right, this,
      inter_univ]

Goal state after:
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))ᶜ)
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 (f ∘ Subtype.val) (𝓝 ((f ∘ Subtype.val) x))

Tactic:
← Filter.comap_comap

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 Subtype.val (Filter.comap f (𝓝 ((f ∘ Subtype.val) x)))
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
⊢ ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i) = ⊤

Tactic:
← top_le_iff

Goal state after:
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
⊢ ⊤ ≤ ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i)
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Closeds α
h : s.carrier = t.carrier
⊢ s = t

Tactic:
cases s; cases t; congr

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Clopens α
h : (fun s ↦ s.carrier) s = (fun s ↦ s.carrier) t
⊢ s = t

Tactic:
cases s; cases t; congr

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : IrreducibleCloseds α
h : s.carrier = t.carrier
⊢ s = t

Tactic:
cases s; cases t; congr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : Compacts α
h : s.carrier = t.carrier
⊢ s = t

Tactic:
cases s; cases t; congr

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
⊢ QuasiSober α ↔ ∀ (i : ι), QuasiSober ↥(U i)

Tactic:
by
  refine ⟨fun h i ↦ (U i).isOpenEmbedding'.quasiSober, fun hU' ↦ (quasiSober_iff _).mpr ?_⟩
  · rintro t ⟨⟨x, hx⟩, h⟩ h'
    obtain ⟨i, hi⟩ := hU.exists_mem x
    have H : IsIrreducible ((↑) ⁻¹' t : Set (U i)) :=
      ⟨⟨⟨x, hi⟩, hx⟩, h.preimage (U i).isOpenEmbedding'⟩
    use H.genericPoint
    apply le_antisymm
    · simpa [h'.closure_subset_iff, h'.closure_eq] using!
        continuous_subtype_val.closure_preimage_subset _ H.isGenericPoint_genericPoint_closure.mem
    rw [← image_singleton, ← closure_image_closure continuous_subtype_val,
      H.isGenericPoint_genericPoint_closure.def]
    refine (subset_closure_inter_of_isPreirreducible_of_isOpen h (U i).isOpen ⟨x, ⟨hx, hi⟩⟩).trans
      (closure_mono ?_)
    simpa only [inter_comm t, ← Subtype.image_preimage_coe] using! Set.image_mono subset_closure

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) →
    ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂

Tactic:
rintro h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩
        exact h x y

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✝
ι✝ : Type u
S : ι✝ → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι✝), IsClosed (S i)
I : ι✝ → Ideal R
hI : ∀ (i : ι✝), S i = zeroLocus ↑(I i)
S_empty : ⨆ i, I i = ⊤
⊢ ∃ u, ⨆ i ∈ u, I i = ⊤

Tactic:
← top_le_iff

Goal state after:
R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
ι✝ : Type u
S : ι✝ → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι✝), IsClosed (S i)
I : ι✝ → Ideal R
hI : ∀ (i : ι✝), S i = zeroLocus ↑(I i)
S_empty : ⊤ ≤ ⨆ i, I i
⊢ ∃ u, ⊤ ≤ ⨆ i ∈ u, I i
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case add
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
D : Derivation R A M
x : A
p✝ q✝ : R[X]
a✝¹ : D ((aeval x) p✝) = (aeval x) (derivative p✝) • D x
a✝ : D ((aeval x) q✝) = (aeval x) (derivative q✝) • D x
⊢ D ((aeval x) (p✝ + q✝)) = (aeval x) (derivative (p✝ + q✝)) • D x

pp: case monomial
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
D : Derivation R A M
x : A
n✝ : ℕ
a✝¹ : R
a✝ : D ((aeval x) (C a✝¹ * X ^ n✝)) = (aeval x) (derivative (C a✝¹ * X ^ n✝)) • D x
⊢ D ((aeval x) (C a✝¹ * X ^ (n✝ + 1))) = (aeval x) (derivative (C a✝¹ * X ^ (n✝ + 1))) • D x

Tactic:
· simp [add_smul, *]

Goal state after:
case monomial
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
D : Derivation R A M
x : A
n✝ : ℕ
a✝¹ : R
a✝ : D ((aeval x) (C a✝¹ * X ^ n✝)) = (aeval x) (derivative (C a✝¹ * X ^ n✝)) • D x
⊢ D ((aeval x) (C a✝¹ * X ^ (n✝ + 1))) = (aeval x) (derivative (C a✝¹ * X ^ (n✝ + 1))) • D x
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ exponent G = 1

Tactic:
simp_rw [exponent, dif_pos h]

Goal state after:
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ Nat.find h = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ g ^ (p ^ (exponent G).factorization p * k) = 1

Tactic:
← hk

Goal state after:
case hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ g ^ exponent G = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Subsingleton R
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

Tactic:
refine ⟨0, 0, ?_, ?_, ?_, ?_⟩ <;> apply Subsingleton.elim

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case refine_1
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
x✝ : ∃ n, Nat.card G ∣ p ^ n
n : ℕ
hn : Nat.card G ∣ p ^ n
⊢ (Nat.card G).primeFactors ⊆ p.primeFactors

Tactic:
rcases eq_or_ne n 0 with (rfl | hn0)
    · simp_all
    grw [← Nat.primeFactors_pow p hn0, Nat.primeFactors_mono hn <| pow_ne_zero n h]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ exponent ((i : ι) → M i) = univ.lcm fun x ↦ exponent (M x)

Tactic:
by
  refine dvd_antisymm ?_ ?_
  · refine exponent_dvd_of_forall_pow_eq_one fun m ↦ ?_
    ext i
    rw [Pi.pow_apply, Pi.one_apply, ← orderOf_dvd_iff_pow_eq_one]
    apply dvd_trans (Monoid.order_dvd_exponent (m i))
    exact Finset.dvd_lcm (mem_univ i)
  · apply Finset.lcm_dvd fun i _ ↦ ?_
    exact MonoidHom.exponent_dvd (f := Pi.evalMonoidHom (M ·) i) (Function.surjective_eval i)

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
h : ↑P ≤ N
⊢ ↑P ≤ N.subtype.range

Tactic:
range_subtype

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
h : ↑P ≤ N
⊢ ↑P ≤ N