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

Goal state before:
pp: 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 : ι) (y : L i),
    (toModule R ι L' f') ⁅x, (of L i) y⁆ = ⁅(toModule R ι L' f') x, (toModule R ι L' f') ((of L i) y)⁆

Tactic:
suffices ∀ (i j) (y : L i) (x : L j),
          toModule R ι L' f' ⁅of L j x, of L i y⁆ =
            ⁅toModule R ι L' f' (of L j x), toModule R ι L' f' (of L i y)⁆ by
        intro i y
        rw [← lie_skew x, ← lie_skew (toModule R ι L' f' x)]
        simp only [map_neg, neg_inj, ← LieAlgebra.ad_apply R]
        rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]
        congr; clear x; ext j x; exact this j i x y

Goal state after:
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),
    (toModule R ι L' f') ⁅(of L j) x, (of L i) y⁆ =
      ⁅(toModule R ι L' f') ((of L j) x), (toModule R ι L' f') ((of L i) y)⁆
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
⊢ ∀ (x y : FreeLieAlgebra R X),
    Quot.liftOn (x + y) ⇑(liftAux R f) ⋯ = Quot.liftOn x ⇑(liftAux R f) ⋯ + Quot.liftOn y ⇑(liftAux R f) ⋯

Tactic:
rintro ⟨a⟩ ⟨b⟩; rw [← liftAux_map_add]; rfl

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

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
⊢ SetLike.GradedMonoid (grade R)

Tactic:
apply gradeBy.gradedMonoid (AddMonoidHom.id _)

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

Goal state before:
pp: case of
ι : 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 ℳ
i : ι
y : ↥(ℳ i) ⊗[R] N
this :
  (rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) y)
⊢ (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ)) ↑⟨(rTensor N (ℳ i).subtype) y, ⋯⟩ =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm
      ((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm
        ((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩))

Tactic:
LinearEquiv.eq_symm_apply,

Goal state after:
case of
ι : 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 ℳ
i : ι
y : ↥(ℳ i) ⊗[R] N
this :
  (rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) y)
⊢ (directSumLeft R R (fun i ↦ ↥(ℳ i)) N)
      ((LinearEquiv.rTensor N (decomposeLinearEquiv ℳ)) ↑⟨(rTensor N (ℳ i).subtype) y, ⋯⟩) =
    (congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm
      ((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩)
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: case of
ι : 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 ℳ
i : ι
y : ↥(ℳ i) ⊗[R] N
this :
  (rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) y)
⊢ (directSumLeft R R (fun i ↦ ↥(ℳ i)) N)
      ((LinearEquiv.rTensor N (decomposeLinearEquiv ℳ)) ↑⟨(rTensor N (ℳ i).subtype) y, ⋯⟩) =
    (congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm
      ((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩)

Tactic:
LinearEquiv.eq_symm_apply,

Goal state after:
case of
ι : 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 ℳ
i : ι
y : ↥(ℳ i) ⊗[R] N
this :
  (rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) y)
⊢ (congrLinearEquiv (decomposeTensorEquiv ℳ N))
      ((directSumLeft R R (fun i ↦ ↥(ℳ i)) N)
        ((LinearEquiv.rTensor N (decomposeLinearEquiv ℳ)) ↑⟨(rTensor N (ℳ i).subtype) y, ⋯⟩)) =
    (of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩
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
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
⊢ { toFun := fun x ↦ (ofProd c) (0, x), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }.ker = ⊥

Tactic:
by
        rw [LieHom.ker_eq_bot]
        intro x y
        simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ↑[l.attach.length] = {l.length}

pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ∀ (x : { x // x ∈ l }), l.attach ≠ [x]

Tactic:
· simp

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ ∀ (x : { x // x ∈ l }), l.attach ≠ [x]
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case h0
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ [l.attach.formPerm].prod = l.attach.formPerm

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:
· simp

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

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.GroupTheory.Perm.Cycle.Concrete

Goal state before:
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:
· simp

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

Goal state before:
pp: case mk.nil
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
h : [].length ≤ 1
⊢ [].formPerm = 1

pp: case mk.cons
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hd : α
tl : List α
h : (hd :: tl).length ≤ 1
⊢ (hd :: tl).formPerm = 1

Tactic:
· simp

Goal state after:
case mk.cons
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hd : α
tl : List α
h : (hd :: tl).length ≤ 1
⊢ (hd :: tl).formPerm = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : (p.cycleOf x) x ≠ x
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ (fun i ↦ (p.toList x)[↑i]) ⟨n, hn✝⟩ = (fun i ↦ (p.toList x)[↑i]) ⟨m, hm✝⟩ → ⟨n, hn✝⟩ = ⟨m, hm✝⟩

Tactic:
← mem_support

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ (fun i ↦ (p.toList x)[↑i]) ⟨n, hn✝⟩ = (fun i ↦ (p.toList x)[↑i]) ⟨m, hm✝⟩ → ⟨n, hn✝⟩ = ⟨m, hm✝⟩
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg.zero.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
hn✝ : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
hm✝ : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ 0) x = (p.cycleOf x ^ 0) x → 0 = 0

pp: case neg.zero.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
hn✝ : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ 0) x = (p.cycleOf x ^ (m + 1)) x → 0 = m + 1

pp: case neg.succ.zero
α : 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)
hm✝ : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ 0) x → n + 1 = 0

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)
⊢ (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x → n + 1 = m + 1

Tactic:
· simp

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

case neg.succ.zero
α : 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)
hm✝ : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ 0) x → n + 1 = 0

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)
⊢ (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x → n + 1 = m + 1
Module: Mathlib.Algebra.Lie.Loop

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

Tactic:
obtain ⟨u, hu⟩ := u

Goal state after:
case tmul.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
y v : L
x : AddMonoidAlgebra R A
hx : x ∈ AddMonoidAlgebra.grade R i
u : AddMonoidAlgebra R A
hu : u ∈ AddMonoidAlgebra.grade R j
⊢ ⁅↑⟨x, hx⟩ ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) (⟨u, hu⟩ ⊗ₜ[R] v)⁆ ∈
    (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.rotate ↑k ~r l

pp: case hl
α : 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
⊢ 2 ≤ (l.rotate ↑k).length

pp: case hn
α : 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).Nodup

Tactic:
· simp

Goal state after:
case hl
α : 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
⊢ 2 ≤ (l.rotate ↑k).length

case hn
α : 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).Nodup
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
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
⊢ l.formPerm = 1

Tactic:
rw [formPerm_eq_one_iff _ hn]

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
⊢ l.length ≤ 1
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Φ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : ¬a + b + c = 0
⊢ -b ≠ a + c

Tactic:
by grind

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : ¬a + b + c = 0
⊢ -c ≠ a + b

Tactic:
by grind

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : ¬a + b + c = 0
⊢ -a ≠ b + c

Tactic:
by grind

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

Goal state before:

Tactic:
_ = Set.insert (α k) (Set.range (k.removeNth α)) := by
        rw [← Fin.range_insertNth, Fin.insertNth_self_removeNth]
      _ = Set.insert (α' k') (Set.range (k'.removeNth α')) := by
        rw [hvalue, hremove]
      _ = Set.range α' := by
        rw [← Fin.range_insertNth, Fin.insertNth_self_removeNth]

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

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ i_1 ∈ S (p + 1) i ×ˢ Finset.univ,
    bminor A i (i_1.1 i_1.2) (i_1.2.removeNth i_1.1) * A (i_1.1 i_1.2) j =
      bminor A i
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).1 *
        A
          (match i_1 with
            | (α, k) => (k.removeNth α, α k)).2
          j

Tactic:
· simp

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

Goal state before:
pp: n : ℕ
i✝ j✝ : Fin n
⊢ (B n)ᵀ i✝ j✝ = C n i✝ j✝

Tactic:
simp only [B, C, transpose_apply, of_apply]

Goal state after:
n : ℕ
i✝ j✝ : Fin n
⊢ (if j✝ = i✝ then 2 else if ↑j✝ + 1 = ↑i✝ then if ↑i✝ = n - 1 then -2 else -1 else if ↑i✝ + 1 = ↑j✝ then -1 else 0) =
    if i✝ = j✝ then 2 else if ↑i✝ + 1 = ↑j✝ then -1 else if ↑j✝ + 1 = ↑i✝ then if ↑i✝ = n - 1 then -2 else -1 else 0
Module: Mathlib.RingTheory.ChainOfDivisors

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

Tactic:
← Associates.le_one_iff,

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

Goal state before:
pp: ⊢ E₆.det = 3

Tactic:
simp only [E₆, norm_det]

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'
⊢ emultiplicity (↑(d ⟨p, ⋯⟩)) n = emultiplicity p m

Tactic:
apply Eq.symm
  suffices emultiplicity (Associates.mk p) (Associates.mk m) = emultiplicity (Associates.mk
    ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by
      simp [dvd_of_mem_normalizedFactors hp]⟩)) (Associates.mk n) by
    simpa only [emultiplicity_mk_eq_emultiplicity, associatesEquivOfUniqueUnits_symm_apply,
      associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq] using this
  have : Associates.mk (d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by
    simp only [dvd_of_mem_normalizedFactors hp, associatesEquivOfUniqueUnits_symm_apply,
      associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq]⟩ : N) =
    ↑(mkFactorOrderIsoOfFactorDvdEquiv hd ⟨associatesEquivOfUniqueUnits.symm p, by
      rw [associatesEquivOfUniqueUnits_symm_apply]
      exact mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp)⟩) := by
    rw [mkFactorOrderIsoOfFactorDvdEquiv_apply_coe]
  rw [this]
  refine
    emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso (mk_ne_zero.mpr hn) ?_
      (mkFactorOrderIsoOfFactorDvdEquiv hd)
  obtain ⟨q, hq, hq'⟩ :=
    exists_mem_normalizedFactors_of_dvd (mk_ne_zero.mpr hm)
      (prime_mk.mpr (prime_of_normalized_factor p hp)).irreducible
      (mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp))
  rwa [associated_iff_eq.mp hq']

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 J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ ∀ x ∈ J, ∀ y ∈ I, x * y ∈ I * J

Tactic:
intro y hy x hx

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
y : K
hy : y ∈ J
x : K
hx : x ∈ I
⊢ y * x ∈ I * J
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✝ : ∃ J, I * J = 1
J : FractionalIdeal R₁⁰ K
hJ : I * J = 1
⊢ I * (1 / I) = 1

Tactic:
rwa [← eq_one_div_of_mul_eq_one_right I J hJ]

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

Goal state before:
pp: case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
I : Ideal A
hI : I = ⊥
⊢ Submodule.FG ⊥

Tactic:
apply Submodule.fg_bot

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 ≠ ⊥

pp: case hJ
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
⊢ Irreducible p

Tactic:
· rw [← Ideal.zero_eq_bot]; apply pow_ne_zero; exact (prime_of_mem q hq).ne_zero

Goal state after:
case hJ
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
⊢ Irreducible p
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ I ⊔ J = (normalizedFactors I ∩ normalizedFactors J).prod

Tactic:
have := prod_inter_normalizedFactors_ne_zero I J
  apply le_antisymm
  · rw [sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]
    constructor <;>
      rw [dvd_iff_normalizedFactors_le_normalizedFactors this (by assumption),
        normalizedFactors_prod_inter_eq_inter]
    exacts [inf_le_left, inf_le_right]
  · rw [← dvd_iff_le, dvd_iff_normalizedFactors_le_normalizedFactors ?H this,
      normalizedFactors_prod_inter_eq_inter, le_iff_count]
    case H => exact ne_bot_of_le_ne_bot hI le_sup_left
    intro a
    rw [Multiset.count_inter]
    exact le_min (count_le_of_ideal_ge le_sup_left hI a) (count_le_of_ideal_ge le_sup_right hJ a)

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

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
J : Ideal A
X : { p // p ∣ J }
⊢ (idealFactorsFunOfQuotHom ⋯) X = OrderHom.id X

Tactic:
simp only [idealFactorsFunOfQuotHom, map_id, OrderHom.coe_mk, OrderHom.id_coe, id,
        comap_map_of_surjective (Ideal.Quotient.mk J) Ideal.Quotient.mk_surjective, ←
        RingHom.ker_eq_comap_bot (Ideal.Quotient.mk J), mk_ker,
        sup_eq_left.mpr (dvd_iff_le.mp X.prop), Subtype.coe_eta]

Goal state after: