mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
⊢ (if f x = x then if f y = y then s else ↑(f.toList y) else ↑(f.toList x)) ≍
    if f y = y then if f x = x then s else ↑(f.toList x) else ↑(f.toList y)

Tactic:
refine heq_of_eq ?_

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
⊢ (if f x = x then if f y = y then s else ↑(f.toList y) else ↑(f.toList x)) =
    if f y = y then if f x = x then s else ↑(f.toList x) else ↑(f.toList y)
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
⊢ ((LinearMap.compr₂ (residuePairing R A L Φ) ↑(TrivialLieModule.equiv R (loopAlgebra R A L) R).symm) f) f = 0

Tactic:
let F := toFinsupp R A L

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
⊢ ((LinearMap.compr₂ (residuePairing R A L Φ) ↑(TrivialLieModule.equiv R (loopAlgebra R A L) R).symm) f) f = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
l : α
hl : f.toCycle hf = ↑(f.toList l)
h : x ∈ f.toList l
⊢ ¬f x = x

Tactic:
have ⟨h1, h2⟩ := mem_toList_iff.mp h

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
l : α
hl : f.toCycle hf = ↑(f.toList l)
h : x ∈ f.toList l
h1 : f.SameCycle l x
h2 : l ∈ f.support
⊢ ¬f x = x
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
x : A
hx : x ∈ Finset.map (Equiv.toEmbedding (Equiv.neg A)) s
⊢ x ∈ (F f).support ∨ x ∈ Finset.image (⇑(Equiv.neg A)) (F f).support

Tactic:
replace hx : -x ∈ (F f).support ∨ -x ∈ (F f).support.image Neg.neg := by simpa [hs] using hx

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
x : A
hx : -x ∈ (F f).support ∨ -x ∈ Finset.image Neg.neg (F f).support
⊢ x ∈ (F f).support ∨ x ∈ Finset.image (⇑(Equiv.neg A)) (F f).support
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case h.refine_1
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
⊢ v ∈ weightSpace V ⇑(χ₀ ∘ₗ π₁ + c • ↑e ∘ₗ π₂)

Tactic:
rw [mem_weightSpace]

Goal state after:
case h.refine_1
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
⊢ ∀ (x : L), ⁅x, v⁆ = (χ₀ ∘ₗ π₁ + c • ↑e ∘ₗ π₂) x • v
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
f : L₁ →ₗ⁅σ₁₂⁆ L₂
g : L₂ →ₗ⁅σ₂₃⁆ L₃
x✝¹ : A₁
x✝ : L₁
⊢ (g.comp f.toLieHom) (x✝¹ • x✝) = (σ₂₃.comp σ₁₂) x✝¹ • (g.comp f.toLieHom) x✝

Tactic:
simp [Hom.map_smul_apply]

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
⊢ Function.Injective toSubmodule

Tactic:
intro L₁'

Goal state after:
A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L₁' : LieRinehartSubalgebra A L
⊢ ∀ ⦃a₂ : LieRinehartSubalgebra A L⦄, L₁'.toSubmodule = a₂.toSubmodule → L₁' = a₂
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
⊢ rootSpace H γ ≤ LieSubmodule.restr I H

Tactic:
intro y hy

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
y : L
hy : y ∈ rootSpace H γ
⊢ y ∈ LieSubmodule.restr I H
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
h : ↥H
hI : ↑h ∈ I
β : ↥LieSubalgebra.root
hβ : ↑β h ≠ 0
⊢ rootSpace H ⇑↑β ≤ LieSubmodule.restr I H

Tactic:
intro y hy

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
h : ↥H
hI : ↑h ∈ I
β : ↥LieSubalgebra.root
hβ : ↑β h ≠ 0
y : L
hy : y ∈ rootSpace H ⇑↑β
⊢ y ∈ LieSubmodule.restr I H
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝⁶ : CommMonoidWithZero M
inst✝⁵ : IsCancelMulZero M
N : Type u_2
inst✝⁴ : CommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
⊢ associatesEquivOfUniqueUnits.symm p ∈ Set.Iic (Associates.mk m)

Tactic:
simp only [associatesEquivOfUniqueUnits_symm_apply]

Goal state after:
M : Type u_1
inst✝⁶ : CommMonoidWithZero M
inst✝⁵ : IsCancelMulZero M
N : Type u_2
inst✝⁴ : CommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
⊢ Associates.mk p ∈ Set.Iic (Associates.mk m)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
⊢ ∀ y ∈ ↑I, 1 * y ∈ 1

Tactic:
intro y hy

Goal state after:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
y : K
hy : y ∈ ↑I
⊢ 1 * y ∈ 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥R⁰
x : R
hx : (algebraMap R K) x = ↑z • y
⊢ x ≠ 0

Tactic:
rw [Ne, ← @IsFractionRing.to_map_eq_zero_iff R _ K, hx, Algebra.smul_def]

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥R⁰
x : R
hx : (algebraMap R K) x = ↑z • y
⊢ ¬(algebraMap R K) ↑z * y = 0
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case refine_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I✝ : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
y₀ : K
hy₀ : y₀ ∈ ↑I
⊢ (algebraMap A K) b * ((algebraMap A K) a)⁻¹ * y₀ ∈ 1

Tactic:
obtain ⟨y, h_Iy, rfl⟩ := (mem_coeIdeal _).mp hy₀

Goal state after:
case refine_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I✝ : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
y : A
h_Iy : y ∈ I
hy₀ : (algebraMap A K) y ∈ ↑I
⊢ (algebraMap A K) b * ((algebraMap A K) a)⁻¹ * (algebraMap A K) y ∈ 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝⁷ : CommRing R₁
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Algebra R₁ K
inst✝⁴ : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ map (↑h) (1 / I) = 1 / map (↑h) I

Tactic:
rw [FractionalIdeal.map_div, FractionalIdeal.map_one]

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

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
⊢ IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1

Tactic:
refine h.toEquiv.forall_congr (fun {x} => ?_)

Goal state after:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
x : FractionalIdeal A⁰ (FractionRing A)
⊢ x ≠ ⊥ → x * x⁻¹ = 1 ↔ h.toEquiv x ≠ ⊥ → h.toEquiv x * (h.toEquiv x)⁻¹ = 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
n : ℕ
⊢ spanSingleton S x ^ n = spanSingleton S (x ^ n)

Tactic:
induction n with
  | zero => rw [pow_zero, pow_zero, spanSingleton_one]
  | succ n hn => rw [pow_succ, hn, spanSingleton_mul_spanSingleton, pow_succ]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R✝ : Type u_1
inst✝¹³ : CommRing R✝
S : Submonoid R✝
P : Type u_2
inst✝¹² : CommRing P
inst✝¹¹ : Algebra R✝ P
R₁ : Type u_3
inst✝¹⁰ : CommRing R₁
K : Type u_4
inst✝⁹ : Field K
inst✝⁸ : Algebra R₁ K
inst✝⁷ : IsFractionRing R₁ K
inst✝⁶ : IsLocalization S P
inst✝⁵ : IsDomain R₁
R : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : R
aI : Ideal R
ha : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑aI
| spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑aI

Tactic:
← span_singleton_generator aI

Goal state after:
R✝ : Type u_1
inst✝¹³ : CommRing R✝
S : Submonoid R✝
P : Type u_2
inst✝¹² : CommRing P
inst✝¹¹ : Algebra R✝ P
R₁ : Type u_3
inst✝¹⁰ : CommRing R₁
K : Type u_4
inst✝⁹ : Field K
inst✝⁸ : Algebra R₁ K
inst✝⁷ : IsFractionRing R₁ K
inst✝⁶ : IsLocalization S P
inst✝⁵ : IsDomain R₁
R : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : R
aI : Ideal R
ha : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑aI
| spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑(R ∙ generator aI)
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
⊢ ∃ n m f g, Function.Surjective ⇑f ∧ Function.Exact ⇑g ⇑f

Tactic:
obtain ⟨n, K, e, h⟩ := exists_fin R M
  obtain ⟨m, g', hg'⟩ := K.fg_iff_exists_fin_linearMap.mp h
  exact ⟨n, m, e.symm ∘ₗ K.mkQ, g', by simpa using K.mkQ_surjective,
    e.symm.injective.comp_exact_iff_exact.mpr (by simp [LinearMap.exact_iff, hg'])⟩

Goal state after:
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
⊢ FinitePresentation R N

Tactic:
have hσ₁ : π ∘ σ = id := by ext i; exact congr_arg Subtype.val (hσ i)

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
⊢ FinitePresentation R N
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hI : I ≠ 0
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
⊢ (Associates.mk J).count (Associates.mk I).factors = Multiset.count J (normalizedFactors I)

Tactic:
by
  replace hI : Associates.mk I ≠ 0 := Associates.mk_ne_zero.mpr hI
  have hJ' : Irreducible (Associates.mk J) := by
    simpa only [Associates.irreducible_mk] using (prime_of_isPrime hJ₀ hJ).irreducible
  apply (count_normalizedFactors_eq (p := J) (x := I) _ _).symm
  all_goals
    rw [← dvd_iff_le, ← Associates.mk_dvd_mk, Associates.mk_pow]
    simp only [Associates.dvd_eq_le]
    rw [Associates.prime_pow_dvd_iff_le hI hJ']
  lia

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring 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'
a : R
x : M'
x' : M
hx : f x' = x
⊢ f (a • x') = a • x

Tactic:
← hx,

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring 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'
a : R
x : M'
x' : M
hx : f x' = x
⊢ f (a • x') = a • f x'
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: 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

Tactic:
rw [h.emultiplicity_eq_multiplicity]
    apply emultiplicity_eq_of_dvd_of_not_dvd <;>
      rw [span_singleton_pow, span_singleton_dvd_span_singleton_iff_dvd]
    · exact pow_multiplicity_dvd a b
    · apply h.not_pow_dvd_of_multiplicity_lt
      apply lt_add_one

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

Goal state before:
pp: R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ (pderiv i) ((monomial s) a) = (monomial (s - single i 1)) (a * ↑(s i))

Tactic:
by
  classical
  simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc,
    ← (monomial _).map_smul]
  refine (Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_
  · simp [Pi.single_eq_of_ne hne]
  · rw [Finsupp.notMem_support_iff] at hi; simp [hi]
  · simp

Goal state after:
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:
rw [pderiv_monomial, X, monomial_mul, smul_monomial]

Goal state after:
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
⊢ (monomial (single i 1 + (m - single i 1))) (1 * (r * ↑(m i))) = (monomial m) (m i • r)
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case hs
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
ι : Type u_1
s : ι → P.Ring
hs✝ : Ideal.span (Set.range s) = P.ker
hs : Submodule.span P.Ring (Set.range s) = P.ker
⊢ ∀ (i : ι), s i ∈ P.ker

Tactic:
· simp [← hs, Ideal.mem_span_range_self]

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

Goal state before:
pp: B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
⊢ v ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) ↔ v ∈ ⊤

Tactic:
simp only [Submodule.mem_top, iff_true]

Goal state after:
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
⊢ v ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
h₄ : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
l : ℕ
f : Fin l →₀ R
x : (Fin l →₀ R) →ₗ[R] M
hfx : x f = 0
f' : Fin l → R := ⇑f
x' : Fin l → M := fun i ↦ x (Finsupp.single i 1)
⊢ x (∑ i, f i • Finsupp.single i 1) = x f

Tactic:
smul_single,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
h₄ : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
l : ℕ
f : Fin l →₀ R
x : (Fin l →₀ R) →ₗ[R] M
hfx : x f = 0
f' : Fin l → R := ⇑f
x' : Fin l → M := fun i ↦ x (Finsupp.single i 1)
⊢ x (∑ x, Finsupp.single x (f x • 1)) = x f
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case mp
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
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.comp P).Ring
hx : (aeval (Q.comp P).val) x = 0
⊢ (aeval Q.val) ((Q.ofComp P).toAlgHom x) = 0

Tactic:
← hx,

Goal state after:
case mp
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
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.comp P).Ring
hx : (aeval (Q.comp P).val) x = 0
⊢ (aeval Q.val) ((Q.ofComp P).toAlgHom x) = (aeval (Q.comp P).val) x