mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case inr.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
g : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
    f ≠ 0 ∧ g ≠ 0 → m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
⊢ m.toSyn (m.degree (m.sPolynomial 0 g)) ≤ m.toSyn (m.degree 0 ⊔ m.degree g)

pp: case inr.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
    f ≠ 0 ∧ g ≠ 0 → m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
⊢ m.toSyn (m.degree (m.sPolynomial f 0)) ≤ m.toSyn (m.degree f ⊔ m.degree 0)

Tactic:
<;>

Goal state after:
case inr.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
g : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
    f ≠ 0 ∧ g ≠ 0 → m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
⊢ m.toSyn (m.degree (m.sPolynomial 0 g)) ≤ m.toSyn (m.degree 0 ⊔ m.degree g)

case inr.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
    f ≠ 0 ∧ g ≠ 0 → m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
⊢ m.toSyn (m.degree (m.sPolynomial f 0)) ≤ m.toSyn (m.degree f ⊔ m.degree 0)
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
kpos : 0 < 0
⊢ f x ^ 0 * f x = ((f.ppow 0).pmul f) x

pp: case succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
a✝ : ∀ {kpos : 0 < n✝}, f x ^ n✝ * f x = ((f.ppow n✝).pmul f) x
kpos : 0 < n✝ + 1
⊢ f x ^ (n✝ + 1) * f x = ((f.ppow (n✝ + 1)).pmul f) x

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
kpos : 0 < 0
⊢ f x ^ 0 * f x = ((f.ppow 0).pmul f) x

case succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
a✝ : ∀ {kpos : 0 < n✝}, f x ^ n✝ * f x = ((f.ppow n✝).pmul f) x
kpos : 0 < n✝ + 1
⊢ f x ^ (n✝ + 1) * f x = ((f.ppow (n✝ + 1)).pmul f) x
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: case zero
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
⊢ (f.pdiv ↑ζ) 0 = f 0

pp: case succ
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
n✝ : ℕ
⊢ (f.pdiv ↑ζ) (n✝ + 1) = f (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
⊢ (f.pdiv ↑ζ) 0 = f 0

case succ
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
n✝ : ℕ
⊢ (f.pdiv ↑ζ) (n✝ + 1) = f (n✝ + 1)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case refine_2.refine_1
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 ∣ b ^ 2 * a

pp: case refine_2.refine_2
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 ∣ b ^ 2 * a

Tactic:
<;>

Goal state after:
case refine_2.refine_1
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 ∣ b ^ 2 * a

case refine_2.refine_2
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 ∣ b ^ 2 * a
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
⊢ n.factorization = Finsupp.single p k

Tactic:
rw [← hn, Nat.Prime.factorization_pow hp]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case h
n : ℕ
S : Finset ℕ := ⋯
hSne : S.Nonempty
s : ℕ := ⋯
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * a = (b * x) ^ 2 * y

pp: case h
n : ℕ
S : Finset ℕ := ⋯
hSne : S.Nonempty
s : ℕ := ⋯
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * a = (b * x) ^ 2 * y

Tactic:
<;>

Goal state after:
case h
n : ℕ
S : Finset ℕ := ⋯
hSne : S.Nonempty
s : ℕ := ⋯
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * a = (b * x) ^ 2 * y

case h
n : ℕ
S : Finset ℕ := ⋯
hSne : S.Nonempty
s : ℕ := ⋯
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * a = (b * x) ^ 2 * y
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ ¬IsPrimePow n ↔ n.primeFactors.Nontrivial

Tactic:
isPrimePow_iff_card_primeFactors_eq_one,

Goal state after:
n : ℕ
hn : 2 ≤ n
⊢ ¬n.primeFactors.card = 1 ↔ n.primeFactors.Nontrivial
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case h
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * (x * x * y) = (b * x) ^ 2 * y

pp: case h
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * (x * x * y) = (b * x) ^ 2 * y

Tactic:
<;>

Goal state after:
case h
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * (x * x * y) = (b * x) ^ 2 * y

case h
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * (x * x * y) = (b * x) ^ 2 * y
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case refine_1
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : b₁ ^ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ (b₁.pred + 1) ^ 2 * (a₁.pred + 1) = n

pp: case refine_2
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : b₁ ^ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ Squarefree (a₁.pred + 1)

Tactic:
<;>

Goal state after:
case refine_1
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : b₁ ^ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ (b₁.pred + 1) ^ 2 * (a₁.pred + 1) = n

case refine_2
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : b₁ ^ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ Squarefree (a₁.pred + 1)
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case inr.inr.inl
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
h : a.factorization p = 0
⊢ k ≤ a.factorization p + b.factorization p → k ≤ a.factorization p ∨ k ≤ b.factorization p

pp: case inr.inr.inr
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
h : b.factorization p = 0
⊢ k ≤ a.factorization p + b.factorization p → k ≤ a.factorization p ∨ k ≤ b.factorization p

Tactic:
<;>

Goal state after:
case inr.inr.inl
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
h : a.factorization p = 0
⊢ k ≤ a.factorization p + b.factorization p → k ≤ a.factorization p ∨ k ≤ b.factorization p

case inr.inr.inr
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
h : b.factorization p = 0
⊢ k ≤ a.factorization p + b.factorization p → k ≤ a.factorization p ∨ k ≤ b.factorization p
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case zero
n : ℕ
⊢ (pow 0) n = if 0 = 0 ∧ n = 0 then 0 else n ^ 0

pp: case succ
n n✝ : ℕ
⊢ (pow (n✝ + 1)) n = if n✝ + 1 = 0 ∧ n = 0 then 0 else n ^ (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
n : ℕ
⊢ (pow 0) n = if 0 = 0 ∧ n = 0 then 0 else n ^ 0

case succ
n n✝ : ℕ
⊢ (pow (n✝ + 1)) n = if n✝ + 1 = 0 ∧ n = 0 then 0 else n ^ (n✝ + 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case pos.zero
m : ℕ
hm : m = 0
⊢ Ω (m ^ 0) = 0 * Ω m

pp: case pos.succ
m : ℕ
hm : m = 0
n✝ : ℕ
⊢ Ω (m ^ (n✝ + 1)) = (n✝ + 1) * Ω m

Tactic:
<;>

Goal state after:
case pos.zero
m : ℕ
hm : m = 0
⊢ Ω (m ^ 0) = 0 * Ω m

case pos.succ
m : ℕ
hm : m = 0
n✝ : ℕ
⊢ Ω (m ^ (n✝ + 1)) = (n✝ + 1) * Ω m
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case mp
n : ℕ
h0 : n ≠ 0
⊢ n.primeFactorsList.dedup.length = Ω n → n.primeFactorsList.Nodup

pp: case mpr
n : ℕ
h0 : n ≠ 0
⊢ n.primeFactorsList.Nodup → n.primeFactorsList.dedup.length = Ω n

Tactic:
<;>

Goal state after:
case mp
n : ℕ
h0 : n ≠ 0
⊢ n.primeFactorsList.dedup.length = Ω n → n.primeFactorsList.Nodup

case mpr
n : ℕ
h0 : n ≠ 0
⊢ n.primeFactorsList.Nodup → n.primeFactorsList.dedup.length = Ω n
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ n.primeFactorsList.dedup.length = 1 ↔ IsPrimePow n

Tactic:
isPrimePow_iff_card_primeFactors_eq_one,

Goal state after:
n : ℕ
⊢ n.primeFactorsList.dedup.length = 1 ↔ #n.primeFactors = 1
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h.h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ∏ p ∈ n.primeFactors.attach with f ↑p ⋯ = f p hp, ↑p ∈ {x | p ∣ x}

pp: case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ∏ p ∈ n.primeFactors.attach with g ↑p ⋯ = f p hp, ↑p ∉ {x | p ∣ x}

Tactic:
<;>

Goal state after:
case h.h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ∏ p ∈ n.primeFactors.attach with f ↑p ⋯ = f p hp, ↑p ∈ {x | p ∣ x}

case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ∏ p ∈ n.primeFactors.attach with g ↑p ⋯ = f p hp, ↑p ∉ {x | p ∣ x}
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case refine_1
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (f a ha).1 ∣ n

pp: case refine_2
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (f a ha).2 ∣ n

pp: case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ match f a ha with
  | (x, y) => x.lcm y = n

Tactic:
<;>

Goal state after:
case refine_1
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (f a ha).1 ∣ n

case refine_2
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (f a ha).2 ∣ n

case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ match f a ha with
  | (x, y) => x.lcm y = n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case «0»
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
⊢ a ((fun i ↦ i) ⟨0, ⋯⟩) = b ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
⊢ a ((fun i ↦ i) ⟨1, ⋯⟩) = b ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2»
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
⊢ a ((fun i ↦ i) ⟨2, ⋯⟩) = b ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
⊢ a ((fun i ↦ i) ⟨0, ⋯⟩) = b ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
⊢ a ((fun i ↦ i) ⟨1, ⋯⟩) = b ((fun i ↦ i) ⟨1, ⋯⟩)

case «2»
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
⊢ a ((fun i ↦ i) ⟨2, ⋯⟩) = b ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h.fst
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := ⋯
a : Fin (succ 0).succ.succ → ℕ := ⋯
ha : a ∈ finMulAntidiag 3 n
⊢ (f a ha).1 = b.1

pp: case h.snd
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := ⋯
a : Fin (succ 0).succ.succ → ℕ := ⋯
ha : a ∈ finMulAntidiag 3 n
⊢ (f a ha).2 = b.2

Tactic:
<;>

Goal state after:
case h.fst
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := ⋯
a : Fin (succ 0).succ.succ → ℕ := ⋯
ha : a ∈ finMulAntidiag 3 n
⊢ (f a ha).1 = b.1

case h.snd
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := ⋯
a : Fin (succ 0).succ.succ → ℕ := ⋯
ha : a ∈ finMulAntidiag 3 n
⊢ (f a ha).2 = b.2
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h.fst
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiag 3 n
⊢ g * (b.1 / g) = b.1

pp: case h.snd
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiag 3 n
⊢ g * (b.2 / g) = b.2

Tactic:
<;>

Goal state after:
case h.fst
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiag 3 n
⊢ g * (b.1 / g) = b.1

case h.snd
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiag 3 n
⊢ g * (b.2 / g) = b.2
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
⊢ hs.toFinset ⊆ Finset.range n

pp: case refine_2
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
⊢ ∀ x ∈ Finset.range n, x ∉ hs.toFinset → s.indicator (fun x ↦ a) x = 0

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
⊢ hs.toFinset ⊆ Finset.range n

case refine_2
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
⊢ ∀ x ∈ Finset.range n, x ∉ hs.toFinset → s.indicator (fun x ↦ a) x = 0
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ hs.toFinset → x ∈ Finset.range n

pp: case refine_2
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ Finset.range n → x ∉ hs.toFinset → s.indicator (fun x ↦ a) x = 0

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ hs.toFinset → x ∈ Finset.range n

case refine_2
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ Finset.range n → x ∉ hs.toFinset → s.indicator (fun x ↦ a) x = 0
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : q ∈ {t | ↑t < a + b}
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
⊢ cutMap β a + cutMap β b ⊆ Rat.cast '' {t | ↑t < a + b}

Tactic:
· rw [mem_ofPred_eq, ← sub_lt_iff_lt_add] at hq
    obtain ⟨q₁, hq₁q, hq₁ab⟩ := exists_rat_btwn hq
    refine ⟨q₁, by rwa [coe_mem_cutMap_iff], q - q₁, ?_, add_sub_cancel _ _⟩
    norm_cast
    rw [coe_mem_cutMap_iff]
    exact mod_cast sub_lt_comm.mp hq₁q

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
⊢ cutMap β a + cutMap β b ⊆ Rat.cast '' {t | ↑t < a + b}
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case e_a.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h✝ :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
h : m.degree (g b') = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b'))
⊢ coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')

pp: case e_a.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h✝ :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
h : g b' = 0
⊢ coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')

Tactic:
<;>

Goal state after:
case e_a.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h✝ :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
h : m.degree (g b') = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b'))
⊢ coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')

case e_a.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h✝ :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
h : g b' = 0
⊢ coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')