mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s // span R s = span R (Set.range v) }
this : #↑↑x = #↑(Subtype.val ⁻¹' ↑x)
⊢ span R (Subtype.val ⁻¹' ↑x) = ⊤

Tactic:
apply map_injective_of_injective (f := (span R _).subtype) (injective_subtype _)

Goal state after:
case refine_2
R : Type u_1
M : Type u
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s // span R s = span R (Set.range v) }
this : #↑↑x = #↑(Subtype.val ⁻¹' ↑x)
⊢ map (span R (Set.range v)).subtype (span R (Subtype.val ⁻¹' ↑x)) = map (span R (Set.range v)).subtype ⊤
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
⊢ (M.charpoly - ∏ i, (X - C (M i i))).degree < ↑(Fintype.card n - 1)

Tactic:
rw [charpoly, det_apply', ← insert_erase (mem_univ (Equiv.refl n)),
    sum_insert (notMem_erase (Equiv.refl n) univ), add_comm]
  simp only [charmatrix_apply_eq, one_mul, Equiv.Perm.sign_refl, id, Int.cast_one,
    Units.val_one, add_sub_cancel_right, Equiv.coe_refl]
  rw [← mem_degreeLT]
  apply Submodule.sum_mem (degreeLT R (Fintype.card n - 1))
  intro c hc; rw [← C_eq_intCast, C_mul']
  apply Submodule.smul_mem (degreeLT R (Fintype.card n - 1)) ↑↑(Equiv.Perm.sign c)
  rw [mem_degreeLT]
  apply lt_of_le_of_lt degree_le_natDegree _
  rw [Nat.cast_lt]
  apply lt_of_le_of_lt _ (Equiv.Perm.fixed_point_card_lt_of_ne_one (ne_of_mem_erase hc))
  apply le_trans (Polynomial.natDegree_prod_le univ fun i : n => charmatrix M (c i) i) _
  rw [card_eq_sum_ones]; rw [sum_filter]; apply sum_le_sum
  intros
  apply charmatrix_apply_natDegree_le

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

Goal state before:
pp: case succ.h₀
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i : Fin n.succ
a✝ : i ∈ univ
⊢ i ≠ 0 →
    (eval 0 (derivative ((-1) ^ ↑i)) * eval 0 (1 0 i) + (-1) ^ ↑i * (eval 0 (derivative (1 0 i)) + M 0 i)) *
          eval 0 (submatrix 1 Fin.succ i.succAbove).det +
        (-1) ^ ↑i * eval 0 (1 0 i) *
          eval 0 (derivative (submatrix 1 Fin.succ i.succAbove + X • (M.submatrix Fin.succ i.succAbove).map ⇑C).det) =
      0

Tactic:
hi

Goal state after:
case succ.h₀
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i : Fin n.succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ (eval 0 (derivative ((-1) ^ ↑i)) * eval 0 (1 0 i) + (-1) ^ ↑i * (eval 0 (derivative (1 0 i)) + M 0 i)) *
        eval 0 (submatrix 1 Fin.succ i.succAbove).det +
      (-1) ^ ↑i * eval 0 (1 0 i) *
        eval 0 (derivative (submatrix 1 Fin.succ i.succAbove + X • (M.submatrix Fin.succ i.succAbove).map ⇑C).det) =
    0
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
j : Fin (n + 1)
⊢ 1 j.succ (i.succAbove 0) = 0

Tactic:
Fin.succAbove_of_castSucc_lt,

Goal state after:
case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
j : Fin (n + 1)
⊢ 1 j.succ (Fin.castSucc 0) = 0

case succ.h₀.succ.h
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
j : Fin (n + 1)
⊢ Fin.castSucc 0 < i
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : CommRing T
inst✝² : Ring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
⊢ ψ (eval₂ (algebraMap R S) a p) = 0

Tactic:
hp.2,

Goal state after:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : CommRing T
inst✝² : Ring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
⊢ ψ 0 = 0
Module: Mathlib.Algebra.Polynomial.Eval.Subring

Goal state before:
pp: case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : f c = p.coeff i
⊢ (mapRingHom f) (C c * X ^ i) = C (p.coeff i) * X ^ i

Tactic:
rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace

Tactic:
rw [det_succ_row_zero, map_sum, eval_finsetSum]
    simp only [add_apply, smul_apply, map_apply, smul_eq_mul, X_mul_C, submatrix_add,
      submatrix_smul, Pi.add_apply, Pi.smul_apply, submatrix_map, derivative_mul, map_add,
      derivative_C, zero_mul, derivative_X, mul_one, zero_add, eval_add, eval_mul, eval_C, eval_X,
      mul_zero, add_zero, eval_det_add_X_smul, eval_pow, eval_neg, eval_one]
    rw [Finset.sum_eq_single 0]
    · simp only [Fin.val_zero, pow_zero, derivative_one, eval_zero, one_apply_eq, eval_one,
        mul_one, zero_add, one_mul, Fin.succAbove_zero, submatrix_one _ (Fin.succ_injective _),
        det_one, IH, trace_submatrix_succ]
    · intro i _ hi
      cases n with
      | zero => exact (hi (Subsingleton.elim i 0)).elim
      | succ n =>
        simp only [one_apply_ne' hi, eval_zero, mul_zero, zero_add, zero_mul, add_zero]
        rw [det_eq_zero_of_column_eq_zero 0, eval_zero, mul_zero]
        intro j
        rw [submatrix_apply, Fin.succAbove_of_castSucc_lt, one_apply_ne]
        · exact (bne_iff_ne (a := Fin.succ j) (b := Fin.castSucc 0)).mp rfl
        · rw [Fin.castSucc_zero]; exact lt_of_le_of_ne (Fin.zero_le _) hi.symm
    · exact fun H ↦ (H <| Finset.mem_univ _).elim

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
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
⊢ (detRowAlternating (1 + X • M.map ⇑C)).coeff k =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)

Tactic:
rw [add_comm]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
⊢ (detRowAlternating (X • M.map ⇑C + 1)).coeff k =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (k + l) = i - l - k

Tactic:
rw [add_comm]

Goal state after:
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (l + k) = i - l - k
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
k : ℕ
⊢ ((taylor r) f).coeff k = coeff 0 k

Tactic:
rw [taylor_coeff, h, coeff_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ integralNormalization 0 = 0

Tactic:
simp [integralNormalization]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = p.coeff n

pp: case neg
R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
h : ¬p.coeff n = 0
⊢ ↑⟨p.coeff n, ⋯⟩ = p.coeff n

Tactic:
· rw [h]
    rfl

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
h : ¬p.coeff n = 0
⊢ ↑⟨p.coeff n, ⋯⟩ = p.coeff n
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
⊢ i ∈ ↑(ofSubring T p).coeffs → i ∈ ↑T

Tactic:
hi

Goal state after:
R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
hi : i ∈ ↑(ofSubring T p).coeffs
⊢ i ∈ ↑T
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
⊢ mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)

Tactic:
simp [Multiset.map_congr rfl hj]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg✝ : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
a : R
⊢ ((X + C a).comp g).Splits

Tactic:
apply of_natDegree_le_one_of_invertible (by simpa)

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg✝ : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
a : R
⊢ Invertible ((X + C a).comp g).leadingCoeff
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hR : IsField R
x : S
hx : x ≠ 0
⊢ ∃ b, x * b = 1

Tactic:
by
    let := hR.toField
    obtain ⟨y, rfl⟩ := (Algebra.IsIntegral.isIntegral (R := R) x).isUnit hx
    exact ⟨y.inv, y.val_inv⟩

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

Goal state before:
pp: case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
use integralNormalization p

Goal state after:
case h
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
⊢ p.integralNormalization.Monic ∧ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = 0
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
R' : Type u_3
inst✝³ : CommRing R'
inst✝² : Algebra R R'
inst✝¹ : Algebra S R'
inst✝ : IsScalarTower R S R'
p : S[X]
x : R'
hx : (aeval x) p = 0
⊢ eval₂ ((algebraMap S R').comp (algebraMap R S)) x (integerNormalization M p) = 0

Tactic:
integerNormalization_eval₂_eq_zero

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
R' : Type u_3
inst✝³ : CommRing R'
inst✝² : Algebra R R'
inst✝¹ : Algebra S R'
inst✝ : IsScalarTower R S R'
p : S[X]
x : R'
hx : (aeval x) p = 0
⊢ 0 = 0

case hx
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
R' : Type u_3
inst✝³ : CommRing R'
inst✝² : Algebra R R'
inst✝¹ : Algebra S R'
inst✝ : IsScalarTower R S R'
p : S[X]
x : R'
hx : (aeval x) p = 0
⊢ eval₂ (algebraMap S R') x p = 0
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
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
hu : u ∈ Algebra.algebraMapSubmonoid S M
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, hu⟩).2 = (algebraMap S Sₘ) (s, ⟨u, hu⟩).1
⊢ (IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegralElem x

Tactic:
obtain ⟨v, hv⟩ := hu

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
⊢ (IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegralElem x
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
⊢ (algebraMap A B) (mk' A 1 h) = (algebraMap A B) 1

Tactic:
rw [algebraMap_mk', map_one]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
hf : f.Splits
hf0 : f ≠ 0
i : R →+* S
x : S
hx : (map i f).IsRoot x
⊢ x ∈ i.range

Tactic:
← mem_roots (map_ne_zero hf0),

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
hf : f.Splits
hf0 : f ≠ 0
i : R →+* S
x : S
hx : x ∈ (map i f).roots
⊢ x ∈ i.range
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra R B
f : R[X]
hf : (map (algebraMap R A) f).Splits
g : A →ₐ[R] B
⊢ ↑(Multiset.map (⇑↑g) (f.aroots A)).toFinset = f.rootSet B

Tactic:
← hf.roots_map,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra R B
f : R[X]
hf : (map (algebraMap R A) f).Splits
g : A →ₐ[R] B
⊢ ↑(map (↑g) (map (algebraMap R A) f)).roots.toFinset = f.rootSet B
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
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap (Quotient.mk (comap (algebraMap R S) I)) (map (Quotient.mk (comap (algebraMap R S) I)) P) = P

Tactic:
refine _root_.trans (comap_map_of_surjective _ Quotient.mk_surjective _) (sup_eq_left.2 ?_)

Goal state after:
case refine_2
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap (Quotient.mk (comap (algebraMap R S) I)) ⊥ ≤ P
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
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
⊢ False

Tactic:
have eq0 : (⊤ : Submodule R (E ⊗[R] M)) = ⊥ := by
    -- suppose `x ∈ E ⊗ M`. We will show `x = 0`.
    ext x
    simp only [Submodule.mem_top, Submodule.mem_bot, true_iff]
    have mem : x ∈ (⊤ : Submodule R _) := ⟨⟩
    rw [← TensorProduct.span_tmul_eq_top, Submodule.mem_span_set] at mem
    obtain ⟨c, hc, rfl⟩ := mem
    choose b a hy using hc
    let r : ⦃a : E ⊗[R] M⦄ → a ∈ ↑c.support → R := fun a ha =>
      Submodule.mem_span_singleton.1 (b ha).2 |>.choose
    have hr : ∀ ⦃i : E ⊗[R] M⦄ (hi : i ∈ c.support), b hi =
        r hi • ⟨l23 (l12 n1), Submodule.mem_span_singleton_self _⟩ := fun a ha =>
      Subtype.ext <| Submodule.mem_span_singleton.1 (b ha).2 |>.choose_spec.symm
    -- Since `M` is flat and `E -> N1` is injective, we only need to check that x = 0
    -- in `N1 ⊗ M`. We write `x = ∑ μᵢ • (l23 (l12 n1)) ⊗ mᵢ = ∑ μᵢ • 0 = 0`
    -- (remember `E = span {l23 (l12 n1)}` and `eq1`)
    refine Finset.sum_eq_zero fun i hi => show c i • i = 0 from
      (Module.Flat.rTensor_preserves_injective_linearMap (M := M) E.subtype <|
              Submodule.injective_subtype E) ?_
    rw [← hy hi, hr hi, smul_tmul, map_smul, LinearMap.rTensor_tmul, Submodule.subtype_apply, eq1,
      smul_zero, map_zero]

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
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
eq0 : ⊤ = ⊥
⊢ False
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
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
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
this : NoZeroDivisors R
⊢ IsAlgebraic R a

Tactic:
have := Algebra.nontrivial_of_isAlgebraic R S

Goal state after:
case pos
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
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
this✝ : NoZeroDivisors R
this : Nontrivial R
⊢ IsAlgebraic R a
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R
⊢ (∀ x ∈ zeroLocus ↑I, f ∈ x.asIdeal) ↔ f ∈ sInf {J | I ≤ J ∧ J.IsPrime}

Tactic:
Submodule.mem_sInf

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R
⊢ (∀ x ∈ zeroLocus ↑I, f ∈ x.asIdeal) ↔ ∀ p ∈ {J | I ≤ J ∧ J.IsPrime}, f ∈ p
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
iff_exact :
  ∀ {N1 : Type (max u v)} [inst : AddCommGroup N1] [inst_1 : Module R N1] {N2 : Type (max u v)}
    [inst_2 : AddCommGroup N2] [inst_3 : Module R N2] {N3 : Type (max u v)} [inst_4 : AddCommGroup N3]
    [inst_5 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
    Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
h : Subsingleton (N ⊗[R] M)
y : N
x : N ⊗[R] M
⊢ (LinearMap.rTensor M 0) x = 0 ↔ x ∈ Set.range ⇑(LinearMap.rTensor M 0)

Tactic:
simpa using Subsingleton.elim _ _

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✝ : Module.FaithfullyFlat A B
I : Ideal A
⊢ Function.Injective
    (⇑↑(LinearEquiv.restrictScalars A ↑(quotIdealMapEquivTensorQuot B I).symm) ∘ ⇑((TensorProduct.mk A B (A ⧸ I)) 1))

Tactic:
exact (LinearEquiv.injective _).comp <|
      Module.FaithfullyFlat.tensorProduct_mk_injective (A ⧸ I)

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑(SemilatticeSup.sup a b ⊓ SemilatticeSup.sup a c)).2 = (↑(SemilatticeSup.sup a (b ⊓ c))).2

Tactic:
(· ⊓ ·),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑(SemilatticeSup.sup (SemilatticeSup.sup a b)ᶜ (SemilatticeSup.sup a c)ᶜ)ᶜ).2 =
    (↑(SemilatticeSup.sup a (SemilatticeSup.sup bᶜ cᶜ)ᶜ)).2
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : 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
j : ι
⊢ ∏ c, e c j = 0 j

Tactic:
Pi.zero_apply,

Goal state after:
ι : 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
j : ι
⊢ ∏ c, e c j = 0
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b a : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑(a ⊓ aᶜ)).2 = 1

Tactic:
(· ⊓ ·),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b a : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑(SemilatticeSup.sup aᶜ aᶜᶜ)ᶜ).2 = 1
Module: Mathlib.RingTheory.Localization.AsSubring

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a s : A
hs : s ∈ S
⊢ IsLocalization.mk' K a ⟨s, ⋯⟩ ∈ (mapToFractionRing K S B hS).range

Tactic:
use IsLocalization.mk' _ a ⟨s, hs⟩

Goal state after:
case h
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a s : A
hs : s ∈ S
⊢ (mapToFractionRing K S B hS).toRingHom (IsLocalization.mk' B a ⟨s, hs⟩) = IsLocalization.mk' K a ⟨s, ⋯⟩
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c : { x // IsIdempotentElem x }
⊢ ↑(a ⊓ SemilatticeSup.sup b c) = ↑(SemilatticeSup.sup (a ⊓ b) (a ⊓ c))

Tactic:
(· ⊓ ·),

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b c : { x // IsIdempotentElem x }
⊢ ↑(SemilatticeInf.inf a (SemilatticeSup.sup b c)) =
    ↑(SemilatticeSup.sup (SemilatticeInf.inf a b) (SemilatticeInf.inf a c))