mathlib-initiative/mathlib-tactics huggingface dataset:
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
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
⊢ M.charpoly.reverse = M.charpolyRev

Tactic:
have hp : toLaurentAlg M.charpoly = p := by
    simp [p, t, charpoly, charmatrix, AlgHom.map_det, map_sub]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
hp : toLaurentAlg M.charpoly = p
⊢ M.charpoly.reverse = M.charpolyRev
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this✝ : Algebra R S := f.toAlgebra
this : (Subalgebra.toSubmodule R[x, y]).FG
⊢ f.IsIntegralElem z

Tactic:
exact
    IsIntegral.of_mem_of_fg (Algebra.adjoin R {x, y}) this z
      (Algebra.mem_adjoin_iff.2 <| Subring.closure_mono Set.subset_union_right hz)

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

Goal state before:
pp: B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ (algebraMap R S) r • x ∈ S[x]

Tactic:
apply Subalgebra.smul_mem

Goal state after:
B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ x ∈ S[x]
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
hil : l ≤ i
⊢ (i - l).choose k * i.choose l = 0

Tactic:
← tsub_lt_iff_right hil

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
⊢ (i - l).choose k * i.choose l = 0
Module: Mathlib.Algebra.Polynomial.Taylor

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

Tactic:
by
  by_cases hp : p = 0
  · rw [hp, map_zero]
  · rw [degree_eq_natDegree hp, degree_eq_iff_natDegree_eq ((taylor_eq_zero r p).not.2 hp),
      natDegree_taylor]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
h : n ≤ (p * q).natDegree
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)

Tactic:
rw [mul_comm, mul_assoc, ← pow_add, add_comm, tsub_add_tsub_cancel natDegree_mul_le h]

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

Goal state before:
pp: R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
s : S
p : MvPolynomial σ N
d : σ →₀ ℕ
⊢ coeff d (rTensorAlgEquiv (s ⊗ₜ[R] p)) = s ⊗ₜ[R] coeff d p

Tactic:
simp [rTensorAlgEquiv, coeff, MvPolynomial, ← tmul_eq_smul_one_tmul]

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

Goal state before:
pp: case refine_1
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
⊢ (Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
          (mapAlgHom M includeRight) ⋯).comp
      rTensorEquivAlgEquiv.invFun =
    AlgHom.id A (A ⊗[R] B)[M]

pp: case refine_2
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
⊢ rTensorEquivAlgEquiv.invFun.comp
      (Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
        (mapAlgHom M includeRight) ⋯) =
    AlgHom.id A (A ⊗[R] B[M])

Tactic:
· apply AlgHom.toLinearMap_injective
    ext
    simp

Goal state after:
case refine_2
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
⊢ rTensorEquivAlgEquiv.invFun.comp
      (Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
        (mapAlgHom M includeRight) ⋯) =
    AlgHom.id A (A ⊗[R] B[M])
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_2
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
a : A
p : B[M]
⊢ (rTensorEquivAlgEquiv R S A B) (a ⊗ₜ[R] p) = a • (mapAlgHom M includeRight) p

Tactic:
simp [rTensorEquivAlgEquiv, Algebra.smul_def]

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
⊢ f.coeff 0 = (-1) ^ f.natDegree * f.leadingCoeff * f.roots.prod

Tactic:
by
  conv_lhs => rw [hf.eq_prod_roots]
  simp [coeff_zero_eq_eval_zero, eval_multiset_prod, hf.natDegree_eq_card_roots,
    mul_assoc, mul_left_comm]

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✝⁵ : Ring B
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R ↑p.coeffs
this : Module.Finite R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
⊢ IsIntegral R x

Tactic:
have hSx : IsIntegral S x := ⟨p', (p.monic_toSubring _ _).mpr pmonic, by
    rw [IsScalarTower.algebraMap_eq S A B, ← eval₂_map]
    convert! hp; apply p.map_toSubring S.toSubring⟩

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Ring B
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R ↑p.coeffs
this : Module.Finite R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
hSx : IsIntegral (↥S) x
⊢ IsIntegral R x
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ (Ideal.quotientMap I f ⋯).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f).IsIntegral

Tactic:
by
  let g := Ideal.Quotient.mk (I.comap f)
  -- Porting note: added type ascription
  have : (Ideal.quotientMap I f le_rfl).comp g = (Ideal.Quotient.mk I).comp f :=
    Ideal.quotientMap_comp_mk le_rfl
  refine ⟨fun h => ?_, fun h => RingHom.IsIntegral.tower_top g _ (this ▸ h)⟩
  refine this ▸ RingHom.IsIntegral.trans g (Ideal.quotientMap I f le_rfl) ?_ h
  exact g.isIntegral_of_surjective Ideal.Quotient.mk_surjective

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

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
⊢ f.Splits

Tactic:
have h : (f /ₘ (X - C x)).natDegree = 1 := by
    rw [natDegree_divByMonic f (monic_X_sub_C x), h₁, natDegree_X_sub_C]
  rw [← mul_divByMonic_eq_iff_isRoot.mpr h₂, splits_mul (X_sub_C_ne_zero x) (by aesop)]
  exact ⟨Splits.X_sub_C x, Splits.of_natDegree_eq_one h⟩

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
hf0 : ¬f = 0
u : R[X]ˣ
hu : (factors f).prod * ↑u = f
⊢ f.Splits

Tactic:
← hu

Goal state after:
case neg
R : Type u_1
inst✝ : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
hf0 : ¬f = 0
u : R[X]ˣ
hu : (factors f).prod * ↑u = f
⊢ ((factors f).prod * ↑u).Splits
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
coeff_eq_zero : p.coeff 0 = 0
a_ne_zero : a ≠ 0
⊢ (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
    p + C a ≠ 0 → eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
coeff_eq_zero : p.coeff 0 = 0
a_ne_zero : a ≠ 0
a✝ : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
⊢ p + C a ≠ 0 → eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
coeff_eq_zero : p.coeff 0 = 0
a_ne_zero : a ≠ 0
a✝ : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
⊢ p + C a ≠ 0 → eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
coeff_eq_zero : p.coeff 0 = 0
a_ne_zero : a ≠ 0
a✝¹ : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p + C a ≠ 0
⊢ eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_3
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
⊢ p * X ≠ 0 → eval₂ f r (p * X) = 0 → ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I

Tactic:
_

Goal state after:
case refine_3
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p * X ≠ 0
⊢ eval₂ f r (p * X) = 0 → ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_3
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ ∀ (p : R[X]),
    p ≠ 0 →
      (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
        p * X ≠ 0 → eval₂ f r (p * X) = 0 → ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I

Tactic:
intro p p_nonzero ih _ hp

Goal state after:
case refine_3
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p * X ≠ 0
hp : eval₂ f r (p * X) = 0
⊢ ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
⊢ ∃ y, y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)

Tactic:
have := Algebra.IsAlgebraic.nontrivial R A

Goal state after:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
⊢ ∃ y, y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
B : Type u_2
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
hpm : p.IsMaximal
inst✝ : P.IsPrime
⊢ P.IsMaximal

Tactic:
by
  rw [P.over_def p] at hpm
  exact isMaximal_of_isIntegral_of_isMaximal_comap P hpm

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ s ⊆ ∅ ↔ s = ∅

Tactic:
Set.subset_empty_iff

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ s = ∅ ↔ s = ∅
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
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.rTensor M f = 0
m : M
n : N
⊢ (TensorProduct.comm R M N') (((AlgebraTensorModule.curry (LinearMap.lTensor M f)) m) n) =
    (TensorProduct.comm R M N') (((AlgebraTensorModule.curry 0) m) n)

Tactic:
simpa using congr($h (n ⊗ₜ m))

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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst✝ : NoZeroDivisors S
⊢ Algebra.IsAlgebraic R[X] S[X]

Tactic:
by_cases h : Function.Injective (algebraMap R S)
  · have := h.noZeroDivisors _ (map_zero _) (map_mul _); infer_instance
  rw [← Polynomial.map_injective_iff] at h
  exact Algebra.isAlgebraic_of_not_injective h

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝¹ : IsDomain S
inst✝ : FaithfulSMul R S
this : IsDomain R
⊢ Module.rank (FractionRing R[X]) (FractionRing S[X]) = Module.rank R S

Tactic:
rw [rank_fractionRing, rank_polynomial_polynomial]

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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfullyFlat R S
inst✝ : Flat S (S ⊗[R] M)
N P : Type (max u v)
⊢ ∀ [inst : AddCommGroup N] [inst_1 : AddCommGroup P] [inst_2 : Module R N] [inst_3 : Module R P] (f : N →ₗ[R] P),
    Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)

Tactic:
_

Goal state after:
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)
N P : Type (max u v)
inst✝ : AddCommGroup N
⊢ ∀ [inst : AddCommGroup P] [inst_1 : Module R N] [inst_2 : Module R P] (f : N →ₗ[R] P),
    Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)
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)
N P : Type (max u v)
inst✝ : AddCommGroup N
⊢ ∀ [inst : AddCommGroup P] [inst_1 : Module R N] [inst_2 : Module R P] (f : N →ₗ[R] P),
    Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)

Tactic:
_

Goal state after:
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)
N P : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : AddCommGroup P
⊢ ∀ [inst : Module R N] [inst_1 : Module R P] (f : N →ₗ[R] P),
    Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)
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)
N P : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : AddCommGroup P
⊢ ∀ [inst : Module R N] [inst_1 : Module R P] (f : N →ₗ[R] P),
    Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)

Tactic:
_

Goal state after:
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)
N P : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : AddCommGroup P
inst✝ : Module R N
⊢ ∀ [inst : Module R P] (f : N →ₗ[R] P), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)
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)
N P : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : AddCommGroup P
inst✝ : Module R N
⊢ ∀ [inst : Module R P] (f : N →ₗ[R] P), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)

Tactic:
_

Goal state after:
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)
N P : Type (max u v)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
⊢ ∀ (f : N →ₗ[R] P), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)
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
⊢ p ≤ q.mkQ.ker

Tactic:
le_ker_iff_comp_subtype_eq_zero,

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
⊢ q.mkQ ∘ₗ 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 ⧸ I
e : (algebraMap (R ⧸ I) I.ResidueField) x = (algebraMap (R ⧸ I) I.ResidueField) y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y
    rw [← sub_eq_zero, ← map_sub, ← map_sub] at e
    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
    use 1
    simp [e]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
h : ∀ I ∈ minimalPrimes R, I.IsMaximal
I : Ideal R
hI : I.IsPrime
J : Ideal R
hJ : J ∈ ⊥.minimalPrimes
hle : J ≤ I
⊢ I.IsMaximal

Tactic:
exact (h J hJ).eq_of_le hI.ne_top hle ▸ h J hJ

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : PrimeSpectrum R
⊢ Set.range (comap (algebraMap R I.asIdeal.ResidueField)) = {I}

Tactic:
rw [Set.range_unique, Set.singleton_eq_singleton_iff]
  exact PrimeSpectrum.ext (Ideal.ext fun x ↦ Ideal.algebraMap_residueField_eq_zero)

Goal state after:
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✝ : α
⊢ ∀ (b c : α), le a✝ b → le b c → le a✝ c

Tactic:
_

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ ∀ (c : α), le a✝ b✝ → le b✝ c → le a✝ c
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✝ b✝ : α
⊢ ∀ (c : α), le a✝ b✝ → le b✝ c → le a✝ c

Tactic:
_

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
⊢ le a✝ b✝ → le b✝ c✝ → le a✝ c✝
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✝ : α
⊢ ∀ (b : α), le a✝ b → le b a✝ → a✝ = b

Tactic:
_

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ le a✝ b✝ → le b✝ a✝ → a✝ = b✝
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✝ : α
⊢ ∀ (b c : α), le a✝ c → le b c → le (sup a✝ b) c

Tactic:
_

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ ∀ (c : α), le a✝ c → le b✝ c → le (sup a✝ b✝) c
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✝ b✝ : α
⊢ ∀ (c : α), le a✝ c → le b✝ c → le (sup a✝ b✝) c

Tactic:
_

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
⊢ le a✝ c✝ → le b✝ c✝ → le (sup a✝ b✝) c✝
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✝ : α
⊢ ∀ (b c : α), le a✝ b → le a✝ c → le a✝ (inf b c)

Tactic:
_

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