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

Goal state before:
pp: α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
l' : Type u_15
m' : Type u_16
n' : Type u_17
p' : Type u_18
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
⊢ kroneckerMap f ((reindex el em) M) ((reindex en ep) N) =
    (reindex (el.prodCongr en) (em.prodCongr ep)) (kroneckerMap f M N)

Tactic:
ext ⟨i, i'⟩ ⟨j, j'⟩

Goal state after:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
l' : Type u_15
m' : Type u_16
n' : Type u_17
p' : Type u_18
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
i : l'
i' : n'
j : m'
j' : p'
⊢ kroneckerMap f ((reindex el em) M) ((reindex en ep) N) (i, i') (j, j') =
    (reindex (el.prodCongr en) (em.prodCongr ep)) (kroneckerMap f M N) (i, i') (j, j')
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
l' : Type u_15
m' : Type u_16
n' : Type u_17
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype m'
inst✝⁷ : NonUnitalNonAssocSemiring α
inst✝⁶ : NonUnitalNonAssocSemiring β
inst✝⁵ : NonUnitalNonAssocSemiring γ
inst✝⁴ : Module R α
inst✝³ : Module R γ
inst✝² : Module S β
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
⊢ ((kroneckerMapBilinear f) (A * B)) (A' * B') = ((kroneckerMapBilinear f) A) A' * ((kroneckerMapBilinear f) B) B'

Tactic:
ext ⟨i, i'⟩ ⟨j, j'⟩

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
l' : Type u_15
m' : Type u_16
n' : Type u_17
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype m'
inst✝⁷ : NonUnitalNonAssocSemiring α
inst✝⁶ : NonUnitalNonAssocSemiring β
inst✝⁵ : NonUnitalNonAssocSemiring γ
inst✝⁴ : Module R α
inst✝³ : Module R γ
inst✝² : Module S β
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
i : l
i' : l'
j : n
j' : n'
⊢ ((kroneckerMapBilinear f) (A * B)) (A' * B') (i, i') (j, j') =
    (((kroneckerMapBilinear f) A) A' * ((kroneckerMapBilinear f) B) B') (i, i') (j, j')
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
⊢ (single i j c).BlockTriangular b

Tactic:
intro r s hrs
  apply single_apply_of_ne
  rintro ⟨rfl, rfl⟩
  exact (hij.trans_lt hrs).false

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
Xs : List (Matrix n n α)
⊢ (A :: Xs).prod⁻¹ = (List.map Inv.inv (A :: Xs).reverse).prod

Tactic:
by
    rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons,
      mul_inv_rev, list_prod_inv_reverse Xs]

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

Goal state before:
pp: case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : { a // b a ≠ k } → α := fun i ↦ b ↑i
h' : (M.toSquareBlockProp fun i ↦ b i ≠ k).BlockTriangular b'
hb' : image b' univ = (image b univ).erase k
l : α
hl : l ∈ (image b univ).erase k
⊢ ((M.toSquareBlockProp fun i ↦ b i ≠ k).toSquareBlock b' l).det = (M.toSquareBlock b l).det

Tactic:
let he : { a // b' a = l } ≃ { a // b a = l } :=
      haveI hc : ∀ i, b i = l → b i ≠ k := fun i hi => ne_of_eq_of_ne hi (ne_of_mem_erase hl)
      Equiv.subtypeSubtypeEquivSubtype @hc

Goal state after:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : { a // b a ≠ k } → α := fun i ↦ b ↑i
h' : (M.toSquareBlockProp fun i ↦ b i ≠ k).BlockTriangular b'
hb' : image b' univ = (image b univ).erase k
l : α
hl : l ∈ (image b univ).erase k
he : { a // b' a = l } ≃ { a // b a = l } := Equiv.subtypeSubtypeEquivSubtype ⋯
⊢ ((M.toSquareBlockProp fun i ↦ b i ≠ k).toSquareBlock b' l).det = (M.toSquareBlock b l).det
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' : n
⊢ ∀ (j_1 : n) (x : R[X]), (matPolyEquiv (single i' j_1 x)).coeff k i j = (single i' j_1 x i j).coeff k

Tactic:
j'

Goal state after:
case refine_3
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
⊢ ∀ (x : R[X]), (matPolyEquiv (single i' j' x)).coeff k i j = (single i' j' x i j).coeff k
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
⊢ (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂).charmatrix = fromBlocks M₁₁.charmatrix (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) M₂₂.charmatrix

Tactic:
simp only [charmatrix]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
⊢ (scalar (m ⊕ n)) X - C.mapMatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂) =
    fromBlocks ((scalar m) X - C.mapMatrix M₁₁) (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) ((scalar n) X - C.mapMatrix M₂₂)
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: n : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_3
inst✝ : CommRing R
A : Matrix n n R[X]
M : Matrix n n R
⊢ eval 0 (A + X • M.map ⇑C).det = eval 0 A.det

Tactic:
simp only [eval_det, map_zero, map_add, eval_add, Algebra.smul_def, map_mul]
  simp only [Algebra.algebraMap_eq_smul_one, matPolyEquiv_smul_one, map_X, X_mul, eval_mul_X,
    mul_zero, add_zero]

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
| M

Tactic:
matrix_eq_sum_single M

Goal state after:
n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
| ∑ i, ∑ j, single i j (M i j)
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
| M

Tactic:
matrix_eq_sum_single M

Goal state after:
n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
| ∑ i, ∑ j, single i j (M i j)
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
⊢ (matrixEquivTensor n R A) (single i j x) = x ⊗ₜ[R] single i j 1

Tactic:
have t : ∀ p : n × n, i = p.1 ∧ j = p.2 ↔ p = (i, j) := by aesop

Goal state after:
n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
t : ∀ (p : n × n), i = p.1 ∧ j = p.2 ↔ p = (i, j)
⊢ (matrixEquivTensor n R A) (single i j x) = x ⊗ₜ[R] single i j 1
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
hle : Fintype.card n ≤ Fintype.card m
⊢ X ^ ?m * (A * B).charpoly = X ^ (?m + (Fintype.card m - Fintype.card n)) * (B * A).charpoly

pp: case m
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
hle : Fintype.card n ≤ Fintype.card m
⊢ ℕ

Tactic:
Nat.add_sub_cancel' hle,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
hle : Fintype.card n ≤ Fintype.card m
⊢ X ^ Fintype.card n * (A * B).charpoly = X ^ Fintype.card m * (B * A).charpoly
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
a : Cardinal.{max u v}
⊢ lift.{v, u} p.spanRank ≤ a ↔ ∃ s, lift.{v, u} #↑s ≤ a ∧ span R s = p

Tactic:
by
  constructor
  · intro h
    obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p
    exact ⟨s, ⟨hs₁ ▸ h, hs₂⟩⟩
  · exact fun ⟨s, ⟨h₁, h₂⟩⟩ ↦ h₂.symm ▸ (Cardinal.lift_le.mpr (spanRank_span_le_card s)).trans h₁

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
inst✝ : Subsingleton R
p : Submodule R M
⊢ p.spanRank = 0

Tactic:
by
  simp [nontriviality]

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

Goal state before:
pp: case pos
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ Fintype.card n = 0

Tactic:
· assumption

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

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
n : ℕ
hn : 0 < n
hx : IsIntegral R (x ^ n)
p : R[X]
hmonic : p.Monic
heval : eval₂ (algebraMap R B) (x ^ n) p = 0
⊢ eval₂ (algebraMap R B) x ((expand R n) p) = 0

Tactic:
by rwa [← aeval_def, expand_aeval]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
⊢ (mapRingHom f) (C r) = C (f r)

Tactic:
simp only [coe_mapRingHom, map_C]

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
h : f r ∈ Set.range ⇑f
⊢ (mapRingHom f) (C r) = C (f r)

Tactic:
simp only [coe_mapRingHom, map_C]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.scaleRoots 0 = p.leadingCoeff • X ^ p.natDegree

Tactic:
by
  ext n
  simp only [coeff_scaleRoots, tsub_eq_zero_iff_le, zero_pow_eq, mul_ite,
    mul_one, mul_zero, coeff_smul, coeff_X_pow, smul_eq_mul]
  split_ifs with h₁ h₂ h₂
  · subst h₂; rfl
  · exact coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne h₁ (Ne.symm h₂))
  · exact (h₁ h₂.ge).elim
  · rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
r : R
hr : IsUnit r
this : Function.Bijective fun x ↦ r * x
a : R
⊢ Multiset.count ((fun x ↦ r * x) a) (p.scaleRoots r).roots =
    Multiset.count ((fun x ↦ r * x) a) (Multiset.map (fun x ↦ r * x) p.roots)

Tactic:
simp [Multiset.count_map_eq_count' _ p.roots this.1 a,
    rootMultiplicity_scaleRoots _ hr.isRegular.left]

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.coeff g.natDegree)
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

Tactic:
hg

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.coeff 1)
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.Algebra.Polynomial.Splits

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

pp: 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

Tactic:
· simp [leadingCoeff_eq_zero.mp hf0]

Goal state after:
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: 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

pp: 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

Tactic:
· simp [leadingCoeff_eq_zero.mp hf0]

Goal state after:
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.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 (C a * (C a⁻¹ * (X - C b)) + C b)

Tactic:
rw [← mul_assoc, ← C_mul, mul_inv_cancel₀ ha, C_1, one_mul, sub_add_cancel, comp_X]

Goal state after:
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
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹) p = 0
⊢ eval a p.reverse = 0

Tactic:
← (injective_iff_map_eq_zero' _).mp inj,

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹) p = 0
⊢ f (eval a p.reverse) = 0
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r p.divX * r + f (p.coeff 0) ∈ I
⊢ eval₂ f r p.divX * r ∈ I

Tactic:
exact I.mul_mem_left _ hr

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
e : N ≃ₗ[R] M
⊢ FaithfullyFlat R N

Tactic:
iff_flat_and_lTensor_faithful

Goal state after:
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
e : N ≃ₗ[R] M
⊢ Flat R N ∧
    ∀ (N_1 : Type (max u u_1)) [inst : AddCommGroup N_1] [inst_1 : Module R N_1],
      Nontrivial N_1 → Nontrivial (N ⊗[R] N_1)
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
e : N ≃ₗ[R] M
⊢ FaithfullyFlat R N

Tactic:
by
  rw [iff_flat_and_lTensor_faithful]
  exact ⟨Flat.of_linearEquiv e,
    fun P _ _ hP ↦ (TensorProduct.congr e (LinearEquiv.refl R P)).toEquiv.nontrivial⟩

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✝
ι : Type u_1
inst✝³ : Nonempty ι
M : ι → Type u_2
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), FaithfullyFlat R (M i)
⊢ FaithfullyFlat R (⨁ (i : ι), M i)

Tactic:
iff_flat_and_lTensor_faithful

Goal state after:
R : Type u
M✝ : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
ι : Type u_1
inst✝³ : Nonempty ι
M : ι → Type u_2
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), FaithfullyFlat R (M i)
⊢ Flat R (⨁ (i : ι), M i) ∧
    ∀ (N : Type (max u u_1 u_2)) [inst : AddCommGroup N] [inst_1 : Module R N],
      Nontrivial N → Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
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
i : ℕ
this : Invertible t := { invOf := s, invOf_mul_self := hst, mul_invOf_self := ⋯ }
⊢ max N (q.coeff i).natDegree ≤ N

Tactic:
by simp [hN]

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

Goal state before:
pp: case inl
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : ↑n ≠ 0
h : ↑n • x = (algebraMap S K) s
⊢ ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s

Tactic:
exact ⟨n, s, mod_cast ha, mod_cast h⟩

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

Goal state before:
pp: case inr
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : -↑n ≠ 0
h : -↑n • x = (algebraMap S K) s
⊢ ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s

Tactic:
exact ⟨n, -s, by simpa using ha, by simp [← h]⟩

Goal state after:
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
this✝ : Nontrivial R
this : IsDomain R
⊢ IsAlgebraic R a

Tactic:
classical
  have ⟨r, hr, int⟩ := Algebra.IsAlgebraic.exists_integral_multiples R (p.support.image (coeff p))
  let p := (r • p).toSubring (integralClosure R S).toSubring fun s hs ↦ by
    obtain ⟨n, hn, rfl⟩ := mem_coeffs_iff.mp hs
    exact int _ (Finset.mem_image_of_mem _ <| support_smul _ _ hn)
  have : IsAlgebraic (integralClosure R S) a := by
    refine ⟨p, ?_, ?_⟩
    · simpa only [← Polynomial.map_ne_zero_iff (f := Subring.subtype _) (p := p)
        Subtype.val_injective, p, map_toSubring, smul_ne_zero_iff] using And.intro hr hp
    rw [← eval_map_algebraMap, Subalgebra.algebraMap_eq, ← map_map, ← Subalgebra.toSubring_subtype,
      map_toSubring, eval_map_algebraMap, ← AlgHom.restrictScalars_apply R,
      map_smul, AlgHom.restrictScalars_apply, eval0, smul_zero]
  exact restrictScalars_of_isIntegral _ this

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
s : S
a : A
ha : IsAlgebraic R a
inst✝ : FaithfulSMul R S
⊢ IsAlgebraic S (s • 1 ⊗ₜ[R] a)

Tactic:
have ⟨p, h, eval0⟩ := ha

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
s : S
a : A
ha : IsAlgebraic R a
inst✝ : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : (aeval a) p = 0
⊢ IsAlgebraic S (s • 1 ⊗ₜ[R] a)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : FaithfulSMul R S
this✝¹ : FaithfulSMul R T
this✝ : IsDomain R
this : IsDomain S
⊢ finrank (FractionRing R) (FractionRing S) * finrank S T = finrank R T

Tactic:
← IsFractionRing.finrank_eq S (FractionRing S) T (FractionRing T),

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : FaithfulSMul R S
this✝¹ : FaithfulSMul R T
this✝ : IsDomain R
this : IsDomain S
⊢ finrank (FractionRing R) (FractionRing S) * finrank (FractionRing S) (FractionRing T) = finrank R T
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
⊢ FaithfullyFlat R M

Tactic:
rw [iff_zero_iff_lTensor_zero]

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
⊢ Flat R M ∧
    ∀ {N : Type (max u_1 u_3)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u_1 u_3)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), lTensor M f = 0 ↔ f = 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
f : R →+* S
hf₁ : I ≤ RingHom.ker f
hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S)
⊢ ∀ (y : ↥(R ⧸ I)⁰), IsUnit ((Quotient.lift I f hf₁) ↑y)

Tactic:
simpa [Ideal.Quotient.mk_surjective.forall, Ideal.Quotient.eq_zero_iff_mem]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal
⊢ KrullDimLE 1 R

Tactic:
by
  rwa [Ring.krullDimLE_one_iff]

Goal state after: