mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
H : IsClosed ↑L
t : ↥L
ht : t ∈ {x_1 | (fun i ↦ ‖‖↑i - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖↑t - x‖ = 0
this✝¹ : 0 < finrank ℤ ↥L
this✝ : ‖↑t - x‖ < 2⁻¹ * ‖t‖
this : ‖↑t‖ - ‖x‖ < 2⁻¹ * ‖t‖
⊢ t ∈ ⇑(Function.Embedding.subtype fun x ↦ x ∈ L) ⁻¹' (Metric.closedBall 0 (2 * ‖x‖) ∩ ↑L)

Tactic:
sub_lt_iff_lt_add,

Goal state after:
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
H : IsClosed ↑L
t : ↥L
ht : t ∈ {x_1 | (fun i ↦ ‖‖↑i - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖↑t - x‖ = 0
this✝¹ : 0 < finrank ℤ ↥L
this✝ : ‖↑t - x‖ < 2⁻¹ * ‖t‖
this : ‖↑t‖ < 2⁻¹ * ‖t‖ + ‖x‖
⊢ t ∈ ⇑(Function.Embedding.subtype fun x ↦ x ∈ L) ⁻¹' (Metric.closedBall 0 (2 * ‖x‖) ∩ ↑L)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ (∑ i ∈ cons a s ha, f i)! = (f a + ∑ i ∈ s, f i).choose (f a) * (f a)! * (∑ i ∈ s, f i)!

pp: α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ 0 < ∏ i ∈ cons a s ha, (f i)!

Tactic:
Nat.choose_symm_add,

Goal state after:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ (∑ i ∈ cons a s ha, f i)! = (f a + ∑ i ∈ s, f i).choose (∑ i ∈ s, f i) * (f a)! * (∑ i ∈ s, f i)!

α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ 0 < ∏ i ∈ cons a s ha, (f i)!
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
⊢ Finsupp.degree n' = d

Tactic:
← add_left_inj,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
⊢ Finsupp.degree n' + ?a = d + ?a

case a
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := ⋯
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
⊢ ℕ
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
hp' : ((optionEquivLeft R { b // b ≠ j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0
⊢ ¬C c * ((optionEquivLeft R { b // ¬b = j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff = 0

Tactic:
contrapose hp'

Goal state after:
case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
hp' : C c * ((optionEquivLeft R { b // ¬b = j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff = 0
⊢ ((optionEquivLeft R { b // b ≠ j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.degree f = 0 ↔ f.totalDegree = 0

Tactic:
← m.toSyn.injective.eq_iff

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree f) = m.toSyn 0 ↔ f.totalDegree = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : ¬m.toSyn (m.degree 0) ≤ m.toSyn (m.degree g)
hf : f = 0
⊢ 0 ≤ m.toSyn (m.degree g)

Tactic:
apply bot_le

Goal state after:
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) =
    Fintype.card (Sym (Fin (n + 2)) k) + Fintype.card (Sym (Fin (n + 1)) (k + 1))

Tactic:
← card_sum

Goal state after:
n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (r • f)) ≤ m.toSyn (m.degree f)

Tactic:
rw [smul_eq_C_mul]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (C r * f)) ≤ m.toSyn (m.degree f)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : r ∈ R⁰
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.degree f ∈ (r • f).support

Tactic:
simp only [mem_support_iff, smul_eq_C_mul]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : r ∈ R⁰
f : MvPolynomial σ R
hf : ¬f = 0
⊢ coeff (m.degree f) (C r * f) ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : f = 0 ∨ g = 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : f ≠ 0 ∧ g ≠ 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
· rcases h0 with h0 | h0 <;> simp [h0]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : f ≠ 0 ∧ g ≠ 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
⊢ n.MinSqFacProp n.minSqFac

Tactic:
dsimp only [minSqFac]; split_ifs with d2 d4
  · exact ⟨prime_two, (dvd_div_iff_mul_dvd d2).1 d4, fun p pp _ => pp.two_le⟩
  · rcases Nat.eq_zero_or_pos n with rfl | n0
    · cases d4 (by decide)
    refine minSqFacProp_div _ prime_two d2 (mt (dvd_div_iff_mul_dvd d2).2 d4) ?_
    refine minSqFacAux_has_prop 3 (Nat.div_pos (le_of_dvd n0 d2) (by decide)) 0 rfl ?_
    refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)
    rintro rfl
    contradiction
  · rcases Nat.eq_zero_or_pos n with rfl | n0
    · cases d2 (by decide)
    refine minSqFacAux_has_prop _ n0 0 rfl ?_
    refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)
    rintro rfl
    contradiction

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisorsAntidiagonal, f i.2

Tactic:
refine sum_congr rfl fun i hi => ?_

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
i : ℕ × ℕ
hi : i ∈ x.divisorsAntidiagonal
⊢ ↑ζ i.1 • f i.2 = f i.2
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: f : ArithmeticFunction ℕ
x : ℕ
⊢ (f * ζ) x = ∑ i ∈ x.divisors, f i

Tactic:
by
  rw [← natCoe_nat ζ, coe_mul_zeta_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
⊢ (f.ppow k).IsMultiplicative

Tactic:
by
  induction k with
  | zero => exact isMultiplicative_zeta.natCast
  | succ k hi => rw [ppow_succ']; apply hf.pmul hi

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

Goal state before:
pp: case inr.inl
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

pp: case inr.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
· refine absurd ?_ hk0.ne'
    simp [← Nat.factorization_eq_zero_of_not_prime n pp, h1]

Goal state after:
case inr.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
| -⅟(f 1) * ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d

Tactic:
← Finset.sum_attach,

Goal state after:
R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
| -⅟(f 1) * ∑ x ∈ n.properDivisors.attach, f (n / ↑x) * dirichletInverseFun f hf ↑x
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
⊢ m.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g) ∨ m.sPolynomial f g = 0

Tactic:
rw [or_iff_not_imp_right]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
⊢ ¬m.sPolynomial f g = 0 → m.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case mp.refine_1
R : Type u_1
inst✝ : CommRing R
f : (ArithmeticFunction R)ˣ
⊢ 1 1 = 1

Tactic:
one_one

Goal state after:
case mp.refine_1
R : Type u_1
inst✝ : CommRing R
f : (ArithmeticFunction R)ˣ
⊢ 1 = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case mp.refine_2
R : Type u_1
inst✝ : CommRing R
f : (ArithmeticFunction R)ˣ
⊢ 1 1 = 1

Tactic:
one_one

Goal state after:
case mp.refine_2
R : Type u_1
inst✝ : CommRing R
f : (ArithmeticFunction R)ˣ
⊢ 1 = 1
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x,
      ∏ x_1, Additive.toMul (Additive.ofMul (x x_1)) = ⟨n, h⟩ ∧
        (fun x_1 ↦ ↑(Additive.toMul (Additive.ofMul (x x_1)))) = f) ↔
    ∏ i, f i = n ∧ n ≠ 0

Tactic:
toMul_ofMul,

Goal state after:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x, ∏ x_1, x x_1 = ⟨n, h⟩ ∧ (fun x_1 ↦ ↑(x x_1)) = f) ↔ ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

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

pp: case neg
m k : ℕ
hm : ¬m = 0
⊢ Ω (m ^ k) = k * Ω m

Tactic:
· cases k <;> aesop

Goal state after:
case neg
m k : ℕ
hm : ¬m = 0
⊢ Ω (m ^ k) = k * Ω m
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 ∈ n.divisorsAntidiagonal, f x.1 * g x.2 =
    ∑ n ∈ Ioc 0 N, ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2

Tactic:
refine sum_congr rfl fun n hn ↦ ?_

Goal state after:
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
⊢ ∑ x ∈ n.divisorsAntidiagonal, 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 g : ArithmeticFunction R
N : ℕ
⊢ (∑ x ∈ Ioc 0 N, ∑ y ∈ Ioc 0 N, if (x, y).1 * (x, y).2 ≤ N then f (x, y).1 * g (x, y).2 else 0) =
    ∑ n ∈ Ioc 0 N, f n * ∑ m ∈ Ioc 0 (N / n), g m

Tactic:
refine sum_congr rfl fun n hn ↦ ?_

Goal state after:
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
⊢ (∑ y ∈ Ioc 0 N, if (n, y).1 * (n, y).2 ≤ N then f (n, y).1 * g (n, y).2 else 0) = f n * ∑ m ∈ Ioc 0 (N / n), g m
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

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

Tactic:
refine sum_congr rfl fun n hn ↦ ?_

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.CompleteField

Goal state before:
pp: β : Type u_3
γ : Type u_4
inst✝⁵ : Field β
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : IsStrictOrderedRing β
inst✝² : Field γ
inst✝¹ : ConditionallyCompleteLinearOrder γ
inst✝ : IsStrictOrderedRing γ
b : β
⊢ inducedMap γ β (inducedMap β γ b) = b

Tactic:
by
  rw [inducedMap_inducedMap, inducedMap_self]

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

Goal state before:
pp: case i_inj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ Set.InjOn
    (fun x ↦
      match x with
      | ((i, j), k, l) => (i * k, j * l))
    ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal)

Tactic:
simp only [Set.InjOn, mem_coe, mem_divisorsAntidiagonal, mem_product, Prod.mk_inj]
    rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩ ⟨⟨c1, c2⟩, ⟨d1, d2⟩⟩ hcd h
    ext
    · trans gcd (a1 * a2) (a1 * b1)
      · rw [gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]
      · rw [← hcd.1.1, ← hcd.2.1] at cop
        rw [← hcd.1.1, h.1, gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one,
          mul_one]
    · trans gcd (a1 * a2) (a2 * b2)
      · rw [mul_comm, gcd_mul_left, cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one,
          mul_one]
      · rw [← hcd.1.1, ← hcd.2.1] at cop
        rw [← hcd.1.1, h.2, mul_comm, gcd_mul_left,
          cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one, mul_one]
    · trans gcd (b1 * b2) (a1 * b1)
      · rw [mul_comm, gcd_mul_right, cop.coprime_mul_right.coprime_mul_left_right.symm.gcd_eq_one,
          one_mul]
      · rw [← hcd.1.1, ← hcd.2.1] at cop
        rw [← hcd.2.1, h.1, mul_comm c1 d1, gcd_mul_left,
          cop.coprime_mul_right.coprime_mul_left_right.symm.gcd_eq_one, mul_one]
    · trans gcd (b1 * b2) (a2 * b2)
      · rw [gcd_mul_right, cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one, one_mul]
      · rw [← hcd.1.1, ← hcd.2.1] at cop
        rw [← hcd.2.1, h.2, gcd_mul_right,
          cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one, one_mul]

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 : ℕ
⊢ (∑ i ∈ s, f i) ^ (n + 1 + 1) = (∑ i ∈ s, f i) ^ (n + 1) * ∑ i ∈ s, f i

Tactic:
by rw [pow_succ]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b c : MulArchimedeanOrder M
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
intro ⟨m, hm⟩ ⟨n, hn⟩
    use m * n
    rw [pow_mul]
    exact hn.trans (pow_le_pow_left' hm n)

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

Goal state before:
pp: case inl
ι : 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✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
x : ι
hx hy : x ∈ ↑s
hgxy : (g ∘ ⇑σ) x < (g ∘ ⇑σ) x
hfxy : f x < f x
τ : Perm ι := Equiv.trans (Equiv.swap x x) σ
hτs : {x | τ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f i • g (σ i) < ∑ i ∈ s, f i • g (τ i)

Tactic:
cases lt_irrefl _ hfxy

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

Goal state before:
pp: ι : 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✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i, f (σ i) • g i < ∑ i, f i • g i ↔ ¬Monovary (f ∘ ⇑σ) g

Tactic:
simp [(hfg.monovaryOn _).sum_comp_perm_smul_lt_sum_smul_iff fun _ _ ↦ mem_univ _]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
inst✝ : MulArchimedean M
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
⊢ mk a ha = B

Tactic:
| mk a ha
     => 

Goal state after:
case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
inst✝ : MulArchimedean M
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
⊢ mk a ha = B
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ b / (1 - b) ≤ ↑⌊a⌋₊

Tactic:
← ceil_le

Goal state after:
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ ⌈b / (1 - b)⌉₊ ≤ ⌊a⌋₊
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + 1 = a + (b - 1) * (b - 1)⁻¹

Tactic:
mul_inv_cancel₀

Goal state after:
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + 1 = a + 1

K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ b - 1 ≠ 0
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
α : Type u_2
inst✝ : PartialOrder α
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
hAB : mk a ha ≤ B
⊢ lift f ⋯ (mk a ha) ≤ lift f ⋯ B

Tactic:
| mk a ha
     => 

Goal state after:
case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
α : Type u_2
inst✝ : PartialOrder α
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
hAB : mk a ha ≤ B
⊢ lift f ⋯ (mk a ha) ≤ lift f ⋯ B
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s✝ t : NonemptyInterval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ - -s = s

Tactic:
apply NonemptyInterval.ext; exact neg_neg _

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
have ho : (x + y).orderTop = x.orderTop := orderTop_add_eq_left hxy

Goal state after:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
⊢ (x + y).leadingCoeff = x.leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
⊢ x.order ≤ y.order

Tactic:
simp only [order, ne_zero_of_eq_add_single hxy hy, ↓reduceDIte, hy]

Goal state after:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case h₁.h.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
order : Γ
a : R
ha : a ≠ 0
⊢ ((finiteArchimedeanClassOrderHomLex Γ R).comp (finiteArchimedeanClassOrderHomInvLex Γ R))
      (toLex (order, FiniteArchimedeanClass.mk a ha)) =
    OrderHom.id (toLex (order, FiniteArchimedeanClass.mk a ha))

Tactic:
| mk a ha
     => 

Goal state after:
case h₁.h.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
order : Γ
a : R
ha : a ≠ 0
⊢ ((finiteArchimedeanClassOrderHomLex Γ R).comp (finiteArchimedeanClassOrderHomInvLex Γ R))
      (toLex (order, FiniteArchimedeanClass.mk a ha)) =
    OrderHom.id (toLex (order, FiniteArchimedeanClass.mk a ha))
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case h₂.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a : Lex R⟦Γ⟧
ha : a ≠ 0
⊢ ↑(((finiteArchimedeanClassOrderHomInvLex Γ R).comp (finiteArchimedeanClassOrderHomLex Γ R))
        (FiniteArchimedeanClass.mk a ha)) =
    ↑(OrderHom.id (FiniteArchimedeanClass.mk a ha))

Tactic:
| mk a ha
     => 

Goal state after:
case h₂.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a : Lex R⟦Γ⟧
ha : a ≠ 0
⊢ ↑(((finiteArchimedeanClassOrderHomInvLex Γ R).comp (finiteArchimedeanClassOrderHomLex Γ R))
        (FiniteArchimedeanClass.mk a ha)) =
    ↑(OrderHom.id (FiniteArchimedeanClass.mk a ha))
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
⊢ iSupIndep u.stratum'

Tactic:
apply (iSupIndep_map_orderIso_iff (Submodule.mapIic u.baseDomain)).mp

Goal state after:
K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
⊢ iSupIndep (⇑u.baseDomain.mapIic ∘ u.stratum')