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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
⊢ ∀ (x y_1 : A ⊗[R] L),
    (LinearMap.lTensor A ↑d) ⁅x, y⁆ = ⁅x, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) x⁆ →
      (LinearMap.lTensor A ↑d) ⁅y_1, y⁆ = ⁅y_1, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) y_1⁆ →
        (LinearMap.lTensor A ↑d) ⁅x + y_1, y⁆ =
          ⁅x + y_1, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x + y_1)⁆

Tactic:
· intros _ _ h1 h2
          simp [h1, h2]
          abel_nf

Goal state after:
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
inst✝ : Infinite K
⊢ ∃ x, (engel K x).IsCartanSubalgebra

Tactic:
by
  apply exists_isCartanSubalgebra_engel_of_finrank_le_card
  exact natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite K›

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
⊢ ∀ (m : M) (r : R) (x : R[M]),
    m ∉ x.coeff.support →
      r ≠ 0 →
        (∀ (hx : x ∈ gradeBy R (⇑f) i),
            (decomposeAux f) ↑⟨x, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨x, hx⟩) →
          ∀ (hx : single m r + x ∈ gradeBy R (⇑f) i),
            (decomposeAux f) ↑⟨single m r + x, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨single m r + x, hx⟩

Tactic:
intro m b y hmy hb ih hmby
    have : Disjoint (Finsupp.single m b).support y.coeff.support := by
      simpa only [Finsupp.support_single _ hb, Finset.disjoint_singleton_left]
    rw [mem_gradeBy_iff, coeff_add, coeff_single, Finsupp.support_add_eq this, Finset.coe_union,
      Set.union_subset_iff] at hmby
    obtain ⟨h1, h2⟩ := hmby
    have : f m = i := by
      rwa [Finsupp.support_single _ hb, Finset.coe_singleton, Set.singleton_subset_iff]
        at h1
    subst this
    simp only [map_add, decomposeAux_single f m]
    let ih' := ih h2
    dsimp at ih'
    rw [ih', ← map_add]
    apply DirectSum.of_eq_of_gradedMonoid_eq
    congr 2

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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ (↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + (↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1 +
        (⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ + ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆) -
      (⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆ + ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆) =
    (↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
        ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆ +
      ((↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆ -
        ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆)

Tactic:
abel

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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ (↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + (↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 +
        (⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆) -
      (⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆ + ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆) =
    (↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ -
        ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆ +
      ((↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
        ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆)

Tactic:
abel

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
x : ⨁ (i : ι), ↥(decomposeTensor ℳ N i)
⊢ (DirectSum.coeAddMonoidHom (decomposeTensor ℳ N)) x =
    (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ).symm)
      ((directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm x))

Tactic:
← LinearEquiv.symm_rTensor,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
x : ⨁ (i : ι), ↥(decomposeTensor ℳ N i)
⊢ (DirectSum.coeAddMonoidHom (decomposeTensor ℳ N)) x =
    (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ)).symm
      ((directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm x))
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
hc : (d₂₃ R L M) ↑c = 0
this :
  (↑c ((ofProd c).symm x).1) ⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆ =
    -(⁅((ofProd c).symm x).1, (↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1⁆ -
              ⁅((ofProd c).symm y).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1⁆ +
            ⁅((ofProd c).symm z).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1⁆ -
          (↑c ⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆) ((ofProd c).symm z).1 +
        -(↑c ((ofProd c).symm y).1) ⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆)
⊢ -(⁅((ofProd c).symm x).1, (↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1⁆ -
                  ⁅((ofProd c).symm y).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1⁆ +
                ⁅((ofProd c).symm z).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1⁆ -
              (↑c ⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆) ((ofProd c).symm z).1 +
            -(↑c ((ofProd c).symm y).1) ⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆) +
        (⁅((ofProd c).symm x).1, (↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1⁆ +
            ⁅((ofProd c).symm x).1, ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆⁆ -
          ⁅((ofProd c).symm x).1, ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆⁆) -
      (⁅((ofProd c).symm y).1, ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆⁆ -
        ⁅((ofProd c).symm z).1, ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆⁆) =
    (↑c ⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆) ((ofProd c).symm z).1 +
          (⁅((ofProd c).symm x).1, ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆⁆ -
            ⁅((ofProd c).symm y).1, ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆⁆) -
        (⁅((ofProd c).symm z).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1⁆ +
            ⁅((ofProd c).symm z).1, ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆⁆ -
          ⁅((ofProd c).symm z).1, ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆⁆) +
      ((↑c ((ofProd c).symm y).1) ⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆ +
          (⁅((ofProd c).symm y).1, (↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1⁆ +
              ⁅((ofProd c).symm y).1, ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆⁆ -
            ⁅((ofProd c).symm y).1, ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆⁆) -
        (⁅((ofProd c).symm x).1, ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆⁆ -
          ⁅((ofProd c).symm z).1, ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆⁆))

Tactic:
abel

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝².left, x✝.left⁆ + ⁅x✝¹.left, x✝.left⁆ + ((ψ x✝².right) x✝.left + (ψ x✝¹.right) x✝.left) -
      ((ψ x✝.right) x✝².left + (ψ x✝.right) x✝¹.left) =
    ⁅x✝².left, x✝.left⁆ + (ψ x✝².right) x✝.left - (ψ x✝.right) x✝².left +
      (⁅x✝¹.left, x✝.left⁆ + (ψ x✝¹.right) x✝.left - (ψ x✝.right) x✝¹.left)

Tactic:
abel

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝².left, x✝¹.left⁆ + ⁅x✝².left, x✝.left⁆ + ((ψ x✝².right) x✝¹.left + (ψ x✝².right) x✝.left) -
      ((ψ x✝¹.right) x✝².left + (ψ x✝.right) x✝².left) =
    ⁅x✝².left, x✝¹.left⁆ + (ψ x✝².right) x✝¹.left - (ψ x✝¹.right) x✝².left +
      (⁅x✝².left, x✝.left⁆ + (ψ x✝².right) x✝.left - (ψ x✝.right) x✝².left)

Tactic:
abel

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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h : ↑c' = ↑c + (d₁₂ R L M) x
x✝¹ x✝ : ofTwoCocycle c
⊢ ((ofProd c).symm x✝¹).2 + ((ofProd c).symm x✝).2 - (x ((ofProd c).symm x✝¹).1 + x ((ofProd c).symm x✝).1) =
    ((ofProd c).symm x✝¹).2 - x ((ofProd c).symm x✝¹).1 + (((ofProd c).symm x✝).2 - x ((ofProd c).symm x✝).1)

Tactic:
abel

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✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h : ↑c' = ↑c + (d₁₂ R L M) x
x✝ y✝ : ofTwoCocycle c
⊢ (↑c ((ofProd c).symm x✝).1) ((ofProd c).symm y✝).1 + ⁅((ofProd c).symm x✝).1, ((ofProd c).symm y✝).2⁆ -
        ⁅((ofProd c).symm y✝).1, ((ofProd c).symm x✝).2⁆ -
      x ⁅((ofProd c).symm x✝).1, ((ofProd c).symm y✝).1⁆ =
    (↑c ((ofProd c).symm x✝).1) ((ofProd c).symm y✝).1 +
          (⁅((ofProd c).symm x✝).1, x ((ofProd c).symm y✝).1⁆ - ⁅((ofProd c).symm y✝).1, x ((ofProd c).symm x✝).1⁆ -
            x ⁅((ofProd c).symm x✝).1, ((ofProd c).symm y✝).1⁆) +
        (⁅((ofProd c).symm x✝).1, ((ofProd c).symm y✝).2⁆ - ⁅((ofProd c).symm x✝).1, x ((ofProd c).symm y✝).1⁆) -
      (⁅((ofProd c).symm y✝).1, ((ofProd c).symm x✝).2⁆ - ⁅((ofProd c).symm y✝).1, x ((ofProd c).symm x✝).1⁆)

Tactic:
abel

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
s✝ s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
⊢ ∀ (a : Nodup ⟦l₁⟧) (a' : Nodup ⟦l₂⟧), a ≍ a' → l₁.formPerm ≍ l₂.formPerm

Tactic:
intro h₁

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
s✝ s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
h₁ : Nodup ⟦l₁⟧
⊢ ∀ (a' : Nodup ⟦l₂⟧), h₁ ≍ a' → l₁.formPerm ≍ l₂.formPerm
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < (p.cycleOf x).support.card
⊢ x ∈ p.support

Tactic:
contrapose! hx

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : x ∉ p.support
⊢ (p.cycleOf x).support.card ≤ n
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 x✝¹ x✝ : L
⊢ ⁅s x, s x✝¹⁆ + ⁅s x, s x✝⁆ - (s ⁅x, x✝¹⁆ + s ⁅x, x✝⁆) = ⁅s x, s x✝¹⁆ - s ⁅x, x✝¹⁆ + (⁅s x, s x✝⁆ - s ⁅x, x✝⁆)

Tactic:
abel

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 x✝ : L
⊢ ⁅s x, s x✝⁆ + ⁅s y, s x✝⁆ - (s ⁅x, x✝⁆ + s ⁅y, x✝⁆) = ⁅s x, s x✝⁆ - s ⁅x, x✝⁆ + (⁅s y, s x✝⁆ - s ⁅y, x✝⁆)

Tactic:
abel

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

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
xj : ↥(AddMonoidAlgebra.grade R j) ⊗[R] L
x : ↥(AddMonoidAlgebra.grade R i)
y : L
⊢ ⁅(LinearMap.rTensor L (AddMonoidAlgebra.grade R i).subtype) (x ⊗ₜ[R] y),
      (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) xj⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range

Tactic:
simp only [LinearMap.rTensor_tmul, Submodule.subtype_apply]

Goal state after:
case tmul
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
xj : ↥(AddMonoidAlgebra.grade R j) ⊗[R] L
x : ↥(AddMonoidAlgebra.grade R i)
y : L
⊢ ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) xj⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate ↑k
⊢ l.formPerm.toList (l.get k) ~r l

Tactic:
formPerm_eq_of_isRotated hn hr

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate ↑k
⊢ (l.rotate ↑k).formPerm.toList (l.get k) ~r l
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
⊢ ((F f).sum fun a v ↦ a • (Φ ((F f) (-a))) v) = 0

Tactic:
set s := (F f).support ∪ (F f).support.image (Equiv.neg A) with hs
    have hs' : (F f).support ⊆ s := Finset.subset_union_left
    rw [Finsupp.sum_of_support_subset _ hs' _ (by simp)]
    refine Function.Odd.finsetSum_eq_zero (fun n ↦ by simp [hΦ.eq]) (Finset.map_eq_of_subset ?_)
    intro x hx
    rw [Finset.mem_union]
    replace hx : -x ∈ (F f).support ∨ -x ∈ (F f).support.image Neg.neg := by simpa [hs] using hx
    obtain (h | h) := hx
    · exact Or.inr <| Finset.mem_image.mpr ⟨-x, by simp [h]⟩
    · exact Or.inl <| by simpa using h

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

Goal state before:
pp: case intro.refine_2.mk.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).SameCycle x y
⊢ 2 ≤ l.length

Tactic:
contrapose! hx

Goal state after:
case intro.refine_2.mk.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).IsCycle
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).SameCycle x y
hx : l.length < 2
⊢ (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
hf : (s.formPerm hs).IsCycle
hs' : ∀ (y : Cycle α), (fun s_1 ↦ ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s
⊢ ∃! s_1, (↑s_1).formPerm ⋯ = s.formPerm hs

Tactic:
refine ⟨⟨s, hs⟩, rfl, ?_⟩

Goal state after:
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
hf : (s.formPerm hs).IsCycle
hs' : ∀ (y : Cycle α), (fun s_1 ↦ ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s
⊢ ∀ (y : { s // s.Nodup }), (fun s_1 ↦ (↑s_1).formPerm ⋯ = s.formPerm hs) y → y = ⟨s, hs⟩
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₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
this : ∀ {s' : L → E.L}, LeftInverse (⇑E.proj) s' → ⁅s x, s' y⁆ = ⁅s' x, s' y⁆ + (⁅s x, s y⁆ - ⁅s' x, s y⁆)
⊢ ⁅s₁ x, s₁ y⁆ + (⁅s x, s y⁆ - -⁅s y, s₁ x⁆) - (⁅s₂ x, s₂ y⁆ + (⁅s x, s y⁆ - -⁅s y, s₂ x⁆)) -
        (⁅s y, s₁ x⁆ - ⁅s y, s₂ x⁆) -
      (s₁ ⁅x, y⁆ - s₂ ⁅x, y⁆) =
    ⁅s₁ x, s₁ y⁆ - s₁ ⁅x, y⁆ - (⁅s₂ x, s₂ y⁆ - s₂ ⁅x, y⁆)

Tactic:
abel

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ Set.MapsTo
    (fun x ↦
      match x with
      | (α, k) => (k.removeNth α, α k))
    ↑(S (p + 1) i ×ˢ Finset.univ) ↑(S p i ×ˢ Finset.Ioi i)

Tactic:
rintro ⟨α, t⟩ hα
    simp only [Finset.coe_product, Finset.coe_univ, Set.mem_prod, Set.mem_univ, and_true,
      Finset.mem_coe, Finset.coe_Ioi, Set.mem_Ioi, mem_S_iff, Fin.strictMono_cons] at hα ⊢
    obtain ⟨hbound, hmono⟩ := hα
    exact ⟨⟨fun q => hbound (t.succAbove q), hmono.removeNth t⟩, hbound t⟩

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 : Prime ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩)
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

Tactic:
by
    simp only [associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq,
      associatesEquivOfUniqueUnits_symm_apply] at this
    obtain ⟨q, hq, hq'⟩ :=
      exists_mem_normalizedFactors_of_dvd hn this.irreducible
        (d ⟨p, by apply dvd_of_mem_normalizedFactors; convert! hp⟩).prop
    rwa [associated_iff_eq.mp hq']

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

Goal state before:
pp: case refine_4
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (a : R₁), ∀ x ∈ span R₁ (f '' ↑s), IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • a • x)

Tactic:
· intro c x _ hx
      rw [smul_comm]
      exact IsLocalization.isInteger_smul hx

Goal state after:
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
inst✝² : IsLocalization S P
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R P
x y : P
⊢ spanSingleton S x = spanSingleton S y ↔ ∃ z, z • x = y

Tactic:
rw [← Submodule.span_singleton_eq_span_singleton, spanSingleton, spanSingleton]

Goal state after:
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
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R P
x y : P
⊢ ⟨R ∙ x, ⋯⟩ = ⟨R ∙ y, ⋯⟩ ↔ R ∙ x = R ∙ y
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case succ
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 : P
n : ℕ
hn : spanSingleton S x ^ n = spanSingleton S (x ^ n)
⊢ spanSingleton S x ^ (n + 1) = spanSingleton S (x ^ (n + 1))

Tactic:
| succ n hn =>

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

Goal state before:
pp: case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
H : Ideal A
hH : ↑H = (↑I)⁻¹ * ↑J
⊢ I ∣ J

Tactic:
use H

Goal state after:
case h
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
H : Ideal A
hH : ↑H = (↑I)⁻¹ * ↑J
⊢ J = I * H
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mp.refine_1
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' : P
hx' : x' ∈ spanSingleton S x
y' : P
hy' : y' ∈ I
⊢ ∃ y'_1 ∈ I, x' * y' = x * y'_1

Tactic:
obtain ⟨a, ha⟩ := (mem_spanSingleton S).mp hx'

Goal state after:
case mp.refine_1
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' : P
hx' : x' ∈ spanSingleton S x
y' : P
hy' : y' ∈ I
a : R
ha : a • x = x'
⊢ ∃ y'_1 ∈ I, x' * y' = x * y'_1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg.a
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₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x ∈ J / spanSingleton R₁⁰ d
⊢ x ∈ 1 / spanSingleton R₁⁰ d * J

Tactic:
rw [← mem_coe, coe_div h_spand, Submodule.mem_div_iff_forall_mul_mem] at hx

Goal state after:
case neg.a
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₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : ∀ y ∈ ↑(spanSingleton R₁⁰ d), x * y ∈ ↑J
⊢ x ∈ 1 / spanSingleton R₁⁰ d * J
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
K : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
V : Type u_3
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Module R V
inst✝⁶ : IsScalarTower R K V
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Module.Finite K V
inst✝² : IsFractionRing R K
M N : Submodule R V
inst✝¹ : IsLattice K M
inst✝ : IsLattice K N
⊢ span K ↑(M ⊓ N) = ⊤

Tactic:
← range_subtype (M ⊓ N)

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
K : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
V : Type u_3
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Module R V
inst✝⁶ : IsScalarTower R K V
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Module.Finite K V
inst✝² : IsFractionRing R K
M N : Submodule R V
inst✝¹ : IsLattice K M
inst✝ : IsLattice K N
⊢ span K ↑(M ⊓ N).subtype.range = ⊤