-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b = b

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
y : ℕ × ℕ
ymem : y ∈ x.divisorsAntidiagonal
ynmem : y ∉ {(1, x)}
con : y.1 = 1
⊢ False

Tactic:
simp only [mem_divisorsAntidiagonal, one_mul, Ne] at ymem

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
y : ℕ × ℕ
ynmem : y ∉ {(1, x)}
con : y.1 = 1
ymem : y.1 * y.2 = x ∧ ¬x = 0
⊢ False

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
y : ℕ × ℕ
ymem : y ∈ x.divisorsAntidiagonal
ynmem : y ∉ {(1, x)}
y1ne : y.1 ≠ 1
⊢ 1 y.1 • b y.2 = 0

Tactic:
simp [y1ne]

Result:
no goals

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
snd✝ : ℕ
ymem : (1, snd✝).1 * (1, snd✝).2 = x ∧ ¬x = 0
ynmem : ¬((1, snd✝).1 = 1 ∧ (1, snd✝).2 = x)
⊢ False

Tactic:
simp only [true_and, one_mul, x0, not_false_eq_true, and_true] at ynmem ymem

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
snd✝ : ℕ
ynmem : ¬snd✝ = x
ymem : snd✝ = x
⊢ False

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
y : ℕ × ℕ
ymem : y ∈ x.divisorsAntidiagonal
ynmem : y ∉ {(1, x)}
⊢ 1 y.1 • b y.2 = 0

Tactic:
have y1ne : y.fst ≠ 1 := by
  intro con
  simp only [mem_divisorsAntidiagonal, one_mul, Ne] at ymem
  simp only [mem_singleton, Prod.ext_iff] at ynmem
  cases y
  subst con
  simp only [true_and, one_mul, x0, not_false_eq_true, and_true] at ynmem ymem
  tauto

Result:
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
y : ℕ × ℕ
ymem : y ∈ x.divisorsAntidiagonal
ynmem : y ∉ {(1, x)}
y1ne : y.1 ≠ 1
⊢ 1 y.1 • b y.2 = 0

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
snd✝ : ℕ
ynmem : ¬snd✝ = x
ymem : snd✝ = x
⊢ False

Tactic:
tauto

Result:
no goals

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
fst✝ snd✝ : ℕ
con : (fst✝, snd✝).1 = 1
ymem : (fst✝, snd✝).1 * (fst✝, snd✝).2 = x ∧ ¬x = 0
ynmem : ¬((fst✝, snd✝).1 = 1 ∧ (fst✝, snd✝).2 = x)
⊢ False

Tactic:
subst con

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
snd✝ : ℕ
ymem : (1, snd✝).1 * (1, snd✝).2 = x ∧ ¬x = 0
ynmem : ¬((1, snd✝).1 = 1 ∧ (1, snd✝).2 = x)
⊢ False

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
⊢ ∑ x ∈ {(1, x)}, 1 x.1 • b x.2 = b x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
y : ℕ × ℕ
ynmem : y ∉ {(1, x)}
con : y.1 = 1
ymem : y.1 * y.2 = x ∧ ¬x = 0
⊢ False

Tactic:
simp only [mem_singleton, Prod.ext_iff] at ynmem

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
y : ℕ × ℕ
con : y.1 = 1
ymem : y.1 * y.2 = x ∧ ¬x = 0
ynmem : ¬(y.1 = 1 ∧ y.2 = x)
⊢ False

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
y : ℕ × ℕ
con : y.1 = 1
ymem : y.1 * y.2 = x ∧ ¬x = 0
ynmem : ¬(y.1 = 1 ∧ y.2 = x)
⊢ False

Tactic:
cases y

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
fst✝ snd✝ : ℕ
con : (fst✝, snd✝).1 = 1
ymem : (fst✝, snd✝).1 * (fst✝, snd✝).2 = x ∧ ¬x = 0
ynmem : ¬((fst✝, snd✝).1 = 1 ∧ (fst✝, snd✝).2 = x)
⊢ False

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
⊢ {(1, x)} ⊆ x.divisorsAntidiagonal

Tactic:
simp [x0]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
⊢ 1 • b = b

Tactic:
ext x

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
⊢ (1 • b) x = b x

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : x = 0
⊢ ∑ x ∈ x.divisorsAntidiagonal, 1 x.1 • b x.2 = b x

Tactic:
simp [x0]

Result:
no goals

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
⊢ ∑ x ∈ x.divisorsAntidiagonal, 1 x.1 • b x.2 = b x

Tactic:
rw [← sum_subset h]

Result:
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
⊢ ∑ x ∈ {(1, x)}, 1 x.1 • b x.2 = b x

case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ x.divisorsAntidiagonal
⊢ ∀ x_1 ∈ x.divisorsAntidiagonal, x_1 ∉ {(1, x)} → 1 x_1.1 • b x_1.2 = 0

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
⊢ (1 • b) x = b x

Tactic:
rw [smul_apply]

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, 1 x.1 • b x.2 = b x

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, 1 x.1 • b x.2 = b x

Tactic:
by_cases x0 : x = 0

Result:
case pos
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : x = 0
⊢ ∑ x ∈ x.divisorsAntidiagonal, 1 x.1 • b x.2 = b x

case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
⊢ ∑ x ∈ x.divisorsAntidiagonal, 1 x.1 • b x.2 = b x