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

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
h : LinearIndependent R w'
⊢ ∀ (a : m), diagonal w a = 0 ∨ ∃ b, w b ≠ 0 ∧ diagonal w b = diagonal w a

Tactic:
or_iff_not_imp_right,

Goal state after:
m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
h : LinearIndependent R w'
⊢ ∀ (a : m), (¬∃ b, w b ≠ 0 ∧ diagonal w b = diagonal w a) → diagonal w a = 0
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_1.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✝¹ : A
y✝¹ : L
x✝ y✝ : A ⊗[R] L
h1 :
  (LinearMap.lTensor A ↑d) ⁅x✝¹ ⊗ₜ[R] y✝¹, x✝⁆ =
    ⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) x✝⁆ - ⁅x✝, (LinearMap.lTensor A ↑d) (x✝¹ ⊗ₜ[R] y✝¹)⁆
h2 :
  (LinearMap.lTensor A ↑d) ⁅x✝¹ ⊗ₜ[R] y✝¹, y✝⁆ =
    ⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) y✝⁆ - ⁅y✝, (LinearMap.lTensor A ↑d) (x✝¹ ⊗ₜ[R] y✝¹)⁆
⊢ (LinearMap.lTensor A ↑d) ⁅x✝¹ ⊗ₜ[R] y✝¹, x✝ + y✝⁆ =
    ⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) (x✝ + y✝)⁆ - ⁅x✝ + y✝, (LinearMap.lTensor A ↑d) (x✝¹ ⊗ₜ[R] y✝¹)⁆

Tactic:
simp [h1, h2]

Goal state after:
case refine_1.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✝¹ : A
y✝¹ : L
x✝ y✝ : A ⊗[R] L
h1 :
  (LinearMap.lTensor A ↑d) ⁅x✝¹ ⊗ₜ[R] y✝¹, x✝⁆ =
    ⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) x✝⁆ - ⁅x✝, (LinearMap.lTensor A ↑d) (x✝¹ ⊗ₜ[R] y✝¹)⁆
h2 :
  (LinearMap.lTensor A ↑d) ⁅x✝¹ ⊗ₜ[R] y✝¹, y✝⁆ =
    ⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) y✝⁆ - ⁅y✝, (LinearMap.lTensor A ↑d) (x✝¹ ⊗ₜ[R] y✝¹)⁆
⊢ ⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) x✝⁆ - ⁅x✝, x✝¹ ⊗ₜ[R] d y✝¹⁆ +
      (⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) y✝⁆ - ⁅y✝, x✝¹ ⊗ₜ[R] d y✝¹⁆) =
    ⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) x✝⁆ + ⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) y✝⁆ -
      (⁅x✝, x✝¹ ⊗ₜ[R] d y✝¹⁆ + ⁅y✝, x✝¹ ⊗ₜ[R] d y✝¹⁆)
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 x✝ y✝ : A ⊗[R] L
h1 : (LinearMap.lTensor A ↑d) ⁅x✝, y⁆ = ⁅x✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) x✝⁆
h2 : (LinearMap.lTensor A ↑d) ⁅y✝, y⁆ = ⁅y✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) y✝⁆
⊢ (LinearMap.lTensor A ↑d) ⁅x✝ + y✝, y⁆ =
    ⁅x✝ + y✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x✝ + y✝)⁆

Tactic:
simp [h1, h2]

Goal state after:
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 x✝ y✝ : A ⊗[R] L
h1 : (LinearMap.lTensor A ↑d) ⁅x✝, y⁆ = ⁅x✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) x✝⁆
h2 : (LinearMap.lTensor A ↑d) ⁅y✝, y⁆ = ⁅y✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) y✝⁆
⊢ ⁅x✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) x✝⁆ +
      (⁅y✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) y✝⁆) =
    ⁅x✝, (LinearMap.lTensor A ↑d) y⁆ + ⁅y✝, (LinearMap.lTensor A ↑d) y⁆ -
      (⁅y, (LinearMap.lTensor A ↑d) x✝⁆ + ⁅y, (LinearMap.lTensor A ↑d) y✝⁆)
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)
⊢ F'.det = (f.mapMatrix (fromBlocks A B C D)).det

Tactic:
RingHom.mapMatrix_apply,

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)
⊢ F'.det = ((fromBlocks A B C D).map ⇑f).det
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y : L
⊢ y ∈ engel K x → engel K x ≤ engel K y

Tactic:
hy

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y : L
hy : y ∈ engel K x
⊢ engel K x ≤ engel K y
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
⊢ (n + 1) % orderOf (p.cycleOf x) = m + 1

Tactic:
← Nat.mod_eq_of_lt hm,

Goal state after:
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
⊢ (n + 1) % orderOf (p.cycleOf x) = (m + 1) % orderOf (p.cycleOf x)
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg.succ.succ.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
y : α
⊢ y ∈ (p.cycleOf x).support → (p.cycleOf x ^ (n + 1)) y = (p.cycleOf x ^ (m + 1)) y

Tactic:
hy

Goal state after:
case neg.succ.succ.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
y : α
hy : y ∈ (p.cycleOf x).support
⊢ (p.cycleOf x ^ (n + 1)) y = (p.cycleOf x ^ (m + 1)) y
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
left✝ : k + 1 < (f.cycleOf x).support.card
hy : (f ^ (k + 1)) x = y
⊢ f.toList ((f ^ k.succ) x) = f.toList y

Tactic:
hy

Goal state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
left✝ : k + 1 < (f.cycleOf x).support.card
hy : (f ^ (k + 1)) x = y
⊢ f.toList y = f.toList y
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: case tmul.add
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
x : ↥(AddMonoidAlgebra.grade R i)
y : L
u v : ↥(AddMonoidAlgebra.grade R j) ⊗[R] L
hu :
  ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) u⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
hv :
  ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) v⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
⊢ ⁅↑x ⊗ₜ[R] y,
      (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) u +
        (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) v⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range

Tactic:
lie_add

Goal state after:
case tmul.add
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
x : ↥(AddMonoidAlgebra.grade R i)
y : L
u v : ↥(AddMonoidAlgebra.grade R j) ⊗[R] L
hu :
  ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) u⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
hv :
  ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) v⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
⊢ ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) u⁆ +
      ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) v⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: case tmul.add
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
x : ↥(AddMonoidAlgebra.grade R i)
y : L
u v : ↥(AddMonoidAlgebra.grade R j) ⊗[R] L
hu :
  ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) u⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
hv :
  ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) v⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range
⊢ ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) (u + v)⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range

Tactic:
| add u v hu hv =>

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
⊢ (f.toList x).formPerm = f.cycleOf x

Tactic:
by
  by_cases hx : f x = x
  · rw [(cycleOf_eq_one_iff f).mpr hx, toList_eq_nil_iff.mpr (notMem_support.mpr hx),
      formPerm_nil]
  ext y
  by_cases hy : SameCycle f x y
  · obtain ⟨k, _, rfl⟩ := hy.exists_pow_eq_of_mem_support (mem_support.mpr hx)
    rw [cycleOf_apply_apply_pow_self, List.formPerm_apply_mem_eq_next (nodup_toList f x),
      next_toList_eq_apply, pow_succ', mul_apply]
    rw [mem_toList_iff]
    exact ⟨⟨k, rfl⟩, mem_support.mpr hx⟩
  · rw [cycleOf_apply_of_not_sameCycle hy, formPerm_apply_of_notMem]
    simp [mem_toList_iff, hy]

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
inst✝ : IsLieAbelian M
E : Extension R M L
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y z : L
hjac : ⁅s z, ⁅s x, s y⁆⁆ = -(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆)
hja : s ⁅z, ⁅x, y⁆⁆ = -s (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)
hj : s ⁅z, ⁅y, x⁆⁆ = -s (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆)
⊢ ⁅s x, ⁅s y, s z⁆⁆ - -⁅s (-⁅z, y⁆), s x⁆ - (⁅s y, ⁅s x, s z⁆⁆ - ⁅s y, s ⁅x, z⁆⁆) +
            (-(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆) - ⁅s z, s ⁅x, y⁆⁆) -
          (-⁅s z, s ⁅x, y⁆⁆ - (s ⁅x, -⁅z, y⁆⁆ - s ⁅y, ⁅x, z⁆⁆)) +
        (-⁅s y, s ⁅x, z⁆⁆ - (s ⁅x, ⁅z, y⁆⁆ - -s (⁅x, -⁅z, y⁆⁆ - ⁅y, ⁅x, z⁆⁆))) -
      (⁅s (-⁅z, y⁆), s x⁆ - (s ⁅y, ⁅z, x⁆⁆ - -s (⁅y, ⁅x, z⁆⁆ - ⁅x, -⁅z, y⁆⁆))) =
    0

Tactic:
← lie_skew x z

Goal state after:
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
inst✝ : IsLieAbelian M
E : Extension R M L
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y z : L
hjac : ⁅s z, ⁅s x, s y⁆⁆ = -(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆)
hja : s ⁅z, ⁅x, y⁆⁆ = -s (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)
hj : s ⁅z, ⁅y, x⁆⁆ = -s (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆)
⊢ ⁅s x, ⁅s y, s z⁆⁆ - -⁅s (-⁅z, y⁆), s x⁆ - (⁅s y, ⁅s x, s z⁆⁆ - ⁅s y, s (-⁅z, x⁆)⁆) +
            (-(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆) - ⁅s z, s ⁅x, y⁆⁆) -
          (-⁅s z, s ⁅x, y⁆⁆ - (s ⁅x, -⁅z, y⁆⁆ - s ⁅y, -⁅z, x⁆⁆)) +
        (-⁅s y, s (-⁅z, x⁆)⁆ - (s ⁅x, ⁅z, y⁆⁆ - -s (⁅x, -⁅z, y⁆⁆ - ⁅y, -⁅z, x⁆⁆))) -
      (⁅s (-⁅z, y⁆), s x⁆ - (s ⁅y, ⁅z, x⁆⁆ - -s (⁅y, -⁅z, x⁆⁆ - ⁅x, -⁅z, y⁆⁆))) =
    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✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
⊢ LinearMap.compr₂ (residuePairing R A L Φ) ↑(TrivialLieModule.equiv R (loopAlgebra R A L) R).symm ∈
    Cohomology.twoCochain R (loopAlgebra R A L) (TrivialLieModule R (loopAlgebra R A L) R)

Tactic:
by
    refine Cohomology.mem_twoCochain_iff.mpr fun f ↦ ?_
    let F := toFinsupp R A L
    suffices ((F f).sum fun a v ↦ a • Φ (F f (-a)) v) = 0 by simpa
    classical
    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.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 j : Fin n
hEq1 : Eq1 A p
⊢ (-1) ^ (p + 1) * ∑ i_1 ∈ S (p + 1) i, pminor A i_1 * A i j +
      ∑ x > i, (-1) ^ p * ∑ i_1 ∈ S p i, bminor A i x i_1 * A x j =
    (-1) ^ (p + 1) * (∑ α ∈ S (p + 1) i, pminor A α * A i j - ∑ k > i, ∑ α ∈ S p i, bminor A i k α * A k j)

Tactic:
← Finset.mul_sum

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
hEq1 : Eq1 A p
⊢ (-1) ^ (p + 1) * ∑ i_1 ∈ S (p + 1) i, pminor A i_1 * A i j +
      (-1) ^ p * ∑ i_1 > i, ∑ i_2 ∈ S p i, bminor A i i_1 i_2 * A i_1 j =
    (-1) ^ (p + 1) * (∑ α ∈ S (p + 1) i, pminor A α * A i j - ∑ k > i, ∑ α ∈ S p i, bminor A i k α * A k j)
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 j : Fin n
α : Fin (p + 1) → Fin n
k : Fin (p + 1)
hi : ∀ (j : Fin (p + 1)), i < α j
hiα : StrictMono α
k' : Fin (p + 1)
hj : ∀ (j : Fin (p + 1)), i < α j
hiα' : StrictMono α
hremove : k.removeNth α = k'.removeNth α
hvalue : α k = α k'
⊢ α = α ∧ k = k'

Tactic:
exact ⟨rfl, hiα.injective hvalue⟩

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 j : Fin n
α : Fin (p + 1) → Fin n
k : Fin (p + 1)
hi : ∀ (j : Fin (p + 1)), i < α j
hiα : StrictMono α
α' : Fin (p + 1) → Fin n
k' : Fin (p + 1)
hj : ∀ (j : Fin (p + 1)), i < α' j
hiα' : StrictMono α'
hremove : k.removeNth α = k'.removeNth α'
hvalue : α k = α' k'
⊢ Set.insert (α k) (Set.range (k.removeNth α)) = Set.insert (α' k') (Set.range (k'.removeNth α'))

Tactic:
rw [hvalue, hremove]

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

Goal state before:
pp: case inl.inr
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
H : derivedSeries k L 1 = ⊤
h✝ : Nontrivial L
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
exact ((derivedSeries_lt_top_of_solvable k L).ne H).elim

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
y : L
⊢ y ∈ rootSpace H γ → y ∈ LieSubmodule.restr I H

Tactic:
hy

Goal state after:
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
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
y : L
hy : y ∈ rootSpace H γ
⊢ y ∈ LieSubmodule.restr I H
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
h : ↥H
hI : ↑h ∈ I
β : ↥LieSubalgebra.root
hβ : ↑β h ≠ 0
y : L
⊢ y ∈ rootSpace H ⇑↑β → y ∈ LieSubmodule.restr I H

Tactic:
hy

Goal state after:
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
h : ↥H
hI : ↑h ∈ I
β : ↥LieSubalgebra.root
hβ : ↑β h ≠ 0
y : L
hy : y ∈ rootSpace H ⇑↑β
⊢ y ∈ LieSubmodule.restr I H
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
x✝ : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
⊢ b = b * (a * ↑ha.unit⁻¹)

Tactic:
IsUnit.mul_val_inv ha,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
x✝ : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
⊢ b = b * 1
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
h_inj : Function.Injective ⇑(algebraMap R P)
⊢ num 0 = 0

Tactic:
by
  simpa [num, LinearMap.ker_eq_bot] using! h_inj

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

Goal state before:
pp: case refine_2
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
x y : P
hx : IsInteger R ((aI * aJ) • x)
⊢ IsInteger R ((aI * aJ) • y) → IsInteger R ((aI * aJ) • (x + y))

Tactic:
hy

Goal state after:
case refine_2
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
x y : P
hx : IsInteger R ((aI * aJ) • x)
hy : IsInteger R ((aI * aJ) • y)
⊢ IsInteger R ((aI * aJ) • (x + y))
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)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : ↑(d ⟨p, ⋯⟩) = q
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

Tactic:
rwa [hq']

Goal state after:
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✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
y : K
⊢ y ∈ ↑I → 1 * y ∈ 1

Tactic:
hy

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✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
y : K
hy : y ∈ ↑I
⊢ 1 * y ∈ 1
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
⊢ ∃ Z, (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I

Tactic:
obtain ⟨Z₀, hZ₀⟩ := exists_primeSpectrum_prod_le_and_ne_bot_of_domain hNF hI0

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
⊢ ∃ Z, (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ spanSingleton R₁⁰ (generator ↑I) * spanSingleton R₁⁰ (generator ↑I)⁻¹ = 1

Tactic:
rw [spanSingleton_mul_spanSingleton, mul_inv_cancel₀, spanSingleton_one]

Goal state after:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ generator ↑I ≠ 0
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
x✝ : K
⊢ x✝ ∈ ⟨↑I / ↑1, ⋯⟩ ↔ x✝ ∈ I

Tactic:
constructor <;> intro h

Goal state after:
case mp
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
x✝ : K
h : x✝ ∈ ⟨↑I / ↑1, ⋯⟩
⊢ x✝ ∈ I

case mpr
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
x✝ : K
h : x✝ ∈ I
⊢ x✝ ∈ ⟨↑I / ↑1, ⋯⟩
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 J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
x : K
hx : x ∈ I
y : K
⊢ y ∈ 1 / I → x * y ∈ 1

Tactic:
hy

Goal state after:
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 J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
x : K
hx : x ∈ I
y : K
hy : y ∈ 1 / I
⊢ x * y ∈ 1