mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Comap

Goal state before:
pp: σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ comap (g.comp f) x i = (aeval x) ((aeval fun i ↦ g (X i)) (f (X i)))

pp: σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ (aeval x) ((aeval fun i ↦ g (X i)) (f (X i))) = comap f (comap g x) i

Tactic:
· apply eval₂Hom_congr rfl rfl
    rw [AlgHom.comp_apply]
    suffices g = aeval fun i => g (X i) by rw [← this]
    exact aeval_unique g

Goal state after:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ (aeval x) ((aeval fun i ↦ g (X i)) (f (X i))) = comap f (comap g x) i
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ ∀ a ∈ t, a ∉ s → (g a)! = 1

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ ∀ a ∈ s, a ∉ t → (f a)! = 1

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ ∀ a ∈ t, a ∈ s → (g a)! = (f a)!

Tactic:
aesop

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

Goal state before:
pp: case pos
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
ha : a ∈ s
⊢ n ! = (Pi.single a n a)!

Tactic:
Pi.single_eq_same

Goal state after:
case pos
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
ha : a ∈ s
⊢ n ! = n !
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsLeftCancelAdd R
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, n i = 0
n : σ →₀ ℕ
⊢ coeff n q = coeff n (p.divMonomial (Finsupp.single i 1))

Tactic:
coeff_divMonomial,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsLeftCancelAdd R
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, n i = 0
n : σ →₀ ℕ
⊢ coeff n q = coeff (Finsupp.single i 1 + n) p
Module: Mathlib.Analysis.BoxIntegral.Basic

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

Tactic:
obtain ⟨C, hC⟩ := (NormedSpace.isBounded_iff_subset_smul_closedBall ℝ).1
                        (I.isCompact_Icc.image_of_continuousOn hc).isBounded
    use ‖C‖, fun x hx ↦ by
      simpa only [smul_unitClosedBall, mem_closedBall_zero_iff] using hC (Set.mem_image_of_mem f hx)

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
H✝ : ∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)
i : σ →₀ ℕ
H : i ∈ Set.range (Finsupp.embDomain f)
⊢ IsNilpotent (coeff i ((rename ⇑f) P))

Tactic:
aesop

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ ((2 * ∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! =
    ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, 2 ^ f i * (f i)!

Tactic:
rw [mul_pow, ← prod_pow_eq_pow_sum, prod_mul_distrib]

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ ((∏ i ∈ s, 2 ^ f i) * (∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! =
    ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ((∏ x ∈ s, 2 ^ f x) * ∏ x ∈ s, (f x)!)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: x✝ : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
this :
  (Finsupp.single 0 x✝ + Finsupp.embDomain succEmb l.toFinsupp).update 0 0 =
    (Finsupp.embDomain succEmb l.toFinsupp).update 0 0
x : ℕ
⊢ succEmb x = x + 1

Tactic:
by simp [succEmb]

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f r : MvPolynomial σ R
hg : f * r ≠ 0
⊢ f ≠ 0

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f r : MvPolynomial σ R
hg : f * r ≠ 0
⊢ r ≠ 0

Tactic:
aesop

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
⊢ m.degree f = 0 ↔ f.totalDegree = 0

Tactic:
rw [← m.toSyn.injective.eq_iff]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree f) = m.toSyn 0 ↔ f.totalDegree = 0
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b ∨ b ≠ a
⊢ {z ∈ s.offDiag | uncurry Sym2.mk z = s(a, b)} = cons (a, b) {(b, a)} ⋯

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
this :
  ∀ (a b : α),
    a ∈ s → b ∈ s → ∀ (hab : a ≠ b ∨ b ≠ a), {z ∈ s.offDiag | uncurry Sym2.mk z = s(a, b)} = cons (a, b) {(b, a)} ⋯
⊢ ∀ (x y : α), s(x, y) ∈ image (uncurry Sym2.mk) s.offDiag → #({a ∈ s.offDiag | uncurry Sym2.mk a = s(x, y)}) = 2

Tactic:
aesop

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:
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.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.leadingCoeff f ^ n ≠ 0

Tactic:
rw [hf.leadingCoeff_eq_one, one_pow]

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
⊢ 1 ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
B : Set (MvPolynomial σ R)
⊢ m.leadingTerm '' (B \ {0}) = m.leadingTerm '' B \ {0}

Tactic:
aesop

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
B : Set (MvPolynomial σ R)
⊢ m.leadingTerm '' insert 0 B = insert 0 (m.leadingTerm '' B)

Tactic:
aesop

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

Goal state before:
pp: n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
⊢ Squarefree n ∧ k = 1 → Squarefree (n ^ k)

Tactic:
rintro ⟨hn, rfl⟩; simpa

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ m.degree p = m.degree q ∧ m.leadingCoeff p = m.leadingCoeff q ∨ m.leadingCoeff p = 0 ∧ m.leadingCoeff q = 0 ↔
    m.leadingCoeff p = m.leadingCoeff q ∧ m.degree p = m.degree q

Tactic:
aesop

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

Goal state before:
pp: n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : (n / k).MinSqFacProp o
⊢ n.MinSqFacProp o

Tactic:
have : ∀ p, Prime p → p * p ∣ n → k * (p * p) ∣ n := fun p pp dp =>
    have :=
      (coprime_primes pk pp).2 fun e => by
        subst e
        contradiction
    (coprime_mul_iff_right.2 ⟨this, this⟩).mul_dvd_of_dvd_of_dvd dk dp

Goal state after:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : (n / k).MinSqFacProp o
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
⊢ n.MinSqFacProp o
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
xₜ : Fin n → R
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'
⊢ #({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}) ≤ degreeOf 0 p

Tactic:
have hpₓdeg : pₓ.natDegree = k := by
          rw [hpₓ, hk, Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ (mem_filter.1 hxₜ).2]

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
xₜ : Fin n → R
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
⊢ #({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}) ≤ degreeOf 0 p
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h✝ : g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)

Tactic:
aesop

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

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

Tactic:
aesop

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

Goal state before:
pp: case mpr.inl
p : ℕ
hp : Nat.Prime p
hq : ∀ (y : ℕ), (fun p ↦ Nat.Prime p ∧ p ∣ 0) y → y = p
hn : p ∣ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = 0

pp: case mpr.inr
n p : ℕ
hq : ∀ (y : ℕ), (fun p ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
· cases (hq 2 ⟨Nat.prime_two, dvd_zero 2⟩).trans (hq 3 ⟨Nat.prime_three, dvd_zero 3⟩).symm

Goal state after:
case mpr.inr
n p : ℕ
hq : ∀ (y : ℕ), (fun p ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case inr
k n : ℕ
hn : n ≠ 0
⊢ ∑ d ∈ n.divisors, d ^ k = 0 ↔ n = 0

Tactic:
aesop

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

Goal state before:
pp: k x✝ : ℕ
⊢ ∀ x ∈ x✝.divisors, (pow k) x = x ^ k

Tactic:
aesop

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

Goal state before:
pp: case pos
k n : ℕ
hn0 : n = 0
⊢ (σ k) n = 1 ↔ n = 1

Tactic:
aesop

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

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

Tactic:
aesop

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

Goal state before:
pp: case pos.succ
m : ℕ
hm : m = 0
n✝ : ℕ
⊢ Ω (m ^ (n✝ + 1)) = (n✝ + 1) * Ω m

Tactic:
aesop

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : ↑t ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
⊢ n ≤ ∑ k ∈ Finset.range (m + 1), s.indicator (fun x ↦ r) k

Tactic:
hn',

Goal state after:
case h
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : ↑t ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
⊢ n' • r ≤ ∑ k ∈ Finset.range (m + 1), s.indicator (fun x ↦ r) k
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
h : m = 1
⊢ 1 (m * n) = 1 m * 1 n

Tactic:
aesop

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
h : ¬m = 1
⊢ 1 (m * n) = 1 m * 1 n

Tactic:
aesop

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
h✝ : mk a < mk b
hneg : a ≤ 1
h : a < b ∧ b < a⁻¹
⊢ a < b

Tactic:
exact h.1

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
⊢ StrictAntiOn subgroup (Set.Iio ⊤)

Tactic:
intro s hs t ht hst

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : s ∈ Set.Iio ⊤
t : UpperSet (MulArchimedeanClass M)
ht : t ∈ Set.Iio ⊤
hst : s < t
⊢ subgroup t < subgroup s
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: case inl
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
a : G
ha : Subgroup.zpowers a = H
ha1 : a < 1
⊢ ∃ a < 1, Subgroup.zpowers a = H

pp: case inr.inl
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
ha : Subgroup.zpowers 1 = H
⊢ ∃ a < 1, Subgroup.zpowers a = H

pp: case inr.inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
a : G
ha : Subgroup.zpowers a = H
ha1 : 1 < a
⊢ ∃ a < 1, Subgroup.zpowers a = H

Tactic:
· exact ⟨a, ha1, ha⟩

Goal state after:
case inr.inl
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
ha : Subgroup.zpowers 1 = H
⊢ ∃ a < 1, Subgroup.zpowers a = H

case inr.inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
a : G
ha : Subgroup.zpowers a = H
ha1 : 1 < a
⊢ ∃ a < 1, Subgroup.zpowers a = H
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case h₂
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
x : ℤ
mx : x ∈ r \ s
⊢ c - ↑(#s) ≤ x

Tactic:
rw [mem_sdiff, mem_Ioc] at mx

Goal state after:
case h₂
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
x : ℤ
mx : (c - ↑(#s) < x ∧ x ≤ c) ∧ x ∉ s
⊢ c - ↑(#s) ≤ x
Module: Mathlib.Algebra.Order.Group.Ideal

Goal state before:
pp: case mp
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
x : M
⊢ x ∈ I → ∃ y z, Minimal (fun x ↦ x ∈ I) z ∧ y * z = x

Tactic:
intro hx
    rcases hpwo.exists_le_minimal hx with ⟨z, hz, hz'⟩
    rw [le_iff_exists_mul'] at hz
    rcases hz with ⟨y, rfl⟩
    exact ⟨y, z, hz', rfl⟩

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ ↑(Ioc (c - ↑(#s)) c)
⊢ x ∈ (fun x ↦ c - ↑x) '' Set.Iio #s

Tactic:
Set.mem_image,

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ ↑(Ioc (c - ↑(#s)) c)
⊢ ∃ x_1 ∈ Set.Iio #s, c - ↑x_1 = x
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
x : ℤ
mx : x ∈ r ∧ x ∉ s
⊢ x ≤ c + ↑(#s)

Tactic:
mem_Ico

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
x : ℤ
mx : (c ≤ x ∧ x < c + ↑(#s)) ∧ x ∉ s
⊢ x ≤ c + ↑(#s)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ c + ↑x ∈ Ico c (c + ↑(#s))

Tactic:
mem_Ico

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ c ≤ c + ↑x ∧ c + ↑x < c + ↑(#s)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ ↑(Ico c (c + ↑(#s)))
⊢ x ∈ (fun x ↦ c + ↑x) '' Set.Iio #s

Tactic:
Set.mem_image,

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ ↑(Ico c (c + ↑(#s)))
⊢ ∃ x_1 ∈ Set.Iio #s, c + ↑x_1 = x
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ Ico c (c + ↑(#s))
⊢ ∃ x_1 < #s, c + ↑x_1 = x

Tactic:
mem_Ico

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : c ≤ x ∧ x < c + ↑(#s)
⊢ ∃ x_1 < #s, c + ↑x_1 = x
Module: Mathlib.Algebra.Order.GroupWithZero.Bounds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
⊢ range f ⊆ {x | 0 ≤ x}

Tactic:
rintro x ⟨a, rfl⟩; exact hf0 a

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

Goal state before:
pp: case coe.coe
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a✝¹ a✝ : NonemptyInterval α
⊢ ↑(a✝¹ * a✝) = 1 ↔ ∃ a b, ↑a✝¹ = pure a ∧ ↑a✝ = pure b ∧ a * b = 1

Tactic:
← NonemptyInterval.coe_one_interval,

Goal state after:
case coe.coe
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a✝¹ a✝ : NonemptyInterval α
⊢ ↑(a✝¹ * a✝) = ↑1 ↔ ∃ a b, ↑a✝¹ = pure a ∧ ↑a✝ = pure b ∧ a * b = 1
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✝ : Subsingleton R
x✝¹ x✝ : R⟦Γ⟧
⊢ x✝¹.coeff = x✝.coeff

Tactic:
by subsingleton

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
h : ¬x = 0
⊢ x.leadingCoeff = x.coeff x.order

Tactic:
· simp [leadingCoeff_of_ne_zero, orderTop_of_ne_zero, order_of_ne, h]

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

Goal state before:
pp: case hg
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
⊢ i ∈ (ofLex x).support

pp: case hx
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
⊢ ∀ g' ∈ (ofLex x).support, i ≤ g'

Tactic:
· simpa using hi.ne.symm

Goal state after:
case hx
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
⊢ ∀ g' ∈ (ofLex x).support, i ≤ g'
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case mpr
M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c x : M
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x) → a * c ≤ x ∧ x < b * c

Tactic:
aesop

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
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

Tactic:
simp_rw [ArchimedeanClass.mk_le_mk]

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
⊢ (∃ n, |y| ≤ n • |x|) ↔ ∃ n, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: M : Type u_1
G✝ : Type u_2
inst✝⁹ : AddCancelCommMonoid M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : LocallyFiniteOrder M
inst✝⁵ : AddCommGroup G✝
inst✝⁴ : LinearOrder G✝
inst✝³ : IsOrderedAddMonoid G✝
inst✝² : LocallyFiniteOrder G✝
G : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : LocallyFiniteOrder Gˣ
a b : G
h : a ≤ b
this : Monotone (↑(orderMonoidHom Gˣ).toMonoidHom).toFun
⊢ (↑((WithZero.map' ↑(orderMonoidHom Gˣ)).comp OrderMonoidIso.withZeroUnits.symm.toMonoidWithZeroHom)).toFun a ≤
    (↑((WithZero.map' ↑(orderMonoidHom Gˣ)).comp OrderMonoidIso.withZeroUnits.symm.toMonoidWithZeroHom)).toFun b

Tactic:
aesop

Goal state after:
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
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

Tactic:
simp_rw [ArchimedeanClass.mk_le_mk]

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, |y| ≤ n • |x|) ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧ ∃ n, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
Module: Mathlib.Algebra.Order.PUnit

Goal state before:
pp: x✝² x✝¹ : PUnit
x✝ : x✝² ≤ x✝¹
⊢ x✝¹ = x✝² + unit

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
⊢ f 0 = 0

Tactic:
aesop

Goal state after: