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

Goal state before:
pp: case h.refine_2
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✝² : Nontrivial V
inst✝¹ : IsSolvable L
inst✝ : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := (toEnd k L V).range
toEndo : L →ₗ[k] ↥imL := LinearMap.codRestrict imL.toSubmodule ↑(toEnd k L V) ⋯
χ : Module.Dual k ↥imL
h : Nontrivial ↥(weightSpace V ⇑χ)
v : V
hv : v ∈ weightSpace V ⇑χ
hv0 : ⟨v, hv⟩ ≠ 0
⊢ ⟨v, ⋯⟩ ≠ 0

Tactic:
·

Goal state after:
case h.refine_2
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✝² : Nontrivial V
inst✝¹ : IsSolvable L
inst✝ : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := (toEnd k L V).range
toEndo : L →ₗ[k] ↥imL := LinearMap.codRestrict imL.toSubmodule ↑(toEnd k L V) ⋯
χ : Module.Dual k ↥imL
h : Nontrivial ↥(weightSpace V ⇑χ)
v : V
hv : v ∈ weightSpace V ⇑χ
hv0 : ⟨v, hv⟩ ≠ 0
⊢ ⟨v, ⋯⟩ ≠ 0
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
x✝ : ℕ
n : ℕ := x✝
h : ¬n < E.order
k : Fin E.order
⊢ n - E.order + ↑k < n

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case pos
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 : ℕ
h' : n < E.order
⊢ u n = init ⟨n, h'⟩

pp: case neg
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 : ℕ
h' : ¬n < E.order
⊢ u n =
    ∑ k,
      have x := ⋯;
      E.coeffs k * E.mkSol init (n - E.order + ↑k)

Tactic:
·

Goal state after:
case pos
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 : ℕ
h' : n < E.order
⊢ u n = init ⟨n, h'⟩
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case neg
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 : ℕ
h' : ¬n < E.order
⊢ u n =
    ∑ k,
      have x := ⋯;
      E.coeffs k * E.mkSol init (n - E.order + ↑k)

Tactic:
·

Goal state after:
case neg
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 : ℕ
h' : ¬n < E.order
⊢ u n =
    ∑ k,
      have x := ⋯;
      E.coeffs k * E.mkSol init (n - E.order + ↑k)
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ E.basis.repr ⟨u, hu⟩ = E.basis.repr ⟨v, hv⟩ → Set.EqOn u v ↑(range E.order)

pp: case mpr
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ Set.EqOn u v ↑(range E.order) → E.basis.repr ⟨u, hu⟩ = E.basis.repr ⟨v, hv⟩

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ E.basis.repr ⟨u, hu⟩ = E.basis.repr ⟨v, hv⟩ → Set.EqOn u v ↑(range E.order)
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ Set.EqOn u v ↑(range E.order) → E.basis.repr ⟨u, hu⟩ = E.basis.repr ⟨v, hv⟩

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ Set.EqOn u v ↑(range E.order) → E.basis.repr ⟨u, hu⟩ = E.basis.repr ⟨v, hv⟩
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun n ↦ q ^ n) → q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0

pp: case mpr
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0 → E.IsSolution fun n ↦ q ^ n

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun n ↦ q ^ n) → q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0 → E.IsSolution fun n ↦ q ^ n

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0 → E.IsSolution fun n ↦ q ^ n
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case pos
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
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : S.pairing δ γ = 0
⊢ rootSpace H ⇑↑((S.reflectionPerm γ) δ) ≤ LieSubmodule.restr I H

pp: case neg
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
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
⊢ rootSpace H ⇑↑((S.reflectionPerm γ) δ) ≤ LieSubmodule.restr I H

Tactic:
·

Goal state after:
case pos
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
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : S.pairing δ γ = 0
⊢ rootSpace H ⇑↑((S.reflectionPerm γ) δ) ≤ LieSubmodule.restr I H
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case neg
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
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
⊢ rootSpace H ⇑↑((S.reflectionPerm γ) δ) ≤ LieSubmodule.restr I H

Tactic:
·

Goal state after:
case neg
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
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
⊢ rootSpace H ⇑↑((S.reflectionPerm γ) δ) ≤ LieSubmodule.restr I H
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ (fun i ↦ p ^ ↑i) 1 = p

pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n✝ : ℕ
hn : n✝ ≠ 0
hp : Prime p
n m : Fin (n✝ + 1)
h : n < m
⊢ (fun i ↦ p ^ ↑i) n < (fun i ↦ p ^ ↑i) m

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, y = (fun i ↦ p ^ ↑i) i

pp: case refine_4
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
⊢ (∃ i, y = (fun i ↦ p ^ ↑i) i) → y ≤ p ^ n

Tactic:
·

Goal state after:
case refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ (fun i ↦ p ^ ↑i) 1 = p
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n✝ : ℕ
hn : n✝ ≠ 0
hp : Prime p
n m : Fin (n✝ + 1)
h : n < m
⊢ (fun i ↦ p ^ ↑i) n < (fun i ↦ p ^ ↑i) m

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, y = (fun i ↦ p ^ ↑i) i

pp: case refine_4
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
⊢ (∃ i, y = (fun i ↦ p ^ ↑i) i) → y ≤ p ^ n

Tactic:
·

Goal state after:
case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n✝ : ℕ
hn : n✝ ≠ 0
hp : Prime p
n m : Fin (n✝ + 1)
h : n < m
⊢ (fun i ↦ p ^ ↑i) n < (fun i ↦ p ^ ↑i) m
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, y = (fun i ↦ p ^ ↑i) i

pp: case refine_4
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
⊢ (∃ i, y = (fun i ↦ p ^ ↑i) i) → y ≤ p ^ n

Tactic:
·

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, y = (fun i ↦ p ^ ↑i) i
Module: Mathlib.RingTheory.ChainOfDivisors

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

Tactic:
·

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

Goal state before:
pp: case zero
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
hn : 0 ≠ 0
c : Fin (0 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
⊢ Irreducible (c 1)

pp: case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
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
⊢ Irreducible (c 1)

Tactic:
·

Goal state after:
case zero
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
hn : 0 ≠ 0
c : Fin (0 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
⊢ Irreducible (c 1)
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ.refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
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
⊢ c 1 ≠ ⊥

pp: case succ.refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
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
b : Associates M
hb : b < c 1
⊢ b = ⊥

Tactic:
·

Goal state after:
case succ.refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
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
⊢ c 1 ≠ ⊥
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ.refine_2.zero
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
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 : 0 < n + 1 + 1
hb : c ⟨0, hi⟩ < c 1
⊢ c ⟨0, hi⟩ = ⊥

pp: case succ.refine_2.succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
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
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
hb : c ⟨n✝ + 1, hi⟩ < c 1
⊢ c ⟨n✝ + 1, hi⟩ = ⊥

Tactic:
·

Goal state after:
case succ.refine_2.zero
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
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 : 0 < n + 1 + 1
hb : c ⟨0, hi⟩ < c 1
⊢ c ⟨0, hi⟩ = ⊥
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ.refine_2.succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
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
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
hb : c ⟨n✝ + 1, hi⟩ < c 1
⊢ c ⟨n✝ + 1, hi⟩ = ⊥

Tactic:
·

Goal state after:
case succ.refine_2.succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
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
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
hb : c ⟨n✝ + 1, hi⟩ < c 1
⊢ c ⟨n✝ + 1, hi⟩ = ⊥
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case zero
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q r : Associates M
hp : Prime p
hr : r ∣ q
hp' : p ∣ r
hn : 0 ≠ 0
c : Fin (0 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
⊢ p = c 1

pp: case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q r : Associates M
hp : Prime p
hr : r ∣ q
hp' : p ∣ r
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
⊢ p = c 1

Tactic:
·

Goal state after:
case zero
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q r : Associates M
hp : Prime p
hr : r ∣ q
hp' : p ∣ r
hn : 0 ≠ 0
c : Fin (0 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
⊢ p = c 1
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ.refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
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
i : Fin (n + 1 + 1)
hp : Prime (c i)
hp' : c i ∣ r
⊢ 1 ≤ i

pp: case succ.refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
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
i : Fin (n + 1 + 1)
hp : Prime (c i)
hp' : c i ∣ r
hi : 1 < i
⊢ False

Tactic:
·

Goal state after:
case succ.refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
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
i : Fin (n + 1 + 1)
hp : Prime (c i)
hp' : c i ∣ r
⊢ 1 ≤ i
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ.refine_2.inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
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
hp : Prime (c 0)
hp' : c 0 ∣ r
hi : 1 < 0
⊢ False

pp: case succ.refine_2.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
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
j : Fin (n + 1)
hp : Prime (c j.succ)
hp' : c j.succ ∣ r
hi : 1 < j.succ
⊢ False

Tactic:
·

Goal state after:
case succ.refine_2.inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
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
hp : Prime (c 0)
hp' : c 0 ∣ r
hi : 1 < 0
⊢ False
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ.refine_2.inr.refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
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
j : Fin (n + 1)
hp : Prime (c j.succ)
hp' : c j.succ ∣ r
hi : 1 < j.succ
⊢ 0 < j.castSucc

pp: case succ.refine_2.inr.refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
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
j : Fin (n + 1)
hp : Prime (c j.succ)
hp' : c j.succ ∣ r
hi : 1 < j.succ
⊢ DvdNotUnit (c j.castSucc) (c j.succ)

Tactic:
·

Goal state after:
case succ.refine_2.inr.refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
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
j : Fin (n + 1)
hp : Prime (c j.succ)
hp' : c j.succ ∣ r
hi : 1 < j.succ
⊢ 0 < j.castSucc
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ.refine_2.inr.refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
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
j : Fin (n + 1)
hp : Prime (c j.succ)
hp' : c j.succ ∣ r
hi : 1 < j.succ
⊢ DvdNotUnit (c j.castSucc) (c j.succ)

Tactic:
·

Goal state after:
case succ.refine_2.inr.refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
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
j : Fin (n + 1)
hp : Prime (c j.succ)
hp' : c j.succ ∣ r
hi : 1 < j.succ
⊢ DvdNotUnit (c j.castSucc) (c j.succ)
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case zero
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hn : 0 ≠ 0
c : Fin (0 + 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

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

Goal state after:
case zero
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hn : 0 ≠ 0
c : Fin (0 + 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
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case h
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : 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
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : (Finset.image (fun m ↦ c 1 ^ ↑m) Finset.univ).card = i + 1
a : Fin (i + 1)
left✝ : a ∈ Finset.univ
⊢ r = c 1 ^ i

pp: case h
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : 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
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : (Finset.image (fun m ↦ c 1 ^ ↑m) Finset.univ).card = i + 1
a : Fin (i + 1)
left✝ : a ∈ Finset.univ
⊢ ↑a ≤ i

Tactic:
·

Goal state after:
case h
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : 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
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : (Finset.image (fun m ↦ c 1 ^ ↑m) Finset.univ).card = i + 1
a : Fin (i + 1)
left✝ : a ∈ Finset.univ
⊢ r = c 1 ^ i
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case h
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : 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
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : (Finset.image (fun m ↦ c 1 ^ ↑m) Finset.univ).card = i + 1
a : Fin (i + 1)
left✝ : a ∈ Finset.univ
⊢ ↑a ≤ i

Tactic:
·

Goal state after:
case h
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : 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
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : (Finset.image (fun m ↦ c 1 ^ ↑m) Finset.univ).card = i + 1
a : Fin (i + 1)
left✝ : a ∈ Finset.univ
⊢ ↑a ≤ i