mathlib-initiative/mathlib-tactics huggingface dataset:
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 ((⅟(fromBlocks A B 0 D)).toBlocks₁₁ * A + (⅟(fromBlocks A B 0 D)).toBlocks₁₂ * 0)
      ((⅟(fromBlocks A B 0 D)).toBlocks₁₁ * B + (⅟(fromBlocks A B 0 D)).toBlocks₁₂ * D)
      ((⅟(fromBlocks A B 0 D)).toBlocks₂₁ * A + (⅟(fromBlocks A B 0 D)).toBlocks₂₂ * 0)
      ((⅟(fromBlocks A B 0 D)).toBlocks₂₁ * B + (⅟(fromBlocks A B 0 D)).toBlocks₂₂ * D) =
    1
⊢ (⅟(fromBlocks A B 0 D)).toBlocks₁₁ * A = 1

Tactic:
simpa using

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₁₁ * A + (⅟(fromBlocks A B 0 D)).toBlocks₁₂ * 0)
      ((⅟(fromBlocks A B 0 D)).toBlocks₁₁ * B + (⅟(fromBlocks A B 0 D)).toBlocks₁₂ * D)
      ((⅟(fromBlocks A B 0 D)).toBlocks₂₁ * A + (⅟(fromBlocks A B 0 D)).toBlocks₂₂ * 0)
      ((⅟(fromBlocks A B 0 D)).toBlocks₂₁ * B + (⅟(fromBlocks A B 0 D)).toBlocks₂₂ * 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 * (⅟(fromBlocks A B 0 D)).toBlocks₁₁ + B * (⅟(fromBlocks A B 0 D)).toBlocks₂₁)
      (A * (⅟(fromBlocks A B 0 D)).toBlocks₁₂ + B * (⅟(fromBlocks A B 0 D)).toBlocks₂₂)
      (0 * (⅟(fromBlocks A B 0 D)).toBlocks₁₁ + D * (⅟(fromBlocks A B 0 D)).toBlocks₂₁)
      (0 * (⅟(fromBlocks A B 0 D)).toBlocks₁₂ + D * (⅟(fromBlocks A B 0 D)).toBlocks₂₂) =
    1
⊢ D * (⅟(fromBlocks A B 0 D)).toBlocks₂₂ = 1

Tactic:
simpa using

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 * (⅟(fromBlocks A B 0 D)).toBlocks₁₁ + B * (⅟(fromBlocks A B 0 D)).toBlocks₂₁)
      (A * (⅟(fromBlocks A B 0 D)).toBlocks₁₂ + B * (⅟(fromBlocks A B 0 D)).toBlocks₂₂)
      (0 * (⅟(fromBlocks A B 0 D)).toBlocks₁₁ + D * (⅟(fromBlocks A B 0 D)).toBlocks₂₁)
      (0 * (⅟(fromBlocks A B 0 D)).toBlocks₁₂ + D * (⅟(fromBlocks A B 0 D)).toBlocks₂₂) =
    1
⊢ D * (⅟(fromBlocks A B 0 D)).toBlocks₂₂ = 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 α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  (fromBlocks (A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ + 0 * (⅟(fromBlocks A 0 C D)).toBlocks₂₁)
        (A * (⅟(fromBlocks A 0 C D)).toBlocks₁₂ + 0 * (⅟(fromBlocks A 0 C D)).toBlocks₂₂)
        (C * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ + D * (⅟(fromBlocks A 0 C D)).toBlocks₂₁)
        (C * (⅟(fromBlocks A 0 C D)).toBlocks₁₂ + D * (⅟(fromBlocks A 0 C D)).toBlocks₂₂)).toBlocks₁₁ =
    toBlocks₁₁ 1
⊢ A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ = 1

Tactic:
simpa using

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 α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  (fromBlocks (A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ + 0 * (⅟(fromBlocks A 0 C D)).toBlocks₂₁)
        (A * (⅟(fromBlocks A 0 C D)).toBlocks₁₂ + 0 * (⅟(fromBlocks A 0 C D)).toBlocks₂₂)
        (C * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ + D * (⅟(fromBlocks A 0 C D)).toBlocks₂₁)
        (C * (⅟(fromBlocks A 0 C D)).toBlocks₁₂ + D * (⅟(fromBlocks A 0 C D)).toBlocks₂₂)).toBlocks₁₁ =
    toBlocks₁₁ 1
⊢ A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ = 1
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
⊢ P M

Tactic:
by
  let Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
  have : Q M := by
    apply diagonal_transvection_induction Q M
    · grind
    · intro t
      exact ⟨by simp, htransvec t⟩
    · intro A B QA QB
      exact ⟨by simp [QA.1, QB.1], hmul A B QA.1 QB.1 QA.2 QB.2⟩
  exact this.2

Goal state after:
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 α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  (fromBlocks ((⅟(fromBlocks A 0 C D)).toBlocks₁₁ * A + (⅟(fromBlocks A 0 C D)).toBlocks₁₂ * C)
        ((⅟(fromBlocks A 0 C D)).toBlocks₁₁ * 0 + (⅟(fromBlocks A 0 C D)).toBlocks₁₂ * D)
        ((⅟(fromBlocks A 0 C D)).toBlocks₂₁ * A + (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * C)
        ((⅟(fromBlocks A 0 C D)).toBlocks₂₁ * 0 + (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * D)).toBlocks₂₂ =
    toBlocks₂₂ 1
⊢ (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * D = 1

Tactic:
simpa using

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 α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  (fromBlocks ((⅟(fromBlocks A 0 C D)).toBlocks₁₁ * A + (⅟(fromBlocks A 0 C D)).toBlocks₁₂ * C)
        ((⅟(fromBlocks A 0 C D)).toBlocks₁₁ * 0 + (⅟(fromBlocks A 0 C D)).toBlocks₁₂ * D)
        ((⅟(fromBlocks A 0 C D)).toBlocks₂₁ * A + (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * C)
        ((⅟(fromBlocks A 0 C D)).toBlocks₂₁ * 0 + (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * D)).toBlocks₂₂ =
    toBlocks₂₂ 1
⊢ (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * D = 1
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelAddMonoid α
p : a ≤ b
H : a' + b < b' + b
⊢ a' < b'

Tactic:
simpa using

Goal state after:
α : Type u_1
a a' b b' : α
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelAddMonoid α
p : a ≤ b
H : a' + b < b' + b
⊢ a' < b'
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)ˣ
N : Matrix n n R
⊢ ((↑M)⁻¹ * N * ↑M).charpoly = N.charpoly

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)ˣ
N : Matrix n n R
⊢ ((↑M)⁻¹ * N * ↑M).charpoly = N.charpoly
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : IsNilpotent (-1)
⊢ False

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : IsNilpotent (-1)
⊢ False
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
hx : IsUnit x
H : IsNilpotent x
⊢ False

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
hx : IsUnit x
H : IsNilpotent x
⊢ False
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
hx : IsNilpotent x
⊢ ¬¬IsNilpotent x

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
hx : IsNilpotent x
⊢ IsNilpotent x
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
r : R
inst✝ : Semiring R
k : ℕ
⊢ C r ^ k = 0 ↔ r ^ k = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
r : R
inst✝ : Semiring R
k : ℕ
⊢ C (r ^ k) = 0 ↔ r ^ k = 0
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
x✝ : i ∈ P.support
⊢ IsNilpotent ((fun n a ↦ (monomial n) a) i (P.coeff i))

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
x✝ : i ∈ P.support
⊢ IsNilpotent (P.coeff i)
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
i k : ℕ
hk : (p + C r) ^ k = 0
hp : eval 0 p = 0
⊢ r ^ k = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
i k : ℕ
hk : (p + C r) ^ k = 0
hp : eval 0 p = 0
⊢ r ^ k = 0
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_2.zero
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
⊢ IsNilpotent ((p + C r).coeff 0)

Tactic:
simpa using

Goal state after:
case refine_2.zero
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
⊢ IsNilpotent r
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_2.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent p

Tactic:
simpa using

Goal state after:
case refine_2.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent p
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_3.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpX : IsNilpotent (p * X)
i : ℕ
⊢ IsNilpotent ((p * X).coeff (i + 1))

Tactic:
simpa using

Goal state after:
case refine_3.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpX : IsNilpotent (p * X)
i : ℕ
⊢ IsNilpotent (p.coeff i)
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_1.inl
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent (P.coeff i)

Tactic:
simpa using

Goal state after:
case refine_1.inl
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent (P.coeff i)
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_2.inl
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent ((reflect N P).coeff i)

Tactic:
simpa using

Goal state after:
case refine_2.inl
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent (P.coeff (N - i))
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_2.inr
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent ((reflect N P).coeff i)

Tactic:
simpa using

Goal state after:
case refine_2.inr
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent (P.coeff i)
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
⊢ x m = y m

Tactic:
obtain ⟨m, rfl⟩ : m ∈ LinearMap.range (Fintype.linearCombination R b) := by
    rw [(Fintype.range_linearCombination R b).trans hb]
    exact Submodule.mem_top

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

Tactic:
simpa using

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 ι
r : R
⊢ Represents b (r • 1) (r • 1)
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case a
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, (↑↑s).encard ≤ ⨅ s, ⨅ (_ : span R s = p), s.encard

Tactic:
refine le_iInf fun s ↦ le_iInf fun h ↦ ?_

Goal state after:
case a
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 : Set M
h : span R s = p
⊢ ⨅ s, (↑↑s).encard ≤ s.encard
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
h : ⨅ s, #↑↑s < ℵ₀
s : { s // span R s = p }
hs : (fun s ↦ #↑↑s) s = ⨅ s, #↑↑s
⊢ (↑s).Finite

Tactic:
simpa using

Goal state after:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ⨅ s, #↑↑s < ℵ₀
s : { s // span R s = p }
hs : (fun s ↦ #↑↑s) s = ⨅ s, #↑↑s
⊢ (↑s).Finite
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
⊢ ↑(toNat p.spanRank) = p.spanRank ↔ p.spanRank < ℵ₀

Tactic:
exact cast_toNat_eq_iff_lt_aleph0

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
h : M.FG
n✝ n : ℕ
ih : (M ^ n).FG
⊢ (M ^ n.succ).FG

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
h : M.FG
n✝ n : ℕ
ih : (M ^ n).FG
⊢ (M ^ n * M).FG
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
h✝ : Nontrivial R
s : Finset M
hs_card : s.card = ⊤.spanFinrank
hs_span : Submodule.span R ↑s = ⊤
this : Submodule.span R (Set.range Subtype.val) = ⊤
A : ↥(isRepresentation R Subtype.val)
h : ∀ (i j : ↥s), ↑A i j ∈ I
hI : range ((isRepresentation.toEnd R Subtype.val this) A) ≤ I • ⊤
⊢ ∀ (k : ℕ), (↑A).charpoly.coeff k ∈ I ^ ((↑A).charpoly.natDegree - k)

Tactic:
simpa using

Goal state after:
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
h✝ : Nontrivial R
s : Finset M
hs_card : s.card = ⊤.spanFinrank
hs_span : Submodule.span R ↑s = ⊤
this : Submodule.span R (Set.range Subtype.val) = ⊤
A : ↥(isRepresentation R Subtype.val)
h : ∀ (i j : ↥s), ↑A i j ∈ I
hI : range ((isRepresentation.toEnd R Subtype.val this) A) ≤ I • ⊤
⊢ ∀ (k : ℕ), (↑A).charpoly.coeff k ∈ I ^ (s.card - k)
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.FG
s : Set M
hs₁ : s.encard = ↑p.spanFinrank
hs₂ : span R s = p
s_f : s.Finite
⊢ span R ↑s_f.toFinset = p

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : s.encard = ↑p.spanFinrank
hs₂ : span R s = p
s_f : s.Finite
⊢ span R s = p
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.FG
s : Set M
hs₁ : s.encard = ↑p.spanFinrank
hs₂ : span R s = p
s_f : s.Finite
⊢ span R ↑s_f.toFinset = p

Tactic:
by simpa using hs₂

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.FG
s : Set M
hs₁ : s.encard = ↑p.spanFinrank
hs₂ : span R s = p
s_f : s.Finite
⊢ s_f.toFinset.card = p.spanFinrank

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : s.encard = ↑p.spanFinrank
hs₂ : span R s = p
s_f : s.Finite
⊢ s_f.toFinset.card = p.spanFinrank
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:
by
  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.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
hp : p.FG
⊢ p.generators.Finite

Tactic:
← Cardinal.lt_aleph0_iff_set_finite,

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
hp : p.FG
⊢ #↑p.generators < ℵ₀
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
fg : p.FG
⊢ ∃ a, p.generators = {a}

Tactic:
simpa using

Goal state after:
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
fg : p.FG
⊢ ∃ a, p.generators = {a}
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

Goal state after:
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
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Ring T
f : R →+* S
g : S →+* T
x : T
p : R[X]
hp : p.Monic
hx : eval₂ (g.comp f) x p = 0
⊢ eval₂ g x (Polynomial.map f p) = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Ring T
f : R →+* S
g : S →+* T
x : T
p : R[X]
hp : p.Monic
hx : eval₂ (g.comp f) x p = 0
⊢ eval x (Polynomial.map (g.comp f) p) = 0
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
hf : Function.Injective ⇑f
p : Submodule R M
s : Set M
hs : Cardinal.mk ↑(⇑f '' s) = (map f p).spanRank
e : span S (⇑f '' s) = map f p
⊢ span R s = p

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
hf : Function.Injective ⇑f
p : Submodule R M
s : Set M
hs : Cardinal.mk ↑(⇑f '' s) = (map f p).spanRank
e : span S (⇑f '' s) = map f p
⊢ span R s = p
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
hf : Function.Injective ⇑f
p : Submodule R M
⊢ (map f p).spanRank = p.spanRank

Tactic:
simpa using

Goal state after:
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
hf : Function.Injective ⇑f
p : Submodule R M
⊢ (map f p).spanRank = p.spanRank
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
⊢ f.range.spanRank ≤ ⊤.spanRank

Tactic:
simpa using

Goal state after:
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
⊢ f.range.spanRank ≤ ⊤.spanRank
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
⊢ ⊤.spanRank = p.spanRank

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⊤.spanRank = p.spanRank