mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
⊢ reindex R M (Equiv.refl ι) = Equiv.refl (Orientation R M ι)

Tactic:
Orientation.reindex,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
⊢ Ray.map (AlternatingMap.domDomCongrₗ R (Equiv.refl ι)) = Equiv.refl (Orientation R M ι)
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: 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✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : Orientation R M ι
⊢ x = e.orientation ∨ x = -e.orientation

Tactic:
by
  induction x using Module.Ray.ind with | h x hx =>
  rw [← x.map_basis_ne_zero_iff e] at hx
  rwa [Basis.orientation, ray_eq_iff, neg_rayOfNeZero, ray_eq_iff, x.eq_smul_basis_det e,
    sameRay_neg_smul_left_iff_of_ne e.det_ne_zero hx, sameRay_smul_left_iff_of_ne e.det_ne_zero hx,
    lt_or_lt_iff_ne, ne_comm]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ Nat.casesAuxOn (motive := fun a ↦ 0 = a → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun h ↦
        if hp :
            -rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ =
              rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ then
          AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
        else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun n h ↦
        Eq.rec (motive := fun x x_1 ↦ [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] o ↦ (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯
          (-rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯))
      ⋯ =
    -AlternatingMap.constLinearEquivOfIsEmpty 1

Tactic:
apply if_neg

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ ¬-rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ =
      rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯
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
hb : b.toBasis.orientation ≠ o
⊢ o.volumeForm = -b.toBasis.det

Tactic:
let e : OrthonormalBasis (Fin n.succ) ℝ E := o.finOrthonormalBasis n.succ_pos Fact.out

Goal state after:
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
hb : b.toBasis.orientation ≠ o
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
⊢ o.volumeForm = -b.toBasis.det
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))
⊢ (-o).volumeForm = -o.volumeForm

Tactic:
let e : OrthonormalBasis (Fin n.succ) ℝ E := o.finOrthonormalBasis n.succ_pos Fact.out

Goal state after:
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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
⊢ (-o).volumeForm = -o.volumeForm
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
⊢ K.orthogonalDecomposition x = WithLp.toLp 2 (K.orthogonalProjectionOnto x, Kᗮ.orthogonalProjectionOnto x)

Tactic:
by
  simp [orthogonalDecomposition, orthogonalProjectionOnto_apply_eq_projectionOnto]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
inst✝ : Fact (finrank ℝ F = n + 1)
x : Fin (n + 1) → F
⊢ ((map (Fin (n + 1)) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)

Tactic:
let e : OrthonormalBasis (Fin n.succ) ℝ E := o.finOrthonormalBasis n.succ_pos Fact.out

Goal state after:
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
inst✝ : Fact (finrank ℝ F = n + 1)
x : Fin (n + 1) → F
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
⊢ ((map (Fin (n + 1)) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)
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₁ L₂ : Submodule ℤ E
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
f : (Fin (finrank ℝ E) → ℝ) ≃L[ℝ] E :=
  (EuclideanSpace.equiv (Fin (finrank ℝ E)) ℝ).symm.trans (↑(stdOrthonormalBasis ℝ E).repr).symm
⊢ covolume L₁ volume / covolume L₂ volume = ↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup)

Tactic:
have hf : MeasurePreserving f := (stdOrthonormalBasis ℝ E).measurePreserving_repr_symm.comp
    (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).symm

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
L₁ L₂ : Submodule ℤ E
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
f : (Fin (finrank ℝ E) → ℝ) ≃L[ℝ] E :=
  (EuclideanSpace.equiv (Fin (finrank ℝ E)) ℝ).symm.trans (↑(stdOrthonormalBasis ℝ E).repr).symm
hf : MeasurePreserving (⇑f) volume volume
⊢ covolume L₁ volume / covolume L₂ volume = ↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup)
Module: Mathlib.Analysis.PSeries

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

Tactic:
grw [← le_sum_condensed' hf n, ← sum_range_add_sum_Ico _ n.one_le_two_pow, sum_range_succ,
    sum_range_zero, zero_add]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case h₂
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
⊢ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k) ≤ ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)

Tactic:
have (k : ℕ) : (u (k + 1) - u k : ℝ≥0∞) = (u (k + 1) - (u k : ℕ) : ℕ) := by simp

Goal state after:
case h₂
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(u (k + 1) - u k)
⊢ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k) ≤ ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: case refine_2
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁵ : DiscreteTopology ↥L
inst✝⁴ : IsZLattice ℝ L
ι : Type u_2
inst✝³ : Fintype ι
b : Basis ι ℤ ↥L
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
⊢ Bornology.IsBounded (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)

Tactic:
rw [← NormedSpace.isVonNBounded_iff ℝ] at hs₁ ⊢

Goal state after:
case refine_2
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁵ : DiscreteTopology ↥L
inst✝⁴ : IsZLattice ℝ L
ι : Type u_2
inst✝³ : Fintype ι
b : Basis ι ℤ ↥L
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set E
hs₁ : IsVonNBounded ℝ s
hs₂ : MeasurableSet s
hs₃ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
⊢ IsVonNBounded ℝ (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: p : ℕ
⊢ (Summable fun n ↦ (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
by
  simp only [← rpow_natCast, summable_nat_rpow_inv, Nat.one_lt_cast]

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁶ : DiscreteTopology ↥L
inst✝⁵ : IsZLattice ℝ L
ι : Type u_2
inst✝⁴ : Fintype ι
b : Basis ι ℤ ↥L
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nonempty ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0
⊢ Tendsto (fun c ↦ ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) atTop
    (𝓝 (volume.real (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})))

Tactic:
by
  refine Tendsto.congr' ?_ <| (tendsto_card_div_pow_atTop_volume'
      ((b.ofZLatticeBasis ℝ).equivFun '' {x ∈ X | F x ≤ 1}) ?_ ?_ h₄ fun x y hx hy ↦ ?_).comp
        (tendsto_rpow_atTop <| inv_pos.mpr
          (Nat.cast_pos.mpr card_pos) : Tendsto (fun x ↦ x ^ (card ι : ℝ)⁻¹) atTop atTop)
  · filter_upwards [eventually_gt_atTop 0] with c hc
    have aux₁ : (card ι : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr card_ne_zero
    have aux₂ : 0 < c ^ (card ι : ℝ)⁻¹ := Real.rpow_pos_of_pos hc _
    have aux₃ : (c ^ (card ι : ℝ)⁻¹)⁻¹ ≠ 0 := inv_ne_zero aux₂.ne'
    have aux₄ : c ^ (-(card ι : ℝ)⁻¹) ≠ 0 := (Real.rpow_pos_of_pos hc _).ne'
    obtain ⟨hc₁, hc₂⟩ := lt_iff_le_and_ne.mp hc
    rw [Function.comp_apply, ← Real.rpow_natCast, Real.rpow_inv_rpow hc₁ aux₁, eq_comm]
    congr
    refine Nat.card_congr <| Equiv.subtypeEquiv ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.trans
          (Equiv.smulRight aux₄)) fun _ ↦ ?_
    rw [Set.mem_inter_iff, Set.mem_inter_iff, Equiv.trans_apply, LinearEquiv.coe_toEquiv,
      Equiv.smulRight_apply, Real.rpow_neg hc₁, Set.smul_mem_smul_set_iff₀ aux₃,
      ← Set.mem_smul_set_iff_inv_smul_mem₀ aux₂.ne', ← image_smul_set,
      tendsto_card_le_div''_aux hX h₁ aux₂, ← Real.rpow_natCast, ← Real.rpow_mul hc₁,
      inv_mul_cancel₀ aux₁, Real.rpow_one]
    simp_rw [SetLike.mem_coe, Set.mem_image, EmbeddingLike.apply_eq_iff_eq, exists_eq_right,
      and_congr_right_iff, ← b.ofZLatticeBasis_span ℝ, Basis.mem_span_iff_repr_mem,
      Pi.basisFun_repr, Basis.equivFun_apply, implies_true]
  · rw [← NormedSpace.isVonNBounded_iff ℝ] at h₂ ⊢
    exact Bornology.IsVonNBounded.image h₂ ((b.ofZLatticeBasis ℝ).equivFunL : E →L[ℝ] ι → ℝ)
  · exact (b.ofZLatticeBasis ℝ).equivFunL.toHomeomorph.toMeasurableEquiv.measurableSet_image.mpr h₃
  · simp_rw [← image_smul_set]
    apply Set.image_mono
    rw [tendsto_card_le_div''_aux hX h₁ hx,
      tendsto_card_le_div''_aux hX h₁ (lt_of_lt_of_le hx hy)]
    exact fun a ⟨ha₁, ha₂⟩ ↦ ⟨ha₁, le_trans ha₂ <| pow_le_pow_left₀ (le_of_lt hx) hy _⟩

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

Goal state before:
pp: case e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
k : ℕ
⊢ 2 * ↑d * (3 ^ (d - 1) * (↑k + 1) ^ (d - 1)) * ((↑k + 1) ^ r * ε ^ r) =
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * ((↑k + 1) ^ (d - 1) * (↑k + 1) ^ r)

Tactic:
group

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

Goal state before:
pp: case e_a.e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
k : ℕ
⊢ (↑k + 1) ^ (↑(d - 1) + r) = ↑(k + 1) ^ (↑d - 1 + r)

Tactic:
Nat.cast_sub hd

Goal state after:
case e_a.e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
k : ℕ
⊢ (↑k + 1) ^ (↑d - ↑1 + r) = ↑(k + 1) ^ (↑d - 1 + r)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ ((f a).succ + (f b).succ).choose (f a).succ =
    ((f a).succ + if b = a then (f a).succ else f b).choose (f a).succ + (f a + (f b).succ).choose (f a)

Tactic:
if_neg h.symm

Goal state after:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ ((f a).succ + (f b).succ).choose (f a).succ = ((f a).succ + f b).choose (f a).succ + (f a + (f b).succ).choose (f a)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
j : α
hj : j ∈ Multiset.replicate (↑m) x
⊢ ¬x ≠ j

Tactic:
simp [Multiset.mem_replicate.mp hj]

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

Goal state before:
pp: case right
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
hb : b ∣ r
hp : p = b • (monomial (Finsupp.single i 1)) 1
⊢ p = (monomial (Finsupp.single i 1)) b

Tactic:
simp [hp, smul_monomial]

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
i : σ
a✝ : Nontrivial R
r : R
⊢ r ∣ 1 ∧ (p = C r ∨ p = r • X i) ↔ IsUnit r ∧ (p = C r ∨ p = r • 1 • X i)

Tactic:
rw [isUnit_iff_dvd_one, one_smul]

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
⊢ m.toSyn (m.degree (f * g)) ≤ m.toSyn (m.degree f + m.degree g)

Tactic:
by
  classical
  rw [degree_le_iff]
  intro c
  rw [← not_lt, mem_support_iff, not_imp_not]
  intro hc
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  rintro ⟨d, e⟩ hde
  simp only [Finset.mem_antidiagonal] at hde
  dsimp only
  by_cases hd : m.degree f ≺[m] d
  · rw [m.coeff_eq_zero_of_lt hd, zero_mul]
  · suffices m.degree g ≺[m] e by
      rw [m.coeff_eq_zero_of_lt this, mul_zero]
    simp only [not_lt] at hd
    apply lt_of_add_lt_add_left (a := m.toSyn d)
    grw [← map_add _ _ e, hd, ← map_add, hde]
    exact hc

Goal state after:
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring L
⊢ ∀ (x y z : L),
    associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y

Tactic:
by
    suffices ∀ a b c : L, associator a b c = 0 by simp
    simp

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: case succ.succ
a n✝ : ℕ
h : DvdNotUnit (a + 1) (n✝ + 1)
h1 : a + 1 ∣ n✝ + 1
h2 : ¬n✝ + 1 ∣ a + 1
con : a + 1 = n✝ + 1
⊢ n✝ + 1 ∣ a + 1

Tactic:
rw [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 : ℕ
⊢ coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n

Tactic:
by
  induction n with
  | zero => simp
  | succ n hrec =>
    simp only [add_smul, one_smul, pow_add, pow_one]
    rw [m.coeff_mul_of_add_of_degree_le (m.degree_pow_le _) le_rfl, hrec, leadingCoeff]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
⊢ m.leadingTerm ((monomial s) c) = (monomial s) c

Tactic:
by
  classical
  by_cases h : c = 0 <;> simp [leadingTerm, degree_monomial, h]

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
this :
  ∀ (f : MvPolynomial σ ?m.74) (g : MvPolynomial σ (?m.96 f)),
    m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f
⊢ m.sPolynomial f g =
    (monomial (m.degree f ⊔ m.degree g - m.degree f)) (m.leadingCoeff g) * f -
      (monomial (m.degree f ⊔ m.degree g - m.degree g)) (m.leadingCoeff f) * g

Tactic:
by
    rw [sPolynomial, this, this, sup_comm]

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

Goal state before:
pp: n : ℕ
⊢ (∃ p k, 0 < k ∧ n.factorization = Finsupp.single p k) ↔ n.factorization.support.card = 1

Tactic:
Finsupp.card_support_eq_one',

Goal state after:
n : ℕ
⊢ (∃ p k, 0 < k ∧ n.factorization = Finsupp.single p k) ↔ ∃ a b, b ≠ 0 ∧ n.factorization = Finsupp.single a b
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
⊢ (pow k) n = if k = 0 ∧ n = 0 then 0 else n ^ k

Tactic:
cases k

Goal state after:
case zero
n : ℕ
⊢ (pow 0) n = if 0 = 0 ∧ n = 0 then 0 else n ^ 0

case succ
n n✝ : ℕ
⊢ (pow (n✝ + 1)) n = if n✝ + 1 = 0 ∧ n = 0 then 0 else n ^ (n✝ + 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

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

Tactic:
cases k

Goal state after:
case pos.zero
m : ℕ
hm : m = 0
⊢ Ω (m ^ 0) = 0 * Ω m

case pos.succ
m : ℕ
hm : m = 0
n✝ : ℕ
⊢ Ω (m ^ (n✝ + 1)) = (n✝ + 1) * Ω m
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case refine_2
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 0 * a 1, a 0 * a 2).2 ∣ a 0 * a 1 * a 2

pp: case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ match (a 0 * a 1, a 0 * a 2) with
  | (x, y) => x.lcm y = a 0 * a 1 * a 2

Tactic:
· use a 1; ring

Goal state after:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ match (a 0 * a 1, a 0 * a 2) with
  | (x, y) => x.lcm y = a 0 * a 1 * a 2
Module: Mathlib.Algebra.Order.Archimedean.Hom

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : α →+*o α
x : α
⊢ f x = x

Tactic:
rw [f.eq_id]; rfl

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Hom

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedAddMonoid R
inst✝³ : Ring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedAddMonoid S
inst✝ : PosMulMono S
hR : ∀ (r : R), 0 ≤ r → IsSquare r
f : R →+* S
s : R
h : 0 ≤ s * s
⊢ 0 ≤ f (s * s)

Tactic:
rw [map_mul]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedAddMonoid R
inst✝³ : Ring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedAddMonoid S
inst✝ : PosMulMono S
hR : ∀ (r : R), 0 ≤ r → IsSquare r
f : R →+* S
s : R
h : 0 ≤ s * s
⊢ 0 ≤ f s * f s
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ m * n ≠ 0
⊢ ((((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2 = m ∧ m ≠ 0) ∧
      ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2 = n ∧ n ≠ 0) ∧
    (((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.1,
        ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2) =
      (b1, b2)

Tactic:
← cop.gcd_mul _,

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ m * n ≠ 0
⊢ ((((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2 = m ∧ m ≠ 0) ∧
      ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2 = n ∧ n ≠ 0) ∧
    (b1.gcd (m * n), ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2) =
      (b1, b2)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ m * n ≠ 0
⊢ ((((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2 = m ∧ m ≠ 0) ∧
      ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2 = n ∧ n ≠ 0) ∧
    (b1.gcd (m * n), ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2) =
      (b1, b2)

Tactic:
← cop.gcd_mul _,

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ m * n ≠ 0
⊢ ((((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2 = m ∧ m ≠ 0) ∧
      ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2 = n ∧ n ≠ 0) ∧
    (b1.gcd (m * n), b2.gcd (m * n)) = (b1, b2)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ x.lcm y ≠ 0

Tactic:
by assumption

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ x.gcd y ≠ 0

Tactic:
by assumption

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ x ≠ 0

Tactic:
by assumption

Goal state after: