mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Field K
inst✝ : IsDedekindDomain A
I : Ideal R
J : Ideal A
f : R ⧸ I →+* A ⧸ J
hf : Function.Surjective ⇑f
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h : X ≤ Y
⊢ map (Ideal.Quotient.mk I) X ≤ comap f (map f (map (Ideal.Quotient.mk I) Y))

Tactic:
comap_map_of_surjective _ hf (map (Ideal.Quotient.mk I) Y)

Goal state after:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Field K
inst✝ : IsDedekindDomain A
I : Ideal R
J : Ideal A
f : R ⧸ I →+* A ⧸ J
hf : Function.Surjective ⇑f
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h : X ≤ Y
⊢ map (Ideal.Quotient.mk I) X ≤ map (Ideal.Quotient.mk I) Y ⊔ comap f ⊥
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → ↥⋯.toFinset := fun i ↦ ⟨l (b i), ⋯⟩
σ : ↥⋯.toFinset → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : ↥⋯.toFinset), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] ↥⋯.toFinset →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
x : ↥⋯.toFinset →₀ R
⊢ x ∈ (linearCombination R Subtype.val).ker ↔ x ∈ Submodule.map f l.ker

Tactic:
simp only [LinearMap.mem_ker, Submodule.mem_map]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → ↥⋯.toFinset := fun i ↦ ⟨l (b i), ⋯⟩
σ : ↥⋯.toFinset → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : ↥⋯.toFinset), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] ↥⋯.toFinset →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
x : ↥⋯.toFinset →₀ R
⊢ (linearCombination R Subtype.val) x = 0 ↔ ∃ y, l y = 0 ∧ f y = x
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
this : (idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩ ≤ (idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩ ↔ ⟨M, hM⟩ ≤ ⟨L, hL⟩
⊢ (idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩ ≤ (idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩ ↔ M ≤ L

Tactic:
this,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
this : (idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩ ≤ (idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩ ↔ ⟨M, hM⟩ ≤ ⟨L, hL⟩
⊢ ⟨M, hM⟩ ≤ ⟨L, hL⟩ ↔ M ≤ L
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
t : Finset M
ht : Submodule.span R ↑t = l.ker
⊢ Submodule.span R (Set.range Subtype.val) = ⊤

Tactic:
Subtype.range_val,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
t : Finset M
ht : Submodule.span R ↑t = l.ker
⊢ Submodule.span R ↑s = ⊤
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
⊢ Submodule.span R (Set.range Subtype.val) = ⊤

Tactic:
Subtype.range_val,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
⊢ Submodule.span R ↑s = ⊤
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := linearCombination R Subtype.val
⊢ Submodule.span R (Set.range Subtype.val) = ⊤

Tactic:
Subtype.range_val,

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := linearCombination R Subtype.val
⊢ Submodule.span R ↑s = ⊤
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
⊢ emultiplicity (span {a}) (span {b}) = emultiplicity a b

Tactic:
by_cases h : FiniteMultiplicity a b

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ emultiplicity (span {a}) (span {b}) = emultiplicity a b

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : ¬FiniteMultiplicity a b
⊢ emultiplicity (span {a}) (span {b}) = emultiplicity a b
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
⊢ Submodule.span R (Set.range Subtype.val) = ⊤

Tactic:
Subtype.range_val,

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
⊢ Submodule.span R ↑σ = ⊤
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
this : C a • D f = D (C a * f)
⊢ C a • D f = a • D f

Tactic:
this,

Goal state after:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
this : C a • D f = D (C a * f)
⊢ D (C a * f) = a • D f
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_pos + m_neg + m_h⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆

Tactic:
lie_add,

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⁆ + ⁅x_χ, m_h⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: case add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
i : σ
p q : MvPolynomial σ R
hp : D (p * X i) = p • D (X i) + X i • D p
hq : D (q * X i) = q • D (X i) + X i • D q
⊢ D ((p + q) * X i) = (p + q) • D (X i) + X i • D (p + q)

Tactic:
| add p q hp hq =>

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

Goal state before:
pp: case add
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
p q : MvPolynomial σ R
hp : coeff m ((pderiv i) p) = coeff (m + single i 1) p * (↑(m i) + 1)
hq : coeff m ((pderiv i) q) = coeff (m + single i 1) q * (↑(m i) + 1)
⊢ coeff m ((pderiv i) (p + q)) = coeff (m + single i 1) (p + q) * (↑(m i) + 1)

Tactic:
| add p q hp hq =>

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

Goal state before:
pp: case add
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p q : MvPolynomial σ R
hp : (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
hq : (pderiv (f x)) ((rename f) q) = (rename f) ((pderiv x) q)
⊢ (pderiv (f x)) ((rename f) (p + q)) = (rename f) ((pderiv x) (p + q))

Tactic:
| add p q hp hq =>

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

Goal state before:
pp: case add
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 q : MvPolynomial (σ ⊕ τ) R
hp : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)
hq : (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) q) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) q)
⊢ (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) (p + q)) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) (p + q))

Tactic:
| add p q hp hq =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
this : C a • D f = D (C a * f)
⊢ C a • D f = a • D f

Tactic:
this,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
this : C a • D f = D (C a * f)
⊢ D (C a * f) = a • D f
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✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
⊢ ∃ r,
    ∃ (hr : r ∈ S),
      ∃ l',
        LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯

Tactic:
obtain ⟨l', s, H⟩ := Module.FinitePresentation.exists_lift_of_isLocalizedModule S g (l ∘ₗ f)
  have : Function.Bijective (IsLocalizedModule.map S f g l') := by
    have : IsLocalizedModule.map S f g l' = (s • LinearMap.id) ∘ₗ l := by
      apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
      apply LinearMap.ext fun x ↦ ?_
      simp only [LinearMap.coe_comp, Function.comp_apply, IsLocalizedModule.map_apply]
      rw [← LinearMap.comp_apply, H]
      simp
    rw [this]
    exact ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units g s)).comp l.bijective
  obtain ⟨r, hr, hr'⟩ := exists_bijective_map_powers S f g _ this
  let rs : Submonoid R := (.powers <| r * s)
  let Rᵣₛ := Localization rs
  have hsu : IsUnit (algebraMap R Rᵣₛ s) := isUnit_of_dvd_unit
      (hu := IsLocalization.map_units (M := rs) Rᵣₛ ⟨_, Submonoid.mem_powers _⟩)
      (map_dvd (algebraMap R Rᵣₛ) ⟨r, mul_comm _ _⟩)
  have : Function.Bijective ((hsu.unit⁻¹).1 • LocalizedModule.map rs l') :=
    ((Module.End.isUnit_iff _).mp ((hsu.unit⁻¹).isUnit.map (algebraMap _ (End Rᵣₛ
      (LocalizedModule rs N))))).comp (hr' (r * s) (dvd_mul_right _ _))
  refine ⟨r * s, mul_mem hr s.2, LinearEquiv.ofBijective _ this, ?_⟩
  apply IsLocalizedModule.ext rs (LocalizedModule.mkLinearMap rs M) fun x ↦ map_units g
    ⟨x.1, SetLike.le_def.mp (Submonoid.powers_le.mpr (mul_mem hr s.2)) x.2⟩
  ext x
  apply ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units g s)).1
  have : ∀ x, g (l' x) = s.1 • (l (f x)) := LinearMap.congr_fun H
  simp only [rs, LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe,
    Function.comp_apply, LocalizedModule.mkLinearMap_apply, LinearEquiv.ofBijective_apply,
    LinearMap.smul_apply, LocalizedModule.map_mk, algebraMap_end_apply]
  rw [← map_smul, ← smul_assoc, Algebra.smul_def s.1, hsu.mul_val_inv, one_smul]
  simp only [LocalizedModule.lift_mk, OneMemClass.coe_one, map_one, IsUnit.unit_one,
    inv_one, Units.val_one, Module.End.one_apply, this]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : R[X]
⊢ (D R R[X]) P = derivative P • (D R R[X]) X

Tactic:
← aeval_X_left_apply P,

Goal state after:
R : Type u
inst✝ : CommRing R
P : R[X]
⊢ (D R R[X]) ((aeval X) P) = derivative ((aeval X) P) • (D R R[X]) X
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: case h
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
g : R →+* MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1} := (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})).comp C
⊢ C r * X () - 1 ∈ Ideal.span {C r * X () - 1}

Tactic:
exact Ideal.mem_span_singleton_self (C r * X () - 1)

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway S r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ RingHom.ker (aeval (Generators.localizationAway S r).val) = Ideal.span {C r * X () - 1}

Tactic:
this,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this :
  aeval (Generators.localizationAway S r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))
⊢ RingHom.ker ((↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) =
    Ideal.span {C r * X () - 1}
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)
⊢ LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H = ⨆ α, sl2SubmoduleOfRoot ⋯

Tactic:
← LieSubmodule.toSubmodule_inj,

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)
⊢ ↑(LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H) = ↑(⨆ α, sl2SubmoduleOfRoot ⋯)
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case add
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
p q : MvPolynomial ι T
hp :
  (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm p) =
    (aeval (Generators.baseChange T P.toGenerators).val) p
hq :
  (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm q) =
    (aeval (Generators.baseChange T P.toGenerators).val) q
⊢ (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm (p + q)) =
    (aeval (Generators.baseChange T P.toGenerators).val) (p + q)

Tactic:
| add p q hp hq =>

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✝⁶ : 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
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq : ∀ (α : ↥LieSubalgebra.root), α ∈ J.rootSet ↔ α ∈ I.rootSet
h_restr : LieSubmodule.restr J H = LieSubmodule.restr I H
⊢ J = I

Tactic:
← LieSubmodule.toSubmodule_inj,

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
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq : ∀ (α : ↥LieSubalgebra.root), α ∈ J.rootSet ↔ α ∈ I.rootSet
h_restr : LieSubmodule.restr J H = LieSubmodule.restr I H
⊢ ↑J = ↑I
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case add
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 ι σ
p q : MvPolynomial ι' S
hp : ∃ a, (Q.aux P) a = p
hq : ∃ a, (Q.aux P) a = q
⊢ ∃ a, (Q.aux P) a = p + q

Tactic:
| add p q hp hq =>

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

Goal state before:
pp: case add
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T✝ : Type ?u.18
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := P.σ b
p q : MvPolynomial ι R
hp : (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) p = 1 ⊗ₜ[R] (aeval fun x ↦ P.val x) p
hq : (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) q = 1 ⊗ₜ[R] (aeval fun x ↦ P.val x) q
⊢ (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) (p + q) = 1 ⊗ₜ[R] (aeval fun x ↦ P.val x) (p + q)

Tactic:
| add p q hp hq =>

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

Goal state before:
pp: case h
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T✝ : Type ?u.18
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := P.σ b
this : ∀ (y : P.Ring), (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) y = 1 ⊗ₜ[R] (aeval fun x ↦ P.val x) y
⊢ a • (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) (P.σ b) = a ⊗ₜ[R] b

Tactic:
this,

Goal state after:
case h
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T✝ : Type ?u.18
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := P.σ b
this : ∀ (y : P.Ring), (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) y = 1 ⊗ₜ[R] (aeval fun x ↦ P.val x) y
⊢ a • 1 ⊗ₜ[R] (aeval fun x ↦ P.val x) (P.σ b) = a ⊗ₜ[R] b
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ pres.toExtension.cotangentComplex ∘ₗ hom₁ pres =
    ↑pres.cotangentSpaceBasis.repr.symm ∘ₗ pres.differentialsRelations.map

Tactic:
by
  ext r
  have := (differentialsRelations pres).map_single
  dsimp at this ⊢
  rw [comm₁₂_single, this]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.DirectSum

Goal state before:
pp: A : Type u
inst✝⁵ : Ring A
ι : Type w
inst✝⁴ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module A (M i)
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (directSum relations).Solution N
i : ι
r : (relations i).R
⊢ (Finsupp.linearCombination A fun g ↦ s.var ⟨i, g⟩) ((relations i).relation r) = 0

Tactic:
← s.linearCombination_var_relation ⟨i, r⟩

Goal state after:
A : Type u
inst✝⁵ : Ring A
ι : Type w
inst✝⁴ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module A (M i)
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (directSum relations).Solution N
i : ι
r : (relations i).R
⊢ (Finsupp.linearCombination A fun g ↦ s.var ⟨i, g⟩) ((relations i).relation r) =
    (Finsupp.linearCombination A s.var) ((directSum relations).relation ⟨i, r⟩)