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

Goal state before:
pp: case neg.inr.hnc
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ ¬n ≤ ↑i

Tactic:
· simpa only [hni.symm, not_le, or_false] using! Nat.lt_succ_iff_lt_or_eq.1 hi

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ L₀ L₀' D₀, (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod
M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁
L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)
D₀ : Fin r → 𝕜
h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀
c : 𝕜 := M' (inr ()) (inr ())
⊢ (List.map toMatrix (List.map (sumInl Unit) L₀ ++ L₁)).prod * M *
      (List.map toMatrix (L₁' ++ List.map (sumInl Unit) L₀')).prod =
    diagonal (Sum.elim D₀ fun x ↦ M' (inr ()) (inr ()))

Tactic:
suffices (L₀.map (toMatrix ∘ sumInl Unit)).prod * M' * (L₀'.map (toMatrix ∘ sumInl Unit)).prod =
      diagonal (Sum.elim D₀ fun _ => c) by
    simpa [M', c, Matrix.mul_assoc]

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ L₀ L₀' D₀, (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod
M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁
L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)
D₀ : Fin r → 𝕜
h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀
c : 𝕜 := M' (inr ()) (inr ())
⊢ (List.map (toMatrix ∘ sumInl Unit) L₀).prod * M' * (List.map (toMatrix ∘ sumInl Unit) L₀').prod =
    diagonal (Sum.elim D₀ fun x ↦ c)
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
h : eval M (matPolyEquiv (M.charpoly • 1)) = 0
⊢ (aeval M) M.charpoly = 0

Tactic:
rw [matPolyEquiv_smul_one, eval_map] at h

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval₂ (algebraMap R (Matrix n n R)) M M.charpoly = 0
⊢ (aeval M) M.charpoly = 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 : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
⊢ (evalRingHom 0).mapMatrix.comp ↑(compRingEquiv m n R[X]) =
    (compRingEquiv m n R).toRingHom.comp (evalRingHom 0).mapMatrix.mapMatrix

Tactic:
ext; simp

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 n α
B : Matrix n m α
⊢ (A * B + 1).det = (B * A + 1).det

Tactic:
by rw [add_comm, det_one_add_mul_comm, add_comm]

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 ι
⊢ ((LinearMap.llcomp R (ι → R) (ι → R) M) (Fintype.linearCombination R b)) (algEquivMatrix'.symm 1) =
    (PiToModule.fromEnd R b) 1

Tactic:
map_one

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 ι
⊢ ((LinearMap.llcomp R (ι → R) (ι → R) M) (Fintype.linearCombination R b)) 1 = (PiToModule.fromEnd R b) 1
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Subsingleton R
⊢ Monic 0 ∧ natDegree 0 = ⊤.spanFinrank ∧ (∀ (k : ℕ), coeff 0 k ∈ I ^ (natDegree 0 - k)) ∧ (aeval f) 0 = 0

Tactic:
simp [nontriviality]

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
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ s.encard = ↑p.spanFinrank

Tactic:
rw [Set.encard, ENat.card, spanFinrank, hs₁, this]

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ toENat ↑p.spanFinrank = ↑(toNat ↑p.spanFinrank)
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.spanRank = 0

Tactic:
simp [nontriviality]

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
h : p.FG
heq : p.spanFinrank = 0
⊢ p = ⊥

Tactic:
← Submodule.FG.generators_ncard h,

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
heq : p.generators.ncard = 0
⊢ p = ⊥
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
this✝ : p.coeff p.natDegree ≠ 0
this : (p.scaleRoots s).coeff p.natDegree = 0
⊢ False

Tactic:
rw [coeff_scaleRoots_natDegree] at this

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
this✝ : p.coeff p.natDegree ≠ 0
this : p.leadingCoeff = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r c : R
⊢ (C c).scaleRoots r = C c

Tactic:
ext; simp

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

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

Tactic:
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:
ext; simp

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

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
⊢ f (p.coeff i) * f s ^ (p.natDegree - i) * (f s * a) ^ i = f (p.coeff i) * (f s ^ (p.natDegree - i) * f s ^ i) * a ^ i

Tactic:
hsa.mul_pow,

Goal state after:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
⊢ f (p.coeff i) * f s ^ (p.natDegree - i) * (f s ^ i * a ^ i) =
    f (p.coeff i) * (f s ^ (p.natDegree - i) * f s ^ i) * a ^ i
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

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

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

Tactic:
· clear hm
    refine .mul (.C _) ?_
    induction m using Multiset.induction_on with
    | empty => simp
    | cons a s IH =>
      rw [Multiset.map_cons, Multiset.prod_cons, mul_scaleRoots', X_add_C_scaleRoots]
      · exact .mul (.X_add_C _) IH
      · simp only [leadingCoeff_X_add_C, one_mul, ne_eq, leadingCoeff_eq_zero]
        exact (monic_multiset_prod_of_monic _ _ fun a _ ↦ monic_X_add_C _).ne_zero

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ∀ f ∈ Multiset.map (fun x ↦ X + C x) m, f.Splits

Tactic:
by simp [Splits.X_add_C]

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

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : CommSemiring A
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : Algebra S B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : IsPushout R S A B
⊢ ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] 0) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap 0

Tactic:
simp_all [IsPushout.equiv_tmul]

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

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : CommSemiring A
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : Algebra S B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : IsPushout R S A B
x✝ y✝ : A[M]
a✝¹ :
  ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] x✝) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap x✝
a✝ :
  ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] y✝) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap y✝
⊢ ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] (x✝ + y✝)) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap (x✝ + y✝)

Tactic:
simp_all [IsPushout.equiv_tmul]

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

Goal state before:
pp: case single
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : CommSemiring A
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : Algebra S B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : IsPushout R S A B
m✝ : M
r✝ : A
⊢ ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] single m✝ r✝) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap (single m✝ r✝)

Tactic:
simp_all [IsPushout.equiv_tmul]

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:
ext; simp

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
hf : f.Splits
hm : f.Monic
S : Type u_4
inst✝ : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, a ∈ i.range
⊢ f ∈ lifts i

Tactic:
rw [hf.eq_prod_roots_of_monic hm, lifts_iff_liftsRing]

Goal state after:
R : Type u_1
inst✝² : CommRing R
f : R[X]
inst✝¹ : IsDomain R
hf : f.Splits
hm : f.Monic
S : Type u_4
inst✝ : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, a ∈ i.range
⊢ (Multiset.map (fun x ↦ X - C x) f.roots).prod ∈ liftsRing i
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Sort u_5
S : ι → Subalgebra R A
⊢ Algebra.IsIntegral R ↥(iSup S) ↔ ∀ (i : ι), Algebra.IsIntegral R ↥(S i)

Tactic:
by
  simp_rw [← le_integralClosure_iff_isIntegral, iSup_le_iff]

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

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ ∑ x ∈ Finset.range (g'.natDegree + 1), (Ideal.Quotient.mkₐ S I) (C (g'.coeff x) * X ^ x) =
    ∑ i ∈ Finset.range (g'.natDegree + 1), g'.coeff i • (Ideal.Quotient.mkₐ S I) X ^ i

Tactic:
simp only [Polynomial.C_mul', ← map_pow, map_smul]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
h : IsIntegral R 1
⊢ 1 = (algebraMap A B) 1

Tactic:
map_one

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
h : IsIntegral R 1
⊢ 1 = 1
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:
ext; simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
⊢ vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t')

Tactic:
intro r
  rw [Submodule.mem_sup, mem_vanishingIdeal]
  rintro ⟨f, hf, g, hg, rfl⟩ x ⟨hxt, hxt'⟩
  rw [mem_vanishingIdeal] at hf hg
  apply Submodule.add_mem <;> solve_by_elim

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.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑f

Tactic:
by
  rw [← LinearMap.exact_zero_iff_injective (M ⊗[R] Unit), ← LinearMap.exact_zero_iff_injective Unit]
  conv_rhs => rw [← lTensor_exact_iff_exact R M]
  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 S A
inst✝ : NoZeroDivisors S
s t : Set S
alg : ∀ x ∈ s \ t, IsAlgebraic (↥(adjoin R t)) x
a : A
ha : IsAlgebraic (↥(adjoin R s)) a
⊢ IsAlgebraic (↥(adjoin R t)) a

Tactic:
by
  set Rs := adjoin R s
  set Rt := adjoin R t
  let Rts := adjoin Rt s
  let _ : Algebra Rs Rts := (Subalgebra.inclusion
    (T := Rts.restrictScalars R) <| adjoin_le <| by apply subset_adjoin).toAlgebra
  have : IsScalarTower Rs Rts A := .of_algebraMap_eq fun ⟨a, _⟩ ↦ rfl
  have : Algebra.IsAlgebraic Rt Rts := by
    have := ha.nontrivial
    have := Subtype.val_injective (p := (· ∈ Rs)).nontrivial
    have := (isDomain_iff_noZeroDivisors_and_nontrivial Rt).mpr ⟨inferInstance, inferInstance⟩
    rw [← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]
    intro x hs
    by_cases ht : x ∈ t
    · exact isAlgebraic_algebraMap (⟨x, subset_adjoin ht⟩ : Rt)
    exact alg _ ⟨hs, ht⟩
  have : IsAlgebraic Rts a := ha.extendScalars (by apply Subalgebra.inclusion_injective)
  exact this.restrictScalars Rt

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
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
⊢ 1 ⊗ₜ[R] m = 0 ↔ m = 0

Tactic:
constructor; swap
  · rintro rfl; rw [tmul_zero]
  intro h
  let f : R →ₗ[R] M := (LinearMap.lsmul R M).flip m
  suffices f = 0 by simpa [f] using DFunLike.congr_fun this 1
  rw [Module.FaithfullyFlat.zero_iff_lTensor_zero R A]
  ext a
  apply_fun (a • ·) at h
  rw [smul_zero, smul_tmul', smul_eq_mul, mul_one] at h
  simpa [f]

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 S L) a * mk' L y' z' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
mk_yz_eq,

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 S L) a * mk' L y ⟨(algebraMap R S) z, hz0'⟩ ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FaithfullyFlat R A
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
h : baseChange A p ≤ baseChange A q
⊢ lTensor A (q.mkQ ∘ₗ p.subtype) = 0

Tactic:
lTensor_comp,

Goal state after:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FaithfullyFlat R A
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
h : baseChange A p ≤ baseChange A q
⊢ lTensor A q.mkQ ∘ₗ lTensor A p.subtype = 0
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
I : Ideal R
inst✝ : I.IsPrime
x y : R
e : (algebraMap (R ⧸ I) I.ResidueField) ((Ideal.Quotient.mk I) (x - y)) = 0
⊢ ∃ c, ↑c * (Ideal.Quotient.mk I) x = ↑c * (Ideal.Quotient.mk I) y

Tactic:
simp only [IsLocalRing.ResidueField.algebraMap_eq, IsLocalRing.residue_eq_zero_iff,
      IsScalarTower.algebraMap_apply R (Localization.AtPrime I) I.ResidueField,
      Ideal.algebraMap_quotient_residueField_mk, IsLocalization.AtPrime.to_map_mem_maximal_iff _ I,
      ← Ideal.Quotient.mk_eq_mk_iff_sub_mem] at e

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
I : Ideal R
inst✝ : I.IsPrime
x y : R
e : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ ∃ c, ↑c * (Ideal.Quotient.mk I) x = ↑c * (Ideal.Quotient.mk I) y
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:
ext; simp

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

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Subsingleton R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

pp: case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
· exact iff_of_true inferInstance fun I h ↦ (h <| Subsingleton.elim ..).elim

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
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
I : Ideal R
hI : ker f = I
a b : PrimeSpectrum S
⊢ comap f a.asIdeal ≤ comap f b.asIdeal ↔ a ≤ b

Tactic:
← Ideal.map_le_iff_le_comap,

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal R
hI : ker f = I
a b : PrimeSpectrum S
⊢ map f (comap f a.asIdeal) ≤ b.asIdeal ↔ a ≤ b
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_5
inst✝ : Finite ι
U : ι → Opens α
⊢ ↑(⨅ i, U i) = ⋂ i, ↑(U i)

Tactic:
induction ι using Finite.induction_empty_option with

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
⊢ ∀ (x : Closeds α),
    (∀ y < x, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S) →
      ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ x = sSup S

Tactic:
intro s H

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
⊢ ↑(⨅ i, s i) = ⋂ i, ↑(s i)

Tactic:
ext; simp

Goal state after: