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✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this✝ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
ε : ℝ
hε : ε > 0
hε' : Metric.ball 0 ε ⊆ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1
x : ↥L
i : ι
hx : ¬x = 0
⊢ ε / 2 * ↑|(b.repr x) i| ≤ ‖x‖

Tactic:
have hx : ‖x.1‖ ≠ 0 := by simpa

Goal state after:
case neg
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this✝ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
ε : ℝ
hε : ε > 0
hε' : Metric.ball 0 ε ⊆ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1
x : ↥L
i : ι
hx✝ : ¬x = 0
hx : ‖↑x‖ ≠ 0
⊢ ε / 2 * ↑|(b.repr x) i| ≤ ‖x‖
Module: Mathlib.Data.Finset.SMulAntidiagonal

Goal state before:
pp: case mp
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ a ∈ s ∧ b ∈ t ∧ a • b = hs.min hns • ht.min hnt → a = hs.min hns ∧ b = ht.min hnt

Tactic:
rintro ⟨has, hat, hst⟩

Goal state after:
case mp
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
has : a ∈ s
hat : b ∈ t
hst : a • b = hs.min hns • ht.min hnt
⊢ a = hs.min hns ∧ b = ht.min hnt
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ Tendsto (fun n ↦ ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ card ι) atTop (𝓝 (volume.real s / covolume L volume))

Tactic:
by
  convert! tendsto_card_div_pow'' b hs₁ hs₂ ?_
  · simp only [measureReal_def]
    rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]
  · rw [frontier_equivFun, volume_image_eq_volume_div_covolume, hs₃, ENNReal.zero_div]

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
n : ℕ
hn : finrank ℤ ↥L < n
x : E
⊢ Summable fun z ↦ ‖↑z - x‖⁻¹ ^ n

Tactic:
simpa using summable_norm_sub_zpow L (-n) (by gcongr) x

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
⊢ Function.LeftInverse (comap ↑f.symm) (comap ↑f)

Tactic:
intro x
    rw [← comap_comp_apply]
    apply comap_eq_id_of_eq_id
    intro
    simp only [AlgHom.id_apply, AlgEquiv.comp_symm]

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

Goal state before:
pp: case h₁
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs' : ⇑s ∉ a.support.piAntidiag n
hs'' : s.support ⊆ a.support
⊢ False

Tactic:
rw [Finset.mem_piAntidiag, not_and_or] at hs'

Goal state after:
case h₁
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs' : ¬a.support.sum ⇑s = n ∨ ¬∀ (i : σ), s i ≠ 0 → i ∈ a.support
hs'' : s.support ⊆ a.support
⊢ False
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case neg
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
ha : a ∉ s
⊢ ∏ x ∈ s, (Pi.single a n x)! = 1

Tactic:
apply Finset.prod_eq_one

Goal state after:
case neg
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
ha : a ∉ s
⊢ ∀ x ∈ s, (Pi.single a n x)! = 1
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s → (monomial i) r ∣ (monomial j) s

Tactic:
· rintro ⟨h | hij, d, rfl⟩
    · simp_rw [h, monomial_zero, dvd_zero]
    · refine ⟨monomial (j - i) d, ?_⟩
      rw [monomial_mul, add_tsub_cancel_of_le hij]

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

Goal state before:
pp: case e_a
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ ∀ x ∈ s, x ∉ f.support → (f x)! = 1

Tactic:
grind [Nat.factorial_eq_one]

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

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable I l f μ.toBoxAdditive.toSMul

Tactic:
apply integrable_of_bounded_and_ae_continuousWithinAt

Goal state after:
case hb
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C

case hc
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
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
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ X i ∣ p * q - p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)

Tactic:
← hp

Goal state after:
case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ X i ∣
    (p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1)) * q -
      p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: 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
⊢ (eval x) p = (eval (Function.extend f x g)) ((rename f) p)

pp: 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
⊢ Function.extend f x g i ∈ s i

Tactic:
· simp only [eval, eval₂Hom_rename, Function.extend_comp hf]

Goal state after:
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
⊢ Function.extend f x g i ∈ s i
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommMonoid α
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
⊢ ((x :: l).toFinsupp.sum fun x a ↦ a) = (x :: l).sum

Tactic:
simp only [toFinsupp_cons_eq_single_add_embDomain, sum_cons]

Goal state after:
α : Type u_1
inst✝¹ : AddCommMonoid α
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
⊢ ((Finsupp.single 0 x + Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp).sum fun x a ↦ a) = x + l.sum
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
hl : l.bRiemann = false
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
ε0' : 0 < ε / 2
H0 : 0 < 2 ^ Fintype.card ι
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : B I * ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
J : Box ι
hJ : J ∈ π.boxes ∧ π.tag J ∉ s
⊢ dist ((vol J) (f (π.tag J))) (g J) ≤ ε' * B J

Tactic:
obtain ⟨hJ, hJs⟩ := hJ

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
hl : l.bRiemann = false
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
ε0' : 0 < ε / 2
H0 : 0 < 2 ^ Fintype.card ι
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : B I * ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
J : Box ι
hJ : J ∈ π.boxes
hJs : π.tag J ∉ s
⊢ dist ((vol J) (f (π.tag J))) (g J) ≤ ε' * B J
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

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

Tactic:
isUnit_iff_dvd_one

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

Goal state before:
pp: α : Type u_1
n✝ n k : ℕ
s : { s // 0 ∉ s }
⊢ (fun s ↦ ⟨map (Fin.succAbove 0) s, ⋯⟩) ((fun s ↦ map (Fin.predAbove 0) ↑s) s) = s

Tactic:
ext1
    simp only [map_map]
    refine (Sym.map_congr fun v hv ↦ ?_).trans (map_id' _)
    exact Fin.succAbove_predAbove (ne_of_mem_of_not_mem hv s.2)

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✝ : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
by
  apply degree_mul_of_mul_leadingCoeff_ne_zero
  simp only [ne_eq, mul_eq_zero, leadingCoeff_eq_zero_iff, not_or]
  tauto

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
⊢ m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

Tactic:
apply m.toSyn.injective
    refine le_antisymm degree_prod_le (m.le_degree ?_)
    simpa [m.coeff_prod_sum_degree, Finset.prod_eq_zero_iff]

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

Goal state before:
pp: case inr
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
⊢ n.factorization p ≤ 1

Tactic:
by_cases hp : p.Prime

Goal state after:
case pos
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
⊢ n.factorization p ≤ 1

case neg
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ n.factorization p ≤ 1
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
⊢ n.factorization p = m.factorization p

Tactic:
by_cases hp : p.Prime

Goal state after:
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
⊢ n.factorization p = m.factorization p

case neg
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : ¬Prime p
⊢ n.factorization p = m.factorization p
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case h
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ₜ : Fin n → R
a✝ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
⊢ #(image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0})) ≤
    #({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0})

Tactic:
exact card_image_le

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

Goal state before:
pp: case a
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) := ⋯
hp' : p' = (finSuccEquiv R n) p
k : ℕ := ⋯
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := ⋯
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ #({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0}) ≤ degreeOf 0 p * ∏ i, #(S i.succ)

Tactic:
calc
          #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ ≠ 0}
            = #{x ∈ S ^^ (n + 1) | eval (tail x) pₖ ≠ 0 ∧ eval x p = 0} := by simp_rw [and_comm]
          _ = #({xₜ ∈ tail S ^^ n | eval xₜ pₖ ≠ 0}.biUnion fun xₜ ↦ image (fun x₀ ↦ (x₀, xₜ))
                {x₀ ∈ S 0 | eval (cons x₀ xₜ) p = 0}) := by
            rw [← filter_filter, filter_piFinset_eq_map_consEquiv S (fun r ↦ eval r pₖ ≠ 0),
              filter_map, card_map, product_eq_biUnion_right, filter_biUnion]
            simp [filter_image]
            rfl
          _ ≤ ∑ xₜ ∈ tail S ^^ n with eval xₜ pₖ ≠ 0,
                #(image (fun x₀ ↦ (x₀, xₜ)) {x₀ ∈ S 0 | eval (cons x₀ xₜ) p = 0}) :=
            card_biUnion_le
          _ ≤ ∑ xₜ ∈ tail S ^^ n with eval xₜ pₖ ≠ 0, #{x₀ ∈ S 0 | eval (cons x₀ xₜ) p = 0} := by
            gcongr; exact card_image_le
          _ ≤ ∑ xₜ ∈ tail S ^^ n with eval xₜ pₖ ≠ 0, p.degreeOf 0 := ?_
          _ ≤ ∑ _xₜ ∈ tail S ^^ n, p.degreeOf 0 := by gcongr; exact filter_subset ..
          _ = p.degreeOf 0 * ∏ i, #(S (.succ i)) := by simp [mul_comm, tail]

Goal state after:
case a
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 fun i ↦ tail S i with (eval xₜ) pₖ ≠ 0, #({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}) ≤
    ∑ xₜ ∈ piFinset fun i ↦ tail S i with (eval xₜ) pₖ ≠ 0, degreeOf 0 p
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
⊢ z ∈ x.val → Irreducible z

Tactic:
hz

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ x.val
⊢ Irreducible z
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
⊢ z ∈ y.val → Irreducible z

Tactic:
hz

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ Irreducible z
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ ∀ x ∈ (normalizedFactors n).toFinset.powerset.val,
    ∀ y ∈ (normalizedFactors n).toFinset.powerset.val, x.val.prod = y.val.prod → x = y

Tactic:
intro x hx y hy h
    rw [← Finset.val_inj, ← Multiset.rel_eq, ← associated_eq_eq]
    rw [← Finset.mem_def, Finset.mem_powerset] at hx hy
    apply UniqueFactorizationMonoid.factors_unique _ _ (associated_iff_eq.2 h)
    · intro z hz
      apply irreducible_of_normalized_factor z
      · rw [← Multiset.mem_toFinset]
        apply hx hz
    · intro z hz
      apply irreducible_of_normalized_factor z
      · rw [← Multiset.mem_toFinset]
        apply hy hz

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

Goal state before:
pp: n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a : ℕ
hn : 0 < s * a
hsa : n = s * a
b : ℕ
hsb : s = b ^ 2
hlts : 0 < s
hlta : 0 < a
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
hsb

Goal state after:
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
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
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.toSyn (m.degree (f - g)) ≤ max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
rw [sub_eq_add_neg]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (f + -g)) ≤ max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))
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.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree (f - g) = m.degree f

Tactic:
rw [sub_eq_add_neg]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree (f + -g) = m.degree f
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.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.leadingCoeff (f - g) = m.leadingCoeff f

Tactic:
rw [sub_eq_add_neg]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.leadingCoeff (f + -g) = m.leadingCoeff f
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

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

Tactic:
dirichletInverse,

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : ¬n = 0
hn1 : ¬n = 1
⊢ (f * { toFun := dirichletInverseFun (⇑f) hf, map_zero' := ⋯ }) n = 1 n
Module: Mathlib.Data.Nat.Factorization.PrimePow

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

Tactic:
simp only [Nat.coprime_zero_left] at hab

Goal state after:
case inl
b : ℕ
hab : b = 1
⊢ {d ∈ (0 * b).divisors | IsPrimePow d} = {d ∈ divisors 0 ∪ b.divisors | IsPrimePow d}
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
⊢ n = b 0 * b 1 * b 2

Tactic:
finMulAntidiag_three b hb

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
⊢ n = n
Module: Mathlib.Algebra.Order.Archimedean.Hom

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁹ : Field α✝
inst✝⁸ : LinearOrder α✝
inst✝⁷ : Field β✝
inst✝⁶ : LinearOrder β✝
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean β
f g : α →+*o β
x : α
h' : f x ≠ g x
h : f x < g x
q : ℚ
hf : f x < f ↑q
hg : g ↑q < g x
⊢ False

Tactic:
exact
      (lt_asymm ((OrderHomClass.mono g).reflect_lt hg) <|
          (OrderHomClass.mono f).reflect_lt hf).elim

Goal state after:
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
    by_contra! ⟨x, h⟩
    have := csSup_le (range_nonempty Nat.cast)
      (forall_mem_range.2 fun m =>
        le_sub_iff_add_le.2 <| le_csSup ⟨x, forall_mem_range.2 h⟩ ⟨m+1, Nat.cast_succ m⟩)
    linarith

Goal state after: