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

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A

Tactic:
by
  have : A * (A.adjugate * A.adjugate.adjugate) =
      A * (A.det ^ (Fintype.card n - 1) • (1 : Matrix n n α)) := by
    rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]
  rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul,
    Matrix.one_mul] at this

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
⊢ A'.det • A'.adjugate.adjugate = A'.det • A'.det ^ (Fintype.card n - 2) • A'

Tactic:
smul_smul,

Goal state after:
case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
⊢ A'.det • A'.adjugate.adjugate = (A'.det * A'.det ^ (Fintype.card n - 2)) • A'
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ Function.Injective ⇑A.vecMulLinear ↔ Function.Injective fun v ↦ v ᵥ* A

Tactic:
coe_vecMulLinear

Goal state after:
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ (Function.Injective fun v ↦ v ᵥ* A) ↔ Function.Injective fun v ↦ v ᵥ* A
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ ↑h.unit⁻¹ • A.det • 1 = 1

Tactic:
smul_smul,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ (↑h.unit⁻¹ * A.det) • 1 = 1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • B.adjugate * A.det⁻¹ʳ • A.adjugate

Tactic:
Matrix.smul_mul,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • (B.adjugate * A.det⁻¹ʳ • A.adjugate)
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • A.det⁻¹ʳ • (B.adjugate * A.adjugate)

Tactic:
smul_smul,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (A * B).det⁻¹ʳ • (A * B).adjugate = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
⊢ (A.det • ↑h.unit⁻¹ • A.adjugate) *ᵥ b = A.adjugate *ᵥ b

Tactic:
smul_smul,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
⊢ ((A.det * ↑h.unit⁻¹) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ (matPolyEquiv (single i j p)).coeff k = single i j (p.coeff k)

Tactic:
by
  refine Polynomial.induction_on' p ?_ ?_
  · intro p q hp hq
    ext
    simp [hp, hq, coeff_add, Matrix.add_apply, single_add]
  · intro k x
    simp only [matPolyEquiv_coeff_apply_aux_1, coeff_monomial]
    split_ifs <;>
      · funext
        simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
μ : R
σ : Equiv.Perm n
a✝¹ : σ ∈ univ
i : n
a✝ : i ∈ univ
hi : σ i = i
⊢ (M - (scalar n) μ).charmatrix (σ i) i = (M.charmatrix (σ i) i).comp (X + C μ)

Tactic:
simp [hi]

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
μ : R
σ : Equiv.Perm n
a✝¹ : σ ∈ univ
i : n
a✝ : i ∈ univ
hi : σ i = i
⊢ X - (C (M i i) - C μ) = X + C μ - C (M i i)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
μ : R
σ : Equiv.Perm n
a✝¹ : σ ∈ univ
i : n
a✝ : i ∈ univ
hi : ¬σ i = i
⊢ (M - (scalar n) μ).charmatrix (σ i) i = (M.charmatrix (σ i) i).comp (X + C μ)

Tactic:
simp [hi]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : R[X]
⊢ IsNilpotent P ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)

Tactic:
by
  refine
    ⟨P.recOnHorner (by simp) (fun p r hp₀ _ hp hpr i ↦ ?_) (fun p _ hnp hpX i ↦ ?_), fun h ↦ ?_⟩
  · rw [← sum_monomial_eq P]
    exact isNilpotent_sum (fun i _ ↦ by simpa only [isNilpotent_monomial_iff] using h i)
  · have hr : IsNilpotent (C r) := by
      obtain ⟨k, hk⟩ := hpr
      replace hp : eval 0 p = 0 := by rwa [coeff_zero_eq_aeval_zero] at hp₀
      refine isNilpotent_C_iff.mpr ⟨k, ?_⟩
      simpa [coeff_zero_eq_aeval_zero, hp] using congr_arg (fun q ↦ coeff q 0) hk
    rcases i with - | i
    · simpa [hp₀] using hr
    simp only [coeff_add, coeff_C_succ, add_zero]
    apply hp
    simpa using Commute.isNilpotent_sub (Commute.all _ _) hpr hr
  · rcases i with - | i
    · simp
    simpa using hnp (isNilpotent_mul_X_iff.mp hpX) i

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsNilpotent (f i)) → (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
i : ι
hi : i ∈ s
⊢ i ∈ insert j s

Tactic:
simp [hi]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
j✝ : ι
s : Finset ι
hj✝ : j✝ ∉ s
ih : (∀ i ∈ s, IsNilpotent (f i)) → (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j✝ s, IsNilpotent (f i)
h_comm : ∀ (i j : ι), i ∈ insert j✝ s → j ∈ insert j✝ s → Commute (f i) (f j)
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ i ∈ insert j✝ s

Tactic:
simp [hi]

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 ι
A : Matrix ι ι R
j : ι
⊢ ∑ x, (1 • A.col j) x • b x = ∑ i, A i j • b i

Tactic:
one_smul,

Goal state after:
ι : 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 ι
A : Matrix ι ι R
j : ι
⊢ ∑ x, A.col j x • b x = ∑ i, A i j • b i
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
a : ℕ
⊢ IsIntegral R ↑a

Tactic:
← Int.cast_natCast

Goal state after:
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
a : ℕ
⊢ IsIntegral R ↑↑a
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
k : ℕ
⊢ ⇑(1 • LinearMap.id) = id

Tactic:
one_smul,

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
k : ℕ
⊢ ⇑LinearMap.id = id
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (((k + 1)! • hasseDeriv (k + 1)) f).coeff n = (derivative ((k ! • hasseDeriv k) f)).coeff n

Tactic:
simp only [LinearMap.smul_apply, coeff_smul, LinearMap.map_smul_of_tower, coeff_derivative,
    hasseDeriv_coeff, ← @choose_symm_add _ k]

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1)! • (↑((n + (k + 1)).choose (k + 1)) * f.coeff (n + (k + 1))) =
    k ! • (↑((n + 1 + k).choose (n + 1)) * f.coeff (n + 1 + k) * (↑n + 1))
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 : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
⊢ (∑ s, X ^ #s • D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i)).coeff k =
    ∑ s, (X ^ #s • D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i)).coeff k

Tactic:
simp only [Polynomial.finsetSum_coeff]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : m < x.1
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
simp only [Nat.choose_eq_zero_of_lt hm, Nat.cast_zero, zero_mul,
                 monomial_zero_right]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ p.coeff i * (p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff) = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)

Tactic:
← pow_succ,

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + 1) = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)
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.natDegree ≠ 0
⊢ f.roots ≠ 0

Tactic:
simpa [hf.natDegree_eq_card_roots] using hf0

Goal state after:
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
⊢ ((Ideal.Quotient.mk I).comp (algebraMap S S[X])).IsIntegralElem ((Ideal.Quotient.mk I) X)

Tactic:
exact ⟨g, mon, by
  rw [← (Ideal.Quotient.eq_zero_iff_mem.mpr h), eval₂_eq_sum_range]
  nth_rw 3 [(as_sum_range_C_mul_X_pow g)]
  simp only [map_sum, algebraMap_eq, RingHom.coe_comp, Function.comp_apply, map_mul, map_pow]⟩

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

Goal state before:
pp: case neg.refine_1
R : Type u_5
S : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : (algebraMap R Rₘ) ↑⟨p.leadingCoeff, hM⟩ * b = 1
⊢ (Polynomial.map (algebraMap R Rₘ) p * C b).Monic

Tactic:
refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_
    rwa [leadingCoeff_map_of_leadingCoeff_ne_zero (algebraMap R Rₘ)]
    refine fun hfp => zero_ne_one
      (_root_.trans (zero_mul b).symm (hfp ▸ hb) : (0 : Rₘ) = 1)

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
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ g ∈ S[(Ideal.Quotient.mkₐ S I) X]

Tactic:
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]

Goal state after:
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
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
this : g = (aeval ((Ideal.Quotient.mkₐ S I) X)) g'
⊢ g ∈ S[(Ideal.Quotient.mkₐ S I) X]
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
v' : Rₘ
hv' : v' * (algebraMap R Rₘ) ↑⟨v, ⋯⟩ = 1
⊢ (algebraMap Rₘ Sₘ) v' * (algebraMap S Sₘ) u = 1

pp: case refine_2
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
v' : Rₘ
hv' : v' * (algebraMap R Rₘ) ↑⟨v, ⋯⟩ = 1
⊢ IsIntegral Rₘ (x * (algebraMap S Sₘ) u)

Tactic:
· replace hv' := congr_arg (@algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S)) hv'
    rw [map_mul, map_one, localizationAlgebraMap_def, IsLocalization.map_eq] at hv'
    exact hv.2 ▸ hv'

Goal state after:
case refine_2
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
v' : Rₘ
hv' : v' * (algebraMap R Rₘ) ↑⟨v, ⋯⟩ = 1
⊢ IsIntegral Rₘ (x * (algebraMap S Sₘ) u)
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_3.refine_1
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : p.coeff i ≠ 0
mem : p.coeff i ∈ comap f I
⊢ (p * X).coeff (i + 1) ≠ 0

Tactic:
simp [hi]

Goal state after:
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
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : Subsingleton (N ⊗[R] M)
⊢ Subsingleton N

Tactic:
by
  revert h; change _ → _; contrapose!
  intro h
  infer_instance

Goal state after:
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 : Transcendental K ((aeval r) f)
⊢ Transcendental K r

Tactic:
rw [Transcendental] 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 : ¬IsAlgebraic K ((aeval r) f)
⊢ ¬IsAlgebraic K r
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst✝ : Away r Sₘ
x : S
hx : IsIntegral R ((algebraMap S Sₘ) x)
⊢ ∃ n, IsIntegral R (r ^ n * x)

Tactic:
by
  nontriviality S
  obtain ⟨p, hpm, hp⟩ := hx
  simp only [IsScalarTower.algebraMap_eq R S Sₘ, ← hom_eval₂,
    IsLocalization.map_eq_zero_iff (.powers r), Subtype.exists, Submonoid.mem_powers_iff,
    exists_prop, exists_exists_eq_and] at hp
  obtain ⟨m, hm⟩ := hp
  have := isIntegral_trans (R := R) _ (isIntegral_leadingCoeff_smul (R := integralClosure R S)
    (C ⟨r, hr⟩ ^ m * p.map (algebraMap _ _)) x (by simpa [← aeval_def] using hm))
  rw [← map_pow, (hpm.map _).leadingCoeff_C_mul] at this
  exact ⟨m, this⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsMin x ↔ x.asIdeal ∈ minimalPrimes R

Tactic:
change IsMin _ ↔ Minimal (fun q : Ideal R ↦ q.IsPrime ∧ ⊥ ≤ q) _

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsMin x ↔ Minimal (fun q ↦ q.IsPrime ∧ ⊥ ≤ q) x.asIdeal
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : FaithfulSMul R S
this : FaithfulSMul R T
⊢ finrank R S * finrank S T = finrank R T

Tactic:
have : IsDomain R := (FaithfulSMul.algebraMap_injective R T).isDomain

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : FaithfulSMul R S
this✝ : FaithfulSMul R T
this : IsDomain R
⊢ finrank R S * finrank S T = finrank R T
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case mp
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
h : 1 ⊗ₜ[R] m = 0
f : R →ₗ[R] M := ⋯
a : A
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor A f)) a) 1 = ((AlgebraTensorModule.curry 0) a) 1

Tactic:
apply_fun (a • ·) at h

Goal state after:
case mp
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
f : R →ₗ[R] M := (LinearMap.lsmul R M).flip m
a : A
h : a • 1 ⊗ₜ[R] m = a • 0
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor A f)) a) 1 = ((AlgebraTensorModule.curry 0) a) 1
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case inr
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨j, q⟩
ne : i ≠ j
⊢ ⟨i, p⟩ = ⟨j, q⟩

Tactic:
refine (p.1.ne_top_iff_one.mp p.2.ne_top ?_).elim
    have : Function.update (1 : ∀ i, R i) j 0 ∈ (sigmaToPi R ⟨j, q⟩).asIdeal := by simp
    simpa [← eq, Function.update_of_ne ne]

Goal state after:
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
p : Ideal R
hp : p.IsMaximal
right✝ : x ∈ p
q : Ideal S
hqp : q.IsPrime
hq : Ideal.comap f q = p
⊢ x ∈ Ideal.comap f q

Tactic:
by rwa [hq]

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
⊢ IsOpenCover fun V ↦ (↑V).1

Tactic:
by
  refine top_le_iff.mp fun x _ ↦ ?_
  obtain ⟨i, hxi⟩ := hU.exists_mem x
  obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := hS.exists_subset_of_mem_open hxi (U i).2
  simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.mem_mk, Set.mem_iUnion, SetLike.mem_coe]
  exact ⟨⟨(V, i), hV, hVU⟩, hxV⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U : Opens α
x : α
⊢ x ∈ Uᶜ ↔ ∃ V, Disjoint V U ∧ x ∈ V

Tactic:
by
  simp [compl_eq_sSup_disjoint]

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a \ b ∈ L

Tactic:
by
  rw [_root_.sdiff_eq]; exact L.infClosed ha (compl_mem hb)

Goal state after:
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
hW : IsCompact W.carrier
κ : Type u
a : κ → ι
heq : W = ⨆ k, U (a k)
⊢ W.carrier ⊆ ⋃ i, (U (a i)).carrier

Tactic:
by simp [heq]

Goal state after:
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
hW : IsCompact W.carrier
⊢ ∃ κ, ∃ (_ : Finite κ), ∃ a, W = ⨆ k, U (a k)

Tactic:
by
  obtain ⟨κ, a, heq⟩ := hU.exists_iSup_eq W
  obtain ⟨s, hs⟩ := hW.elim_finite_subcover _ (fun k : κ ↦ (U (a k)).2) (by simp [heq])
  use s, s.finite_toSet, a ∘ Subtype.val
  refine le_antisymm ?_ ?_
  · simpa [← SetLike.coe_subset_coe, Set.iUnion_subtype]
  · rw [heq, iSup_le_iff]
    intro i
    exact le_iSup_of_le _ le_rfl

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT (Closeds α)
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Tactic:
tfae_have 1 ↔ 4 := noetherianSpace_iff_opens α

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
⊢ ∀ t ⊆ ⋃ i, f i, IsCompact t

Tactic:
intro t ht

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
t : Set α
ht : t ⊆ ⋃ i, f i
⊢ IsCompact t
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Closeds α
hs : IsAtom s
⊢ ∃ a, ↑s = {a}

Tactic:
by
  refine minimal_nonempty_closed_eq_singleton s.2 (coe_nonempty.2 hs.1) fun t hts ht ht' ↦ ?_
  lift t to Closeds α using ht'
  exact SetLike.coe_injective.eq_iff.2 <| (hs.le_iff_eq <| coe_nonempty.1 ht).1 hts

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

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

Tactic:
induction s using Finset.induction_on with

Goal state after: