mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Set M
⊢ ⨅ s_1, #↑↑s_1 ≤ #↑s

Tactic:
let s' : {s1 : Set M // span R s1 = span R s} := ⟨s, rfl⟩

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s' : { s1 // span R s1 = span R s } := ⟨s, ⋯⟩
⊢ ⨅ s_1, #↑↑s_1 ≤ #↑s
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
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ ∑ i, (M.charmatrix (c i) i).natDegree ≤ ∑ a, if c a = a then 1 else 0

Tactic:
apply sum_le_sum

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ ∀ i ∈ univ, (M.charmatrix (c i) i).natDegree ≤ if c i = i then 1 else 0
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
⊢ ⨆ ι, #↑↑ι ≤ ⊤.spanRank

Tactic:
Submodule.spanRank

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
⊢ ⨆ ι, #↑↑ι ≤ ⨅ s, #↑↑s
Module: Mathlib.Algebra.Polynomial.Eval.Subring

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ (mapRingHom f).rangeS → ∀ (n : ℕ), p.coeff n ∈ f.rangeS

Tactic:
rintro ⟨p, rfl⟩ n
    rw [coe_mapRingHom, coeff_map]
    exact Set.mem_range_self _

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k) (g k)
hq : map f q = p
⊢ q.support = p.support

Tactic:
Finset.ext_iff,

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k) (g k)
hq : map f q = p
⊢ ∀ (a : ℕ), a ∈ q.support ↔ a ∈ p.support
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n : ℕ
⊢ (lcoeff R n ∘ₗ taylor r) f = (leval r ∘ₗ hasseDeriv n) f

Tactic:
congr 1; clear! f; ext i
    simp only [leval_apply, mul_one, one_mul, eval_monomial, LinearMap.comp_apply, map_sum,
      hasseDeriv_monomial, taylor_apply, monomial_comp, C_1, (commute_X (C r)).add_pow i]
    simp only [lcoeff_apply, ← C_eq_natCast, mul_assoc, ← C_pow, ← C_mul, coeff_mul_C,
      (Nat.cast_commute _ _).eq, coeff_X_pow, boole_mul, Finset.sum_ite_eq, Finset.mem_range]
    split_ifs with h; · rfl
    push Not at h; rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]

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
⊢ (f * X).Splits ↔ f.Splits

Tactic:
simp [mul_comm f]

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

Goal state before:
pp: case mpr
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
⊢ g ∈ ⊤ → g ∈ S[(Ideal.Quotient.mkₐ S I) X]

Tactic:
· intro _
      obtain ⟨g', hg⟩ := Ideal.Quotient.mkₐ_surjective S I g
      have : g = (Polynomial.aeval ((Ideal.Quotient.mkₐ S I) X)) g' := by
        nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _),
          as_sum_range_C_mul_X_pow g', map_sum]
        simp only [Polynomial.C_mul', ← map_pow, map_smul]
      exact this ▸ (aeval_mem_adjoin_singleton S ((Ideal.Quotient.mk I) Polynomial.X))

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : IsIntegralClosure A R B
A' : Type u_4
inst✝⁶ : CommRing A'
inst✝⁵ : Algebra A' B
inst✝⁴ : IsIntegralClosure A' R B
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R A' B
⊢ (lift R A' B).comp (lift R A B) = AlgHom.id R A'

Tactic:
ext x; apply algebraMap_injective A' R B; simp

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

Goal state before:
pp: 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
⊢ p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff)) ∈ lifts (algebraMap R Rₘ)

Tactic:
by
  rw [Polynomial.lifts_iff_coeff_lifts]
  intro n
  rw [Polynomial.coeff_scaleRoots]
  by_cases h₁ : n ∈ p.support
  on_goal 1 => by_cases h₂ : n = p.natDegree
  · rwa [h₂, Polynomial.coeff_natDegree, tsub_self, pow_zero, _root_.mul_one]
  · have : n + 1 ≤ p.natDegree := lt_of_le_of_ne (Polynomial.le_natDegree_of_mem_supp _ h₁) h₂
    rw [← tsub_add_cancel_of_le (le_tsub_of_add_le_left this), pow_add, pow_one, mul_comm,
      _root_.mul_assoc, ← map_pow]
    change _ ∈ (algebraMap R Rₘ).range
    apply mul_mem
    · exact RingHom.mem_range_self _ _
    · rw [← Algebra.smul_def]
      exact ⟨_, IsLocalization.map_integerMultiple M p.support p.coeff ⟨n, h₁⟩⟩
  · rw [Polynomial.notMem_support_iff] at h₁
    rw [h₁, zero_mul]
    exact zero_mem (algebraMap R Rₘ).range

Goal state after:
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.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p.coeff p.support, IsIntegral R (r • z)
n : ℕ
hn : n ∈ (r • p).support
hs : (r • p).coeff n ∈ ↑(r • p).coeffs
⊢ (r • p).coeff n ∈ ↑(integralClosure R S).toSubring

Tactic:
exact int _ (Finset.mem_image_of_mem _ <| support_smul _ _ hn)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus s = Set.univ ↔ s ⊆ ↑(nilradical R)

Tactic:
← Set.univ_subset_iff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ Set.univ ⊆ zeroLocus s ↔ s ⊆ ↑(nilradical R)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

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

Tactic:
rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : (algebraMap R S) z * y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩

Tactic:
mul_comm _ y,

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : (algebraMap R S) z * y' = y * ↑z'
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : y' * (algebraMap R S) z = y * ↑z'
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ ↑z' * y = ↑⟨(algebraMap R S) z, hz0'⟩ * y'

Tactic:
mul_comm _ y,

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : y' * (algebraMap R S) z = y * ↑z'
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ y * ↑z' = ↑⟨(algebraMap R S) z, hz0'⟩ * y'
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

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

Tactic:
rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]

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

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
x✝ : { asIdeal := I, isPrime := ⋯ } ∈ Set.range (sigmaToPi R)
i : ι
p : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = { asIdeal := I, isPrime := ⋯ }
⊢ ⇑(DFinsupp.single i 1) ∉ (sigmaToPi R ⟨i, p⟩).asIdeal

Tactic:
simpa using p.1.ne_top_iff_one.mp p.2.ne_top

Goal state after:
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 ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
j : ι
⊢ (∏ i, e i) j = 0 j

Tactic:
rw [Finset.prod_apply, Pi.zero_apply, Finset.prod_eq_zero (Finset.mem_univ j)]

Goal state after:
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
j : ι
⊢ e j j = 0
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
add_sub_cancel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ 1 - ↑a * (1 - ↑a) = ↑⊤
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ ∀ ⦃a : R⦄, a ∈ p → ∃ x, ¬x = 0 ∧ x * a = 0

Tactic:
← mul_comm

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ ∀ ⦃a : R⦄, a ∈ p → ∃ x, ¬x = 0 ∧ a * x = 0
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I p : Ideal S
h : p ∈ I.minimalPrimes
H : comap f p ∈ (comap f I).minimalPrimes
⊢ comap f p ∈ comap f '' I.minimalPrimes

Tactic:
exact ⟨p, h, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
⊢ p ∈ Ideal.under R ⁻¹' J.minimalPrimes

Tactic:
refine ⟨⟨Ideal.IsPrime.comap _, Ideal.map_le_iff_le_comap.mp hp.le⟩, ?_⟩

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
⊢ ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ J ≤ q) y → y ≤ Ideal.under R p → Ideal.under R p ≤ y
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
⊢ ∀ (a : α), bot ≤ a

Tactic:
intros; simp +instances [eq_le, eq_bot]

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✝] (U ∩ Z ∪ (frontier (U ∩ Z))ᶜ)

Tactic:
inter_union_distrib_right,

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))ᶜ) ∩ (Z ∪ (frontier (U ∩ Z))ᶜ))
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f✝ : BoundedLatticeHom α β
s t : Set α
a✝ b : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra α
a : α
ha : a ∈ ↑L
⊢ (f a)ᶜ ∈ ⇑f '' ↑L

Tactic:
exact ⟨aᶜ, by simpa [map_compl']⟩

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ closure[inst✝] (range f) = univ ↔ ⋃ i, {x | x ∈ U i} ⊆ closure[inst✝] (range f)

Tactic:
← Set.univ_subset_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ univ ⊆ closure[inst✝] (range f) ↔ ⋃ i, {x | x ∈ U i} ⊆ closure[inst✝] (range f)
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
⊢ GeneralizingMap f ↔ ∀ (i : ι), GeneralizingMap (f ∘ Subtype.val)

Tactic:
refine ⟨fun hf i ↦ ((U i).isOpenEmbedding'.generalizingMap).comp hf, fun hf ↦ fun x y h ↦ ?_⟩
  obtain ⟨i, hi⟩ := hU.exists_mem x
  replace h : y ⤳ (f ∘ ((↑) : U i → α)) ⟨x, hi⟩ := h
  obtain ⟨a, ha, rfl⟩ := hf i h
  use a.val
  simp [ha.map (U i).isOpenEmbedding'.continuous]

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s : Finset ι
f : ι → Compacts α
⊢ ↑(s.sup f) = s.sup fun i ↦ ↑(f i)

Tactic:
refine Finset.cons_induction_on s rfl fun a s _ h => ?_
  simp_rw [Finset.sup_cons, coe_sup, sup_eq_union]
  congr

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hs : IsRetrocompact s
⊢ IsRetrocompact (f ⁻¹' s)

Tactic:
by
  rintro U hUcomp hUopen
  rw [hf.isCompact_iff, image_preimage_inter]
  exact hs (hUcomp.image hf.continuous) <| hf.isOpenMap _ hUopen

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
this : (RelSeries.head L).asIdeal.LiesOver l.head.asIdeal
Q : Ideal S
Qlt : Q < (RelSeries.head L).asIdeal
hQ : Q.IsPrime
Qlo : Q.LiesOver q.asIdeal
⊢ (RelSeries.cons L { asIdeal := Q, isPrime := hQ } Qlt).length = (l.cons q lt).length ∧
    (RelSeries.cons L { asIdeal := Q, isPrime := hQ } Qlt).last = { asIdeal := P, isPrime := ⋯ } ∧
      List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.cons L { asIdeal := Q, isPrime := hQ } Qlt).toList =
        (l.cons q lt).toList

Tactic:
simp only [RelSeries.cons_length, add_left_inj, RelSeries.last_cons]

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
this : (RelSeries.head L).asIdeal.LiesOver l.head.asIdeal
Q : Ideal S
Qlt : Q < (RelSeries.head L).asIdeal
hQ : Q.IsPrime
Qlo : Q.LiesOver q.asIdeal
⊢ L.length = l.length ∧
    RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
      List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.cons L { asIdeal := Q, isPrime := hQ } Qlt).toList =
        (l.cons q lt).toList
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).Flat
⊢ (algebraMap S (S ⊗[R] T)).Flat

Tactic:
rw [flat_algebraMap_iff] at h ⊢

Goal state after:
R S T : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Flat R T
⊢ Module.Flat S (S ⊗[R] T)
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
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
x : A
⊢ (Ideal.Quotient.mk I) ((algebraMap A B) x) = (algebraMap A (B ⧸ I)) x

Tactic:
Ideal.Quotient.mk_algebraMap

Goal state after:
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
x : A
⊢ (algebraMap A (B ⧸ I)) x = (algebraMap A (B ⧸ I)) x
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : I.radical = J.radical
⊢ zeroLocus ↑I = zeroLocus ↑J

Tactic:
← zeroLocus_radical,

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : I.radical = J.radical
⊢ zeroLocus ↑I.radical = zeroLocus ↑J
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ IsClosed (zeroLocus ↑(ker f))

Tactic:
exact isClosed_zeroLocus _

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr
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
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p

Tactic:
obtain ⟨k, hk : exponent G = p ^ _ * k⟩ := Nat.ordProj_dvd _ _

Goal state after:
case inr
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
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
n₁ : ℕ
heq₁ : Nat.card ↥H₁ = p₁ ^ n₁
⊢ (p₁ ^ n₁).Coprime (Nat.card ↥H₂)

Tactic:
clear heq₁

Goal state after:
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
n₁ : ℕ
⊢ (p₁ ^ n₁).Coprime (Nat.card ↥H₂)
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
⊢ rank ↥(closure ↑s) ≤ s.card

Tactic:
apply (rank_le ht).trans

Goal state after:
G : Type u_1
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := ⋯
ht : closure ↑t = ⊤
⊢ t.card ≤ s.card
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) → vanishingIdeal s ∈ minimalPrimes R

Tactic:
· rw [← vanishingIdeal_irreducibleComponents, ← vanishingIdeal_closure]
    exact Set.mem_image_of_mem _

Goal state after: