mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x y : Derivation R A' A' × Derivation R A A
hx : x ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}
hy : y ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}
⊢ ⁅x, y⁆ ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}

Tactic:
by
    have hxx (a : A) := congrArg (fun f => f a) hx
    have hyy (a : A) := congrArg (fun f => f a) hy
    ext z
    simp at hxx hyy
    simp [Derivation.commutator_apply, hxx, hyy]

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

Goal state before:
pp: 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
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
v : ↥U := α • u + x'
z : L
z' : Q := (LieSubmodule.Quotient.mk' E) z
n : ℕ
⊢ ((toEnd K (↥U) Q) v ^ n) z' = (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z)

Tactic:
induction n with
    | zero => simp only [z', pow_zero, Module.End.one_apply]
    | succ n ih => rw [pow_succ', pow_succ', Module.End.mul_apply, ih]; rfl

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
h : ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
⊢ a ∈ twoCocycle R L M

Tactic:
ext x y z

Goal state after:
case mpr
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
h : ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
x y z : L
⊢ ((((d₂₃ R L M) a) x) y) z = ((0 x) y) z
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
h : m ∈ (coeff 1).support
⊢ f m = 0

Tactic:
rw [one_def] at h
    obtain rfl : m = 0 := Finset.mem_singleton.1 <| Finsupp.support_single_subset h
    apply map_zero

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i j : ι
a b : R[M]
ha : a ∈ gradeBy R (⇑f) i
hb : b ∈ gradeBy R (⇑f) j
c : M
hc : c ∈ (a * b).coeff.support
⊢ f c = i + j

Tactic:
by
    classical
    obtain ⟨ma, hma, mb, hmb, rfl⟩ : ∃ y ∈ a.coeff.support, ∃ z ∈ b.coeff.support, y + z = c :=
      Finset.mem_add.1 <| support_coeff_mul_subset a b hc
    rw [map_add, ha ma hma, hb mb hmb]

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

Goal state before:
pp: case of
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
x : ↥(decomposeTensor ℳ N i)
⊢ (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ))
      ((DirectSum.coeAddMonoidHom (decomposeTensor ℳ N)) ((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) x)) =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm
      ((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm ((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) x))

Tactic:
obtain ⟨-, y, rfl⟩ := x
    have : (rTensor N (lof R ι (fun i ↦ ℳ i) i)) y =
        (directSumLeft R R (fun i ↦ ℳ i) N).symm ((of (fun i ↦ ℳ i ⊗[R] N) i) y) :=
      (TensorProduct.directSumLeft_symm_of R R (M₁ := fun i ↦ ℳ i) y).symm
    rw [coeAddMonoidHom_of, LinearEquiv.eq_symm_apply, LinearEquiv.eq_symm_apply,
      ← (LinearEquiv.rTensor N _).coe_coe, LinearEquiv.coe_rTensor, ← rTensor_comp_apply,
      decomposeLinearEquiv_comp_subtype, this, LinearEquiv.apply_symm_apply,
      decomposeTensorEquiv_of_apply, decomposeTensorEquiv_apply]

Goal state after:
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
h : ∀ (x : L), (LinearMap.trace k M) ((toEnd k L M) x) = 0
this : finrank k M ≠ 0
⊢ HasTrivialRadical k L

Tactic:
obtain ⟨_i, h'⟩ := hasCentralRadical_and_of_isIrreducible_of_isFaithful k L M

Goal state after:
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
h : ∀ (x : L), (LinearMap.trace k M) ((toEnd k L M) x) = 0
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' : ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ k ∙ LinearMap.id
⊢ HasTrivialRadical k L
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
h : s.Nodup
⊢ s.reverse.formPerm ⋯ = (s.formPerm h)⁻¹

Tactic:
induction s using Quot.inductionOn
  simpa using formPerm_reverse _

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
y : M
z : E.L
x : M
hx : ↑E.incl x = Exists.choose ⋯ (E.proj z) - z
⊢ ⁅Exists.choose ⋯ (E.proj z) - z, E.incl y⁆ = ↑0

Tactic:
ZeroMemClass.coe_zero,

Goal state after:
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
y : M
z : E.L
x : M
hx : ↑E.incl x = Exists.choose ⋯ (E.proj z) - z
⊢ ⁅Exists.choose ⋯ (E.proj z) - z, E.incl y⁆ = 0
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
⊢ LieModule R L M

Tactic:
let := E.ringModuleOf
  set h := E.proj_surjective.hasRightInverse
  exact
    { smul_lie r x m := by
        rw [ringModuleOf_bracket, ringModuleOf_bracket, ← map_smul, ← smul_lie,
          EquivLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie]
        exact trivial_lie_zero E.proj.ker _ ⟨_, by simp [h.choose_spec _]⟩ (E.toKer m)
      lie_smul r x m := by simp }

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
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
⊢ ⟨(E.twoCocycleAux hs).compr₂ ↑E.toKer.symm.toLinearEquiv, ⋯⟩ ∈ twoCocycle R L M

Tactic:
ext x y z

Goal state after:
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
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y z : L
⊢ ((((d₂₃ R L M) ⟨(E.twoCocycleAux hs).compr₂ ↑E.toKer.symm.toLinearEquiv, ⋯⟩) x) y) z = ((0 x) y) z
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
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y z : L
hjac : ⁅s z, ⁅s x, s y⁆⁆ = -(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆)
hja : s ⁅z, ⁅x, y⁆⁆ = -s (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)
hj : s ⁅z, ⁅y, x⁆⁆ = -s (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆)
⊢ ⁅s x, ⁅s y, s z⁆⁆ - ⁅s x, s ⁅y, z⁆⁆ - (⁅s y, ⁅s x, s z⁆⁆ - ⁅s y, s ⁅x, z⁆⁆) +
            (-(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆) - ⁅s z, s ⁅x, y⁆⁆) -
          (⁅s ⁅x, y⁆, s z⁆ - (s ⁅x, ⁅y, z⁆⁆ - s ⁅y, ⁅x, z⁆⁆)) +
        (⁅s ⁅x, z⁆, s y⁆ - (s ⁅x, ⁅z, y⁆⁆ - s ⁅z, ⁅x, y⁆⁆)) -
      (⁅s ⁅y, z⁆, s x⁆ - (s ⁅y, ⁅z, x⁆⁆ - -s (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆))) =
    0

Tactic:
hja,

Goal state after:
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
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y z : L
hjac : ⁅s z, ⁅s x, s y⁆⁆ = -(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆)
hja : s ⁅z, ⁅x, y⁆⁆ = -s (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)
hj : s ⁅z, ⁅y, x⁆⁆ = -s (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆)
⊢ ⁅s x, ⁅s y, s z⁆⁆ - ⁅s x, s ⁅y, z⁆⁆ - (⁅s y, ⁅s x, s z⁆⁆ - ⁅s y, s ⁅x, z⁆⁆) +
            (-(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆) - ⁅s z, s ⁅x, y⁆⁆) -
          (⁅s ⁅x, y⁆, s z⁆ - (s ⁅x, ⁅y, z⁆⁆ - s ⁅y, ⁅x, z⁆⁆)) +
        (⁅s ⁅x, z⁆, s y⁆ - (s ⁅x, ⁅z, y⁆⁆ - -s (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆))) -
      (⁅s ⁅y, z⁆, s x⁆ - (s ⁅y, ⁅z, x⁆⁆ - -s (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆))) =
    0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case step
R : Type u_1
inst✝ : CommRing R
n : ℕ
f : ℕ → R
lo : ℕ
hlo : lo < n
ih : BirdDet.sumFrom n (lo + 1) f = ∑ k ∈ Finset.Ico (lo + 1) n, f k
⊢ f lo + BirdDet.sumFrom n (lo + 1) f = ∑ k ∈ Finset.Ico lo n, f k

Tactic:
ih,

Goal state after:
case step
R : Type u_1
inst✝ : CommRing R
n : ℕ
f : ℕ → R
lo : ℕ
hlo : lo < n
ih : BirdDet.sumFrom n (lo + 1) f = ∑ k ∈ Finset.Ico (lo + 1) n, f k
⊢ f lo + ∑ k ∈ Finset.Ico (lo + 1) n, f k = ∑ k ∈ Finset.Ico lo n, f k
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
hA : A.size = n * n
t : ℕ
ih :
  ∀ (i j : Fin n),
    (stepEntry n A)^[t] (BirdDet.get n A) ↑i ↑j =
      (Spec.stepEntry (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0))^[t] (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0) i j
i j : Fin n
⊢ (-∑ k > i, (stepEntry n A)^[t] (BirdDet.get n A) ↑k ↑k) * BirdDet.get n A ↑i ↑j +
      ∑ k > i, (stepEntry n A)^[t] (BirdDet.get n A) ↑i ↑k * BirdDet.get n A ↑k ↑j =
    Matrix.of
      (fun i j ↦
        (-∑ k > i,
                (Spec.stepEntry (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0))^[t]
                  (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0) k k) *
            Matrix.of (fun i j ↦ A.getD (n * ↑i + ↑j) 0) i j +
          ∑ k > i,
            (Spec.stepEntry (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0))^[t]
                (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0) i k *
              Matrix.of (fun i j ↦ A.getD (n * ↑i + ↑j) 0) k j)
      i j

Tactic:
ih,

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
hA : A.size = n * n
t : ℕ
ih :
  ∀ (i j : Fin n),
    (stepEntry n A)^[t] (BirdDet.get n A) ↑i ↑j =
      (Spec.stepEntry (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0))^[t] (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0) i j
i j : Fin n
⊢ (-∑ x > i,
            (Spec.stepEntry (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0))^[t]
              (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0) x x) *
        BirdDet.get n A ↑i ↑j +
      ∑ x > i,
        (Spec.stepEntry (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0))^[t] (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0) i
            x *
          BirdDet.get n A ↑x ↑j =
    Matrix.of
      (fun i j ↦
        (-∑ x > i,
                (Spec.stepEntry (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0))^[t]
                  (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0) x x) *
            Matrix.of (fun i j ↦ A.getD (n * ↑i + ↑j) 0) i j +
          ∑ k > i,
            (Spec.stepEntry (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0))^[t]
                (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0) i k *
              Matrix.of (fun i j ↦ A.getD (n * ↑i + ↑j) 0) k j)
      i j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case h.refine_1.refine_1
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin p
x : Fin (p + 1)
hjx : j.castSucc < x
h : k ≤ α j
⊢ ∃ i, k < α i ∧ i.castSucc < x

Tactic:
have k_ne (j : Fin p) : k ≠ α j := fun hj ↦ hk ⟨j, hj.symm⟩

Goal state after:
case h.refine_1.refine_1
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin p
x : Fin (p + 1)
hjx : j.castSucc < x
h : k ≤ α j
k_ne : ∀ (j : Fin p), k ≠ α j
⊢ ∃ i, k < α i ∧ i.castSucc < x
Module: Mathlib.RingTheory.ChainOfDivisors

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

Tactic:
rw [Finset.card_image_iff]

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

Goal state before:
pp: case neg.refine_3
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
⊢ (∃ i, r = c₂ i) → r ≤ ↑(d ⟨c₁ 1 ^ s, hs'⟩)

Tactic:
rintro ⟨i, hr⟩
    rw [hr, c₂_def, Subtype.coe_le_coe, d.le_iff_le]
    simpa [Subtype.mk_le_mk] using hc₁''.2 ⟨i, rfl⟩

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✝¹ : 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)
b : Associates N
this✝² : b ≤ n
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : ⊥ = ⟨b, this✝²⟩
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
this : x = ⊥
⊢ b = ⊥

Tactic:
refine (Subtype.mk_eq_bot_iff ?_ _).mp hx.symm

Goal state after:
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)
b : Associates N
this✝² : b ≤ n
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : ⊥ = ⟨b, this✝²⟩
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
this : x = ⊥
⊢ ⊥ ∈ Set.Iic n
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case mpr.inl
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1
i j : ι
hij✝ : i ≠ j
hij : i < j
⊢ A i j = 0 ∨ A i j = -1

pp: case mpr.inr
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1
i j : ι
hij✝ : i ≠ j
hij : j < i
⊢ A i j = 0 ∨ A i j = -1

Tactic:
· simpa only [hA.apply i j] using h hij

Goal state after:
case mpr.inr
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1
i j : ι
hij✝ : i ≠ j
hij : j < i
⊢ A i j = 0 ∨ A i j = -1
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case refine_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I✝ : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
y : A
h_Iy : y ∈ I
hy₀ : (algebraMap A K) y ∈ ↑I
c : A
hc : c * a = y * b
⊢ (algebraMap A K) (y * b) * ((algebraMap A K) a)⁻¹ ∈ 1

Tactic:
rw [← hc, map_mul, mul_assoc, mul_inv_cancel₀ hnz_fa, mul_one]

Goal state after:
case refine_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I✝ : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
y : A
h_Iy : y ∈ I
hy₀ : (algebraMap A K) y ∈ ↑I
c : A
hc : c * a = y * b
⊢ (algebraMap A K) c ∈ 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg
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
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ I ≤ I * (1 / I)

Tactic:
· rw [← coe_le_coe, coe_mul, coe_div hI_nz, coe_one]
    rw [← coe_le_coe, coe_one] at hI
    exact Submodule.le_self_mul_one_div hI

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

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
⊢ IsNoetherianRing A

Tactic:
let := h.commGroupWithZero (FractionRing A)
  refine isNoetherianRing_iff.mpr ⟨fun I : Ideal A => ?_⟩
  by_cases hI : I = ⊥
  · rw [hI]; apply Submodule.fg_bot
  have hI : (I : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hI
  exact I.fg_of_isUnit (IsFractionRing.injective A (FractionRing A)) hI.isUnit

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

Goal state before:
pp: case hI
R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ q ^ Multiset.count q P ≠ 0

Tactic:
apply pow_ne_zero

Goal state after:
case hI
R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := ⋯
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ q ≠ 0
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✝⁶ : IsLocalization S P
inst✝⁵ : IsDomain R₁
R : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : R
aI : Ideal R
ha : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑aI
this : I = spanSingleton R⁰ (((algebraMap R K) a)⁻¹ * (algebraMap R K) (generator aI))
⊢ ↑I = R ∙ ((algebraMap R K) a)⁻¹ * (algebraMap R K) (generator aI)

Tactic:
rw [spanSingleton] at this
    exact congr_arg Subtype.val this

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

Goal state before:
pp: case h
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
r : R
hr0 : ¬r = 0
x : K
hx : x ∈ I
r' : R
hr' : (algebraMap R K) r' = r • x
⊢ (algebraMap S L) (f r') = (IsFractionRing.ringEquivOfRingEquiv f) (r • x)

Tactic:
← hr',

Goal state after:
case h
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
r : R
hr0 : ¬r = 0
x : K
hx : x ∈ I
r' : R
hr' : (algebraMap R K) r' = r • x
⊢ (algebraMap S L) (f r') = (IsFractionRing.ringEquivOfRingEquiv f) ((algebraMap R K) r')
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Module A V
inst✝¹ : IsScalarTower R A V
a : Aˣ
s : Finset V
inst✝ : IsLattice A (span R ↑s)
⊢ (a • span R ↑s).FG

Tactic:
Submodule.smul_span

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Module A V
inst✝¹ : IsScalarTower R A V
a : Aˣ
s : Finset V
inst✝ : IsLattice A (span R ↑s)
⊢ (span R (a • ↑s)).FG
Module: Mathlib.RingTheory.Finiteness.Cofinite

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
S T : Submodule R M
hS : S.CoFG
hT : T.CoFG
⊢ (S.mkQ.ker ⊓ T.mkQ.ker).CoFG

Tactic:
← LinearMap.ker_prod

Goal state after:
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
S T : Submodule R M
hS : S.CoFG
hT : T.CoFG
⊢ (S.mkQ.prod T.mkQ).ker.CoFG