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

Goal state before:
pp: case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.mk (Rel R X) ((fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 + x2) a b) c) =
    Quot.mk (Rel R X) ((fun x1 x2 ↦ x1 + x2) ((fun x1 x2 ↦ x1 * x2) a c) ((fun x1 x2 ↦ x1 * x2) b c))

Tactic:
;

Goal state after:
case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.mk (Rel R X) ((fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 + x2) a b) c) =
    Quot.mk (Rel R X) ((fun x1 x2 ↦ x1 + x2) ((fun x1 x2 ↦ x1 * x2) a c) ((fun x1 x2 ↦ x1 * x2) b c))
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b + Quot.mk (Rel R X) c) =
    Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b) +
      Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) c)

Tactic:
;

Goal state after:
case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b + Quot.mk (Rel R X) c) =
    Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b) +
      Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) c)
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.mk (Rel R X) ((fun x1 x2 ↦ x1 * x2) a ((fun x1 x2 ↦ x1 + x2) b c)) =
    Quot.mk (Rel R X) ((fun x1 x2 ↦ x1 + x2) ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c))

Tactic:
;

Goal state after:
case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.mk (Rel R X) ((fun x1 x2 ↦ x1 * x2) a ((fun x1 x2 ↦ x1 + x2) b c)) =
    Quot.mk (Rel R X) ((fun x1 x2 ↦ x1 + x2) ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c))
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) a) = 0

Tactic:
;

Goal state after:
case mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) a) = 0
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a)
      (Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) b) (Quot.mk (Rel R X) c)) =
    Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯
        (Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b)) (Quot.mk (Rel R X) c) +
      Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) b)
        (Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) c))

Tactic:
;

Goal state after:
case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a)
      (Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) b) (Quot.mk (Rel R X) c)) =
    Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯
        (Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) b)) (Quot.mk (Rel R X) c) +
      Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) b)
        (Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ (Quot.mk (Rel R X) a) (Quot.mk (Rel R X) c))
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (Quot.mk (Rel R X) a + Quot.mk (Rel R X) b) ⇑(liftAux R f) ⋯ =
    (Quot.mk (Rel R X) a).liftOn ⇑(liftAux R f) ⋯ + (Quot.mk (Rel R X) b).liftOn ⇑(liftAux R f) ⋯

Tactic:
;

Goal state after:
case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (Quot.mk (Rel R X) a + Quot.mk (Rel R X) b) ⇑(liftAux R f) ⋯ =
    (Quot.mk (Rel R X) a).liftOn ⇑(liftAux R f) ⋯ + (Quot.mk (Rel R X) b).liftOn ⇑(liftAux R f) ⋯
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (Quot.mk (Rel R X) a + Quot.mk (Rel R X) b) ⇑(liftAux R f) ⋯ = (liftAux R f) (a + b)

Tactic:
;

Goal state after:
case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (Quot.mk (Rel R X) a + Quot.mk (Rel R X) b) ⇑(liftAux R f) ⋯ = (liftAux R f) (a + b)
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
t : R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (t • Quot.mk (Rel R X) a) ⇑(liftAux R f) ⋯ =
    (RingHom.id R) t • (Quot.mk (Rel R X) a).liftOn ⇑(liftAux R f) ⋯

Tactic:
;

Goal state after:
case mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
t : R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (t • Quot.mk (Rel R X) a) ⇑(liftAux R f) ⋯ =
    (RingHom.id R) t • (Quot.mk (Rel R X) a).liftOn ⇑(liftAux R f) ⋯
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
t : R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (t • Quot.mk (Rel R X) a) ⇑(liftAux R f) ⋯ = (liftAux R f) ((RingHom.id R) t • a)

Tactic:
;

Goal state after:
case mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
t : R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (t • Quot.mk (Rel R X) a) ⇑(liftAux R f) ⋯ = (liftAux R f) ((RingHom.id R) t • a)
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn ⁅Quot.mk (Rel R X) a, Quot.mk (Rel R X) b⁆ ⇑(liftAux R f) ⋯ =
    ⁅(Quot.mk (Rel R X) a).liftOn ⇑(liftAux R f) ⋯, (Quot.mk (Rel R X) b).liftOn ⇑(liftAux R f) ⋯⁆

Tactic:
;

Goal state after:
case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn ⁅Quot.mk (Rel R X) a, Quot.mk (Rel R X) b⁆ ⇑(liftAux R f) ⋯ =
    ⁅(Quot.mk (Rel R X) a).liftOn ⇑(liftAux R f) ⋯, (Quot.mk (Rel R X) b).liftOn ⇑(liftAux R f) ⋯⁆
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn ⁅Quot.mk (Rel R X) a, Quot.mk (Rel R X) b⁆ ⇑(liftAux R f) ⋯ = (liftAux R f) (a * b)

Tactic:
;

Goal state after:
case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn ⁅Quot.mk (Rel R X) a, Quot.mk (Rel R X) b⁆ ⇑(liftAux R f) ⋯ = (liftAux R f) (a * b)
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 : FreeLieAlgebra R X →ₗ⁅R⁆ L
⊢ (lift R) ((lift R).symm F) = F

Tactic:
;

Goal state after:
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F : FreeLieAlgebra R X →ₗ⁅R⁆ L
⊢ (lift R) ((lift R).symm F) = F
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₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L
h : ∀ (x : X), F₁ (of R x) = F₂ (of R x)
x✝ : X
⊢ (lift R).symm F₁ x✝ = (lift R).symm F₂ x✝

Tactic:
;

Goal state after:
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L
h : ∀ (x : X), F₁ (of R x) = F₂ (of R x)
x✝ : X
⊢ (lift R).symm F₁ x✝ = (lift R).symm F₂ x✝
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
x✝ : X
⊢ (⇑(((UniversalEnvelopingAlgebra.lift R) ((lift R) (FreeAlgebra.ι R))).comp
            ((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ of R))) ∘
        FreeAlgebra.ι R)
      x✝ =
    (⇑(AlgHom.id R (FreeAlgebra R X)) ∘ FreeAlgebra.ι R) x✝

Tactic:
;

Goal state after:
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝ : X
⊢ (⇑(((UniversalEnvelopingAlgebra.lift R) ((lift R) (FreeAlgebra.ι R))).comp
            ((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ of R))) ∘
        FreeAlgebra.ι R)
      x✝ =
    (⇑(AlgHom.id R (FreeAlgebra R X)) ∘ FreeAlgebra.ι R) x✝
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
x✝ : X
⊢ ((((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ of R)).comp
              ((UniversalEnvelopingAlgebra.lift R) ((lift R) (FreeAlgebra.ι R)))).toLieHom.comp
        (UniversalEnvelopingAlgebra.ι R))
      (of R x✝) =
    ((AlgHom.id R (UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))).toLieHom.comp (UniversalEnvelopingAlgebra.ι R))
      (of R x✝)

Tactic:
;

Goal state after:
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝ : X
⊢ ((((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ of R)).comp
              ((UniversalEnvelopingAlgebra.lift R) ((lift R) (FreeAlgebra.ι R)))).toLieHom.comp
        (UniversalEnvelopingAlgebra.ι R))
      (of R x✝) =
    ((AlgHom.id R (UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))).toLieHom.comp (UniversalEnvelopingAlgebra.ι R))
      (of R x✝)
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ (∃ b, a.coeff = Finsupp.single m b) ↔ a ∈ (lsingle m).range

Tactic:
;

Goal state after:
M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ (∃ b, a.coeff = Finsupp.single m b) ↔ a ∈ (lsingle m).range
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case single_zero_right
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m✝ a✝ : M
⊢ (((coeAlgHom (gradeBy R ⇑f)).comp (decomposeAux f)) (single m✝ 1)).coeff a✝ =
    ((AlgHom.id R R[M]) (single m✝ 1)).coeff a✝

Tactic:
;

Goal state after:
case single_zero_right
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m✝ a✝ : M
⊢ (((coeAlgHom (gradeBy R ⇑f)).comp (decomposeAux f)) (single m✝ 1)).coeff a✝ =
    ((AlgHom.id R R[M]) (single m✝ 1)).coeff a✝
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:
;

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✝³ : 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⁆)
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
i : ι
x y : S ⊗[R] ↥(ℳ i)
h : (Submodule.toBaseChange S (ℳ i)) x = (Submodule.toBaseChange S (ℳ i)) y
⊢ Function.Bijective
    ⇑↑((LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)).trans
          (directSumRight R S S fun i ↦ ↥(ℳ i)))

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
i : ι
x y : S ⊗[R] ↥(ℳ i)
h : (Submodule.toBaseChange S (ℳ i)) x = (Submodule.toBaseChange S (ℳ i)) y
⊢ Function.Bijective
    ⇑↑((LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)).trans
          (directSumRight R S S fun i ↦ ↥(ℳ i)))
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
i : ι
x y : S ⊗[R] ↥(ℳ i)
h : (Submodule.toBaseChange S (ℳ i)) x = (Submodule.toBaseChange S (ℳ i)) y
⊢ x = y

Tactic:
by
  have := (Function.Bijective.of_comp_iff (lmap (ℳ · |>.toBaseChange S))
    (by rw [← LinearEquiv.coe_trans]; exact LinearEquiv.bijective _)).1
    (decompose (M := S ⊗[R] M) fun i ↦ (ℳ i).baseChange S).bijective
  refine of_injective (β := fun i ↦ S ⊗[R] ℳ i) i <| this.injective ?_
  simpa using congr(of (fun i ↦ (ℳ i).baseChange S) i $h)

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 ℳ
i : ι
x✝¹ : ↥(ℳ i)
x✝ : N
⊢ ((AlgebraTensorModule.curry
          (rTensor N (component R ι (fun i ↦ ↥(ℳ i)) i ∘ₗ ↑(decomposeLinearEquiv ℳ)) ∘ₗ rTensor N (ℳ i).subtype))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry LinearMap.id) x✝¹) x✝

Tactic:
;

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 ℳ
i : ι
x✝¹ : ↥(ℳ i)
x✝ : N
⊢ ((AlgebraTensorModule.curry
          (rTensor N (component R ι (fun i ↦ ↥(ℳ i)) i ∘ₗ ↑(decomposeLinearEquiv ℳ)) ∘ₗ rTensor N (ℳ i).subtype))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry LinearMap.id) x✝¹) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
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 : ι
x : ↥(ℳ i) ⊗[R] N
⊢ (rTensor N (ℳ i).subtype) x = ↑((decomposeTensorEquiv ℳ N i) x)

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
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 : ι
x : ↥(ℳ i) ⊗[R] N
⊢ (rTensor N (ℳ i).subtype) x = ↑((decomposeTensorEquiv ℳ N i) x)
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 ℳ
i : ι
x : ↥(ℳ i) ⊗[R] N
i✝ : ι
⊢ ↑(((congrLinearEquiv fun i ↦ decomposeTensorEquiv ℳ N i) ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) x)) i✝) =
    ↑(((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ((decomposeTensorEquiv ℳ N i) x)) i✝)

Tactic:
;

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 ℳ
i : ι
x : ↥(ℳ i) ⊗[R] N
i✝ : ι
⊢ ↑(((congrLinearEquiv fun i ↦ decomposeTensorEquiv ℳ N i) ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) x)) i✝) =
    ↑(((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ((decomposeTensorEquiv ℳ N i) x)) i✝)
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
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
x✝ : ↥(ℳ i)
i✝ : ι
⊢ ↑(((↑(decomposeLinearEquiv ℳ) ∘ₗ (ℳ i).subtype) x✝) i✝) = ↑(((lof R ι (fun i ↦ ↥(ℳ i)) i) x✝) i✝)

Tactic:
;

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
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
x✝ : ↥(ℳ i)
i✝ : ι
⊢ ↑(((↑(decomposeLinearEquiv ℳ) ∘ₗ (ℳ i).subtype) x✝) i✝) = ↑(((lof R ι (fun i ↦ ↥(ℳ i)) i) x✝) i✝)