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

Goal state before:
pp: case refine_3
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
n : ℕ
a : R
hna : ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x
⊢ ((aeval f) (C a * X ^ (n + 1))) x = eval μ (C a * X ^ (n + 1)) • x

Tactic:
rw [mul_comm, pow_succ', mul_assoc, map_mul, Module.End.mul_apply, mul_comm, hna]

Goal state after:
case refine_3
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
n : ℕ
a : R
hna : ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x
⊢ ((aeval f) X) (eval μ (C a * X ^ n) • x) = eval μ (X * (C a * X ^ n)) • x
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: n k : ℕ
⊢ n.ascFactorial (k + 1) = ∏ i ∈ range (k + 1), (n + i)

Tactic:
rw [ascFactorial, prod_range_succ_comm, ascFactorial_eq_prod_range n k]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: k : ℕ
n : ℤ
⊢ (∏ i ∈ range k, (n + ↑i)) % ↑k ! = 0

Tactic:
Finset.prod_int_mod

Goal state after:
k : ℕ
n : ℤ
⊢ (∏ i ∈ range k, (n + ↑i) % ↑k !) % ↑k ! = 0
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝² : Semiring S
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
p : R[X]
inst✝ : Algebra R S
x : S
⊢ eval x ((ascPochhammer S n).comp (map (algebraMap R S) p)) = eval₂ (algebraMap R S) x ((ascPochhammer R n).comp p)

Tactic:
← ascPochhammer_map (algebraMap R S),

Goal state after:
S : Type u
inst✝² : Semiring S
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
p : R[X]
inst✝ : Algebra R S
x : S
⊢ eval x ((map (algebraMap R S) (ascPochhammer R n)).comp (map (algebraMap R S) p)) =
    eval₂ (algebraMap R S) x ((ascPochhammer R n).comp p)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝ : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)
| ascPochhammer ℕ (n + 1 + 1)

Tactic:
rw [ascPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← ascPochhammer_succ_left, add_comp,
          X_comp, natCast_comp, add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]

Goal state after:
S : Type u
inst✝ : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)
| ascPochhammer ℕ (n + 1) * (X + ↑n.succ)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
T : Type v
inst✝ : Ring T
f : R →+* T
n : ℕ
⊢ map f (descPochhammer R n) = descPochhammer T n

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => simp [ih, descPochhammer_succ_left, map_comp]

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₂
⊢ Surjective ⇑((LieHom.snd R L₁ L₂).comp (prod eι b₁ b₂).incl)

Tactic:
by
  set L : LieSubalgebra R (L₁ × L₂) := b₁.prod eι b₂
  set p₂ : L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
  have h₁ : range b₂.e = range (p₂ ∘ prodE eι b₁ b₂) := by
    simp [show p₂ ∘ prodE eι b₁ b₂ = b₂.e ∘ eι from rfl]
  have h₂ : range b₂.f = range (p₂ ∘ prodF eι b₁ b₂) := by
    simp [show p₂ ∘ prodF eι b₁ b₂ = b₂.f ∘ eι from rfl]
  rw [← LieHom.range_eq_top, eq_top_iff, ← b₂.span_ef, map_top,
    ← b₁.basisProd_aux eι b₂, map_lieSpan, image_union, h₁, h₂]
  simp [range_comp]

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

Goal state before:
pp: ι : Type u_4
R : Type u_5
K : Type u_6
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : ↥E →+ R
⊢ ∃ r, ∀ (i j : ι), Polynomial.eval (a i - a j) r = (algebraMap R K) (f ⟨a i, ⋯⟩) - (algebraMap R K) (f ⟨a j, ⋯⟩)

Tactic:
by
  suffices ∀ (ij kl : ι × ι) (hij : a ij.1 - a ij.2 = a kl.1 - a kl.2),
      algebraMap R K (f ⟨a ij.1, ha ij.1⟩) - algebraMap R K (f ⟨a ij.2, ha ij.2⟩) =
      algebraMap R K (f ⟨a kl.1, ha kl.1⟩) - algebraMap R K (f ⟨a kl.2, ha kl.2⟩) by
    obtain ⟨r, hr⟩ := (Polynomial.exists_eval_eq_iff _ _).mpr this
    exact ⟨r, fun i j ↦ hr (i, j)⟩
  rintro ⟨i, j⟩ ⟨k, l⟩ hij
  have heq : (⟨a i, ha i⟩ - ⟨a j, ha j⟩ : E) = ⟨a k, ha k⟩ - ⟨a l, ha l⟩ := Subtype.ext hij
  rw [← (algebraMap R K).map_sub, ← (algebraMap R K).map_sub, ← map_sub, ← map_sub, heq]

Goal state after:
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
x y : L
hy : ∀ y_1 ∈ engel R x, ⁅y, y_1⁆ ∈ engel R x
⊢ y ∈ engel R x

Tactic:
specialize hy x (self_mem_engel R x)

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
hy : ⁅y, x⁆ ∈ engel R x
⊢ y ∈ engel R x
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✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
⊢ N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule

Tactic:
have aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N := fun n hn ↦ le_normalizer H (aux₁ _ hn)

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
⊢ N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule
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
⊢ LieRing.IsNilpotent ↥H

Tactic:
by
  rw [LieAlgebra.isNilpotent_iff_forall (R := R)]
  intro x
  let K : ℕ →o Submodule R H :=
    ⟨fun n ↦ LinearMap.ker ((ad R H x) ^ n), fun m n hmn ↦ ?mono⟩
  case mono =>
    intro y hy
    rw [LinearMap.mem_ker] at hy ⊢
    exact Module.End.pow_map_zero_of_le hmn hy
  obtain ⟨n, hn⟩ := monotone_stabilizes_iff_noetherian.mpr inferInstance K
  use n
  ext y
  rw [coe_ad_pow]
  specialize h x x.2 y.2
  rw [mem_engel_iff] at h
  obtain ⟨m, hm⟩ := h
  obtain (hmn | hmn) : m ≤ n ∨ n ≤ m := le_total m n
  · exact Module.End.pow_map_zero_of_le hmn hm
  · have : ∀ k : ℕ, ((ad R L) x ^ k) y = 0 ↔ y ∈ K k := by simp [K, Subtype.ext_iff, coe_ad_pow]
    rwa [this, ← hn m hmn, ← this] at hm

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ Fintype.card ↑↑G = Fintype.card ↥G

Tactic:
exact rfl

Goal state after:
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
⊢ IsSolvable ↥(LieIdeal.killingCompl R L ⊤)

Tactic:
refine LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero _ ?_

Goal state after:
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
⊢ ∀ x ∈ LieIdeal.killingCompl R L ⊤,
    ∀ y ∈ ⁅LieIdeal.killingCompl R L ⊤, LieIdeal.killingCompl R L ⊤⁆, ((killingForm R L) x) y = 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯
p : MvPolynomial σ R
hp✝ : IsWeightedHomogeneous w p m
hp : p ∈ AddMonoidAlgebra.supported R R {d | (weight w) d = m}
A : Submodule R (MvPolynomial σ R) :=
  { carrier := {p | ∃ (hp : IsWeightedHomogeneous w p m), ∀ (a : R), motive (C a * p) ⋯}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
⊢ ∀ (a : R), motive (C a * p) ⋯

Tactic:
AddMonoidAlgebra.supported_eq_span_single

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯
p : MvPolynomial σ R
hp✝ : IsWeightedHomogeneous w p m
hp : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = m})
A : Submodule R (MvPolynomial σ R) :=
  { carrier := {p | ∃ (hp : IsWeightedHomogeneous w p m), ∀ (a : R), motive (C a * p) ⋯}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
⊢ ∀ (a : R), motive (C a * p) ⋯
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ r ∈ (homogeneousHull 𝒜 I).toIdeal

Tactic:
classical
  rw [← DirectSum.sum_support_decompose 𝒜 r]
  refine Ideal.sum_mem _ ?_
  intro j _
  apply Ideal.subset_span
  use j
  use ⟨r, hr⟩

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Finite ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f g : M₁ →ₗ[R] M₂
⊢ toMvPolynomial b₁ b₂ (f + g) = toMvPolynomial b₁ b₂ f + toMvPolynomial b₁ b₂ g

Tactic:
by
  unfold toMvPolynomial; simp only [map_add, Matrix.toMvPolynomial_add]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
σ : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : IsAddTorsionFree M
hw : ∀ (i : σ), w i ≠ 0
⊢ (weightedHomogeneousComponent w 0) φ = C (coeff 0 φ)

Tactic:
ext1 d
  rcases Classical.em (d = 0) with (rfl | hd)
  · simp only [coeff_weightedHomogeneousComponent, if_pos, map_zero, coeff_zero_C]
  · rw [coeff_weightedHomogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]
    simp only [weight, LinearMap.toAddMonoidHom_coe, Finsupp.linearCombination_apply, Finsupp.sum,
      sum_eq_zero_iff, Finsupp.mem_support_iff, Ne, smul_eq_zero, not_forall, not_or,
      and_self_left, exists_prop]
    simp only [DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply, not_forall] at hd
    obtain ⟨i, hi⟩ := hd
    exact ⟨i, hi, hw i⟩

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ b ∈ φ.support, (b.sum fun x e ↦ e) < n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ degree d ≠ n

Tactic:
exact ne_of_lt (h d hd)

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:
by
  rw [LieHom.map_lie, LieRing.of_associative_ring_bracket, mul_comm, sub_self]

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
⊢ Submodule.map (toLin' (diagonal w)) ⊤ = ⨆ i, ⨆ (_ : w i ≠ 0), (LinearMap.single K (fun x ↦ K) i).range

Tactic:
← iSup_range_single,

Goal state after:
m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ Submodule.map (toLin' (diagonal w)) (⨆ i, (LinearMap.single K (fun a ↦ K) i).range) =
    ⨆ i, ⨆ (_ : w i ≠ 0), (LinearMap.single K (fun x ↦ K) i).range
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 : oneCochain R L M
x y z : L
this : ∀ (a : oneCochain R L M) (x : L), ((d₁₂ R L M) a) x = ↑((d₁₂ R L M) a) x
⊢ a ⁅y, ⁅z, x⁆⁆ = a ⁅x, ⁅z, y⁆⁆ + a ⁅z, ⁅y, x⁆⁆

Tactic:
rw [congr_arg a (leibniz_lie y z x), ← lie_skew, ← lie_skew z y, lie_neg, map_add]

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

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
ext
    simp only [lie_smul, lie_module_bracket_apply, smul_apply]

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
⊢ ∀ (x y z : FreeLieAlgebra R X),
    Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ x (y + z) =
      Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ x y + Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ x z

Tactic:
rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; change Quot.mk _ _ = Quot.mk _ _; simp_rw [mul_add]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
⊢ l.formPerm.Disjoint l'.formPerm ↔ l.Disjoint l'

Tactic:
by
  rw [disjoint_iff_eq_or_eq, List.Disjoint]
  constructor
  · rintro h x hx hx'
    specialize h x
    rw [formPerm_apply_mem_eq_self_iff _ hl _ hx, formPerm_apply_mem_eq_self_iff _ hl' _ hx'] at h
    lia
  · intro h x
    by_cases hx : x ∈ l
    on_goal 1 => by_cases hx' : x ∈ l'
    · exact (h hx hx').elim
    all_goals have := List.formPerm_apply_of_notMem ‹_›; tauto

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
⊢ (p.toList x).Nodup

Tactic:
by
  by_cases hx : p x = x
  · rw [← notMem_support, ← toList_eq_nil_iff] at hx
    simp [hx]
  have hc : IsCycle (cycleOf p x) := isCycle_cycleOf p hx
  rw [nodup_iff_injective_getElem]
  intro ⟨n, hn⟩ ⟨m, hm⟩
  rw [length_toList, ← hc.orderOf] at hm hn
  rw [← cycleOf_apply_self, ← Ne, ← mem_support] at hx
  simp only [Fin.mk.injEq]
  rw [getElem_toList, getElem_toList, ← cycleOf_pow_apply_self p x n, ←
    cycleOf_pow_apply_self p x m]
  rcases n with - | n <;> rcases m with - | m
  · simp
  · rw [← hc.support_pow_of_pos_of_lt_orderOf m.zero_lt_succ hm, mem_support,
      cycleOf_pow_apply_self] at hx
    simp [hx.symm]
  · rw [← hc.support_pow_of_pos_of_lt_orderOf n.zero_lt_succ hn, mem_support,
      cycleOf_pow_apply_self] at hx
    simp [hx]
  intro h
  have hn' : ¬orderOf (p.cycleOf x) ∣ n.succ := Nat.not_dvd_of_pos_of_lt n.zero_lt_succ hn
  have hm' : ¬orderOf (p.cycleOf x) ∣ m.succ := Nat.not_dvd_of_pos_of_lt m.zero_lt_succ hm
  rw [← hc.support_pow_eq_iff] at hn' hm'
  rw [← Nat.mod_eq_of_lt hn, ← Nat.mod_eq_of_lt hm, ← pow_inj_mod]
  refine support_congr ?_ ?_
  · rw [hm', hn']
  · rw [hm']
    intro y hy
    obtain ⟨k, rfl⟩ := hc.exists_pow_eq (mem_support.mp hx) (mem_support.mp hy)
    rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply, h, ← mul_apply, ← mul_apply,
      (Commute.pow_pow_self _ _ _).eq]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
⊢ x ∈ p.support → p.SameCycle x ((p ^ n) x)

Tactic:
refine fun _ => SameCycle.symm ?_

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
x✝ : x ∈ p.support
⊢ p.SameCycle ((p ^ n) x) x
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case inr
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)
⊢ finrank R ↥U ≠ 0

Tactic:
suffices Nontrivial U from Module.finrank_pos.ne'

Goal state after:
case inr
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)
⊢ Nontrivial ↥U
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' L'' : LieRinehartSubalgebra A L
h : (fun L' ↦ L'.carrier) L' = (fun L' ↦ L'.carrier) L''
⊢ L' = L''

Tactic:
rcases L'
    rcases L''
    congr
    exact SetLike.coe_injective h

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ.refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hp : Prime (c 0)
hp' : c 0 ∣ r
⊢ False

Tactic:
exact hp.not_isUnit (first_of_chain_isUnit h₁ @h₂)

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
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ b ∈ J, IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
m : P
hm : m ∈ I
n : P
hn : n ∈ J
n' : R
hn' : (algebraMap R P) n' = aJ • n
⊢ IsInteger R (aI • (aJ • n * m))

Tactic:
← hn',

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
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ b ∈ J, IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
m : P
hm : m ∈ I
n : P
hn : n ∈ J
n' : R
hn' : (algebraMap R P) n' = aJ • n
⊢ IsInteger R (aI • ((algebraMap R P) n' * m))
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case 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 p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝¹ : b ≤ n
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, this✝¹⟩
⊢ ⟨a, ha⟩ = ⊥

Tactic:
rw [Subtype.mk_eq_bot_iff]

Goal state after:
case 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 p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝¹ : b ≤ n
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, this✝¹⟩
⊢ a = ⊥

case refine_2.hbot
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)
b : Associates N
this✝¹ : b ≤ n
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(d ⟨a, ha⟩) < ↑(d ⟨p, ⋯⟩)
hx : d ⟨a, ha⟩ = ⟨b, this✝¹⟩
⊢ ⊥ ∈ Set.Iic m
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case e'_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ I = I * I * I⁻¹

Tactic:
simp only [(mul_inv_cancel_iff_isUnit K).mpr hI, mul_assoc, mul_one]

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

Goal state before:
pp: case e'_3
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ 1 = I * I⁻¹

Tactic:
simp only [(mul_inv_cancel_iff_isUnit K).mpr hI, mul_assoc, mul_one]

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

Goal state before:
pp: case mp
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
hI : I * I⁻¹ = 1
hg : generator ↑I = 0
⊢ False

Tactic:
apply ne_zero_of_mul_eq_one _ _ hI

Goal state after:
case mp
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
hI : I * I⁻¹ = 1
hg : generator ↑I = 0
⊢ I = 0