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

Goal state before:
pp: case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h_det : IsUnit A.det
val✝ : Invertible A
⊢ A⁻¹ = A⁻¹ʳ

Tactic:
← invOf_eq_nonsing_inv,

Goal state after:
case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h_det : IsUnit A.det
val✝ : Invertible A
⊢ ⅟A = A⁻¹ʳ
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A
⊢ A * A⁻¹ = 1

Tactic:
← invOf_eq_nonsing_inv,

Goal state after:
case intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A
⊢ A * ⅟A = 1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A
⊢ A⁻¹ * A = 1

Tactic:
← invOf_eq_nonsing_inv,

Goal state after:
case intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A
⊢ ⅟A * A = 1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
inst✝² : DecidableEq m
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m m R
⊢ (∃ B, B * A = 1) ↔ IsUnit A

Tactic:
isUnit_iff_exists_inv'

Goal state after:
m : Type u
inst✝² : DecidableEq m
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m m R
⊢ (∃ B, B * A = 1) ↔ ∃ b, b * A = 1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A.det
this : Invertible A := A.invertibleOfDetInvertible
⊢ A⁻¹.det = ⅟A.det

Tactic:
← invOf_eq_nonsing_inv,

Goal state after:
case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A.det
this : Invertible A := A.invertibleOfDetInvertible
⊢ (⅟A).det = ⅟A.det
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • (B.adjugate * A.det⁻¹ʳ • A.adjugate)

Tactic:
Matrix.mul_smul,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • A.det⁻¹ʳ • (B.adjugate * A.adjugate)
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case pos.intro
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 α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
this : Invertible (A.submatrix ⇑e₁ ⇑e₂) := A.submatrixEquivInvertible e₁ e₂
⊢ (A.submatrix ⇑e₁ ⇑e₂)⁻¹ = A⁻¹.submatrix ⇑e₂ ⇑e₁

Tactic:
← invOf_eq_nonsing_inv,

Goal state after:
case pos.intro
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 α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
this : Invertible (A.submatrix ⇑e₁ ⇑e₂) := A.submatrixEquivInvertible e₁ e₂
⊢ ⅟(A.submatrix ⇑e₁ ⇑e₂) = A⁻¹.submatrix ⇑e₂ ⇑e₁
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case pos.intro
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 α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
this : Invertible (A.submatrix ⇑e₁ ⇑e₂) := A.submatrixEquivInvertible e₁ e₂
⊢ ⅟(A.submatrix ⇑e₁ ⇑e₂) = A⁻¹.submatrix ⇑e₂ ⇑e₁

Tactic:
← invOf_eq_nonsing_inv,

Goal state after:
case pos.intro
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 α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
this : Invertible (A.submatrix ⇑e₁ ⇑e₂) := A.submatrixEquivInvertible e₁ e₂
⊢ ⅟(A.submatrix ⇑e₁ ⇑e₂) = (⅟A).submatrix ⇑e₂ ⇑e₁
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
h : i ≠ j
⊢ M.charmatrix i j = -C (M i j)

Tactic:
by
  simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply, diagonal_apply_ne _ h,
    map_apply, sub_eq_neg_self]

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
p : R[X]
M : Matrix n n R[X]
⊢ matPolyEquiv (p • M) = Polynomial.map (algebraMap R (Matrix n n R)) p * matPolyEquiv M

Tactic:
← one_mul M,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
M : Matrix n n R[X]
⊢ matPolyEquiv (p • (1 * M)) = Polynomial.map (algebraMap R (Matrix n n R)) p * matPolyEquiv (1 * M)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
e : n ≃ m
M : Matrix n n R
⊢ ((reindex e e) M).charpoly = M.charpoly

Tactic:
unfold Matrix.charpoly
  rw [charmatrix_reindex, Matrix.det_reindex_self]

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

Goal state before:
pp: case cons
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)
L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
t : TransvectionStruct n 𝕜
L₁ : List (TransvectionStruct n 𝕜)
IH : P ((List.map toMatrix L₁).prod * (E * (List.map toMatrix L₂).prod))
⊢ P (t.toMatrix * ((List.map toMatrix L₁).prod * (E * (List.map toMatrix L₂).prod)))

Tactic:
exact hmul _ _ (htransvec _) IH

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

Goal state before:
pp: case pos.intro.intro
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 α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val✝¹ : Invertible A
val✝ : Invertible D
this : Invertible (fromBlocks A B 0 D) := A.fromBlocksZero₂₁Invertible B D
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹

Tactic:
← invOf_eq_nonsing_inv,

Goal state after:
case pos.intro.intro
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 α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val✝¹ : Invertible A
val✝ : Invertible D
this : Invertible (fromBlocks A B 0 D) := A.fromBlocksZero₂₁Invertible B D
⊢ ⅟(fromBlocks A B 0 D) = fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case pos.intro.intro
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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val✝¹ : Invertible A
val✝ : Invertible D
this : Invertible (fromBlocks A 0 C D) := A.fromBlocksZero₁₂Invertible C D
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹

Tactic:
← invOf_eq_nonsing_inv,

Goal state after:
case pos.intro.intro
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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val✝¹ : Invertible A
val✝ : Invertible D
this : Invertible (fromBlocks A 0 C D) := A.fromBlocksZero₁₂Invertible C D
⊢ ⅟(fromBlocks A 0 C D) = fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) ⅟D
Module: Mathlib.Tactic.Ring.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LE α
a b c d : α
h1 : a = b
h2 : b ≤ c
h3 : d = c
⊢ a ≤ d

Tactic:
h1,

Goal state after:
α : Type u_1
inst✝ : LE α
a b c d : α
h1 : a = b
h2 : b ≤ c
h3 : d = c
⊢ b ≤ d
Module: Mathlib.Tactic.Ring.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b c d : α
h1 : a = b
h2 : b < c
h3 : d = c
⊢ a < d

Tactic:
h1,

Goal state after:
α : Type u_1
inst✝ : LT α
a b c d : α
h1 : a = b
h2 : b < c
h3 : d = c
⊢ b < d
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case inl
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h1 : ⨅ s, ⨅ (_ : span R s = p), s.encard = ⊤
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard = ⨅ s, ↑(↑s).card

Tactic:
h1,

Goal state after:
case inl
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h1 : ⨅ s, ⨅ (_ : span R s = p), s.encard = ⊤
⊢ ⊤ = ⨅ s, ↑(↑s).card
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
⊢ ∑ x ∈ univ.erase (Equiv.refl n), ↑↑(Equiv.Perm.sign x) * ∏ i, M.charmatrix (x i) i ∈ degreeLT R (Fintype.card n - 1)

Tactic:
apply Submodule.sum_mem (degreeLT R (Fintype.card n - 1))

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∀ c ∈ univ.erase (Equiv.refl n), ↑↑(Equiv.Perm.sign c) * ∏ i, M.charmatrix (c i) i ∈ degreeLT R (Fintype.card n - 1)
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
inst✝ : Subsingleton R
p : Submodule R M
⊢ p.spanFinrank = 0

Tactic:
by
  have := Module.subsingleton R M
  simp [Submodule.eq_bot_of_subsingleton]

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
p : Submodule R M
⊢ Cardinal.lift.{u, v} (map f p).spanRank ≤ Cardinal.lift.{v, u} p.spanRank

Tactic:
rw [← generators_card p, lift_spanRank_le_iff_exists_span_set_card_le]
  exact ⟨f '' p.generators, Cardinal.mk_image_le_lift, le_antisymm (span_le.2 (fun n ⟨m, hm, h⟩ ↦
    ⟨m, span_generators p ▸ subset_span hm, h⟩)) (by simp [span_generators])⟩

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R →+* T
I : Ideal R
r : R
hr : r ∈ I
⊢ f r ∈ map f (Submodule.span R (generators I))

Tactic:
span_generators

Goal state after:
R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R →+* T
I : Ideal R
r : R
hr : r ∈ I
⊢ f r ∈ map f I
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ∑ n_1 ∈ f.support, ((monomial (n_1 - k)) (↑(n_1.choose k) * f.coeff n_1)).coeff n =
    ↑((n + k).choose k) * f.coeff (n + k)

Tactic:
Finset.sum_eq_single (n + k),

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = ↑((n + k).choose k) * f.coeff (n + k)

case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ∀ b ∈ f.support, b ≠ n + k → ((monomial (b - k)) (↑(b.choose k) * f.coeff b)).coeff n = 0

case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ n + k ∉ f.support → ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
hk : 0 < k
⊢ (hasseDeriv k) 1 = 0

Tactic:
by
  rw [← C_1, hasseDeriv_C k _ hk]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ eval r (LinearMap.id f) = eval r f

Tactic:
LinearMap.id_apply

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ eval r f = eval r f
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ((taylor r) f).coeff ((taylor r) f).natDegree = f.coeff f.natDegree

Tactic:
natDegree_taylor,

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ((taylor r) f).coeff f.natDegree = f.coeff f.natDegree
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
p_ne_zero : p.coeff i ≠ 0
⊢ p.coeff i * s ^ (p.natDegree - i) ≠ 0

Tactic:
ps_zero

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
p_ne_zero : p.coeff i ≠ 0
ps_zero : p.coeff i * s ^ (p.natDegree - i) = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.scaleRoots 1 = p

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
⊢ scaleRoots 1 r = 1

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝ : CommSemiring R
m : M
r₁ : R
n : N
r₂ : R
⊢ (tensorEquiv R) (single m r₁ ⊗ₜ[R] single n r₂) = single (m, n) (r₁ * r₂)

Tactic:
by ext; simp

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

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

Tactic:
simp only [hf.eval_derivative, hf.eval_eq_prod_roots, ← Multiset.sum_map_mul_left, mul_assoc]

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
⊢ (Multiset.map (fun i ↦ f.leadingCoeff * (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase i)).prod) f.roots).sum =
    (Multiset.map (fun x_1 ↦ f.leadingCoeff * ((Multiset.map (fun x_2 ↦ x - x_2) f.roots).prod * (1 / (x - x_1))))
        f.roots).sum
Module: Mathlib.Algebra.Polynomial.Splits

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

Tactic:
mul_div_cancel_left₀ _ hx

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
⊢ (Multiset.map (fun z ↦ 1 / (x - z)) f.roots).sum = (Multiset.map (fun z ↦ 1 / (x - z)) f.roots).sum
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
inst✝¹ : Algebra.IsIntegral R S
x : S
this : ∀ r ∉ p, ∀ (c : S), c * x ≠ (algebraMap R S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint ↑Q ↑(Algebra.algebraMapSubmonoid S p.primeCompl)
hQp' : under R Q ≤ p
Q' : Ideal S
hQ'Q : Q' ≥ Q
hQ' : Q'.IsPrime
hQ'p : comap (algebraMap R S) Q' = p
inst✝ : Q'.IsPrime
hq : p.primesOver S = {Q'}
hx : x ∉ Q'
⊢ False

Tactic:
exact hx (hQ'Q (hxQ (Ideal.mem_span_singleton_self _)))

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ f ∈ ⨅ x ∈ t, x.asIdeal ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asIdeal}

Tactic:
Submodule.mem_iInf

Goal state after:
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ (∀ (i : PrimeSpectrum R), f ∈ ⨅ (_ : i ∈ t), i.asIdeal) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asIdeal}
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
x : PrimeSpectrum R
⊢ f ∈ ⨅ (_ : x ∈ t), x.asIdeal ↔ x ∈ t → f ∈ x.asIdeal

Tactic:
Submodule.mem_iInf

Goal state after:
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
x : PrimeSpectrum R
⊢ x ∈ t → f ∈ x.asIdeal ↔ x ∈ t → f ∈ x.asIdeal
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
s : S
a : A
ha : IsAlgebraic R a
inst✝ : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : (aeval a) p = 0
⊢ (algebraMap S (TensorProduct R S A)).comp (algebraMap R S) =
    (↑Algebra.TensorProduct.includeRight).comp (algebraMap R A)

Tactic:
by ext; simp

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
inst✝ : FaithfulSMul R S
⊢ (∀ (x : A), IsAlgebraic R x) ↔ ∀ (x : A), IsAlgebraic S x

Tactic:
Algebra.IsAlgebraic.isAlgebraic_iff R S

Goal state after:
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
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
hy : (algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)
⊢ ((algebraMap K L) ((algebraMap R K) z))⁻¹ * ((algebraMap S L) a * (algebraMap S L) y) ∈
    ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
← map_inv₀,

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
hy : (algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)
⊢ (algebraMap K L) ((algebraMap R K) z)⁻¹ * ((algebraMap S L) a * (algebraMap S L) y) ∈
    ↑(Submodule.span K (⇑(algebraMap S L) '' b))
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
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
hy : (algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)
⊢ (algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
rw [mk_yz_eq, IsFractionRing.mk'_eq_div, ← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R K L, div_eq_mul_inv, ← mul_assoc, mul_comm, ← map_inv₀, ←
      Algebra.smul_def, ← map_mul]

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
hy : (algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)
⊢ ((algebraMap R K) z)⁻¹ • (algebraMap S L) (a * y) ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
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)
⊢ Flat R M

Tactic:
by
  rw [Module.Flat.iff_lTensor_preserves_injective_linearMap]
  intro N P _ _ _ _ f hf
  have : Flat R (S ⊗[R] M) := Flat.trans _ S _
  rw [← FaithfullyFlat.lTensor_injective_iff_injective R S]
  have : LinearMap.lTensor S (LinearMap.lTensor M f) =
      (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ LinearMap.lTensor (S ⊗[R] M) f ∘ₗ
        (TensorProduct.assoc _ _ _ _).symm.toLinearMap := by
    ext
    simp
  simpa [this] using Flat.lTensor_preserves_injective_linearMap f hf

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
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
⊢ (algebraMap S (S ⊗[R] T)).SurjectiveOnStalks

Tactic:
let g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
  intro J hJ
  rw [surjective_localRingHom_iff]
  intro x
  obtain ⟨t, r, a, ht, e⟩ := hf.exists_mul_eq_tmul x (J.comap g) inferInstance
  refine ⟨a, algebraMap _ _ r, 1 ⊗ₜ (r • t), ht, ?_, ?_⟩
  · intro H
    simp only [Algebra.algebraMap_eq_smul_one (A := S), Algebra.TensorProduct.algebraMap_apply,
      Algebra.algebraMap_self, id_apply, smul_tmul, ← Algebra.algebraMap_eq_smul_one (A := T)] at H
    rw [Ideal.mem_comap, Algebra.smul_def, g.map_mul] at ht
    exact ht (J.mul_mem_right _ H)
  · simp only [tmul_smul, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self,
      RingHomCompTriple.comp_apply, Algebra.smul_mul_assoc, Algebra.TensorProduct.tmul_mul_tmul,
      one_mul, mul_one, id_apply, ← e]
    rw [Algebra.algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
inst✝ : I.IsPrime
⊢ mapₐ I I (AlgHom.id R A) ⋯ = AlgHom.id R I.ResidueField

Tactic:
by ext; simp

Goal state after: