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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝¹⁰ : RCLike 𝕜
E✝ : Type u_4
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace 𝕜 E✝
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
F' : Type u_6
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : InnerProductSpace ℝ F'
inst✝³ : Fintype ι
V : Type u_7
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L✝ L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this✝ : CompleteSpace ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := ↑S.orthogonalProjectionOnto
p2 : V →ₗ[𝕜] ↥Sᗮ := ↑Sᗮ.orthogonalProjectionOnto
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
x : V
Mx_decomp : M x = L (p1 x) + L3 (p2 x)
Mx_orth : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ‖L (p1 x) + L3 (p2 x)‖ * ‖L (p1 x) + L3 (p2 x)‖ =
    ‖S.orthogonalProjectionOnto x‖ * ‖S.orthogonalProjectionOnto x‖ +
      ‖Sᗮ.orthogonalProjectionOnto x‖ * ‖Sᗮ.orthogonalProjectionOnto x‖

Tactic:
norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (L (p1 x)) (L3 (p2 x)) Mx_orth

Goal state after:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝¹⁰ : RCLike 𝕜
E✝ : Type u_4
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace 𝕜 E✝
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
F' : Type u_6
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : InnerProductSpace ℝ F'
inst✝³ : Fintype ι
V : Type u_7
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L✝ L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this✝ : CompleteSpace ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := ↑S.orthogonalProjectionOnto
p2 : V →ₗ[𝕜] ↥Sᗮ := ↑Sᗮ.orthogonalProjectionOnto
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
x : V
Mx_decomp : M x = L (p1 x) + L3 (p2 x)
Mx_orth : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ‖L (p1 x)‖ * ‖L (p1 x)‖ + ‖L3 (p2 x)‖ * ‖L3 (p2 x)‖ =
    ‖S.orthogonalProjectionOnto x‖ * ‖S.orthogonalProjectionOnto x‖ +
      ‖Sᗮ.orthogonalProjectionOnto x‖ * ‖Sᗮ.orthogonalProjectionOnto x‖
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
hb : b < a
⊢ ⟪gramSchmidt 𝕜 f b, gramSchmidt 𝕜 f a⟫_𝕜 = 0

Tactic:
exact this _ _ hb

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ x ∈ (prepartition n B).boxes,
      if (prepartition n B).tag x ∈ s then volume.real ↑x * F ((prepartition n B).tag x) else volume.real ↑x * 0

Tactic:
mul_zero,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ x ∈ (prepartition n B).boxes,
      if (prepartition n B).tag x ∈ s then volume.real ↑x * F ((prepartition n B).tag x) else 0
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
⊢ LinearIndependent 𝕜 (gramSchmidtNormed 𝕜 f)

Tactic:
unfold gramSchmidtNormed
  have (i : ι) : IsUnit (‖gramSchmidt 𝕜 f i‖⁻¹ : 𝕜) :=
    isUnit_iff_ne_zero.mpr (by simp [gramSchmidt_ne_zero i h₀])
  let w : ι → 𝕜ˣ := fun i ↦ (this i).unit
  apply (gramSchmidt_linearIndependent h₀).units_smul (w := fun i ↦ (this i).unit)

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this✝ : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
n : ℕ
this : ∀ J ∈ π.filter fun J ↦ N (π.tag J) = n, ‖μ.real ↑J • f (π.tag J)‖ ≤ μ.real ↑J * ↑n
⊢ ‖∑ J ∈ (π.filter fun x ↦ N (π.tag x) = n).boxes, μ.toBoxAdditive J • f ((π.filter fun x ↦ N (π.tag x) = n).tag J)‖ ≤
    ↑(δ n)

Tactic:
refine (norm_sum_le_of_le _ this).trans ?_

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this✝ : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
n : ℕ
this : ∀ J ∈ π.filter fun J ↦ N (π.tag J) = n, ‖μ.real ↑J • f (π.tag J)‖ ≤ μ.real ↑J * ↑n
⊢ ∑ b ∈ (π.filter fun J ↦ N (π.tag J) = n).boxes, μ.real ↑b * ↑n ≤ ↑(δ n)
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ J ∈ π, (πi J).IsPartition
J : Box ι
hJ : J ∈ π.boxes
⊢ ∑ J' ∈ (πi J).boxes, (vol J') (f ((π.biUnionPrepartition πi).tag J')) = (vol J) (f (π.tag J))

Tactic:
calc
    (∑ J' ∈ (πi J).boxes, vol J' (f (π.tag <| π.toPrepartition.biUnionIndex πi J'))) =
        ∑ J' ∈ (πi J).boxes, vol J' (f (π.tag J)) :=
      sum_congr rfl fun J' hJ' => by rw [Prepartition.biUnionIndex_of_mem _ hJ hJ']
    _ = vol J (f (π.tag J)) :=
      (vol.map ⟨⟨fun g : E →L[ℝ] F => g (f (π.tag J)), rfl⟩, fun _ _ => rfl⟩).sum_partition_boxes
        le_top (hπi J hJ)

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: case neg
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ
hc : c ≠ 0
hf : ¬Integrable I l f vol
⊢ integral I l (fun x ↦ c • f x) vol = c • integral I l f vol

Tactic:
· have : ¬Integrable I l (fun x => c • f x) vol := mt (fun h => h.of_smul hc) hf
    rw [integral, integral, dif_neg hf, dif_neg this, smul_zero]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
c : ℝ≥0
⊢ l.RCond (h.convergenceR ε c)

Tactic:
rw [convergenceR]

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
c : ℝ≥0
⊢ l.RCond ((if hε : 0 < ε then ⋯.choose else fun x x_1 ↦ ⟨1, convergenceR._proof_2⟩) c)
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = n✝ + 1)
o : Orientation ℝ E (Fin (n✝ + 1))
b : OrthonormalBasis (Fin (n✝ + 1)) ℝ E
v : Fin (n✝ + 1) → E
⊢ |o.volumeForm v| = |b.toBasis.det v|

Tactic:
rw [o.volumeForm_robust (b.adjustToOrientation o) (b.orientation_adjustToOrientation o),
      b.abs_det_adjustToOrientation]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x ↦ x ^ p / x ^ q) atTop atTop

Tactic:
tendsto_congr' pow_div_pow_eventuallyEq_atTop

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x ↦ x ^ (↑p - ↑q)) atTop atTop
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ Tendsto (fun x ↦ x ^ p / x ^ q) atTop (𝓝 0)

Tactic:
tendsto_congr' pow_div_pow_eventuallyEq_atTop

Goal state after:
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ Tendsto (fun x ↦ x ^ (↑p - ↑q)) atTop (𝓝 0)
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: case left
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := ⋯
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
⊢ μ.measureOf s = μ (s ∩ v)

Tactic:
refine measure_eq_measure_of_null_sdiff s.inter_subset_left ?_ |>.symm

Goal state after:
case left
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
⊢ μ (s \ (s ∩ v)) = 0
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inl.h_mono
p : ℝ
hp : 0 ≤ p
⊢ ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹

Tactic:
intro m n hm hmn
      gcongr

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x✝ x y : k[A]
hy : y ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}
m : A
hm✝¹ : m ∈ (x.coeff.sum fun i n ↦ y.coeff.sum fun i_1 n_1 ↦ (single (i + i_1) (n * n_1)).coeff).support
xm : A
hm✝ : m ∈ (y.coeff.sum fun i n ↦ (single (xm + i) (x.coeff xm * n)).coeff).support
ym : A
hym : ym ∈ y.coeff.support
hm : m ∈ (single (xm + ym) (x.coeff xm * y.coeff ym)).coeff.support
⊢ ∃ m' ∈ s, ∃ d, m = d + m'

Tactic:
obtain rfl := Finset.mem_singleton.mp <| Finsupp.support_single_subset hm

Goal state after:
k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x✝ x y : k[A]
hy : y ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}
xm ym : A
hym : ym ∈ y.coeff.support
hm✝¹ : xm + ym ∈ (x.coeff.sum fun i n ↦ y.coeff.sum fun i_1 n_1 ↦ (single (i + i_1) (n * n_1)).coeff).support
hm✝ : xm + ym ∈ (y.coeff.sum fun i n ↦ (single (xm + i) (x.coeff xm * n)).coeff).support
hm : xm + ym ∈ (single (xm + ym) (x.coeff xm * y.coeff ym)).coeff.support
⊢ ∃ m' ∈ s, ∃ d, xm + ym = d + m'
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
n : ℕ
⊢ (↑n).toAddMonoidAlgebra = ↑n

Tactic:
by
  ext : 1; exact DFinsupp.toFinsupp_single ..

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Ring M
inst✝ : (m : M) → Decidable (m ≠ 0)
z : ℤ
⊢ (↑z).toAddMonoidAlgebra = ↑z

Tactic:
by
  ext : 1; exact DFinsupp.toFinsupp_single ..

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : Zero ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
⊢ toAddMonoidAlgebra 1 = 1

Tactic:
by
  ext : 1; exact DFinsupp.toFinsupp_single ..

Goal state after:
Module: Mathlib.Data.Nat.Factorial.DoubleFactorial

Goal state before:
pp: n : ℕ
⊢ (2 * (n + 1))‼ = 2 ^ (n + 1) * (n + 1)!

Tactic:
mul_add,

Goal state after:
n : ℕ
⊢ (2 * n + 2 * 1)‼ = 2 ^ (n + 1) * (n + 1)!
Module: Mathlib.Algebra.MvPolynomial.Comap

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), f φ = φ
x : σ → R
⊢ f = AlgHom.id R (MvPolynomial σ R)

Tactic:
ext1 φ

Goal state after:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), f φ = φ
x : σ → R
φ : σ
⊢ f (X φ) = (AlgHom.id R (MvPolynomial σ R)) (X φ)
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
hn : 0 < n
g g' : MvPolynomial σ R
H : (expand n) g = (expand n) g'
d : σ →₀ ℕ
⊢ coeff d g = coeff d g'

Tactic:
rw [← coeff_expand_smul _ (n.ne_zero_iff_zero_lt.mpr hn), H, coeff_expand_smul _
      (n.ne_zero_iff_zero_lt.mpr hn)]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p

Tactic:
apply induction_on p
  · simp
  · intro p q hp hq
    simp [hp, hq]
  · intro p n hp
    simp [hp]

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ : β → β → Prop
a : α
b : β
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
⊢ (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
    (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (a₁, b₁) (b₂, a₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂))

Tactic:
Prod.gameAdd_swap_swap_mk _ _ a₁ b₂ b₁ a₂

Goal state after:
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ : β → β → Prop
a : α
b : β
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
⊢ (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
    (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂))
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
rα : α → α → Prop
⊢ ∀ {x y : α × α}, GameAdd rα s(x.1, x.2) s(y.1, y.2) ↔ Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα x.swap y

Tactic:
by
  rintro ⟨_, _⟩ ⟨_, _⟩
  rfl

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

Goal state before:
pp: case succ
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k
⊢ (m.sum + k • m.sum).choose m.sum * m.multinomial *
      ((Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k) =
    ((m.sum + ∑ i ∈ Finset.range k, m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun x ↦ m.sum) *
      (m.multinomial * m.multinomial ^ k)

Tactic:
simp [smul_eq_mul, Finset.sum_const, Finset.card_range]

Goal state after:
case succ
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k
⊢ (m.sum + k * m.sum).choose m.sum * m.multinomial *
      ((Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k) =
    ((m.sum + k * m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun x ↦ m.sum) *
      (m.multinomial * m.multinomial ^ k)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : (∀ i ∈ s, f i ≠ 0) → degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
ha : ¬f a = 0
hs : ∀ a ∈ s, ¬f a = 0
⊢ ?m.84 ≠ 0

Tactic:
by rw [prod_ne_zero_iff]; exact hs

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
⊢ p ∣ (monomial n) 1 ↔ ∃ m u, m ≤ n ∧ IsUnit u ∧ p = (monomial m) u

Tactic:
rcases subsingleton_or_nontrivial R with hR | hR
  · suffices ∃ m, m ≤ n by simpa [Subsingleton.elim _ p]
    use n
  rw [dvd_monomial_iff_exists (one_ne_zero' R)]
  apply exists_congr
  intro m
  simp_rw [isUnit_iff_dvd_one]

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✝ : Subsingleton R
f : MvPolynomial σ R
⊢ m.degree 0 = 0

Tactic:
degree_zero

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
f : MvPolynomial σ R
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : ¬n = 0
⊢ m.degree 0 = 0

Tactic:
degree_zero

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : ¬n = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.degree (-f) = m.degree f

Tactic:
by
  unfold degree
  rw [support_neg]

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 : ℕ
⊢ (↑ζ • f) x = ∑ i ∈ x.divisors, f i

Tactic:
smul_apply

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 : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisors, f i
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
⊢ (f.pmul g) 1 = 1

Tactic:
by simp [hf, hg]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
⊢ (f.pdiv g) 1 = 1

Tactic:
by simp [hf, hg]

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

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ ¬n.primeFactors.card = 1 ↔ n.primeFactors.Nontrivial

Tactic:
← Finset.one_lt_card_iff_nontrivial

Goal state after:
n : ℕ
hn : 2 ≤ n
⊢ ¬n.primeFactors.card = 1 ↔ 1 < n.primeFactors.card
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
⊢ m.leadingCoeff g * coeff (m.degree f) f -
      coeff (m.degree f ⊔ m.degree g) ((monomial (m.degree f ⊔ m.degree g - m.degree g)) (m.leadingCoeff f) * g) =
    0

Tactic:
← tsub_add_cancel_of_le le_sup_right,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.leadingCoeff g * coeff (m.degree f) f -
      coeff (m.degree f ⊔ m.degree g - m.degree g + m.degree g)
        ((monomial (m.degree f ⊔ m.degree g - m.degree g)) (m.leadingCoeff f) * g) =
    0
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
⊢ (σ k) n = ∑ d ∈ n.divisors, (n / d) ^ k

Tactic:
by
  rw [sigma_apply, ← sum_div_divisors]

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

Goal state before:
pp: n : ℕ
⊢ Ω n = n.factorization.sum fun x k ↦ k

Tactic:
simp [cardFactors_apply, ← List.sum_toFinset_count_eq_length, Finsupp.sum]

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

Goal state before:
pp: case cons
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
⊢ ω (∏ i ∈ cons a s ha, f i) = ∑ i ∈ cons a s ha, ω (f i)

Tactic:
rw [prod_cons, sum_cons, cardDistinctFactors_mul, ih]

Goal state after:
case cons
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
⊢ (↑s).Pairwise (Coprime on f)

case cons
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
⊢ (f a).Coprime (∏ x ∈ s, f x)
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Field α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ∀ (x : α), ∃ n, x < ↑n

Tactic:
by_contra! ⟨x, h⟩

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Field α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
h : ∀ (n : ℕ), ↑n ≤ x
⊢ False