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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
⊢ (mapRingHom f) X = X

Tactic:
simp only [coe_mapRingHom, map_X]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
x : ↥(integralClosure R K)
⊢ ↑(1 • x) = ↑x

Tactic:
exact one_smul G (x : K)

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

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
⊢ f (p.coeff i) * f s ^ (p.natDegree - i) * (f s * a) ^ i = f (p.coeff i) * f s ^ (p.natDegree - i + i) * a ^ i

Tactic:
pow_add,

Goal state after:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
⊢ f (p.coeff i) * f s ^ (p.natDegree - i) * (f s * a) ^ i = f (p.coeff i) * (f s ^ (p.natDegree - i) * f s ^ i) * a ^ i
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : R[X]
r : R
inst✝ : NoZeroDivisors R
a : R[X]
⊢ p.scaleRoots r ∣ (p * a).scaleRoots r

Tactic:
rw [mul_scaleRoots_of_noZeroDivisors]

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p : R[X]
r : R
inst✝ : NoZeroDivisors R
a : R[X]
⊢ p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

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

Tactic:
obtain ⟨a, rfl⟩ := hpq
  rw [mul_scaleRoots_of_noZeroDivisors]
  exact dvd_mul_right (scaleRoots p r) (scaleRoots a r)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

Tactic:
cases subsingleton_or_nontrivial R
  · simp [Subsingleton.elim p 0]
  obtain rfl | hp := eq_or_ne p 0
  · simp
  obtain ⟨q, e, hq⟩ := exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp a
  have hq0 : q ≠ 0 := by contrapose hp; simp_all
  conv_lhs => rw [e]
  rw [mul_scaleRoots', pow_scaleRoots', X_sub_C_scaleRoots, mul_comm, mul_comm _ (q.scaleRoots r),
    rootMultiplicity_mul_X_sub_C_pow (q.scaleRoots_ne_zero hq0 _)]
  · rw [dvd_iff_isRoot, IsRoot.def] at hq
    simp only [Nat.add_eq_right, rootMultiplicity_eq_zero_iff, IsRoot.def]
    rw [mul_comm, scaleRoots_eval_mul, (hr.pow q.natDegree).mul_left_eq_zero_iff]
    tauto
  · simp
  · rwa [leadingCoeff_pow' (by simp), leadingCoeff_X_sub_C,
      one_pow, one_mul, ne_eq, leadingCoeff_eq_zero]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod

Tactic:
exact ⟨m.map (- ·), by simpa⟩

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod

Tactic:
exact ⟨m.map (- ·), by simpa⟩

Goal state after:
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
x : R
hr : f.roots = {x}
⊢ f = C f.leadingCoeff * (X - C x)

Tactic:
by
  rw [hf.eq_prod_roots, hr]
  simp

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
inst✝ : IsDomain R
hM : M ≤ nonZeroDivisors R
p : S[X]
w✝ : R
hb₁ : w✝ ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = w✝ • p
this✝ : IsDomain S := isDomain_of_le_nonZeroDivisors S hM
this : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr (IsLocalization.injective S hM)
⊢ integerNormalization M p = 0 ↔ p = 0

Tactic:
let : Function.Injective <| mapRingHom (algebraMap R S) := by
    rw [coe_mapRingHom, map_injective_iff]
    exact IsLocalization.injective S hM

Goal state after:
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
inst✝ : IsDomain R
hM : M ≤ nonZeroDivisors R
p : S[X]
w✝ : R
hb₁ : w✝ ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = w✝ • p
this✝¹ : IsDomain S := isDomain_of_le_nonZeroDivisors S hM
this✝ : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr (IsLocalization.injective S hM)
this : Function.Injective ⇑(mapRingHom (algebraMap R S)) :=
  Eq.mpr (id (congrArg (fun _a ↦ Function.Injective _a) (coe_mapRingHom (algebraMap R S))))
    (Eq.mpr (id (congrArg (fun _a ↦ _a) (propext (map_injective_iff (algebraMap R S)))))
      (IsLocalization.injective S hM))
⊢ integerNormalization M p = 0 ↔ p = 0
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 = (Multiset.map (fun x ↦ X - C x) g.roots).prod
| (Multiset.map (fun x ↦ eval x g) s).prod

Tactic:
rw [this]

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 = (Multiset.map (fun x ↦ X - C x) g.roots).prod
| (Multiset.map (fun x ↦ eval x (Multiset.map (fun x ↦ X - C x) g.roots).prod) s).prod
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ (Ideal.Quotient.mkₐ S I) g' = ∑ i ∈ Finset.range (g'.natDegree + 1), g'.coeff i • (Ideal.Quotient.mkₐ S I) X ^ i

Tactic:
as_sum_range_C_mul_X_pow g',

Goal state after:
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ (Ideal.Quotient.mkₐ S I) (∑ i ∈ Finset.range (g'.natDegree + 1), C (g'.coeff i) * X ^ i) =
    ∑ i ∈ Finset.range (g'.natDegree + 1), g'.coeff i • (Ideal.Quotient.mkₐ S I) X ^ i
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
this : f = (f.comp (C a * X + C b)).comp (C a⁻¹ * (X - C b))
⊢ f.Splits

Tactic:
rw [this]

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
this : f = (f.comp (C a * X + C b)).comp (C a⁻¹ * (X - C b))
⊢ ((f.comp (C a * X + C b)).comp (C a⁻¹ * (X - C b))).Splits
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n - 1 + 1) ∈
    Set.range ⇑(algebraMap R Rₘ)

Tactic:
pow_add,

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ p.coeff n *
      ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n - 1) *
        (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ 1) ∈
    Set.range ⇑(algebraMap R Rₘ)
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
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
hm : m.IsMaximal
rid : m • ⊤ = ⊤
⊢ False

Tactic:
have : Nontrivial ((R ⧸ m) ⊗[R] M) :=
    (congr (ULift.moduleEquiv : ULift (R ⧸ m) ≃ₗ[R] R ⧸ m)
      (LinearEquiv.refl R M)).symm.toEquiv.nontrivial

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
hm : m.IsMaximal
rid : m • ⊤ = ⊤
this : Nontrivial ((R ⧸ m) ⊗[R] M)
⊢ False
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: K : Type u_1
A : Type u_4
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
r : A
f : K[X]
h : IsAlgebraic K r
⊢ IsAlgebraic K ((aeval r) f)

Tactic:
rw [isAlgebraic_iff_isIntegral] at h ⊢

Goal state after:
K : Type u_1
A : Type u_4
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
r : A
f : K[X]
h : IsIntegral K r
⊢ IsIntegral K ((aeval r) f)
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
⊢ Function.Injective ⇑(LinearMap.lTensor M LinearMap.id)

Tactic:
apply Module.Flat.lTensor_preserves_injective_linearMap

Goal state after:
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
⊢ Function.Injective ⇑LinearMap.id
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
⊢ f.SurjectiveOnStalks ↔
    ∀ (I : Ideal S) (x : I.IsMaximal), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯)

Tactic:
refine ⟨fun H I hI ↦ H I hI.isPrime, fun H I hI ↦ ?_⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
H : ∀ (I : Ideal S) (x : I.IsMaximal), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯)
I : Ideal S
hI : I.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯)
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
⊢ ∃ a, f a = x

Tactic:
obtain ⟨y, r, c, hc, hr, e⟩ :=
    (surjective_localRingHom_iff _).mp (H (IsLocalRing.maximalIdeal _) inferInstance) x

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
hc : c ∉ IsLocalRing.maximalIdeal S
hr : f r ∉ IsLocalRing.maximalIdeal S
e : c * f r * x = c * f y
⊢ ∃ a, f a = x
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
⊢ Function.Surjective (sigmaToPi R)

Tactic:
intro q

Goal state after:
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
q : PrimeSpectrum ((i : ι) → R i)
⊢ ∃ a, sigmaToPi R a = q
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

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

Tactic:
rw [this]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
this✝ : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ comap f J ≤ K ⊔ comap f ⊥

Tactic:
← Ideal.comap_map_of_surjective f hf

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
this✝ : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ comap f J ≤ comap f (map f K)
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Surjective (comap f)
x : R
hfx : IsUnit (f x)
hx : ¬IsUnit x
⊢ False

Tactic:
obtain ⟨p, hp, _⟩ := exists_max_ideal_of_mem_nonunits hx

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Surjective (comap f)
x : R
hfx : IsUnit (f x)
hx : ¬IsUnit x
p : Ideal R
hp : p.IsMaximal
right✝ : x ∈ p
⊢ False
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i ↦ ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i ↦ ↑i
s : Set ↑b
hs : s.Finite
hU : U = ⋃ i ∈ s, ↑i
this : Finite ↑s
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Tactic:
let _ : Fintype s := Fintype.ofFinite _

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i ↦ ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i ↦ ↑i
s : Set ↑b
hs : s.Finite
hU : U = ⋃ i ∈ s, ↑i
this : Finite ↑s
x✝ : Fintype ↑s := Fintype.ofFinite ↑s
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
Us : Set (Opens X)
hsub : Us ⊆ range U
hUs : W = sSup Us
⊢ ∃ κ a, W = ⨆ k, U (a k)

Tactic:
choose a ha using hsub

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
Us : Set (Opens X)
hUs : W = sSup Us
a : ⦃a : Opens X⦄ → a ∈ Us → ι
ha : ∀ ⦃a_1 : Opens X⦄ (a_2 : a_1 ∈ Us), U (a a_2) = a_1
⊢ ∃ κ a, W = ⨆ k, U (a k)
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
S : Finset (Closeds α)
hS : ∀ t ∈ ↑S, IsIrreducible ↑t
⊢ ↑(sSup ↑S) = ⋃₀ (SetLike.coe '' ↑S)

Tactic:
simp [← Finset.sup_id_eq_sSup, Closeds.coe_finset_sup]

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_2
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
s : Finset ι
⊢ s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t

Tactic:
induction s using Finset.induction_on

Goal state after:
case empty
P : Type u_2
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
⊢ ∅.sup f ∈ t ↔ ∀ i ∈ ∅, f i ∈ t

case insert
P : Type u_2
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : s✝.sup f ∈ t ↔ ∀ i ∈ s✝, f i ∈ t
⊢ (insert a✝² s✝).sup f ∈ t ↔ ∀ i ∈ insert a✝² s✝, f i ∈ t
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤
    match Encodable.decode n with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)

Tactic:
cases (Encodable.decode n : Option ι)

Goal state after:
case none
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤
    match none with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)

case some
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
val✝ : ι
⊢ sequenceOfCofinals p 𝒟 n ≤
    match some val✝ with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)
Module: Mathlib.Order.Ideal

Goal state before:
pp: case some
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
val✝ : ι
⊢ sequenceOfCofinals p 𝒟 n ≤
    match some val✝ with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)

Tactic:
apply Cofinal.le_above

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
s : Finset ι
⊢ ↑(s.sup f) = ⋃ i ∈ s, ↑(f i)

Tactic:
induction s using Finset.induction_on

Goal state after:
case empty
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
⊢ ↑(∅.sup f) = ⋃ i ∈ ∅, ↑(f i)

case insert
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : ↑(s✝.sup f) = ⋃ i ∈ s✝, ↑(f i)
⊢ ↑((insert a✝² s✝).sup f) = ⋃ i ∈ insert a✝² s✝, ↑(f i)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝] U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst✝] V
htV : IsConstructible (V ↓∩ t)
this : (U ∩ V) ↓∩ (s ∪ t) = inclusion ⋯ ⁻¹' U ↓∩ s ∪ inclusion ⋯ ⁻¹' V ↓∩ t
⊢ IsConstructible ((U ∩ V) ↓∩ (s ∪ t))

Tactic:
rw [this]

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝] U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst✝] V
htV : IsConstructible (V ↓∩ t)
this : (U ∩ V) ↓∩ (s ∪ t) = inclusion ⋯ ⁻¹' U ↓∩ s ∪ inclusion ⋯ ⁻¹' V ↓∩ t
⊢ IsConstructible (inclusion ⋯ ⁻¹' U ↓∩ s ∪ inclusion ⋯ ⁻¹' V ↓∩ t)
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
this :
  AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D)) =
    (↑(Algebra.TensorProduct.comm R D C)).comp
      ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑(Algebra.TensorProduct.comm R A D))
⊢ (AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D))).Flat

Tactic:
rw [this]

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
this :
  AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D)) =
    (↑(Algebra.TensorProduct.comm R D C)).comp
      ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑(Algebra.TensorProduct.comm R A D))
⊢ ((↑(Algebra.TensorProduct.comm R D C)).comp
      ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑(Algebra.TensorProduct.comm R A D))).Flat
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑g
hf : (g.comp f).Flat
e : S ≃+* T := RingEquiv.ofBijective g hg
this : f = e.symm.toRingHom.comp (e.toRingHom.comp f)
⊢ f.Flat

Tactic:
rw [this]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑g
hf : (g.comp f).Flat
e : S ≃+* T := RingEquiv.ofBijective g hg
this : f = e.symm.toRingHom.comp (e.toRingHom.comp f)
⊢ (e.symm.toRingHom.comp (e.toRingHom.comp f)).Flat
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : T →+* R
hg : Function.Bijective ⇑g
hf : (f.comp g).Flat
e : T ≃+* R := RingEquiv.ofBijective g hg
this : f = (f.comp e.toRingHom).comp e.symm.toRingHom
⊢ f.Flat

Tactic:
rw [this]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : T →+* R
hg : Function.Bijective ⇑g
hf : (f.comp g).Flat
e : T ≃+* R := RingEquiv.ofBijective g hg
this : f = (f.comp e.toRingHom).comp e.symm.toRingHom
⊢ ((f.comp e.toRingHom).comp e.symm.toRingHom).Flat
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ D (a ^ n.natAbs)⁻¹ = -↑n.natAbs • a ^ (-↑n.natAbs - 1) • D a

Tactic:
leibniz_inv,

Goal state after:
case neg.inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ -(a ^ n.natAbs)⁻¹ ^ 2 • D (a ^ n.natAbs) = -↑n.natAbs • a ^ (-↑n.natAbs - 1) • D a
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ (fun x ↦ ⟨a, ⋯⟩ +ᵥ x)^[minimalPeriod (fun x ↦ a +ᵥ x) b] b = b

Tactic:
exact isPeriodicPt_minimalPeriod (a +ᵥ ·) b

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.hnot
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 ^ k) ^ p ^ t = 1

Tactic:
rwa [hk, mul_comm, ht, pow_succ, ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg

Goal state after: