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

Goal state before:
pp: n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n 𝕜
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ M =
    (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod * M *
      ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)

Tactic:
reverse_inv_prod_mul_prod,

Goal state after:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n 𝕜
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ M = 1 * M * ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this : ⅟(fromBlocks A B 0 D) * fromBlocks A B 0 D = 1
⊢ (⅟(fromBlocks A B 0 D)).toBlocks₁₁ * A = 1

Tactic:
← fromBlocks_toBlocks (⅟(fromBlocks A B 0 D)),

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this :
  fromBlocks (⅟(fromBlocks A B 0 D)).toBlocks₁₁ (⅟(fromBlocks A B 0 D)).toBlocks₁₂ (⅟(fromBlocks A B 0 D)).toBlocks₂₁
        (⅟(fromBlocks A B 0 D)).toBlocks₂₂ *
      fromBlocks A B 0 D =
    1
⊢ (⅟(fromBlocks A B 0 D)).toBlocks₁₁ * A = 1
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this : fromBlocks A B 0 D * ⅟(fromBlocks A B 0 D) = 1
⊢ D * (⅟(fromBlocks A B 0 D)).toBlocks₂₂ = 1

Tactic:
← fromBlocks_toBlocks (⅟(fromBlocks A B 0 D)),

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this :
  fromBlocks A B 0 D *
      fromBlocks (⅟(fromBlocks A B 0 D)).toBlocks₁₁ (⅟(fromBlocks A B 0 D)).toBlocks₁₂
        (⅟(fromBlocks A B 0 D)).toBlocks₂₁ (⅟(fromBlocks A B 0 D)).toBlocks₂₂ =
    1
⊢ D * (⅟(fromBlocks A B 0 D)).toBlocks₂₂ = 1
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u v : n → R
h✝ : Nonempty n
h : 1 ≤ Fintype.card n
⊢ (vecMulVec u v).charpoly = X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1)

Tactic:
vecMulVec_eq (ι := Unit),

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u v : n → R
h✝ : Nonempty n
h : 1 ≤ Fintype.card n
⊢ (replicateCol Unit u * replicateRow Unit v).charpoly = X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1)
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) * (x + y) ^ (n + 1) = (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2)

Tactic:
rw [hz]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r u
⊢ IsUnit (u + r)

Tactic:
← Units.isUnit_mul_units _ hu.unit⁻¹,

Goal state after:
R : Type u_1
inst✝ : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r u
⊢ IsUnit ((u + r) * ↑hu.unit⁻¹)
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
nilp : IsNilpotent e
⊢ e = 0

Tactic:
by
  obtain ⟨rfl | n, hn⟩ := nilp
  · rw [pow_zero] at hn; rw [← one_mul e, hn, zero_mul]
  · rw [← hn, idem.pow_succ_eq]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsNilpotent (f i)) → (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
i : ι
hi : i ∈ s
⊢ i ∈ insert j s

Tactic:
by simp [hi]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
j✝ : ι
s : Finset ι
hj✝ : j✝ ∉ s
ih : (∀ i ∈ s, IsNilpotent (f i)) → (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j✝ s, IsNilpotent (f i)
h_comm : ∀ (i j : ι), i ∈ insert j✝ s → j ∈ insert j✝ s → Commute (f i) (f j)
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ i ∈ insert j✝ s

Tactic:
by simp [hi]

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
hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : (fromEnd R b) x = (fromEnd R b) y
m : M
⊢ m ∈ (Fintype.linearCombination R b).range

Tactic:
rw [(Fintype.range_linearCombination R b).trans hb]
    exact Submodule.mem_top

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

Goal state before:
pp: case mpr
ι : 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 ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i, A i j • b i = f (b j)
i✝ : ι
⊢ ∑ i, A i i✝ • b i = f (b i✝)

Tactic:
apply h

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 ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ (((LinearMap.llcomp R (ι → R) (ι → R) M) (Fintype.linearCombination R b))
          (algEquivMatrix'.symm A * algEquivMatrix'.symm A') ∘ₗ
        LinearMap.single R (fun i ↦ R) i✝)
      1 =
    ((PiToModule.fromEnd R b) (f * f') ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1

Tactic:
dsimp [PiToModule.fromEnd]

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 ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ (Fintype.linearCombination R b) ((algEquivMatrix'.symm A) ((algEquivMatrix'.symm A') (Pi.single i✝ 1))) =
    f (f' ((Fintype.linearCombination R b) (Pi.single i✝ 1)))
Module: Mathlib.Algebra.Module.SpanRank

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

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:
· rw [h1, eq_comm]; simp_rw [iInf_eq_top] at h1 ⊢
    exact fun s ↦ False.elim (Set.encard_ne_top_iff.mpr s.1.finite_toSet (h1 s.1 s.2))

Goal state after:
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
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 : ℕ
h : Fintype.card n - 1 ≤ k
⊢ Fintype.card n - 1 ≤ k

Tactic:
apply h

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_5
B : Type u_6
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A ≃ₐ[R] B
x : A
h : IsIntegral R (f x)
⊢ IsIntegral R x

Tactic:
by simpa using h.map f.symm

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 _ 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

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

Goal state before:
pp: R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
h' : algebraMap T S = (algebraMap R S).comp φ.symm.toRingHom
this : Algebra T R := φ.symm.toRingHom.toAlgebra
r : T
t : R
s : S
⊢ (r • t) • s = r • t • s

Tactic:
simp only [Algebra.smul_def, map_mul, h', mul_assoc]; rfl

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

Goal state before:
pp: R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
h' : algebraMap T S = (algebraMap R S).comp φ.symm.toRingHom
this : Algebra T R := φ.symm.toRingHom.toAlgebra
r : T
t : R
s : S
⊢ (r • t) • s = r • t • s

Tactic:
by simp only [Algebra.smul_def, map_mul, h', mul_assoc]; rfl

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

Goal state before:
pp: case mp
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f) → ↑p.coeffs ⊆ Set.range ⇑f

Tactic:
intro h _ hc
    obtain ⟨n, ⟨-, hn⟩⟩ := mem_coeffs_iff.mp hc
    exact hn ▸ h n

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
⊢ 0 = if n - k = i then 0 else 0

Tactic:
ite_self

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
⊢ 0 = 0
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
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
h_blocks :
  A.submatrix ⇑e ⇑e = fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1
⊢ (M.submatrix Subtype.val Subtype.val).det * det 1 = (M.submatrix Subtype.val Subtype.val).det

Tactic:
Matrix.det_one,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
h_blocks :
  A.submatrix ⇑e ⇑e = fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1
⊢ (M.submatrix Subtype.val Subtype.val).det * 1 = (M.submatrix Subtype.val Subtype.val).det
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
hy : y ^ 2 = 0
⊢ eval (x + y) p = eval x p + eval x (derivative p) * y

Tactic:
by
  rcases exists_mul_sq_add_linear_part_eq_eval_add p x y with ⟨c, h⟩
  rw [← h, hy]; ring

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

Goal state before:
pp: 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).coeff p.natDegree ≠ 0

Tactic:
rw [coeff_scaleRoots_natDegree]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ p.leadingCoeff ≠ 0
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
by_cases h' : i < p.degree

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
h' : ¬↑i < p.degree
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = ↑i
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)

Tactic:
by_cases h' : i < p.degree

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = ↑i
h' : ¬↑i < p.degree
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
⊢ f.integralNormalization.support = f.support

Tactic:
by
  nontriviality R using Subsingleton.eq_zero (α := R[X])
  have : IsDomain R := {}
  by_cases hf : f = 0; · simp [hf]
  ext i
  refine ⟨fun h => support_integralNormalization_subset h, ?_⟩
  simp only [integralNormalization_coeff, mem_support_iff]
  intro hfi
  split_ifs with hi <;> simp [hf, hfi]

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

Goal state before:
pp: case inl
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
⊢ (f.comp g).Splits

Tactic:
eq_C_of_natDegree_eq_zero (Nat.lt_one_iff.mp hg)

Goal state after:
case inl
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
⊢ (f.comp (C (g.coeff 0))).Splits
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
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:
ext : 1

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
⊢ (AlgHom.restrictScalars R
          (rTensorEquivAlgEquiv.invFun.comp
            (Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
              (mapAlgHom M includeRight) ⋯))).comp
      includeRight =
    (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))).comp includeRight
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 = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod

Tactic:
by_cases hf0 : f.leadingCoeff = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : f.leadingCoeff = 0
⊢ f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod

case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
⊢ f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod
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.natDegree = f.roots.card

Tactic:
by_cases hf0 : f.leadingCoeff = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : f.leadingCoeff = 0
⊢ f.natDegree = f.roots.card

case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
⊢ f.natDegree = f.roots.card
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
val✝ : A
h : val✝ ∈ integralClosure R A
⊢ IsIntegral R ((algebraMap (↥(integralClosure R A)) A) ⟨val✝, h⟩)

Tactic:
exact h

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

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
⊢ f = f.comp (X - C b + C b)

Tactic:
sub_add_cancel,

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
⊢ f = f.comp X
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
rbar_root :
  eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
i : ℕ
ne_zero : (Quotient.mk (comap f I)) (p.coeff i) ≠ 0
mem :
  (Quotient.mk (comap f I)) (p.coeff i) ∈
    comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)
⊢ (Quotient.mk I) (f (p.coeff i)) ∈ map (Quotient.mk I) J

pp: case refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
rbar_root :
  eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
i : ℕ
ne_zero : (Quotient.mk (comap f I)) (p.coeff i) ≠ 0
mem :
  (Quotient.mk (comap f I)) (p.coeff i) ∈
    comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)
⊢ p.coeff i ∈ ↑(comap f I) → (Quotient.mk (comap f I)) (p.coeff i) = 0

Tactic:
· simpa using mem

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
rbar_root :
  eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
i : ℕ
ne_zero : (Quotient.mk (comap f I)) (p.coeff i) ≠ 0
mem :
  (Quotient.mk (comap f I)) (p.coeff i) ∈
    comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)
⊢ p.coeff i ∈ ↑(comap f I) → (Quotient.mk (comap f I)) (p.coeff i) = 0
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
⊢ (comap (algebraMap R S) I).IsMaximal

Tactic:
by
  refine Ideal.Quotient.maximal_of_isField _ ?_
  have : IsPrime (I.comap (algebraMap R S)) := comap_isPrime _ _
  exact isField_of_isIntegral_of_isField
    algebraMap_quotient_injective (by rwa [← Quotient.maximal_ideal_iff_isField_quotient])

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_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : FaithfullyFlat R M
⊢ Nontrivial (M ⊗[R] N) ↔ Nontrivial N

Tactic:
by
  contrapose!; exact subsingleton_tensorProduct_iff_right R M

Goal state after:
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)
⊢ IsAlgebraic R z

Tactic:
by
  have ⟨p, monic, eval0⟩ := h
  refine ⟨p.comp (C y * X), fun h ↦ ?_, by simpa [aeval_comp, Algebra.smul_def] using! eval0⟩
  apply_fun (coeff · p.natDegree) at h
  have hy0 : y ≠ 0 := by rintro rfl; exact hy .zero
  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
  · exact hy ⟨_, h⟩
  · rw [natDegree_C_mul_X _ hy0]; rintro ⟨⟩

Goal state after: