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_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
H : Function.Surjective ⇑(linearCombination R Subtype.val)
f : N → M
hf : ∀ (b : N), l (f b) = b
⊢ (l ∘ₗ linearCombination R fun i ↦ f ↑i) = linearCombination R Subtype.val

Tactic:
ext

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
H : Function.Surjective ⇑(linearCombination R Subtype.val)
f : N → M
hf : ∀ (b : N), l (f b) = b
a✝ : ↥s
⊢ ((l ∘ₗ linearCombination R fun i ↦ f ↑i) ∘ₗ lsingle a✝) 1 = (linearCombination R Subtype.val ∘ₗ lsingle a✝) 1
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
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
⊢ π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f

Tactic:
ext

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
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
x✝ : ↥(l ∘ₗ π).ker
⊢ (π ∘ₗ (l ∘ₗ π).ker.subtype) x✝ = (l.ker.subtype ∘ₗ f) x✝
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
⊢ ⇑f '' (fun t ↦ integerMultiple S f s id t) '' ↑s.attach = commonDenomOfFinset S f s • ↑s

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ ⇑f '' (fun t ↦ integerMultiple S f s id t) '' ↑s.attach ↔ x✝ ∈ commonDenomOfFinset S f s • ↑s
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ ⇑f '' (fun t ↦ integerMultiple S f s id t) '' ↑s.attach ↔ x✝ ∈ commonDenomOfFinset S f s • ↑s

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ ⇑f '' (fun t ↦ integerMultiple S f s id t) '' ↑s.attach → x✝ ∈ commonDenomOfFinset S f s • ↑s

case mpr
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ commonDenomOfFinset S f s • ↑s → x✝ ∈ ⇑f '' (fun t ↦ integerMultiple S f s id t) '' ↑s.attach
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
ι : Sort ?u.18
inst✝² : Finite ι
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
⊢ FinitePresentation R (M × N)

Tactic:
have hf : Function.Surjective (LinearMap.fst R M N) := LinearMap.fst_surjective
  have : FinitePresentation R ↥(LinearMap.ker (LinearMap.fst R M N)) := by
    rw [LinearMap.ker_fst]
    exact .of_equiv (LinearEquiv.ofInjective (LinearMap.inr R M N) LinearMap.inr_injective)
  apply Module.finitePresentation_of_ker (.fst R M N) hf

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

Goal state before:
pp: A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : IsTorsionFree A B
⊢ ↑(primesOverFinset p B) = p.primesOver B

Tactic:
ext

Goal state after:
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : IsTorsionFree A B
x✝ : Ideal B
⊢ x✝ ∈ ↑(primesOverFinset p B) ↔ x✝ ∈ p.primesOver B
Module: Mathlib.Algebra.Module.Presentation.Cokernel

Goal state before:
pp: A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
i : ι
⊢ (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ }) (f (g₁ i)) = 0

Tactic:
← data.π_lift,

Goal state after:
A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
i : ι
⊢ (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ }) (pres₂.π (data.lift i)) = 0
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ (∃ x, (rename Subtype.val) x = p) ↔ ↑p.vars ⊆ s

Tactic:
constructor

Goal state after:
case mp
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ (∃ x, (rename Subtype.val) x = p) → ↑p.vars ⊆ s

case mpr
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ ↑p.vars ⊆ s → ∃ x, (rename Subtype.val) x = p
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t ↔ s ⊆ t

Tactic:
constructor

Goal state after:
case mp
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t → s ⊆ t

case mpr
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
⊢ s ⊆ t → supported R s ≤ supported R t
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
f : (R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) ≃ₗ[R] ↥(R ∙ y) :=
  (R ∙ p ^ (pOrder hM y - k) * p ^ k).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
⊢ p ^ (pOrder hM y - k) • ⟨p ^ k • x, h⟩ = 0

Tactic:
ext

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
f : (R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) ≃ₗ[R] ↥(R ∙ y) := ⋯
⊢ ↑(p ^ (pOrder hM y - k) • ⟨p ^ k • x, h⟩) = ↑0
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ R ∙ z
a : R
ha : p ^ k • f1.choose = p ^ k • a • z
⊢ Submodule.Quotient.mk f1.choose - a • Submodule.Quotient.mk z = f 1

Tactic:
(Quotient.mk_eq_zero _).mpr <| Submodule.mem_span_singleton_self _,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ R ∙ z
a : R
ha : p ^ k • f1.choose = p ^ k • a • z
⊢ Submodule.Quotient.mk f1.choose - a • 0 = f 1
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
inst✝ : IsScalarTower R R[X] A
a b : A
⊢ (LinearMap.toSpanSingleton R[X] A (a + b)).compDer derivative' =
    (LinearMap.toSpanSingleton R[X] A a).compDer derivative' + (LinearMap.toSpanSingleton R[X] A b).compDer derivative'

Tactic:
ext

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
inst✝ : IsScalarTower R R[X] A
a b : A
⊢ ((LinearMap.toSpanSingleton R[X] A (a + b)).compDer derivative') X =
    ((LinearMap.toSpanSingleton R[X] A a).compDer derivative' +
        (LinearMap.toSpanSingleton R[X] A b).compDer derivative')
      X
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
inst✝ : IsScalarTower R R[X] A
t : R
a : A
⊢ (LinearMap.toSpanSingleton R[X] A (t • a)).compDer derivative' =
    (RingHom.id R) t • (LinearMap.toSpanSingleton R[X] A a).compDer derivative'

Tactic:
ext

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
inst✝ : IsScalarTower R R[X] A
t : R
a : A
⊢ ((LinearMap.toSpanSingleton R[X] A (t • a)).compDer derivative') X =
    ((RingHom.id R) t • (LinearMap.toSpanSingleton R[X] A a).compDer derivative') X
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
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✝
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
⊢ IsLocalizedModule S (IsLocalizedModule.map S f g)

Tactic:
constructor

Goal state after:
case map_units
R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
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✝
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
⊢ ∀ (x : ↥S), IsUnit ((algebraMap R (End R (M' →ₗ[R] N'))) ↑x)

case surj
R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
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✝
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
⊢ ∀ (y : M' →ₗ[R] N'), ∃ x, x.2 • y = (IsLocalizedModule.map S f g) x.1

case exists_of_eq
R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
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✝
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
⊢ ∀ {x₁ x₂ : M →ₗ[R] N}, (IsLocalizedModule.map S f g) x₁ = (IsLocalizedModule.map S f g) x₂ → ∃ c, c • x₁ = c • x₂
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case map_units
R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
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✝
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
s : ↥S
this : Function.Bijective ⇑((algebraMap R (End R N')) ↑s)
⊢ Function.Bijective ⇑((algebraMap R (End R (M' →ₗ[R] N'))) ↑s)

Tactic:
constructor

Goal state after:
case map_units.left
R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
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✝
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
s : ↥S
this : Function.Bijective ⇑((algebraMap R (End R N')) ↑s)
⊢ Function.Injective ⇑((algebraMap R (End R (M' →ₗ[R] N'))) ↑s)

case map_units.right
R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
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✝
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
s : ↥S
this : Function.Bijective ⇑((algebraMap R (End R N')) ↑s)
⊢ Function.Surjective ⇑((algebraMap R (End R (M' →ₗ[R] N'))) ↑s)
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
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✝
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
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
⊢ g ∘ₗ h' = (IsLocalizedModule.map S f g) (h', s).1 ∘ₗ f

Tactic:
ext

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
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✝
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
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
x✝ : M
⊢ (g ∘ₗ h') x✝ = ((IsLocalizedModule.map S f g) (h', s).1 ∘ₗ f) x✝
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
inst✝ : FinitePresentation R S
H : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG := FinitePresentation.out
n : ℕ := H.choose
f : MvPolynomial (Fin n) R →ₐ[R] S := ⋯.choose
hf : Function.Surjective ⇑f
hf' : (RingHom.ker f).FG
H' : ∃ n_1 s, Submodule.span (MvPolynomial (Fin n) R) (Set.range s) = RingHom.ker f :=
  Submodule.fg_iff_exists_fin_generating_family.mp hf'
m : ℕ := H'.choose
v : Fin m → MvPolynomial (Fin n) R := ⋯.choose
hv : Ideal.span (Set.range v) = RingHom.ker f
⊢ (aeval fun x ↦ f (X x)) = f

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
H : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG := FinitePresentation.out
n : ℕ := H.choose
f : MvPolynomial (Fin n) R →ₐ[R] S := ⋯.choose
hf : Function.Surjective ⇑f
hf' : (RingHom.ker f).FG
H' : ∃ n_1 s, Submodule.span (MvPolynomial (Fin n) R) (Set.range s) = RingHom.ker f :=
  Submodule.fg_iff_exists_fin_generating_family.mp hf'
m : ℕ := H'.choose
v : Fin m → MvPolynomial (Fin n) R := ⋯.choose
hv : Ideal.span (Set.range v) = RingHom.ker f
i✝ : Fin n
⊢ (aeval fun x ↦ f (X x)) (X i✝) = f (X i✝)
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
inst✝ : FinitePresentation R S
H : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG := FinitePresentation.out
n : ℕ := H.choose
f : MvPolynomial (Fin n) R →ₐ[R] S := ⋯.choose
hf : Function.Surjective ⇑f
hf' : (RingHom.ker f).FG
H' : ∃ n_1 s, Submodule.span (MvPolynomial (Fin n) R) (Set.range s) = RingHom.ker f :=
  Submodule.fg_iff_exists_fin_generating_family.mp hf'
m : ℕ := H'.choose
v : Fin m → MvPolynomial (Fin n) R := ⋯.choose
hv : Ideal.span (Set.range v) = RingHom.ker f
⊢ f = aeval fun x ↦ f (X x)

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
H : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG := FinitePresentation.out
n : ℕ := H.choose
f : MvPolynomial (Fin n) R →ₐ[R] S := ⋯.choose
hf : Function.Surjective ⇑f
hf' : (RingHom.ker f).FG
H' : ∃ n_1 s, Submodule.span (MvPolynomial (Fin n) R) (Set.range s) = RingHom.ker f :=
  Submodule.fg_iff_exists_fin_generating_family.mp hf'
m : ℕ := H'.choose
v : Fin m → MvPolynomial (Fin n) R := ⋯.choose
hv : Ideal.span (Set.range v) = RingHom.ker f
i✝ : Fin n
⊢ f (X i✝) = (aeval fun x ↦ f (X x)) (X i✝)
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
⊢ Function.Injective P.σ

Tactic:
intro x y e
  rw [← P.algebraMap_σ x, ← P.algebraMap_σ y, e]

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
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
α : ↥LieSubalgebra.root
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
⊢ α ∈ J.rootSet ↔ (rootSystem H).root α ∈ q

Tactic:
constructor

Goal state after:
case mp
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)
α : ↥LieSubalgebra.root
J : LieIdeal K L := ⋯
⊢ α ∈ J.rootSet → (rootSystem H).root α ∈ q

case mpr
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)
α : ↥LieSubalgebra.root
J : LieIdeal K L := ⋯
⊢ (rootSystem H).root α ∈ q → α ∈ J.rootSet
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
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
⊢ f.comp (Hom.id P) = f

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Extension R S
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
x✝ : P.Ring
⊢ (f.comp (Hom.id P)).toRingHom x✝ = f.toRingHom x✝
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
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
⊢ (Hom.id P').comp f = f

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Extension R S
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
x✝ : P.Ring
⊢ ((Hom.id P').comp f).toRingHom x✝ = f.toRingHom x✝