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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)

Tactic:
let := e.symm.toRingHom.toAlgebra
    have : IsLocalization.Away (1 : S) R :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.symm.bijective
    have : IsLocalization.Away (f 1) T :=
      IsLocalization.away_of_isUnit_of_bijective _ (by simp) (Equiv.refl _).bijective
    convert! hP f 1 R T hf
    have : RingHomInvPair (e : R →+* S) e.symm := RingHomInvPair.of_ringEquiv _
    have : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f :=
      IsLocalization.map_comp ..
    conv_lhs => rw [← this, RingHom.comp_assoc]
    simp only [RingEquiv.toRingHom_eq_coe, RingHomCompTriple.comp_eq]

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 α
i j : n
⊢ (cramer 1 ∘ₗ LinearMap.single α (fun i ↦ α) i) 1 j = (1 ∘ₗ LinearMap.single α (fun i ↦ α) i) 1 j

Tactic:
convert! congr_fun (cramer_row_self (1 : Matrix n n α) (Pi.single i 1) i _) j

Goal state after:
case e'_3.e'_1
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j : n
⊢ 1 = det 1

n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j : n
⊢ ∀ (j : n), Pi.single i 1 j = 1 j i
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 α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ (A.updateCol i (∑ x ∈ s, fun j ↦ f j x)).det = A.cramer (fun j ↦ ∑ x ∈ s, f j x) i

Tactic:
congr with j

Goal state after:
case e_b
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i j : n
⊢ (∑ x ∈ s, fun j ↦ f j x) j = ∑ x ∈ s, f j x
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 α
b : n → α
⊢ (∑ i, b i • fun j ↦ if i = j then 1 else 0) = ∑ i, b i • Pi.single i 1

Tactic:
congr with j

Goal state after:
case e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
j x✝ : n
⊢ (b j • fun j_1 ↦ if j = j_1 then 1 else 0) x✝ = (b j • Pi.single j 1) x✝
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case cons
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH :
  ∀ (M : Matrix n n R) (N : Matrix p p R),
    fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) L).prod = fromBlocks (M * (List.map toMatrix L).prod) 0 0 N
M : Matrix n n R
N : Matrix p p R
⊢ fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) (t :: L)).prod =
    fromBlocks (M * (List.map toMatrix (t :: L)).prod) 0 0 N

Tactic:
simp [IH, toMatrix_sumInl, fromBlocks_multiply]

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

Goal state before:
pp: m : Type u_2
R : Type u_6
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : CommSemiring R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ (↑M * N * ↑M⁻¹).trace = N.trace

Tactic:
trace_mul_cycle,

Goal state after:
m : Type u_2
R : Type u_6
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : CommSemiring R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ (↑M⁻¹ * ↑M * N).trace = N.trace
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_9
n : Type u_10
R : Type u_11
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Fintype m
i : n
j : m
a : R
x : Matrix m n R
⊢ (single i j a * x).trace = a • x j i

Tactic:
simp [trace, mul_apply, single, ite_and]

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

Goal state before:
pp: m : Type u_9
n : Type u_10
R : Type u_11
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Fintype m
x : Matrix m n R
i : n
j : m
a : R
⊢ (x * single i j a).trace = MulOpposite.op a • x j i

Tactic:
simp [trace, mul_apply, single, ite_and]

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 β
⊢ (kroneckerMap (fun r s ↦ (f r) s) A (diagonal fun x ↦ 1)).det *
      (((kroneckerMapBilinear f) (diagonal fun x ↦ 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:
kroneckerMap_diagonal_right _ fun _ => _,

Goal state after:
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 β
⊢ (blockDiagonal fun i ↦ A.map fun a ↦ (f a) 1).det * (((kroneckerMapBilinear f) (diagonal fun x ↦ 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

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 β
⊢ ∀ (x : α), (f x) 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
⊢ (M * (listTransvecRow M).prod) i (inr ()) = M i (inr ())

Tactic:
have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
  rw [← List.take_length (l := listTransvecRow M), A]
  simpa using mul_listTransvecRow_last_col_take M i le_rfl

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

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
B C : Matrix m n α
h : B = C * A
⊢ B * A⁻¹ = C

Tactic:
rw [h, mul_inv_cancel_right_of_invertible]

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 α
h : Fintype.card n ≠ 1
⊢ A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A

Tactic:
rcases h_card : Fintype.card n with _ | n'
  · subsingleton [Fintype.card_eq_zero_iff.mp h_card]
  cases n'
  · exact (h h_card).elim
  rw [← h_card]
  -- express `A` as an evaluation of a polynomial in n^2 variables, and solve in the polynomial ring
  -- where `A'.det` is non-zero.
  let A' := mvPolynomialX n n ℤ
  suffices adjugate (adjugate A') = det A' ^ (Fintype.card n - 2) • A' by
    rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_adjugate, this,
      ← AlgHom.map_det, ← map_pow (MvPolynomial.aeval fun p : n × n ↦ A p.1 p.2),
      AlgHom.mapMatrix_apply, AlgHom.mapMatrix_apply, Matrix.map_smul' _ _ _ (map_mul _)]
  have h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1 := by simp [h_card]
  have is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) (det A') := fun x y =>
    mul_left_cancel₀ (det_mvPolynomialX_ne_zero n ℤ)
  apply is_reg.matrix
  simp only
  rw [smul_smul, ← pow_succ', h_card', det_smul_adjugate_adjugate]

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

Goal state before:
pp: m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : LinearOrder m
M : Matrix m m R
h : M.IsLowerTriangular
⊢ M.det = ∏ i, M i i

Tactic:
← det_transpose

Goal state after:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : LinearOrder m
M : Matrix m m R
h : M.IsLowerTriangular
⊢ Mᵀ.det = ∏ i, M i i
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h✝ : i' = i ∧ j' = j
⊢ x.coeff k = x.coeff k

Tactic:
rename_i h

Goal state after:
case pos
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h : i' = i ∧ j' = j
⊢ x.coeff k = x.coeff k
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h✝ : ¬(i' = i ∧ j' = j)
⊢ 0 = coeff 0 k

Tactic:
rename_i h

Goal state after:
case neg
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h : ¬(i' = i ∧ j' = j)
⊢ 0 = coeff 0 k
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 n α
B : Matrix n m α
⊢ (1 + -(B * A)).det = (1 - B * A).det

Tactic:
← sub_eq_add_neg

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 n α
B : Matrix n m α
⊢ (1 - B * A).det = (1 - B * A).det
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval (x + y) f = f.sum fun e a ↦ a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(polyBinomAux1 x y e a) * y ^ 2)

Tactic:
unfold eval

Goal state after:
R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval₂ (RingHom.id R) (x + y) f = f.sum fun e a ↦ a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(polyBinomAux1 x y e a) * y ^ 2)
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_2.inr
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent ((reflect N P).coeff i)

Tactic:
simpa [revAt_eq_self_of_lt hi] using h i

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
⊢ ∃ a, (toEnd R b hb) a = f

Tactic:
obtain ⟨M, e, -⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R b hb f ⊤ (by simp)

Goal state after:
ι : Type u_1
inst✝⁴ : Fintype ι
M✝ : Type u_2
inst✝³ : AddCommGroup M✝
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M✝
b : ι → M✝
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M✝
M : ↥(isRepresentation R b)
e : (toEnd R b hb) M = f
⊢ ∃ a, (toEnd R b hb) a = f
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
⊢ p.spanRank < ℵ₀ ↔ p.FG

Tactic:
rw [spanRank, Submodule.fg_def]

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⨅ s, #↑↑s < ℵ₀ ↔ ∃ S, S.Finite ∧ span R S = p
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
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ ↑(1 * I) ≤ span R ↑T * span R ↑T' * ↑I

Tactic:
Units.val_mul,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ ↑1 * ↑I ≤ span R ↑T * span R ↑T' * ↑I
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
hp : ¬p.FG
h : p.spanRank < ℵ₀
⊢ False

Tactic:
exact hp (spanRank_finite_iff_fg.1 h)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
hf : Function.Injective ⇑f
p : Submodule R M
s : Set M
hs : Cardinal.mk ↑(⇑f '' s) = (map f p).spanRank
e : span S (⇑f '' s) = map f p
⊢ span R s = p

Tactic:
by simpa [(map_injective_of_injective hf).eq_iff] using e

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case right
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
⊢ eval₂ (algebraMap R B) ((algebraMap A B) x) f = 0

Tactic:
rw [IsScalarTower.algebraMap_eq R A B, ← hom_eval₂, hx, map_zero]

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
hM : IsNilpotent M
a✝ : Nontrivial R
p : R[X] := M.charpolyRev
⊢ p %ₘ X + X * (p /ₘ X) - 1 = X * (p /ₘ X)

Tactic:
simp [p, modByMonic_X]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x : R
hx : x ≠ 0
⊢ (C x).integralNormalization = 1

Tactic:
by
  simp [integralNormalization, sum_def, support_C hx, degree_C hx]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
⊢ (p.scaleRoots r).Splits

Tactic:
obtain rfl | hp0 := eq_or_ne p 0

Goal state after:
case inr.inl
R : Type u_1
inst✝ : CommSemiring R
r : R
h✝ : Nontrivial R
hp : Splits 0
⊢ (Polynomial.scaleRoots 0 r).Splits

case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
⊢ (p.scaleRoots r).Splits
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]
b : R
hb : b ∈ ↑M
h : IsInteger R[X] (C b • p)
⊢ ∃ b ∈ M, ∃ q, Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support

Tactic:
C_eq_algebraMap,

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]
b : R
hb : b ∈ ↑M
h : IsInteger R[X] ((algebraMap R R[X]) b • p)
⊢ ∃ b ∈ M, ∃ q, Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support
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)
n1 : N1
⊢ l23 (l12 n1) = 0

Tactic:
by_contra! hn1

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)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
⊢ False
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := ⋯
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := ⋯
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := ⋯
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ eval₂ (algebraMap R S) t q' = t ^ N * q.sum fun x1 x2 ↦ t ^ x1 * φ.toRingHom x2

Tactic:
simp [φ, q', Polynomial.sum, ← aeval_def, this, mul_left_comm _ (t ^ N), ← Finset.mul_sum]

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
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Function.Injective ⇑(lTensor B ((TensorProduct.mk A B M) 1))

Tactic:
have : (lTensor B <| TensorProduct.mk A B M 1) =
      (TensorProduct.leftComm A B B M).symm.comp (TensorProduct.mk A B (B ⊗[A] M) 1) := by
    apply TensorProduct.ext'
    intro x y
    simp

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
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
this : lTensor B ((TensorProduct.mk A B M) 1) = ↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1
⊢ Function.Injective ⇑(lTensor B ((TensorProduct.mk A B M) 1))
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Surjective ⇑f
x✝¹ x✝ : PrimeSpectrum S
h : { asIdeal := Ideal.comap f x✝¹.asIdeal, isPrime := ⋯ } = { asIdeal := Ideal.comap f x✝.asIdeal, isPrime := ⋯ }
⊢ Ideal.comap f x✝¹.asIdeal = Ideal.comap f x✝.asIdeal

Tactic:
simpa using h

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

Goal state before:
pp: case intro
ι : 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
this : Ideal.comap (Pi.evalRingHom R i) (Ideal.map (Pi.evalRingHom R i) p.asIdeal) = p.asIdeal
⊢ ∃ i q, comap (Pi.evalRingHom R i) q = p

Tactic:
exact ⟨i, ⟨_, Ideal.map_isPrime_of_surjective h₁ h₂⟩, PrimeSpectrum.ext this⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
⊢ KrullDimLE 1 R

Tactic:
by_cases hR : (⊥ : Ideal R).IsPrime

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ⊥.IsPrime
⊢ KrullDimLE 1 R

case neg
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ¬⊥.IsPrime
⊢ KrullDimLE 1 R
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case a
ι : Type u_3
R : ι → Type u_4
inst✝² : (i : ι) → CommRing (R i)
inst✝¹ : _root_.Finite ι
S : Type u_5
inst✝ : CommRing S
f : S →+* (i : ι) → R i
⊢ Set.range (comap f) ⊆ ⋃ i, Set.range (comap f ∘ comap (Pi.evalRingHom R i))

Tactic:
rintro _ ⟨p, rfl⟩
    obtain ⟨i, p, rfl⟩ := exists_comap_evalRingHom_eq p
    exact Set.mem_iUnion_of_mem i ⟨p, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case refine_1
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
⊢ Ideal.map (algebraMap R A) q ∈ Ideal.under R ⁻¹' I.minimalPrimes

Tactic:
Set.mem_preimage,

Goal state after:
case refine_1
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
⊢ Ideal.under R (Ideal.map (algebraMap R A) q) ∈ I.minimalPrimes
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ False

Tactic:
rw [← IsLocalization.lift_eq (M := J.primeCompl) (S := Localization J.primeCompl), hJ, map_one,
    Function.update_of_ne] at hI

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI : 1 = 0 I
⊢ False

case h
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI : 1 = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ I ≠ { asIdeal := J, isPrime := ⋯ }

case hg
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ ∀ (y : ↥J.primeCompl), IsUnit ((algebraMap R (Localization I.asIdeal.primeCompl)) ↑y)
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s = univ ↔ IsClosed[inst✝] s

Tactic:
simp [coborder, sdiff_eq_empty, closure_subset_iff_isClosed]

Goal state after: