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

Goal state before:
pp: case neg.inr
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h✝ : Nonempty m
hAB : ¬IsUnit (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B).det
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ B⁻¹

Tactic:
nonsing_inv_apply_not_isUnit _ hB,

Goal state after:
case neg.inr
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h✝ : Nonempty m
hAB : ¬IsUnit (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B).det
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ 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
  ext : 1
  · ext M : 1
    simp [Function.comp_def]
  · simp

Goal state after:
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]
i j : n
⊢ (m i j).support ⊆ (matPolyEquiv m).support

Tactic:
by
  intro k
  contrapose
  simp only [notMem_support_iff]
  intro hk
  rw [← matPolyEquiv_coeff_apply, hk, Matrix.zero_apply]

Goal state after:
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 α
⊢ IsUnit (fromBlocks A B 0 D) ↔ IsUnit A ∧ IsUnit D

Tactic:
simp only [← nonempty_invertible_iff_isUnit, ← nonempty_prod,
    (fromBlocksZero₂₁InvertibleEquiv _ _ _).nonempty_congr]

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A) x) = x
hy : invFun n R A ((toFunAlgHom n R A) y) = y
| invFun n R A ((toFunAlgHom n R A) x) + invFun n R A ((toFunAlgHom n R A) y)

Tactic:
← invFun_add

Goal state after:
n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A) x) = x
hy : invFun n R A ((toFunAlgHom n R A) y) = y
| invFun n R A ((toFunAlgHom n R A) x + (toFunAlgHom n R A) y)
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
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : Semiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : Fintype n
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : StarRing R
inst✝³ : StarAddMonoid A
inst✝² : StarAddMonoid B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
x : Matrix m m A ⊗[R] Matrix n n B
⊢ ∀ (x y : Matrix m m A ⊗[R] Matrix n n B),
    (kroneckerTMulAlgEquiv m n R S A B) (star x) = star ((kroneckerTMulAlgEquiv m n R S A B) x) →
      (kroneckerTMulAlgEquiv m n R S A B) (star y) = star ((kroneckerTMulAlgEquiv m n R S A B) y) →
        (kroneckerTMulAlgEquiv m n R S A B) (star (x + y)) = star ((kroneckerTMulAlgEquiv m n R S A B) (x + y))

Tactic:
by simp_all

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
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Semiring B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : StarRing R
x : Matrix m m R ⊗[R] Matrix n n R
⊢ ∀ (x y : Matrix m m R ⊗[R] Matrix n n R),
    (kroneckerAlgEquiv m n R) (star x) = star ((kroneckerAlgEquiv m n R) x) →
      (kroneckerAlgEquiv m n R) (star y) = star ((kroneckerAlgEquiv m n R) y) →
        (kroneckerAlgEquiv m n R) (star (x + y)) = star ((kroneckerAlgEquiv m n R) (x + y))

Tactic:
by simp_all

Goal state after:
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 α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ fromBlocks A B C D = (fromBlocks D C B A).submatrix ⇑(Equiv.sumComm m n) ⇑(Equiv.sumComm m n)

Tactic:
ext (i j)

Goal state after:
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 α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
i j : m ⊕ n
⊢ fromBlocks A B C D i j = (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) i j
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval₂ (RingHom.id R) x f - eval₂ (RingHom.id R) y f = (f.sum fun i r ↦ r * ↑(powSubPowFactor x y i)) * (x - y)

Tactic:
eval₂_eq_sum,

Goal state after:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (f.sum fun e a ↦ (RingHom.id R) a * x ^ e) - eval₂ (RingHom.id R) y f =
    (f.sum fun i r ↦ r * ↑(powSubPowFactor x y i)) * (x - y)
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r u
⊢ IsUnit (u + r)

Tactic:
by
  rw [← Units.isUnit_mul_units _ hu.unit⁻¹, add_mul, IsUnit.mul_val_inv]
  replace h_comm : Commute r (↑hu.unit⁻¹) := Commute.units_inv_right h_comm
  refine IsNilpotent.isUnit_one_add ?_
  exact (hu.unit⁻¹.isUnit.isNilpotent_mul_unit_of_commute_iff h_comm).mpr hnil

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

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x + y)

Tactic:
by
  obtain ⟨n, hn⟩ := hx
  obtain ⟨m, hm⟩ := hy
  exact ⟨_, add_pow_add_eq_zero_of_pow_eq_zero h_comm hn hm⟩

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
x✝ : p.IsPrincipal ∧ p ≠ ⊥
a : M
ha : p = R ∙ a
right✝ : p ≠ ⊥
⊢ a ≠ 0

Tactic:
by simp_all

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
this : Nontrivial R
I : Type u_2
B : Basis I R M
⊢ #I = #↑(Set.range ⇑B)

Tactic:
← Cardinal.lift_id #(Set.range B),

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
this : Nontrivial R
I : Type u_2
B : Basis I R M
⊢ #I = lift.{u_2, u_2} #↑(Set.range ⇑B)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
n : ℕ
hn : 0 < n
hx : IsIntegral R (x ^ n)
p : R[X]
hmonic : p.Monic
heval : eval₂ (algebraMap R B) (x ^ n) p = 0
⊢ (aeval x) ((expand R n) p) = 0

Tactic:
expand_aeval

Goal state after:
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
n : ℕ
hn : 0 < n
hx : IsIntegral R (x ^ n)
p : R[X]
hmonic : p.Monic
heval : eval₂ (algebraMap R B) (x ^ n) p = 0
⊢ (aeval (x ^ n)) p = 0
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
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
⊢ M.charpoly.coeff i = (X ^ 2 - C M.trace * X + C M.det).coeff i

Tactic:
by_cases hi : i ∈ Finset.range 3

Goal state after:
case pos
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

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
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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
⊢ ∀ i ∈ univ, ∀ (k : ℕ), (M.charmatrix (c i) i).coeff k ∈ I ^ (1 - k)

Tactic:
rintro i - (_ | k)

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
⊢ (M.charmatrix (c i) i).coeff 0 ∈ I ^ (1 - 0)

case succ
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
k : ℕ
⊢ (M.charmatrix (c i) i).coeff (k + 1) ∈ I ^ (1 - (k + 1))
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
⊢ p.integralNormalization.coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
rw [integralNormalization_coeff]
  split_ifs with h
  · simp [natDegree_eq_of_degree_eq_some h, leadingCoeff,
      ← pow_succ', tsub_add_cancel_of_le (natDegree_eq_of_degree_eq_some h ▸ hp)]
  · simp only [mul_assoc, ← pow_add]
    by_cases h' : i < p.degree
    · rw [tsub_add_cancel_of_le]
      rw [le_tsub_iff_right hp, Nat.succ_le_iff]
      exact coe_lt_degree.mp h'
    · simp [coeff_eq_zero_of_degree_lt (lt_of_le_of_ne (le_of_not_gt h') h)]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
p : R[X]
r : R
n : ℕ
hp : ¬p = 0
hn : ¬n = 0
⊢ p.leadingCoeff ^ n ≠ 0

Tactic:
by simp_all

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ ((X + C a).comp (-X)).Splits

Tactic:
· rw [add_comp, X_comp, C_comp, neg_add_eq_sub, ← neg_sub]
      exact (X_sub_C a).neg

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
g : R[X]
hg : (f * g).Splits
hg₀ : f * g ≠ 0
⊢ f ≠ 0

Tactic:
by simp_all

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
g : R[X]
hg : (f * g).Splits
hg₀ : f * g ≠ 0
⊢ g ≠ 0

Tactic:
by simp_all

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✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
inst✝ : IsScalarTower R A B
f : R[X]
hf : (map (algebraMap R A) f).Splits
⊢ ⇑(algebraMap A B) '' f.rootSet A = f.rootSet B

Tactic:
classical
  rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, hf.map_aroots_algebraMap, ← rootSet]

Goal state after:
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
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff (p.natDegree * (C y * X).natDegree) = 0
hy0 : y ≠ 0
⊢ (C y * X).natDegree ≠ 0

Tactic:
rw [natDegree_C_mul_X _ hy0]; rintro ⟨⟩

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
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Surjective ⇑f

Tactic:
rw [← LinearMap.exact_zero_iff_surjective (M ⊗[R] Unit),
    ← LinearMap.exact_zero_iff_surjective Unit]
  conv_rhs => rw [← lTensor_exact_iff_exact R M]
  simp

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

Goal state before:
pp: case hx
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral R ((algebraMap S L) x)

Tactic:
apply IsIntegral.map (IsScalarTower.toAlgHom R S L)

Goal state after:
case hx
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral R x
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case hy
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral R ⅟(mk' L 1 s)

Tactic:
apply IsIntegral.map (IsScalarTower.toAlgHom R S L)

Goal state after:
case hy
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral R ↑s
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ ∃ x_1 r,
    ∃ c ∉ J, (algebraMap S (S ⊗[R] T)) r ∉ J ∧ c * (algebraMap S (S ⊗[R] T)) r * x = c * (algebraMap S (S ⊗[R] T)) x_1

Tactic:
refine ⟨a, algebraMap _ _ r, 1 ⊗ₜ (r • t), ht, ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ (algebraMap S (S ⊗[R] T)) ((algebraMap R S) r) ∉ J

case refine_2
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ 1 ⊗ₜ[R] (r • t) * (algebraMap S (S ⊗[R] T)) ((algebraMap R S) r) * x = 1 ⊗ₜ[R] (r • t) * (algebraMap S (S ⊗[R] T)) a
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
⊢ Set.range (comap f) = zeroLocus ↑(ker f)

Tactic:
← Set.image_univ

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ comap f '' Set.univ = zeroLocus ↑(ker f)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
⊢ ∃ p' ∈ I.minimalPrimes, comap f p' = p

Tactic:
obtain ⟨p', h₁, h₂, h₃⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f p H

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
⊢ ∃ p' ∈ I.minimalPrimes, comap f p' = p
Module: Mathlib.Topology.NoetherianSpace

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

Tactic:
by
  simp_rw [noetherianSpace_set_iff] at hf ⊢
  intro t ht
  rw [← Set.inter_eq_left.mpr ht, Set.inter_iUnion]
  exact isCompact_iUnion fun i => hf i _ Set.inter_subset_right

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

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

Tactic:
h.isEmbedding.isCompact_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst✝¹] U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen[inst✝¹] V
hV'' : IsCompact V
⊢ IsCompact (f '' (U ∩ V))
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsOpen[inst✝] s
⊢ IsQuasiSeparated s ↔ QuasiSeparatedSpace ↑s

Tactic:
by
  rw [← isQuasiSeparated_univ_iff]
  convert! (hs.isOpenEmbedding_subtypeVal.isQuasiSeparated_iff (s := Set.univ)).symm
  simp

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
b : ι → Set X
basis : IsTopologicalBasis (Set.range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
⊢ ∀ U ∈ Set.range b, IsCompact U

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
⊢ ⊥ ∈ (⨅ s ∈ S, s.toLowerSet).carrier

Tactic:
rw [LowerSet.carrier_eq_coe, LowerSet.coe_iInf₂, Set.mem_iInter₂]

Goal state after:
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
⊢ ∀ i ∈ S, ⊥ ∈ ↑i.toLowerSet
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
⊢ IsRetrocompact ∅

Tactic:
by simp [IsRetrocompact]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
h : Function.Injective (NonemptyCompacts.map f hf)
x✝² x✝¹ : α
x✝ : ((fun x ↦ {x}) ∘ f) x✝² = ((fun x ↦ {x}) ∘ f) x✝¹
⊢ NonemptyCompacts.map f hf ((fun x ↦ {x}) x✝²) = NonemptyCompacts.map f hf ((fun x ↦ {x}) x✝¹)

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: case h.a
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : R1Space α
S✝ : Set α
h : IsIrreducible S✝
hs : IsClosed S✝
x : α
hx : x ∈ S✝
⊢ closure {x} ⊆ S✝

Tactic:
rw [← hs.closure_eq]

Goal state after:
case h.a
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : R1Space α
S✝ : Set α
h : IsIrreducible S✝
hs : IsClosed S✝
x : α
hx : x ∈ S✝
⊢ closure {x} ⊆ closure S✝
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
⊢ (algebraMap R S).Flat ↔ Module.Flat R S

Tactic:
RingHom.Flat,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Module.Flat R S ↔ Module.Flat R S
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : (Ideal.comap f P).IsPrime
algInst✝¹ : Algebra R S := f.toAlgebra
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
algebraizeInst✝ : Module.Flat R S
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯).Flat

Tactic:
RingHom.Flat,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : (Ideal.comap f P).IsPrime
algInst✝¹ : Algebra R S := f.toAlgebra
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
algebraizeInst✝ : Module.Flat R S
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: b : ℕ
⊢ factorizationLCMLeft 0 b = 1

Tactic:
by
  simp [factorizationLCMLeft]

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

Goal state before:
pp: a : ℕ
⊢ a.factorizationLCMLeft 0 = 1

Tactic:
by
  simp [factorizationLCMLeft]

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

Goal state before:
pp: a b : ℕ
⊢ a.factorizationLCMRight b ≠ 0

Tactic:
factorizationLCMRight,

Goal state after:
a b : ℕ
⊢ ((a.lcm b).factorization.prod fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n) ≠ 0
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ((a.lcm b).factorization.prod fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1) *
      a.factorizationLCMRight b =
    (a.lcm b).factorization.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
factorizationLCMRight,

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (((a.lcm b).factorization.prod fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1) *
      (a.lcm b).factorization.prod fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n) =
    (a.lcm b).factorization.prod fun x1 x2 ↦ x1 ^ x2