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

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
hy_range : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
hny_comm : Commute n y
htr_n : (trace K M) (n * y) = 0
htr_s : (trace K M) (s * y) = ∑ i, fμ i * μ i
⊢ (trace K M) (n * y) + (trace K M) (s * y) = ∑ i, fμ i * μ i

Tactic:
htr_n,

Goal state after:
L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
hy_range : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
hny_comm : Commute n y
htr_n : (trace K M) (n * y) = 0
htr_s : (trace K M) (s * y) = ∑ i, fμ i * μ i
⊢ 0 + (trace K M) (s * y) = ∑ i, fμ i * μ i
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case neg
ι : 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
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support ((decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
mem₁ : ↑(((decompose 𝒜) r) k) * x ∈ 𝒜 (k + i)
h✝ : ¬k + i = j
⊢ ↑0 ∈ I

Tactic:
· exact I.zero_mem

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
M : n × n → S
⊢ Polynomial.map (eval₂Hom f M) (univ R n) = (of (Function.curry M)).charpoly

Tactic:
rw [univ, ← charpoly_map, coe_eval₂Hom, ← mvPolynomialX_map_eval₂ f (Matrix.of M.curry)]
  simp only [of_apply, Function.curry_apply, Prod.mk.eta]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
⊢ toMvPolynomial 1 = X

Tactic:
ext i : 1
  rw [toMvPolynomial, Finset.sum_eq_single i]
  · simp only [one_apply_eq, ← C_mul_X_eq_monomial, C_1, one_mul]
  · rintro j - hj
    simp only [one_apply_ne hj.symm, map_zero]
  · grind

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case e_f.hX
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
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 ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij kl : ιM × ιM
⊢ ((basis A bₘ).end.repr
        ((TensorProduct.lift (↑R { toFun := fun a ↦ a • baseChangeHom R A M M, map_add' := ⋯, map_smul' := ⋯ }))
          ((basis A bₘ.end) kl)))
      ij =
    if kl = ij then 1 else 0

Tactic:
basis_apply,

Goal state after:
case e_f.hX
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
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 ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij kl : ιM × ιM
⊢ ((basis A bₘ).end.repr
        ((TensorProduct.lift (↑R { toFun := fun a ↦ a • baseChangeHom R A M M, map_add' := ⋯, map_smul' := ⋯ }))
          (1 ⊗ₜ[R] bₘ.end kl)))
      ij =
    if kl = ij then 1 else 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
x : ι → R
y : R
⊢ y ∈ span (Set.range x) ^ n ↔ ∃ p, p.IsHomogeneous n ∧ (MvPolynomial.eval x) p = y

Tactic:
by
  simp [Ideal.span_pow_eq_map_homogeneousSubmodule]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : ι → R
y : R
⊢ y ∈ span (Set.range x) ↔ ∃ p, p.IsHomogeneous 1 ∧ (MvPolynomial.eval x) p = y

Tactic:
by
  simp [Ideal.span_eq_map_homogeneousSubmodule]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P A : Matrix n n R
h : Invertible P
⊢ (P.lieConj h).symm A = P⁻¹ * A * P

Tactic:
by
  simp [LinearEquiv.symm_conj_apply, Matrix.lieConj, LinearMap.toMatrix'_comp,
    LinearMap.toMatrix'_toLin']

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst✝⁶ : Semiring K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : AddCommMonoid V'
inst✝² : Module K V'
inst✝¹ : AddCommMonoid V''
inst✝ : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ lift.{v', v''} (Module.rank K ↥(Submodule.map f g.range)) ≤ lift.{v'', v'} (Module.rank K ↥g.range)

Tactic:
exact lift_rank_map_le _ _

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

Goal state before:
pp: R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ J * -B * -A - J * -A * -B = J * -(A * B - B * A)

Tactic:
noncomm_ring

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
⊢ ∀ {a b : Derivation R A' A' × Derivation R A A},
    a ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2} →
      b ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2} →
        a + b ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}

Tactic:
by simp_all

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
⊢ ∀ (c : R) {x : Derivation R A' A' × Derivation R A A},
    x ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2} →
      c • x ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}

Tactic:
by simp_all

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

Goal state before:
pp: 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
a : ↥(twoCochain R L M)
⊢ a ∈ twoCocycle R L M ↔ (d₂₃ R L M) a = 0

Tactic:
by
  simp [twoCocycle]

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)
hF' : IsUnit F'
x : l → k
hx1 : A' *ᵥ x = 0
hx2 : C' *ᵥ x = 0
⊢ x = 0

Tactic:
have hv0 : F' *ᵥ (Sum.elim x 0) = F' *ᵥ (Sum.elim 0 0) := by
      simp [fromBlocks_mulVec, hx1, hx2, F'_def]

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)
hF' : IsUnit F'
x : l → k
hx1 : A' *ᵥ x = 0
hx2 : C' *ᵥ x = 0
hv0 : F' *ᵥ Sum.elim x 0 = F' *ᵥ Sum.elim 0 0
⊢ x = 0
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: case smul
L : Type u_2
M : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
R : Type u_4
inst✝³ : CommRing R
inst✝² : LieAlgebra R L
inst✝¹ : Module R M
inst✝ : LieModule R L M
s : Set L
hs : ∀ x ∈ s, (trace R M) ((toEnd R L M) x) = 0
x : L
t : R
u : L
hx✝ : u ∈ LieSubalgebra.lieSpan R L s
hu : (trace R M) ((toEnd R L M) u) = 0
⊢ (trace R M) ((toEnd R L M) (t • u)) = 0

Tactic:
simp [hu]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ x ∈ a✝

Tactic:
by simp_all

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

Goal state before:
pp: R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V := ⋯
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V := ⋯
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
w : A
key : ∀ (i : ℕ), i ≠ 0 → ∃ j < i, Submodule.map (T χ w) (U' i) ≤ U' j
⊢ _root_.IsNilpotent (T χ w)

Tactic:
Module.End.isNilpotent_iff_of_finite

Goal state after:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
w : A
key : ∀ (i : ℕ), i ≠ 0 → ∃ j < i, Submodule.map (T χ w) (U' i) ≤ U' j
⊢ ∀ (m : ↥U), ∃ n, (T χ w ^ n) m = 0
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
r : R
x : loopAlgebra R A L
⊢ ((r • F x).sum fun a v ↦ a • (Φ ((F f) (-a))) v) = (RingHom.id R) r • (F x).sum fun a v ↦ a • (Φ ((F f) (-a))) v

Tactic:
sum_of_support_subset _ support_smul _ (by simp),

Goal state after:
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
r : R
x : loopAlgebra R A L
⊢ ∑ x_1 ∈ (F x).support, x_1 • (Φ ((F f) (-x_1))) ((r • F x) x_1) =
    (RingHom.id R) r • (F x).sum fun a v ↦ a • (Φ ((F f) (-a))) v
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
s : { s // s.Nodup ∧ s.Nontrivial }
⊢ (fun f ↦ ⟨(↑f).toCycle ⋯, ⋯⟩) ((fun s ↦ ⟨(↑s).formPerm ⋯, ⋯⟩) s) = s

Tactic:
rcases s with ⟨⟨s⟩, hn, ht⟩
    obtain ⟨x, -, -, hx, -⟩ := id ht
    have hl : 2 ≤ s.length := by simpa using Cycle.length_nontrivial ht
    simp only [Cycle.mk_eq_coe, Cycle.nodup_coe_iff, Cycle.mem_coe_iff,
      Cycle.formPerm_coe] at hn hx ⊢
    apply Subtype.ext
    dsimp
    rw [toCycle_eq_toList _ _ x]
    · refine Quotient.sound' ?_
      exact toList_formPerm_isRotated_self _ hl hn _ hx
    · rw [← mem_support, support_formPerm_of_nodup _ hn]
      · simpa using hx
      · rintro _ rfl
        simp at hl

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✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
x : A
h : -x ∈ Finset.image Neg.neg (F f).support
⊢ x ∈ (F f).support

Tactic:
by simpa using h

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

Goal state before:
pp: R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
trace_T_U_zero : ∀ (w : A), (LinearMap.trace R ↥U) (T χ w) = 0
trace_za : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = χ ⁅z, a⁆ • ↑(finrank R ↥U)
this : finrank R ↥U ≠ 0
⊢ χ ⁅z, a⁆ = 0

Tactic:
by simp_all

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
α : Fin (p + 1) → Fin n
i j : Fin n
⊢ bminor A i j α =
    A i j * pminor A α + ∑ s, (-1) ^ (↑s + 1) * A (α s) j * (A.submatrix (Fin.cons i (s.removeNth α)) α).det

Tactic:
rw [bminor, Matrix.det_succ_column_zero, Fin.sum_univ_succ]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
α : Fin (p + 1) → Fin n
i j : Fin n
⊢ (-1) ^ ↑0 * A.submatrix (Fin.cons i α) (Fin.cons j α) 0 0 *
        ((A.submatrix (Fin.cons i α) (Fin.cons j α)).submatrix (Fin.succAbove 0) Fin.succ).det +
      ∑ i_1,
        (-1) ^ ↑i_1.succ * A.submatrix (Fin.cons i α) (Fin.cons j α) i_1.succ 0 *
          ((A.submatrix (Fin.cons i α) (Fin.cons j α)).submatrix i_1.succ.succAbove Fin.succ).det =
    A i j * pminor A α + ∑ s, (-1) ^ (↑s + 1) * A (α s) j * (A.submatrix (Fin.cons i (s.removeNth α)) α).det
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1)
hr : 1 = c i
⊢ IsUnit (c 0)

Tactic:
rw [Associates.isUnit_iff_eq_one, ← Associates.le_one_iff, hr]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1)
hr : 1 = c i
⊢ c 0 ≤ c i
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
⊢ q = c 1 ^ n

Tactic:
obtain ⟨i, hi'⟩ := element_of_chain_eq_pow_second_of_chain hn h₁ (@fun r => h₂) (dvd_refl q) hq
    convert! hi'
    refine (Nat.lt_succ_iff.1 i.prop).antisymm' (Nat.le_of_succ_le_succ ?_)
    calc
      n + 1 = (Finset.univ : Finset (Fin (n + 1))).card := (Finset.card_fin _).symm
      _ = (Finset.univ.image c).card := (Finset.card_image_iff.mpr h₁.injective.injOn).symm
      _ ≤ (Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ)).card :=
        (Finset.card_le_card ?_)
      _ ≤ (Finset.univ : Finset (Fin (i + 1))).card := Finset.card_image_le
      _ = i + 1 := Finset.card_fin _
    intro r hr
    obtain ⟨j, -, rfl⟩ := Finset.mem_image.1 hr
    have := h₂.2 ⟨j, rfl⟩
    rw [hi'] at this
    have h := (dvd_prime_pow (show Prime (c 1) from ?_) i).1 this
    · rcases h with ⟨u, hu, hu'⟩
      refine Finset.mem_image.mpr ⟨⟨u, Nat.lt_succ_of_le hu⟩, Finset.mem_univ _, ?_⟩
      rwa [associated_iff_eq, eq_comm] at hu'
    · rw [← irreducible_iff_prime]
      exact second_of_chain_is_irreducible hn h₁ (@h₂) hq

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'
this :
  emultiplicity (Associates.mk p) (Associates.mk m) =
    emultiplicity (Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩))
      (Associates.mk n)
⊢ emultiplicity p m = emultiplicity (↑(d ⟨p, ⋯⟩)) n

Tactic:
by
    simpa only [emultiplicity_mk_eq_emultiplicity, associatesEquivOfUniqueUnits_symm_apply,
      associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq] using this

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

Tactic:
exact mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp)

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
⊢ ∃ x, x ≠ 0 ∧ (algebraMap R K) x ∈ I

Tactic:
obtain ⟨y : K, y_mem, y_notMem⟩ :=
    SetLike.exists_of_lt (bot_lt_iff_ne_bot.mpr hI)

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
⊢ ∃ x, x ≠ 0 ∧ (algebraMap R K) x ∈ I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: 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)⁻¹)⁻¹
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ y ∈ ↑I, x * b * y ∈ 1

Tactic:
rw [mem_inv_iff hJ0] at hx

Goal state after:
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 : ∀ y ∈ ↑I * (↑I)⁻¹, x * y ∈ 1
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ y ∈ ↑I, x * b * y ∈ 1
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ spanSingleton A⁰ (((algebraMap A (FractionRing A)) a)⁻¹ * (algebraMap A (FractionRing A)) a) = 1

pp: case hI0
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ J ≠ ⊥

Tactic:
inv_mul_cancel₀,

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ spanSingleton A⁰ 1 = 1

A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ (algebraMap A (FractionRing A)) a ≠ 0

case hI0
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ J ≠ ⊥