mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
⊢ Polynomial.map (MvPolynomial.eval₂Hom (MvPolynomial.C.comp f) MvPolynomial.X) (univ R n) = univ S n

Tactic:
univ_map_eval₂Hom

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
⊢ (of (Function.curry MvPolynomial.X)).charpoly = univ S n
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case single_add
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
r : R
a : σ
b : ℕ
f : σ →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : b ≠ 0
h : (monomial f) r ∈ homogeneousSubmodule σ R 1 ^ degree f
⊢ (monomial (single a b + f)) r ∈ homogeneousSubmodule σ R 1 ^ degree (single a b + f)

Tactic:
rw [map_add, Finsupp.degree_single, monomial_single_add, pow_add]

Goal state after:
case single_add
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
r : R
a : σ
b : ℕ
f : σ →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : b ≠ 0
h : (monomial f) r ∈ homogeneousSubmodule σ R 1 ^ degree f
⊢ X a ^ b * (monomial f) r ∈ homogeneousSubmodule σ R 1 ^ b * homogeneousSubmodule σ R 1 ^ degree f
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
tfae_2_to_3 : (minpoly K φ).IsRoot 0 → constantCoeff (charpoly φ) = 0
⊢ constantCoeff (charpoly φ) = 0 → LinearMap.det φ = 0

Tactic:
← LinearMap.det_toMatrix (chooseBasis K M),

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
tfae_2_to_3 : (minpoly K φ).IsRoot 0 → constantCoeff (charpoly φ) = 0
⊢ constantCoeff (charpoly φ) = 0 → ((toMatrix (chooseBasis K M) (chooseBasis K M)) φ).det = 0
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
inst✝² : LinearOrder M
inst✝¹ : OrderBot M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
⊢ IsWeightedHomogeneous w p 0 ↔ ∀ s ∈ p.support, (weight w) s = 0

Tactic:
IsWeightedHomogeneous

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
σ : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : LinearOrder M
inst✝¹ : OrderBot M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
⊢ (∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weight w) d = 0) ↔ ∀ s ∈ p.support, (weight w) s = 0
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
inst✝² : LinearOrder M
inst✝¹ : OrderBot M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
⊢ IsWeightedHomogeneous w p 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0

Tactic:
IsWeightedHomogeneous

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
σ : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : LinearOrder M
inst✝¹ : OrderBot M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
⊢ (∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weight w) d = 0) ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d ((homogeneousComponent n) φ) = if degree d = n then coeff d φ else 0

Tactic:
rw [degree_eq_weight_one]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d ((homogeneousComponent n) φ) = if (weight fun x ↦ 1) d = n then coeff d φ else 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ φ.totalDegree < d.support.sum ⇑d → 0 = coeff d φ

Tactic:
exact fun h => (coeff_eq_zero_of_totalDegree_lt h).symm

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ ((homogeneousComponent n) p).support = {c ∈ p.support | degree c = n}

Tactic:
rw [degree_eq_weight_one]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ ((homogeneousComponent n) p).support = {c ∈ p.support | (weight fun x ↦ 1) c = n}
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ DirectSum.Decomposition.decompose' = fun φ ↦
    (DirectSum.mk (fun i ↦ ↥(homogeneousSubmodule σ R i)) (Finset.image (⇑degree) φ.support)) fun m ↦
      ⟨(homogeneousComponent ↑m) φ, ⋯⟩

Tactic:
rw [degree_eq_weight_one]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ DirectSum.Decomposition.decompose' = fun φ ↦
    (DirectSum.mk (fun i ↦ ↥(homogeneousSubmodule σ R i)) (Finset.image (⇑(weight fun x ↦ 1)) φ.support)) fun m ↦
      ⟨(homogeneousComponent ↑m) φ, ⋯⟩
Module: Mathlib.Algebra.Lie.Matrix

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type w₁
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
x y : Matrix n n R
v : n → R
⊢ x *ᵥ y *ᵥ v = ⁅x, y⁆ *ᵥ v + y *ᵥ x *ᵥ v

Tactic:
simp only [Ring.lie_def, mulVec_mulVec, sub_mulVec, sub_add_cancel]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
⊢ Aᵀ * J l R * Aᵀᵀ = J l R

Tactic:
rw [transpose_transpose]

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
⊢ Aᵀ * J l R * A = J l R
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C)

Tactic:
have hf (x) : f x = x.submatrix s.symm s.symm := rfl

Goal state after:
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C)
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
o : Type uo
R : Type uR
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
⊢ (A * B).rank ≤ B.rank

Tactic:
by
  nontriviality R
  rw [rank, rank, mulVecLin_mul]
  exact finrank_le_finrank_of_rank_le_rank (LinearMap.lift_rank_comp_le_right _ _)
    (rank_lt_aleph0 _ _)

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

Goal state before:
pp: case e'_4
m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := ⋯
hli' : LinearIndependent R fun i ↦ Pi.single i (if w i = 0 then 1 else w i)
⊢ w' = (fun i ↦ Pi.single i (if w i = 0 then 1 else w i)) ∘ Subtype.val

Tactic:
ext ⟨j, hj⟩ k

Goal state after:
case e'_4
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
hli' : LinearIndependent R fun i ↦ Pi.single i (if w i = 0 then 1 else w i)
j : m
hj : w j ≠ 0
k : m
⊢ w' ⟨j, hj⟩ k = ((fun i ↦ Pi.single i (if w i = 0 then 1 else w i)) ∘ Subtype.val) ⟨j, hj⟩ k
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
⊢ eval α (χ.coeff i) = 0

Tactic:
rw [← coe_evalRingHom, ← coeff_map, lieCharpoly_map_eval,
    (LinearMap.charpoly_eq_X_pow_iff _).mpr, coeff_X_pow, if_neg hi.ne]

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
⊢ ∀ (m : ↥E), ∃ n, ((toEnd K ↥U ↥E) (α • u + x') ^ n) m = 0
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: case inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
hik : k ≠ i
⊢ ⁅0, ((of L j) y) k⁆ = 0 k

Tactic:
zero_lie,

Goal state after:
case inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
hik : k ≠ i
⊢ 0 = 0 k
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
a b c : lib R X
h : Rel R X b c
⊢ Rel R X (a + b) (a + c)

Tactic:
rw [add_comm _ b, add_comm _ c]; exact h.add_right _

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
k : ℕ
left✝ : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k) x)
⊢ (f.toList x).formPerm ((f ^ k) x) = (f.cycleOf x) ((f ^ k) x)

Tactic:
cycleOf_apply_apply_pow_self,

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
k : ℕ
left✝ : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k) x)
⊢ (f.toList x).formPerm ((f ^ k) x) = (f ^ (k + 1)) x
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : { s // s.Nodup ∧ s.Nontrivial } → { f // f.IsCycle } := fun s ↦ ⟨(↑s).formPerm ⋯, ⋯⟩
⊢ ∀ (b : { f // f.IsCycle }), ∃! a, f a = b

Tactic:
rintro ⟨f, hf⟩

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f✝ : { s // s.Nodup ∧ s.Nontrivial } → { f // f.IsCycle } := fun s ↦ ⟨(↑s).formPerm ⋯, ⋯⟩
f : Perm α
hf : f.IsCycle
⊢ ∃! a, f✝ a = ⟨f, hf⟩
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
⊢ BirdDet.sumFrom n (↑i + 1) f = ∑ k ∈ Finset.Ico (↑i + 1) n, f k

Tactic:
rw [sumFrom_eq_sum_Ico]

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
L' L'' : LieRinehartSubalgebra A L
h : (fun L' ↦ L'.carrier) L' = (fun L' ↦ L'.carrier) L''
⊢ L' = L''

Tactic:
rcases 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
toSubmodule✝ : Submodule A L
lie_mem'✝ : ∀ {a b : L}, a ∈ toSubmodule✝.carrier → b ∈ toSubmodule✝.carrier → ⁅a, b⁆ ∈ toSubmodule✝.carrier
h : (fun L' ↦ L'.carrier) { toSubmodule := toSubmodule✝, lie_mem' := lie_mem'✝ } = (fun L' ↦ L'.carrier) L''
⊢ { toSubmodule := toSubmodule✝, lie_mem' := lie_mem'✝ } = L''
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
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
hγ : rootSpace H ⇑(S.root' γ) ≤ LieSubmodule.restr I H
⊢ -S.pairing δ γ ≠ 0

Tactic:
neg_ne_zero

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
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
hγ : rootSpace H ⇑(S.root' γ) ≤ LieSubmodule.restr I H
⊢ S.pairing δ γ ≠ 0
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: 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
hI : I ≠ ⊥
⊢ (algebraMap R₁ K) ↑I.den ∈ I⁻¹

Tactic:
mem_inv_iff hI

Goal state after:
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
hI : I ≠ ⊥
⊢ ∀ y ∈ I, (algebraMap R₁ K) ↑I.den * 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₁
I J J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ J / J' ↔ I * J' ≤ J

Tactic:
rw [div_of_ne_zero hJ', ← coe_le_coe (I := I * J') (J := J), coe_mul]

Goal state after:
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₁
I J J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ ⟨↑J / ↑J', ⋯⟩ ↔ ↑I * ↑J' ≤ ↑J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
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₁
I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
y' : R₁
left✝ : y' ∈ ↑⊤
⊢ x✝ * (Algebra.linearMap R₁ K) y' ∈ ↑I

Tactic:
convert! Submodule.smul_mem _ y' h using 1

Goal state after:
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₁
I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
y' : R₁
left✝ : y' ∈ ↑⊤
⊢ x✝ * (Algebra.linearMap R₁ K) y' = y' • x✝
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_2
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₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x' : R₁
hx'✝ : x' ∈ comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)
hy : (algebraMap R₁ K) x' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I))
y' : K
hy' : y' ∈ I
hx' : (Algebra.linearMap R₁ K) x' = (algebraMap R₁ K) a_inv * y'
⊢ ((algebraMap R₁ K) a_inv)⁻¹ * (algebraMap R₁ K) x' ∈ I

Tactic:
Algebra.linearMap_apply

Goal state after:
case refine_2
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₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x' : R₁
hx'✝ : x' ∈ comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)
hy : (algebraMap R₁ K) x' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I))
y' : K
hy' : y' ∈ I
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * y'
⊢ ((algebraMap R₁ K) a_inv)⁻¹ * (algebraMap R₁ K) x' ∈ I
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✝ : IsNoetherianRing R₁
I : Ideal R₁
⊢ IsNoetherian R₁ ↥↑↑I

Tactic:
rw [isNoetherian_iff]
  intro J hJ
  obtain ⟨J, rfl⟩ := le_one_iff_exists_coeIdeal.mp (le_trans hJ coeIdeal_le_one)
  exact (IsNoetherian.noetherian J).map _

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

Goal state before:
pp: case mp
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
x : K
y : L
⊢ (∃ a, (semilinearEquivOfRingEquiv K L f) (a • x) = y) → ∃ a, a • (IsLocalization.map L ↑f ⋯) x = y

Tactic:
rintro ⟨r, rfl⟩
    use f r
    exact .symm (map_smulₛₗ _ r x)

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
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
this : (idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩ ≤ (idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩ ↔ ⟨M, hM⟩ ≤ ⟨L, hL⟩
⊢ ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩) ∣ ↑((idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩) ↔ L ∣ M

Tactic:
rw [dvd_iff_le, dvd_iff_le, Subtype.coe_le_coe, this, Subtype.mk_le_mk]

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

Goal state before:
pp: case refine_2
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
inst✝ : IsLocalizedModule.Away r f
u : Rˣ
⊢ ∀ (x : N), ∃ n y, (↑u * r) ^ n • x = f y

Tactic:
intro y
    obtain ⟨n, x, hx⟩ := surj f r y
    use n, (u ^ n) • x
    simp [mul_pow, ← hx, mul_smul, Units.smul_def]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Field K
ι : ?m.1
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ (Multiset.map (fun P ↦ P) (factors I)).prod = (factors I).prod

Tactic:
Multiset.map_id'

Goal state after:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Field K
ι : ?m.1
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ (factors I).prod = (factors I).prod
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: case C
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), D (p * X i) = p • D (X i) + X i • D p
p : MvPolynomial σ R
c : R
⊢ D (c • p) = p • D (C c) + C c • D p

Tactic:
hC,

Goal state after:
case C
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), D (p * X i) = p • D (X i) + X i • D p
p : MvPolynomial σ R
c : R
⊢ D (c • p) = p • 0 + C c • D p
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h.succ.refine_2
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
hs' : Submodule.span R ((fun a ↦ Submodule.Quotient.mk a) ∘ s '' {j}ᶜ) = ⊤
⊢ Submodule.span R (Submodule.Quotient.mk ∘ s '' {j}ᶜ) = ⊤

Tactic:
exact hs'

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: case single.e_a.mul_X
R : Type u
inst✝ : CommRing R
σ : Type u_1
b p✝ : MvPolynomial σ R
n✝ : σ
a✝ :
  (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1) p✝) =
    (D R (MvPolynomial σ R)) p✝
⊢ (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1) (p✝ * MvPolynomial.X n✝)) =
    (D R (MvPolynomial σ R)) (p✝ * MvPolynomial.X n✝)

Tactic:
· simp [*]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : Unit
⊢ invSelf r = (aeval fun x ↦ invSelf r) (X x)

Tactic:
aeval_X

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : Unit
⊢ invSelf r = invSelf r