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

Goal state before:
pp: case neg.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : g = 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)

Tactic:
[

Goal state after:
case neg.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : g = 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#S)) = ↑p.totalDegree / ↑(#S)

Tactic:
[

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#S)) = ↑p.totalDegree / ↑(#S)
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
n : ℕ
⊢ (↑ζ * f) n = (f * ↑ζ) n

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
n : ℕ
⊢ (↑ζ * f) n = (f * ↑ζ) n
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
h0 : ¬k = 0
⊢ f 0 ^ k = 0

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
h0 : ¬k = 0
⊢ f 0 ^ k = 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case 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 ∈ S

Tactic:
[

Goal state after:
case 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 ∈ S
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case mpr
n p k : ℕ
⊢ 0 < k ∧ n.factorization = Finsupp.single p k → Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
· rintro ⟨hk, hn⟩
    have hn0 : n ≠ 0 := by
      rintro rfl
      simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
    rw [Nat.eq_pow_of_factorization_eq_single hn0 hn]
    exact ⟨Nat.prime_of_mem_primeFactors <|
      Finsupp.mem_support_iff.2 (by simp [hn, hk.ne'] : n.factorization p ≠ 0), hk, rfl⟩

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ n.primeFactors.card = 1

Tactic:
[

Goal state after:
n : ℕ
⊢ IsPrimePow n ↔ n.primeFactors.card = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : n = 0
⊢ (f * dirichletInverse (⇑f) hf) n = 1 n

Tactic:
simp [hn0]

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

Goal state before:
pp: case succ
n : ℕ
⊢ ∃ a b, b ^ 2 * a = n + 1 ∧ Squarefree a

Tactic:
· obtain ⟨a, b, -, -, h₁, h₂⟩ := sq_mul_squarefree_of_pos (succ_pos n)
    exact ⟨a, b, h₁, h₂⟩

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ IsUnit f ↔ IsUnit (f 1)

Tactic:
constructor
  · rintro ⟨f, rfl⟩
    refine ⟨⟨f.val 1, f⁻¹.val 1, ?_, ?_⟩, rfl⟩
    · rw [← ArithmeticFunction.mul_apply_one, Units.mul_inv, one_one]
    · rw [← ArithmeticFunction.mul_apply_one, Units.inv_mul, one_one]
  · suffices Invertible (f 1) → Invertible f by simpa using Nonempty.map this
    exact fun hf ↦ ⟨_, dirichletInverse_mul_self f hf, self_mul_dirichletInverse f hf⟩

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (f + g) p = (f * g) n

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (f + g) p = (f * g) n
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k k' n : ℕ
hk : k ≤ k'
⊢ (σ k) n ≤ (σ k') n

Tactic:
[

Goal state after:
k k' n : ℕ
hk : k ≤ k'
⊢ (σ k) n ≤ (σ k') n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: divisorsAntidiagonal : ℕ+ → Finset (ℕ+ × ℕ+) :=
  fun n ↦ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ x ∈ divisorsAntidiagonal n ↔ x.1 * x.2 = n

Tactic:
[

Goal state after:
divisorsAntidiagonal : ℕ+ → Finset (ℕ+ × ℕ+) :=
  fun n ↦ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ x ∈ divisorsAntidiagonal n ↔ x.1 * x.2 = n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ f ∈
      map (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight
        (finAntidiagonal d (Additive.ofMul ⟨n, h⟩)) ↔
    ∏ i, f i = n ∧ n ≠ 0

Tactic:
[

Goal state after:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ f ∈
      map (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight
        (finAntidiagonal d (Additive.ofMul ⟨n, h⟩)) ↔
    ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiag n, a i = k

Tactic:
[

Goal state after:
case mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiag n, a i = k
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ ∑ n ∈ Ioc 0 N, ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2 =
    ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 ≤ N, f x.1 * g x.2

Tactic:
[

Goal state after:
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ ∑ n ∈ Ioc 0 N, ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2 =
    ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 ≤ N, f x.1 * g x.2
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
f : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
⊢ f n * ∑ m ∈ Ioc 0 (N / n), ↑zeta m = f n * ↑(N / n)

Tactic:
[

Goal state after:
R : Type u_2
inst✝ : Semiring R
f : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
⊢ f n * ∑ m ∈ Ioc 0 (N / n), ↑zeta m = f n * ↑(N / n)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: 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
⊢ f ≠ g → d.primeFactorsPiBij n f hf ≠ d.primeFactorsPiBij n g hg

Tactic:
[

Goal state after:
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
⊢ f ≠ g → d.primeFactorsPiBij n f hf ≠ d.primeFactorsPiBij n g hg
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}

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}
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
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₂)

Tactic:
[

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.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.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 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:
· rw [Finset.prod_filter]
    convert! Finset.dvd_prod_of_mem _ (mem_attach (n.primeFactors) ⟨p, hp⟩)
    rw [if_pos rfl]

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: 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
⊢ a = b

Tactic:
have hab1 : a 1 = b 1 := by
    rw [hab0] at hfab1
    exact (mul_right_inj' <| ne_zero_of_mem_finMulAntidiag hb 0).mp hfab1;

Goal state after:
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 = b
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]
⊢ b.1 * (b.2 / g) = b.1.lcm b.2

Tactic:
lcm,

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]
⊢ b.1 * (b.2 / g) = b.1 * b.2 / b.1.gcd b.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
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
cop : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).Coprime (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2)
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
⊢ (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).gcd (a2 * b2) = ((c1, c2), d1, d2).1.2

Tactic:
h.2,

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
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
cop : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).Coprime (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2)
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
⊢ (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).gcd (((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2) =
    ((c1, c2), d1, d2).1.2
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case h
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 ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : ↑t ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
⊢ n ≤ ∑ k ∈ Finset.range (m + 1), s.indicator (fun x ↦ r) k

Tactic:
grw [hn', ← t_s]

Goal state after:
case h
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 ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : ↑t ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
⊢ n' • r ≤ ∑ k ∈ Finset.range (m + 1), (↑t).indicator (fun x ↦ r) k
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Field β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
q : ℚ
⊢ cutMap β ↑q = Rat.cast '' {r | ↑r < ↑q}

Tactic:
[

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Field β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
q : ℚ
⊢ cutMap β ↑q = Rat.cast '' {r | ↑r < ↑q}
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c

Tactic:
refine ⟨(q ^ 2 : ℚ), coe_mem_cutMap_iff.2 ?_, hbq⟩

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ↑(q ^ 2) < a * a
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
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
cop : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).Coprime (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2)
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
⊢ (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2).gcd (a2 * b2) = ((c1, c2), d1, d2).2.2

Tactic:
h.2,

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
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
cop : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).Coprime (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2)
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
⊢ (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2).gcd (((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2) =
    ((c1, c2), d1, d2).2.2
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) x * (inducedAddHom α β) x = (inducedAddHom α β) (-x) * (inducedAddHom α β) (-x)

Tactic:
[

Goal state after:
case e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) x * (inducedAddHom α β) x = (inducedAddHom α β) (-x) * (inducedAddHom α β) (-x)
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case insert
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ insert a s, f i • g (σ i) ≤ ∑ i ∈ insert a s, f i • g i

Tactic:
[

Goal state after:
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ insert a s, f i • g (σ i) ≤ ∑ i ∈ insert a s, f i • g i
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
⊢ f = g ↔ ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)

Tactic:
constructor <;> intro h
  · simp [h]
  ext n
  by_cases hn : n = 0
  · rw [hn, ArithmeticFunction.map_zero, ArithmeticFunction.map_zero]
  rw [multiplicative_factorization f hf hn, multiplicative_factorization g hg hn]
  exact prod_congr rfl fun p hp ↦ h p _ (prime_of_mem_primeFactors hp)

Goal state after:
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ ↑(#s) ^ n * (↑(#s) * ∑ i ∈ s, f i ^ (n + 1) * f i) = ↑(#s) ^ (n + 1) * ∑ i ∈ s, f i ^ (n + 1 + 1)

Tactic:
[

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ ↑(#s) ^ n * (↑(#s) * ∑ i ∈ s, f i ^ (n + 1) * f i) = ↑(#s) ^ (n + 1) * ∑ i ∈ s, f i ^ (n + 1 + 1)