mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ((F f).sum fun a v ↦ a • (Φ ((F f) (-a))) v) = 0

Tactic:
rw [Finsupp.sum_of_support_subset _ hs' _ (by simp)]

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 ∈ s, x • (Φ ((F f) (-x))) ((F f) x) = 0
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Φ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
⊢ twoCochainOfBilinear R A L Φ hΦs ∈
    Cohomology.twoCocycle R (loopAlgebra R A L) (TrivialLieModule R (loopAlgebra R A L) R)

Tactic:
apply (LieModule.Cohomology.mem_twoCocycle_iff ..).mpr

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Φ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
⊢ (Cohomology.d₂₃ R (loopAlgebra R A L) (TrivialLieModule R (loopAlgebra R A L) R)) (twoCochainOfBilinear R A L Φ hΦs) =
    0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
α : Fin (p + 1) → Fin n
i j : Fin n
⊢ pminor A α * A i j + ∑ s, -(bminor A i (α s) (s.removeNth α) * A (α s) j) =
    pminor A α * A i j - ∑ s, bminor A i (α s) (s.removeNth α) * A (α s) j

Tactic:
simp only [Finset.sum_neg_distrib, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: 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
hπ : ↑(π₁ x) + ↑(π₂ x) = x
this : ⁅((k ∙ z).projection ↑A ⋯) x, v⁆ = (c • e (π₂ x)) • v
⊢ ⁅π₁ x, v⁆ + ⁅((k ∙ z).projection ↑A ⋯) x, v⁆ = χ₀ (π₁ x) • v + (c • e (π₂ x)) • v

Tactic:
hv' (π₁ x),

Goal state after:
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
hπ : ↑(π₁ x) + ↑(π₂ x) = x
this : ⁅((k ∙ z).projection ↑A ⋯) x, v⁆ = (c • e (π₂ x)) • v
⊢ χ₀ (π₁ x) • v + ⁅((k ∙ z).projection ↑A ⋯) x, v⁆ = χ₀ (π₁ x) • v + (c • e (π₂ x)) • v
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i j : Fin n
h : i ≠ j
⊢ D n i j ≤ 0

Tactic:
by
  simp only [D, Matrix.of_apply]; split_ifs <;> omega

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ↥E.solSpace
⊢ (fun x ↦ ↑(u + v) ↑x) = (fun x ↦ ↑u ↑x) + fun x ↦ ↑v ↑x

Tactic:
ext
    simp

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
a : R
u : ↥E.solSpace
⊢ (fun x ↦ ↑(a • u) ↑x) = (RingHom.id R) a • fun x ↦ ↑u ↑x

Tactic:
ext
    simp

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✝⁶ : 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
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
β : ↥LieSubalgebra.root
hβ : β ∉ I.rootSet
h_ker : coroot ↑α ∈ Weight.ker
⊢ coroot ↑β ∈ Weight.ker

Tactic:
rw [← orthogonal_span_coroot_eq_ker,
    LinearMap.BilinForm.orthogonal_span_singleton_eq_toLin_ker, LinearMap.mem_ker]

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
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
β : ↥LieSubalgebra.root
hβ : β ∉ I.rootSet
h_ker : coroot ↑α ∈ Weight.ker
⊢ ((traceForm K (↥H) L).toLinHomAux₁ (coroot ↑α)) (coroot ↑β) = 0
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ (Finset.image (fun m ↦ c 1 ^ ↑m) Finset.univ).card = Finset.univ.card

Tactic:
cases n

Goal state after:
case zero
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hn : 0 ≠ 0
c : Fin (0 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ (Finset.image (fun m ↦ c 1 ^ ↑m) Finset.univ).card = Finset.univ.card

case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
n✝ : ℕ
hn : n✝ + 1 ≠ 0
c : Fin (n✝ + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ (Finset.image (fun m ↦ c 1 ^ ↑m) Finset.univ).card = Finset.univ.card
Module: Mathlib.RingTheory.FractionalIdeal.Basic

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
I : FractionalIdeal S P
x : P
hx : x ∈ 0
⊢ x ∈ I

Tactic:
convert! zero_mem I

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
x : P
hx : x ∈ 0
⊢ x = 0
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ∃ I, ↑I = J

Tactic:
refine ⟨⟨⟨⟨{ x : R | algebraMap R P x ∈ J }, ?_⟩, ?_⟩, ?_⟩, ?_⟩

Goal state after:
case mp.refine_1
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ∀ {a b : R},
    a ∈ {x | (algebraMap R P) x ∈ J} → b ∈ {x | (algebraMap R P) x ∈ J} → a + b ∈ {x | (algebraMap R P) x ∈ J}

case mp.refine_2
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ 0 ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ?mp.refine_1 }.carrier

case mp.refine_3
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ∀ (c : R) {x : R},
    x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ?mp.refine_1, zero_mem' := ?mp.refine_2 }.carrier →
      c • x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ?mp.refine_1, zero_mem' := ?mp.refine_2 }.carrier

case mp.refine_4
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ↑{ carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ?mp.refine_1, zero_mem' := ?mp.refine_2,
        smul_mem' := ?mp.refine_3 } =
    J
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'
this : Prime ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩)
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

Tactic:
simp only [associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq,
      associatesEquivOfUniqueUnits_symm_apply] at this

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'
this : Prime ↑(d ⟨p, ⋯⟩)
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case a
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
⊢ LieSubmodule.restr I H ≤ ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯

Tactic:
rw [lieIdeal_eq_inf_cartan_sup_biSup_rootSpace, restr_inf_cartan_eq_biSup_corootSubmodule]

Goal state after:
case a
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
⊢ (⨆ α ∈ I.rootSet, corootSubmodule ↑α) ⊔ ⨆ α, ⨆ (_ : rootSpace H ⇑↑α ≤ LieSubmodule.restr I H), rootSpace H ⇑↑α ≤
    ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯
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
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P'
x : P
⊢ x ∈ (canonicalEquiv S P P').symm I ↔ x ∈ (canonicalEquiv S P' P) I

Tactic:
mem_canonicalEquiv_apply,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P'
x : P
⊢ x ∈ (canonicalEquiv S P P').symm I ↔ ∃ y ∈ I, (IsLocalization.map P (RingHom.id R) ⋯) y = x
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
v : V₂ →ₗ[K] V₃
h : v.HasNoetherianRange
u : V →ₗ[K] V₂
⊢ (v ∘ₗ u).HasNoetherianRange

Tactic:
HasNoetherianRange,

Goal state after:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
v : V₂ →ₗ[K] V₃
h : IsNoetherian K ↥v.range
u : V →ₗ[K] V₂
⊢ IsNoetherian K ↥(v ∘ₗ u).range
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
hf : f.HasNoetherianRange
⊢ (-f).HasNoetherianRange

Tactic:
HasNoetherianRange,

Goal state after:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
hf : f.HasNoetherianRange
⊢ IsNoetherian K ↥(-f).range
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
H : Function.Surjective ⇑(linearCombination R Subtype.val)
σ : M → ↥s →₀ R
hσ : ∀ (b : M), (linearCombination R Subtype.val) (σ b) = b
⊢ ⇑(linearCombination R Subtype.val) '' σ '' ↑t = ↑t

Tactic:
simp only [Set.image_image, hσ, Set.image_id']

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ∨ b ∈ I ^ n

Tactic:
cases n

Goal state after:
case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
h : a * b ∈ I ^ 0
⊢ a ∈ I ∨ b ∈ I ^ 0

case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

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

Tactic:
Associates.mk_pow

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ Associates.mk J ^ (Associates.mk J).count (Associates.mk I).factors ∣ Associates.mk I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ ¬Associates.mk (J ^ ((Associates.mk J).count (Associates.mk I).factors + 1)) ∣ Associates.mk I

Tactic:
Associates.mk_pow

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ ¬Associates.mk J ^ ((Associates.mk J).count (Associates.mk I).factors + 1) ∣ Associates.mk I
Module: Mathlib.Algebra.Module.LocalizedModule.Away

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
r : R
h₁ : IsUnit ((algebraMap R (Module.End R N)) r)
h₂ : ∀ (x : N), ∃ n y, r ^ n • x = f y
h₃ : ∀ (x y : M), f x = f y → ∃ n, r ^ n • x = r ^ n • y
x✝ : ↥(Submonoid.powers r)
n : ℕ
⊢ IsUnit ((algebraMap R (Module.End R N)) ↑⟨(fun x ↦ r ^ x) n, ⋯⟩)

Tactic:
by simp [h₁.pow]

Goal state after:
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 : M
⊢ Associates.mk (generator (torsionOf R M x)) = Associates.mk (p ^ Nat.find ⋯)

Tactic:
Associates.mk_pow

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 : M
⊢ Associates.mk (generator (torsionOf R M x)) = Associates.mk p ^ Nat.find ⋯
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
⊢ (pderiv i) ((map φ) f) = (map φ) ((pderiv i) f)

Tactic:
by
  apply induction_on f (fun r ↦ by simp) (fun p q hp hq ↦ by simp [hp, hq]) fun p j eq ↦ ?_
  obtain rfl | h := eq_or_ne j i
  · simp [eq]
  · simp [eq, h]

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

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

Tactic:
cases q <;> simp [Pi.single_apply]

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

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

Tactic:
cases n

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

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

Goal state before:
pp: case a
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 ι σ
x : MvPolynomial ι T
y : σ
hy : (fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i)) y = x
Z : TensorProduct.includeRight ((aeval P.val) (P.relation y)) = 0
⊢ (aeval (Generators.baseChange T P.toGenerators).val) (P.relation y) =
    (eval₂Hom ((↑TensorProduct.includeRight).comp (algebraMap R S)) fun i ↦ ↑TensorProduct.includeRight (P.val i))
      (P.relation y)

Tactic:
RingHom.coe_coe,

Goal state after:
case a
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 ι σ
x : MvPolynomial ι T
y : σ
hy : (fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i)) y = x
Z : TensorProduct.includeRight ((aeval P.val) (P.relation y)) = 0
⊢ (aeval (Generators.baseChange T P.toGenerators).val) (P.relation y) =
    (eval₂Hom ((↑TensorProduct.includeRight).comp (algebraMap R S)) fun i ↦ TensorProduct.includeRight (P.val i))
      (P.relation y)
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
T : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ (((monomial (Finsupp.single () 1)) g + C (-1)).coeff.sum fun x j ↦
      (rename Sum.inr) (P.σ j) * (monomial (Finsupp.mapDomain Sum.inl x)) 1) =
    (rename Sum.inr) (P.σ g) * X (Sum.inl ()) + C (-1)

Tactic:
refine (Finsupp.sum_single_add_single (Finsupp.single () 1) 0 g (-1 : S) _ ?_ ?_).trans ?_

Goal state after:
case refine_1
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ Finsupp.single () 1 ≠ 0

case refine_2
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ ∀ (f : Unit →₀ ℕ), (rename Sum.inr) (P.σ 0) * (monomial (Finsupp.mapDomain Sum.inl f)) 1 = 0

case refine_3
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ (rename Sum.inr) (P.σ g) * (monomial (Finsupp.mapDomain Sum.inl (Finsupp.single () 1))) 1 +
      (rename Sum.inr) (P.σ (-1)) * (monomial (Finsupp.mapDomain Sum.inl 0)) 1 =
    (rename Sum.inr) (P.σ g) * X (Sum.inl ()) + C (-1)