mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

Goal state before:
pp: 𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
y : E ⧸ K
⊢ ‖(K.quotientEquivOfIsCompl Kᗮ ⋯) y‖ = ‖y‖

Tactic:
set f := K.quotientEquivOfIsCompl Kᗮ K.isCompl_orthogonal

Goal state after:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
y : E ⧸ K
f : (E ⧸ K) ≃ₗ[𝕜] ↥Kᗮ := K.quotientEquivOfIsCompl Kᗮ ⋯
⊢ ‖f y‖ = ‖y‖
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommMonoid R
m : ℕ
inst✝ : NeZero m
f : ℕ → R
⊢ f = ∑ a, {n | ↑n = a}.indicator f

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝¹ : AddCommMonoid R
m : ℕ
inst✝ : NeZero m
f : ℕ → R
n : ℕ
⊢ f n = (∑ a, {n | ↑n = a}.indicator f) n
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
⊢ ∑ k ∈ Ico (u 0) (u n), f k ≤ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)

Tactic:
induction n with

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
⊢ ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k

Tactic:
induction n with

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
⊢ ∑ a ∈ range n.succ, (↑(u (a + 1)) - ↑(u a)) * f (u a) ≤ (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑' (k : ℕ), f k

Tactic:
grw [← ENNReal.sum_le_tsum <| Finset.Ico (u 0 + 1) (u n + 1)]

Goal state after:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
⊢ ∑ a ∈ range n.succ, (↑(u (a + 1)) - ↑(u a)) * f (u a) ≤
    (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑ x ∈ Ico (u 0 + 1) (u n + 1), f x
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f g : M[ι]
⊢ (f * g).toDirectSum = f.toDirectSum * g.toDirectSum

Tactic:
by
  let to_hom : AddMonoidAlgebra M ι →+ ⨁ _ : ι, M :=
  { toFun := toDirectSum
    map_zero' := toDirectSum_zero
    map_add' := toDirectSum_add }
  change to_hom (f * g) = to_hom f * to_hom g
  revert f g
  rw [AddMonoidHom.map_mul_iff]
  ext xi xv yi yv : 4
  simp [to_hom, AddMonoidAlgebra.single_mul_single, DirectSum.of_mul_of]

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst✝¹ : DecidablePred fun x ↦ l₁.getD x 0 ≠ 0
inst✝ : DecidablePred fun x ↦ l₂.getD x 0 ≠ 0
⊢ (l₁ ++ l₂).toFinsupp = l₁.toFinsupp + Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp

Tactic:
ext n

Goal state after:
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst✝¹ : DecidablePred fun x ↦ l₁.getD x 0 ≠ 0
inst✝ : DecidablePred fun x ↦ l₂.getD x 0 ≠ 0
n : ℕ
⊢ (l₁ ++ l₂).toFinsupp n = (l₁.toFinsupp + Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) n
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: case e'_3.e'_6
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 ↦ (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x ↦ xs.getD x 0 ≠ 0
⊢ addRightEmbedding 1 = addLeftEmbedding [x].length

Tactic:
ext n

Goal state after:
case e'_3.e'_6
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 ↦ (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x ↦ xs.getD x 0 ≠ 0
n : ℕ
⊢ (addRightEmbedding 1) n = (addLeftEmbedding [x].length) n
Module: Mathlib.Data.Nat.Factorial.DoubleFactorial

Goal state before:
pp: n : ℕ
⊢ (n + 1)‼ = (n + 1) * (n - 1)‼

Tactic:
by cases n <;> rfl

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
⊢ multinomial s f = multinomial s g

Tactic:
by
  simp only [multinomial]; congr 1
  · rw [Finset.sum_congr rfl h]
  · exact Finset.prod_congr rfl fun a ha => by rw [h a ha]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsLeftCancelAdd R
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, n i = 0
⊢ q = p.divMonomial (Finsupp.single i 1)

Tactic:
ext n

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsLeftCancelAdd R
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, n i = 0
n : σ →₀ ℕ
⊢ coeff n q = coeff n (p.divMonomial (Finsupp.single i 1))
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
⊢ X i ∣ p * q → X i ∣ p ∨ X i ∣ q

Tactic:
intro h
    suffices (p.modMonomial (Finsupp.single i 1)) * (q.modMonomial (Finsupp.single i 1)) =
          (p * q).modMonomial (Finsupp.single i 1) by
      simp only [X_dvd_iff_modMonomial_eq_zero] at h ⊢
      rwa [h, mul_eq_zero] at this
    have hp := p.modMonomial_add_divMonomial_single i
    have hq := q.modMonomial_add_divMonomial_single i
    rw [eq_modMonomial_single_iff]
    · intro n
      contrapose
      intro hn
      classical
      rw [notMem_support_iff, coeff_mul]
      apply Finset.sum_eq_zero
      intro x hx
      simp only [Finset.mem_antidiagonal] at hx
      simp only [← hx, Finsupp.coe_add, Pi.add_apply, Nat.add_eq_zero_iff, not_and_or] at hn
      rcases hn with hn | hn
      · rw [coeff_modMonomial_of_le, zero_mul]
        simpa [← Nat.one_le_iff_ne_zero] using hn
      · rw [mul_comm, coeff_modMonomial_of_le, zero_mul]
        simpa [← Nat.one_le_iff_ne_zero] using hn
    · nth_rewrite 1 [← hp]
      nth_rewrite 1 [← hq]
      simp only [add_mul, mul_add, add_assoc, add_sub_cancel_left]
      simp only [← mul_assoc, mul_comm _ (X i)]
      simp only [mul_assoc, ← mul_add (X i)]
      apply dvd_mul_right

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
p : MvPolynomial (Fin n) R
s : Fin n → Set R
hs : ∀ (i : Fin n), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = 0
⊢ p = 0

Tactic:
induction n with

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p✝ q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h✝ : ∀ x ∈ Set.univ.pi s, (eval x) p✝ = (eval x) q
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ x ∈ Set.univ.pi s, (eval x) ((rename f) p) = 0
x : Fin n → R
hx : x ∈ Set.univ.pi (s ∘ f)
g : σ → R
hg : ∀ (i : σ), g i ∈ s i
i : σ
x✝ : i ∈ Set.univ
nex : ¬∃ x, f x = i
⊢ Function.extend f x g i ∈ s i

Tactic:
Function.extend,

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p✝ q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h✝ : ∀ x ∈ Set.univ.pi s, (eval x) p✝ = (eval x) q
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ x ∈ Set.univ.pi s, (eval x) ((rename f) p) = 0
x : Fin n → R
hx : x ∈ Set.univ.pi (s ∘ f)
g : σ → R
hg : ∀ (i : σ), g i ∈ s i
i : σ
x✝ : i ∈ Set.univ
nex : ¬∃ x, f x = i
⊢ (if h : ∃ a, f a = i then x (Classical.choose h) else g i) ∈ s i
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a : α
b : β
ha : Acc rα a
hb : Acc rβ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b)

Tactic:
induction ha generalizing b with | _ a _ iha
  induction hb with | _ b hb ihb
  refine Acc.intro _ fun h => ?_
  rintro (⟨ra⟩ | ⟨rb⟩)
  exacts [iha _ ra (Acc.intro b hb), ihb _ rb]

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a < degree b ∨ degree a = degree b ∧ toLex a ≤ toLex b

Tactic:
refine Or.inr ⟨le_antisymm ?_ ha, toLex_monotone h⟩
      rw [← add_tsub_cancel_of_le h, map_add]
      exact Nat.le_add_right a.degree (b - a).degree

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ m.degree (X s) = Finsupp.single s 1

Tactic:
classical
  change m.degree (monomial (Finsupp.single s 1) (1 : R)) = _
  rw [degree_monomial, if_neg one_ne_zero]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
⊢ c ∈ (f * g).support → m.toSyn c ≤ m.toSyn (m.degree f + m.degree g)

Tactic:
rw [← not_lt, mem_support_iff, not_imp_not]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
⊢ m.toSyn (m.degree f + m.degree g) < m.toSyn c → coeff c (f * g) = 0
Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ↥(s.finsuppAntidiag n)
⊢ ((subtypeDomain (fun x ↦ x ∈ s) ↑f).sum fun x ↦ id) = n

Tactic:
have hf := f.2

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ↥(s.finsuppAntidiag n)
hf : ↑f ∈ s.finsuppAntidiag n
⊢ ((subtypeDomain (fun x ↦ x ∈ s) ↑f).sum fun x ↦ id) = n
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ normalizedFactors s.prod = s

Tactic:
by
  rw [← Multiset.rel_eq, ← associated_eq_eq]
  apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor h
    (prod_normalizedFactors _)
  rw [Ne, Multiset.prod_eq_zero_iff]
  exact fun con ↦ not_irreducible_zero (h 0 con)

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
induction n with

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
⊢ coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n

Tactic:
induction n with

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
h✝ : Nontrivial R
⊢ ∑ i ∈ s, m.degree (P i) ∈ (∏ i ∈ s, P i).support

Tactic:
simpa [m.coeff_prod_sum_degree, Finset.prod_eq_zero_iff]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ #({r ∈ piFinset (tail S) | (eval r) pₖ ≠ 0}.biUnion fun a ↦
        filter ((fun x ↦ (eval x) p = 0) ∘ ⇑(consEquiv fun i ↦ R).toEmbedding) (image (fun a_1 ↦ (a_1, a)) (S 0))) =
    #({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}.biUnion fun xₜ ↦
        image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}))

Tactic:
simp [filter_image]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ #({x ∈ piFinset (tail S) | ¬(eval x) pₖ = 0}.biUnion fun a ↦
        image (fun a_1 ↦ (a_1, a)) ({a_1 ∈ S 0 | (eval ((consEquiv fun i ↦ R) (a_1, a))) p = 0})) =
    #({x ∈ piFinset fun i ↦ tail S i | ¬(eval x) pₖ = 0}.biUnion fun xₜ ↦
        image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}))
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

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

Tactic:
ext n

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑1 = 1

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ↑1 n = 1 n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
⊢ ↑1 = 1

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑1 n = 1 n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

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

Tactic:
ext n

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f g : ArithmeticFunction ℤ
⊢ ↑(f * g) = ↑f * ↑g

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : Ring R
f g : ArithmeticFunction ℤ
n : ℕ
⊢ ↑(f * g) n = (↑f * ↑g) n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: 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
⊢ (f * g) • h = f • g • h

Tactic:
ext n

Goal state after:
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 : ℕ
⊢ ((f * g) • h) n = (f • g • h) n
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
⊢ f.pdiv ↑ζ = f

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
n : ℕ
⊢ (f.pdiv ↑ζ) n = f n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
⊢ f * dirichletInverse (⇑f) hf = 1

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
⊢ (f * dirichletInverse (⇑f) hf) n = 1 n
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n k : ℕ
hk : k ≠ 0
⊢ IsPrimePow (n ^ k) ↔ IsPrimePow n

Tactic:
simp only [isPrimePow_iff_unique_prime_dvd]

Goal state after:
n k : ℕ
hk : k ≠ 0
⊢ (∃! p, Nat.Prime p ∧ p ∣ n ^ k) ↔ ∃! p, Nat.Prime p ∧ p ∣ n
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.degree f = m.degree g
hs : m.sPolynomial f g ≠ 0
⊢ m.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f)

Tactic:
simpa [h] using m.degree_sPolynomial_lt_sup_degree hs

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

Goal state before:
pp: case inr.inr
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
⊢ {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}

Tactic:
ext n

Goal state after:
case inr.inr
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ n ∈ {d ∈ (a * b).divisors | IsPrimePow d} ↔ n ∈ {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: ⊢ pow 0 = ζ

Tactic:
ext n

Goal state after:
n : ℕ
⊢ (pow 0) n = ζ n
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: ⊢ pow 1 = ArithmeticFunction.id

Tactic:
ext n

Goal state after:
n : ℕ
⊢ (pow 1) n = ArithmeticFunction.id n
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 =
    ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 ≤ N, f x.1 * g x.2

Tactic:
trans ∑ n ∈ Ioc 0 N, ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2

Goal state after:
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

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.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
⊢ (b1 * b2).gcd (a1 * b1) = ((c1, c2), d1, d2).2.1

Tactic:
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]

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

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

Tactic:
ext n

Goal state after:
case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
⊢ f n = g n
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 : MulArchimedeanOrder M
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
lt_def,

Goal state after:
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 : MulArchimedeanOrder M
⊢ (∀ (n : ℕ), |val b|ₘ ^ n < |val a|ₘ) ↔ a ≤ b ∧ ¬b ≤ a
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
⊢ mk a = ⊤ → a = 1

Tactic:
simp [← mk_one, mk_eq_mk]

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

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
hba : mk b ≤ mk a
⊢ mk b ≤ mk (a / b)

Tactic:
by
  simpa [div_eq_mul_inv, hba] using mk_right_le_mk_mul (a := a) (b := b⁻¹)

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

Goal state before:
pp: case insert.inr.refine_3
ι : 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
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
x : ι
hx : x ∈ s.erase ((Equiv.symm σ) a)
⊢ f x • g (σ x) = f x • g ((Equiv.swap a (σ a)) (σ x))

Tactic:
mem_erase,

Goal state after:
case insert.inr.refine_3
ι : 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
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
x : ι
hx : x ≠ (Equiv.symm σ) a ∧ x ∈ s
⊢ f x • g (σ x) = f x • g ((Equiv.swap a (σ a)) (σ x))
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌊↑r + ↑n⌋ₑ = ↑(⌊r⌋₊ + n)

Tactic:
rw [← ENNReal.ofNNReal_add_natCast]

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌊↑(r + ↑n)⌋ₑ = ↑(⌊r⌋₊ + n)
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌈↑r + ↑n⌉ₑ = ↑(⌈r⌉₊ + n)

Tactic:
rw [← ENNReal.ofNNReal_add_natCast]

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌈↑(r + ↑n)⌉ₑ = ↑(⌈r⌉₊ + n)
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : CommGroup α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulLeftStrictMono α
a b c : α
hc : a * b < c
a' : α
ha' : b < a'
hc' : a' < c / a
⊢ ∃ b', b' > b ∧ a * b' < c

Tactic:
exact ⟨a', ha', lt_div_iff_mul_lt'.1 hc'⟩

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: S : Type u_1
G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : SetLike S G
C : S
inst✝² : GroupConeClass S G
inst✝¹ : HasMemOrInvMem C
inst✝ : DecidablePred fun x ↦ x ∈ C
a b : G
⊢ a ≤ b ∨ b ≤ a

Tactic:
by simpa using mem_or_inv_mem C (b / a)

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S✝ : Type u_4
U : Type u_5
V✝ : Type u_6
α : Type u_7
inst✝⁶ : PartialOrder Γ
V : Type u_8
inst✝⁵ : Monoid R
inst✝⁴ : AddMonoid V
inst✝³ : DistribMulAction R V
S : Type u_9
inst✝² : Monoid S
inst✝¹ : DistribMulAction S V
inst✝ : SMulCommClass R S V
r : R
s : S
a : V⟦Γ⟧
⊢ r • s • a = s • r • a

Tactic:
ext
    simp [smul_comm]

Goal state after: