mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M := span R (⇑P.root ∘ Subtype.val '' {i | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), P.root ↑k ∈ q ↔ p k
hq_notMem : ∀ (k : ↥b.support), P.root ↑k ∉ q → q ≤ LinearMap.ker (P.coroot' ↑k)
k : ι
hkb : k ∈ b.support
x : M
hx : x ∈ q
hk : P.root k ∉ q
⊢ (P.coroot' k) x • P.root k ∈ q

Tactic:
replace hk : P.coroot' k x = 0 := hq_notMem ⟨k, hkb⟩ hk hx
      simp [hk]

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
this : (reindex b.baseSupportEquiv.symm b.baseSupportEquiv.symm) b.base.cartanMatrix = b.A
⊢ b.base.cartanMatrix = (reindex b.baseSupportEquiv b.baseSupportEquiv) b.A

Tactic:
rwa [← (reindex b.baseSupportEquiv b.baseSupportEquiv).symm_apply_eq]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
h_deg_le : f.degree ≤ ↑(#s)
h_deg_eq : f.degree = g.degree
hlc : f.leadingCoeff = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x f = eval x g
⊢ f = g

Tactic:
rcases eq_or_ne f 0 with rfl | hf
  · rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq
  · exact eq_of_degree_sub_lt_of_eval_finset_eq s
      (lt_of_lt_of_le (degree_sub_lt_left h_deg_eq hf hlc) h_deg_le) h_eval

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : basisDivisor x y = 0
⊢ x = y

Tactic:
basisDivisor,

Goal state after:
F : Type u_1
inst✝ : Field F
x y : F
hxy : C (x - y)⁻¹ * (X - C y) = 0
⊢ x = y
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (basisDivisor x y).degree = 1

Tactic:
basisDivisor,

Goal state after:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (C (x - y)⁻¹ * (X - C y)).degree = 1
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x : F
⊢ (basisDivisor x x).degree = ⊥

Tactic:
rw [basisDivisor_self, degree_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ ∑ j ∈ s, Lagrange.basis s v j = 1

Tactic:
refine eq_of_degrees_lt_of_eval_index_eq s hvs (lt_of_le_of_lt (degree_sum_le _ _) ?_) ?_ ?_

Goal state after:
case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ (s.sup fun b ↦ (Lagrange.basis s v b).degree) < ↑(#s)

case refine_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ degree 1 < ↑(#s)

case refine_3
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ ∀ i ∈ s, eval (v i) (∑ j ∈ s, Lagrange.basis s v j) = eval (v i) 1
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = basisDivisor (id x) (id y) + basisDivisor (id y) (id x)

Tactic:
id,

Goal state after:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = basisDivisor x (id y) + basisDivisor (id y) x
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
j : Fin n
a✝ : j.succ ∈ univ
hj0 : j.succ ≠ 0
⊢ ((-1) ^ ↑j.succ = 0 ∨ W 0 j.succ = 0) ∨ (W.submatrix succ j.succ.succAbove).det = 0

Tactic:
refine .inl (.inr ?_)

Goal state after:
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
j : Fin n
a✝ : j.succ ∈ univ
hj0 : j.succ ≠ 0
⊢ W 0 j.succ = 0
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ ∏ i, ∏ j > succAbove 0 i, (↑↑j - ↑↑(succAbove 0 i)) = ↑n.superFactorial

Tactic:
det_vandermonde

Goal state after:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : ∏ i, ∏ j > i, (↑↑j - ↑↑i) = ↑n.superFactorial
⊢ ∏ i, ∏ j > succAbove 0 i, (↑↑j - ↑↑(succAbove 0 i)) = ↑n.superFactorial
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ (interpolate (insert i (s \ {i, j})) v) r * basisDivisor (v i) (v j) +
      (interpolate (insert j (s \ {i, j})) v) r * Lagrange.basis {i, j} v j =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ {i, j} ⊆ s

Tactic:
basis_pair_right hij,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ (interpolate (insert i (s \ {i, j})) v) r * basisDivisor (v i) (v j) +
      (interpolate (insert j (s \ {i, j})) v) r * basisDivisor (v j) (v i) =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ {i, j} ⊆ s
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H := { toFun := fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → K n = K m
y : ↥H
h : ↑y ∈ engel R ↑x
⊢ ((ad R L) ↑x ^ n) ↑y = ↑(0 y)

Tactic:
rw [mem_engel_iff] at h

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H := { toFun := fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → K n = K m
y : ↥H
h : ∃ n, ((ad R L) ↑x ^ n) ↑y = 0
⊢ ((ad R L) ↑x ^ n) ↑y = ↑(0 y)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
⊢ ∏ j ∈ s.erase i, basisDivisor (v i) (v j) = C (nodalWeight s v i) * (nodal s v / (X - C (v i)))

Tactic:
basisDivisor,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
⊢ ∏ j ∈ s.erase i, C (v i - v j)⁻¹ * (X - C (v j)) = C (nodalWeight s v i) * (nodal s v / (X - C (v i)))
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x ∈ antidiagonal c, coeff x.1 φ * coeff x.2 ψ ≠ 0
⊢ (weight w) c = m + n

Tactic:
obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x ∈ antidiagonal c, coeff x.1 φ * coeff x.2 ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ antidiagonal c
H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0
⊢ (weight w) c = m + n
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ weightedTotalDegree (fun i ↦ {i}) p = p.degrees

Tactic:
by
  rw [degrees_def]; rfl

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ (weight w) d < n

Tactic:
exact lt_of_le_of_lt (le_weightedTotalDegree w hd.1) h

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Free R M
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
tfae_2_to_3 : charpoly φ = X ^ finrank R M → ∀ (m : M), ∃ n, (φ ^ n) m = 0
tfae_3_to_1 : (∀ (m : M), ∃ n, (φ ^ n) m = 0) → IsNilpotent φ
⊢ [IsNilpotent φ, charpoly φ = X ^ finrank R M, ∀ (m : M), ∃ n, (φ ^ n) m = 0,
      (charpoly φ).natTrailingDegree = finrank R M].TFAE

Tactic:
tfae_have 2 ↔ 4 := by
    rw [← φ.charpoly_natDegree, φ.charpoly_monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree]

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Free R M
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
tfae_2_to_3 : charpoly φ = X ^ finrank R M → ∀ (m : M), ∃ n, (φ ^ n) m = 0
tfae_3_to_1 : (∀ (m : M), ∃ n, (φ ^ n) m = 0) → IsNilpotent φ
tfae_2_iff_4 : charpoly φ = X ^ finrank R M ↔ (charpoly φ).natTrailingDegree = finrank R M
⊢ [IsNilpotent φ, charpoly φ = X ^ finrank R M, ∀ (m : M), ∃ n, (φ ^ n) m = 0,
      (charpoly φ).natTrailingDegree = finrank R M].TFAE
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
⊢ (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w)) (decompose' R w φ) =
    ∑ᶠ (m : M), (weightedHomogeneousComponent w m) φ

Tactic:
← DirectSum.sum_support_of (decompose' R w φ)

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
⊢ (DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w))
      (∑ i ∈ DFinsupp.support (decompose' R w φ),
        (DirectSum.of (fun i ↦ ↥(weightedHomogeneousSubmodule R w i)) i) ((decompose' R w φ) i)) =
    ∑ᶠ (m : M), (weightedHomogeneousComponent w m) φ
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'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥f.range →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set V
hsc : lift.{v', v} #↑s = lift.{v, v'} c
si : LinearIndepOn K (⇑f) s
⊢ LinearIndependent (ι := ↑s) K (⇑f.range.subtype ∘ fun x ↦ f.rangeRestrict ↑x)

Tactic:
convert! si

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✝ : Invertible A
hA : fromBlocks A B C D ∈ symplecticGroup l R
h_block : Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1
⊢ A.det * (D - C * ⅟A * B).det = 1

Tactic:
invOf_eq_nonsing_inv,

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✝ : Invertible A
hA : fromBlocks A B C D ∈ symplecticGroup l R
h_block : Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1
⊢ A.det * (D - C * A⁻¹ * B).det = 1
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝³ : Field R
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq R
w : m → R
⊢ (diagonal w).rank = Fintype.card { i // w i ≠ 0 }

Tactic:
rw [Matrix.rank, ← Matrix.toLin'_apply', Module.finrank, ← LinearMap.rank,
    LinearMap.rank_diagonal, Cardinal.toNat_natCast]

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

Goal state before:
pp: m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
i✝ j✝ : m
⊢ (diagonal E * diagonal D) i✝ j✝ = diagonal (fun i ↦ if i ∈ s then 1 else 0) i✝ j✝

Tactic:
simp only [E_def, mul_diagonal, diagonal_apply, ite_mul, one_mul, zero_mul, s_def,
      Finset.mem_filter, Finset.mem_univ, true_and, ite_not]

Goal state after:
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
i✝ j✝ : m
⊢ (if i✝ = j✝ then if D i✝ = 0 then D j✝ else (D i✝)⁻¹ * D j✝ else 0) = if i✝ = j✝ then if D i✝ = 0 then 0 else 1 else 0
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
i✝ : ι
⊢ (((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)) ∘ₗ
      lof S ι (fun i ↦ ↥(Submodule.baseChange S (ℳ i))) i✝ =
    LinearMap.id ∘ₗ lof S ι (fun i ↦ ↥(Submodule.baseChange S (ℳ i))) i✝

Tactic:
rw [← LinearMap.cancel_right ((ℳ _).toBaseChange_surjective S)]

Goal state after:
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
i✝ : ι
⊢ ((((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)) ∘ₗ
        lof S ι (fun i ↦ ↥(Submodule.baseChange S (ℳ i))) i✝) ∘ₗ
      Submodule.toBaseChange S (ℳ i✝) =
    (LinearMap.id ∘ₗ lof S ι (fun i ↦ ↥(Submodule.baseChange S (ℳ i))) i✝) ∘ₗ Submodule.toBaseChange S (ℳ i✝)
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, ((toEnd k L ↥W) z).HasEigenvalue c

Tactic:
have : Nontrivial W := inferInstanceAs (Nontrivial (weightSpace V χ₀))
    apply Module.End.exists_hasEigenvalue_of_genEigenspace_eq_top
    exact LieModule.IsTriangularizable.maxGenEigenspace_eq_top z

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

Goal state before:
pp: case h.refine_1
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
⊢ StrictMono (t.insertNth k α)

pp: case h.refine_2
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin (p + 1)
⊢ i < t.insertNth k α t

pp: case h.refine_3
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin (p + 1)
⊢ ∀ (j : Fin p), i < t.insertNth k α (t.succAbove j)

Tactic:
· simp only [t_eq, Set.mem_ofPred_eq, Fin.strictMono_insertNth_iff, hα.2, lt_iInf_iff,
      le_iInf_iff, forall_exists_index, and_imp, iInf_le_iff_forall_lt, iInf_lt_iff,
      exists_prop, true_and]
    refine ⟨fun j x hjx h ↦ ?_, fun j h ↦ ?_⟩
    · contrapose! h
      have k_ne (j : Fin p) : k ≠ α j := fun hj ↦ hk ⟨j, hj.symm⟩
      exact ⟨j, h.lt_of_ne (k_ne _), hjx⟩
    · obtain ⟨q, hkq, hqj⟩ := h j.succ j.castSucc_lt_succ
      exact hkq.trans_le <| hα.2.monotone <| Fin.castSucc_lt_succ_iff.mp hqj

Goal state after:
case h.refine_2
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin (p + 1)
⊢ i < t.insertNth k α t

case h.refine_3
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin (p + 1)
⊢ ∀ (j : Fin p), i < t.insertNth k α (t.succAbove j)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ Set.InjOn
    (fun x ↦
      match x with
      | (α, k) => (k.removeNth α, α k))
    ↑(S (p + 1) i ×ˢ Finset.univ)

pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ Set.MapsTo
    (fun x ↦
      match x with
      | (α, k) => (k.removeNth α, α k))
    ↑(S (p + 1) i ×ˢ Finset.univ) ↑(S p i ×ˢ Finset.Ioi i)

pp: case refine_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S p i ×ˢ Finset.Ioi i,
    i_1 ∉
        (fun x ↦
            match x with
            | (α, k) => (k.removeNth α, α k)) ''
          ↑(S (p + 1) i ×ˢ Finset.univ) →
      bminor A i i_1.2 i_1.1 * A i_1.2 j = 0

pp: case refine_4
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S (p + 1) i ×ˢ Finset.univ,
    bminor A i (i_1.1 i_1.2) (i_1.2.removeNth i_1.1) * A (i_1.1 i_1.2) j =
      bminor A i
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).1 *
        A
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          j

Tactic:
· simp only [Set.InjOn, Finset.coe_product, Finset.coe_univ, Set.mem_prod, Set.mem_univ,
      and_true, Finset.mem_coe, Prod.mk.injEq, and_imp, Prod.forall, mem_S_iff, Fin.strictMono_cons]
    intros α k hi hiα α' k' hj hiα' hremove hvalue
    suffices hrange : Set.range α = Set.range α' by
      rw [hiα.range_inj hiα'] at hrange
      subst α'
      exact ⟨rfl, hiα.injective hvalue⟩
    calc
      _ = Set.insert (α k) (Set.range (k.removeNth α)) := by
        rw [← Fin.range_insertNth, Fin.insertNth_self_removeNth]
      _ = Set.insert (α' k') (Set.range (k'.removeNth α')) := by
        rw [hvalue, hremove]
      _ = Set.range α' := by
        rw [← Fin.range_insertNth, Fin.insertNth_self_removeNth]

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
⊢ Set.MapsTo
    (fun x ↦
      match x with
      | (α, k) => (k.removeNth α, α k))
    ↑(S (p + 1) i ×ˢ Finset.univ) ↑(S p i ×ˢ Finset.Ioi i)

case refine_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S p i ×ˢ Finset.Ioi i,
    i_1 ∉
        (fun x ↦
            match x with
            | (α, k) => (k.removeNth α, α k)) ''
          ↑(S (p + 1) i ×ˢ Finset.univ) →
      bminor A i i_1.2 i_1.1 * A i_1.2 j = 0

case refine_4
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S (p + 1) i ×ˢ Finset.univ,
    bminor A i (i_1.1 i_1.2) (i_1.2.removeNth i_1.1) * A (i_1.1 i_1.2) j =
      bminor A i
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).1 *
        A
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          j