Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case hi
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.1.divisorsAntidiagonal,
    (match a with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩) ∈
      n.divisorsAntidiagonal.sigma fun a ↦ a.2.divisorsAntidiagonal

pp: case hj
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.2.divisorsAntidiagonal,
    (match a with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i * k, l), (i, k)⟩) ∈
      n.divisorsAntidiagonal.sigma fun a ↦ a.1.divisorsAntidiagonal

pp: case left_neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.1.divisorsAntidiagonal,
    (match
        match a with
        | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩ with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i * k, l), (i, k)⟩) =
      a

pp: case right_neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.2.divisorsAntidiagonal,
    (match
        match a with
        | ⟨(i, _j), (k, l)⟩ => ⟨(i * k, l), (i, k)⟩ with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩) =
      a

pp: case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.1.divisorsAntidiagonal,
    f a.snd.1 • g a.snd.2 • h a.fst.2 =
      f
          (match a with
              | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩).fst.1 •
        g
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩).snd.1 •
          h
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩).snd.2

Tactic:
<;>

Goal state after:
case hi
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.1.divisorsAntidiagonal,
    (match a with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩) ∈
      n.divisorsAntidiagonal.sigma fun a ↦ a.2.divisorsAntidiagonal

case hj
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.2.divisorsAntidiagonal,
    (match a with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i * k, l), (i, k)⟩) ∈
      n.divisorsAntidiagonal.sigma fun a ↦ a.1.divisorsAntidiagonal

case left_neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.1.divisorsAntidiagonal,
    (match
        match a with
        | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩ with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i * k, l), (i, k)⟩) =
      a

case right_neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.2.divisorsAntidiagonal,
    (match
        match a with
        | ⟨(i, _j), (k, l)⟩ => ⟨(i * k, l), (i, k)⟩ with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩) =
      a

case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.1.divisorsAntidiagonal,
    f a.snd.1 • g a.snd.2 • h a.fst.2 =
      f
          (match a with
              | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩).fst.1 •
        g
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩).snd.1 •
          h
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩).snd.2