mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f g : V →ₗ[K] V'
⊢ (f + g).rank ≤ Module.rank K ↥(f.range ⊔ g.range)

Tactic:
by
      refine Submodule.rank_mono ?_
      exact LinearMap.range_le_iff_comap.2 <| eq_top_iff'.2 fun x =>
        show f x + g x ∈ (LinearMap.range f ⊔ LinearMap.range g : Submodule K V') from
        mem_sup.2 ⟨_, ⟨x, rfl⟩, _, ⟨x, rfl⟩, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
this : ∀ i < (lieCharpoly K (↥E) x' u).natDegree, χ.coeff i = 0
⊢ χ = X ^ (lieCharpoly K (↥E) x' u).natDegree

Tactic:
rw [(lieCharpoly_monic K E x' u).eq_X_pow_iff_natDegree_le_natTrailingDegree]

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
this : ∀ i < (lieCharpoly K (↥E) x' u).natDegree, χ.coeff i = 0
⊢ (lieCharpoly K (↥E) x' u).natDegree ≤ (lieCharpoly K (↥E) x' u).natTrailingDegree
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝² : Fintype n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
a✝ : Nontrivial R
⊢ (B * A).rank = B.rank

Tactic:
refine le_antisymm (rank_mul_le_left B A) ?_

Goal state after:
m : Type um
n : Type un
inst✝² : Fintype n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
a✝ : Nontrivial R
⊢ B.rank ≤ (B * A).rank
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
⊢ (diagonal w).cRank = lift.{uR, um} #{ i // w i ≠ 0 }

Tactic:
classical
  set w' : {i // (w i) ≠ 0} → _ := fun i ↦ (diagonal w) i
  have h : LinearIndependent R w' := by
    have hli' := Pi.linearIndependent_single_of_ne_zero (R := R)
      (v := fun i : m ↦ if w i = 0 then (1 : R) else w i) (by simp [ite_eq_iff'])
    convert! hli'.comp Subtype.val Subtype.val_injective
    ext ⟨j, hj⟩ k
    simp [w', diagonal, hj, Pi.single_apply, eq_comm]
  have hrw : insert 0 (range (diagonal w).col) = insert 0 (range w') := by
    suffices ∀ a, diagonal w a = 0 ∨ ∃ b, w b ≠ 0 ∧ diagonal w b = diagonal w a
      by aesop (add simp [col_eq_transpose, subset_def])
    simp_rw [or_iff_not_imp_right, not_exists, not_and, not_imp_not]
    simp +contextual [funext_iff, diagonal]
  rw [cRank, ← span_insert_zero, hrw, span_insert_zero, rank_span h,
    ← lift_umax, ← Cardinal.mk_range_eq_of_injective h.injective, lift_id']

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

Goal state before:
pp: l : Type ul
m : Type um
n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
⊢ A.rank + B.rank ≤ Fintype.card m

Tactic:
let en : Basis n R (n → R) := Pi.basisFun R n

Goal state after:
l : Type ul
m : Type um
n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
el : Basis l R (l → R) := Pi.basisFun R l
em : Basis m R (m → R) := Pi.basisFun R m
en : Basis n R (n → R) := Pi.basisFun R n
⊢ A.rank + B.rank ≤ Fintype.card m
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a + Quot.mk (Rel R X) b) (Quot.mk (Rel R X) c) =
    Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) c) +
      Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) b) (Quot.mk (Rel R X) c)

Tactic:
change Quot.mk _ _ = Quot.mk _ _

Goal state after:
case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.mk (Rel R X) ((fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 + x2) a b) c) =
    Quot.mk (Rel R X) ((fun x1 x2 ↦ x1 + x2) ((fun x1 x2 ↦ x1 * x2) a c) ((fun x1 x2 ↦ x1 * x2) b c))
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b + Quot.mk (Rel R X) c) =
    Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b) +
      Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) c)

Tactic:
change Quot.mk _ _ = Quot.mk _ _

Goal state after:
case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.mk (Rel R X) ((fun x1 x2 ↦ x1 * x2) a ((fun x1 x2 ↦ x1 + x2) b c)) =
    Quot.mk (Rel R X) ((fun x1 x2 ↦ x1 + x2) ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c))
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (((lmap fun x ↦ Submodule.toBaseChange S (ℳ x)) ∘ₗ
        ↑(directSumRight R S S fun i ↦ ↥(ℳ i)) ∘ₗ
          ↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ))) ∘ₗ
      coeLinearMap fun i ↦ Submodule.baseChange S (ℳ i)) =
    LinearMap.id

Tactic:
· ext : 1
    rw [← LinearMap.cancel_right ((ℳ _).toBaseChange_surjective S)]
    ext : 3
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: case add
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
x y : ⨁ (i : ι), ↥(decomposeTensor ℳ N i)
hx :
  (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ)) ((DirectSum.coeAddMonoidHom (decomposeTensor ℳ N)) x) =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm x)
hy :
  (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ)) ((DirectSum.coeAddMonoidHom (decomposeTensor ℳ N)) y) =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm y)
⊢ (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ)) ((DirectSum.coeAddMonoidHom (decomposeTensor ℳ N)) (x + y)) =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm (x + y))

Tactic:
simp [hx, hy]

Goal state after:
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case right
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V := ⋯
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V := ⋯
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
trace_T_U_zero : ∀ (w : A), (LinearMap.trace R ↥U) (T χ w) = 0
trace_za : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = χ ⁅z, a⁆ • ↑(finrank R ↥U)
⊢ ((toEnd R L V) z ^ 0) v = v

Tactic:
pow_zero,

Goal state after:
case right
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
trace_T_U_zero : ∀ (w : A), (LinearMap.trace R ↥U) (T χ w) = 0
trace_za : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = χ ⁅z, a⁆ • ↑(finrank R ↥U)
⊢ 1 v = v
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i : Fin n
hEq1 : Eq1 A p
⊢ (-1) ^ (p + 1) * ∑ k > i, ∑ α ∈ S p k, bminor A k k α = (-1) ^ (p + 1) * ∑ α ∈ S (p + 1) i, pminor A α

Tactic:
by
      rw [S_succ_eq_biUnion, Finset.sum_biUnion]
      · congrm (((-1) ^ (p + 1) * ∑ k ∈ Finset.Ioi i, ?_))
        symm
        exact Finset.sum_image fun _ _ _ _ hαβ => (Fin.cons_inj.mp hαβ).2
      · grind [Set.PairwiseDisjoint, Set.Pairwise, Finset.disjoint_left, Fin.cons_inj]

Goal state after:
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ ⁅↑(((k ∙ z).projectionOnto ↑A ⋯) x), v⁆ = e (π₂ x) • ↑(c • ⟨v, hv⟩)

Tactic:
← he,

Goal state after:
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ ⁅e (((k ∙ z).projectionOnto ↑A ⋯) x) • z, v⁆ = e (π₂ x) • ↑(c • ⟨v, hv⟩)
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
⊢ ⊤ ≤ ⨆ α, f α

Tactic:
← biSup_corootSpace_eq_top

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
⊢ ⨆ α, ⨆ (_ : α.IsNonZero), corootSpace ⇑α ≤ ⨆ α, f α
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
⊢ y ≠ 0

Tactic:
simpa using y_notMem

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case zero
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
⊢ spanSingleton S x ^ 0 = spanSingleton S (x ^ 0)

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
⊢ 1 = spanSingleton S (x ^ 0)
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case zero
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
⊢ 1 = spanSingleton S (x ^ 0)

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
⊢ 1 = spanSingleton S 1
Module: Mathlib.Algebra.Module.DedekindDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
this : Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0
⊢ p ^ 0 = ⊤

Tactic:
pow_zero,

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
this : Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0
⊢ 1 = ⊤
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra R K
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Module R V
inst✝⁴ : IsScalarTower R K V
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsTorsionFree R K
M : Submodule R V
inst✝ : IsLattice K M
⊢ Free R ↥M

Tactic:
by
  have := Module.IsTorsionFree.trans_faithfulSMul R K V
  -- any torsion free finite module over a PID is free
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : Semiring K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : AddCommMonoid V₂
inst✝² : Module K V₂
inst✝¹ : AddCommMonoid V₃
inst✝ : Module K V₃
u : V →ₗ[K] V₂
h : u.HasFiniteRange
v : V₂ →ₗ[K] V₃
⊢ (v ∘ₗ u).HasFiniteRange

Tactic:
by
  rw [LinearMap.HasFiniteRange, LinearMap.range_comp] at *
  exact Submodule.FG.map v h

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u : V →ₗ[K] V₂
v : V₂ →ₗ[K] V₃
u' : V₂ →ₗ[K] V
w : V₃ →ₗ[K] V
hu : u'.IsRightQuasiInverse u
hw : w.IsLeftQuasiInverse (v ∘ₗ u)
⊢ u ∘ₗ (w ∘ₗ v ∘ₗ u) ∘ₗ u' ≈ u ∘ₗ id ∘ₗ u'

Tactic:
grw [hw.equiv]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u : V →ₗ[K] V₂
v : V₂ →ₗ[K] V₃
v' : V₃ →ₗ[K] V₂
w : V₃ →ₗ[K] V
hv : v'.IsLeftQuasiInverse v
hw : w.IsRightQuasiInverse (v ∘ₗ u)
⊢ v' ∘ₗ ((v ∘ₗ u) ∘ₗ w) ∘ₗ v ≈ v' ∘ₗ id ∘ₗ v

Tactic:
grw [hw.equiv]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this :
  ↑(Multiset.count (span {X} * ↑(normUnit (span {X}))) (normalizedFactors (span {r}))) =
    ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ span {r} ≠ 0

pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Prime (span {X})

Tactic:
normUnit_eq_one,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this :
  ↑(Multiset.count (span {X} * ↑1) (normalizedFactors (span {r}))) =
    ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ span {r} ≠ 0

R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Prime (span {X})