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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : ↥σ → N := fun x ↦ (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : ↥τ → ↥S
hs' : ∀ (x : ↥τ), s' x • (linearCombination R i) ↑x = 0
s₁ : ↥S := ∏ i, s' i
this : π.ker ≤ (s₁ • linearCombination R i).ker
x : ↥σ →₀ R
⊢ ((f ∘ₗ π.ker.liftQ (s₁ • linearCombination R i) this ∘ₗ ↑(π.quotKerEquivOfSurjective hπ).symm) ∘ₗ π) x =
    ((s₁ • s₀ • g) ∘ₗ π) x

Tactic:
LinearMap.smul_comp,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : ↥σ → N := fun x ↦ (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : ↥τ → ↥S
hs' : ∀ (x : ↥τ), s' x • (linearCombination R i) ↑x = 0
s₁ : ↥S := ∏ i, s' i
this : π.ker ≤ (s₁ • linearCombination R i).ker
x : ↥σ →₀ R
⊢ ((f ∘ₗ π.ker.liftQ (s₁ • linearCombination R i) this ∘ₗ ↑(π.quotKerEquivOfSurjective hπ).symm) ∘ₗ π) x =
    (s₁ • (s₀ • g) ∘ₗ π) x
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
⊢ ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆

Tactic:
hm_α_decomp,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
⊢ ⁅x_χ, m_pos + m_neg + m_h⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
⊢ (s₀ • ↑e.symm ∘ₗ g) ∘ₗ l = f ∘ₗ (s₀ • LinearMap.id)

Tactic:
LinearMap.smul_comp,

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
⊢ s₀ • (↑e.symm ∘ₗ g) ∘ₗ l = f ∘ₗ (s₀ • LinearMap.id)
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h.zero
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin 0 → M
hs : Submodule.span R (Set.range s) = ⊤
⊢ ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin 0), R ⧸ R ∙ p ^ k i)

Tactic:
use finZeroElim

Goal state after:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin 0 → M
hs : Submodule.span R (Set.range s) = ⊤
⊢ Nonempty (M ≃ₗ[R] ⨁ (i : Fin 0), R ⧸ R ∙ p ^ finZeroElim i)
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h.succ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst : AddCommGroup M] [inst_1 : Module R M],
    IsTorsion' M ↥(Submonoid.powers p) →
      ∀ (s : Fin d → M), Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
⊢ ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin (d + 1)), R ⧸ R ∙ p ^ k i)

Tactic:
have := IH ?_ s' ?_

Goal state after:
case h.succ.refine_3
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst : AddCommGroup M] [inst_1 : Module R M],
    IsTorsion' M ↥(Submonoid.powers p) →
      ∀ (s : Fin d → M), Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
this : ∃ k, Nonempty ((M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
⊢ ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin (d + 1)), R ⧸ R ∙ p ^ k i)

case h.succ.refine_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst : AddCommGroup M] [inst_1 : Module R M],
    IsTorsion' M ↥(Submonoid.powers p) →
      ∀ (s : Fin d → M), Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
⊢ IsTorsion' (M ⧸ R ∙ s j) ↥(Submonoid.powers p)

case h.succ.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst : AddCommGroup M] [inst_1 : Module R M],
    IsTorsion' M ↥(Submonoid.powers p) →
      ∀ (s : Fin d → M), Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
⊢ Submodule.span R (Set.range s') = ⊤
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ (s₀ • LinearMap.id)
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • s₀ • LinearMap.id
t : R
ht : ↑s₀ * ↑s₁ * ↑s₂ ∣ t
Rₛ : Type u_3 := Localization (Submonoid.powers t)
lₛ : LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) N :=
  (LocalizedModule.map (Submonoid.powers t)) l
hu : IsUnit ((algebraMap R Rₛ) ↑⟨t, ⋯⟩)
hu₀ : IsUnit ((algebraMap R Rₛ) ↑s₀)
hu₁ : IsUnit ((algebraMap R Rₛ) ↑s₁)
hu₂ : IsUnit ((algebraMap R Rₛ) ↑s₂)
lₛ' : LocalizedModule (Submonoid.powers t) N →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) M :=
  (LocalizedModule.map (Submonoid.powers t)) l'
⊢ ↑s₂ • ↑s₀ • (↑hu₀.unit⁻¹ • lₛ') ∘ₗ lₛ = ↑s₂ • ↑s₀ • LinearMap.id

Tactic:
LinearMap.smul_comp,

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ (s₀ • LinearMap.id)
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • s₀ • LinearMap.id
t : R
ht : ↑s₀ * ↑s₁ * ↑s₂ ∣ t
Rₛ : Type u_3 := Localization (Submonoid.powers t)
lₛ : LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) N :=
  (LocalizedModule.map (Submonoid.powers t)) l
hu : IsUnit ((algebraMap R Rₛ) ↑⟨t, ⋯⟩)
hu₀ : IsUnit ((algebraMap R Rₛ) ↑s₀)
hu₁ : IsUnit ((algebraMap R Rₛ) ↑s₁)
hu₂ : IsUnit ((algebraMap R Rₛ) ↑s₂)
lₛ' : LocalizedModule (Submonoid.powers t) N →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) M :=
  (LocalizedModule.map (Submonoid.powers t)) l'
⊢ ↑s₂ • ↑s₀ • ↑hu₀.unit⁻¹ • lₛ' ∘ₗ lₛ = ↑s₂ • ↑s₀ • LinearMap.id
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
⊢ X i * (pderiv i) ((monomial m) r) = m i • (monomial m) r

Tactic:
by
  rw [pderiv_monomial, X, monomial_mul, smul_monomial]
  by_cases h : m i = 0
  · simp_rw [h, Nat.cast_zero, mul_zero, zero_smul, monomial_zero]
  rw [one_mul, mul_comm, nsmul_eq_mul, add_comm, sub_add_single_one_cancel h]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case monomial
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m n : σ →₀ ℕ
a : R
⊢ (if n - single i 1 = m then a * ↑(n i) else 0) = (if n = m + single i 1 then a else 0) * (↑(m i) + 1)

Tactic:
by_cases h : n = m + single i 1

Goal state after:
case pos
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m n : σ →₀ ℕ
a : R
h : n = m + single i 1
⊢ (if n - single i 1 = m then a * ↑(n i) else 0) = (if n = m + single i 1 then a else 0) * (↑(m i) + 1)

case neg
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m n : σ →₀ ℕ
a : R
h : ¬n = m + single i 1
⊢ (if n - single i 1 = m then a * ↑(n i) else 0) = (if n = m + single i 1 then a else 0) * (↑(m i) + 1)
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case pos
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h : (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
h✝ : a = x
⊢ (rename f) p + X (f a) * (rename f) ((pderiv x) p) = (rename f) p + X (f a) * (rename f) ((pderiv x) p)

pp: case neg
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h : (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
h✝ : ¬a = x
⊢ 0 + X (f a) * (rename f) ((pderiv x) p) = (rename f) 0 + X (f a) * (rename f) ((pderiv x) p)

Tactic:
<;>

Goal state after:
case pos
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h : (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
h✝ : a = x
⊢ (rename f) p + X (f a) * (rename f) ((pderiv x) p) = (rename f) p + X (f a) * (rename f) ((pderiv x) p)

case neg
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h : (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
h✝ : ¬a = x
⊢ 0 + X (f a) * (rename f) ((pderiv x) p) = (rename f) 0 + X (f a) * (rename f) ((pderiv x) p)
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case mul_X.inl
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : σ
⊢ (aeval (Sum.elim X (⇑C ∘ f))) p * (aeval (Sum.elim X (⇑C ∘ f))) (Pi.single (Sum.inl j) 1 (Sum.inl val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inl val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p) =
    (aeval (Sum.elim X (⇑C ∘ f))) p * (pderiv j) (Sum.elim X (⇑C ∘ f) (Sum.inl val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inl val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)

pp: case mul_X.inr
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : τ
⊢ (aeval (Sum.elim X (⇑C ∘ f))) p * (aeval (Sum.elim X (⇑C ∘ f))) (Pi.single (Sum.inl j) 1 (Sum.inr val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inr val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p) =
    (aeval (Sum.elim X (⇑C ∘ f))) p * (pderiv j) (Sum.elim X (⇑C ∘ f) (Sum.inr val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inr val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)

Tactic:
<;>

Goal state after:
case mul_X.inl
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : σ
⊢ (aeval (Sum.elim X (⇑C ∘ f))) p * (aeval (Sum.elim X (⇑C ∘ f))) (Pi.single (Sum.inl j) 1 (Sum.inl val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inl val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p) =
    (aeval (Sum.elim X (⇑C ∘ f))) p * (pderiv j) (Sum.elim X (⇑C ∘ f) (Sum.inl val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inl val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)

case mul_X.inr
R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : τ → S
j : σ
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : τ
⊢ (aeval (Sum.elim X (⇑C ∘ f))) p * (aeval (Sum.elim X (⇑C ∘ f))) (Pi.single (Sum.inl j) 1 (Sum.inr val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inr val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p) =
    (aeval (Sum.elim X (⇑C ∘ f))) p * (pderiv j) (Sum.elim X (⇑C ∘ f) (Sum.inr val✝)) +
      Sum.elim X (⇑C ∘ f) (Sum.inr val✝) * (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case mul_X.inl
R : Type u
inst✝ : CommSemiring R
σ : Type u_1
ι : Type u_2
i : σ
p : MvPolynomial (σ ⊕ ι) R
a✝ : (pderiv i) ((sumRingEquiv R σ ι) p) = (sumRingEquiv R σ ι) ((pderiv (Sum.inl i)) p)
val✝ : σ
⊢ (pderiv i) ((sumRingEquiv R σ ι) (p * X (Sum.inl val✝))) =
    (sumRingEquiv R σ ι) ((pderiv (Sum.inl i)) (p * X (Sum.inl val✝)))

pp: case mul_X.inr
R : Type u
inst✝ : CommSemiring R
σ : Type u_1
ι : Type u_2
i : σ
p : MvPolynomial (σ ⊕ ι) R
a✝ : (pderiv i) ((sumRingEquiv R σ ι) p) = (sumRingEquiv R σ ι) ((pderiv (Sum.inl i)) p)
val✝ : ι
⊢ (pderiv i) ((sumRingEquiv R σ ι) (p * X (Sum.inr val✝))) =
    (sumRingEquiv R σ ι) ((pderiv (Sum.inl i)) (p * X (Sum.inr val✝)))

Tactic:
<;>

Goal state after:
case mul_X.inl
R : Type u
inst✝ : CommSemiring R
σ : Type u_1
ι : Type u_2
i : σ
p : MvPolynomial (σ ⊕ ι) R
a✝ : (pderiv i) ((sumRingEquiv R σ ι) p) = (sumRingEquiv R σ ι) ((pderiv (Sum.inl i)) p)
val✝ : σ
⊢ (pderiv i) ((sumRingEquiv R σ ι) (p * X (Sum.inl val✝))) =
    (sumRingEquiv R σ ι) ((pderiv (Sum.inl i)) (p * X (Sum.inl val✝)))

case mul_X.inr
R : Type u
inst✝ : CommSemiring R
σ : Type u_1
ι : Type u_2
i : σ
p : MvPolynomial (σ ⊕ ι) R
a✝ : (pderiv i) ((sumRingEquiv R σ ι) p) = (sumRingEquiv R σ ι) ((pderiv (Sum.inl i)) p)
val✝ : ι
⊢ (pderiv i) ((sumRingEquiv R σ ι) (p * X (Sum.inr val✝))) =
    (sumRingEquiv R σ ι) ((pderiv (Sum.inl i)) (p * X (Sum.inr val✝)))
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case refine_3.exac
R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : FinitePresentation R M
n m : ℕ
f : (Fin n → R) →ₗ[R] M
g : (Fin m → R) →ₗ[R] Fin n → R
hf : Function.Surjective ⇑f
hfg : Function.Exact ⇑g ⇑f
⊢ Function.Exact ⇑(baseChange S g) ⇑(baseChange S f)

Tactic:
exact lTensor_exact S hfg hf

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ mk.ker = P.ker • ⊤

Tactic:
by
  ext ⟨x, hx⟩
  simp [LinearMap.mem_ker, mk_eq_zero_iff, Submodule.mem_smul_top_iff, sq]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case inl
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
val✝ : ι'
⊢ (Q.aux P) (X (Sum.inl val✝)) = ((mapAlgHom (aeval P.val)).comp ↑(sumAlgEquiv R ι' ι)) (X (Sum.inl val✝))

pp: case inr
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
val✝ : ι
⊢ (Q.aux P) (X (Sum.inr val✝)) = ((mapAlgHom (aeval P.val)).comp ↑(sumAlgEquiv R ι' ι)) (X (Sum.inr val✝))

Tactic:
<;>

Goal state after:
case inl
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
val✝ : ι'
⊢ (Q.aux P) (X (Sum.inl val✝)) = ((mapAlgHom (aeval P.val)).comp ↑(sumAlgEquiv R ι' ι)) (X (Sum.inl val✝))

case inr
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
val✝ : ι
⊢ (Q.aux P) (X (Sum.inr val✝)) = ((mapAlgHom (aeval P.val)).comp ↑(sumAlgEquiv R ι' ι)) (X (Sum.inr val✝))
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case inl
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
val✝ : ι'
⊢ (aeval (Q.comp P.toGenerators).val) (X (Sum.inl val✝)) =
    (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) ((Q.aux P) (X (Sum.inl val✝)))

pp: case inr
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
val✝ : ι
⊢ (aeval (Q.comp P.toGenerators).val) (X (Sum.inr val✝)) =
    (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) ((Q.aux P) (X (Sum.inr val✝)))

Tactic:
<;>

Goal state after:
case inl
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
val✝ : ι'
⊢ (aeval (Q.comp P.toGenerators).val) (X (Sum.inl val✝)) =
    (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) ((Q.aux P) (X (Sum.inl val✝)))

case inr
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
val✝ : ι
⊢ (aeval (Q.comp P.toGenerators).val) (X (Sum.inr val✝)) =
    (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) ((Q.aux P) (X (Sum.inr val✝)))