mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: case inr
α : Type u_1
m : Type u_2
n : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
a b : α
h✝ : ¬ja = jb
⊢ single ia ja a ⊙ single ib jb b = 0

Tactic:
(simp only [single]; aesop)

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

Goal state before:
pp: case succ.succ.inl
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)

pp: case succ.succ.inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ = 0
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)

Tactic:
· calc
        A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n := by
          simp only [pow_succ A⁻¹, pow_succ' A, Matrix.mul_assoc]
        _ = A ^ n * A⁻¹ ^ m := by simp only [h, Matrix.mul_one, IH m]
        _ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one]
        _ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by
          simp only [pow_succ A, pow_succ' A⁻¹, Matrix.mul_assoc]

Goal state after:
case succ.succ.inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ = 0
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ 0 ^ (n + 1) = 0 ^ (n + 2) * A

Tactic:
zero_pow <| Nat.succ_ne_zero _,

Goal state after:
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ 0 = 0 * A
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case pos
ι : 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

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:
· exact q.smul_mem _ hk

Goal state after:
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
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: ι : 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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
this : ∀ (k : ι), P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k
⊢ (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix

Tactic:
ext; simp [f', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: n : ℕ
⊢ eval n (ascPochhammer ℕ 0) = n.ascFactorial 0

Tactic:
ascPochhammer_zero,

Goal state after:
n : ℕ
⊢ eval n 1 = n.ascFactorial 0
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case zero
⊢ 1 = (ascPochhammer ℤ 0).comp (X - ↑0 + 1)

Tactic:
ascPochhammer_zero,

Goal state after:
case zero
⊢ 1 = comp 1 (X - ↑0 + 1)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case zero
R : Type u
inst✝ : Ring R
r : R
⊢ 1 = eval (r - ↑0 + 1) (ascPochhammer R 0)

Tactic:
ascPochhammer_zero,

Goal state after:
case zero
R : Type u
inst✝ : Ring R
r : R
⊢ 1 = eval (r - ↑0 + 1) 1
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
⊢ eval (-r) (ascPochhammer R 0) = (-1) ^ 0 * eval r (descPochhammer R 0)

Tactic:
ascPochhammer_zero,

Goal state after:
R : Type u
inst✝ : Ring R
r : R
⊢ eval (-r) 1 = (-1) ^ 0 * eval r (descPochhammer R 0)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
⊢ eval (-r) (ascPochhammer R 0) = (-1) ^ 0 * eval r (descPochhammer R 0)

Tactic:
rw [ascPochhammer_zero, descPochhammer_zero]
    simp only [eval_one, pow_zero, mul_one]

Goal state after:
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
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
i₀ : Fin (n + 1)
hi₀ : w i₀ ≠ 0
⊢ ↑↑(Perm.sign (swap 0 i₀)) ≠ 0

Tactic:
simp [show 0 ≠ i₀ by rintro rfl; contradiction]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v : ι → F
i : ι
⊢ ∏ j ∈ ∅, basisDivisor (v i) (v j) = 1

Tactic:
prod_empty

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v : ι → F
i : ι
⊢ 1 = 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 = 1

Tactic:
classical
  rw [← sum_basis Function.injective_id.injOn ⟨x, mem_insert_self _ {y}⟩,
    sum_insert (notMem_singleton.mpr hxy), sum_singleton, basis_pair_left hxy,
    basis_pair_right hxy, id, id]

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

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
⊢ Surjective ⇑((LieHom.fst R L₁ L₂).comp L.incl)

Tactic:
set p₁ : L →ₗ⁅R⁆ L₁ := (LieHom.fst R L₁ L₂).comp L.incl

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅R⁆ L₁ := (LieHom.fst R L₁ L₂).comp L.incl
⊢ Surjective ⇑p₁
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
x y : L
n : ℕ
hn : ((ad R L) x ^ n) ⁅x, y⁆ = 0
⊢ ((ad R L) x ^ n * (ad R L) x) y = 0

Tactic:
Module.End.mul_apply

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
n : ℕ
hn : ((ad R L) x ^ n) ⁅x, y⁆ = 0
⊢ ((ad R L) x ^ n) (((ad R L) x) y) = 0
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ IsHomogeneous 𝒜 I ↔ ∃ S, I = span (Subtype.val '' S)

Tactic:
Ideal.IsHomogeneous.iff_eq,

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ (homogeneousCore 𝒜 I).toIdeal = I ↔ ∃ S, I = span (Subtype.val '' S)
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: case h
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
n : ℕ
y : M
H : ∀ (i : ℕ), ∃ y_1, (φ ^ i) y_1 = (φ ^ n) y
⊢ (φ * φ ^ n) y = φ ((φ ^ n) y)

Tactic:
Module.End.mul_apply

Goal state after:
case h
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
n : ℕ
y : M
H : ∀ (i : ℕ), ∃ y_1, (φ ^ i) y_1 = (φ ^ n) y
⊢ φ ((φ ^ n) y) = φ ((φ ^ n) y)
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

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

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

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

Goal state before:
pp: m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ (fun i ↦ Submodule.map (toLin' (diagonal w)) (LinearMap.single K (fun a ↦ K) i).range) = fun i ↦
    ⨆ (_ : w i ≠ 0), (LinearMap.single K (fun x ↦ K) i).range

Tactic:
funext i

Goal state after:
m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
i : m
⊢ Submodule.map (toLin' (diagonal w)) (LinearMap.single K (fun a ↦ K) i).range =
    ⨆ (_ : w i ≠ 0), (LinearMap.single K (fun x ↦ K) i).range
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
⊢ A ∈ so n R ↔ Aᵀ = -A

Tactic:
by
  rw [so, mem_skewAdjointMatricesLieSubalgebra, mem_skewAdjointMatricesSubmodule]
  simp only [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, Matrix.mul_one, Matrix.one_mul]

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
h_eq : Submodule.map f (span R (range A.col)) = span R (range (A.submatrix r id).col)
⊢ lift.{um, max uR um₀} (A.submatrix r id).cRank ≤ lift.{um₀, max uR um} A.cRank

Tactic:
rw [cRank, ← h_eq]

Goal state after:
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
h_eq : Submodule.map f (span R (range A.col)) = span R (range (A.submatrix r id).col)
⊢ lift.{um, max uR um₀} (Module.rank R ↥(Submodule.map f (span R (range A.col)))) ≤ lift.{um₀, max uR um} A.cRank
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
w : m → R
v : n → R
⊢ (vecMulVec w v).rank ≤ 1

Tactic:
by
  rw [Matrix.vecMulVec_eq Unit]
  refine le_trans (rank_mul_le_left _ _) ?_
  nontriviality R
  exact rank_le_card_width _

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
A : Matrix m n R
⊢ A.eRank.toNat = A.rank

Tactic:
by
  rw [eRank_toNat_eq_finrank, ← rank_eq_finrank_span_cols]

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

Goal state before:
pp: case h.refine_2
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
α : 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
k : ℕ
hk : n = k + 1
hsψ : z' ≠ 0
⊢ ((toEnd K (↥U) Q) (α • u + x')) (((toEnd K (↥U) Q) v ^ k) z') = ((toEnd K (↥U) Q) v * (toEnd K (↥U) Q) v ^ k) z'

Tactic:
Module.End.mul_apply

Goal state after:
case h.refine_2
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
α : 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
k : ℕ
hk : n = k + 1
hsψ : z' ≠ 0
⊢ ((toEnd K (↥U) Q) (α • u + x')) (((toEnd K (↥U) Q) v ^ k) z') = ((toEnd K (↥U) Q) v) (((toEnd K (↥U) Q) v ^ k) z')
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mul_left
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b c' b✝ c✝ : lib R X
a✝ : Rel R X b✝ c✝
h₂ : (liftAux R f) b✝ = (liftAux R f) c✝
⊢ (liftAux R f) (c' * b✝) = (liftAux R f) (c' * c✝)

Tactic:
simp only [liftAux_map_mul, h₂]

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

Goal state before:
pp: case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c' : lib R X
a✝ : Rel R X a✝¹ b✝
h₂ : (liftAux R f) a✝¹ = (liftAux R f) b✝
⊢ (liftAux R f) (a✝¹ * c') = (liftAux R f) (b✝ * c')

Tactic:
simp only [liftAux_map_mul, h₂]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A := (F x).support ∪ (F y).support
hu₁ : (F x).support ⊆ u
hu₂ : (F y).support ⊆ u
a : A
ha : a ∈ (F (x + y)).support
⊢ (F x) a + (F y) a ≠ 0

Tactic:
simpa using ha

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 : α
hx : ¬f x = x
y : α
hy : ¬f.SameCycle x y
⊢ y ∉ f.toList x

Tactic:
simp [mem_toList_iff, hy]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ D n i i = 2

Tactic:
simp [D, Matrix.of_apply]

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
x y : Fin E.order → R
i : Fin E.order
h : ↑i + 1 < E.order
⊢ (x + y) ⟨↑i + 1, h⟩ =
    ((fun i ↦ if h : ↑i + 1 < E.order then x ⟨↑i + 1, h⟩ else ∑ i, E.coeffs i * x i) + fun i ↦
        if h : ↑i + 1 < E.order then y ⟨↑i + 1, h⟩ else ∑ i, E.coeffs i * y i)
      i

Tactic:
simp [h, mul_add, sum_add_distrib]

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
x y : Fin E.order → R
i : Fin E.order
h : ¬↑i + 1 < E.order
⊢ ∑ i, E.coeffs i * (x + y) i =
    ((fun i ↦ if h : ↑i + 1 < E.order then x ⟨↑i + 1, h⟩ else ∑ i, E.coeffs i * x i) + fun i ↦
        if h : ↑i + 1 < E.order then y ⟨↑i + 1, h⟩ else ∑ i, E.coeffs i * y i)
      i

Tactic:
simp [h, mul_add, sum_add_distrib]

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
α β : ↥LieSubalgebra.root
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
hγ : rootSpace H ⇑(S.root' γ) ≤ LieSubmodule.restr I H
⊢ S.pairing ((S.reflectionPerm γ) δ) γ ≠ 0

Tactic:
rwa [← S.pairing_reflectionPerm γ δ γ, S.pairing_reflectionPerm_self_right, neg_ne_zero]

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 : FractionalIdeal S P
h : I = 0
x : P
hx : x ∈ I
⊢ x = 0

Tactic:
by simpa [h, mem_zero_iff] using hx

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.symm p ∈ Set.Iic (Associates.mk m)

Tactic:
associatesEquivOfUniqueUnits_symm_apply

Goal state after:
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'
⊢ Associates.mk p ∈ Set.Iic (Associates.mk m)
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg
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 : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * ↑(1 / I)

Tactic:
coe_div hI_nz,

Goal state after:
case neg
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 : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * (↑1 / ↑I)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case neg.succ
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ b ∈ (↑I)⁻¹, x * b ∈ (↑I)⁻¹
p : A[X]
hy : (Polynomial.aeval x) p ∈ Subalgebra.toSubmodule (Polynomial.aeval x).range
i : ℕ
ih : x ^ i ∈ ↑(↑I)⁻¹
⊢ x * x ^ i ∈ ↑(↑I)⁻¹

Tactic:
exact x_mul_mem _ ih

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

Goal state before:
pp: case mp.refine_2
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
⊢ ∀ (x_1 y : P), (∃ y' ∈ I, x_1 = x * y') → (∃ y' ∈ I, y = x * y') → ∃ y' ∈ I, x_1 + y = x * y'

Tactic:
· rintro _ _ ⟨y, hy, rfl⟩ ⟨y', hy', rfl⟩
      exact ⟨y + y', Submodule.add_mem (I : Submodule R P) hy hy', (mul_add _ _ _).symm⟩

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

Goal state before:
pp: case h
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₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : ∀ J ≤ I, (↑J).FG
hx : ¬x = 0
h_gx : (algebraMap R₁ K) x ≠ 0
h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0
J : FractionalIdeal R₁⁰ K
hJ : J * spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≤ I
s : Finset K
hs : span R₁ ↑s = ↑(J * spanSingleton R₁⁰ ((algebraMap R₁ K) x))
⊢ span R₁ ↑(s * {((algebraMap R₁ K) x)⁻¹}) = ↑J

Tactic:
rw [Finset.coe_mul, Finset.coe_singleton, ← span_mul_span, hs, ← coe_spanSingleton R₁⁰, ←
    coe_mul, mul_assoc, spanSingleton_mul_spanSingleton, mul_inv_cancel₀ h_gx, spanSingleton_one,
    mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
P Q : HeightOneSpectrum R
hPQ : P ≠ Q
⊢ P.asIdeal ≠ Q.asIdeal

Tactic:
by simpa [HeightOneSpectrum.ext_iff] using hPQ

Goal state after: