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

Goal state before:
pp: 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
w : A
key : ∀ (i : ℕ), i ≠ 0 → ∃ j < i, Submodule.map (T χ w) (U' i) ≤ U' j
x : ↥U
this : ↑x ∈ (T χ w).maxGenEigenspace 0
⊢ ∃ n, (T χ w ^ n) x = 0

Tactic:
simp only [Module.End.mem_maxGenEigenspace, zero_smul, sub_zero] at this

Goal state after:
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
w : A
key : ∀ (i : ℕ), i ≠ 0 → ∃ j < i, Submodule.map (T χ w) (U' i) ≤ U' j
x : ↥U
this : ∃ k, (T χ w ^ k) ↑x = 0
⊢ ∃ n, (T χ w ^ n) x = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
key : Finset.univ.val = x ::ₘ Finset.univ.val.erase x
⊢ (x ::ₘ Finset.univ.val.erase x).recOn (Quot.mk ⇑(IsRotated.setoid α) [])
      (fun x x_1 l ↦ if f x = x then l else ↑(f.toList x)) ⋯ =
    ↑(f.toList x)

Tactic:
simp [hx]

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
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
have hA : IsCompl A.toSubmodule (k ∙ z) := isCompl_span_singleton_of_isCoatom_of_notMem hA hz

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)
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: n : ℕ
i : Fin n
a✝ : Fin 0 → Fin n
⊢ a✝ ∈ S 0 i ↔ a✝ ∈ {![]}

Tactic:
simp [mem_S_iff, Fin.strictMono_iff_lt_succ, eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case refine_1
n p : ℕ
i : Fin n
α : Fin (p + 1) → Fin n
hα : StrictMono (Fin.cons i α)
⊢ StrictMono (Fin.cons (α 0) (Fin.tail α))

Tactic:
simp only [Fin.cons_self_tail]

Goal state after:
case refine_1
n p : ℕ
i : Fin n
α : Fin (p + 1) → Fin n
hα : StrictMono (Fin.cons i α)
⊢ StrictMono α
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ Set.MapsTo
    (fun x ↦
      match x with
      | (α, k) => (k.removeNth α, α k))
    ↑(S (p + 1) i ×ˢ Finset.univ) ↑(S p i ×ˢ Finset.Ioi i)

Tactic:
rintro ⟨α, t⟩ hα

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
α : Fin (p + 1) → Fin n
t : Fin (p + 1)
hα : (α, t) ∈ ↑(S (p + 1) i ×ˢ Finset.univ)
⊢ (fun x ↦
        match x with
        | (α, k) => (k.removeNth α, α k))
      (α, t) ∈
    ↑(S p i ×ˢ Finset.Ioi i)
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
x : P
hx : x = 0
⊢ (Algebra.linearMap R P) 0 = x

Tactic:
simp [hx]

Goal state after:
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
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ ↑I
⊢ I.den • ↑I = ⊥

Tactic:
rw [den_mul_self_eq_num, hI, Submodule.map_bot]

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case pos
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : s = 0
⊢ ↑(d ⟨p, ⋯⟩) ^ s ≤ n

pp: case neg
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
⊢ ↑(d ⟨p, ⋯⟩) ^ s ≤ n

Tactic:
· simp [← Associates.bot_eq_one, hs]

Goal state after:
case neg
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
⊢ ↑(d ⟨p, ⋯⟩) ^ s ≤ n
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ˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
l : ↑(Set.Iic (Associates.mk m))
⊢ associatesEquivOfUniqueUnits ↑l ∣ m

Tactic:
obtain ⟨x, hx⟩ := l
            rw [Subtype.coe_mk, associatesEquivOfUniqueUnits_apply, out_dvd_iff]
            exact hx

Goal state after:
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ˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
l : ↑(Set.Iic (Associates.mk n))
⊢ associatesEquivOfUniqueUnits ↑l ∣ n

Tactic:
obtain ⟨x, hx⟩ := l
            rw [Subtype.coe_mk, associatesEquivOfUniqueUnits_apply, out_dvd_iff]
            exact hx

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

Goal state before:
pp: case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
h : Prime P
⊢ P ≠ ⊤

pp: case refine_2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
h : Prime P
x✝ y✝ : A
hxy : x✝ * y✝ ∈ P
⊢ x✝ ∈ P ∨ y✝ ∈ P

Tactic:
· rintro rfl
    rw [← one_eq_top] at h
    exact h.not_isUnit isUnit_one

Goal state after:
case refine_2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
h : Prime P
x✝ y✝ : A
hxy : x✝ * y✝ ∈ P
⊢ x✝ ∈ P ∨ y✝ ∈ P
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : ¬p = 0
⊢ Prime p ∧ p ∣ I ↔ p.IsPrime ∧ p ∣ I

Tactic:
prime_iff_isPrime

Goal state after:
case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : ¬p = 0
⊢ p.IsPrime ∧ p ∣ I ↔ p.IsPrime ∧ p ∣ I

case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : ¬p = 0
⊢ p ≠ ⊥
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: 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
I : Submodule R K
hI : IsFractional R⁰ I
⊢ IsFractional S⁰ (Submodule.map (↑(semilinearEquivOfRingEquiv K L f)) I)

Tactic:
by
  simp only [IsFractional, mem_nonZeroDivisors_iff_ne_zero, ne_eq, Submodule.mem_map,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hI ⊢
  obtain ⟨r, hr0, hr⟩ := hI
  use f r
  refine ⟨by simp [hr0], ?_⟩
  intro x hx
  specialize hr x hx
  simp only [IsLocalization.IsInteger, RingHom.mem_rangeS] at hr ⊢
  obtain ⟨r', hr'⟩ := hr
  use f r'
  simp only [semilinearEquivOfRingEquiv, RingEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe,
    EquivLike.coe_coe, Equiv.invFun_as_coe, LinearMap.coe_mk, AddHom.coe_mk]
  rw [Algebra.smul_def, ← ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
    ← map_mul, ← Algebra.smul_def, ← hr', ringEquivOfRingEquiv_algebraMap]

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

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
S✝ : Submonoid R✝
P : Type u_2
inst✝¹⁶ : CommRing P
inst✝¹⁵ : Algebra R✝ P
R₁ : Type u_3
inst✝¹⁴ : CommRing R₁
K✝ : Type u_4
inst✝¹³ : Field K✝
inst✝¹² : Algebra R₁ K✝
inst✝¹¹ : IsFractionRing R₁ K✝
inst✝¹⁰ : IsDomain R₁
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
I : FractionalIdeal R⁰ K
⊢ (fun J ↦ ⟨Submodule.map ↑(semilinearEquivOfRingEquiv L K f.symm) ↑J, ⋯⟩)
      ((fun I ↦ ⟨Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑I, ⋯⟩) I) =
    I

Tactic:
simp only [RingEquiv.symm_symm, val_eq_coe, ← Submodule.map_comp, LinearEquiv.comp_coe,
        coe_ext_iff, coe_mk]

Goal state after:
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
S✝ : Submonoid R✝
P : Type u_2
inst✝¹⁶ : CommRing P
inst✝¹⁵ : Algebra R✝ P
R₁ : Type u_3
inst✝¹⁴ : CommRing R₁
K✝ : Type u_4
inst✝¹³ : Field K✝
inst✝¹² : Algebra R₁ K✝
inst✝¹¹ : IsFractionRing R₁ K✝
inst✝¹⁰ : IsDomain R₁
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
I : FractionalIdeal R⁰ K
⊢ Submodule.map ↑((semilinearEquivOfRingEquiv K L f).trans (semilinearEquivOfRingEquiv L K f.symm)) ↑I = ↑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
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₁
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
I : FractionalIdeal S⁰ L
⊢ (fun I ↦ ⟨Submodule.map ↑(semilinearEquivOfRingEquiv K L f) ↑I, ⋯⟩)
      ((fun J ↦ ⟨Submodule.map ↑(semilinearEquivOfRingEquiv L K f.symm) ↑J, ⋯⟩) I) =
    I

Tactic:
simp only [RingEquiv.symm_symm, val_eq_coe, ← Submodule.map_comp, LinearEquiv.comp_coe,
        coe_ext_iff, coe_mk]

Goal state after:
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
S✝ : Submonoid R✝
P : Type u_2
inst✝¹⁶ : CommRing P
inst✝¹⁵ : Algebra R✝ P
R₁ : Type u_3
inst✝¹⁴ : CommRing R₁
K✝ : Type u_4
inst✝¹³ : Field K✝
inst✝¹² : Algebra R₁ K✝
inst✝¹¹ : IsFractionRing R₁ K✝
inst✝¹⁰ : IsDomain R₁
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
I : FractionalIdeal S⁰ L
⊢ Submodule.map ↑((semilinearEquivOfRingEquiv L K f.symm).trans (semilinearEquivOfRingEquiv K L f)) ↑I = ↑I
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
B : Type u_4
inst✝¹ : CommRing B
inst✝ : IsDedekindDomain B
L : Ideal B
f : R ⧸ I →+* A ⧸ J
g : A ⧸ J →+* B ⧸ L
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
x : { p // p ∣ I }
⊢ ((idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf)) x = (idealFactorsFunOfQuotHom ⋯) x

Tactic:
rw [idealFactorsFunOfQuotHom, idealFactorsFunOfQuotHom, OrderHom.comp_coe, OrderHom.coe_mk,
    OrderHom.coe_mk, Function.comp_apply, idealFactorsFunOfQuotHom, OrderHom.coe_mk,
    Subtype.mk_eq_mk, Subtype.coe_mk, map_comap_of_surjective (Ideal.Quotient.mk J)
    Ideal.Quotient.mk_surjective, map_map]

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

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ Prime (span {a})

Tactic:
prime_iff_isPrime

Goal state after:
case neg.refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ (span {a}).IsPrime

case neg.refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ span {a} ≠ ⊥
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
hf : Function.Surjective ⇑f
this : π.ker ≤ (l ∘ₗ π).ker
⊢ π.ker.FG

Tactic:
rw [← inf_eq_right.mpr this, ← Submodule.range_subtype (LinearMap.ker _),
    ← Submodule.map_comap_eq, ← LinearMap.ker_comp, e, LinearMap.ker_comp f,
    LinearMap.ker_eq_bot.mpr (Submodule.injective_subtype (LinearMap.ker l)), Submodule.comap_bot]

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := π.restrict ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
hf : Function.Surjective ⇑f
this : π.ker ≤ (l ∘ₗ π).ker
⊢ (Submodule.map (l ∘ₗ π).ker.subtype f.ker).FG
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
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this :
  ↑(Multiset.count (normalize (span {X})) (normalizedFactors (span {r}))) =
    ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ span {r} ≠ 0

pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Prime (span {X})

Tactic:
normalize_apply,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this :
  ↑(Multiset.count (span {X} * ↑(normUnit (span {X}))) (normalizedFactors (span {r}))) =
    ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ span {r} ≠ 0

R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Prime (span {X})
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₁
⊢ ∀ (r : (pres₂.cokernelRelations data).R),
    (Finsupp.linearCombination A fun g ↦ f.range.mkQ (pres₂.var g)) ((pres₂.cokernelRelations data).relation r) = 0

Tactic:
intro x
    erw [← Finsupp.apply_linearCombination]
    obtain (r | i) := x
    · erw [pres₂.linearCombination_var_relation]
      dsimp
    · erw [data.π_lift]
      simp

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R M'
this : IsLocalizedModule S LinearMap.id
r : R
hrp : r ∈ S
H : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) f)
hrp' : Submonoid.powers r ≤ S
x₁ x₂ : M
hx : f x₁ = f x₂
⊢ ((LocalizedModule.map (Submonoid.powers r)) f) ((LocalizedModule.mkLinearMap (Submonoid.powers r) M) x₁) =
    ((LocalizedModule.map (Submonoid.powers r)) f) ((LocalizedModule.mkLinearMap (Submonoid.powers r) M) x₂)

Tactic:
simp [hx]

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

Goal state before:
pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
a x : MvPolynomial Unit R
hx✝ : x ∈ MvPolynomial Unit R ∙ (C r * X () - 1)
hx : (aeval fun x ↦ invSelf r) x = 0
⊢ (aeval fun x ↦ invSelf r) (a • x) = 0

Tactic:
simp [hx]

Goal state after:
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
R' : Type ?u.16
S' : Type ?u.18
inst✝¹¹ : CommRing R'
inst✝¹⁰ : CommRing S'
inst✝⁹ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝⁸ : CommRing R''
inst✝⁷ : CommRing S''
inst✝⁶ : Algebra R'' S''
P'' : Extension R'' S''
R₁ : Type u_1
R₂ : Type u_2
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Algebra R₁ S
inst✝² : Algebra R₂ S
inst✝¹ : Algebra R₁ R₂
inst✝ : IsScalarTower R₁ R₂ S
r : R₁
s : R₂
m : P.Cotangent
⊢ (algebraMap R₂ S) ((algebraMap R₁ R₂) r) • (algebraMap R₂ S) s • m = (algebraMap R₁ S) r • (algebraMap R₂ S) s • m

Tactic:
← IsScalarTower.algebraMap_apply

Goal state after:
R : Type u
S : Type v
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝¹¹ : CommRing R'
inst✝¹⁰ : CommRing S'
inst✝⁹ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝⁸ : CommRing R''
inst✝⁷ : CommRing S''
inst✝⁶ : Algebra R'' S''
P'' : Extension R'' S''
R₁ : Type u_1
R₂ : Type u_2
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Algebra R₁ S
inst✝² : Algebra R₂ S
inst✝¹ : Algebra R₁ R₂
inst✝ : IsScalarTower R₁ R₂ S
r : R₁
s : R₂
m : P.Cotangent
⊢ (algebraMap R₁ S) r • (algebraMap R₂ S) s • m = (algebraMap R₁ S) r • (algebraMap R₂ S) s • m
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : f.toRingHom ↑x ∈ Ideal.map f.toRingHom P.ker ^ 2
⊢ mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))

Tactic:
← Ideal.map_pow,

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : f.toRingHom ↑x ∈ Ideal.map f.toRingHom (P.ker ^ 2)
⊢ mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))