mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : NullMeasurableSet s μ
r : ℝ
hs' : s.Nonempty
⊢ NullMeasurableSet (r • s) μ

Tactic:
obtain rfl | hr := eq_or_ne r 0

Goal state after:
case inr.inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : NullMeasurableSet s μ
hs' : s.Nonempty
⊢ NullMeasurableSet (0 • s) μ

case inr.inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : NullMeasurableSet s μ
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
⊢ NullMeasurableSet (r • s) μ
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : r ≠ 0
⊢ μ (sphere x r) = 0

Tactic:
rcases hr.lt_or_gt with (h | h)

Goal state after:
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : r ≠ 0
h : r < 0
⊢ μ (sphere x r) = 0

case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ μ (sphere x r) = 0
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: case zero
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ J ≤ I, ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun m ↦ (fun J ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
i : ι
⊢ (J 0).upper i - (J 0).lower i = (I.upper i - I.lower i) / 2 ^ 0

Tactic:
simp [J]

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

Goal state before:
pp: case mp
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
⊢ π₁ ≤ π₂ → (∀ J ∈ π₁, ∀ J' ∈ π₂, (↑J ∩ ↑J').Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion

Tactic:
refine fun H => ⟨fun J hJ J' hJ' Hne => ?_, iUnion_mono H⟩
    rcases H hJ with ⟨J'', hJ'', Hle⟩
    rcases Hne with ⟨x, hx, hx'⟩
    rwa [π₂.eq_of_mem_of_mem hJ' hJ'' hx' (Hle hx)]

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

Goal state before:
pp: case mp
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ₁ : J₁ ∈ π
J₂ : Box ι
hJ₂ : J₂ ∈ πi J₁
hJ : J ∈ πi' J₁ J₂
⊢ J ∈ πi' (π.biUnionIndex πi J₂) J₂

Tactic:
rwa [π.biUnionIndex_of_mem hJ₁ hJ₂]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝² : Module.Finite ℤ ↥L
this✝¹ : Module ℚ E
this✝ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
⊢ Fintype.card (Free.ChooseBasisIndex ℤ ↥L) ≤ finrank K E

Tactic:
have : Fintype t := Set.Finite.fintype ((Set.range b).toFinite.subset ht_inc)

Goal state after:
case refine_1
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝³ : Module.Finite ℤ ↥L
this✝² : Module ℚ E
this✝¹ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
⊢ Fintype.card (Free.ChooseBasisIndex ℤ ↥L) ≤ finrank K E
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I J J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π₁ π₂ : Prepartition I
h : Disjoint π₁.iUnion π₂.iUnion
this : ∀ J₁ ∈ π₁, ∀ J₂ ∈ π₂, J₁ ≠ J₂ → Disjoint ↑J₁ ↑J₂
⊢ (↑(π₁.boxes ∪ π₂.boxes)).Pairwise (Disjoint on Box.toSet)

Tactic:
by
      simpa [pairwise_union_of_symm, pairwiseDisjoint]

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

Goal state before:
pp: ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion

Tactic:
by
  simp [disjUnion, Prepartition.iUnion, iUnion_or, iUnion_union_distrib]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case insert
ι : Type u_1
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
a✝ : p ∉ s
ihp : π ⊓ splitMany I s = π.biUnion fun J ↦ splitMany J s
⊢ π ⊓ splitMany I (insert p s) = π.biUnion fun J ↦ splitMany J (insert p s)

Tactic:
simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: case pos
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : T.Nonempty
⊢ ∃ r > 0, K ⊆ S r

pp: case neg
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : ¬T.Nonempty
⊢ ∃ r > 0, K ⊆ S r

Tactic:
· use Tfin.isWF.min T_nonempty, Tb (Tfin.isWF.min_mem T_nonempty)
      intro x hx
      obtain ⟨r, hr⟩ := mem_iUnion.1 (hT hx)
      simp only [mem_iUnion, exists_prop] at hr
      exact (S_antitone _ r (IsWF.min_le Tfin.isWF T_nonempty hr.1)) hr.2

Goal state after:
case neg
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : ¬T.Nonempty
⊢ ∃ r > 0, K ⊆ S r
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ Metric.diam (Set.univ.pi fun i ↦ Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤ 1 / ↑n

Tactic:
refine ENNReal.toReal_le_of_le_ofReal (by positivity) <| Metric.ediam_pi_le_of_le fun i ↦ ?_

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
i : ι
⊢ Metric.ediam (Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤ ENNReal.ofReal (1 / ↑n)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_3
ι : 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 : Box ι
hI : I ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s
⊢ (prepartition n B).tag (box n (index n ((prepartition n B).tag I))) ∈
    (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
prepartition_tag n
      (mem_admissibleIndex_of_mem_box n hB (hs₀ hI.2))

Goal state after:
case refine_3
ι : 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 : Box ι
hI : I ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s
⊢ tag n (index n ((prepartition n B).tag I)) ∈ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
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 ι
π : TaggedPrepartition I
f₁ f₂ : (ι → ℝ) → E
vol₁ vol₂ : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : EqOn f₁ f₂ (Box.Icc I)
hvol : EqOn ⇑vol₁ ⇑vol₂ ↑π.boxes
⊢ integralSum f₁ vol₁ π = integralSum f₂ vol₂ π

Tactic:
unfold integralSum
  refine Finset.sum_congr rfl (fun J hJ ↦ ?_)
  congr 1
  · exact hvol hJ
  exact hf (π.tag_mem_Icc J)

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constLinearEquivOfIsEmpty 1]
⊢ False

Tactic:
set f : (M [⋀^ι]→ₗ[R] R) ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm

Goal state after:
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constLinearEquivOfIsEmpty 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
⊢ False
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg : ∀ x ∈ Box.Icc I, 0 ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
by_cases hgi : Integrable I l g μ.toBoxAdditive.toSMul
  · refine ge_of_tendsto' hgi.hasIntegral fun π => sum_nonneg fun J _ => ?_
    exact mul_nonneg ENNReal.toReal_nonneg (hg _ <| π.tag_mem_Icc _)
  · rw [integral, dif_neg hgi]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
p q : ℕ
hpq : p < q
⊢ (fun x ↦ x ^ p) =o[cobounded R] fun x ↦ x ^ q

Tactic:
by
  rw [← Nat.add_sub_of_le hpq.le]
  simpa [pow_add] using (isBigO_refl (· ^ p) (cobounded R)).mul_isLittleO
    ((isLittleO_const_id_cobounded 1).pow (Nat.sub_pos_of_lt hpq))

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

Goal state before:
pp: E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι ℤ ↥L
s : Set E
hs : NullMeasurableSet s volume
⊢ Fintype.card (Fin (finrank ℝ E)) = Fintype.card ι

Tactic:
Fintype.card_fin,

Goal state after:
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι ℤ ↥L
s : Set E
hs : NullMeasurableSet s volume
⊢ finrank ℝ E = Fintype.card ι
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
⊢ Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, u i) atTop (𝓝 l)

Tactic:
rw [← tendsto_sub_nhds_zero_iff, ← isLittleO_one_iff ℝ]
  have := Asymptotics.isLittleO_sum_range_of_tendsto_zero (tendsto_sub_nhds_zero_iff.2 h)
  apply ((isBigO_refl (fun n : ℕ => (n : ℝ)⁻¹) atTop).smul_isLittleO this).congr' _ _
  · filter_upwards [Ici_mem_atTop 1] with n npos
    have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
    simp only [smul_sub, sum_sub_distrib, sum_const, card_range, sub_right_inj]
    rw [← Nat.cast_smul_eq_nsmul ℝ, smul_smul, inv_mul_cancel₀ nposℝ.ne', one_smul]
  · filter_upwards [Ici_mem_atTop 1] with n npos
    have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
    rw [smul_eq_mul, inv_mul_cancel₀ nposℝ.ne']

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable fun k ↦ 2 ^ k * f (2 ^ k)) ↔ Summable f

Tactic:
have h_succ_diff : SuccDiffBounded 2 (2 ^ ·) := by
    intro n
    simp [pow_succ, mul_two, two_mul]
  convert!
    summable_schlomilch_iff_of_nonneg h_nonneg h_mono (pow_pos zero_lt_two)
      (pow_right_strictMono₀ one_lt_two) two_ne_zero h_succ_diff
  simp [pow_succ, mul_two]

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

Goal state before:
pp: case mpr
k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hx : x ∈ RHS
⊢ x ∈ Ideal.span (⇑(of k G) '' s)

Tactic:
← x.sum_coeff_single

Goal state after:
case mpr
k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hx : x ∈ RHS
⊢ x.coeff.sum single ∈ Ideal.span (⇑(of k G) '' s)
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: case mpr
k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x : k[A]
RHS : Ideal k[A] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hx : x ∈ RHS
⊢ x ∈ Ideal.span (of' k A '' s)

Tactic:
← x.sum_coeff_single

Goal state after:
case mpr
k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x : k[A]
RHS : Ideal k[A] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hx : x ∈ RHS
⊢ x.coeff.sum single ∈ Ideal.span (of' k A '' s)
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
d : σ →₀ ℕ
n : ℕ
⊢ coeff d ((∑ i, X i) ^ n) = ↑(if (d.sum fun x m ↦ m) = n then d.multinomial else 0)

Tactic:
have : (∑ i, X i : MvPolynomial σ R) = ∑ i, (1 : σ → R) i • X i := by simp
  simp [this, coeff_linearCombination_X_pow_of_fintype]

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro.intro.h.inl.fst
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c : α
rc : rα c a
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(c, b)

Tactic:
exact iha c rc ⟨b, hb⟩

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i : ι
hi : Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) i
⊢ ∀ (a : α i), Acc (DFinsupp.Lex r s) (single i a)

Tactic:
induction hi with | _ i _ ih
   =>  _ 

Goal state after:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
⊢ ∀ (a : α i), Acc (DFinsupp.Lex r s) (single i a)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
h : f ∣ g
hg : g ≠ 0
⊢ f.totalDegree ≤ g.totalDegree

Tactic:
obtain ⟨r, rfl⟩ := h

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f r : MvPolynomial σ R
hg : f * r ≠ 0
⊢ f.totalDegree ≤ (f * r).totalDegree
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
⊢ degLex.toSyn (single 0 1 + single 1 1) < degLex.toSyn (single 0 2)

Tactic:
rw [degLex_lt_iff, lt_iff, ofDegLex_toDegLex]

Goal state after:
α : Type u_1
⊢ degree (single 0 1 + single 1 1) < degree (ofDegLex (toDegLex (single 0 2))) ∨
    degree (single 0 1 + single 1 1) = degree (ofDegLex (toDegLex (single 0 2))) ∧
      toLex (single 0 1 + single 1 1) < toLex (ofDegLex (toDegLex (single 0 2)))
Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
⊢ #(s.finsuppAntidiag n) = (#s).multichoose n

Tactic:
simp [card_eq_of_equiv_fintype (finsuppAntidiagEquiv s n), Sym.card_sym_eq_multichoose]

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 : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ m.degree (f ^ n) = n • m.degree f

Tactic:
by
  apply m.toSyn.injective
  apply le_antisymm (m.degree_pow_le n)
  apply le_degree
  rw [mem_support_iff, coeff_pow_nsmul_degree]
  exact hf

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

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

Tactic:
factorization_eq_zero_of_not_prime _ hp

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

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

Tactic:
factorization_eq_zero_of_not_prime _ hp

Goal state after:
case neg
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : ¬Prime p
⊢ 0 = 0
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.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : SemigroupWithZero R
f₁ f₂ f₃ : ArithmeticFunction R
x✝ : ℕ
⊢ ((f₁.pmul f₂).pmul f₃) x✝ = (f₁.pmul (f₂.pmul f₃)) x✝

Tactic:
simp only [pmul_apply, mul_assoc]

Goal state after:
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:
by
  simpa [h] using m.degree_sPolynomial_lt_sup_degree hs

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

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

Tactic:
PNat.mk_coe,

Goal state after:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x, ↑(∏ x_1, x x_1) = n ∧ (fun x_1 ↦ ↑(x x_1)) = f) ↔ ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.Algebra.Order.Antidiag.Nat

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

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

Tactic:
· rintro ⟨f, hf, rfl⟩
    exact ⟨dvd_of_mem_finMulAntidiag hf _, (mem_finMulAntidiag.mp hf).2⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
⊢ BddAbove (cutMap β a)

Tactic:
obtain ⟨q, hq⟩ := exists_rat_gt a
  exact ⟨q, forall_mem_image.2 fun r hr => mod_cast (hq.trans' hr).le⟩

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

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

Tactic:
simp only [Set.SurjOn, Set.subset_def, mem_coe, mem_divisorsAntidiagonal, mem_product,
      Set.mem_image]
    rintro ⟨b1, b2⟩ h
    use ((b1.gcd m, b2.gcd m), (b1.gcd n, b2.gcd n))
    rw [← cop.gcd_mul _, ← cop.gcd_mul _, ← h.1, gcd_mul_gcd_of_coprime_of_mul_eq_mul cop h.1,
      gcd_mul_gcd_of_coprime_of_mul_eq_mul cop.symm _]
    · rw [Ne, mul_eq_zero, not_or] at h
      simp [h.2.1, h.2.2]
    rw [mul_comm n m, h.1]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ disjointed f (i + 1) ⊔ f i = f (i + 1)

Tactic:
simpa only [succ_eq_add_one i] using hf.disjointed_succ_sup i

Goal state after: