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

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
this : x ^ i * y ^ j = 0
⊢ k.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2) = 0

Tactic:
simp only [this, nsmul_eq_mul, mul_zero]

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case pos
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : s.Finite
⊢ ⨅ s, (↑↑s).encard ≤ s.encard

pp: case neg
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : ¬s.Finite
⊢ ⨅ s, (↑↑s).encard ≤ s.encard

Tactic:
· exact iInf_le_of_le ⟨hs.toFinset, by simpa⟩ (by simp)

Goal state after:
case neg
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : ¬s.Finite
⊢ ⨅ s, (↑↑s).encard ≤ s.encard
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
⊢ ∃ s, s.encard = ↑p.spanFinrank ∧ span R s = p

Tactic:
obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p
  refine ⟨s, ⟨?_, hs₂⟩⟩
  have := fg_iff_spanRank_eq_spanFinrank.mpr h
  rw [Set.encard, ENat.card, spanFinrank, hs₁, this]
  simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
⊢ ∃ s, #↑s ≤ p.spanRank + q.spanRank ∧ span R s = p ⊔ q

Tactic:
obtain ⟨sp, ⟨hp₁, rfl⟩⟩ := exists_span_set_card_eq_spanRank p

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
q : Submodule R M
sp : Set M
hp₁ : #↑sp = (span R sp).spanRank
⊢ ∃ s, #↑s ≤ (span R sp).spanRank + q.spanRank ∧ span R s = span R sp ⊔ q
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1
⊢ (-(M.charpoly - ∏ i, (X - C (M i i)))).degree < ↑(Fintype.card n)

Tactic:
rw [degree_neg]

Goal state after:
case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1
⊢ (M.charpoly - ∏ i, (X - C (M i i))).degree < ↑(Fintype.card n)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : (aeval x.1) p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : (aeval x.2) p₂ = 0
⊢ (0, (aeval x.2) p₁ * (aeval x.2) p₂) = 0

Tactic:
hp₂Eval,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : (aeval x.1) p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : (aeval x.2) p₂ = 0
⊢ (0, (aeval x.2) p₁ * 0) = 0
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ r • x ∈ S[x]

Tactic:
rw [← algebraMap_smul S]; apply Subalgebra.smul_mem; exact Algebra.subset_adjoin rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
s : Finset n
i j : n
n✝ : ℕ
h : i ∈ s
⊢ (M.map (⇑C) i j).coeff n✝ = (C (M i j)).coeff n✝

Tactic:
simp [Matrix.one_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
s : Finset n
i j : n
n✝ : ℕ
h : i ∉ s
⊢ (1 i j).coeff n✝ = (C (1 i j)).coeff n✝

Tactic:
simp [Matrix.one_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
⊢ ((taylor r) p).degree = p.degree

Tactic:
by_cases hp : p = 0
  · rw [hp, map_zero]
  · rw [degree_eq_natDegree hp, degree_eq_iff_natDegree_eq ((taylor_eq_zero r p).not.2 hp),
      natDegree_taylor]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
hcharpolyRev : M.charpolyRev = (1 + X • (-M).map ⇑C).det
⊢ M.charpolyRev.coeff k = (-1) ^ k * ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det

Tactic:
hcharpolyRev,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
hcharpolyRev : M.charpolyRev = (1 + X • (-M).map ⇑C).det
⊢ (1 + X • (-M).map ⇑C).det.coeff k = (-1) ^ k * ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
hpq : p ∣ q
⊢ p.scaleRoots r ∣ q.scaleRoots r

Tactic:
by
  obtain ⟨a, rfl⟩ := hpq
  rw [← ((hr.pow (natDegree p + natDegree a - natDegree (p * a))).map
    (algebraMap R R[X])).dvd_mul_left, ← Algebra.smul_def, mul_scaleRoots]
  exact dvd_mul_right (scaleRoots p r) (scaleRoots a r)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inr.h
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ (X - C a).leadingCoeff ^ rootMultiplicity a p * q.leadingCoeff ≠ 0

Tactic:
leadingCoeff_X_sub_C,

Goal state after:
case inr.inr.h
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ 1 ^ rootMultiplicity a p * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain A
inst✝² : IsDomain B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ : A →ₐ[R] B
hφ : map (↑φ) (map (algebraMap R A) f) ≠ 0
hf : (map (algebraMap R B) f).roots = Multiset.map (⇑↑φ) (map (algebraMap R A) f).roots
⊢ ⇑φ '' f.rootSet A = f.rootSet B

Tactic:
simp [rootSet, aroots, hf, Multiset.toFinset_map]

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

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

Tactic:
leadingCoeff_X_sub_C,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
a : R
hf : ((X - C a) * f).Splits
hf₀ : ¬f = 0
this : (X - C a) * f = C (1 * f.leadingCoeff) * (Multiset.map (fun x ↦ X - C x) ((X - C a) * f).roots).prod
⊢ f.Splits
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
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (g.roots ×ˢ s)).prod =
    (-1) ^ (s.card * g.roots.card) * (Multiset.map (fun x ↦ eval x g) s).prod

Tactic:
by
  trans ((s ×ˢ g.roots).map fun ij ↦ (-1) * (ij.1 - ij.2)).prod
  · rw [← Multiset.map_swap_product, Multiset.map_map]; simp
  · rw [Multiset.prod_map_mul]; simp [map_sub_sprod_roots_eq_prod_map_eval _ _ hg hg']

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

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
⊢ f.Splits ↔ f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1

Tactic:
refine ⟨fun hf ↦ or_iff_not_imp_left.mpr fun h0 g hg hgf ↦
    (hf.of_dvd h0 hgf).degree_eq_one_of_irreducible hg, ?_⟩
  rintro (rfl | hf)
  · aesop
  by_cases hf0 : f = 0
  · simp [hf0]
  obtain ⟨u, hu⟩ := factors_prod hf0
  rw [← hu]
  refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits
  exact Splits.of_degree_eq_one (hf (irreducible_of_factor g hg) (dvd_of_mem_factors hg))

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

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
p : R[X]
p_ne_zero : p ≠ 0
px : (aeval z) p = 0
a : R := p.leadingCoeff
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
have a_ne_zero : a ≠ 0 := mt Polynomial.leadingCoeff_eq_zero.mp p_ne_zero

Goal state after:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
p : R[X]
p_ne_zero : p ≠ 0
px : (aeval z) p = 0
a : R := p.leadingCoeff
a_ne_zero : a ≠ 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization ↑f.symm ⋯).comp (mapPiLocalization (↑f) hf) = RingHom.id (PiLocalization R)

Tactic:
· rw [← mapPiLocalization_comp]
    simp_rw [RingEquiv.symm_comp, mapPiLocalization_id]

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∩ (frontier s)ᶜᶜ = closure[inst✝] s \ s

Tactic:
compl_compl,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∩ frontier s = closure[inst✝] s \ s
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∩ (closure[inst✝] s)ᶜᶜ = closure[inst✝] s \ s

Tactic:
compl_compl,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∩ closure[inst✝] s = closure[inst✝] s \ s
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
tfae_2_to_3 : IsOpen[inst✝] (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)) →
    ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
x✝ : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
H : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s := x✝
⊢ IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)

Tactic:
choose U hxU hU e using H
    refine ⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩
    · rintro ⟨_, ⟨⟨y, rfl⟩, ⟨_, ⟨hy, rfl⟩, hxU⟩⟩⟩
      exact e y hy ⟨hxU, x.2⟩
    · exact (subset_iUnion₂ _ _ <| hxU x ·)

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s

Tactic:
NoetherianSpace,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ WellFoundedGT (Opens α) ↔ ∀ (s : Opens α), IsCompact ↑s
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: case h
α : 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
⊢ (((↑x)ᶜ ⊔ (↑y)ᶜᶜ) ⊓ (↑z ⊓ (↑w)ᶜ) ⊔ t.sup fun x ↦ ↑x.1 ⊓ (↑x.2)ᶜ) =
    (↑x)ᶜ ⊓ (↑z ⊓ (↑w)ᶜ) ⊔ ↑y ⊓ ↑z ⊓ (↑w)ᶜ ⊔ t.sup fun x ↦ ↑x.1 ⊓ (↑x.2)ᶜ

Tactic:
compl_compl,

Goal state after:
case h
α : 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
⊢ (((↑x)ᶜ ⊔ ↑y) ⊓ (↑z ⊓ (↑w)ᶜ) ⊔ t.sup fun x ↦ ↑x.1 ⊓ (↑x.2)ᶜ) =
    (↑x)ᶜ ⊓ (↑z ⊓ (↑w)ᶜ) ⊔ ↑y ⊓ ↑z ⊓ (↑w)ᶜ ⊔ t.sup fun x ↦ ↑x.1 ⊓ (↑x.2)ᶜ
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
⊢ (fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }) ((fun I ↦ ⨆ U ∈ I, U.toOpens) I) =
    I

Tactic:
ext U

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
⊢ U ∈
      ↑((fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ })
          ((fun I ↦ ⨆ U ∈ I, U.toOpens) I)) ↔
    U ∈ ↑I
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
⊢ (fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }) ((fun I ↦ ⨆ U ∈ I, U.toOpens) I) =
    I

Tactic:
ext U
    dsimp
    change U.toOpens ≤ _ ↔ _
    refine ⟨fun H ↦ ?_, fun h ↦ le_iSup₂ (f := fun U (h : U ∈ I) ↦ U.toOpens) U h⟩
    simp only [← SetLike.coe_subset_coe, Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk] at H
    obtain ⟨s, hsI, hs, hU⟩ := U.isCompact.elim_finite_subcover_image (fun U _ ↦ U.2) H
    exact I.lower (a := hs.toFinset.sup fun i ↦ i) (by simpa [← SetLike.coe_subset_coe]) (by simpa)

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
t : Finset ↑Us
ht : U ⊆ ⋃ i ∈ t, f '' ↑↑i
⊢ ∃ V, IsCompact V.carrier ∧ f '' ↑V = U

Tactic:
refine ⟨⨆ s ∈ t, s.1, ?_, ?_⟩

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
t : Finset ↑Us
ht : U ⊆ ⋃ i ∈ t, f '' ↑↑i
⊢ IsCompact (⨆ s ∈ t, ↑s).carrier

case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
t : Finset ↑Us
ht : U ⊆ ⋃ i ∈ t, f '' ↑↑i
⊢ f '' ↑(⨆ s ∈ t, ↑s) = U
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_1
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
d : Derivation R A ↥I
⊢ (Ideal.Quotient.mkₐ R I).comp (liftOfDerivationToSquareZero I hI d) = IsScalarTower.toAlgHom R A (B ⧸ I)

Tactic:
ext x; exact liftOfDerivationToSquareZero_mk_apply I hI d x

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

Goal state before:
pp: a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
⊢ ((fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1) p ((a.lcm b).factorization p)).Coprime
    ((fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n) q ((a.lcm b).factorization q))

Tactic:
dsimp only

Goal state after:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
⊢ (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1).Coprime
    (if b.factorization q ≤ a.factorization q then 1 else q ^ (a.lcm b).factorization q)
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ (ulift.{u₁, u₂, u_1, u_2} f).Flat ↔ f.Flat

Tactic:
by
  refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
  · rwa [← comp_ulift_eq.{u₁, u₂} f, comp_iff_of_bijective_left (Equiv.bijective _),
      comp_iff_of_bijective_right (Equiv.bijective _)]
  · exact .comp (.comp (.of_bijective <| Equiv.bijective _) hf)
      (.of_bijective <| Equiv.bijective _)

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

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1) p ((a.lcm b).factorization p) ∣
    p ^ a.factorization p

Tactic:
dsimp only

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) ∣ p ^ a.factorization p
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n) p ((a.lcm b).factorization p) ∣
    p ^ b.factorization p

Tactic:
dsimp only

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) ∣ p ^ b.factorization p
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 : zeroLocus ↑(⨆ i, I i) = ∅
⊢ ∃ u, zeroLocus ↑(⨆ i ∈ u, I i) = ∅

Tactic:
zeroLocus_empty_iff_eq_top,

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.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R
⊢ basicOpen (f * g) ≤ basicOpen g

Tactic:
rw [basicOpen_mul f g]
  exact inf_le_right

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

Goal state before:
pp: α : 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) k = x
hk : g ^ k = x
⊢ g ^ k.natAbs ∈ H

Tactic:
by
            rcases k with k | k
            · rw [Int.ofNat_eq_natCast, Int.natAbs_natCast k, ← zpow_natCast,
                ← Int.ofNat_eq_natCast, hk]
              exact hx₁
            · rw [Int.natAbs_negSucc, ← Subgroup.inv_mem_iff H]; simp_all

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ s, s.Finite ∧ s✝ = (zeroLocus s)ᶜ
s : Set R
hs : s.Finite
e : s✝ = (zeroLocus s)ᶜ
⊢ (zeroLocus ↑hs.toFinset)ᶜ = s✝

Tactic:
simpa using e.symm

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ t, (zeroLocus ↑t)ᶜ = s✝
s : Finset R
e : (zeroLocus ↑s)ᶜ = s✝
⊢ s✝ = (zeroLocus ↑s)ᶜ

Tactic:
simpa using e.symm

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

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

Goal state before:
pp: G : Type u
inst✝ : Monoid G
S : Submonoid G
g : G
g_in_s : g ∈ S
⊢ g ^ exponent ↥S = 1

Tactic:
have := Monoid.pow_exponent_eq_one (⟨g, g_in_s⟩ : S)
  rwa [SubmonoidClass.mk_pow, ← OneMemClass.coe_eq_one] at this

Goal state after:
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
⊢ (I * J).radical = Ideal.radical 0

Tactic:
rw [← zeroLocus_eq_iff, Ideal.zero_eq_bot, zeroLocus_bot,
      zeroLocus_mul, hI', hJ', Set.compl_union_self]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
k : G → ℕ
hk : ∀ (g : G), orderOf g ∣ p ^ k g
this : Fintype G
g : G
left✝ : g ∈ Finset.univ
hg : ∀ x' ∈ Finset.univ, k x' ≤ k g
g' : G
⊢ orderOf g' ∣ p ^ k g

Tactic:
← Nat.pow_dvd_pow p <| hg g' <| Finset.mem_univ g'

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
k : G → ℕ
hk : ∀ (g : G), orderOf g ∣ p ^ k g
this : Fintype G
g : G
left✝ : g ∈ Finset.univ
hg : ∀ x' ∈ Finset.univ, k x' ≤ k g
g' : G
⊢ orderOf g' ∣ p ^ k g'
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : CommMonoid G
h : ∃ g, orderOf g = 0
⊢ exponent G = 0

Tactic:
obtain ⟨g, hg⟩ := h

Goal state after:
case pos
G : Type u
inst✝ : CommMonoid G
g : G
hg : orderOf g = 0
⊢ exponent G = 0