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

Goal state before:
pp: case inr.inr.inl
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
hi : 0 < r
⊢ χ.coeff 0 = 0

Tactic:
apply eq_zero_of_forall_eval_zero_of_natDegree_lt_card _ _ ?deg
    case deg =>
      -- We need to show `(natDegree (coeff χ 0)) < #K` and know that `finrank K L ≤ #K`
      apply lt_of_lt_of_le _ hLK
      rw [Nat.cast_lt]
      -- So we are left with showing `natDegree (coeff χ 0) < finrank K L`
      apply lt_of_le_of_lt _ hr
      apply lieCharpoly_coeff_natDegree _ _ _ _ 0 r (zero_add r)
    -- Fix an element of `K`.
    intro α
    -- We want to show that `α` is a root of `coeff χ 0`.
    -- So we need to show that there is a `z ≠ 0` in `E` satisfying `⁅α • u + x, z⁆ = 0`.
    rw [← coe_evalRingHom, ← coeff_map, lieCharpoly_map_eval,
      ← constantCoeff_apply, LinearMap.charpoly_constantCoeff_eq_zero_iff]
    -- We consider `z = α • u + x`, and split into the cases `z = 0` and `z ≠ 0`.
    let z := α • u + x'
    obtain hz₀ | hz₀ := eq_or_ne z 0
    · -- If `z = 0`, then `⁅α • u + x, x⁆` vanishes and we use our assumption `x ≠ 0`.
      refine ⟨⟨x, self_mem_engel K x⟩, ?_, ?_⟩
      · exact Subtype.coe_ne_coe.mp hx₀
      · dsimp only [z] at hz₀
        simp only [hz₀, map_zero, LinearMap.zero_apply]
    -- If `z ≠ 0`, then `⁅α • u + x, z⁆` vanishes per axiom of Lie algebras
    refine ⟨⟨z, hUle z.2⟩, ?_, ?_⟩
    · simpa only [coe_bracket_of_module, ne_eq, Submodule.mk_eq_zero, Subtype.ext_iff] using! hz₀
    · change ⁅z, _⁆ = (0 : E)
      ext
      exact lie_self z.1

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✝² : Fintype n
inst✝¹ : Fintype n₀
inst✝ : CommSemiring R
em : m ≃ m₀
en : n ≃ n₀
A : Matrix m n R
⊢ finrank R ↥(Submodule.map (↑(LinearEquiv.funCongrLeft R R em.symm)) A.mulVecLin.range) = finrank R ↥A.mulVecLin.range

Tactic:
LinearEquiv.finrank_map_eq

Goal state after:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝² : Fintype n
inst✝¹ : Fintype n₀
inst✝ : CommSemiring R
em : m ≃ m₀
en : n ≃ n₀
A : Matrix m n R
⊢ finrank R ↥A.mulVecLin.range = finrank R ↥A.mulVecLin.range
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
hi : i ∈ s
a : ↥s
ha : a ≠ ⟨i, hi⟩
⊢ 0 * A (↑a) j = 0

Tactic:
zero_mul

Goal state after:
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
a : ↥s
ha : a ≠ ⟨i, hi⟩
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
hli' : LinearIndependent R fun i ↦ Pi.single i (if w i = 0 then 1 else w i)
⊢ LinearIndependent R w'

Tactic:
convert! hli'.comp Subtype.val Subtype.val_injective

Goal state after:
case e'_4
m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := ⋯
hli' : LinearIndependent R fun i ↦ Pi.single i (if w i = 0 then 1 else w i)
⊢ w' = (fun i ↦ Pi.single i (if w i = 0 then 1 else w i)) ∘ Subtype.val
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (A * Aᴴ).rank = A.rank

Tactic:
by
  simpa only [rank_conjTranspose, conjTranspose_conjTranspose] using
    rank_conjTranspose_mul_self Aᴴ

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✝¹ : Field R
inst✝ : Fintype m
A : Matrix m n R
⊢ Aᵀ.rank = A.rank

Tactic:
Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,

Goal state after:
m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Fintype m
A : Matrix m n R
⊢ finrank R ↥((toLin (Pi.basisFun R m).dualBasis (Pi.basisFun R n).dualBasis) Aᵀ).range = A.rank
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
⊢ A.rank + B.rank ≤ Fintype.card m

Tactic:
let el : Basis l R (l → R) := Pi.basisFun R l

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
⊢ A.rank + B.rank ≤ Fintype.card m
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: case mp
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
h : (d₂₃ R L M) a = 0
x y z : L
this : -(a ⁅x, y⁆) z + (a ⁅x, z⁆) y - (a ⁅y, z⁆) x = 0
⊢ (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆

Tactic:
sub_eq_zero

Goal state after:
case mp
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
h : (d₂₃ R L M) a = 0
x y z : L
this : -(a ⁅x, y⁆) z + (a ⁅x, z⁆) y = (a ⁅y, z⁆) x
⊢ (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
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
x✝¹ x✝ : LieDerivation R L L
⊢ { toFun := ⇑(LinearMap.lTensor A ↑⁅x✝¹, x✝⁆), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } =
    ⁅{ toFun := ⇑(LinearMap.lTensor A ↑x✝¹), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ },
      { toFun := ⇑(LinearMap.lTensor A ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }⁆

Tactic:
ext z
    refine z.induction_on (by simp) (fun a l ↦ ?_) (fun _ _ hx hy ↦ ?_)
    · simp [tmul_sub]
    · simp_all [sub_add_sub_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
A B C D : Matrix l l R
inst✝ : IsLocalRing R
hA : fromBlocks A B C D ∈ symplecticGroup l R
k : Type u_2 := IsLocalRing.ResidueField R
f : R →+* IsLocalRing.ResidueField R := IsLocalRing.residue R
A' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix A
C' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix C
F' : Matrix (l ⊕ l) (l ⊕ l) (IsLocalRing.ResidueField R) := fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
F'_def : F' = fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
⊢ IsUnit F'.det

Tactic:
convert (symplectic_det hA).map f

Goal state after:
l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
A B C D : Matrix l l R
inst✝ : IsLocalRing R
hA : fromBlocks A B C D ∈ symplecticGroup l R
k : Type u_2 := IsLocalRing.ResidueField R
f : R →+* IsLocalRing.ResidueField R := IsLocalRing.residue R
A' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix A
C' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix C
F' : Matrix (l ⊕ l) (l ⊕ l) (IsLocalRing.ResidueField R) := fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
F'_def : F' = fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
⊢ F'.det = f (fromBlocks A B C D).det
Module: Mathlib.Algebra.Lie.UniversalEnveloping

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ⇑g ∘ ⇑(ι R) = ⇑f ↔ g = (lift R) f

Tactic:
refine Iff.trans ?_ (lift R).symm_apply_eq
  constructor <;> · intro h; ext; simp [← h]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ a ∈ grade R m ↔ a.coeff.support ⊆ {m}

Tactic:
← Finset.coe_subset,

Goal state after:
M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ a ∈ grade R m ↔ ↑a.coeff.support ⊆ ↑{m}
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : 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
i : ι
x y : S ⊗[R] ↥(ℳ i)
h : (Submodule.toBaseChange S (ℳ i)) x = (Submodule.toBaseChange S (ℳ i)) y
⊢ Function.Bijective
    ⇑↑((LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)).trans
          (directSumRight R S S fun i ↦ ↥(ℳ i)))

Tactic:
exact LinearEquiv.bijective _

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
⊢ (inl ψ).range = LieIdeal.toLieSubalgebra R (K ⋊⁅ψ⁆ L) (projr ψ).ker

Tactic:
ext ⟨x, y⟩

Goal state after:
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
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
r : R
x y : ofTwoCocycle c
⊢ ⁅x, r • y⁆ = r • ⁅x, y⁆

Tactic:
simp only [bracket_ofTwoCocycle]
    exact Equiv.congr_arg (by simp [← smul_add, smul_sub])

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

Goal state before:
pp: case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s✝ : Cycle α
s : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ ∀ (x : α), s ≠ [x]

Tactic:
rintro _ rfl

Goal state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Cycle α
x✝ : α
h : Nodup (Quot.mk ⇑(IsRotated.setoid α) [x✝])
hn : Nontrivial (Quot.mk ⇑(IsRotated.setoid α) [x✝])
⊢ False
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ n) x = (p ^ m) x → n = m

Tactic:
←
    cycleOf_pow_apply_self p x m

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ n) x = (p.cycleOf x ^ m) x → n = m
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
⊢ LieModule R L M

Tactic:
let := E.ringModuleOf

Goal state after:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
this : LieRingModule L M := E.ringModuleOf
⊢ LieModule R L M
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
hy✝ : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : (p.toList x)[k] = y
⊢ (p ^ ((k + 1) % (p.cycleOf x).support.card)) x = (p ^ (k + 1)) x

Tactic:
rw [← pow_mod_orderOf_cycleOf_apply p (k + 1), IsCycle.orderOf]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
hy✝ : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : (p.toList x)[k] = y
⊢ (p.cycleOf x).IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k : ℕ
⊢ p.toList ((p ^ k) x) = (p.toList x).rotate k

Tactic:
by
  apply ext_getElem
  · simp only [length_toList, cycleOf_self_apply_pow, length_rotate]
  · intro n hn hn'
    rw [getElem_toList, getElem_rotate, getElem_toList, length_toList,
      pow_mod_card_support_cycleOf_self_apply, pow_add, mul_apply]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ f.toList x ~r f.toList y

Tactic:
rw [toList_eq_nil_iff.mpr hx, isRotated_nil_iff', eq_comm, toList_eq_nil_iff]
    rwa [← h.mem_support_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
⊢ ∀ (x : α), l ≠ [x]

Tactic:
rintro _ rfl

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x✝ : α
hl : 2 ≤ [x✝].length
hn : [x✝].Nodup
hc : [x✝].formPerm.IsCycle
⊢ False
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate ↑k
⊢ (l.rotate ↑k).Nodup

Tactic:
simpa using hn

Goal state after:
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
⊢ ∀ (x : α), s ≠ [x]

Tactic:
rintro _ rfl

Goal state after:
case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝¹ : α
val✝ : Cycle α
x x✝ : α
hn✝ : Cycle.Nodup (Quot.mk ⇑(IsRotated.setoid α) [x✝])
ht : Cycle.Nontrivial (Quot.mk ⇑(IsRotated.setoid α) [x✝])
hl : 2 ≤ [x✝].length
hn : [x✝].Nodup
hx : x ∈ [x✝]
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
α : Fin p → Fin n
k : Fin n
hnotmem :
  (α, k) ∉
    (fun x ↦
        match x with
        | (α, k) => (k.removeNth α, α k)) ''
      ↑(S (p + 1) i ×ˢ Finset.univ)
hα : α ∈ S p i
hk : i < k
hoccurs : k ∈ Set.range α
⊢ 0 * A (α, k).2 j = 0

Tactic:
zero_mul

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
α : Fin p → Fin n
k : Fin n
hnotmem :
  (α, k) ∉
    (fun x ↦
        match x with
        | (α, k) => (k.removeNth α, α k)) ''
      ↑(S (p + 1) i ×ˢ Finset.univ)
hα : α ∈ S p i
hk : i < k
hoccurs : k ∈ Set.range α
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

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

Tactic:
paper_eq3_eq5_off_diag A

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p✝ p : ℕ
ih : Eq1 A p
i j : Fin n
⊢ (-1) ^ (p + 1) *
      (∑ α ∈ S (p + 1) i, pminor A α * A i j -
        ∑ α' ∈ S (p + 1) i, ∑ t, bminor A i (α' t) (t.removeNth α') * A (α' t) j) =
    (-1) ^ (p + 1) *
      (∑ α ∈ S (p + 1) i, pminor A α * A i j - ∑ α ∈ S (p + 1) i, ∑ t, bminor A i (α t) (t.removeNth α) * A (α t) j)
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
imL : LieSubalgebra k (Module.End k V) := (toEnd k L V).range
toEndo : L →ₗ[k] ↥imL := LinearMap.codRestrict imL.toSubmodule ↑(toEnd k L V) ⋯
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
have ⟨χ, h⟩ := exists_forall_lie_eq_smul_of_isSolvable_of_finite k V imL

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
toEndo : L →ₗ[k] ↥imL := LinearMap.codRestrict imL.toSubmodule ↑(toEnd k L V) ⋯
χ : Module.Dual k ↥imL
h : Nontrivial ↥(weightSpace V ⇑χ)
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ (fun i ↦ p ^ ↑i) 1 = p

pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n✝ : ℕ
hn : n✝ ≠ 0
hp : Prime p
n m : Fin (n✝ + 1)
h : n < m
⊢ (fun i ↦ p ^ ↑i) n < (fun i ↦ p ^ ↑i) m

pp: case refine_3
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
h : y ≤ p ^ n
⊢ ∃ i, y = (fun i ↦ p ^ ↑i) i

pp: case refine_4
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
⊢ (∃ i, y = (fun i ↦ p ^ ↑i) i) → y ≤ p ^ n

Tactic:
· dsimp only
    rw [Fin.coe_ofNat_eq_mod, Nat.mod_eq_of_lt, pow_one]
    exact Nat.lt_succ_of_le (Nat.one_le_iff_ne_zero.mpr hn)

Goal state after:
case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n✝ : ℕ
hn : n✝ ≠ 0
hp : Prime p
n m : Fin (n✝ + 1)
h : n < m
⊢ (fun i ↦ p ^ ↑i) n < (fun i ↦ p ^ ↑i) m

case refine_3
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
h : y ≤ p ^ n
⊢ ∃ i, y = (fun i ↦ p ^ ↑i) i

case refine_4
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
⊢ (∃ i, y = (fun i ↦ p ^ ↑i) i) → y ≤ p ^ n
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n✝ : ℕ
hn : n✝ ≠ 0
hp : Prime p
n m : Fin (n✝ + 1)
h : n < m
⊢ (fun i ↦ p ^ ↑i) n < (fun i ↦ p ^ ↑i) m

Tactic:
exact Associates.dvdNotUnit_iff_lt.mp
        ⟨pow_ne_zero n hp.ne_zero, p ^ (m - n : ℕ),
          not_isUnit_of_not_isUnit_dvd hp.not_isUnit (dvd_pow dvd_rfl (Nat.sub_pos_of_lt h).ne'),
          (pow_mul_pow_sub p h.le).symm⟩

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ.refine_2.inr.refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
j : Fin (n + 1)
hp : Prime (c j.succ)
hp' : c j.succ ∣ r
hi : 1 < j.succ
⊢ DvdNotUnit (c j.castSucc) (c j.succ)

Tactic:
refine Associates.dvdNotUnit_iff_lt.2 (h₁ ?_)
    simpa only [Fin.coe_eq_castSucc] using Fin.castSucc_lt_succ

Goal state after:
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 α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
hspan_compl_roots_vanish : ∀ μ ∈ I.rootSet, ↑span_compl_roots ≤ Weight.ker
hx_top : ⟨x, hxH⟩ ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ ↑span_I_roots
b : ↥H
hb : b ∈ ↑span_compl_roots
hab : a + b = ⟨x, hxH⟩
haI : ↑a ∈ I
hbI : ↑b ∈ I
⊢ x ∈ ⨆ α ∈ I.rootSet, corootSubmodule ↑α

Tactic:
suffices b = 0 by
    subst this; simp only [add_zero] at hab; subst hab
    exact hspan_I_roots_incl ▸ LieSubmodule.mem_map_of_mem ha

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 α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
hspan_compl_roots_vanish : ∀ μ ∈ I.rootSet, ↑span_compl_roots ≤ Weight.ker
hx_top : ⟨x, hxH⟩ ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ ↑span_I_roots
b : ↥H
hb : b ∈ ↑span_compl_roots
hab : a + b = ⟨x, hxH⟩
haI : ↑a ∈ I
hbI : ↑b ∈ I
⊢ b = 0