mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case h.refine_2
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
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : z ∈ engel K ↑v
z' : Q := (LieSubmodule.Quotient.mk' E) z
hz' : ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
n : ℕ := Nat.find hz'
_hn : n = Nat.find hz'
hn : ((toEnd K (↥U) Q) v ^ n) z' = 0
k : ℕ
hk : n = k + 1
hsψ : z' ≠ 0
⊢ ((toEnd K (↥U) Q) (α • u + x')) (((toEnd K (↥U) Q) v ^ k) z') = ((toEnd K (↥U) Q) v ^ (k + 1)) z'

Tactic:
pow_succ',

Goal state after:
case h.refine_2
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
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : z ∈ engel K ↑v
z' : Q := (LieSubmodule.Quotient.mk' E) z
hz' : ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
n : ℕ := Nat.find hz'
_hn : n = Nat.find hz'
hn : ((toEnd K (↥U) Q) v ^ n) z' = 0
k : ℕ
hk : n = k + 1
hsψ : z' ≠ 0
⊢ ((toEnd K (↥U) Q) (α • u + x')) (((toEnd K (↥U) Q) v ^ k) z') = ((toEnd K (↥U) Q) v * (toEnd K (↥U) Q) v ^ k) z'
Module: Mathlib.Algebra.Lie.UniversalEnveloping

Goal state before:
pp: case lie_compat
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f✝ f : L →ₗ⁅R⁆ A
a b : TensorAlgebra R L
x✝ y✝ : L
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [LieRing.of_associative_ring_bracket]

Goal state after:
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
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
⊢ ∃ x, (engel K x).IsCartanSubalgebra

Tactic:
use x

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
⊢ (engel K x).IsCartanSubalgebra
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)
n : ℕ
hn :
  ∀ (w : A),
    ∀ a < n + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}
w : A
hm : n + 1 < n + 1 + 1
H : ∀ (w : A), ⁅w, ((toEnd R L V) z ^ n) v⁆ = (T χ w) (((toEnd R L V) z ^ n) v) + χ w • ((toEnd R L V) z ^ n) v
⊢ ((toEnd R A V) w) (((toEnd R L V) z ^ (n + 1)) v) - (χ w • 1) (((toEnd R L V) z ^ (n + 1)) v) ∈
    Submodule.span R {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}

Tactic:
pow_succ',

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)
n : ℕ
hn :
  ∀ (w : A),
    ∀ a < n + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}
w : A
hm : n + 1 < n + 1 + 1
H : ∀ (w : A), ⁅w, ((toEnd R L V) z ^ n) v⁆ = (T χ w) (((toEnd R L V) z ^ n) v) + χ w • ((toEnd R L V) z ^ n) v
⊢ ((toEnd R A V) w) (((toEnd R L V) z * (toEnd R L V) z ^ n) v) -
      (χ w • 1) (((toEnd R L V) z * (toEnd R L V) z ^ n) v) ∈
    Submodule.span R {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ (x :: y :: l).formPerm.IsCycle

Tactic:
use x

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ (x :: y :: l).formPerm x ≠ x ∧ ∀ ⦃y_1 : α⦄, (x :: y :: l).formPerm y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg.zero.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hc : (p.cycleOf x).IsCycle
hn✝ : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
m : ℕ
hx : (p ^ m.succ) x ≠ x
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ 0) x = (p.cycleOf x ^ (m + 1)) x → 0 = m + 1

Tactic:
simp [hx.symm]

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 ((f ^ k) x) = (f ^ (k + 1)) x

pp: case pos.hx
α : 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 ^ k) x ∈ f.toList x

Tactic:
pow_succ',

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 ((f ^ k) x) = (f * f ^ k) x

case pos.hx
α : 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 ^ k) x ∈ f.toList x
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ ∀ (x : α), s ≠ [x]

Tactic:
· rintro _ rfl
        simp at hl

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ ((monomial E.order) 1).degree = ↑E.order

Tactic:
degree_monomial E.order one_ne_zero

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ ↑E.order = ↑E.order
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (E.coeffs i)).degree < ((monomial E.order) 1).degree

Tactic:
degree_monomial E.order one_ne_zero

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (E.coeffs i)).degree < ↑E.order
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case neg.refine_2
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t ↦ ↑(d ⟨c₁ t, ⋯⟩)
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)
r : Associates N
hr : r ≤ ↑(d ⟨c₁ 1 ^ s, hs'⟩)
⊢ ∃ i, r = c₂ i

Tactic:
have : r ≤ n := hr.trans (d ⟨c₁ 1 ^ s, _⟩).2

Goal state after:
case neg.refine_2
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t ↦ ↑(d ⟨c₁ t, ⋯⟩)
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)
r : Associates N
hr : r ≤ ↑(d ⟨c₁ 1 ^ s, hs'⟩)
this : r ≤ n
⊢ ∃ i, r = c₂ i
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'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
b' : P
b'_mem : b' ∈ I
hb' : g b' = b
x : R
hx : (algebraMap R P) x = a • b'
⊢ IsInteger R (a • b)

Tactic:
use x

Goal state after:
case h
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'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
b' : P
b'_mem : b' ∈ I
hb' : g b' = b
x : R
hx : (algebraMap R P) x = a • b'
⊢ (algebraMap R P') x = a • b
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
s : Set P
x✝³ : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s, IsInteger R (a • b)
x✝² : P
hb : x✝² ∈ span R s
x y : P
x✝¹ : x ∈ span R s
x✝ : y ∈ span R s
hx : IsInteger R (a • x)
hy : IsInteger R (a • y)
⊢ IsInteger R (a • x + a • y)

Tactic:
exact isInteger_add hx hy

Goal state after:
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:
rw [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.DedekindDomain.Ideal.Basic

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
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
hJ : J ≠ 0
this : I / J * J ≤ I
⊢ I / J ≤ I * J⁻¹

Tactic:
by
        simpa [mul_assoc, isDedekindDomainInv_iff.mp h _ hJ] using mul_left_mono (a := J⁻¹) this

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

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ ⊥
hI : I = ⊥
⊢ J = ⊥

Tactic:
← eq_bot_iff

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J = ⊥
hI : I = ⊥
⊢ J = ⊥
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
x : P
I J : FractionalIdeal S P
⊢ (∀ (i : P), (∃ z, z • x = i) → ∀ j ∈ I, i * j ∈ J) → ∀ z ∈ I, x * z ∈ J

pp: case mpr
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
I J : FractionalIdeal S P
⊢ (∀ z ∈ I, x * z ∈ J) → ∀ (i : P), (∃ z, z • x = i) → ∀ j ∈ I, i * j ∈ J

Tactic:
· intro h zI hzI
    exact h x ⟨1, one_smul _ _⟩ zI hzI

Goal state after:
case mpr
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
I J : FractionalIdeal S P
⊢ (∀ z ∈ I, x * z ∈ J) → ∀ (i : P), (∃ z, z • x = i) → ∀ j ∈ I, i * j ∈ J
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: K : Type u_3
inst✝ : Field K
p : K[X]
⊢ factors (span {p}) = Multiset.map (fun q ↦ span {q}) (factors p)

Tactic:
by
  rcases eq_or_ne p 0 with rfl | hp; · simpa [Set.singleton_zero] using! normalizedFactors_zero
  have : ∀ q ∈ (factors p).map (fun q ↦ span {q}), Prime q := fun q hq ↦ by
    obtain ⟨r, hr, rfl⟩ := Multiset.mem_map.mp hq
    exact prime_span_singleton_iff.mpr <| prime_of_factor r hr
  rw [← span_singleton_eq_span_singleton.mpr (factors_prod hp), ← multiset_prod_span_singleton,
    factors_eq_normalizedFactors, normalizedFactors_prod_of_prime this]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid 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'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
x : M
s : Finset M'
y : ↥S := commonDenomOfFinset S f s
hx₁✝ : y • ↑s = ⇑f '' ↑(finsetIntegerMultiple S f s)
hx₁ : y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))
hx : f (↑y • x) ∈ Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)

Tactic:
← Submodule.map_span f

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid 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'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
x : M
s : Finset M'
y : ↥S := commonDenomOfFinset S f s
hx₁✝ : y • ↑s = ⇑f '' ↑(finsetIntegerMultiple S f s)
hx₁ : y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))
hx : f (↑y • x) ∈ Submodule.map f (Submodule.span R ↑(finsetIntegerMultiple S f s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)
Module: Mathlib.Algebra.Module.Presentation.Cokernel

Goal state before:
pp: A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
i : ι
⊢ (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ }) (pres₂.π (data.lift i)) = 0

Tactic:
Relations.Solution.IsPresentation.π_desc_apply

Goal state after:
A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
i : ι
⊢ { var := s.var, linearCombination_var_relation := ⋯ }.π (data.lift i) = 0
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P✝ : Extension R S
M : Submonoid S
S' : Type u_1
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : IsLocalization M S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R S S'
P : Extension R S
⊢ IsScalarTower R (Localization (Submonoid.comap (algebraMap P.Ring S) M)) S'

Tactic:
by
    let : Algebra (Localization (M.comap (algebraMap P.Ring S))) S' :=
      (IsLocalization.lift (M := (M.comap (algebraMap P.Ring S)))
        (g := (algebraMap S S').comp (algebraMap P.Ring S))
        (by simpa using fun x hx ↦ IsLocalization.map_units S' ⟨_, hx⟩)).toAlgebra
    apply IsScalarTower.of_algebraMap_eq'
    rw [RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_eq R P.Ring (Localization _),
      ← RingHom.comp_assoc, IsLocalization.lift_comp, RingHom.comp_assoc,
      ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]

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

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span (Set.range (Sum.elim (Q.compRelationAux P) fun rp ↦ (rename Sum.inr) (P.relation rp))) =
    Ideal.comap (Q.aux P) (Ideal.span (⇑(Q.aux P) '' Set.range (Q.compRelationAux P)))

Tactic:
← Ideal.map_span,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span (Set.range (Sum.elim (Q.compRelationAux P) fun rp ↦ (rename Sum.inr) (P.relation rp))) =
    Ideal.comap (Q.aux P) (Ideal.map (Q.aux P) (Ideal.span (Set.range (Q.compRelationAux P))))
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Generators R S ι
T : Type u_8
inst✝¹ : CommRing T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
⊢ Ideal.comap (aeval P.val) (RingHom.ker ↑e) = P.ker

Tactic:
AlgHom.ker_coe_equiv,

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Generators R S ι
T : Type u_8
inst✝¹ : CommRing T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
⊢ Ideal.comap (aeval P.val) ⊥ = P.ker
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : 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 ι
⊢ Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker = Q.ker

Tactic:
ext x
  rw [Ideal.mem_map_iff_of_surjective _ (toAlgHom_ofComp_surjective Q P)]
  constructor
  · rintro ⟨x, hx, rfl⟩
    simp only [ker_eq_ker_aeval_val,
      RingHom.mem_ker] at hx ⊢
    rw [← hx, Hom.algebraMap_toAlgHom, algebraMap_self_apply]
  · intro hx
    exact ⟨_, (kerCompPreimage Q P ⟨x, hx⟩).2, ofComp_kerCompPreimage Q P ⟨x, hx⟩⟩

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∀ (M' : Submodule R M), Injective ⇑(rTensor N M'.subtype)) →
    ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n

Tactic:
intro h k m n hmn

Goal state after:
case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : ∀ (M' : Submodule R M), Injective ⇑(rTensor N M'.subtype)
k : ℕ
m : Fin k → M
n : Fin k → N
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
⊢ VanishesTrivially R m n
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)) →
    ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n

Tactic:
intro h k m n hmn

Goal state after:
case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : ∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)
k : ℕ
m : Fin k → M
n : Fin k → N
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
⊢ VanishesTrivially R m n
Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct

Goal state before:
pp: R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝¹ : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
⊢ ∀ [inst : DecidableEq (ι₁ ⊕ ι₂)] (m : (i : ι₁ ⊕ ι₂) → N i) (i : ι₁ ⊕ ι₂) (c : R) (x : N i),
    ((a fun i₁ ↦ Function.update m i (c • x) (Sum.inl i₁)) ⊗ₜ[R] b fun i₂ ↦ Function.update m i (c • x) (Sum.inr i₂)) =
      c • (a fun i₁ ↦ Function.update m i x (Sum.inl i₁)) ⊗ₜ[R] b fun i₂ ↦ Function.update m i x (Sum.inr i₂)

Tactic:
rintro _ m (i₁ | i₂) p q
    · let := Classical.decEq ι₁; simp
    · let := Classical.decEq ι₂; simp

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

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
x : ↥(⋀[R]^n M)
s : ↑(powersetCard I n)
⊢ ((Basis.exteriorPower n b).repr x) s = (ιMultiDual R n b s) x

Tactic:
simpa [← Basis.coord_apply] using LinearMap.congr_fun (basis_coord R n b s) x

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
y : R
m : ↥M
⊢ ↑(M.rTensorOne' (m ⊗ₜ[R] (algebraMap R ↥⊥) y)) = ↑(y • m)

Tactic:
simp_rw [rTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul]
  rw [Algebra.smul_def, Algebra.commutes]
  exact mulMap_tmul M _ _ _

Goal state after: