mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: case a
n x✝ : ℕ
h : x✝ ∈ range n.succ
⊢ n.choose x✝ ^ 2 = n.choose (x✝, n - x✝).1 * n.choose x✝

Tactic:
sq

Goal state after:
case a
n x✝ : ℕ
h : x✝ ∈ range n.succ
⊢ n.choose x✝ * n.choose x✝ = n.choose (x✝, n - x✝).1 * n.choose x✝
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
A : Matrix n n R
h : IsUnit A
⊢ A⁻¹.charpoly = (-1) ^ Fintype.card n * C A.det⁻¹ʳ * A.charpolyRev

Tactic:
by
  have : Invertible A := h.invertible
  calc
  _ = (scalar n X - C.mapMatrix A⁻¹).det := rfl
  _ = C (A⁻¹ * A).det * (scalar n X - C.mapMatrix A⁻¹).det := by simp
  _ = C A⁻¹.det * C A.det * (scalar n X - C.mapMatrix A⁻¹).det := by rw [det_mul]; simp
  _ = C A⁻¹.det * (C A.det * (scalar n X - C.mapMatrix A⁻¹).det) := by ac_rfl
  _ = C A⁻¹.det * (C.mapMatrix A * (scalar n X - C.mapMatrix A⁻¹)).det := by simp [RingHom.map_det]
  _ = C A⁻¹.det * (C.mapMatrix A * scalar n X - 1).det := by rw [mul_sub, ← map_mul]; simp
  _ = C A⁻¹.det * ((-1) ^ Fintype.card n * (1 - scalar n X * C.mapMatrix A).det) := by
    rw [← neg_sub, det_neg, det_one_sub_mul_comm]
  _ = _ := by simp [charpolyRev, smul_eq_diagonal_mul]; ac_rfl

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 : M ^ k = 0
⊢ 1 = 1 - 0

Tactic:
sub_zero

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 : M ^ k = 0
⊢ 1 = 1
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
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
rw [mem_antidiagonal] at hx

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
x : ℕ × ℕ
hx : x.1 + x.2 = k
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
h : n ≤ (p * q).natDegree
⊢ (p * q).coeff n * r ^ (p.natDegree + q.natDegree - (p * q).natDegree + ((p * q).natDegree - n)) =
    (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)

Tactic:
tsub_add_tsub_cancel natDegree_mul_le h

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
h : n ≤ (p * q).natDegree
⊢ (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n) = (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)
Module: Mathlib.Algebra.Polynomial.Splits

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

Tactic:
natDegree_C_mul hf0,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
| (Multiset.map (fun x ↦ X - C x) f.roots).prod.natDegree
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case mem
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
φ : R →+* S
p : R[X]
hp : p ∈ {x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x}
hφ : map φ p ≠ 0
⊢ (map φ p).roots = Multiset.map (⇑φ) p.roots

Tactic:
| mem p hp =>

Goal state after:
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
p : S[X]
i : ℕ
h : coeffIntegerNormalization M p i ≠ 0
⊢ i ∈ p.support

Tactic:
contrapose h
  simp only [mem_support_iff, ne_eq, not_not] at h
  exact coeffIntegerNormalization_of_coeff_zero M p i h

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra R B
f : R[X]
hf : (map (algebraMap R A) f).Splits
g : A →ₐ[R] B
⊢ Subalgebra.map g (Algebra.adjoin R (f.rootSet A)) = g.range ↔ Algebra.adjoin R (f.rootSet A) = ⊤

Tactic:
← Algebra.map_top

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra R B
f : R[X]
hf : (map (algebraMap R A) f).Splits
g : A →ₐ[R] B
⊢ Subalgebra.map g (Algebra.adjoin R (f.rootSet A)) = Subalgebra.map g ⊤ ↔ Algebra.adjoin R (f.rootSet A) = ⊤
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : p.comp (C y * X) = 0
⊢ False

Tactic:
apply_fun (coeff · p.natDegree) at h

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff p.natDegree = coeff 0 p.natDegree
⊢ False
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
⊢ RingHom.ker (algebraMap R S) ≤ P

Tactic:
by
    simp [(RingHom.injective_iff_ker_eq_bot _).mp (FaithfulSMul.algebraMap_injective R S)]

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

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

Tactic:
exact nonempty_iff_nontrivial

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus (insert 0 (s \ {0})) = zeroLocus s

Tactic:
← zeroLocus_insert_zero (s := s)

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus (insert 0 (s \ {0})) = zeroLocus (insert 0 s)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case hgt
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Submodule A A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
change Ideal A at M
  have hA_nont : Nontrivial A := IsDomain.toNontrivial
  by_cases h_topM : M = ⊤
  · rcases h_topM with rfl
    obtain ⟨p_id, h_nzp, h_pp⟩ : ∃ p : Ideal A, p ≠ ⊥ ∧ p.IsPrime := by
      apply Ring.not_isField_iff_exists_prime.mp h_fA
    use ({⟨p_id, h_pp⟩} : Multiset (PrimeSpectrum A)), le_top
    rwa [Multiset.map_singleton, Multiset.prod_singleton]
  by_cases h_prM : M.IsPrime
  · use ({⟨M, h_prM⟩} : Multiset (PrimeSpectrum A))
    rw [Multiset.map_singleton, Multiset.prod_singleton]
    exact ⟨le_rfl, h_nzI⟩
  obtain ⟨x, hx, y, hy, h_xy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left h_topM
  have lt_add : ∀ z ∉ M, M < M + span A {z} := by
    intro z hz
    refine lt_of_le_of_ne le_sup_left fun m_eq => hz ?_
    rw [m_eq]
    exact mem_sup_right (mem_span_singleton_self z)
  obtain ⟨Wx, h_Wx_le, h_Wx_ne⟩ := hgt (M + span A {x}) (lt_add _ hx) (ne_bot_of_gt (lt_add _ hx))
  obtain ⟨Wy, h_Wy_le, h_Wx_ne⟩ := hgt (M + span A {y}) (lt_add _ hy) (ne_bot_of_gt (lt_add _ hy))
  use Wx + Wy
  rw [Multiset.map_add, Multiset.prod_add]
  refine ⟨le_trans (mul_le_mul' h_Wx_le h_Wy_le) ?_, mt Ideal.mul_eq_bot.mp ?_⟩
  · rw [add_mul]
    apply sup_le (show M * (M + span A {y}) ≤ M from Ideal.mul_le_left)
    rw [mul_add]
    apply sup_le (show span A {x} * M ≤ M from Ideal.mul_le_right)
    rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]
  · rintro (hx | hy) <;> contradiction

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

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

Tactic:
by simp_rw [add_mul,
      mul_mul_mul_comm _ b.1.1, b.2.1, mul_zero, ← mul_assoc, a.2.1, zero_mul, add_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ 1 - 0 = ↑⊤

Tactic:
sub_zero

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ 1 = ↑⊤
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 R
hI : ker f = I
⊢ LeftInverse
    (fun x ↦
      match x with
      | ⟨{ asIdeal := p, isPrime := isPrime }, hp⟩ => { asIdeal := map f p, isPrime := ⋯ })
    fun p ↦ ⟨PrimeSpectrum.comap f p, ⋯⟩

Tactic:
by
    intro ⟨p, _⟩
    simp only [PrimeSpectrum.mk.injEq]
    exact p.map_comap_of_surjective f hf

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : max.IsMaximal
n d : R
hd : d ∈ { asIdeal := max, isMaximal := hmax }.asIdeal.primeCompl
hrange : (algebraMap R K) n * ((algebraMap R K) d)⁻¹ ∉ range ⇑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    (algebraMap R K) n * ((algebraMap R K) d)⁻¹ ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K ((algebraMap R K) n * ((algebraMap R K) d)⁻¹)) 1
hdenom : 1 ∉ denom
hle : denom ≤ max
⊢ False

Tactic:
exact hd (hle ⟨n, by simp [Algebra.smul_def, mul_left_comm, mul_inv_cancel₀ <|
      (map_ne_zero_iff _ <| IsFractionRing.injective R K).mpr fun h ↦ hd (h ▸ max.zero_mem :)]⟩)

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteLattice α
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
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
x✝ : Set α
⊢ IsGLB x✝ (sInf x✝)

Tactic:
simp +instances only [eq_le, eq_sInf, isGLB_sInf]

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ Dense (coborder s)

Tactic:
rw [dense_iff_closure_eq, coborder_eq_union_closure_compl, closure_union, ← univ_subset_iff]
  refine _root_.subset_trans ?_ (union_subset_union_right _ (subset_closure))
  simp

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

Goal state before:
pp: case h.refine_1
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
hW : IsCompact W.carrier
κ : Type u
a : κ → ι
heq : W = ⨆ k, U (a k)
s : Finset κ
hs : W.carrier ⊆ ⋃ i ∈ s, (U (a i)).carrier
⊢ W ≤ ⨆ k, U ((a ∘ Subtype.val) k)

pp: case h.refine_2
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
hW : IsCompact W.carrier
κ : Type u
a : κ → ι
heq : W = ⨆ k, U (a k)
s : Finset κ
hs : W.carrier ⊆ ⋃ i ∈ s, (U (a i)).carrier
⊢ ⨆ k, U ((a ∘ Subtype.val) k) ≤ W

Tactic:
· simpa [← SetLike.coe_subset_coe, Set.iUnion_subtype]

Goal state after:
case h.refine_2
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
hW : IsCompact W.carrier
κ : Type u
a : κ → ι
heq : W = ⨆ k, U (a k)
s : Finset κ
hs : W.carrier ⊆ ⋃ i ∈ s, (U (a i)).carrier
⊢ ⨆ k, U ((a ∘ Subtype.val) k) ≤ W
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
⊢ IsEmbedding f ↔ ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
simpa [isEmbedding_iff, forall_and] using and_congr (hU.isInducing_iff_restrictPreimage h)
    (injective_iff_injective_of_iUnion_eq_univ hU.iSup_set_eq_univ)

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case inr
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
a : CofiniteTopology α
hs : s ∈ ↑(pure a)
⊢ ∃ x ∈ s, ↑(pure a) ≤ pure x ∨ ↑(pure a) ≤ Filter.cofinite

Tactic:
· exact ⟨a, hs, Or.inl le_rfl⟩

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 : Closeds α
⊢ (Opens.compl ∘ ⇑ofDual) ((⇑toDual ∘ compl) s) = s

Tactic:
by simp [Closeds.compl_compl]

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 : (Closeds α)ᵒᵈ
⊢ (⇑toDual ∘ compl) ((Closeds.compl ∘ ⇑ofDual) s) = s

Tactic:
by simp [Closeds.compl_compl]

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : closure[inst✝¹] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z
⊢ (⋃₀ (irreducibleComponents α \ {Z}))ᶜ.Nonempty

Tactic:
contrapose! hZ
    rw [hZ, closure_empty, ← Set.nonempty_iff_empty_ne]
    exact H.1.nonempty

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 α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst✝¹] U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen[inst✝¹] V
hV'' : IsCompact V
⊢ IsCompact (f '' U ∩ f '' V)

Tactic:
exact
    H (f '' U) (f '' V) (image_mono hU) (h.isOpenMap _ hU') (hU''.image h.continuous)
      (image_mono hV) (h.isOpenMap _ hV') (hV''.image h.continuous)

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case insert
α✝ : Type u_1
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s✝ : Set (Set α)
a✝ : Set α
s : Set (Set α)
ha : a✝ ∉ s
hs : s.Finite
ih :
  (∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t) →
    (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen[inst✝¹] t) → s.Nonempty → IsCompact (⋂₀ s)
ho : ∀ t ∈ insert a✝ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ insert a✝ s, IsCompact t
h : ∀ t ∈ insert a✝ s, IsOpen[inst✝¹] t
⊢ (insert a✝ s).Nonempty → IsCompact (⋂₀ insert a✝ s)

Tactic:
obtain (rfl | hne) := s.eq_empty_or_nonempty

Goal state after:
case insert.inl
α✝ : Type u_1
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
a✝ : Set α
ha : a✝ ∉ ∅
hs : ∅.Finite
ih :
  (∀ t ∈ ∅, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t) →
    (∀ t ∈ ∅, IsCompact t) → (∀ t ∈ ∅, IsOpen[inst✝¹] t) → ∅.Nonempty → IsCompact (⋂₀ ∅)
ho : ∀ t ∈ insert a✝ ∅, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ insert a✝ ∅, IsCompact t
h : ∀ t ∈ insert a✝ ∅, IsOpen[inst✝¹] t
⊢ (insert a✝ ∅).Nonempty → IsCompact (⋂₀ insert a✝ ∅)

case insert.inr
α✝ : Type u_1
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s✝ : Set (Set α)
a✝ : Set α
s : Set (Set α)
ha : a✝ ∉ s
hs : s.Finite
ih :
  (∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t) →
    (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen[inst✝¹] t) → s.Nonempty → IsCompact (⋂₀ s)
ho : ∀ t ∈ insert a✝ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ insert a✝ s, IsCompact t
h : ∀ t ∈ insert a✝ s, IsOpen[inst✝¹] t
hne : s.Nonempty
⊢ (insert a✝ s).Nonempty → IsCompact (⋂₀ insert a✝ s)
Module: Mathlib.Topology.QuasiSeparated

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

Tactic:
obtain (rfl | hne) := s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSeparatedSpace α
inst✝ : CompactSpace α
hf : ∅.Finite
ho : ∀ t ∈ ∅, IsOpen[inst✝²] t ∨ IsClosed[inst✝²] t
hc : ∀ t ∈ ∅, IsCompact t
⊢ IsCompact (⋂₀ ∅)

case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSeparatedSpace α
inst✝ : CompactSpace α
s : Set (Set α)
hf : s.Finite
ho : ∀ t ∈ s, IsOpen[inst✝²] t ∨ IsClosed[inst✝²] t
hc : ∀ t ∈ s, IsCompact t
hne : s.Nonempty
⊢ IsCompact (⋂₀ s)
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
h : Function.Injective (Compacts.map f hf)
⊢ Function.Injective ((fun x ↦ {x}) ∘ f)

Tactic:
simp_rw [Function.comp_def, ← map_singleton hf]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
h : Function.Injective (Compacts.map f hf)
⊢ Function.Injective fun x ↦ Compacts.map f hf {x}
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s : Set X
hs : IsConstructible s
⊢ P s hs

Tactic:
by
  induction s, hs using BooleanSubalgebra.closure_sdiff_sup_induction with
  | isSublattice =>
    exact ⟨fun s hs t ht ↦ ⟨hs.1.union ht.1, hs.2.union ht.2⟩,
      fun s hs t ht ↦ ⟨hs.1.inter ht.1, hs.2.inter_isOpen ht.2 ht.1⟩⟩
  | bot_mem => exact ⟨isOpen_empty, .empty⟩
  | top_mem => exact ⟨isOpen_univ, .univ⟩
  | sdiff U hU V hV =>
    have := isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis _ basis isCompact_basis
    obtain ⟨s, hs, rfl⟩ := (this _).1 ⟨hU.2.isCompact, hU.1⟩
    obtain ⟨t, ht, rfl⟩ := (this _).1 ⟨hV.2.isCompact, hV.1⟩
    simp_rw [iUnion_sdiff]
    induction s, hs using Set.Finite.induction_on with
    | empty => simpa using sdiff (Classical.arbitrary _) {Classical.arbitrary _}
    | @insert i s hi hs ih =>
      simp_rw [biUnion_insert]
      exact union _ _ _
        (.biUnion hs fun i _ ↦ ((isCompact_basis _).isConstructible (basis.isOpen ⟨i, rfl⟩)).sdiff
          <| .biUnion ht fun j _ ↦ (isCompact_basis _).isConstructible (basis.isOpen ⟨_, rfl⟩))
        (sdiff _ _ ht)
        (ih ⟨isOpen_biUnion fun  _ _ ↦ basis.isOpen ⟨_, rfl⟩, .biUnion hs
          fun i _ ↦ (isCompact_basis _).isRetrocompact (basis.isOpen ⟨i, rfl⟩)⟩)
  | sup s _ t _ hs' ht' => exact union _ _ _ _ hs' ht'

Goal state after:
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
⊢ Derivation R A ↥I

Tactic:
by
  refine
    { diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ?_ with
      map_one_eq_zero' := ?_
      leibniz' := ?_ }
  · ext; simp [e]
  · ext; simp
  · intro x y
    let F := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) (by rw [e]; ext; rfl)
    have : (f x - algebraMap A B x) * (f y - algebraMap A B y) = 0 := by
      rw [← Ideal.mem_bot, ← hI, pow_two]
      convert! Ideal.mul_mem_mul (F x).2 (F y).2 using 1
    ext
    dsimp only [Submodule.coe_add, Submodule.coe_mk, LinearMap.coe_mk,
      diffToIdealOfQuotientCompEq_apply, Submodule.coe_smul_of_tower, IsScalarTower.coe_toAlgHom',
      LinearMap.toFun_eq_coe]
    simp only [map_mul, sub_mul, mul_sub, Algebra.smul_def] at this ⊢
    rw [sub_eq_iff_eq_add, sub_eq_iff_eq_add] at this
    simp only [this]
    ring

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

Goal state before:
pp: R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)

Tactic:
convert! h

Goal state after:
case e'_5
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
algInst✝ : Algebra R S := ⋯
a✝ : ↑s
e_4✝ : OreLocalization.instAddCommMonoidOreLocalization = CommRing.toCommSemiring.toAddCommMonoid
⊢ OreLocalization.instModuleOfIsScalarTower = Algebra.toModule
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : (Ideal.span {x} * Ideal.span {y}).radical ≤ I
⊢ (Ideal.span {x} ⊓ Ideal.span {y}).radical ≤ I

Tactic:
simpa only [Ideal.radical_inf, Ideal.radical_mul] using h'

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H'.subgroupOf H = ⊥ ∨ H'.subgroupOf H = ⊤) ↔
    H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H' = ⊥ ∨ H' = H

Tactic:
simp +contextual [disjoint_of_le_iff_left_eq_bot, LE.le.ge_iff_eq]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf
      (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)) *
        y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)

Tactic:
rw [(h.pow_pow _ _).orderOf_mul_eq_mul_orderOf_of_coprime]
  all_goals iterate 2 rw [orderOf_pow_orderOf_div]; try rw [Coprime]
  all_goals simp [factorizationLCMLeft_mul_factorizationLCMRight, factorizationLCMLeft_dvd_left,
    factorizationLCMRight_dvd_right, coprime_factorizationLCMLeft_factorizationLCMRight, hx, hy]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
⊢ orderOf t < orderOf (t ^ p ^ k * g)

Tactic:
obtain ⟨a, ha⟩ := Nat.exists_eq_add_of_lt hpe

Goal state after:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
⊢ orderOf t < orderOf (t ^ p ^ k * g)