mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
a✝ : R
x : MvPolynomial σ R
x✝ : x ∈ {p | ∃ (hp : IsWeightedHomogeneous w p m), ∀ (a : R), motive (C a * p) ⋯}
w✝ : IsWeightedHomogeneous w x m
hx : ∀ (a : R), motive (C a * x) ⋯
a : R
⊢ motive (C (a * a✝) * x) ⋯

Tactic:
apply hx

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = n then coeff x p else 0) = coeff x 0

Tactic:
rw [if_neg]
    · rw [coeff_zero]
    · rw [hp zero_coeff]; exact Ne.symm hn

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
B : Basis (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) := (Free.chooseBasis R M).end
g : ι → MvPolynomial ι' R := toMvPolynomial b' b id
H : (bind₁ g) (↑(bind₁ (toMvPolynomial b B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k)) = (bind₁ g) 0
⊢ ↑(bind₁ (toMvPolynomial b' B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0

Tactic:
have : toMvPolynomial b' B φ = fun i ↦ (MvPolynomial.bind₁ g) (toMvPolynomial b B φ i) :=
    funext <| toMvPolynomial_comp b' b B φ LinearMap.id

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
B : Basis (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) := (Free.chooseBasis R M).end
g : ι → MvPolynomial ι' R := toMvPolynomial b' b id
H : (bind₁ g) (↑(bind₁ (toMvPolynomial b B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k)) = (bind₁ g) 0
this : toMvPolynomial b' B φ = fun i ↦ (bind₁ g) (toMvPolynomial b B φ i)
⊢ ↑(bind₁ (toMvPolynomial b' B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝¹ : Fintype n
R : Type u_1
inst✝ : CommRing R
c : R
B : Matrix m n R
hc : c ∈ nonZeroDivisors R
hc' : IsSMulRegular R c
hreg : IsSMulRegular (m → R) c
⊢ (c • B).rank = B.rank

Tactic:
let f := LinearMap.lsmul R (m → R) c

Goal state after:
m : Type um
n : Type un
inst✝¹ : Fintype n
R : Type u_1
inst✝ : CommRing R
c : R
B : Matrix m n R
hc : c ∈ nonZeroDivisors R
hc' : IsSMulRegular R c
hreg : IsSMulRegular (m → R) c
f : (m → R) →ₗ[R] m → R := (LinearMap.lsmul R (m → R)) c
⊢ (c • B).rank = B.rank
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case neg
m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
s : Finset m
hz : ∀ x ∉ ↑s, A.row x = 0
B : Matrix m (↥s) R := of fun i a ↦ if ↑a = i then 1 else 0
hBdef : B = of fun i a ↦ if ↑a = i then 1 else 0
i : m
j : n
hi : i ∉ s
⊢ ∑ j_1, (if ↑j_1 = i then 1 else 0) * A (↑j_1) j = A i j

Tactic:
· have h0 : A i = 0 := hz i hi
      aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
⊢ (diagonal w).cRank = lift.{uR, um} #{ i // w i ≠ 0 }

Tactic:
set w' : {i // (w i) ≠ 0} → _ := fun i ↦ (diagonal w) i

Goal state after:
m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
⊢ (diagonal w).cRank = lift.{uR, um} #{ i // w i ≠ 0 }
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
x y : L
m : M
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
⊢ Exists.choose h x + Exists.choose h y - Exists.choose h (x + y) ∈ E.proj.ker

Tactic:
by simp [h.choose_spec _]

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

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
x y : L
m : M
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
z : ↥E.proj.ker
⊢ ⁅Exists.choose h x, Exists.choose h y⁆ - Exists.choose h ⁅x, y⁆ ∈ E.proj.ker

Tactic:
by simp [h.choose_spec _]

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

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
this : LieRingModule L M := E.ringModuleOf
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
r : R
x : L
m : M
⊢ Exists.choose ⋯ (r • x) - r • Exists.choose ⋯ x ∈ E.proj.ker

Tactic:
by simp [h.choose_spec _]

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

Goal state before:
pp: case inr
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
trace_T_U_zero : ∀ (w : A), (LinearMap.trace R ↥U) (T χ w) = 0
trace_za : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = χ ⁅z, a⁆ • ↑(finrank R ↥U)
⊢ Nontrivial ↥U

Tactic:
have hvU : v ∈ U := by
    apply Submodule.mem_iSup_of_mem 1
    apply Submodule.subset_span
    use 0, zero_lt_one
    rw [pow_zero, Module.End.one_apply]

Goal state after:
case inr
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
trace_T_U_zero : ∀ (w : A), (LinearMap.trace R ↥U) (T χ w) = 0
trace_za : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = χ ⁅z, a⁆ • ↑(finrank R ↥U)
hvU : v ∈ U
⊢ Nontrivial ↥U
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 : ℕ
i j : Fin n
hEq1 : Eq1 A p
⊢ (-∑ k > i, (Spec.stepEntry A)^[p] A k k) * A i j + ∑ k > i, (Spec.stepEntry A)^[p] A i k * A k j =
    (-1) ^ (p + 1) * (∑ α ∈ S (p + 1) i, pminor A α * A i j - ∑ k > i, ∑ α ∈ S p i, bminor A i k α * A k j)

Tactic:
paper_eq2 _ _ hEq1,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
hEq1 : Eq1 A p
⊢ ((-1) ^ (p + 1) * ∑ α ∈ S (p + 1) i, pminor A α) * A i j + ∑ k > i, (Spec.stepEntry A)^[p] A i k * A k j =
    (-1) ^ (p + 1) * (∑ α ∈ S (p + 1) i, pminor A α * A i j - ∑ k > i, ∑ α ∈ S p i, bminor A i k α * A k j)
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: case mp
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
⊢ I * I⁻¹ = 1 → generator ↑I ≠ 0

Tactic:
intro hI

Goal state after:
case mp
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
hI : I * I⁻¹ = 1
⊢ generator ↑I ≠ 0
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: case mpr
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
hg : generator ↑I ≠ 0
⊢ spanSingleton R₁⁰ (generator ↑I) ≠ 0

Tactic:
intro hI

Goal state after:
case mpr
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
hg : generator ↑I ≠ 0
hI : spanSingleton R₁⁰ (generator ↑I) = 0
⊢ False
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α_span : Weight.toLinear K (↥H) L ↑α ∈ I.rootSpan
hα_not : α ∉ I.rootSet
hα_nz : (↑α).IsNonZero
⊢ I.rootSpan ≤ LinearMap.ker ((Dual.eval K ↥H) (coroot ↑α))

Tactic:
rw [LieIdeal.rootSpan, Submodule.span_le]

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α_span : Weight.toLinear K (↥H) L ↑α ∈ I.rootSpan
hα_not : α ∉ I.rootSet
hα_nz : (↑α).IsNonZero
⊢ ⇑(rootSystem H).root '' I.rootSet ⊆ ↑(LinearMap.ker ((Dual.eval K ↥H) (coroot ↑α)))
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
inj : Function.Injective ⇑(algebraMap R P)
I : Ideal R
h : IsUnit ↑I
⊢ I.FG

Tactic:
rw [← coeIdeal_fg S inj I]
  exact FractionalIdeal.fg_of_isUnit (R := R) I h

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
⊢ ¬I = 0 → I = 1

Tactic:
intro hI

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
⊢ I = 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x y : K
y_ne : y ≠ 0
y_mem : (algebraMap K L) y ∈ I
⊢ (x / y) • (algebraMap K L) y ∈ I

Tactic:
exact smul_mem (M := L) I (x / y) y_mem

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

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
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)

Tactic:
mem_spanSingleton

Goal state after:
case mp
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
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z, z • (IsLocalization.map P' (RingHom.id R) ⋯) x = y
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
h : Prime P
⊢ P.IsPrime

Tactic:
by
  refine ⟨?_, fun hxy => ?_⟩
  · rintro rfl
    rw [← one_eq_top] at h
    exact h.not_isUnit isUnit_one
  · simp only [← dvd_span_singleton, ← span_singleton_mul_span_singleton] at hxy ⊢
    exact h.dvd_or_dvd hxy

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

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ∧ gcd I J ∣ J

Tactic:
exact ⟨gcd_dvd_left _ _, gcd_dvd_right _ _⟩

Goal state after:
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
x : ⨁ (i : ιB), M i
⊢ 0 • x = 0

Tactic:
simp only [smul_def, map_zero, AddMonoidHom.zero_apply]

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

Goal state before:
pp: T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ I ≠ 0

Tactic:
by assumption

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

Goal state before:
pp: T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ J ≠ 0

Tactic:
by assumption

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ I ≠ ⊥

Tactic:
intro hI

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I = ⊥
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
a : R
ha : a ∈ {d | d ∈ normalizedFactors r}
hx : (normalizedFactorsEquivSpanNormalizedFactors hr) ⟨a, ha⟩ = I
⊢ emultiplicity a r = emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr) ⟨a, ha⟩)) (span {r})

Tactic:
emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity hr ha

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
I : ↑{I | I ∈ normalizedFactors (span {r})}
a : R
ha : a ∈ {d | d ∈ normalizedFactors r}
hx : (normalizedFactorsEquivSpanNormalizedFactors hr) ⟨a, ha⟩ = I
⊢ emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr) ⟨a, ha⟩)) (span {r}) =
    emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr) ⟨a, ha⟩)) (span {r})
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
h : FinitePresentation R M
g : M →ₗ[R] N'
⊢ ∃ h s, f ∘ₗ h = s • g

Tactic:
by
  obtain ⟨σ, hσ, τ, hτ⟩ := h
  let π := Finsupp.linearCombination R ((↑) : σ → M)
  have hπ : Function.Surjective π :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hσ])
  classical
  choose s hs using IsLocalizedModule.surj S f
  let i : σ → N :=
    fun x ↦ (∏ j ∈ σ.erase x.1, (s (g j)).2) • (s (g x)).1
  let s₀ := ∏ j ∈ σ, (s (g j)).2
  have hi : f ∘ₗ Finsupp.linearCombination R i = (s₀ • g) ∘ₗ π := by
    ext j
    simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply,
      linearCombination_single, one_smul, LinearMap.map_smul_of_tower, ← hs, LinearMap.smul_apply,
      i, s₀, π]
    rw [← mul_smul, Finset.prod_erase_mul]
    exact j.prop
  have : ∀ x : τ, ∃ s : S, s • (Finsupp.linearCombination R i x) = 0 := by
    intro x
    convert_to ∃ s : S, s • (Finsupp.linearCombination R i x) = s • 0
    · simp only [smul_zero]
    apply IsLocalizedModule.exists_of_eq (S := S) (f := f)
    rw [← LinearMap.comp_apply, map_zero, hi, LinearMap.comp_apply]
    convert! map_zero (s₀ • g)
    rw [← LinearMap.mem_ker, ← hτ]
    exact Submodule.subset_span x.prop
  choose s' hs' using this
  let s₁ := ∏ i : τ, s' i
  have : LinearMap.ker π ≤ LinearMap.ker (s₁ • Finsupp.linearCombination R i) := by
    rw [← hτ, Submodule.span_le]
    intro x hxσ
    simp only [s₁]
    rw [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.smul_apply,
      ← Finset.prod_erase_mul _ _ (Finset.mem_univ ⟨x, hxσ⟩), mul_smul]
    convert! smul_zero _
    exact hs' ⟨x, hxσ⟩
  refine ⟨Submodule.liftQ _ _ this ∘ₗ
    (LinearMap.quotKerEquivOfSurjective _ hπ).symm.toLinearMap, s₁ * s₀, ?_⟩
  ext x
  obtain ⟨x, rfl⟩ := hπ x
  rw [← LinearMap.comp_apply, ← LinearMap.comp_apply, mul_smul, LinearMap.smul_comp, ← hi,
    ← LinearMap.comp_smul, LinearMap.comp_assoc, LinearMap.comp_assoc]
  simp

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
s : M → ↥S
hs : ∀ (x : M), s x • g₁ x = s x • g₂ x
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
⊢ σ.prod s • g₁ - σ.prod s • g₂ = 0

Tactic:
← LinearMap.ker_eq_top,

Goal state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
s : M → ↥S
hs : ∀ (x : M), s x • g₁ x = s x • g₂ x
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
⊢ (σ.prod s • g₁ - σ.prod s • g₂).ker = ⊤
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h.succ.refine_3.refine_2.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
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
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
⊢ ((↑f ∘ₗ (R ∙ s j).mkQ) ∘ₗ
      DirectSum.toModule R (Fin d) M fun i ↦ liftQSpanSingleton (p ^ k i) (LinearMap.toSpanSingleton R M ⋯.choose) ⋯) =
    LinearMap.id

Tactic:
rw [LinearMap.comp_assoc]

Goal state after:
case h.succ.refine_3.refine_2.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
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
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
⊢ (↑f ∘ₗ
      (R ∙ s j).mkQ ∘ₗ
        DirectSum.toModule R (Fin d) M fun i ↦
          liftQSpanSingleton (p ^ k i) (LinearMap.toSpanSingleton R M ⋯.choose) ⋯) =
    LinearMap.id
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case neg
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m n : σ →₀ ℕ
a : R
h : ¬n = m + single i 1
hn : ¬n i = 0
⊢ (if n - single i 1 = m then a * ↑(n i) else 0) = 0

Tactic:
apply if_neg

Goal state after:
case neg
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m n : σ →₀ ℕ
a : R
h : ¬n = m + single i 1
hn : ¬n i = 0
⊢ ¬n - single i 1 = m
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
h' : Module.Finite R M
hM : IsTorsion R M
I : Type u
fI : Fintype I
w✝ : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal fun i ↦ torsionBy R M (p i ^ e i)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (M ≃ₗ[R] ⨁ (i : ι), R ⧸ R ∙ p i ^ e i)

Tactic:
have :
    ∀ i,
      ∃ (d : ℕ) (k : Fin d → ℕ),
        Nonempty <| torsionBy R M (p i ^ e i) ≃ₗ[R] ⨁ j, R ⧸ R ∙ p i ^ k j := by
    exact fun i =>
      torsion_by_prime_power_decomposition.{u, v} (hp i)
        ((isTorsion'_powers_iff <| p i).mpr fun x => ⟨e i, smul_torsionBy _ _⟩)

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
h' : Module.Finite R M
hM : IsTorsion R M
I : Type u
fI : Fintype I
w✝ : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal fun i ↦ torsionBy R M (p i ^ e i)
this : ∀ (i : I), ∃ d k, Nonempty (↥(torsionBy R M (p i ^ e i)) ≃ₗ[R] ⨁ (j : Fin d), R ⧸ R ∙ p i ^ k j)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (M ≃ₗ[R] ⨁ (i : ι), R ⧸ R ∙ p i ^ e i)