mathlib-initiative/mathlib-tactics huggingface dataset:
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
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
con3 : IsUnit (f Q).toBlocks₂₂
Y : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
Y_def : Y = fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
hY_symm : Y.IsSymm
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C)

Tactic:
set X := (f Vᵀ) * Y * (f V) with X_def

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
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
con3 : IsUnit (f Q).toBlocks₂₂
Y : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
Y_def : Y = fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
hY_symm : Y.IsSymm
X : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R := f Vᵀ * Y * f V
X_def : X = f Vᵀ * Y * f V
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C)
Module: Mathlib.Algebra.Lie.Free

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

Tactic:
simpa only [neg_one_smul] using h.smul (-1)

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
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y✝ : L
hy✝ : y✝ ∈ engel K x
Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩
y : L
hy : y ∈ engel K x
hyx : ⟨engel K y, ⋯⟩ ≤ Ex
⊢ finrank K ↥(engel K x) ≤ finrank K ↥(engel K y)

Tactic:
rw [(isRegular_iff_finrank_engel_eq_rank K x).mp hx]

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
y✝ : L
hy✝ : y✝ ∈ engel K x
Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩
y : L
hy : y ∈ engel K x
hyx : ⟨engel K y, ⋯⟩ ≤ Ex
⊢ rank K L ≤ finrank K ↥(engel K y)
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.attach.length
⊢ l.attach.formPerm.cycleType = {l.length}

Tactic:
rw [← nodup_attach] at hl

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ l.attach.formPerm.cycleType = {l.length}
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
E : Extension R M L
x : E.L
y : M
⊢ ⁅E.proj x, 0⁆ = 0

Tactic:
lie_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
E : Extension R M L
x : E.L
y : M
⊢ 0 = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
⊢ (fun x ↦ l₁.formPerm) ≍ fun x ↦ l₂.formPerm

Tactic:
apply Function.hfunext
    · ext
      exact h.nodup_iff
    · intro h₁ h₂ _
      exact heq_of_eq (formPerm_eq_of_isRotated h₁ h)

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : x ∉ p.support
⊢ (p.cycleOf x).support.card ≤ n

Tactic:
← support_cycleOf_eq_nil_iff

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : (p.cycleOf x).support = ∅
⊢ (p.cycleOf x).support.card ≤ n
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: case tmul.tmul
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
x : ↥(AddMonoidAlgebra.grade R i)
y : L
u : ↥(AddMonoidAlgebra.grade R j)
v : L
⊢ ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) (u ⊗ₜ[R] v)⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range

Tactic:
obtain ⟨x, hx⟩ := x
        obtain ⟨u, hu⟩ := u
        use ⟨x * u, SetLike.mul_mem_graded hx hu⟩ ⊗ₜ ⁅y, v⁆
        simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
⊢ l.formPerm.toList (l.get k) ~r l

Tactic:
have hr : l ~r l.rotate k := ⟨k, rfl⟩

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate ↑k
⊢ l.formPerm.toList (l.get k) ~r l
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
hy : ¬f.SameCycle x y
⊢ (f.toList x).formPerm y = (f.cycleOf x) y

Tactic:
rw [cycleOf_apply_of_not_sameCycle hy, formPerm_apply_of_notMem]

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
hy : ¬f.SameCycle x y
⊢ y ∉ f.toList x
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
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x : L
⊢ E.proj (s₁ x) - E.proj (s₂ x) = 0

Tactic:
sub_eq_zero,

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
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x : L
⊢ E.proj (s₁ x) = E.proj (s₂ x)
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
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ E.proj (s x) - E.proj (s' x) = 0

Tactic:
sub_eq_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
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ E.proj (s x) = E.proj (s' x)
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
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ E.proj (s' y) - E.proj (s y) = 0

Tactic:
sub_eq_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
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
s' : L → E.L
h : LeftInverse (⇑E.proj) s'
⊢ E.proj (s' y) = E.proj (s y)
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 ⋯, ⋯⟩
⊢ Function.Bijective f

Tactic:
Function.bijective_iff_existsUnique

Goal state after:
α : 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
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case h.refine_1.refine_2
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
h : ∀ (b : Fin (p + 1)), j.castSucc < b → ∃ i, k < α i ∧ i.castSucc < b
⊢ k < α j

Tactic:
obtain ⟨q, hkq, hqj⟩ := h j.succ j.castSucc_lt_succ

Goal state after:
case h.refine_1.refine_2
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
h : ∀ (b : Fin (p + 1)), j.castSucc < b → ∃ i, k < α i ∧ i.castSucc < b
q : Fin p
hkq : k < α q
hqj : q.castSucc < j.succ
⊢ k < α j
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 : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ L₁' = L₂'

Tactic:
← coe_set_eq

Goal state after:
A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L₁' L₂' : LieRinehartSubalgebra A L
h : ↑L₁'.toSubmodule = ↑L₂'.toSubmodule
⊢ ↑L₁' = ↑L₂'
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
inst✝⁵ : LieRingModule L A
inst✝⁴ : LieRinehartRing A L
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R A
inst✝¹ : LieAlgebra R L
inst✝ : LieRinehartAlgebra R A L
L₁' L₂' : LieRinehartSubalgebra A L
h : ↑((fun L' ↦ L'.toLieSubalgebra R) L₁') = ↑((fun L' ↦ L'.toLieSubalgebra R) L₂')
⊢ L₁' = L₂'

Tactic:
← coe_set_eq

Goal state after:
A : Type u_1
L : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : LieRing L
inst✝⁶ : Module A L
inst✝⁵ : LieRingModule L A
inst✝⁴ : LieRinehartRing A L
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R A
inst✝¹ : LieAlgebra R L
inst✝ : LieRinehartAlgebra R A L
L₁' L₂' : LieRinehartSubalgebra A L
h : ↑((fun L' ↦ L'.toLieSubalgebra R) L₁') = ↑((fun L' ↦ L'.toLieSubalgebra R) L₂')
⊢ ↑L₁' = ↑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
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
μ : ↥LieSubalgebra.root
hμ : μ ∈ I.rootSet
⊢ ↑span_compl_roots = ⨆ β, ⨆ (_ : β ∉ I.rootSet), ↑(f β)

Tactic:
span_compl_roots,

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
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
μ : ↥LieSubalgebra.root
hμ : μ ∈ I.rootSet
⊢ ↑(⨆ β, ⨆ (_ : β ∉ I.rootSet), f β) = ⨆ β, ⨆ (_ : β ∉ I.rootSet), ↑(f β)
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'
x✝ : ↑(Set.Iic (Associates.mk m))
l : Associates M
hl : l ∈ Set.Iic (Associates.mk m)
⊢ (fun l ↦ ⟨Associates.mk ↑(d.symm ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩)
      ((fun l ↦ ⟨Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩) ⟨l, hl⟩) =
    ⟨l, hl⟩

Tactic:
simp only [Subtype.coe_eta, Equiv.symm_apply_apply, Subtype.coe_mk,
      associatesEquivOfUniqueUnits_apply, mk_out, out_mk, normalize_eq]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case a.a
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
⊢ ⨆ α ∈ I.rootSet, corootSubmodule ↑α ≤ ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯

Tactic:
exact iSup₂_le fun β hβ ↦ le_iSup₂_of_le β hβ
        (by rw [sl2SubmoduleOfRoot_eq_sup]; exact le_sup_right)

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥R⁰
x : R
hx : (algebraMap R K) x = ↑z • y
⊢ ↑z • y ∈ I

Tactic:
exact smul_mem _ _ y_mem

Goal state after:
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 : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
⊢ IsFractional R₁⁰ (I / J)

Tactic:
by
    obtain ⟨y, mem_J, notMem_zero⟩ :=
      SetLike.exists_of_lt (show 0 < J by simpa only using! bot_lt_iff_ne_bot.mpr h)
    obtain ⟨y', hy'⟩ := hJ y mem_J
    use aI * y'
    constructor
    · apply (nonZeroDivisors R₁).mul_mem haI (mem_nonZeroDivisors_iff_ne_zero.mpr _)
      intro y'_eq_zero
      have : algebraMap R₁ K aJ * y = 0 := by
        rw [← Algebra.smul_def, ← hy', y'_eq_zero, map_zero]
      have y_zero :=
        (mul_eq_zero.mp this).resolve_left
          (mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).1 (IsFractionRing.injective _ _) _)
            (mem_nonZeroDivisors_iff_ne_zero.mp haJ))
      apply notMem_zero
      simpa
    intro b hb
    convert! hI _ (hb _ (Submodule.smul_mem _ aJ mem_J)) using 1
    rw [← hy', mul_comm b, ← Algebra.smul_def, mul_smul]

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

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
⊢ IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1

Tactic:
let h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K :=
    FractionalIdeal.mapEquiv (FractionRing.algEquiv A K)
  refine h.toEquiv.forall_congr (fun {x} => ?_)
  rw [← h.toEquiv.apply_eq_iff_eq]
  simp [h]

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
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
x : FractionRing A
hx : x ∈ (↑M)⁻¹ * ↑P
⊢ (↑M)⁻¹ * ↑P ≤ 1

Tactic:
rw [← inv_mul_cancel₀ M'_ne]

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
x : FractionRing A
hx : x ∈ (↑M)⁻¹ * ↑P
⊢ (↑M)⁻¹ * ↑P ≤ (↑M)⁻¹ * ↑M
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
⊢ (decomposeAddEquiv 𝓜).toAddHom.toFun (x • y) = (RingHom.id A) x • (decomposeAddEquiv 𝓜).toAddHom.toFun y

Tactic:
AddHom.toFun_eq_coe,

Goal state after:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
⊢ (decomposeAddEquiv 𝓜).toAddHom (x • y) = (RingHom.id A) x • (decomposeAddEquiv 𝓜).toAddHom y
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case h.left
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
p : Ideal T
hpi : p ∈ filter (fun x ↦ ¬P = x) (normalizedFactors I)
hp : Prime p
⊢ P ⊔ p = ⊤

Tactic:
exact hpm.coprime_of_ne ((isPrime_of_prime hp).isMaximal hp.ne_zero) (of_mem_filter hpi)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
t : Finset M
ht : Submodule.span R ↑t = l.ker
⊢ (linearCombination R Subtype.val).range = ⊤

Tactic:
rw [range_linearCombination, Subtype.range_val, ← hs]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : AddCommGroup N
k : Type u_3
inst✝⁸ : DivisionRing k
inst✝⁷ : Module k M
inst✝⁶ : Module k N
f : M →ₗ[k] N
P : Type u_4
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module k P
g : N →ₗ[k] P
inst✝³ : FiniteDimensional k ↥f.ker
inst✝² : FiniteDimensional k ↥g.ker
inst✝¹ : FiniteDimensional k (N ⧸ f.range)
inst✝ : FiniteDimensional k (P ⧸ g.range)
aux : f.range ≤ comap g (g ∘ₗ f).range
f₀ : ↥f.ker →ₗ[k] ↥(g ∘ₗ f).ker := inclusion ⋯
f₁ : ↥(g ∘ₗ f).ker →ₗ[k] ↥g.ker := f.restrict ⋯
f₂ : ↥g.ker →ₗ[k] N ⧸ f.range := f.range.mkQ ∘ₗ g.ker.subtype
f₃ : N ⧸ f.range →ₗ[k] P ⧸ (g ∘ₗ f).range := f.range.mapQ (g ∘ₗ f).range g aux
f₄ : P ⧸ (g ∘ₗ f).range →ₗ[k] P ⧸ g.range := factor ⋯
h₀ : Injective ⇑f₀
h₁ : Exact ⇑f₀ ⇑f₁
h₂ : Exact ⇑f₁ ⇑f₂
h₃ : Exact ⇑f₂ ⇑f₃
⊢ (g ∘ₗ f).index = g.index + f.index

Tactic:
have h₄ : Exact f₃ f₄ := by rw [exact_iff]; simp [f₃, f₄, factor, ker_mapQ, range_mapQ]

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : AddCommGroup N
k : Type u_3
inst✝⁸ : DivisionRing k
inst✝⁷ : Module k M
inst✝⁶ : Module k N
f : M →ₗ[k] N
P : Type u_4
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module k P
g : N →ₗ[k] P
inst✝³ : FiniteDimensional k ↥f.ker
inst✝² : FiniteDimensional k ↥g.ker
inst✝¹ : FiniteDimensional k (N ⧸ f.range)
inst✝ : FiniteDimensional k (P ⧸ g.range)
aux : f.range ≤ comap g (g ∘ₗ f).range
f₀ : ↥f.ker →ₗ[k] ↥(g ∘ₗ f).ker := inclusion ⋯
f₁ : ↥(g ∘ₗ f).ker →ₗ[k] ↥g.ker := f.restrict ⋯
f₂ : ↥g.ker →ₗ[k] N ⧸ f.range := f.range.mkQ ∘ₗ g.ker.subtype
f₃ : N ⧸ f.range →ₗ[k] P ⧸ (g ∘ₗ f).range := f.range.mapQ (g ∘ₗ f).range g aux
f₄ : P ⧸ (g ∘ₗ f).range →ₗ[k] P ⧸ g.range := factor ⋯
h₀ : Injective ⇑f₀
h₁ : Exact ⇑f₀ ⇑f₁
h₂ : Exact ⇑f₁ ⇑f₂
h₃ : Exact ⇑f₂ ⇑f₃
h₄ : Exact ⇑f₃ ⇑f₄
⊢ (g ∘ₗ f).index = g.index + f.index
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
⊢ (linearCombination R Subtype.val).range = ⊤

Tactic:
rw [range_linearCombination, Subtype.range_val, ← hs]

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a x : R
hx : Prime x
n : ℕ
q : R
hq : a = x ^ n * q
q' : R
hq' : q = x * q'
⊢ a = x ^ (n + 1) * q'

Tactic:
hq,

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
a x : R
hx : Prime x
n : ℕ
q : R
hq : a = x ^ n * q
q' : R
hq' : q = x * q'
⊢ x ^ n * q = x ^ (n + 1) * q'
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
⊢ π.range = ⊤

Tactic:
rw [range_linearCombination, Subtype.range_val, ← hs]

Goal state after: