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

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
hb : b.toBasis.orientation ≠ o
⊢ o.volumeForm = -b.toBasis.det

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:
· classical
      have : positiveOrientation ≠ o := by rwa [b.toBasis.orientation_isEmpty] at hb
      simp_rw [volumeForm, Or.by_cases, dif_neg this.symm, Nat.rec_zero, Basis.det_isEmpty]

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
⊢ o.volumeForm = -b.toBasis.det
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: U : Type u_4
V : Type u_5
inst✝⁹ : NormedAddCommGroup U
inst✝⁸ : InnerProductSpace ℝ U
inst✝⁷ : MeasurableSpace U
inst✝⁶ : BorelSpace U
inst✝⁵ : FiniteDimensional ℝ U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
this : MeasurePreserving (⇑(volumePreservingSymmMeasurableEquivToLpProdAux U V)) volume volume
⊢ MeasurePreserving (⇑(MeasurableEquiv.toLp 2 (U × V)).symm) volume volume

Tactic:
by
    convert! this
    ext uv
    <;> simp [volumePreservingSymmMeasurableEquivToLpProdAux, MeasurableEquiv.coe_sumPiEquivProdPi,
      MeasurableEquiv.prodCongr]

Goal state after:
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n ↦ m * n + k
hg : Function.Injective g
n : ℕ
hn : n ∉ range g
⊢ {n | ↑n = ↑k ∧ k ≤ n}.indicator f n = 0

Tactic:
contrapose! hn

Goal state after:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n ↦ m * n + k
hg : Function.Injective g
n : ℕ
hn : {n | ↑n = ↑k ∧ k ≤ n}.indicator f n ≠ 0
⊢ n ∈ range g
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x ↦ ‖u x‖) l atTop
c : ℝ
hc : c > 0
hcuv : IsBigOWith c l u v
⊢ Tendsto (fun x ↦ ‖v x‖) l atTop

Tactic:
IsBigOWith

Goal state after:
𝕜 : Type u_1
inst✝ : NormedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x ↦ ‖u x‖) l atTop
c : ℝ
hc : c > 0
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
⊢ Tendsto (fun x ↦ ‖v x‖) l atTop
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
h_pow : Filter.Tendsto (fun n ↦ 2 ^ n) Filter.atTop Filter.atTop
a✝ : ℕ
hk : n + m ≤ 2 ^ a✝
⊢ 2 ^ a✝ * f (2 ^ a✝) = 2 ^ a✝ * f (max (2 ^ a✝) (n + m))

Tactic:
simp [max_eq_left hk]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
a✝ : ℕ
hk : n + m ≤ a✝
⊢ f a✝ = f (max a✝ (n + m))

Tactic:
simp [max_eq_left hk]

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
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
aux₂ : 0 < c ^ (↑(card ι))⁻¹
aux₃ : (c ^ (↑(card ι))⁻¹)⁻¹ ≠ 0
aux₄ : c ^ (-(↑(card ι))⁻¹) ≠ 0
hc₁ : 0 ≤ c
hc₂ : 0 ≠ c
⊢ ((fun x ↦
          ↑(Nat.card
                ↑(⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1} ∩
                    x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) /
            x ^ card ι) ∘
        fun x ↦ x ^ (↑(card ι))⁻¹)
      c =
    ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c

Tactic:
rw [Function.comp_apply, ← Real.rpow_natCast, Real.rpow_inv_rpow hc₁ aux₁, eq_comm]

Goal state after:
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
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
aux₂ : 0 < c ^ (↑(card ι))⁻¹
aux₃ : (c ^ (↑(card ι))⁻¹)⁻¹ ≠ 0
aux₄ : c ^ (-(↑(card ι))⁻¹) ≠ 0
hc₁ : 0 ≤ c
hc₂ : 0 ≠ c
⊢ ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c =
    ↑(Nat.card
          ↑(⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1} ∩
              (c ^ (↑(card ι))⁻¹)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) /
      c
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inr
p : ℝ
hp : p < 0
h : Summable fun n ↦ (↑n ^ p)⁻¹
k : ℕ
hk₁ : (↑k ^ p)⁻¹ < 1
hk₀ : k ≠ 0
⊢ False

Tactic:
apply hk₀

Goal state after:
case inr
p : ℝ
hp : p < 0
h : Summable fun n ↦ (↑n ^ p)⁻¹
k : ℕ
hk₁ : (↑k ^ p)⁻¹ < 1
hk₀ : k ≠ 0
⊢ k = 0
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
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
r : ℝ
hr : r < -↑d
e : (I → ℤ) ≃ₗ[ℤ] ↥L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I).symm
u : Finset (I → ℤ)
⊢ ∃ n, u ⊆ Fintype.piFinset fun x ↦ Finset.Icc (-↑n) ↑n

Tactic:
obtain ⟨r, hr, hr'⟩ := u.finite_toSet.isCompact.isBounded.subset_closedBall_lt 0 0
      refine ⟨⌊r⌋.toNat, fun x hx ↦ ?_⟩
      have hr'' : ⌊r⌋ ⊔ 0 = ⌊r⌋ := by rw [sup_eq_left]; positivity
      have := hr' hx
      simp only [Metric.mem_closedBall, dist_zero_right, pi_norm_le_iff_of_nonneg hr.le,
        Int.norm_eq_abs, ← Int.cast_abs, ← Int.le_floor] at this
      simpa only [Int.ofNat_toNat, Fintype.mem_piFinset, Finset.mem_Icc, ← abs_le, hr'']

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: case append_singleton
R : Type u_2
inst✝ : AddMonoid R
x : List R
xs : R
ih : ∀ [inst : DecidablePred fun x_1 ↦ x.getD x_1 0 ≠ 0], x.toFinsupp = (mapIdx (fun n r ↦ Finsupp.single n r) x).sum
⊢ ∀ [inst : DecidablePred fun x_1 ↦ (x ++ [xs]).getD x_1 0 ≠ 0],
    (x ++ [xs]).toFinsupp = (mapIdx (fun n r ↦ Finsupp.single n r) (x ++ [xs])).sum

Tactic:
simp [toFinsupp_concat_eq_toFinsupp_add_single, sum_append, ih]

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

Goal state before:
pp: k : ℕ
⊢ (k + 1).succ * (k + 1)! = (k + 2) * k‼ * (k + 1)‼

Tactic:
factorial_eq_mul_doubleFactorial _,

Goal state after:
k : ℕ
⊢ (k + 1).succ * ((k + 1)‼ * k‼) = (k + 2) * k‼ * (k + 1)‼
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : f a = 0
⊢ Nat.multinomial f.support ⇑f = (f.sum fun x ↦ id).choose 0 * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)

Tactic:
Nat.choose_zero_right,

Goal state after:
case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : f a = 0
⊢ Nat.multinomial f.support ⇑f = 1 * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)
Module: Mathlib.Algebra.MvPolynomial.Polynomial

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

Tactic:
intro p q hp hq

Goal state after:
case add
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p✝ p q : MvPolynomial σ R
hp : Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p
hq : Polynomial.eval x (eval₂ f g q) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) q
⊢ Polynomial.eval x (eval₂ f g (p + q)) =
    eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p + q)
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)
hr : WellFounded (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2)
x : Π₀ (i : ι), α i
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
by classical exact Lex.acc hbot hs x fun i _ => hr.apply i

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
h : a + b ≤ a + c
⊢ b ≤ c

Tactic:
rw [le_iff] at h ⊢
    simpa only [ofDegLex_add, map_add, add_lt_add_iff_left, add_right_inj, toLex_add,
      add_le_add_iff_left] using h

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

Goal state before:
pp: case mp
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
⊢ (monomial m) b = C b ∨ (monomial m) b = b • (monomial (Finsupp.single i 1)) 1

Tactic:
suffices m = 0 ∨ m = Finsupp.single i 1 by
      apply this.imp <;> simp +contextual [smul_monomial, smul_eq_mul, mul_one]

Goal state after:
case mp
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
⊢ m = 0 ∨ m = Finsupp.single i 1
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 + 1) → R
a✝ : x ∈ piFinset fun i ↦ S i
⊢ (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0 → (eval (tail x)) pₖ = 0

Tactic:
exact And.right

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 * g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
apply ne_zero_and_ne_zero_of_mul at hf

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0 ∧ g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ f = 0 → 0 = m.degree f

Tactic:
simp_intro h

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

Goal state before:
pp: case neg
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | n0

Goal state after:
case neg.inl
d2 : 2 ∣ 0
d4 : ¬2 ∣ 0 / 2
⊢ MinSqFacProp 0 ((0 / 2).minSqFacAux 3)

case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: 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
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
h : pₓ = 0
⊢ (eval xₜ) (p'.coeff (Polynomial.natDegree 0)) = 0

Tactic:
Polynomial.natDegree_zero,

Goal state after:
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
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
h : pₓ = 0
⊢ (eval xₜ) (p'.coeff 0) = 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n / 2 → 3 ≤ m

Tactic:
refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)

Goal state after:
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n / 2
⊢ 2 ≠ p
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case neg
n : ℕ
d2 : ¬2 ∣ n
⊢ n.MinSqFacProp (n.minSqFacAux 3)

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | n0

Goal state after:
case neg.inl
d2 : ¬2 ∣ 0
⊢ MinSqFacProp 0 (minSqFacAux 0 3)

case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ n.MinSqFacProp (n.minSqFacAux 3)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n → 3 ≤ m

Tactic:
refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)

Goal state after:
case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n
⊢ 2 ≠ p
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case neg
n : ℕ
d2 : ¬2 ∣ n
⊢ n.MinSqFacProp (n.minSqFacAux 3)

Tactic:
· rcases Nat.eq_zero_or_pos n with rfl | n0
    · cases d2 (by decide)
    refine minSqFacAux_has_prop _ n0 0 rfl ?_
    refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)
    rintro rfl
    contradiction

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

Goal state before:
pp: case mp
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (a ∣ n ∧ n ≠ 0) ∧ Squarefree a → ∃ a_2 ∈ (normalizedFactors n).toFinset.powerset, a_2.val.prod = a

Tactic:
rintro ⟨⟨an, h0⟩, hsq⟩

Goal state after:
case mp
n : ℕ
h0✝ : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ ∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n p : ℕ
hn : p ^ n.factorization p ≠ 1
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ 0 < n.factorization p

Tactic:
contrapose! hn

Goal state after:
n p : ℕ
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
hn : n.factorization p ≤ 0
⊢ p ^ n.factorization p = 1
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case succ
n : ℕ
⊢ ∃ a b, b ^ 2 * a = n + 1 ∧ Squarefree a

Tactic:
obtain ⟨a, b, -, -, h₁, h₂⟩ := sq_mul_squarefree_of_pos (succ_pos n)
    exact ⟨a, b, h₁, h₂⟩

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

Goal state before:
pp: p a m n : ℕ
hp : Prime p
hn : n ≠ 0
h : p ^ m = a ^ n
⊢ ∃ k, a = p ^ k

Tactic:
rcases exponent_dvd_of_prime_pow_eq_pow hp h with ⟨k, m_eq⟩
  rw [m_eq, pow_mul'] at h
  use k
  exact Nat.pow_left_injective hn h.symm

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

Goal state before:
pp: case insert
ι : 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)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
⊢ ∑ i ∈ insert a s, f i • g (σ i) ≤ ∑ i ∈ insert a s, f i • g i

Tactic:
have hτs : {x | τ x ≠ x} ⊆ s := by
    intro x hx
    simp only [τ, Ne, Set.mem_ofPred_eq, Equiv.swap_comp_apply] at hx
    split_ifs at hx with h₁ h₂
    · obtain rfl | hax := eq_or_ne x a
      · contradiction
      · exact mem_of_mem_insert_of_ne (hσ fun h ↦ hax <| h.symm.trans h₁) hax
    · exact (hx <| σ.injective h₂.symm).elim
    · exact mem_of_mem_insert_of_ne (hσ hx) (ne_of_apply_ne _ h₂)

Goal state after:
case insert
ι : 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)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ insert a s, f i • g (σ i) ≤ ∑ i ∈ insert a s, f i • g i
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hf_lcm : f (x.lcm y) ≠ 0
⊢ f (x.gcd y) = f x * f y / f (x.lcm y)

Tactic:
rw [← hf.lcm_apply_mul_gcd_apply, mul_div_cancel_left₀ _ hf_lcm]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Class

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

Tactic:
by
  rw [← orderHom_mk, ← orderHom_mk, h]

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

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ b * ↑⌊a⌋₊ + b ≤ ↑⌊a⌋₊

Tactic:
← le_sub_iff_add_le',

Goal state after:
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ b ≤ ↑⌊a⌋₊ - b * ↑⌊a⌋₊
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
hb : ¬IsMax b
⊢ insert (b + 1) (Ioc a b) = Ioc a (b + 1)

Tactic:
simpa [succ_eq_add_one] using insert_Ioc_right_eq_Ioc_succ_of_not_isMax h hb

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ : Interval α
s t : NonemptyInterval α
h✝ : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ ↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } ≤ some t

Tactic:
exact WithBot.coe_le_coe.2 ⟨le_sup_right, inf_le_right⟩

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order

Tactic:
by
  by_cases h : x = 0
  · simp_all
  · simp_all [order_of_ne h, orderTop_of_ne_zero h]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
this : |(ofLex y).leadingCoeff| < (n + 1) • |(ofLex x).leadingCoeff|
⊢ (ofLex |y|).coeff ((ofLex x).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex x).orderTop.untop ⋯)

Tactic:
simp_rw [← leadingCoeff_abs] at this

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
this : (ofLex |y|).leadingCoeff < (n + 1) • (ofLex |x|).leadingCoeff
⊢ (ofLex |y|).coeff ((ofLex x).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex x).orderTop.untop ⋯)
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hgt : (ofLex y).orderTop < (ofLex x).orderTop
n : ℕ
hn : |y| ≤ n • |x|
⊢ (ofLex x).orderTop < (ofLex y).orderTop ∨
    (ofLex x).orderTop = (ofLex y).orderTop ∧ ∃ n, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|

Tactic:
contrapose! hn

Goal state after:
case inr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hgt : (ofLex y).orderTop < (ofLex x).orderTop
n : ℕ
hn :
  (ofLex y).orderTop ≤ (ofLex x).orderTop ∧
    ((ofLex x).orderTop = (ofLex y).orderTop → ∀ (n : ℕ), n • |(ofLex x).leadingCoeff| < |(ofLex y).leadingCoeff|)
⊢ n • |x| < |y|
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
R : Type u_3
V : Type u_5
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬(of R).symm y = 0
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

Tactic:
HahnSeries.order_of_ne hx,

Goal state after:
case neg
R : Type u_3
V : Type u_5
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬(of R).symm y = 0
⊢ ((of R).symm (x • y)).coeff (⋯.min ⋯ + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff