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

Goal state before:
pp: case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
i : m
hi : b i = k
j : m
⊢ ¬b j = k → M i j = 0

Tactic:
hj

Goal state after:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
i : m
hi : b i = k
j : m
hj : ¬b j = k
⊢ M i j = 0
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)[X]
r : R
⊢ (matPolyEquiv.symm M).map (eval r) = eval ((scalar n) r) M

Tactic:
suffices ((aeval r).mapMatrix.comp matPolyEquiv.symm.toAlgHom : (Matrix n n R)[X] →ₐ[R] _) =
      (eval₂AlgHom (AlgHom.id R _) (scalar n r)
        fun x => (scalar_commute _ (Commute.all _) _).symm) from
    DFunLike.congr_fun this M

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)[X]
r : R
⊢ (aeval r).mapMatrix.comp ↑matPolyEquiv.symm = eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
H :
  ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
    P E → P ((List.map toMatrix L₁).prod * E * (List.map toMatrix L₂).prod)
⊢ P (diagonal D)

Tactic:
exact PD

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
M : Type u_9
N : Type u_10
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : Semiring S
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid N
inst✝¹² : Algebra R S
inst✝¹¹ : Module R M
inst✝¹⁰ : Module S M
inst✝⁹ : Module R N
inst✝⁸ : IsScalarTower R S M
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
ia : l
ja : m
ib : n
jb : p
a : M
b : N
⊢ single (ia, ib) (ja, jb) (a ⊗ₜ[R] b) = kroneckerMap (tmul R) (single ia ja a) (single ib jb b)

Tactic:
single_kroneckerTMul_single

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
M : Type u_9
N : Type u_10
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : Semiring S
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid N
inst✝¹² : Algebra R S
inst✝¹¹ : Module R M
inst✝¹⁰ : Module S M
inst✝⁹ : Module R N
inst✝⁸ : IsScalarTower R S M
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
ia : l
ja : m
ib : n
jb : p
a : M
b : N
⊢ single (ia, ib) (ja, jb) (a ⊗ₜ[R] b) = single (ia, ib) (ja, jb) (a ⊗ₜ[R] b)
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: case e_f
R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
n : ℕ
z : R
⊢ (RingHom.id R) z * (x + y) ^ n = z * (x ^ n + ↑n * x ^ (n - 1) * y + ↑(polyBinomAux1 x y n z) * y ^ 2)

Tactic:
apply (polyBinomAux1 x y _ _).property

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ span R ↑{1} = toSubmodule ⊥

Tactic:
by simp [Algebra.toSubmodule_bot, one_eq_span]

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
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ ∑ i, (M.charmatrix (c i) i).natDegree ≤ ∑ x with c x = x, 1

Tactic:
sum_filter

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, (M.charmatrix (c i) i).natDegree ≤ ∑ a, if c a = a then 1 else 0
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case empty
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
his : ∀ x ∈ ∅, IsIntegral R x
x : A
⊢ x ∈ span R ↑{1} ↔ x ∈ Subalgebra.toSubmodule ⊥

Tactic:
Finset.coe_singleton,

Goal state after:
case empty
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
his : ∀ x ∈ ∅, IsIntegral R x
x : A
⊢ x ∈ R ∙ 1 ↔ x ∈ Subalgebra.toSubmodule ⊥
Module: Mathlib.Data.Nat.Factorial.Cast

Goal state before:
pp: S : Type u_1
inst✝ : Ring S
a : ℕ
⊢ ↑((a - 1) * a.descFactorial 1) = ↑a * (↑a - 1)

Tactic:
cases a

Goal state after:
case zero
S : Type u_1
inst✝ : Ring S
⊢ ↑((0 - 1) * descFactorial 0 1) = ↑0 * (↑0 - 1)

case succ
S : Type u_1
inst✝ : Ring S
n✝ : ℕ
⊢ ↑((n✝ + 1 - 1) * (n✝ + 1).descFactorial 1) = ↑(n✝ + 1) * (↑(n✝ + 1) - 1)
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
h : s ∈ Set.range ⇑f
⊢ (monomial n) s ∈ lifts f

Tactic:
obtain ⟨r, rfl⟩ := Set.mem_range.1 h
  use monomial n r
  simp only [coe_mapRingHom, map_monomial]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = 0

Tactic:
by_cases! hil : i < l

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
hil : i < l
⊢ (i - l).choose k * i.choose l = 0

case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
hil : l ≤ i
⊢ (i - l).choose k * i.choose l = 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
x : R
f : R →+* S
h : f p.leadingCoeff ≠ 0
n✝ : ℕ
⊢ (map f (p.scaleRoots x)).coeff n✝ = ((map f p).scaleRoots (f x)).coeff n✝

Tactic:
simp [Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ h]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
ha : a ≤ p.natDegree
x✝ : q.natDegree < b ∨ b ≤ q.natDegree
⊢ p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
    p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))

Tactic:
cases lt_or_ge (natDegree q) b with

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ((C p.leadingCoeff).scaleRoots r * (Multiset.map (fun x ↦ X + C x) m).prod.scaleRoots r).Splits

pp: case inr.inr.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ (C p.leadingCoeff).leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod.leadingCoeff ≠ 0

Tactic:
scaleRoots_C

Goal state after:
case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ (C p.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod.scaleRoots r).Splits

case inr.inr.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ (C p.leadingCoeff).leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod.leadingCoeff ≠ 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
i : ℕ
H : (p.toSubring T hp).coeff i = 0
⊢ ↑((p.toSubring T hp).coeff i) = 0

Tactic:
by rw [H, ZeroMemClass.coe_zero]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : coeffIntegerNormalization M p i ≠ 0
⊢ i ∈ p.support

Tactic:
contrapose h

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : i ∉ p.support
⊢ coeffIntegerNormalization M p i = 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
fl : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := (R ∙ n).annihilator
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.lsmul R N).flip n) ⋯
⊢ inc.ker ≤ ⊥

Tactic:
by
    intro r hr
    induction r using Quotient.inductionOn' with | h r =>
    simpa only [Submodule.Quotient.mk''_eq_mk, Submodule.mem_bot, Submodule.Quotient.mk_eq_zero,
      Submodule.mem_annihilator_span_singleton, LinearMap.mem_ker, Submodule.liftQ_apply,
      LinearMap.flip_apply, LinearMap.lsmul_apply, I, inc] using hr

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 : ¬IsAlgebraic K ((aeval r) f)
⊢ ¬IsAlgebraic K r

Tactic:
contrapose 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 r
⊢ IsAlgebraic K ((aeval r) f)
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)

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:
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)
s : S
hs : s ∈ ↑(r • p).coeffs
⊢ s ∈ ↑(integralClosure R S).toSubring

Tactic:
by
    obtain ⟨n, hn, rfl⟩ := mem_coeffs_iff.mp hs
    exact int _ (Finset.mem_image_of_mem _ <| support_smul _ _ hn)

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
⊢ (∀ (P : Ideal S), P.IsPrime → ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x) ↔
    ∀ (I : Ideal S), I ≠ ⊤ → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x

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

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
H : ∀ (P : Ideal S), P.IsPrime → ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
I : Ideal S
hI : I ≠ ⊤
s : S
⊢ ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f 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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfullyFlat R S
inst✝ : Flat S (S ⊗[R] M)
⊢ ∀ ⦃N N' : Type (max u v)⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)

Tactic:
intro N P _ _ _ _ f hf

Goal state after:
R : Type u
M : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : FaithfullyFlat R S
inst✝⁴ : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
hf : Function.Injective ⇑f
⊢ Function.Injective ⇑(LinearMap.lTensor M f)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ map (Quotient.mk I) I = ⊥

Tactic:
map_quotient_self

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ⊥ = ⊥
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
hn : (algebraMap R (Localization.AtPrime p)) x ^ n ∈ map (algebraMap R (Localization.AtPrime p)) I
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
rw [IsLocalization.mem_map_algebraMap_iff (M := p.primeCompl)] at hn

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ sInf (Ideal.map (algebraMap R A) I).minimalPrimes = Ideal.map (algebraMap R A) q

Tactic:
IsLocalization.minimalPrimes_map q.primeCompl A I

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ sInf (Ideal.under R ⁻¹' I.minimalPrimes) = Ideal.map (algebraMap R A) q
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: 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✝ ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ →
    x✝ ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯

Tactic:
simpa only [Algebra.mem_iInf] using fun hx ⟨v, hv⟩ ↦ hx ⟨v, hv.isPrime⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U : Opens α
⊢ ¬(↑U).Nonempty ↔ U = ⊥

Tactic:
← coe_inj,

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
U : Opens α
⊢ ¬(↑U).Nonempty ↔ ↑U = ↑⊥
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
⊢ IsClosedMap (s.restrictPreimage f)

Tactic:
by
  intro t
  suffices ∀ u, IsClosed u → Subtype.val ⁻¹' u = t →
    ∃ v, IsClosed v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t by
      simpa [isClosed_induced_iff]
  exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
y : ↑s
⊢ IsCompact (f ⁻¹' {↑y})

Tactic:
exact H.isCompact_preimage isCompact_singleton

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ f ⁻¹' U ⊆ s

pp: case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' U)

pp: case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ f ⁻¹' V ⊆ s

pp: case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' V)

Tactic:
· intro x hx
    rw [← h.injective.injOn.mem_image_iff (Set.subset_univ _) trivial]
    exact hU hx

Goal state after:
case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' U)

case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ f ⁻¹' V ⊆ s

case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' V)
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
D : Type u_7
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : B →ₐ[R] D
hf : f.Flat
⊢ (Algebra.TensorProduct.lTensor A f).Flat

Tactic:
by
  algebraize [f.toRingHom, (Algebra.TensorProduct.lTensor (S := A) A f).toRingHom]
  let e : A ⊗[R] D ≃ₐ[A ⊗[R] B] (A ⊗[R] B) ⊗[B] D :=
    { __ := (Algebra.IsPushout.cancelBaseChangeAlg _ _ _ _ _).symm,
      commutes' x := congr($(Algebra.IsPushout.cancelBaseChange_symm_comp_lTensor R B D A) x) }
  exact .of_linearEquiv e.toLinearEquiv

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

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

Tactic:
have : (Algebra.TensorProduct.map f (AlgHom.id R D)).restrictScalars R =
        (Algebra.TensorProduct.comm _ _ _).toAlgHom.comp
          ((Algebra.TensorProduct.lTensor _ (f.restrictScalars R)).comp
            (Algebra.TensorProduct.comm _ _ _).toAlgHom) := by
      ext <;> simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (vanishingIdeal s).radical.IsRadical

Tactic:
apply Ideal.radical_isRadical

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ IsClosed Z ↔ IsClosed[TopologicalSpace.induced (comap (algebraMap R S)) zariskiTopology] Z

Tactic:
simp_rw [isClosed_induced_iff, isClosed_iff_zeroLocus, @eq_comm _ _ (zeroLocus _),
    exists_exists_eq_and, preimage_comap_zeroLocus]

Goal state after:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ (∃ s, zeroLocus s = Z) ↔ ∃ a, zeroLocus (⇑(algebraMap R S) '' a) = Z
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
h : IsCyclic α
⊢ ∃ g, orderOf g = Nat.card α

Tactic:
by
  obtain ⟨g, hg⟩ := h.exists_generator
  use g
  rw [← card_zpowers g, (eq_top_iff' (zpowers g)).mpr hg]
  exact Nat.card_congr (Equiv.Set.univ α)

Goal state after: