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

Goal state before:
pp: case zero
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
⊢ (M.charmatrix (c i) i).coeff 0 ∈ I

Tactic:
charmatrix_apply,

Goal state after:
case zero
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
⊢ (diagonal (fun x ↦ X) (c i) i - C (M (c i) i)).coeff 0 ∈ I
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 = 1 - (X • M.map ⇑C) ^ k

Tactic:
← C.mapMatrix_apply,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 = 1 - (X • C.mapMatrix M) ^ k
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
⊢ f = 0

Tactic:
rw [← taylor_eq_zero r]
  ext k
  rw [taylor_coeff, h, coeff_zero]

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
r : R
f : R →+* S
⊢ map f ((taylor r) p) = (taylor (f r)) (map f p)

Tactic:
simp [taylor_apply, Polynomial.map_comp]

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

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

Tactic:
subst hx

Goal state after:
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 : ℕ × ℕ
⊢ (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))
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
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 : x.1 ≤ m
hn : x.2 ≤ n
⊢ (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:
tsub_add_eq_add_tsub hm,

Goal state after:
case neg
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 : x.1 ≤ m
hn : x.2 ≤ n
⊢ (monomial (m + (n - x.2) - x.1)) (↑(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))
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

Tactic:
rw [eq_C_of_natDegree_eq_zero h, eval₂_C] at hz

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : f (p.coeff 0) = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
H : (p.toSubring T hp).coeff p.natDegree = 1
⊢ ↑((p.toSubring T hp).coeff p.natDegree) = 1

Tactic:
by rw [H, OneMemClass.coe_one]

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

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

Tactic:
exact (Subalgebra.map_injective g.injective).eq_iff

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

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
⊢ eval x (derivative f) / eval x f = (Multiset.map (fun z ↦ 1 / (x - z)) f.roots).sum

Tactic:
by
  rw [hf.eval_derivative_eq_eval_mul_sum hx, mul_div_cancel_left₀ _ hx]

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

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
⊢ f.natDegree - (X - C x).natDegree = 1

Tactic:
h₁,

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
⊢ 2 - (X - C x).natDegree = 1
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg.a
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
⊢ (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) * p.coeff n ∈ (algebraMap R Rₘ).range

Tactic:
← Algebra.smul_def

Goal state after:
case neg.a
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
⊢ ↑(commonDenom M p.support p.coeff) • p.coeff n ∈ (algebraMap R Rₘ).range
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₁ : p.coeff n = 0
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
h₁,

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₁ : p.coeff n = 0
⊢ 0 * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra.IsIntegral R A
inst✝¹ : IsDomain A
inst✝ : Nontrivial R
I : Ideal A
⊢ comap (algebraMap R A) I = ⊥ → I = ⊥

Tactic:
contrapose

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra.IsIntegral R A
inst✝¹ : IsDomain A
inst✝ : Nontrivial R
I : Ideal A
⊢ ¬I = ⊥ → ¬comap (algebraMap R A) I = ⊥
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
⊢ ∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Tactic:
let Sₚ := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
⊢ ∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x✝ : A
h : x✝ ∈ s
⊢ IsIntegral R ((∏ x ∈ s, r x) • x✝)

Tactic:
rw [← Finset.prod_erase_mul _ _ h, mul_smul]

Goal state after:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x✝ : A
h : x✝ ∈ s
⊢ IsIntegral R ((∏ x ∈ s.erase x✝, r x) • r x✝ • x✝)
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)
⊢ l23.ker = l12.range

Tactic:
have complex : LinearMap.range l12 ≤ LinearMap.ker l23 := range_le_ker_of_exact_rTensor R M _ _ ex

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)
complex : l12.range ≤ l23.ker
⊢ l23.ker = l12.range
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ map f I = ⊤ → I = ⊤

Tactic:
contrapose

Goal state after:
case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ ¬I = ⊤ → ¬map f I = ⊤
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case refine_1
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)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ p ≠ 0

Tactic:
simpa only [← Polynomial.map_ne_zero_iff (f := Subring.subtype _) (p := p)
        Subtype.val_injective, p, map_toSubring, smul_ne_zero_iff] using And.intro hr hp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R ((algebraMap R S) ra * a * ((algebraMap R S) rb * b))

Tactic:
← Algebra.smul_def

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (ra • a * rb • b)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ R[y]
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R (y * z * t)
⊢ IsAlgebraic R z

Tactic:
mul_right_comm,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ R[y]
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R (y * t * z)
⊢ IsAlgebraic R z
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ R[y]
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R ((algebraMap R S) r * z)
⊢ IsAlgebraic R z

Tactic:
← Algebra.smul_def

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ R[y]
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R (r • z)
⊢ IsAlgebraic R z
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
mul_right_comm,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).1 * (↑a).1 * (↑b).1 = (↑a).1 * (↑b).1
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
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
h₂ : ker (Pi.evalRingHom R i) ≤ p.asIdeal
⊢ Ideal.comap (Pi.evalRingHom R i) (Ideal.map (Pi.evalRingHom R i) p.asIdeal) = p.asIdeal

Tactic:
Ideal.comap_map_of_surjective _ h₁,

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
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
h₂ : ker (Pi.evalRingHom R i) ≤ p.asIdeal
⊢ p.asIdeal ⊔ Ideal.comap (Pi.evalRingHom R i) ⊥ = p.asIdeal
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
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
h₂ : ker (Pi.evalRingHom R i) ≤ p.asIdeal
⊢ Ideal.comap (Pi.evalRingHom R i) (Ideal.map (Pi.evalRingHom R i) p.asIdeal) = p.asIdeal

Tactic:
rwa [Ideal.comap_map_of_surjective _ h₁, sup_eq_left]

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

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

Tactic:
mul_right_comm,

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
⊢ (map f I).minimalPrimes = map f '' (I ⊔ RingHom.ker f).minimalPrimes

Tactic:
by
  apply Set.image_injective.mpr (Ideal.comap_injective_of_surjective f hf)
  rw [← Ideal.comap_minimalPrimes_eq_of_surjective hf, ← Set.image_comp,
    Ideal.comap_map_of_surjective f hf, Set.image_congr, Set.image_id, RingHom.ker]
  intro x hx
  exact (Ideal.comap_map_of_surjective f hf _).trans (sup_eq_left.mpr <| le_sup_right.trans hx.le)

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

Goal state before:
pp: case mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) →
    x ∈ range ⇑(algebraMap R K)

Tactic:
contrapose

Goal state after:
case mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∉ range ⇑(algebraMap R K) → ¬∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[instTopologicalSpaceSubtype] (coborder s ↓∩ s)

Tactic:
by
  rw [isClosed_preimage_val, inter_eq_right.mpr subset_coborder, coborder_inter_closure]

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 ⊆ B, Us.Finite ∧ U = sSup Us

Tactic:
by
  classical
  obtain ⟨Us', hsub, hsup⟩ := isBasis_iff_cover.mp hB U
  obtain ⟨t, ht⟩ := hU.elim_finite_subcover (fun s : Us' ↦ s.1) (fun s ↦ s.1.2) (by simp [hsup])
  refine ⟨Finset.image Subtype.val t, subset_trans (by simp) hsub, Finset.finite_toSet _, ?_⟩
  exact le_antisymm (subset_trans (a := U.carrier) ht (by simp))
    (le_trans (sSup_le_sSup (by simp)) hsup.ge)

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
⊢ DenseRange f ↔ ∀ (i : ι), DenseRange ((U i).carrier.restrictPreimage f)

Tactic:
by
  simp_rw [denseRange_iff_closure_range, Set.range_restrictPreimage,
    ← (U _).2.isOpenEmbedding_subtypeVal.isOpenMap.preimage_closure_eq_closure_preimage
      continuous_subtype_val]
  simp only [Opens.carrier_eq_coe, SetLike.coe_sort_coe, preimage_eq_univ_iff,
    Subtype.range_coe_subtype, SetLike.mem_coe]
  rw [← iUnion_subset_iff, ← Set.univ_subset_iff, iff_iff_eq]
  congr 1
  exact hU.iSup_set_eq_univ.symm

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsCodirectedOrder P
x : P
I✝ J✝ s t I J : Ideal P
w : P
h : w ∈ ↑I ∩ ↑J
⊢ {x | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}.Nonempty

Tactic:
exact ⟨w, w, h.1, w, h.2, le_sup_left⟩

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsCodirectedOrder P
x : P
I : Ideal P
hx : x ∉ I
h : I = I ⊔ principal x
⊢ x ∈ I

Tactic:
simpa only [left_eq_sup, principal_le_iff] using h

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.inf' hs t)

Tactic:
by
  rw [Finset.inf'_eq_inf]; exact .finsetInf ht

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf' hs t)

Tactic:
by
  rw [Finset.inf'_eq_inf]; exact .finsetInf ht

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.Flat
⊢ PreservesFiniteLimits (extendScalars f)

Tactic:
by
  have : PreservesFiniteLimits (extendScalars.{_, _, u} f ⋙ restrictScalars.{_, _, u} f) :=
    ModuleCat.preservesFiniteLimits_tensorLeft_of_ringHomFlat hf
  exact preservesFiniteLimits_of_reflects_of_preserves (extendScalars f) (restrictScalars f)

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

Goal state before:
pp: case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime✝ } =
    { asIdeal := pl, isPrime := ⋯ }
⊢ p = Ideal.under R (Ideal.under S Pl)

Tactic:
let := Localization.AtPrime.algebraOfLiesOver (Q.under R) Q
      replace hl : Pl.under _ = pl := by simpa [PrimeSpectrum.ext_iff] using! hl
      rw [Ideal.under_under, ← Ideal.under_under (B := (Localization.AtPrime <| Q.under R)) Pl, hl,
        Ideal.under_map_of_isLocalizationAtPrime (Q.under R) hlt.le]

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

Goal state before:
pp: R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ Module.Flat R S

Tactic:
apply Module.flat_of_isLocalized_maximal S S (fun P ↦ Localization.AtPrime P)
    (fun P ↦ Algebra.linearMap S _)

Goal state after:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := ⋯
⊢ ∀ (P : Ideal S) [inst : P.IsMaximal], Module.Flat R (Localization.AtPrime P)
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case pos
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime 1

pp: case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : ¬b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime (q ^ (a.lcm b).factorization q)

pp: case pos
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : ¬b.factorization p ≤ a.factorization p
h✝ : b.factorization q ≤ a.factorization q
⊢ Coprime 1 1

pp: case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : ¬b.factorization p ≤ a.factorization p
h✝ : ¬b.factorization q ≤ a.factorization q
⊢ Coprime 1 (q ^ (a.lcm b).factorization q)

Tactic:
any_goals simp only [coprime_one_right_eq_true, coprime_one_left_eq_true]

Goal state after:
case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : ¬b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime (q ^ (a.lcm b).factorization q)