mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: l : Type u_4
R : Type u₂
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ PD l R * ⅟2 • (PD l R)ᵀ = 1

Tactic:
rw [PD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_smul,
    Matrix.fromBlocks_multiply]

Goal state after:
l : Type u_4
R : Type u₂
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ fromBlocks (1 * ⅟2 • 1ᵀ + -1 * ⅟2 • (-1)ᵀ) (1 * ⅟2 • 1ᵀ + -1 * ⅟2 • 1ᵀ) (1 * ⅟2 • 1ᵀ + 1 * ⅟2 • (-1)ᵀ)
      (1 * ⅟2 • 1ᵀ + 1 * ⅟2 • 1ᵀ) =
    1
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ ↥(typeD l R) ≃ₗ⁅R⁆ ↥(so' l l R)

Tactic:
apply (skewAdjointMatricesLieSubalgebraEquiv (JD l R) (PD l R) (by infer_instance)).trans
  apply LieEquiv.ofEq
  ext A
  rw [jd_transform, ← val_unitOfInvertible (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe,
    mem_skewAdjointMatricesLieSubalgebra_unit_smul]
  rfl

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

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
⊢ span R ((fun a ↦ f (of.symm Aᵀ a)) '' Set.univ) = span R ((fun a ↦ of.symm (Aᵀ.submatrix id r) a) '' Set.univ)

Tactic:
aesop

Goal state after:
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
c : R
B : Matrix m n R
hc : c ∈ nonZeroDivisors R
hc' : IsSMulRegular R c
hreg : IsSMulRegular (m → R) c
f : (m → R) →ₗ[R] m → R := (LinearMap.lsmul R (m → R)) c
⊢ (c • B).mulVecLin = f ∘ₗ B.mulVecLin

Tactic:
aesop

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

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
s : Finset m
hz : ∀ x ∉ ↑s, A.row x = 0
B : Matrix m (↥s) R := of fun i a ↦ if ↑a = i then 1 else 0
hBdef : B = of fun i a ↦ if ↑a = i then 1 else 0
i : m
j : n
⊢ ∑ j_1, (if ↑j_1 = i then 1 else 0) * A (↑j_1) j = A i j

Tactic:
by_cases hi : i ∈ s

Goal state after:
case pos
m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
s : Finset m
hz : ∀ x ∉ ↑s, A.row x = 0
B : Matrix m (↥s) R := of fun i a ↦ if ↑a = i then 1 else 0
hBdef : B = of fun i a ↦ if ↑a = i then 1 else 0
i : m
j : n
hi : i ∈ s
⊢ ∑ j_1, (if ↑j_1 = i then 1 else 0) * A (↑j_1) j = A i j

case neg
m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
s : Finset m
hz : ∀ x ∉ ↑s, A.row x = 0
B : Matrix m (↥s) R := of fun i a ↦ if ↑a = i then 1 else 0
hBdef : B = of fun i a ↦ if ↑a = i then 1 else 0
i : m
j : n
hi : i ∉ s
⊢ ∑ j_1, (if ↑j_1 = i then 1 else 0) * A (↑j_1) j = A i j
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case neg
m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
s : Finset m
hz : ∀ x ∉ ↑s, A.row x = 0
B : Matrix m (↥s) R := of fun i a ↦ if ↑a = i then 1 else 0
hBdef : B = of fun i a ↦ if ↑a = i then 1 else 0
i : m
j : n
hi : i ∉ s
h0 : A i = 0
⊢ ∑ j_1, (if ↑j_1 = i then 1 else 0) * A (↑j_1) j = A i j

Tactic:
aesop

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
i : ℕ
hi : i < r
hi0 : i ≠ 0
H : constantCoeff ψ = 0
z : L
hz0 : (LieSubmodule.Quotient.mk' E) z ≠ 0
hxz : ⁅x', (LieSubmodule.Quotient.mk' E) z⁆ = 0
⊢ ⁅x, z⁆ ∈ E

Tactic:
rwa [← LieSubmodule.Quotient.mk_eq_zero']

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
⊢ Uᵀ * (Aᵀ * C * U) = Uᵀ * (Cᵀ * (A * U))

Tactic:
hsymm,

Goal state after:
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
⊢ Uᵀ * (Cᵀ * A * U) = Uᵀ * (Cᵀ * (A * U))
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case mp
m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : x ᵥ* Aᵀ ⬝ᵥ A *ᵥ x = 0
⊢ A *ᵥ x = 0

Tactic:
vecMul_transpose,

Goal state after:
case mp
m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : A *ᵥ x ⬝ᵥ A *ᵥ x = 0
⊢ A *ᵥ x = 0
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
⊢ { toFun := ⇑(LinearMap.rTensor L ↑d), map_add' := ⋯, map_smul' := ⋯ } ⁅x, y⁆ =
    ⁅x, { toFun := ⇑(LinearMap.rTensor L ↑d), map_add' := ⋯, map_smul' := ⋯ } y⁆ -
      ⁅y, { toFun := ⇑(LinearMap.rTensor L ↑d), map_add' := ⋯, map_smul' := ⋯ } x⁆

Tactic:
by
        simp only [LinearMap.coe_mk, AddHom.coe_mk]
        refine x.induction_on (by simp) (fun _ l ↦ ?_) (fun _ _ h1 h2 ↦ ?_)
        · refine y.induction_on (by simp) (fun _ l' ↦ ?_) (fun _ _ h1 h2 ↦ ?_)
          · simp [← lie_skew l' l, -lie_skew, add_tmul, tmul_neg]
          · simp [h1, h2, sub_add_sub_comm]
        · simp [h1, h2, sub_add_sub_comm]

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
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : z ∈ engel K ↑v
z' : Q := (LieSubmodule.Quotient.mk' E) z
hz' : ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
n : ℕ := Nat.find hz'
_hn : n = Nat.find hz'
hn : ((toEnd K (↥U) Q) v ^ n) z' = 0
⊢ n = 0 ∨ ∃ k, n = k + 1

Tactic:
by cases n <;> simp

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
a b c : lib R X
h : Rel R X b c
⊢ Rel R X (a + b) (a + c)

Tactic:
rw [add_comm _ b, add_comm _ c]

Goal state after:
R : Type u
X : Type v
inst✝ : CommRing R
a b c : lib R X
h : Rel R X b c
⊢ Rel R X (b + a) (c + a)
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: 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' := ⋯ }
n : ℕ
⊢ ∀ a < n, ∃ b < n + 1, ((toEnd R L V) z ^ b) v = ((toEnd R L V) z ^ (a + 1)) v

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x : K
y : L
⊢ { left := x, right := y } ∈ (inl ψ).range ↔
    { left := x, right := y } ∈ LieIdeal.toLieSubalgebra R (K ⋊⁅ψ⁆ L) (projr ψ).ker

Tactic:
aesop

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
h : s.Subsingleton
⊢ s.formPerm ⋯ = 1

Tactic:
by
  obtain ⟨s⟩ := s
  simp only [formPerm_coe, mk_eq_coe]
  simp only [length_subsingleton_iff, length_coe, mk_eq_coe] at h
  obtain - | ⟨hd, tl⟩ := s
  · simp
  · simp only [length_eq_zero_iff, add_le_iff_nonpos_left, List.length, nonpos_iff_eq_zero] at h
    simp [h]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case pos.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
left✝ : 0 < (f.cycleOf x).support.card
hy : (f ^ 0) x = y
⊢ f.toList x ~r f.toList y

Tactic:
simp only [coe_one, id, pow_zero] at hy

Goal state after:
case pos.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
left✝ : 0 < (f.cycleOf x).support.card
hy : x = y
⊢ f.toList x ~r f.toList y
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
xj : ↥(AddMonoidAlgebra.grade R j) ⊗[R] L
x y : ↥(AddMonoidAlgebra.grade R i) ⊗[R] L
hx :
  ⁅(LinearMap.rTensor L (AddMonoidAlgebra.grade R i).subtype) x,
      (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) xj⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
hy :
  ⁅(LinearMap.rTensor L (AddMonoidAlgebra.grade R i).subtype) y,
      (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) xj⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
⊢ ⁅(LinearMap.rTensor L (AddMonoidAlgebra.grade R i).subtype) x +
        (LinearMap.rTensor L (AddMonoidAlgebra.grade R i).subtype) y,
      (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) xj⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range

Tactic:
add_lie

Goal state after:
case add
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
xj : ↥(AddMonoidAlgebra.grade R j) ⊗[R] L
x y : ↥(AddMonoidAlgebra.grade R i) ⊗[R] L
hx :
  ⁅(LinearMap.rTensor L (AddMonoidAlgebra.grade R i).subtype) x,
      (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) xj⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
hy :
  ⁅(LinearMap.rTensor L (AddMonoidAlgebra.grade R i).subtype) y,
      (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) xj⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
⊢ ⁅(LinearMap.rTensor L (AddMonoidAlgebra.grade R i).subtype) x,
        (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) xj⁆ +
      ⁅(LinearMap.rTensor L (AddMonoidAlgebra.grade R i).subtype) y,
        (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) xj⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ ↑(s.formPerm.toList x) = ↑s

Tactic:
refine Quotient.sound' ?_

Goal state after:
case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ (IsRotated.setoid α) (s.formPerm.toList x) s
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
⊢ z ≠ 0

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case e_s
R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
a✝ : ℕ
⊢ a✝ ∈ Finset.Ico (↑i + 1) n ↔ a✝ ∈ {x ∈ Finset.range n | ↑i < x}

Tactic:
aesop

Goal state after:
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 : ℕ
α : Fin (p + 1) → Fin n
i : Fin n
s : Fin (p + 1)
⊢ (-1) ^ ↑s * ((A.submatrix (Fin.cons i (s.removeNth α)) α).submatrix id ⇑(Equiv.symm s.cycleRange)).det =
    (-1) ^ ↑s * bminor A i (α s) (s.removeNth α)

Tactic:
congrm _ * Matrix.det ?_
      simp [Fin.cons_removeNth_eq_comp_cycleRange_symm]

Goal state after:
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 : ℕ
α : Fin (p + 1) → Fin n
i j : Fin n
⊢ pminor A α * A i j + ∑ x, (-1) ^ (↑x + 1 + ↑x) * bminor A i (α x) (x.removeNth α) * A (α x) j =
    pminor A α * A i j + ∑ s, -(bminor A i (α s) (s.removeNth α) * A (α s) j)

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
α : Fin (p + 1) → Fin n
t : Fin (p + 1)
hα : (∀ (j : Fin (p + 1)), i < α j) ∧ StrictMono α
⊢ ((∀ (j : Fin p), i < t.removeNth α j) ∧ StrictMono (t.removeNth α)) ∧ i < α t

Tactic:
obtain ⟨hbound, hmono⟩ := hα

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
α : Fin (p + 1) → Fin n
t : Fin (p + 1)
hbound : ∀ (j : Fin (p + 1)), i < α j
hmono : StrictMono α
⊢ ((∀ (j : Fin p), i < t.removeNth α j) ∧ StrictMono (t.removeNth α)) ∧ i < α t
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
A : Matrix (Fin (k + 1)) (Fin (k + 1)) R
this : ∑ α ∈ S k 0, bminor A 0 0 α = A.det
⊢ A.det = (-1) ^ (k + k) * ∑ α ∈ S k 0, bminor A 0 0 α

Tactic:
aesop

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✝² : Nontrivial V
inst✝¹ : IsSolvable L
inst✝ : IsTriangularizable k L V
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
let imL := (toEnd k L V).range

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✝² : Nontrivial V
inst✝¹ : IsSolvable L
inst✝ : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := (toEnd k L V).range
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' : LieRinehartSubalgebra A L
x y z : ↥L'
⊢ ⟨⁅↑(x + y), ↑z⁆, ⋯⟩ = ⟨⁅↑x, ↑z⁆, ⋯⟩ + ⟨⁅↑y, ↑z⁆, ⋯⟩

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' : LieRinehartSubalgebra A L
x y z : ↥L'
⊢ ⟨⁅↑x, ↑(y + z)⁆, ⋯⟩ = ⟨⁅↑x, ↑y⁆, ⋯⟩ + ⟨⁅↑x, ↑z⁆, ⋯⟩

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' : LieRinehartSubalgebra A L
x : ↥L'
⊢ ⟨⁅↑x, ↑x⁆, ⋯⟩ = 0

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' : LieRinehartSubalgebra A L
x y z : ↥L'
⊢ ⟨⁅↑x, ↑⟨⁅↑y, ↑z⁆, ⋯⟩⁆, ⋯⟩ = ⟨⁅↑⟨⁅↑x, ↑y⁆, ⋯⟩, ↑z⁆, ⋯⟩ + ⟨⁅↑y, ↑⟨⁅↑x, ↑z⁆, ⋯⟩⁆, ⋯⟩

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
⊢ Function.Injective toSubmodule

Tactic:
by
  intro L₁' L₂' h
  rw [SetLike.ext'_iff] at h
  rw [← coe_set_eq]
  exact h

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : LieRing L
inst✝⁶ : Module A L
L' : LieRinehartSubalgebra A L
inst✝⁵ : LieRingModule L A
inst✝⁴ : LieRinehartRing A L
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R A
inst✝¹ : LieAlgebra R L
inst✝ : LieRinehartAlgebra R A L
⊢ ∀ (t : R) (x y : ↥L'), ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
x✝ : m ∈ ↑p
⊢ 0 • m ∈ ↑p

Tactic:
simp only [zero_smul, SetLike.mem_coe, zero_mem]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : Ideal R
⊢ ↑(I * J) = ↑I * ↑J

Tactic:
simp only [mul_def]
  exact coeToSubmodule_injective (coeSubmodule_mul _ _ _)

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

Goal state before:
pp: case mp.refine_4
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ↑{ carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } = J

Tactic:
· ext x
      constructor
      · rintro ⟨y, hy, eq_y⟩
        rwa [← eq_y]
      · intro hx
        obtain ⟨y, rfl⟩ := (mem_one_iff S).mp (hJ hx)
        exact mem_ofPred.mpr ⟨y, hx, rfl⟩

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

Goal state before:
pp: ι : Type u_1
A : Matrix ι ι ℤ
⊢ (∀ (b a : ι), a ≠ b → Aᵀ a b = 0 ∨ Aᵀ a b = -1) ↔ ∀ ⦃i j : ι⦄, i ≠ j → A i j = 0 ∨ A i j = -1

Tactic:
aesop

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝⁶ : CommMonoidWithZero M
inst✝⁵ : IsCancelMulZero M
N : Type u_2
inst✝⁴ : CommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
⊢ associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p) ∣ m

Tactic:
by
    simp only [dvd_of_mem_normalizedFactors hp, associatesEquivOfUniqueUnits_symm_apply,
      associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq]

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

Goal state before:
pp: R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I = 0
⊢ 0 = I * J

Tactic:
simp [hI]

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

Goal state before:
pp: case mp
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
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z, z • (IsLocalization.map P' (RingHom.id R) ⋯) x = y

Tactic:
obtain ⟨x', hx', rfl⟩ := (mem_canonicalEquiv_apply _ _ _).mp h

Goal state after:
case mp
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
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x x' : P
hx' : x' ∈ spanSingleton S x
h : (IsLocalization.map P' (RingHom.id R) ⋯) x' ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z, z • (IsLocalization.map P' (RingHom.id R) ⋯) x = (IsLocalization.map P' (RingHom.id R) ⋯) x'