mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Injective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
⊢ Function.Injective ⇑f

Tactic:
algebraize [f]
  let (r : s) : Algebra R (Sᵣ r) := (algebraMap S (Sᵣ r)).comp f |>.toAlgebra
  have (r : s) : IsScalarTower R S (Sᵣ r) := IsScalarTower.of_algebraMap_eq' rfl
  have : ∀ r, IsLocalization.Away (algebraMap R S r.val) (Sᵣ r) := ‹_›
  let (r : s) : Algebra (Rᵣ r) (Sᵣ r) := localizationAlgebra (.powers r.val) S
  have (r : s) : IsScalarTower R (Rᵣ r) (Sᵣ r) :=
    .of_algebraMap_eq <| by simp [RingHom.algebraMap_toAlgebra]
  apply injective_of_isLocalized_span s hs Rᵣ (fun r : s ↦ Algebra.linearMap _ _) _
    (fun r : s ↦ ((IsScalarTower.toAlgHom R S (Sᵣ r)).toLinearMap)) (Algebra.linearMap R S)
  simpa [IsLocalization.map_linearMap_eq_toLinearMap_mapₐ] using! h

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Surjective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
this✝² : (r : ↑s) → Algebra R (Sᵣ r) := fun r ↦ ((algebraMap S (Sᵣ r)).comp f).toAlgebra
this✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
this✝ : ∀ (r : ↑s), IsLocalization.Away ((algebraMap R S) ↑r) (Sᵣ r)
this : (r : ↑s) → Algebra (Rᵣ r) (Sᵣ r) := fun r ↦ localizationAlgebra (Submonoid.powers ↑r) S
r : ↑s
⊢ ∀ (x : R), (algebraMap R (Sᵣ r)) x = (algebraMap (Rᵣ r) (Sᵣ r)) ((algebraMap R (Rᵣ r)) x)

Tactic:
by simp [RingHom.algebraMap_toAlgebra]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
R' : Type u_2
R'' : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing R''
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R R''
inst✝² : Algebra R' R''
inst✝¹ : IsScalarTower R R' R''
inst✝ : Algebra R S
e : R' ⊗[R] S
a : R''
b : R'
c : S
⊢ (tensorQuotientTensorEquiv R'' e) (a ⊗ₜ[R'] (Ideal.Quotient.mk (Ideal.span {e})) (b ⊗ₜ[R] c)) =
    (Ideal.Quotient.mk (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e})) ((a * (algebraMap R' R'') b) ⊗ₜ[R] c)

Tactic:
simp [Algebra.tensorQuotientTensorEquiv, ← Ideal.Quotient.mk_algebraMap, ← map_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
r : R
J : Ideal R
h :
  ∀ (P : Ideal R) (x : P.IsMaximal),
    (algebraMap R (Localization.AtPrime P)) r ∈ map (algebraMap R (Localization.AtPrime P)) J
P : Ideal R
hP : P.IsMaximal
⊢ (?m.45 P) r ∈ Submodule.localized₀ P.primeCompl (?m.45 P) J

Tactic:
apply (localized'_eq_map (Localization.AtPrime P) P.primeCompl J).symm ▸ h P hP

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
mul_T : ∀ (f : R[X]) (n : ℕ), motive (toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : toLaurent f' = f * T ↑n
⊢ motive (f * T 0)

Tactic:
← Nat.cast_zero,

Goal state after:
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
mul_T : ∀ (f : R[X]) (n : ℕ), motive (toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : toLaurent f' = f * T ↑n
⊢ motive (f * T ↑0)
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : StarRing α
A : Matrix n n α
inst✝ : Invertible Aᴴ
⊢ Invertible A

Tactic:
rw [← conjTranspose_conjTranspose A, ← star_eq_conjTranspose]

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : StarRing α
A : Matrix n n α
inst✝ : Invertible Aᴴ
⊢ Invertible (star Aᴴ)
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ (A + U * C * V) * (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) = 1

Tactic:
by
  calc
    (A + U*C*V)*(⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)
    _ = A*⅟A - A*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A + U*C*V*⅟A - U*C*V*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by
      simp_rw [add_sub_assoc, add_mul, mul_sub, Matrix.mul_assoc]
    _ = (1 + U*C*V*⅟A) - (U*⅟(⅟C + V*⅟A*U)*V*⅟A + U*C*V*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) := by
      rw [mul_invOf_self, Matrix.one_mul]
      abel
    _ = 1 + U*C*V*⅟A - (U + U*C*V*⅟A*U)*⅟(⅟C + V*⅟A*U)*V*⅟A := by
      rw [sub_right_inj, Matrix.add_mul, Matrix.add_mul, Matrix.add_mul]
    _ = 1 + U*C*V*⅟A - U*C*(⅟C + V*⅟A*U)*⅟(⅟C + V*⅟A*U)*V*⅟A := by
      congr
      simp only [Matrix.mul_add, Matrix.mul_invOf_cancel_right, ← Matrix.mul_assoc]
    _ = 1 := by
      rw [Matrix.mul_invOf_cancel_right]
      abel

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

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ (((kroneckerMapBilinear f) A) 1 * ((kroneckerMapBilinear f) 1) B).det =
    (blockDiagonal fun x ↦ A.map fun a ↦ (f a) 1).det * (blockDiagonal fun x ↦ B.map fun b ↦ (f 1) b).det

Tactic:
rw [det_mul, ← diagonal_one, ← diagonal_one, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_right _ fun _ => _, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_left _ fun _ => _, det_reindex_self]
      · intro; exact LinearMap.map_zero₂ _ _
      · intro; exact map_zero _

Goal state after:
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 α
hA : IsLeftRegular A.det
⊢ IsRegular A

Tactic:
by
  constructor
  · intro B C h
    refine hA.matrix ?_
    simp only at h ⊢
    rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←
      adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, h]
  · intro B C (h : B * A = C * A)
    refine hA.matrix ?_
    simp only
    rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←
      mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]

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

Goal state before:
pp: α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
A : Matrix l m α
b : ℕ
x✝ : n
i✝ : l
j✝ : m
⊢ (A <• ↑b) i✝ j✝ = (b •> A) i✝ j✝

Tactic:
simp [(Nat.cast_commute b _).eq]

Goal state after:
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 α
inst✝ : Invertible A
⊢ ⅟A = A⁻¹

Tactic:
by
  let := detInvertibleOfInvertible A
  rw [inv_def, Ring.inverse_invertible, invOf_eq]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝¹ : LT α
inst✝ : NegZeroClass R
M : Matrix m m R
hM : M.BlockTriangular b
x✝¹ x✝ : m
h : b x✝ < b x✝¹
⊢ (-M) x✝¹ x✝ = 0

Tactic:
by rw [neg_apply, hM h, neg_zero]

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

Goal state before:
pp: case inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ∀ (i : Fin r), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0
j : Fin r
⊢ of (fun i j ↦ M (inr i) (inl j)) PUnit.unit j = 0 PUnit.unit j

Tactic:
exact (H j).2

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

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : MulActionWithZero R S
inst✝¹ : SMulCommClass R S S
inst✝ : IsScalarTower R S S
a : S
t : R
k : ℕ
ha : a ^ k = 0
⊢ (t • a) ^ k = 0

Tactic:
rw [smul_pow, ha, smul_zero]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
h_comm : ∀ (i j : ι), Commute (f i) (f j)
h : ¬HasFiniteSupport f
⊢ IsNilpotent (finsum f)

Tactic:
simp only [finsum_def, dif_neg h, IsNilpotent.zero]

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
⊢ ⊤.spanRank = p.spanRank

Tactic:
by
  simpa using (spanRank_map_eq_of_injective _ p.subtype_injective ⊤).symm

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

Goal state before:
pp: case e'_2
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
⊢ (reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n)) (1 + X • M.map ⇑C) = 1 + X • (e M).map ⇑C

Tactic:
ext; simp [map_add, e]

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
⊢ (1 + X • M.map ⇑C).det = (1 + X • M.map ⇑C).det.divX * X + C 1

Tactic:
convert! (divX_mul_X_add _).symm

Goal state after:
case e'_3
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 = (1 + X • M.map ⇑C).det.coeff 0
Module: Mathlib.Data.Nat.Choose.Cast

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
⊢ ↑(b.choose a) = ↑b ! / (↑a ! * ↑(b - a)!)

Tactic:
have : ∀ {n : ℕ}, (n ! : K) ≠ 0 := Nat.cast_ne_zero.2 (factorial_pos _).ne'

Goal state after:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ ↑(b.choose a) = ↑b ! / (↑a ! * ↑(b - a)!)
Module: Mathlib.Data.Nat.Choose.Cast

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
⊢ ↑(b.choose a) = ↑b ! / (↑a ! * ↑(b - a)!)

Tactic:
have : ∀ {n : ℕ}, (n ! : K) ≠ 0 := Nat.cast_ne_zero.2 (factorial_pos _).ne'
  rw [eq_div_iff_mul_eq (mul_ne_zero this this)]
  rw_mod_cast [← mul_assoc, choose_mul_factorial_mul_factorial h]

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

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

Tactic:
choose_succ_right_eq,

Goal state after:
case succ.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (k + 1) * (n + k + 1).choose n = (n + k + 1).choose n * (n + k + 1 - n)
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
hm : f.Monic
⊢ f = (Multiset.map (fun x ↦ X - C x) f.roots).prod

Tactic:
by
  conv_lhs => rw [hf.eq_prod_roots, hm.leadingCoeff, C_1, one_mul]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain A
inst✝² : IsDomain B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
hf : (map (algebraMap R A) f).Splits
φ : A →ₐ[R] B
hφ : map (algebraMap R B) f ≠ 0
⊢ map ((↑φ).comp (algebraMap R A)) f ≠ 0

Tactic:
φ.comp_algebraMap

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain A
inst✝² : IsDomain B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
hf : (map (algebraMap R A) f).Splits
φ : A →ₐ[R] B
hφ : map (algebraMap R B) f ≠ 0
⊢ map (algebraMap R B) f ≠ 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain A
inst✝² : IsDomain B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ : A →ₐ[R] B
hφ : map (↑φ) (map (algebraMap R A) f) ≠ 0
hf : (map ((↑φ).comp (algebraMap R A)) f).roots = Multiset.map (⇑↑φ) (map (algebraMap R A) f).roots
⊢ ⇑φ '' f.rootSet A = f.rootSet B

Tactic:
φ.comp_algebraMap

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain A
inst✝² : IsDomain B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ : A →ₐ[R] B
hφ : map (↑φ) (map (algebraMap R A) f) ≠ 0
hf : (map (algebraMap R B) f).roots = Multiset.map (⇑↑φ) (map (algebraMap R A) f).roots
⊢ ⇑φ '' f.rootSet A = f.rootSet B
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

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

Tactic:
by
  obtain rfl | h0 := eq_or_ne x 0
  · rw [inv_zero]; exact Subalgebra.zero_mem _
  have : FiniteDimensional R (R[x]) := .of_fg int.fg_adjoin_singleton
  obtain ⟨⟨y, hy⟩, h1⟩ := FiniteDimensional.exists_mul_eq_one R
    (K := R[x]) (x := ⟨x, subset_adjoin rfl⟩) (mt Subtype.ext_iff.mp h0)
  rwa [← mul_left_cancel₀ h0 ((Subtype.ext_iff.mp h1).trans (mul_inv_cancel₀ h0).symm)]

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

Goal state before:
pp: S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
⊢ ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s

Tactic:
obtain ⟨a, s, ha, h⟩ := hx.exists_smul_eq S
  obtain ⟨n, rfl | rfl⟩ := a.eq_nat_or_neg
  · exact ⟨n, s, mod_cast ha, mod_cast h⟩
  · exact ⟨n, -s, by simpa using ha, by simp [← h]⟩

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

Goal state before:
pp: case pos.inr
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
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h✝ : Nontrivial R
⊢ IsAlgebraic R a

Tactic:
have ⟨r, hr, _, e⟩ := (int.1 s).isAlgebraic.exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero hs)

Goal state after:
case pos.inr
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
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h✝ : Nontrivial R
r : R
hr : r ≠ 0
w✝ : S
e : (algebraMap R S) r = s * w✝
⊢ IsAlgebraic R a
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
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
hq : p.primesOver S = {q}
inst✝ : Algebra.IsIntegral R S
x : S
hx : x ∉ q
this : ∀ r ∉ p, ∀ (c : S), c * x ≠ (algebraMap R S) r
⊢ Disjoint ↑(span {x}) ↑(Algebra.algebraMapSubmonoid S p.primeCompl)

Tactic:
by simpa [Set.disjoint_iff_forall_ne, Ideal.mem_span_singleton',
      Algebra.algebraMapSubmonoid, @forall_comm S]

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

Goal state before:
pp: case right
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : K), IsAlgebraic R x
x : S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval ((algebraMap S K) x)) f = 0
⊢ (aeval x) f = 0

Tactic:
Polynomial.aeval_algebraMap_apply

Goal state after:
case right
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : K), IsAlgebraic R x
x : S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (algebraMap S K) ((aeval x) f) = 0
⊢ (aeval x) f = 0
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
g : S →+* T
f : R →+* S
hg : g.SurjectiveOnStalks
hf : f.SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
this :
  Function.Surjective
    (⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯) ∘
      ⇑(Localization.localRingHom (Ideal.comap f (Ideal.comap g I)) (Ideal.comap g I) f ⋯))
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)

Tactic:
rwa [← RingHom.coe_comp, ← Localization.localRingHom_comp] at this

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : FaithfullyFlat A B
a₁ a₂ : A
⊢ (∀ (a : B), a₁ • a = a₂ • a) → a₁ = a₂

Tactic:
ha

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : FaithfullyFlat A B
a₁ a₂ : A
ha : ∀ (a : B), a₁ • a = a₂ • a
⊢ a₁ = a₂
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
⊢ comap f J ∈ (comap f I).minimalPrimes

Tactic:
have := h.isPrime
  refine ⟨⟨inferInstance, Ideal.comap_mono h.le⟩, ?_⟩
  rintro K ⟨hK, e₁⟩ e₂
  have : RingHom.ker f ≤ K := (Ideal.comap_mono bot_le).trans e₁
  rw [← sup_eq_left.mpr this, RingHom.ker_eq_comap_bot, ← Ideal.comap_map_of_surjective f hf]
  apply Ideal.comap_mono _
  apply h.2 _ _
  · exact ⟨Ideal.map_isPrime_of_surjective hf this, Ideal.le_map_of_comap_le_of_surjective f hf e₁⟩
  · exact Ideal.map_le_of_le_comap e₂

Goal state after:
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case refine_2
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ∀ i ∈ ↑(Finset.image f' t), b i ⊆ U

Tactic:
rintro i hi

Goal state after:
case refine_2
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
i : ι
hi : i ∈ ↑(Finset.image f' t)
⊢ b i ⊆ U
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
⊢ ∀ (a : α), le a a

Tactic:
by intros; simp [eq_le]

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
a : X
⊢ ∃ i, a ∈ u i

Tactic:
simpa [← hu.iSup_set_eq_univ] using mem_univ a

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
Us : Set (Opens α)
x : α
⊢ x ∈ ⨆ a ∈ Us, a ↔ ∃ u ∈ Us, x ∈ u

Tactic:
mem_iSup,

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
Us : Set (Opens α)
x : α
⊢ (∃ i, ∃ (_ : i ∈ Us), x ∈ i) ↔ ∃ u ∈ Us, x ∈ u
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Function.Surjective ⇑(MaximalSpectrum.toPiLocalization ((i : ι) → R i))

Tactic:
rw [← AlgHom.coe_toRingHom, ← piLocalizationToMaximal_comp_toPiLocalization]

Goal state after:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Function.Surjective ⇑↑((piLocalizationToMaximal ((i : ι) → R i)).comp (toPiLocalization ((i : ι) → R i)))
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
Us : Set (Opens X)
hUs : W = sSup Us
a : ⦃a : Opens X⦄ → a ∈ Us → ι
ha : ∀ ⦃a_1 : Opens X⦄ (a_2 : a_1 ∈ Us), U (a a_2) = a_1
⊢ ∃ κ a, W = ⨆ k, U (a k)

Tactic:
use Us, fun i ↦ a i.2

Goal state after:
case h
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
Us : Set (Opens X)
hUs : W = sSup Us
a : ⦃a : Opens X⦄ → a ∈ Us → ι
ha : ∀ ⦃a_1 : Opens X⦄ (a_2 : a_1 ∈ Us), U (a a_2) = a_1
⊢ W = ⨆ k, U ((fun i ↦ a ⋯) k)
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible ↑t
h₂ : s ⊓ z₂ = sSup S₂
⊢ s = s ⊓ z₁ ⊔ s ⊓ z₂

Tactic:
← inf_sup_left,

Goal state after:
case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible ↑t
h₂ : s ⊓ z₂ = sSup S₂
⊢ s = s ⊓ (z₁ ⊔ z₂)
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a = ∅
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)

Tactic:
simp only [ha, Set.sInter_empty, Set.univ_inter]
      exact IsCompact.of_isClosed_subset (hc _ ht) (isClosed_sInter (by grind)) (by grind)

Goal state after: