mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹

Tactic:
by
  by_cases hA : IsUnit A
  · have hD := hAD.mp hA
    cases hA.nonempty_invertible
    cases hD.nonempty_invertible
    let := fromBlocksZero₂₁Invertible A B D
    simp_rw [← invOf_eq_nonsing_inv, invOf_fromBlocks_zero₂₁_eq]
  · have hD := hAD.not.mp hA
    have : ¬IsUnit (fromBlocks A B 0 D) :=
      isUnit_fromBlocks_zero₂₁.not.mpr (not_and'.mpr fun _ => hA)
    simp_rw [nonsing_inv_eq_ringInverse, Ring.inverse_non_unit _ hA, Ring.inverse_non_unit _ hD,
      Ring.inverse_non_unit _ this, Matrix.zero_mul, neg_zero, fromBlocks_zero]

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
r : R
⊢ Represents b ((Algebra.algebraMap R (Matrix ι ι R)) r) ((Algebra.algebraMap R (Module.End R M)) r)

Tactic:
by
  simpa only [Algebra.algebraMap_eq_smul_one] using Matrix.Represents.one.smul r

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : R[X]
⊢ IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)

Tactic:
suffices P = C (eval 0 P) + X * (P /ₘ X) by
    conv_lhs => rw [this]; simp
  conv_lhs => rw [← modByMonic_add_div P X]
  simp [modByMonic_X]

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 : Submodule R M
hp : ¬p.FG
⊢ p.spanRank = 0 ∨ ℵ₀ ≤ p.spanRank

Tactic:
right

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
hp : ¬p.FG
⊢ ℵ₀ ≤ p.spanRank
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h✝ : IsEmpty n
⊢ M.trace = -M.charpoly.nextCoeff

Tactic:
simp [nextCoeff]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
N : Submodule S M
⊢ N.spanRank ≤ (restrictScalars R N).spanRank

Tactic:
by
  obtain ⟨s, hs, e⟩ := (N.restrictScalars R).exists_span_set_card_eq_spanRank
  obtain rfl : span S s = N :=
    le_antisymm (span_le.mpr (span_le.mp e.le :)) (e.ge.trans (span_le_restrictScalars R S s))
  grw [← hs, spanRank_span_le_card]

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
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : i ∉ range 3
⊢ M.charpoly.coeff i = (X ^ 2 - C M.trace * X + C M.det).coeff i

Tactic:
· rw [Finset.mem_range, not_lt, Nat.succ_le_iff] at hi
    suffices M.charpoly.coeff i = 0 by
      simpa [show i ≠ 2 by lia, show 1 ≠ i by lia, show i ≠ 0 by lia, coeff_X, coeff_C]
    apply coeff_eq_zero_of_natDegree_lt
    simpa [charpoly_natDegree_eq_dim, hn] using hi

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
a✝ : Nontrivial R
⊢ M.charpoly.reverse = M.charpolyRev

Tactic:
let t : R[T;T⁻¹] := T 1

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
⊢ M.charpoly.reverse = M.charpolyRev
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ n + k ∉ f.support → ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0

Tactic:
intro h
    simp only [notMem_support_iff.mp h, monomial_zero_right, mul_zero, coeff_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (if p.natDegree ≤ n then p.coeff n else 0) = if n = p.natDegree then p.leadingCoeff else 0

Tactic:
split_ifs with h₁ h₂ h₂

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : p.natDegree ≤ n
h₂ : n = p.natDegree
⊢ p.coeff n = p.leadingCoeff

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : p.natDegree ≤ n
h₂ : ¬n = p.natDegree
⊢ p.coeff n = 0

case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : ¬p.natDegree ≤ n
h₂ : n = p.natDegree
⊢ 0 = p.leadingCoeff

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : ¬p.natDegree ≤ n
h₂ : ¬n = p.natDegree
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
hmg : mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)
⊢ ∃ m, C a * (Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)).prod = C a * (Multiset.map (fun x ↦ X + C x) m).prod

pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
hmg : mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)
⊢ (Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)).prod.Monic

Tactic:
· use mg.map j

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
hmg : mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)
⊢ (Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)).prod.Monic
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
hmg : mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)
⊢ (Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)).prod.Monic

Tactic:
rw [hmg]
      apply monic_multiset_prod_of_monic
      simp [monic_X_add_C]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
A : Subalgebra R S
int : IsIntegral R x
inv_mem : x⁻¹ ∈ A
⊢ x⁻¹⁻¹ ∈ A

Tactic:
exact int.inv.inv_mem inv_mem

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

Goal state before:
pp: case mpr
R : Type u_1
A : Type u_2
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : A ≃ₐ[R] S
y : S
⊢ y ∈ integralClosure R S → ∃ x ∈ integralClosure R A, ↑f x = y

Tactic:
intro hy
    use f.symm y, hy.map (f.symm : S →ₐ[R] A)
    simp

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

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

Tactic:
rw [← Multiset.map_swap_product, Multiset.map_map]

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
⊢ (Multiset.map ((fun ij ↦ ij.1 - ij.2) ∘ Prod.swap) (s ×ˢ g.roots)).prod =
    (Multiset.map (fun ij ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)).prod
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
hf : f.Splits
hf0 : f ≠ 0
i : R →+* S
x : S
hx : ∃ a ∈ f.roots, i a = x
⊢ x ∈ i.range

Tactic:
obtain ⟨x, -, hx⟩ := hx

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
hf : f.Splits
hf0 : f ≠ 0
i : R →+* S
x✝ : S
x : R
hx : i x = x✝
⊢ x✝ ∈ i.range
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
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
⊢ mk' A ((algebraMap S B) 1) ⋯ = 1

Tactic:
simp only [map_one, mk'_one]

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, ?_⟩

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
⊢ (f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1) → f.Splits
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case neg
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)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

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)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
· rw [injective_iff_map_eq_zero] at inj; push Not at inj
    have ⟨r, eq, ne⟩ := inj
    exact ⟨r, ne, by simpa [← algebraMap_smul A, eq, zero_smul] using isIntegral_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)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)
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
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
⊢ False

Tactic:
let E : Submodule R N3 := Submodule.span R {l23 (l12 n1)}

Goal state after:
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
⊢ False
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
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
x : ↥E ⊗[R] M
⊢ x = 0

Tactic:
have mem : x ∈ (⊤ : Submodule R _) := ⟨⟩

Goal state after:
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
x : ↥E ⊗[R] M
mem : x ∈ ⊤
⊢ x = 0
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.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M LinearMap.id)

Tactic:
by
      rw [LinearMap.exact_iff, hf, LinearMap.range_zero, LinearMap.ker_eq_bot]
      apply Module.Flat.lTensor_preserves_injective_linearMap
      exact fun _ _ h => h

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : R
t : ↥(Ideal.comap f P).primeCompl
ha : (algebraMap S (Localization.AtPrime P)) (↑1 * f a) = (algebraMap S (Localization.AtPrime P)) (↑⟨f ↑t, ⋯⟩ * y)
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x

Tactic:
Submonoid.coe_one,

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : R
t : ↥(Ideal.comap f P).primeCompl
ha : (algebraMap S (Localization.AtPrime P)) (1 * f a) = (algebraMap S (Localization.AtPrime P)) (↑⟨f ↑t, ⋯⟩ * y)
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x
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
⊢ RightInverse
    (fun x ↦
      match x with
      | ⟨{ asIdeal := p, isPrime := isPrime }, hp⟩ => { asIdeal := map f p, isPrime := ⋯ })
    fun p ↦ ⟨PrimeSpectrum.comap f p, ⋯⟩

Tactic:
intro ⟨⟨p, _⟩, hp⟩

Goal state after:
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
p : Ideal R
isPrime✝ : p.IsPrime
hp : { asIdeal := p, isPrime := isPrime✝ } ∈ zeroLocus ↑I
⊢ (fun p ↦ ⟨PrimeSpectrum.comap f p, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨{ asIdeal := p, isPrime := isPrime }, hp⟩ => { asIdeal := map f p, isPrime := ⋯ })
        ⟨{ asIdeal := p, isPrime := isPrime✝ }, hp⟩) =
    ⟨{ asIdeal := p, isPrime := isPrime✝ }, hp⟩
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
r : R
I : MaximalSpectrum S
⊢ IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) ⟨f ↑1, ⋯⟩ =
    IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) 1

Tactic:
Submonoid.coe_one,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
r : R
I : MaximalSpectrum S
⊢ IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) ⟨f 1, ⋯⟩ =
    IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) 1
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
⊢ IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) ⟨f ↑1, ⋯⟩ =
    IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) 1

Tactic:
Submonoid.coe_one,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
⊢ IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) ⟨f 1, ⋯⟩ =
    IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) 1
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
t : Set Y
ht : IsLocallyClosed t
hs : IsLocallyClosed (f ⁻¹' t)
⊢ IsLocallyClosed (t ∩ range f)

Tactic:
exact ht.inter hf'

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
⊢ U.carrier ⊆ ⋃ i, ↑↑i

Tactic:
simp [hsup]

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

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

Tactic:
rw [NoetherianSpace, CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact,
    CompleteLattice.isSupFiniteCompact_iff_all_elements_compact]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ (∀ (k : Opens α), IsCompactElement k) ↔ ∀ (s : Opens α), IsCompact ↑s
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
H : ∀ y < ⊥, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ ⊥ = sSup S

pp: case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
· use ∅; simp

Goal state after:
case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: 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)

Tactic:
· exact QuasiSeparatedSpace.isCompact_sInter_of_nonempty hf hne ho hc

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
S : Set α
hS : IsIrreducible S
hS' : IsClosed S
⊢ S = closure S

Tactic:
exact hS'.closure_eq.symm

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
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst✝¹] U
⊢ IsCompact (f ⁻¹' s ∩ U)

Tactic:
rw [hf.isCompact_iff, image_preimage_inter]

Goal state after:
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
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst✝¹] U
⊢ IsCompact (s ∩ f '' U)
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : (ulift.{u₁, u₂, u_1, u_2} f).Flat
⊢ ((ulift.{u₁, u₂, u_1, u_2} f).comp ULift.ringEquiv.symm.toRingHom).Flat

Tactic:
comp_iff_of_bijective_right (Equiv.bijective _)

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : (ulift.{u₁, u₂, u_1, u_2} f).Flat
⊢ (ulift.{u₁, u₂, u_1, u_2} f).Flat
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case e_g
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
⊢ ((if b.factorization p ≤ a.factorization p then p ^ n else 1) *
      if b.factorization p ≤ a.factorization p then 1 else p ^ n) =
    p ^ n

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ p ^ (a.lcm b).factorization p ∣ p ^ a.factorization p

Tactic:
rw [factorization_lcm ha hb]

Goal state after:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ p ^ (a.factorization ⊔ b.factorization) p ∣ p ^ a.factorization p
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : a.factorization p ≠ 0
⊢ (a.lcm b).factorization p ≠ 0

Tactic:
rw [factorization_lcm ha hb]

Goal state after:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : a.factorization p ≠ 0
⊢ (a.factorization ⊔ b.factorization) p ≠ 0
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ p ^ (a.lcm b).factorization p ∣ p ^ b.factorization p

Tactic:
rw [factorization_lcm ha hb]

Goal state after:
case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ p ^ (a.factorization ⊔ b.factorization) p ∣ p ^ b.factorization p
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : b.factorization p ≠ 0
⊢ (a.lcm b).factorization p ≠ 0

Tactic:
rw [factorization_lcm ha hb]

Goal state after:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : b.factorization p ≠ 0
⊢ (a.factorization ⊔ b.factorization) p ≠ 0
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring A
inst✝¹⁴ : CommSemiring B
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra R A
inst✝¹¹ : Algebra R B
inst✝¹⁰ : Module A M
inst✝⁹ : Module B M
inst✝⁸ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
S : Type u_5
T : Type u_6
inst✝⁷ : Monoid S
inst✝⁶ : DistribMulAction S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : SMulCommClass S A M
inst✝³ : Monoid T
inst✝² : DistribMulAction T M
inst✝¹ : SMulCommClass R T M
inst✝ : SMulCommClass T A M
r : S
D : Derivation R A M
⊢ r • ↑D 1 = 0

Tactic:
coeFn_coe,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring A
inst✝¹⁴ : CommSemiring B
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra R A
inst✝¹¹ : Algebra R B
inst✝¹⁰ : Module A M
inst✝⁹ : Module B M
inst✝⁸ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
S : Type u_5
T : Type u_6
inst✝⁷ : Monoid S
inst✝⁶ : DistribMulAction S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : SMulCommClass S A M
inst✝³ : Monoid T
inst✝² : DistribMulAction T M
inst✝¹ : SMulCommClass R T M
inst✝ : SMulCommClass T A M
r : S
D : Derivation R A M
⊢ r • D 1 = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Set.range (comap (RingHom.snd R S)) = zeroLocus ↑(RingHom.ker (RingHom.snd R S))

Tactic:
by
  refine Set.ext fun p ↦ ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨I, hI, rfl⟩; exact Ideal.comap_mono bot_le
  obtain ⟨p, hp, eq⟩ | ⟨p, hp, eq⟩ := p.1.ideal_prod_prime.mp p.2
  · refine (hp.ne_top <| (Ideal.eq_top_iff_one _).mpr ?_).elim
    simpa [eq] using h (show (1, 0) ∈ RingHom.ker (RingHom.snd R S) by simp)
  · exact ⟨⟨p, hp⟩, PrimeSpectrum.ext <| by simpa [Ideal.prod] using eq.symm⟩

Goal state after: