mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: case h
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
x✝ : ∀ (m : M), ∃ n, (φ ^ n) m = 0
h : ∀ (m : M), ∃ n, (φ ^ n) m = 0 := x✝
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → ⨆ m, (φ ^ m).ker = (φ ^ b).ker
x : M
⊢ x ∈ ⨆ m, (φ ^ m).ker

Tactic:
obtain ⟨k, hk⟩ := h x

Goal state after:
case h
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
x✝ : ∀ (m : M), ∃ n, (φ ^ n) m = 0
h : ∀ (m : M), ∃ n, (φ ^ n) m = 0 := x✝
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → ⨆ m, (φ ^ m).ker = (φ ^ b).ker
x : M
k : ℕ
hk : (φ ^ k) x = 0
⊢ x ∈ ⨆ m, (φ ^ m).ker
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case h
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
F : MvPolynomial (Fin 0) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
⊢ (eval 0) F ≠ 0

Tactic:
contrapose hF₀

Goal state after:
case h
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
F : MvPolynomial (Fin 0) R
n : ℕ
hF : F.IsHomogeneous n
hnR : ↑n ≤ #R
hF₀ : (eval 0) F = 0
⊢ F = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
⊢ finrank K ↥V = F.charpoly.natTrailingDegree + G.charpoly.natTrailingDegree

Tactic:
rw [hG, add_zero, eq_comm]

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
⊢ F.charpoly.natTrailingDegree = finrank K ↥V
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
F : MvPolynomial (Fin N) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
⊢ ∃ r, (eval r) F ≠ 0

Tactic:
induction N generalizing n with
  | zero =>
    use 0
    contrapose hF₀
    ext d
    simpa only [Subsingleton.elim d 0, eval_zero, coeff_zero] using! hF₀
  | succ N IH =>
    have hdeg : natDegree (finSuccEquiv R N F) < n + 1 := by
      linarith [natDegree_finSuccEquiv F, degreeOf_le_totalDegree F 0, hF.totalDegree hF₀]
    obtain ⟨i, hi⟩ : ∃ i : ℕ, (finSuccEquiv R N F).coeff i ≠ 0 := by
      contrapose! hF₀
      exact (finSuccEquiv _ _).injective <| Polynomial.ext <| by simpa using! hF₀
    have hin : i ≤ n := by
      contrapose! hi
      exact coeff_eq_zero_of_natDegree_lt <| (Nat.le_of_lt_succ hdeg).trans_lt hi
    obtain hFn | hFn := ne_or_eq ((finSuccEquiv R N F).coeff n) 0
    · exact hF.exists_eval_ne_zero_of_coeff_finSuccEquiv_ne_zero_aux hFn
    have hin : i < n := hin.lt_or_eq.elim id <| by aesop
    obtain ⟨j, hj⟩ : ∃ j, i + (j + 1) = n := (Nat.exists_eq_add_of_lt hin).imp <| by lia
    obtain ⟨r, hr⟩ : ∃ r, (eval r) (Polynomial.coeff ((finSuccEquiv R N) F) i) ≠ 0 :=
      IH (hF.finSuccEquiv_coeff_isHomogeneous _ _ hj) hi (.trans (by norm_cast; lia) hnR)
    set φ : R[X] := Polynomial.map (eval r) (finSuccEquiv _ _ F) with hφ
    have hφ₀ : φ ≠ 0 := fun hφ₀ ↦ hr <| by
      rw [← coeff_eval_eq_eval_coeff, ← hφ, hφ₀, Polynomial.coeff_zero]
    have hφR : φ.natDegree < #R := by
      refine lt_of_lt_of_le ?_ hnR
      norm_cast
      refine lt_of_le_of_lt natDegree_map_le ?_
      suffices (finSuccEquiv _ _ F).natDegree ≠ n by lia
      rintro rfl
      refine leadingCoeff_ne_zero.mpr ?_ hFn
      simpa using! (finSuccEquiv R N).injective.ne hF₀
    obtain ⟨r₀, hr₀⟩ : ∃ r₀, Polynomial.eval r₀ φ ≠ 0 :=
      φ.exists_eval_ne_zero_of_natDegree_lt_card hφ₀ hφR
    use Fin.cons r₀ r
    rwa [eval_eq_eval_mv_eval']

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

Goal state before:
pp: R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
hnR : ↑n ≤ #R
⊢ F = G

Tactic:
← sub_eq_zero

Goal state after:
R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
hnR : ↑n ≤ #R
⊢ F - G = 0
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ φ.nilRankAux b = (φ.polyCharpoly b').natTrailingDegree

Tactic:
apply le_antisymm <;> apply nilRankAux_le

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

Goal state before:
pp: case monomial
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
τ : Type u_5
φ : σ → τ
n : ℕ
d : σ →₀ ℕ
c : R
⊢ (rename φ) (if n = degree d then (monomial d) c else 0) = if n = degree d then (monomial (mapDomain φ d)) c else 0

Tactic:
split_ifs <;> simp [rename_monomial]

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
⊢ χ ⁅x, y⁆ = 0

Tactic:
rw [LieHom.map_lie, LieRing.of_associative_ring_bracket, mul_comm, sub_self]

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

Goal state before:
pp: p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
⊢ Pso p q R i * Pso p q R (-i) = 1

Tactic:
ext (x y)

Goal state after:
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p ⊕ q
⊢ (Pso p q R i * Pso p q R (-i)) x y = 1 x y
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
⊢ (Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i = 1

Tactic:
ext (x y)

Goal state after:
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p ⊕ q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) x y = 1 x y
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
⊢ det 1 = 1

Tactic:
det_one

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
⊢ 1 = 1
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
⊢ A.rank ≤ s.card

Tactic:
set B : Matrix m {x // x ∈ s} R := Matrix.of fun i a => if (a : m) = i then 1 else 0 with hBdef
  have hB : B * A.submatrix Subtype.val id = A := by
    ext i j
    simp only [hBdef, mul_apply, of_apply, submatrix_apply, id_eq]
    by_cases hi : i ∈ s
    · rw [Fintype.sum_eq_single (⟨i, hi⟩ : {x // x ∈ s})
        fun a ha => by rw [if_neg fun he => ha (Subtype.ext he), zero_mul], if_pos rfl, one_mul]
    · have h0 : A i = 0 := hz i hi
      aesop
  calc A.rank = (B * A.submatrix Subtype.val id).rank := by rw [hB]
    _ ≤ (A.submatrix Subtype.val id).rank := rank_mul_le_right _ _
    _ ≤ Fintype.card {x // x ∈ s} := rank_le_card_height _
    _ = s.card := Fintype.card_coe s

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
con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
⊢ IsUnit (f Q).toBlocks₂₂

Tactic:
refine mulVec_injective_iff_isUnit.1 ?_

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
con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
⊢ Function.Injective (f Q).toBlocks₂₂.mulVec
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✝ : Derivation R A A
z : A ⊗[R] L
⊢ ∀ (x : A) (y : L),
    { toFun := ⇑(LinearMap.rTensor L ↑⁅x✝¹, x✝⁆), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } (x ⊗ₜ[R] y) =
      ⁅{ toFun := ⇑(LinearMap.rTensor L ↑x✝¹), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ },
          { toFun := ⇑(LinearMap.rTensor L ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }⁆
        (x ⊗ₜ[R] y)

Tactic:
simp [sub_tmul]

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 a b
⊢ Rel R X (a - c) (b - c)

Tactic:
by
  simpa only [sub_eq_add_neg] using h.add_right (-c)

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

Goal state before:
pp: case of
ι : 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 ℳ
i : ι
y : ↥(ℳ i) ⊗[R] N
this :
  (rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) y)
⊢ (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ))
      ((DirectSum.coeAddMonoidHom (decomposeTensor ℳ N))
        ((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩)) =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm
      ((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm
        ((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩))

Tactic:
coeAddMonoidHom_of,

Goal state after:
case of
ι : 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 ℳ
i : ι
y : ↥(ℳ i) ⊗[R] N
this :
  (rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) y)
⊢ (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ)) ↑⟨(rTensor N (ℳ i).subtype) y, ⋯⟩ =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm
      ((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm
        ((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩))
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: case of
ι : 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 ℳ
i : ι
y : ↥(ℳ i) ⊗[R] N
this :
  (rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) y)
⊢ (congrLinearEquiv (decomposeTensorEquiv ℳ N))
      ((directSumLeft R R (fun i ↦ ↥(ℳ i)) N) ((rTensor N (↑(decomposeLinearEquiv ℳ) ∘ₗ (ℳ i).subtype)) y)) =
    (of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩

Tactic:
decomposeLinearEquiv_comp_subtype,

Goal state after:
case of
ι : 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 ℳ
i : ι
y : ↥(ℳ i) ⊗[R] N
this :
  (rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) y)
⊢ (congrLinearEquiv (decomposeTensorEquiv ℳ N))
      ((directSumLeft R R (fun i ↦ ↥(ℳ i)) N) ((rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y)) =
    (of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩
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 c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h : ↑c' = ↑c + (d₁₂ R L M) x
x✝¹ x✝ : ofTwoCocycle c
⊢ (ofProd c') (((ofProd c).symm (x✝¹ + x✝)).1, ((ofProd c).symm (x✝¹ + x✝)).2 - x ((ofProd c).symm (x✝¹ + x✝)).1) =
    (ofProd c') (((ofProd c).symm x✝¹).1, ((ofProd c).symm x✝¹).2 - x ((ofProd c).symm x✝¹).1) +
      (ofProd c') (((ofProd c).symm x✝).1, ((ofProd c).symm x✝).2 - x ((ofProd c).symm x✝).1)

Tactic:
simp [← of_add]

Goal state after:
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 c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h : ↑c' = ↑c + (d₁₂ R L M) x
x✝¹ x✝ : ofTwoCocycle c
⊢ ((ofProd c).symm x✝¹).2 + ((ofProd c).symm x✝).2 - (x ((ofProd c).symm x✝¹).1 + x ((ofProd c).symm x✝).1) =
    ((ofProd c).symm x✝¹).2 - x ((ofProd c).symm x✝¹).1 + (((ofProd c).symm x✝).2 - x ((ofProd c).symm x✝).1)
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✝⁴ : LieRing M
inst✝³ : LieAlgebra R M
inst✝² : IsLieAbelian M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x✝¹ x✝ : M
⊢ (ofProd c) (0, x✝¹ + x✝) = (ofProd c) (0, x✝¹) + (ofProd c) (0, x✝)

Tactic:
simp [← of_add]

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

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ ∀ ⦃y_1 : α⦄, (x :: y :: l).formPerm y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1

Tactic:
intro w

Goal state after:
case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
w : α
⊢ (x :: y :: l).formPerm w ≠ w → (x :: y :: l).formPerm.SameCycle x w
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ↑(map (Finset.card ∘ support) [l.attach.formPerm]) = {l.length}

Tactic:
simp only [map, Function.comp_apply]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ↑[l.attach.formPerm.support.card] = {l.length}
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s ↦ (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
⊢ s.Nontrivial

Tactic:
rw [hn.nontrivial_iff]

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s ↦ (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
⊢ ¬s.Subsingleton
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
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:
simpa using hα.1

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x✝ : P
hx : x✝ ∈ ↑I
⊢ (DistribSMul.toLinearMap R P I.den) x✝ ∈ Submodule.map (Algebra.linearMap R P) I.num

Tactic:
rw [← den_mul_self_eq_num]

Goal state after:
case refine_1
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : FaithfulSMul R P
I : FractionalIdeal S P
reg : IsSMulRegular P I.den
x✝ : P
hx : x✝ ∈ ↑I
⊢ (DistribSMul.toLinearMap R P I.den) x✝ ∈ I.den • ↑I
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ι : Type u_1
A : Matrix ι ι ℤ
⊢ Aᵀ.IsSimplyLaced ↔ A.IsSimplyLaced

Tactic:
rw [IsSimplyLaced, IsSimplyLaced, Pairwise, Pairwise, forall_comm]

Goal state after:
ι : 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
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
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K) y' = aJ • y
⊢ y' ≠ 0

Tactic:
intro y'_eq_zero

Goal state after:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
⊢ False