mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (a1 * a2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (a1 * a2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
⊢ ∏ x ∈ n.primeFactors, x = n

pp: case h
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
⊢ ∀ i ∈ n.primeFactors.attach, f ↑i ⋯ ∈ univ

Tactic:
·

Goal state after:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
⊢ ∏ x ∈ n.primeFactors, x = n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
⊢ ∀ i ∈ n.primeFactors.attach, f ↑i ⋯ ∈ univ

Tactic:
·

Goal state after:
case h
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
⊢ ∀ i ∈ n.primeFactors.attach, f ↑i ⋯ ∈ univ
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
hm1 : ¬(monomial d₁) c₁ = 0
⊢ (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₁) c₁ * p₁)))
          (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
        ((monomial d₁) c₁ * p₁) -
      (monomial
            (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₂) c₂ * p₂)))
          (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
        ((monomial d₂) c₂ * p₂) =
    (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) *
      ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
        (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)

Tactic:
have hm2 := (monomial_eq_zero (s := d₂)).not.mpr hc2

Goal state after:
σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
hm1 : ¬(monomial d₁) c₁ = 0
hm2 : ¬(monomial d₂) c₂ = 0
⊢ (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₁) c₁ * p₁)))
          (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
        ((monomial d₁) c₁ * p₁) -
      (monomial
            (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₂) c₂ * p₂)))
          (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
        ((monomial d₂) c₂ * p₂) =
    (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) *
      ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
        (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)
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 ∣ ∏ p ∈ n.primeFactors.attach with f ↑p ⋯ = f p hp, ↑p

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 ∣ ∏ p ∈ n.primeFactors.attach with g ↑p ⋯ = f p hp, ↑p

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 ∣ ∏ p ∈ n.primeFactors.attach with f ↑p ⋯ = f p hp, ↑p
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
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 ∣ ∏ p ∈ n.primeFactors.attach with g ↑p ⋯ = f p hp, ↑p

Tactic:
·

Goal state after:
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 ∣ ∏ p ∈ n.primeFactors.attach with g ↑p ⋯ = f p hp, ↑p
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case refine_1
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
⊢ f ∈ n.primeFactors.pi fun x ↦ univ

pp: case refine_2
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
⊢ d.primeFactorsPiBij n f ?refine_1 = t

Tactic:
·

Goal state after:
case refine_1
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
⊢ f ∈ n.primeFactors.pi fun x ↦ univ
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ d.primeFactorsPiBij n f ⋯ i = ∏ p ∈ n.primeFactors.attach, if ↑p ∣ t i then ↑p else 1

pp: d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ (∏ p ∈ n.primeFactors.attach, if ↑p ∣ t i then ↑p else 1) = t i

Tactic:
·

Goal state after:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ d.primeFactorsPiBij n f ⋯ i = ∏ p ∈ n.primeFactors.attach, if ↑p ∣ t i then ↑p else 1
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
⊢ (a 0 * a 1, a 0 * a 2).1 ∣ a 0 * a 1 * a 2

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

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

Tactic:
·

Goal state after:
case refine_1
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 0 * a 1, a 0 * a 2).1 ∣ a 0 * a 1 * a 2
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case refine_2
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 0 * a 1, a 0 * a 2).2 ∣ a 0 * a 1 * a 2

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

Tactic:
·

Goal state after:
case refine_2
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 0 * a 1, a 0 * a 2).2 ∣ a 0 * a 1 * a 2
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * (a 1 * a 2) = a 0 * a 1 * a 2

pp: case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 1).Coprime (a 2)

Tactic:
·

Goal state after:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * (a 1 * a 2) = a 0 * a 1 * a 2
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).1.2 = (a1 * a2).gcd (a2 * b2)

pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (a1 * a2).gcd (a2 * b2) = ((c1, c2), d1, d2).1.2

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).1.2 = (a1 * a2).gcd (a2 * b2)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i, a i = n

Tactic:
·

Goal state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i, a i = n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (a1 * a2).gcd (a2 * b2) = ((c1, c2), d1, d2).1.2

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (a1 * a2).gcd (a2 * b2) = ((c1, c2), d1, d2).1.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
⊢ 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 : ℕ := ⋯
a : Fin (succ 0).succ.succ → ℕ := ⋯
ha : a ∈ finMulAntidiag 3 n
⊢ 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 : ℕ := ⋯
a : Fin (succ 0).succ.succ → ℕ := ⋯
ha : a ∈ finMulAntidiag 3 n
⊢ g ∣ b.1
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
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
⊢ g ∣ b.2

Tactic:
·

Goal state after:
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
⊢ g ∣ b.2
Module: Mathlib.Algebra.Order.Archimedean.Hom

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : f x ≠ g x
h₂ :
  ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : Field β] [inst_3 : LinearOrder β]
    [IsStrictOrderedRing β] [Archimedean β] (f g : α →+*o β) (x : α), f x ≠ g x → f x < g x → False
h : ¬f x < g x
⊢ False

pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁹ : Field α✝
inst✝⁸ : LinearOrder α✝
inst✝⁷ : Field β✝
inst✝⁶ : LinearOrder β✝
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : f x ≠ g x
h : f x < g x
⊢ False

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : f x ≠ g x
h₂ :
  ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : Field β] [inst_3 : LinearOrder β]
    [IsStrictOrderedRing β] [Archimedean β] (f g : α →+*o β) (x : α), f x ≠ g x → f x < g x → False
h : ¬f x < g x
⊢ False
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 ∈ s → 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 ∉ s → 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 ∈ s → x ∈ Finset.range n
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
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 ∉ s → s.indicator (fun x ↦ a) x = 0

Tactic:
·

Goal state after:
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 ∉ s → s.indicator (fun x ↦ a) x = 0
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ s.Infinite → Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop

pp: case mpr
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop → s.Infinite

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ s.Infinite → Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case i_inj.snd.fst
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).2.1

pp: case i_inj.snd.snd
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).2.2

Tactic:
·

Goal state after:
case i_inj.snd.fst
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).2.1