mathlib-initiative/mathlib-tactics huggingface dataset:
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 m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible A
⊢ IsUnit (fromBlocks A B C D) ↔ IsUnit (D - C * ⅟A * B)

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
    (invertibleEquivFromBlocks₁₁Invertible A B C D).nonempty_congr]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (1 - r)

Tactic:
rw [← IsUnit.neg_iff, neg_sub]

Goal state after:
R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r - 1)
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : (f P).degree = 0 ∧ (f Q).degree = 0
⊢ (f P).degree < ↑n

Tactic:
hPQ.1

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : (f P).degree = 0 ∧ (f Q).degree = 0
⊢ 0 < ↑n
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ IsUnit (C r + X * P) ↔ IsUnit r ∧ IsNilpotent P

Tactic:
by
  have : ∀ i, coeff (C r + X * P) (i + 1) = coeff P i := by simp
  simp_rw [isUnit_iff_coeff_isUnit_isNilpotent, Nat.forall_ne_zero_iff, this]
  simp only [coeff_add, coeff_C_zero, mul_coeff_zero, coeff_X_zero, zero_mul, add_zero,
    ← Polynomial.isNilpotent_iff]

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

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

Tactic:
· simp_rw [← Set.encard_coe_eq_coe_finsetCard]
    apply le_antisymm
    · exact le_iInf fun s ↦ iInf₂_le (s.1 : Set M) s.2
    · refine le_iInf fun s ↦ le_iInf fun h ↦ ?_
      by_cases hs : s.Finite
      · exact iInf_le_of_le ⟨hs.toFinset, by simpa⟩ (by simp)
      · rw [Set.Infinite.encard_eq hs]
        exact OrderTop.le_top _

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{max u v}
⊢ lift.{v, u} p.spanRank ≤ a → ∃ s, lift.{v, u} #↑s ≤ a ∧ span R s = p

pp: case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{max u v}
⊢ (∃ s, lift.{v, u} #↑s ≤ a ∧ span R s = p) → lift.{v, u} p.spanRank ≤ a

Tactic:
· intro h
    obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p
    exact ⟨s, ⟨hs₁ ▸ h, hs₂⟩⟩

Goal state after:
case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{max u v}
⊢ (∃ s, lift.{v, u} #↑s ≤ a ∧ span R s = p) → lift.{v, u} p.spanRank ≤ a
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 q : Submodule R M
⊢ (p ⊔ q).spanRank ≤ p.spanRank + q.spanRank

Tactic:
by
  apply (FG.spanRank_le_iff_exists_span_set_card_le (p ⊔ q)).mpr
  obtain ⟨sp, ⟨hp₁, rfl⟩⟩ := exists_span_set_card_eq_spanRank p
  obtain ⟨sq, ⟨hq₁, rfl⟩⟩ := exists_span_set_card_eq_spanRank q
  exact ⟨sp ∪ sq, ⟨hp₁ ▸ hq₁ ▸ (Cardinal.mk_union_le sp sq), span_union sp sq⟩⟩

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.spanFinrank = 1
⊢ p.spanRank < ℵ₀

Tactic:
by simp_all [spanFinrank]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M N : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module S N
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] N
p : Submodule R M
⊢ (map f p).spanRank ≤ p.spanRank

Tactic:
simpa using lift_spanRank_map_le f p

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
⊢ ∀ b ∈ univ,
    b ≠ 0 →
      (eval 0 (derivative ((-1) ^ ↑b)) * eval 0 (1 0 b) + (-1) ^ ↑b * (eval 0 (derivative (1 0 b)) + M 0 b)) *
            eval 0 (submatrix 1 Fin.succ b.succAbove).det +
          (-1) ^ ↑b * eval 0 (1 0 b) *
            eval 0 (derivative (submatrix 1 Fin.succ b.succAbove + X • (M.submatrix Fin.succ b.succAbove).map ⇑C).det) =
        0

Tactic:
intro i

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
⊢ 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
Module: Mathlib.Algebra.Polynomial.Eval.Subring

Goal state before:
pp: case mpr
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
⊢ ∀ c ∈ Finset.range (p.natDegree + 1), C (p.coeff c) * X ^ c ∈ (mapRingHom f).rangeS

Tactic:
intro i

Goal state after:
case mpr
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 : ℕ
⊢ i ∈ Finset.range (p.natDegree + 1) → C (p.coeff i) * X ^ i ∈ (mapRingHom f).rangeS
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
hp : toLaurentAlg M.charpoly = p
hq : toLaurentAlg M.charpolyRev = q
⊢ t_inv ^ Fintype.card n * p = invert q

Tactic:
← det_smul,

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
hq : toLaurentAlg M.charpolyRev = q
⊢ (t_inv • ((scalar n) t - M.map ⇑LaurentPolynomial.C)).det = invert q
Module: Mathlib.Algebra.Polynomial.HasseDeriv

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

Tactic:
rw [hasseDeriv_apply, coeff_sum, sum_def, Finset.sum_eq_single (n + k), coeff_monomial]

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ (if n + k - k = n then ↑((n + k).choose k) * f.coeff (n + k) else 0) = ↑((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: 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

Tactic:
intro i

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * ↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1) =
    ↑k ! * ↑((n + k + 1).choose (n + 1)) * ↑(n + 1) * f.coeff (n + k + 1)

Tactic:
norm_cast

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k ! * (n + k + 1).choose (k + 1)) * f.coeff (n + k + 1) =
    ↑(k ! * (n + k + 1).choose (n + 1) * (n + 1)) * f.coeff (n + k + 1)
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_cases hp : p = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : p = 0
⊢ ((taylor r) p).degree = p.degree

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : ¬p = 0
⊢ ((taylor r) p).degree = p.degree
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
⊢ p.support ⊆ (p.scaleRoots s).support

Tactic:
intro i

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ i ∈ p.support → i ∈ (p.scaleRoots s).support
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
⊢ (p.scaleRoots s).degree = p.degree

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : p = 0
⊢ (p.scaleRoots s).degree = p.degree

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ (p.scaleRoots s).degree = p.degree
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r s : R
a✝ : Nontrivial R
⊢ (X + C r).scaleRoots s = X + C (r * s)

Tactic:
ext (_ | _ | i) <;> 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 + i) * a ^ i

Tactic:
f.map_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 * a) ^ i = f (p.coeff i) * f s ^ (p.natDegree - i + i) * a ^ i
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
⊢ p.integralNormalization.degree = p.degree

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : p = 0
⊢ p.integralNormalization.degree = p.degree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.degree = p.degree
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
⊢ p.integralNormalization.natDegree = p.natDegree

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : p = 0
⊢ p.integralNormalization.natDegree = p.natDegree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.natDegree = p.natDegree
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

case neg
R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
p : R[X]
r : R
n : ℕ
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
p : R[X]
r : R
n : ℕ
hp : p = 0
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

case neg
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
p : R[X]
r : R
n : ℕ
hp : ¬p = 0
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
n : ℕ
_hn : n ∈ Finset.range (p.natDegree + 1)
⊢ f (p.leadingCoeff ^ (p.natDegree - 1)) * f (p.coeff n) * x ^ n =
    f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff n) * x ^ n)

Tactic:
f.map_pow,

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
n : ℕ
_hn : n ∈ Finset.range (p.natDegree + 1)
⊢ f p.leadingCoeff ^ (p.natDegree - 1) * f (p.coeff n) * x ^ n =
    f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff n) * x ^ n)
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r s : R
a✝ : Nontrivial R
⊢ (X - C r).scaleRoots s = X - C (r * s)

Tactic:
ext (_ | _ | i) <;> simp

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

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

Tactic:
intro i

Goal state after:
R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
⊢ i ∈ ↑(ofSubring T p).coeffs → i ∈ ↑T
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
⊢ ((Ideal.Quotient.mkₐ S I).comp (Algebra.ofId S S[X])).IsIntegral

Tactic:
have eq_top : Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X} = ⊤ := by
    ext g
    constructor
    · simp only [Algebra.mem_top, implies_true]
    · intro _
      obtain ⟨g', hg⟩ := Ideal.Quotient.mkₐ_surjective S I g
      have : g = (Polynomial.aeval ((Ideal.Quotient.mkₐ S I) X)) g' := by
        nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _),
          as_sum_range_C_mul_X_pow g', map_sum]
        simp only [Polynomial.C_mul', ← map_pow, map_smul]
      exact this ▸ (aeval_mem_adjoin_singleton S ((Ideal.Quotient.mk I) Polynomial.X))
  exact fun a ↦ (eq_top ▸ adjoin_le_integralClosure <| mon.quotient_isIntegralElem h)
    Algebra.mem_top

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : DivisionSemiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
ha : ¬a = 0
⊢ (C a * X + C b).Splits

Tactic:
rw [← mul_inv_cancel_left₀ ha b, C_mul, ← mul_add]

Goal state after:
case neg
R : Type u_1
inst✝ : DivisionSemiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
ha : ¬a = 0
⊢ (C a * (X + C (a⁻¹ * b))).Splits
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
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff p.natDegree = coeff 0 p.natDegree
hy0 : y ≠ 0
⊢ False

Tactic:
rw [coeff_zero, ← mul_one p.natDegree, ← natDegree_C_mul_X y hy0,
    coeff_comp_degree_mul_degree, monic, one_mul, leadingCoeff_C_mul_X] at h

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : y ^ p.natDegree = 0
hy0 : y ≠ 0
⊢ False

R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff (p.natDegree * (C y * X).natDegree) = 0
hy0 : y ≠ 0
⊢ (C y * X).natDegree ≠ 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_1.refine_2.h₀
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ ∀ b ∈ q.support,
    b ≠ q.natDegree → (if b ≤ q.natDegree + N then (q.coeff b).coeff ((revAt N) (q.natDegree + N - b)) else 0) = 0

Tactic:
intro i

Goal state after:
case refine_1.refine_2.h₀
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
i : ℕ
⊢ i ∈ q.support →
    i ≠ q.natDegree → (if i ≤ q.natDegree + N then (q.coeff i).coeff ((revAt N) (q.natDegree + N - i)) else 0) = 0
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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
x : ↥l23.ker ⊗[R] M
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = x

Tactic:
induction x using TensorProduct.induction_on with
  | zero => exact ⟨0, by simp⟩
  -- let `x ⊗ m` be an element in `ker l23 ⊗ M`, then `x ⊗ m` is in the kernel of `l23 ⊗ 𝟙M`.
  -- Since `N1 ⊗ M -l12 ⊗ M-> N2 ⊗ M -l23 ⊗ M-> N3 ⊗ M` is exact, we have that `x ⊗ m` is in
  -- the range of `l12 ⊗ 𝟙M`, i.e. `x ⊗ m = (l12 ⊗ 𝟙M) y` for some `y ∈ N1 ⊗ M` as elements of
  -- `N2 ⊗ M`. We need to prove that `x ⊗ m = (l12 ⊗ 𝟙M) y` still holds in `(ker l23) ⊗ M`.
  -- This is okay because `M` is flat and `ker l23 -> N2` is injective.
  | tmul x m =>
    rcases x with ⟨x, (hx : l23 x = 0)⟩
    have mem : x ⊗ₜ[R] m ∈ LinearMap.ker (l23.rTensor M) := by simp [hx]
    rw [LinearMap.exact_iff.1 ex] at mem
    obtain ⟨y, hy⟩ := mem
    refine ⟨LinearMap.rTensor M (LinearMap.rangeRestrict _ ∘ₗ LinearMap.rangeRestrict l12) y,
      Module.Flat.rTensor_preserves_injective_linearMap (LinearMap.ker l23).subtype
      Subtype.val_injective ?_⟩
    simp only [LinearMap.comp_codRestrict, LinearMap.rTensor_tmul, Submodule.coe_subtype, ← hy]
    rw [← LinearMap.comp_apply, ← LinearMap.rTensor_def, ← LinearMap.rTensor_comp,
      ← LinearMap.comp_apply, ← LinearMap.rTensor_comp, LinearMap.comp_assoc,
      LinearMap.subtype_comp_codRestrict, ← LinearMap.comp_assoc, Submodule.subtype_comp_inclusion,
      LinearMap.subtype_comp_codRestrict]
  | add x y hx hy =>
    obtain ⟨x, rfl⟩ := hx; obtain ⟨y, rfl⟩ := hy
    exact ⟨x + y, by simp⟩

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
⊢ Module.rank (FractionRing R[X]) (FractionRing S[X]) = Module.rank R S

Tactic:
have := IsDomain.of_faithfulSMul R S

Goal state after:
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
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
σ : Type u
⊢ Module.rank (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) = lift.{u, u_2} (Module.rank R S)

Tactic:
have := IsDomain.of_faithfulSMul R S

Goal state after:
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
σ : Type u
this : IsDomain R
⊢ Module.rank (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) = lift.{u, u_2} (Module.rank R 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
x✝³ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (M ⊗[R] N)
⊢ LinearMap.lTensor M LinearMap.id = 0

Tactic:
ext; exact Subsingleton.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
x✝³ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (N ⊗[R] M)
⊢ LinearMap.rTensor M LinearMap.id = 0

Tactic:
ext; exact Subsingleton.elim _ _

Goal state after: