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
w : A
x : V
hx : x ∈ (⨆ k, U' k).carrier
⊢ ⁅w, x⁆ ∈ (⨆ k, U' k).carrier

Tactic:
by
      rw [show ⁅w, x⁆ = (T χ w) x + χ w • x by simp]
      apply add_mem _ (Submodule.smul_mem _ _ hx)
      set U := ⨆ k : ℕ, U' k
      suffices Submodule.map (T χ w) U ≤ U from this <| Submodule.mem_map_of_mem hx
      rw [Submodule.map_iSup, iSup_le_iff]
      rintro (_ | i)
      · simp [U']
      · exact (T_apply_succ w i).trans (le_iSup _ _)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ y ∈ p.toList x ↔ p.SameCycle x y ∧ x ∈ p.support

Tactic:
simp only [toList, mem_iterate, iterate_eq_pow, eq_comm (a := y)]
  constructor
  · rintro ⟨n, hx, rfl⟩
    refine ⟨⟨n, rfl⟩, ?_⟩
    contrapose! hx
    rw [← support_cycleOf_eq_nil_iff] at hx
    simp [hx]
  · rintro ⟨h, hx⟩
    simpa using h.exists_pow_eq_of_mem_support hx

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ ∃! s, (↑s).formPerm ⋯ = f

Tactic:
obtain ⟨s, ⟨hs, rfl⟩, hs'⟩ := hf.existsUnique_cycle
  refine ⟨⟨s, hs⟩, rfl, ?_⟩
  rintro ⟨t, ht⟩ ht'
  simpa using hs' _ ⟨ht, ht'⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
A : Array R
⊢ birdDet (k + 1) A = (-1) ^ k * (stepEntry (k + 1) A)^[k] (BirdDet.get (k + 1) A) 0 0

Tactic:
exact birdDet_succ k A

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i : Fin n
hEq1 : Eq1 A p
⊢ (-1) ^ (p + 1) * ∑ k > i, ∑ α ∈ S p k, bminor A k k α = (-1) ^ (p + 1) * ∑ α ∈ S (p + 1) i, pminor A α

Tactic:
rw [S_succ_eq_biUnion, Finset.sum_biUnion]
      · congrm (((-1) ^ (p + 1) * ∑ k ∈ Finset.Ioi i, ?_))
        symm
        exact Finset.sum_image fun _ _ _ _ hαβ => (Fin.cons_inj.mp hαβ).2
      · grind [Set.PairwiseDisjoint, Set.Pairwise, Finset.disjoint_left, Fin.cons_inj]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
α : Fin p → Fin n
k : Fin n
hnotmem :
  (α, k) ∉
    (fun x ↦
        match x with
        | (α, k) => (k.removeNth α, α k)) ''
      ↑(S (p + 1) i ×ˢ Finset.univ)
hα : α ∈ S p i
hk : i < k
hoccurs : k ∉ Set.range α
⊢ bminor A i (α, k).2 (α, k).1 * A (α, k).2 j = 0

Tactic:
contrapose hnotmem

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
α : Fin p → Fin n
k : Fin n
hα : α ∈ S p i
hk : i < k
hoccurs : k ∉ Set.range α
hnotmem : ¬bminor A i (α, k).2 (α, k).1 * A (α, k).2 j = 0
⊢ (α, k) ∈
    (fun x ↦
        match x with
        | (α, k) => (k.removeNth α, α k)) ''
      ↑(S (p + 1) i ×ˢ Finset.univ)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
⊢ A.det = Spec.birdDet A

Tactic:
by
  cases n with
  | zero => simp
  | succ k =>
    have : ∑ α ∈ S k 0, bminor A 0 0 α = A.det := by simp [bminor]
    rw [Spec.birdDetSpec_succ, paper_eq1, Matrix.of_apply, ← mul_assoc, ← pow_add]; aesop

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
⊢ ∀ (n : ℕ), u n = E.mkSol init n

Tactic:
intro n
  rw [mkSol]
  split_ifs with h'
  · exact mod_cast heq ⟨n, h'⟩
  · dsimp only
    rw [← tsub_add_cancel_of_le (le_of_not_gt h'), h (n - E.order)]
    congr with k
    rw [eq_mk_of_is_sol_of_eq_init h heq (n - E.order + k)]
    simp

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
β : ↥LieSubalgebra.root
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
⊢ (rootSystem H).root α ∈
    Submodule.comap (↑((rootSystem H).reflection β)) (Submodule.span K (⇑(rootSystem H).root '' I.rootSet))

Tactic:
Submodule.mem_comap,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
β : ↥LieSubalgebra.root
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
⊢ ↑((rootSystem H).reflection β) ((rootSystem H).root α) ∈ Submodule.span K (⇑(rootSystem H).root '' I.rootSet)
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_3
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
h : y ≤ p ^ n
i : ℕ
i_le : i ≤ n
hi : Associated y (p ^ i)
⊢ ∃ i, y = (fun i ↦ p ^ ↑i) i

Tactic:
associated_iff_eq

Goal state after:
case refine_3
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
h : y ≤ p ^ n
i : ℕ
i_le : i ≤ n
hi : y = p ^ i
⊢ ∃ i, y = (fun i ↦ p ^ ↑i) i
Module: Mathlib.RingTheory.ChainOfDivisors

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

Tactic:
obtain ⟨j, -, rfl⟩ := Finset.mem_image.1 hr

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
⊢ c j ∈ Finset.image (fun m ↦ c 1 ^ ↑m) Finset.univ
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✝ : IsCancelMulZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : u = 1
⊢ ↑(d ⟨u, hu'⟩) = 1

Tactic:
simp_rw [hu]
    conv_rhs => rw [← factor_orderIso_map_one_eq_bot d]
    rfl

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case neg.refine_1
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, ⋯⟩)
t u : Fin (s + 1)
h : t < u
⊢ ⟨c₁ t, ⋯⟩ < ⟨c₁ u, ⋯⟩

Tactic:
Subtype.mk_lt_mk,

Goal state after:
case neg.refine_1
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, ⋯⟩)
t u : Fin (s + 1)
h : t < u
⊢ c₁ t < c₁ u
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)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : Associated (↑(d ⟨p, ⋯⟩)) q
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

Tactic:
associated_iff_eq

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)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : ↑(d ⟨p, ⋯⟩) = q
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors 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ˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
this : Prime ↑(d ⟨p, ⋯⟩)
⊢ p ∈ normalizedFactors m

Tactic:
convert! hp

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ˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
⊢ ↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n

Tactic:
suffices
    Prime (d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by
            simp [dvd_of_mem_normalizedFactors hp]⟩ : N) by
    simp only [associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq,
      associatesEquivOfUniqueUnits_symm_apply] at this
    obtain ⟨q, hq, hq'⟩ :=
      exists_mem_normalizedFactors_of_dvd hn this.irreducible
        (d ⟨p, by apply dvd_of_mem_normalizedFactors; convert! hp⟩).prop
    rwa [associated_iff_eq.mp hq']

Goal state after:
M : Type u_1
inst✝⁶ : CommMonoidWithZero M
inst✝⁵ : IsCancelMulZero M
N : Type u_2
inst✝⁴ : CommMonoidWithZero N
inst✝³ : Subsingleton Mˣ
inst✝² : Subsingleton Nˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
⊢ Prime ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩)
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ˣ
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'
this✝ :
  Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) =
    ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
⊢ p ∈ normalizedFactors ?m.243

Tactic:
convert! hp

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

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

Tactic:
j

Goal state after:
case mp
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : A.IsSimplyLaced
i j : ι
⊢ j < i → A i j = 0 ∨ A i j = -1
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case mpr
ι : 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 : ι⦄, i ≠ j → (fun i j ↦ A i j = 0 ∨ A i j = -1) i j

Tactic:
j

Goal state after:
case mpr
ι : 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 : ι
⊢ i ≠ j → (fun i j ↦ A i j = 0 ∨ A i j = -1) i j
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i : Fin n
⊢ ∀ ⦃j : Fin n⦄, i ≠ j → (fun i j ↦ A n i j = 0 ∨ A n i j = -1) i j

Tactic:
j

Goal state after:
n : ℕ
i j : Fin n
⊢ i ≠ j → (fun i j ↦ A n i j = 0 ∨ A n i j = -1) i j
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i : Fin n
⊢ ∀ ⦃j : Fin n⦄, i ≠ j → (fun i j ↦ D n i j = 0 ∨ D n i j = -1) i j

Tactic:
j

Goal state after:
n : ℕ
i j : Fin n
⊢ i ≠ j → (fun i j ↦ D n i j = 0 ∨ D n i j = -1) i j
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case 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
⊢ LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : rootSpace H ⇑↑α ≤ LieSubmodule.restr I H), rootSpace H ⇑↑α ≤
    ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯

Tactic:
restr_inf_cartan_eq_biSup_corootSubmodule

Goal state after:
case 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 ↑α) ⊔ ⨆ α, ⨆ (_ : rootSpace H ⇑↑α ≤ LieSubmodule.restr I H), rootSpace H ⇑↑α ≤
    ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
⊢ genWeightSpace L ⇑↑α ≤ LieSubmodule.restr I H

Tactic:
exact hα

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

Goal state before:
pp: case h.left
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
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K) y' = aJ • y
⊢ aI * y' ∈ R₁⁰

Tactic:
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

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 : FractionalIdeal R₁⁰ K
h : J ≠ 0
x : K
⊢ x ∈ ⟨↑I / ↑J, ⋯⟩ ↔ ∀ y ∈ J, x * y ∈ I

Tactic:
exact Submodule.mem_div_iff_forall_mul_mem

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

Goal state before:
pp: case mpr
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x y : K
y_ne : y ≠ 0
y_mem : (algebraMap K L) y ∈ I
⊢ (algebraMap K L) x ∈ I

Tactic:
rw [← div_mul_cancel₀ x y_ne, map_mul, ← Algebra.smul_def]

Goal state after:
case mpr
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x y : K
y_ne : y ≠ 0
y_mem : (algebraMap K L) y ∈ I
⊢ (x / y) • (algebraMap K L) y ∈ I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

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

Tactic:
let := h.commGroupWithZero (K := FractionRing A)
  constructor
  rintro P P_ne hP
  refine Ideal.isMaximal_def.mpr ⟨hP.ne_top, fun M hM => ?_⟩
  -- We may assume `P` and `M` (as fractional ideals) are nonzero.
  have P'_ne : (P : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr P_ne
  have M'_ne : (M : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hM.ne_bot
  -- In particular, we'll show `M⁻¹ * P ≤ P`
  suffices (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ P by
    rw [eq_top_iff, ← coeIdeal_le_coeIdeal (FractionRing A), coeIdeal_top]
    calc
      (1 : FractionalIdeal A⁰ (FractionRing A)) = (↑M)⁻¹ * P * ((↑P)⁻¹ * M) := by
        simp [mul_assoc, *]
      _ ≤ P * ((↑P)⁻¹ * M) := by gcongr
      _ = M := by simp [*]
  -- Suppose we have `x ∈ M⁻¹ * P`, then in fact `x = algebraMap _ _ y` for some `y`.
  intro x hx
  have le_one : (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ 1 := by
    rw [← inv_mul_cancel₀ M'_ne]; gcongr
  obtain ⟨y, _hy, rfl⟩ := (mem_coeIdeal _).mp (le_one hx)
  -- Since `M` is strictly greater than `P`, let `z ∈ M \ P`.
  obtain ⟨z, hzM, hzp⟩ := SetLike.exists_of_lt hM
  -- We have `z * y ∈ M * (M⁻¹ * P) = P`.
  have zy_mem := mul_mem_mul (mem_coeIdeal_of_mem A⁰ hzM) hx
  rw [← map_mul, ← mul_assoc, mul_inv_cancel₀ M'_ne, one_mul] at zy_mem
  obtain ⟨zy, hzy, zy_eq⟩ := (mem_coeIdeal A⁰).mp zy_mem
  rw [IsFractionRing.injective A (FractionRing A) zy_eq] at hzy
  -- But `P` is a prime ideal, so `z ∉ P` implies `y ∈ P`, as desired.
  exact mem_coeIdeal_of_mem A⁰ (Or.resolve_left (hP.mem_or_mem hzy) hzp)

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

Goal state before:
pp: case h
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
H : Ideal A
hH : ↑H = (↑I)⁻¹ * ↑J
⊢ J = I * H

Tactic:
refine coeIdeal_injective (show (J : FractionalIdeal A⁰ (FractionRing A)) = ↑(I * H) from ?_)

Goal state after:
case h
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
H : Ideal A
hH : ↑H = (↑I)⁻¹ * ↑J
⊢ ↑J = ↑(I * H)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case inr
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
a : A
ha : a ≠ 0
⊢ Prime (span {a}) ↔ Prime a

Tactic:
have ha' : span {a} ≠ ⊥ := by simpa only [ne_eq, span_singleton_eq_bot] using ha

Goal state after:
case inr
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
a : A
ha : a ≠ 0
ha' : span {a} ≠ ⊥
⊢ Prime (span {a}) ↔ Prime a
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
K : Type u_2
inst✝⁷ : Field K
inst✝⁶ : Algebra R K
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : Module R V
inst✝² : IsScalarTower R K V
inst✝¹ : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst✝ : IsLattice K M
b : Basis κ R ↥M
hli : LinearIndependent K fun i ↦ ↑(b i)
⊢ ⊤ ≤ span K (Set.range fun i ↦ (⇑M.subtype ∘ ⇑b) i)

Tactic:
by
    rw [← Submodule.span_span_of_tower R, Set.range_comp, ← Submodule.map_span]
    simp [b.span_eq, Submodule.map_top, span_eq_top]

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

Goal state before:
pp: T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
⊢ (normalizedFactors (J ^ n) ∩ normalizedFactors I).prod = J ^ min n (count J (normalizedFactors I))

Tactic:
normalizedFactors_of_irreducible_pow hJ,

Goal state after:
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
⊢ (replicate n (normalize J) ∩ normalizedFactors I).prod = J ^ min n (count J (normalizedFactors I))
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ ↑s
⊢ ∀ ⦃y : ι⦄, y ∈ ↑s → i ≠ y → Function.onFun IsCoprime (fun i ↦ (f i).asIdeal ^ e i) i y

Tactic:
j

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ ↑s
j : ι
⊢ j ∈ ↑s → i ≠ j → Function.onFun IsCoprime (fun i ↦ (f i).asIdeal ^ e i) i j
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ ↑s
⊢ ∀ ⦃y : ι⦄, y ∈ ↑s → i ≠ y → Function.onFun IsCoprime (fun i ↦ f i ^ e i) i y

Tactic:
j

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ ↑s
j : ι
⊢ j ∈ ↑s → i ≠ j → Function.onFun IsCoprime (fun i ↦ f i ^ e i) i j
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case hsucc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ ¬a ^ (multiplicity a b + 1) ∣ b

Tactic:
· apply h.not_pow_dvd_of_multiplicity_lt
      apply lt_add_one

Goal state after: