mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
⊢ (π ∘ₗ (l ∘ₗ π).ker.subtype).range = l.ker

Tactic:
LinearMap.range_comp,

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 ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
⊢ Submodule.map π (l ∘ₗ π).ker.subtype.range = l.ker
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝ : CommSemiring R
⊢ supported R Set.univ = ⊤

Tactic:
by
  simp [Algebra.eq_top_iff, mem_supported]

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)
χ : 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
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
h e f : L
ht : IsSl2Triple h e f
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
⊢ x_χ ∈ sl2SubalgebraOfRoot hα₀

Tactic:
mem_sl2SubalgebraOfRoot_iff hα₀ ht he hf

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
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
h e f : L
ht : IsSl2Triple h e f
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
⊢ ∃ c₁ c₂ c₃, x_χ = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: 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
x : M
⊢ Submodule.Quotient.mk (⋯.choose • x) = 0

Tactic:
(@hM x).choose_spec,

Goal state after:
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
x : M
⊢ Submodule.Quotient.mk 0 = 0
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
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : ¬Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α = 0
h e f : L
ht : IsSl2Triple h e f
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
⊢ x_χ ∈ sl2SubalgebraOfRoot hα₀

Tactic:
mem_sl2SubalgebraOfRoot_iff hα₀ ht he hf

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
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : ¬Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α = 0
h e f : L
ht : IsSl2Triple h e f
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
⊢ ∃ c₁ c₂ c₃, x_χ = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R M'
⊢ ∃ r ∈ S, IsLocalizedModule.Away r f

Tactic:
have : IsLocalizedModule S (.id (R := R) (M := M')) :=
    ⟨IsLocalizedModule.map_units f, fun y ↦ ⟨⟨y, 1⟩, by simp⟩, by simpa using ⟨1, S.one_mem⟩⟩

Goal state after:
R : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R M'
this : IsLocalizedModule S LinearMap.id
⊢ ∃ r ∈ S, IsLocalizedModule.Away r f
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case refine_4
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.Injective ⇑(lcomp S (S ⊗[R] N) (baseChange S f))

Tactic:
apply lcomp_injective_of_surjective
    exact LinearMap.lTensor_surjective S hf

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

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P✝ P : Presentation R S ι σ
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
⊢ Ideal.span (Set.range fun i ↦ P.relation i) = (P.ofAlgEquiv e).ker

Tactic:
simp [P.span_range_relation_eq_ker]

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
a✝ : Nontrivial L
hL : ¬IsLieAbelian L
⊢ (rootSystem H).IsIrreducible ↔ IsSimple K L

Tactic:
RootPairing.isIrreducible_iff_invtRootSubmodule,

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
a✝ : Nontrivial L
hL : ¬IsLieAbelian L
⊢ IsSimpleOrder ↥(rootSystem H).invtRootSubmodule ↔ IsSimple K L
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 ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Extension.Cotangent.mk.range = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = ⊤
r : σ
⊢ φ (Finsupp.single r 1) = Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk, hom₁_single, φ]

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Extension.Cotangent.mk.range = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = ⊤
r : σ
⊢ Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩ = Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩
Module: Mathlib.Algebra.Module.Presentation.Finite

Goal state before:
pp: case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝¹ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
R : Type w₁
w✝ : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = (Finsupp.linearCombination A var).ker
⊢ ∃ pres, Finite pres.G ∧ Finite pres.R

Tactic:
exact
     ⟨{ G := G
        R := R
        relation := relation
        var := var
        linearCombination_var_relation := fun r ↦ by
          rw [Submodule.ext_iff] at hR
          exact (hR _).1 (Submodule.subset_span ⟨_, rfl⟩)
        toIsPresentation := by
          rw [Relations.Solution.isPresentation_iff]
          exact ⟨hG, hR.symm⟩ },
        inferInstance, inferInstance⟩

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
ι : Type w
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
P✝ : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra R' R''
inst✝⁷ : Algebra R' S''
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra S S''
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
⊢ ((↑x).coeff.sum fun n r ↦ (rename Sum.inr) (P.σ r) * (monomial (Finsupp.mapDomain Sum.inl n)) 1) ∈ (Q.comp P).ker

Tactic:
simp only [ker_eq_ker_aeval_val, RingHom.mem_ker]

Goal state after:
case refine_2
R : Type u
S : Type v
ι : Type w
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
P✝ : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra R' R''
inst✝⁷ : Algebra R' S''
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra S S''
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
⊢ (aeval (Q.comp P).val)
      ((↑x).coeff.sum fun n r ↦ (rename Sum.inr) (P.σ r) * (monomial (Finsupp.mapDomain Sum.inl n)) 1) =
    0
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (IsScalarTower.toAlgHom R P.Ring S).comp (aeval P.σ) =
    (IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R (Generators.self R S).toExtension.Ring S)

Tactic:
by dsimp; ext; simp

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (support R M).Nonempty ↔ Nontrivial M

Tactic:
rw [Set.nonempty_iff_ne_empty, ne_eq,
    Module.support_eq_empty_iff, ← not_subsingleton_iff_nontrivial]

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), (f i) (x i) = 1
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a : Fin n ↪o ι
i j : Fin n
hij : ¬i = j
⊢ (f (a j)) (x (a i)) = 1 i j

Tactic:
· rw [h₀ (by simpa using Ne.symm hij), Matrix.one_apply_ne hij]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
M N : Submodule R S
H : Function.Injective ⇑(M.mulMap N)
T : Type w
inst✝¹ : Semiring T
inst✝ : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective ⇑f
this :
  Function.Injective
    (⇑((Submodule.map (↑f) M).mulMap (Submodule.map (↑f) N)) ∘
      ⇑(TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N)))
⊢ Function.Injective ⇑((Submodule.map (↑f) M).mulMap (Submodule.map (↑f) N))

Tactic:
refine this.of_comp_right ?_

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
M N : Submodule R S
H : Function.Injective ⇑(M.mulMap N)
T : Type w
inst✝¹ : Semiring T
inst✝ : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective ⇑f
this :
  Function.Injective
    (⇑((Submodule.map (↑f) M).mulMap (Submodule.map (↑f) N)) ∘
      ⇑(TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N)))
⊢ Function.Surjective ⇑(TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N))
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul (algebraMap₀ r) (algebraMap₀ s)) = algebraMap₀ (r * s)

Tactic:
rw [← smul_eq_mul, map_smul]
  exact algebraMap₀_mul r (@algebraMap₀ R M _ _ _ s)

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
this : Nontrivial R
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))

Tactic:
have := (IsLocalizedModule.isBaseChange S Rₛ f).equiv.lift_rank_eq.symm

Goal state after:
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
this✝ : Nontrivial R
this :
  Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) =
    Cardinal.lift.{uM', max uM uR'} (Module.rank Rₛ (TensorProduct R Rₛ M))
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
hx : x ∈ ((preimageEquivFiber R S p) q₁).asIdeal
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
⊢ x ∈ ((preimageEquivFiber R S p) q₂).asIdeal

Tactic:
rw [← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r), ← Algebra.smul_def, e] at hx ⊢

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
hx : 1 ⊗ₜ[R] s ∈ ((preimageEquivFiber R S p) q₁).asIdeal
e : r • x = 1 ⊗ₜ[R] s
⊢ 1 ⊗ₜ[R] s ∈ ((preimageEquivFiber R S p) q₂).asIdeal

case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
r : R
hx : (algebraMap R (p.asIdeal.Fiber S)) r * x ∈ ((preimageEquivFiber R S p) q₁).asIdeal
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉ ((preimageEquivFiber R S p) q₂).asIdeal

case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
hx : x ∈ ((preimageEquivFiber R S p) q₁).asIdeal
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉ ((preimageEquivFiber R S p) q₁).asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Flat R M
inst✝ : Module.Finite R M
p : PrimeSpectrum R
h : rankAtStalk M p = 0
⊢ Subsingleton (LocalizedModule p.asIdeal.primeCompl M)

Tactic:
apply subsingleton_of_rank_zero (R := Localization.AtPrime p.asIdeal)

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Flat R M
inst✝ : Module.Finite R M
p : PrimeSpectrum R
h : rankAtStalk M p = 0
⊢ Module.rank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) = 0
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
⊢ Module.Finite R M ∧ Projective R M

Tactic:
by
  let N := Dual R M
  let e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm .. ≪≫ₗ linearEquiv R M
  have ⟨S, hS⟩ := TensorProduct.exists_finset (e.symm 1)
  let f : (S →₀ N) →ₗ[R] R := Finsupp.lsum R fun i ↦ e.toLinearMap ∘ₗ TensorProduct.mk R M N i.1.1
  have : Function.Surjective f := by
    rw [← LinearMap.range_eq_top, Ideal.eq_top_iff_one]
    use Finsupp.equivFunOnFinite.symm fun i ↦ i.1.2
    simp_rw [f, Finsupp.coe_lsum]
    rw [Finsupp.sum_fintype _ _ fun _ ↦ map_zero _]
    rwa [e.symm_apply_eq, map_sum, ← Finset.sum_coe_sort, eq_comm] at hS
  have ⟨g, hg⟩ := projective_lifting_property f .id this
  classical
  let aux := finsuppRight R _ M N S ≪≫ₗ Finsupp.mapRange.linearEquiv e
  let f' : (S →₀ R) →ₗ[R] M := TensorProduct.rid R M ∘ₗ f.lTensor M ∘ₗ aux.symm
  let g' : M →ₗ[R] S →₀ R := aux ∘ₗ g.lTensor M ∘ₗ (TensorProduct.rid R M).symm
  have : Function.Surjective f' := by simpa [f'] using LinearMap.lTensor_surjective _ this
  refine ⟨.of_surjective f' this, .of_split g' f' <| LinearMap.ext fun m ↦ ?_⟩
  simp [f', g', show f (g 1) = 1 from DFunLike.congr_fun hg 1]

Goal state after:
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ Normal F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K

Tactic:
rw [normal_iff_normalClosure_le, normalClosure_def, iSup_le_iff]

Goal state after:
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
σ : L →ₐ[F] L
this : ∀ (σ : Gal(L/F)), normalClosure F (↥(map (↑σ) K)) L = normalClosure F (↥K) L
⊢ normalClosure F (↥(map σ K)) L = normalClosure F (↥K) L

Tactic:
exact this ((Algebra.IsAlgebraic.algEquivEquivAlgHom _ _).symm σ)

Goal state after: