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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ a.toBasis.toMatrix ⇑b ∈ Matrix.unitaryGroup ι 𝕜

Tactic:
by
  rw [Matrix.mem_unitaryGroup_iff']
  exact a.toMatrix_orthonormalBasis_conjTranspose_mul_self b

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
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)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
r_top : ¬r = ∞
⊢ ∃ i, 0 < i ∧ x ∈ S i

Tactic:
· obtain ⟨r', hr'⟩ := exists_between (toReal_pos (ne_of_gt r0) r_top)
      use r', hr'.1, r.toReal, hr'.2, this r.toReal ofReal_toReal_le

Goal state after:
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 ι
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
⊢ f j ∈ (𝕜 ∙ (gramSchmidtOrthonormalBasis h f) i)ᗮ

Tactic:
suffices span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ 𝕜 ∙ gramSchmidtOrthonormalBasis h f i by
    apply this
    rw [span_gramSchmidtNormed]
    exact mem_span_gramSchmidt 𝕜 f le_rfl

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : WellFoundedLT ι
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
⊢ span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ 𝕜 ∙ (gramSchmidtOrthonormalBasis h f) i
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : PartialOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ b.det = AlternatingMap.constLinearEquivOfIsEmpty 1

Tactic:
exact b.det_isEmpty

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case hf₁
b : ℝ
hb : 1 < b
⊢ Summable fun n ↦ |↑n| ^ (-b)

Tactic:
fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))

Goal state after:
case hf₁
b : ℝ
hb : 1 < b
⊢ Summable fun n ↦ ↑n ^ (-b)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n ↦ |↑n| ^ (-b)

Tactic:
fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))

Goal state after:
case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n ↦ ↑n ^ (-b)
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: case hnc
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : ((indicator a.support fun i x_1 ↦ x i).sum fun x m ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
⊢ ((indicator a.support fun i x_1 ↦ x i).sum fun x m ↦ m) = n

Tactic:
rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]

Goal state after:
case hnc
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : ((indicator a.support fun i x_1 ↦ x i).sum fun x m ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
⊢ ∑ x_1 ∈ a.support, (indicator a.support fun i x_2 ↦ x i) x_1 = a.support.sum x
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case inr.succ.refine_1
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hp : p ∣ (monomial n') 1 * X i * q
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : Finsupp.degree n' = d
⊢ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r

Tactic:
mul_comm _ (X i),

Goal state after:
case inr.succ.refine_1
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hp : p ∣ X i * (monomial n') 1 * q
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : Finsupp.degree n' = d
⊢ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
⊢ ∃ a',
    InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧
      (fun x ↦ x.2.1.piecewise x.2.2 x.1) a' = x

Tactic:
refine ⟨⟨{ j | r j i → j ∈ p }, piecewise x₁ x { j | r j i }, x₂⟩,
      .fst ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩ <;> simp only [piecewise_apply, Set.mem_ofPred_eq]

Goal state after:
case pos.refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
hj : r j i
⊢ (if r j i then x₁ j else x j) = x₁ j

case pos.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
⊢ s i (if r i i then x₁ i else x i) (x₁ i)

case pos.refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
⊢ (x₁.piecewise x {j | r j i}).piecewise x₂ {j | r j i → j ∈ p} = x
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
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
⊢ Fibration (InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd) (DFinsupp.Lex r s) fun x ↦
    x.2.1.piecewise x.2.2 x.1

Tactic:
rintro ⟨p, x₁, x₂⟩ x ⟨i, hr, hs⟩
  simp_rw [piecewise_apply] at hs hr
  split_ifs at hs with hp
  · refine ⟨⟨{ j | r j i → j ∈ p }, piecewise x₁ x { j | r j i }, x₂⟩,
      .fst ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩ <;> simp only [piecewise_apply, Set.mem_ofPred_eq]
    · simp only [if_pos hj]
    · split_ifs with hi
      · rwa [hr i hi, if_pos hp] at hs
      · assumption
    · ext1 j
      simp only [piecewise_apply, Set.mem_ofPred_eq]
      split_ifs with h₁ h₂ <;> try rfl
      · rw [hr j h₂, if_pos (h₁ h₂)]
      · rw [Classical.not_imp] at h₁
        rw [hr j h₁.1, if_neg h₁.2]
  · refine ⟨⟨{ j | r j i ∧ j ∈ p }, x₁, piecewise x₂ x { j | r j i }⟩,
      .snd ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩ <;> simp only [piecewise_apply, Set.mem_ofPred_eq]
    · exact if_pos hj
    · split_ifs with hi
      · rwa [hr i hi, if_neg hp] at hs
      · assumption
    · ext1 j
      simp only [piecewise_apply, Set.mem_ofPred_eq]
      split_ifs with h₁ h₂ <;> try rfl
      · rw [hr j h₁.1, if_pos h₁.2]
      · rw [hr j h₂, if_neg]
        simpa [h₂] using h₁

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ m.degree 1 = 0

Tactic:
classical rw [MvPolynomial.one_def, degree_monomial]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ (if 1 = 0 then 0 else 0) = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
Monic,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ m.leadingCoeff ((monomial d) c) = 1 ↔ c = 1
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : d = 0
⊢ coeff d f = coeff d (C (coeff 0 f))

Tactic:
simp [hd]

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
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ m.Monic (f * g)

Tactic:
Monic,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ m.leadingCoeff (f * g) = 1
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.Monic f
a✝ : Nontrivial R
⊢ m.Monic (f ^ n)

Tactic:
Monic,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.Monic f
a✝ : Nontrivial R
⊢ m.leadingCoeff (f ^ n) = 1
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ m.Monic (∏ i ∈ s, P i)

Tactic:
Monic,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ m.leadingCoeff (∏ i ∈ s, P i) = 1
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
p : MvPolynomial σ R
⊢ m.Monic p

Tactic:
by
  simp [Subsingleton.eq_one (α := MvPolynomial σ R)]

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

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : g ≠ 0
hf : f ≠ 0
⊢ m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0

Tactic:
simp [withBotDegree_eq, hf, hg, toWithBotSyn_apply]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#S)) = ↑p.totalDegree / ↑(#S)

Tactic:
simp_rw [totalDegree, Nat.cast_finsetSup]

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#S)) = (p.support.sup fun i ↦ ↑(i.sum fun x e ↦ e)) / ↑(#S)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

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

Tactic:
simp_all [← map_div_left_divisors, sum_eq_single 1]

Goal state after:
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
⊢ (f * dirichletInverse (⇑f) hf) n = 1 n

Tactic:
by_cases hn1 : n = 1

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

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
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
h : Ω n = 1
⊢ Nat.Prime n

Tactic:
cases n with | zero => simp at h | succ n =>
  rcases List.length_eq_one_iff.1 h with ⟨x, hx⟩
  rw [← prod_primeFactorsList n.add_one_ne_zero, hx, List.prod_singleton]
  apply prime_of_mem_primeFactorsList
  rw [hx, List.mem_singleton]

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

Goal state before:
pp: N : ℕ
⊢ ∑ n ∈ Ioc 0 N, zeta n = N

Tactic:
simp only [zeta_apply, sum_ite, sum_const_zero, sum_const, smul_eq_mul, mul_one, zero_add]

Goal state after:
N : ℕ
⊢ #({x ∈ Ioc 0 N | ¬x = 0}) = N
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.Monic (X i + C (-r))

Tactic:
apply monic_X_add_C

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (n + 1 + 1) = (∑ i ∈ s, f i) ^ (n + 1) * ∑ i ∈ s, f i

Tactic:
pow_succ

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (n + 1) * ∑ i ∈ s, f i = (∑ i ∈ s, f i) ^ (n + 1) * ∑ i ∈ s, f i
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case refine_1
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
ha : a ≠ 1
x✝ : mk a ≤ mk b
n : ℕ
hn : |MulArchimedeanOrder.val (MulArchimedeanOrder.of b)|ₘ ≤ |MulArchimedeanOrder.val (MulArchimedeanOrder.of a)|ₘ ^ n
⊢ |MulArchimedeanOrder.val (MulArchimedeanOrder.of a)|ₘ ^ n < |a|ₘ ^ (n + 1)

Tactic:
pow_succ

Goal state after:
case refine_1
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
ha : a ≠ 1
x✝ : mk a ≤ mk b
n : ℕ
hn : |MulArchimedeanOrder.val (MulArchimedeanOrder.of b)|ₘ ≤ |MulArchimedeanOrder.val (MulArchimedeanOrder.of a)|ₘ ^ n
⊢ |MulArchimedeanOrder.val (MulArchimedeanOrder.of a)|ₘ ^ n < |a|ₘ ^ n * |a|ₘ
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case insert.inr.refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
x : ι
hx : ¬x = (Equiv.symm σ) a ∧ x ∈ s
⊢ f x • g (σ x) = f x • g ((Equiv.swap a (σ a)) (σ x))

Tactic:
eq_symm_apply

Goal state after:
case insert.inr.refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
x : ι
hx : ¬σ x = a ∧ x ∈ s
⊢ f x • g (σ x) = f x • g ((Equiv.swap a (σ a)) (σ x))
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
hk : (f ^ k).IsMultiplicative
⊢ (f ^ (k + 1)).IsMultiplicative

Tactic:
pow_succ

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
hk : (f ^ k).IsMultiplicative
⊢ (f ^ k * f).IsMultiplicative
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
⊢ (orderHom f) ⊤ = ⊤

Tactic:
rw [← mk_one, ← mk_one, orderHom_mk, map_one]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : (i : ι) → AddCommMonoid (π i)
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → SMulZeroClass α (π i)
inst✝ : (i : ι) → FloorDiv α (π i)
a : α
ha : a ≤ 0
f : (i : ι) → π i
⊢ (fun i ↦ f i ⌊/⌋ a) = 0

Tactic:
by ext i; exact floorDiv_of_nonpos ha _

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : (i : ι) → AddCommMonoid (π i)
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → SMulZeroClass α (π i)
inst✝ : (i : ι) → CeilDiv α (π i)
a : α
⊢ (fun i ↦ 0 i ⌈/⌉ a) = 0

Tactic:
ext; exact zero_ceilDiv _

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : FloorDiv α β
f✝ : ι →₀ β
a✝ a : α
ha : a ≤ 0
f : ι →₀ β
⊢ mapRange (fun x ↦ x ⌊/⌋ a) ⋯ f = 0

Tactic:
by ext i; exact floorDiv_of_nonpos ha _

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : CeilDiv α β
f : ι →₀ β
a✝ a : α
⊢ mapRange (fun x ↦ x ⌈/⌉ a) ⋯ 0 = 0

Tactic:
ext; exact zero_ceilDiv _

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
n : ℕ∞
hn : n ≠ ⊤
⊢ n < ⌊r⌋ₑ ↔ ↑n + 1 ≤ r

Tactic:
simp [← add_one_le_iff hn]

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

Goal state before:
pp: case inl
M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
x : M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
hx : 1 < x
y : M
hy : 1 < y
hyx✝ : y < x
hyx : y ^ 2 ≤ x
⊢ ∃ y, 1 < y ∧ y ^ 2 ≤ x

pp: case inr
M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
x : M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
hx : 1 < x
y : M
hy : 1 < y
hyx : y < x
hxy : x ≤ y ^ 2
⊢ ∃ y, 1 < y ∧ y ^ 2 ≤ x

Tactic:
· exact ⟨y, hy, hyx⟩

Goal state after:
case inr
M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
x : M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
hx : 1 < x
y : M
hy : 1 < y
hyx : y < x
hxy : x ≤ y ^ 2
⊢ ∃ y, 1 < y ∧ y ^ 2 ≤ x
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a < b
⊢ insert (a + 1) (Ioc (a + 1) b) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using insert_Ioc_succ_left_eq_Ioc h

Goal state after:
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
s t : Interval α
⊢ ↑s ⊓ ↑t ⊆ ⊥ ↔ s ⊓ t ≤ ⊥

Tactic:
← coe_subset_coe,

Goal state after:
α : Type u_1
inst✝ : Lattice α
s t : Interval α
⊢ ↑s ⊓ ↑t ⊆ ⊥ ↔ ↑(s ⊓ t) ⊆ ↑⊥
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s t : Interval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
⊢ ∀ (a b : Interval α), -(a + b) = -b + -a

Tactic:
rintro (_ | s) (_ | t) <;> first | rfl | exact congr_arg WithBot.some (neg_add_rev _ _)

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Lex (Γ × Γ')⟧
⊢ (Function.support fun g ↦ { coeff := fun g' ↦ x.coeff (g, g'), isPWO_support' := ⋯ }).IsPWO

Tactic:
have h₁ : (Function.support fun g => HahnSeries.mk (fun g' => x.coeff (g, g'))
        (Set.PartiallyWellOrderedOn.fiberProdLex x.isPWO_support' g)) = Function.support
        fun g => fun g' => x.coeff (g, g') := by
      simp only [Function.support, ne_eq, mk_eq_zero]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Lex (Γ × Γ')⟧
h₁ :
  (Function.support fun g ↦ { coeff := fun g' ↦ x.coeff (g, g'), isPWO_support' := ⋯ }) =
    Function.support fun g g' ↦ x.coeff (g, g')
⊢ (Function.support fun g ↦ { coeff := fun g' ↦ x.coeff (g, g'), isPWO_support' := ⋯ }).IsPWO
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Zero R
Γ : Type u_5
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
⊢ x.orderTop ≤ ↑g

Tactic:
by
  rw [orderTop_of_ne_zero (ne_zero_of_coeff_ne_zero h), WithTop.coe_le_coe]
  exact Set.IsWF.min_le _ _ ((mem_support _ _).2 h)

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

Goal state before:
pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
simp_rw [leadingCoeff_of_ne_zero h, leadingCoeff_of_ne_zero hx, ho, coeff_add]
    rw [coeff_eq_zero_of_lt_orderTop (x := y) (by simpa using hxy), add_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
x : G
hx : (orderAddMonoidHom G).toAddMonoidHom x = 1
⊢ Function.Surjective ⇑(orderAddMonoidHom G)

Tactic:
exact fun a ↦ ⟨a • x, by simp_all⟩

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case h.mp
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this : 0 ≤ ↑b
x : G
⊢ 0 ≤ x ∧ x < ↑b → x = 0

Tactic:
rintro ⟨h₁, h₂⟩
    by_contra hx'
    have := b.2
    simp only [Finset.mem_Icc] at this
    exact hb.2 (c := ⟨x, by simpa [h₁] using! h₂.le.trans this.2⟩)
      (lt_of_le_of_ne h₁ (by simpa using! Ne.symm hx')) h₂

Goal state after: