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

Goal state before:
pp: 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
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
m n : ℕ
hmn : m ≤ n
y : ↥H
hy : ((ad R ↥H) x ^ m) y = 0
⊢ ((ad R ↥H) x ^ n) y = 0

Tactic:
exact Module.End.pow_map_zero_of_le hmn hy

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
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ nodalWeight s v i ≠ 0

Tactic:
rw [nodalWeight, prod_ne_zero_iff]
  intro j hj
  rcases mem_erase.mp hj with ⟨hij, hj⟩
  exact inv_ne_zero (sub_ne_zero_of_ne (mt (hvs.eq_iff hi hj).mp hij.symm))

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
hm' : weightedTotalDegree' w p ≤ ↑m
⊢ ↑(p.support.sup fun s ↦ (weight w) s) ≤ weightedTotalDegree' w p

Tactic:
rw [← hm]

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
hm' : weightedTotalDegree' w p ≤ ↑m
⊢ ↑(p.support.sup fun s ↦ (weight w) s) ≤ ↑m
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext :
  ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)), _root_.IsNilpotent ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M)) x)
x : L
hx : x ∈ derivedSeries R L 1
⊢ _root_.IsNilpotent ((toEnd R (↥(derivedSeries R L 1)) M) ⟨x, hx⟩)

Tactic:
have hx_ext : 1 ⊗ₜ[R] x ∈ derivedSeries A (A ⊗[R] L) 1 := by
    rw [derivedSeries_baseChange]
    exact Submodule.tmul_mem_baseChange_of_mem 1 hx

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext :
  ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)), _root_.IsNilpotent ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M)) x)
x : L
hx : x ∈ derivedSeries R L 1
hx_ext : 1 ⊗ₜ[R] x ∈ derivedSeries A (A ⊗[R] L) 1
⊢ _root_.IsNilpotent ((toEnd R (↥(derivedSeries R L 1)) M) ⟨x, hx⟩)
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
I : LieIdeal R L
h : ∀ x ∈ I, ∀ y ∈ ⁅I, I⁆, ((killingForm R L) x) y = 0
⊢ IsSolvable ↥I

Tactic:
by
  set DI : LieIdeal R L := ⁅I, I⁆
  set DDI : LieIdeal R L := ⁅DI, DI⁆
  have tf_eq_zero : LieModule.traceForm R DI L = 0 := by
    ext ⟨x, hx⟩ ⟨y, hy⟩
    change killingForm R L x y = 0
    exact h x (LieSubmodule.lie_le_left I I hx) y hy
  have module_nilp : LieModule.IsNilpotent (derivedSeries R DI 1) L :=
    LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero tf_eq_zero
  have ring_nilp : LieRing.IsNilpotent DDI := by
    rw [LieAlgebra.isNilpotent_iff_forall (R := R)]
    rintro ⟨x, hx⟩
    apply LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad (DDI : LieSubalgebra R L) (x := ⟨x, hx⟩)
    refine (LieModule.isNilpotent_iff_forall' (R := R)).mp module_nilp
      ⟨⟨x, LieSubmodule.lie_le_left DI DI hx⟩, ?_⟩
    rwa [derivedSeries_eq_derivedSeriesOfIdeal_comap, mem_comap]
  obtain ⟨k, hk⟩ := IsSolvable.solvable R DDI
  rw [derivedSeries_eq_bot_iff] at hk
  refine IsSolvable.mk (k := k + 2) ((derivedSeries_eq_bot_iff I (k + 2)).mpr ?_)
  rwa [derivedSeriesOfIdeal_add, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ,
    derivedSeriesOfIdeal_zero]

Goal state after:
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
ι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
x : L
⊢ Polynomial.map (eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = ((toMatrix bₘ bₘ) (φ x)).charpoly

Tactic:
by
  rw [polyCharpolyAux, Polynomial.map_map, ← MvPolynomial.eval₂Hom_C_eq_bind₁,
    MvPolynomial.comp_eval₂Hom, charpoly.univ_map_eval₂Hom]
  congr
  ext
  rw [of_apply, Function.curry_apply, toMvPolynomial_eval_eq_apply, LinearEquiv.symm_apply_apply]
  rfl

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''} (f ∘ₗ g).rank ≤ lift.{v'', v'} g.rank

Tactic:
rw [rank, rank, LinearMap.range_comp]; exact lift_rank_map_le _ _

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

Goal state before:
pp: m : Type um
n : Type un
o : Type uo
R : Type uR
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
a✝ : Nontrivial R
⊢ finrank R ↥(A * B).mulVecLin.range ≤ finrank R ↥A.mulVecLin.range

Tactic:
mulVecLin_mul

Goal state after:
m : Type um
n : Type un
o : Type uo
R : Type uR
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
a✝ : Nontrivial R
⊢ finrank R ↥(A.mulVecLin ∘ₗ B.mulVecLin).range ≤ finrank R ↥A.mulVecLin.range
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
o : Type uo
R : Type uR
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
a✝ : Nontrivial R
⊢ finrank R ↥(A * B).mulVecLin.range ≤ finrank R ↥B.mulVecLin.range

Tactic:
mulVecLin_mul

Goal state after:
m : Type um
n : Type un
o : Type uo
R : Type uR
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
a✝ : Nontrivial R
⊢ finrank R ↥(A.mulVecLin ∘ₗ B.mulVecLin).range ≤ finrank R ↥B.mulVecLin.range
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: 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
⊢ ∃ z, z ≠ 0 ∧ ⁅x', z⁆ = 0

Tactic:
apply_fun (evalRingHom 0) at H

Goal state after:
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 : (evalRingHom 0) (constantCoeff ψ) = (evalRingHom 0) 0
⊢ ∃ z, z ≠ 0 ∧ ⁅x', z⁆ = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝² : Fintype n
inst✝¹ : Fintype n₀
inst✝ : CommSemiring R
em : m ≃ m₀
en : n ≃ n₀
A : Matrix m n R
⊢ ((reindex em en) A).rank = A.rank

Tactic:
rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp,
    LinearEquiv.range, Submodule.map_top, LinearEquiv.finrank_map_eq]

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

Goal state before:
pp: case inr
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x✝ y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
i j : ι
y : L i
x : L j
hij : i ≠ j
⊢ (toAddMonoid fun i ↦ (↑(f i)).toAddMonoidHom) ⁅(of L j) x, (of L i) y⁆ =
    ⁅(↑(f j)).toAddMonoidHom x, (↑(f i)).toAddMonoidHom y⁆

Tactic:
lie_of_of_ne _ hij.symm,

Goal state after:
case inr
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x✝ y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
i j : ι
y : L i
x : L j
hij : i ≠ j
⊢ (toAddMonoid fun i ↦ (↑(f i)).toAddMonoidHom) 0 = ⁅(↑(f j)).toAddMonoidHom x, (↑(f i)).toAddMonoidHom y⁆
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
h : 0 ∈ (single 0 1).coeff.support
⊢ f 0 = 0

Tactic:
apply map_zero

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
x y : L
⊢ { toFun := fun x ↦ (decomposeLinearEquiv ℒ).symm ((ofGradingSum ℒ φ) ((decomposeLinearEquiv ℒ) x)), map_add' := ⋯,
        map_smul' := ⋯ }
      ⁅x, y⁆ =
    ⁅x,
        { toFun := fun x ↦ (decomposeLinearEquiv ℒ).symm ((ofGradingSum ℒ φ) ((decomposeLinearEquiv ℒ) x)),
            map_add' := ⋯, map_smul' := ⋯ }
          y⁆ -
      ⁅y,
        { toFun := fun x ↦ (decomposeLinearEquiv ℒ).symm ((ofGradingSum ℒ φ) ((decomposeLinearEquiv ℒ) x)),
            map_add' := ⋯, map_smul' := ⋯ }
          x⁆

Tactic:
simp [decomposeLinearEquiv_apply, decomposeLinearEquiv_symm_apply]

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

Goal state before:
pp: case h1
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ∀ σ ∈ [l.attach.formPerm], σ.IsCycle

pp: case h2
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ Pairwise Perm.Disjoint [l.attach.formPerm]

Tactic:
· simpa using isCycle_formPerm hl hn

Goal state after:
case h2
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ Pairwise Perm.Disjoint [l.attach.formPerm]
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
this : LieRingModule L M := E.ringModuleOf
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
r : R
x : L
m : M
⊢ ⁅r • x, m⁆ = r • ⁅x, m⁆

Tactic:
rw [ringModuleOf_bracket, ringModuleOf_bracket, ← map_smul, ← smul_lie,
          EquivLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie]

Goal state after:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
this : LieRingModule L M := E.ringModuleOf
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
r : R
x : L
m : M
⊢ ⁅Exists.choose ⋯ (r • x) - r • Exists.choose ⋯ x, E.toKer m⁆ = 0
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x : E.L
y : ↥E.proj.ker
⊢ s (E.proj x) - x ∈ E.proj.ker

Tactic:
by simp [hs.eq]

Goal state after:
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
E : Extension R M L
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y : L
⊢ ⁅s x, s y⁆ - s ⁅x, y⁆ ∈ E.proj.ker

Tactic:
by simp [hs.eq]

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 : ℕ
i : Fin n
hEq1 : Eq1 A p
⊢ -∑ k > i, (Spec.stepEntry A)^[p] A k k = (-1) ^ (p + 1) * ∑ α ∈ S (p + 1) i, pminor A α

Tactic:
by
  calc
    (-∑ k ∈ Finset.Ioi i, (Spec.stepEntry A)^[p] A k k) =
        (-1) ^ (p + 1) * ∑ k ∈ Finset.Ioi i, ∑ α ∈ S p k, bminor A k k α := by
      simp only [hEq1, Matrix.of_apply, ← Finset.mul_sum]
      ring
    _ = (-1) ^ (p + 1) * ∑ α ∈ S (p + 1) i, pminor A α := by
      rw [S_succ_eq_biUnion, Finset.sum_biUnion]
      · congrm (((-1) ^ (p + 1) * ∑ k ∈ Finset.Ioi i, ?_))
        symm
        exact Finset.sum_image fun _ _ _ _ hαβ => (Fin.cons_inj.mp hαβ).2
      · grind [Set.PairwiseDisjoint, Set.Pairwise, Finset.disjoint_left, Fin.cons_inj]

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case neg.refine_2
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t ↦ ↑(d ⟨c₁ t, ⋯⟩)
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)
r : Associates N
hr : r ≤ ↑(d ⟨c₁ 1 ^ s, hs'⟩)
this : r ≤ n
⊢ d.symm ⟨r, this⟩ ≤ d.symm (d ⟨c₁ 1 ^ s, hs'⟩)

Tactic:
d.symm.le_iff_le

Goal state after:
case neg.refine_2
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t ↦ ↑(d ⟨c₁ t, ⋯⟩)
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)
r : Associates N
hr : r ≤ ↑(d ⟨c₁ 1 ^ s, hs'⟩)
this : r ≤ n
⊢ ⟨r, this⟩ ≤ d ⟨c₁ 1 ^ s, hs'⟩
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✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ emultiplicity p m = emultiplicity (↑(d ⟨p, ⋯⟩)) n

Tactic:
refine le_antisymm (emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso hp d) ?_
  suffices emultiplicity (↑(d ⟨p, dvd_of_mem_normalizedFactors hp⟩)) n ≤
      emultiplicity (↑(d.symm (d ⟨p, dvd_of_mem_normalizedFactors hp⟩))) m by
    rw [d.symm_apply_apply ⟨p, dvd_of_mem_normalizedFactors hp⟩, Subtype.coe_mk] at this
    exact this
  let := Classical.decEq (Associates N)
  simpa only [Subtype.coe_eta] using
    emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso
      (mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors hn hp d) d.symm

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

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

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

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
hspan_compl_roots_vanish : ∀ μ ∈ I.rootSet, ↑span_compl_roots ≤ Weight.ker
hx_top : ⟨x, hxH⟩ ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ ↑span_I_roots
b : ↥H
hb : b ∈ ↑span_compl_roots
hab : a + b = ⟨x, hxH⟩
haI : ↑a ∈ I
hbI : ↑b ∈ I
μ : Weight K (↥H) L
hμ : ¬μ.IsNonZero
⊢ b ∈ Weight.ker

Tactic:
simp only [Weight.IsNonZero, not_not] at hμ

Goal state after:
case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
hspan_compl_roots_vanish : ∀ μ ∈ I.rootSet, ↑span_compl_roots ≤ Weight.ker
hx_top : ⟨x, hxH⟩ ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ ↑span_I_roots
b : ↥H
hb : b ∈ ↑span_compl_roots
hab : a + b = ⟨x, hxH⟩
haI : ↑a ∈ I
hbI : ↑b ∈ I
μ : Weight K (↥H) L
hμ : μ.IsZero
⊢ b ∈ Weight.ker
Module: Mathlib.RingTheory.FractionalIdeal.Operations

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
s✝ : Set P
x✝² : ∃ a ∈ S, ∀ b ∈ s✝, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s✝, IsInteger R (a • b)
x✝¹ : P
hb : x✝¹ ∈ span R s✝
s : R
x : P
x✝ : x ∈ span R s✝
hx : IsInteger R (a • x)
⊢ IsInteger R (a • s • x)

Tactic:
rw [smul_comm]
        exact isInteger_smul hx

Goal state after:
Module: Mathlib.Algebra.Module.DedekindDomain

Goal state before:
pp: case prime
R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
⊢ ∀ i ∈ (factors I).toFinset, Prime i

Tactic:
exact prime_of_mem

Goal state after:
Module: Mathlib.Algebra.Module.DedekindDomain

Goal state before:
pp: case hI
R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ q ^ Multiset.count q P ≠ ⊥

Tactic:
rw [← Ideal.zero_eq_bot]

Goal state after:
case hI
R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ q ^ Multiset.count q P ≠ 0
Module: Mathlib.Algebra.Module.DedekindDomain

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ DirectSum.IsInternal fun p ↦ torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))

Tactic:
have hM' := Module.isTorsionBySet_annihilator_top R M
  have hI := Submodule.annihilator_top_inter_nonZeroDivisors hM
  refine isInternal_prime_power_torsion_of_is_torsion_by_ideal ?_ hM'
  rw [Submodule.ne_bot_iff]
  obtain ⟨x, H, hx⟩ := hI; exact ⟨x, H, nonZeroDivisors.ne_zero hx⟩

Goal state after:
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 : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
⊢ ∃ a aI, a ≠ 0 ∧ I = spanSingleton R₁⁰ ((algebraMap R₁ K) a)⁻¹ * ↑aI

Tactic:
refine
    ⟨a_inv,
      Submodule.comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ (algebraMap R₁ K a_inv) * I),
      nonzero, ext fun x => Iff.trans ⟨?_, ?_⟩ mem_singleton_mul.symm⟩

Goal state after:
case refine_1
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
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
⊢ x ∈ I →
    ∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
      x = ((algebraMap R₁ K) a_inv)⁻¹ * y'

case refine_2
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
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
⊢ (∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
      x = ((algebraMap R₁ K) a_inv)⁻¹ * y') →
    x ∈ I