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

Goal state before:
pp: case inr.succ.refine_1.inl
σ : 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
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : Finsupp.degree n' = d
hp : p ∣ (monomial n') 1 * q
⊢ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r

Tactic:
obtain ⟨m, r, hm, hr, hp⟩ := (hd n' hd' p q).mp hp
        exact ⟨m, r, le_trans hm hnn', hr, hp⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = (eval x) q
this : ∀ (p : MvPolynomial σ R), (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0
x : σ → R
hx : x ∈ Set.univ.pi s
⊢ (eval x) p - (eval x) q = 0

Tactic:
h x hx,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = (eval x) q
this : ∀ (p : MvPolynomial σ R), (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0
x : σ → R
hx : x ∈ Set.univ.pi s
⊢ (eval x) q - (eval x) q = 0
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p✝ q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h✝ : ∀ x ∈ Set.univ.pi s, (eval x) p✝ = (eval x) q
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ x ∈ Set.univ.pi s, (eval x) ((rename f) p) = 0
x : Fin n → R
hx : x ∈ Set.univ.pi (s ∘ f)
g : σ → R
hg : ∀ (i : σ), g i ∈ s i
i : Fin n
x✝ : f i ∈ Set.univ
⊢ Function.extend f x g (f i) ∈ s (f i)

Tactic:
rw [hf.extend_apply]

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p✝ q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h✝ : ∀ x ∈ Set.univ.pi s, (eval x) p✝ = (eval x) q
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ x ∈ Set.univ.pi s, (eval x) ((rename f) p) = 0
x : Fin n → R
hx : x ∈ Set.univ.pi (s ∘ f)
g : σ → R
hg : ∀ (i : σ), g i ∈ s i
i : Fin n
x✝ : f i ∈ Set.univ
⊢ x i ∈ s (f i)
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case neg
ι : 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 : ι
h₁ : r j i ∧ j ∉ p
⊢ x₂ j = if j ∈ p then x₁ j else x₂ j

Tactic:
if_neg h₁.2

Goal state after:
case neg
ι : 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 : ι
h₁ : r j i ∧ j ∉ p
⊢ x₂ j = x₂ j
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ {r ∈ piFinset S | P (init r)} = map (snocEquiv α).toEmbedding (S (last n) ×ˢ {r ∈ piFinset (init S) | P r})

Tactic:
by
  simp [← map_snocEquiv_filter_piFinset, map_map]

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ z ∈ (normalizedFactors ?m.439).toFinset

Tactic:
apply hy hz

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 : MvPolynomial σ R
⊢ m.leadingCoeff (-f) = -m.leadingCoeff f

Tactic:
by
  simp only [leadingCoeff, degree_neg, coeff_neg]

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

Goal state before:
pp: k n : ℕ
⊢ (σ k) n = 0 ↔ n = 0

Tactic:
rcases eq_or_ne n 0 with rfl | hn
  · simp
  · simp only [ArithmeticFunction.sigma_apply]
    aesop

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

Goal state before:
pp: k n : ℕ
hn0 : n ≠ 0
⊢ 0 < (σ k) n

Tactic:
rwa [sigma_pos_iff, pos_iff_ne_zero]

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

Goal state before:
pp: d n p : ℕ
hn : Squarefree n
hp : p ∈ n.primeFactorsList
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
⊢ ∃! i, p ∣ f i

Tactic:
rw [mem_finMulAntidiag] at hf
  rw [mem_primeFactorsList hf.2, ← hf.1, hp.1.prime.dvd_finsetProd_iff] at hp
  obtain ⟨i, his, hi⟩ := hp.2
  refine ⟨i, hi, ?_⟩
  intro j hj
  by_contra hij
  apply Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp.1, hi, hj⟩
  apply Nat.coprime_of_squarefree_mul
  apply hn.squarefree_of_dvd
  rw [← hf.1, ← Finset.mul_prod_erase _ _ his,
    ← Finset.mul_prod_erase _ _ (mem_erase.mpr ⟨hij, mem_univ _⟩), ← mul_assoc]
  apply Nat.dvd_mul_right

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

Goal state before:
pp: case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : Prime p ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
q : ↥n.primeFactors
hq : q ∈ {p_1 ∈ n.primeFactors.attach | g ↑p_1 ⋯ = f p hp✝}
⊢ ¬p ∣ ↑q

Tactic:
rw [Nat.prime_dvd_prime_iff_eq hp.1 (Nat.prime_of_mem_primeFactorsList
      <| List.mem_toFinset.mp q.2)]

Goal state after:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : Prime p ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
q : ↥n.primeFactors
hq : q ∈ {p_1 ∈ n.primeFactors.attach | g ↑p_1 ⋯ = f p hp✝}
⊢ ¬p = ↑q
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
h :
  (∀ b_1 ∈ B, m.toSyn (m.degree (g b_1)) = m.toSyn (m.degree (g b)) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
hd : ∀ a ∈ B, m.toSyn (m.degree (g a)) = m.toSyn (m.degree (g b)) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ ∑ b ∈ insert b B, g b =
    ∑ b₁ ∈ insert b B,
      ∑ b₂ ∈ insert b B, (fun b₁ b₂ ↦ if b₂ = b then ↑isunit_gb.unit⁻¹ else 0) b₁ b₂ • m.sPolynomial (g b₁) (g b₂)

Tactic:
simp only [Finset.sum_insert hb, ite_smul, zero_smul, ↓reduceIte, Finset.sum_ite_eq', hb,
        add_zero, sPolynomial_self, smul_zero, zero_add]

Goal state after:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
h :
  (∀ b_1 ∈ B, m.toSyn (m.degree (g b_1)) = m.toSyn (m.degree (g b)) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
hd : ∀ a ∈ B, m.toSyn (m.degree (g a)) = m.toSyn (m.degree (g b)) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ g b + ∑ b ∈ B, g b = ∑ x ∈ B, ↑isunit_gb.unit⁻¹ • m.sPolynomial (g x) (g b)
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
⊢ ∀ (x : α), (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x

Tactic:
suffices ∀ x, 0 < x → inducedAddHom α β (x * x) = inducedAddHom α β x * inducedAddHom α β x by
        intro x
        obtain h | rfl | h := lt_trichotomy x 0
        · convert! this (-x) (neg_pos.2 h) using 1
          · rw [neg_mul, mul_neg, neg_neg]
          · simp_rw [map_neg, neg_mul, mul_neg, neg_neg]
        · simp only [mul_zero, map_zero]
        · exact this x h
        -- prove that the (Sup of rationals less than x) ^ 2 is the Sup of the set of rationals less
        -- than (x ^ 2) by showing it is an upper bound and any smaller number is not an upper bound
      refine fun x hx => csSup_eq_of_forall_le_of_forall_lt_exists_gt (cutMap_nonempty β _) ?_ ?_
      · exact le_inducedMap_mul_self_of_mem_cutMap hx
      · exact exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self hx

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

Goal state before:
pp: case e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
a✝ b✝ : β
h : (inducedOrderRingHom β γ).toRingHom a✝ ≤ (inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ =
    inducedMap γ β
      ({ toRingHom := (inducedAddHom β γ).mkRingHomOfMulSelfOfTwoNeZero ⋯ ⋯ ⋯, monotone' := ⋯ }.toRingHom a✝)

Tactic:
AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero,

Goal state after:
case e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
a✝ b✝ : β
h : (inducedOrderRingHom β γ).toRingHom a✝ ≤ (inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ = inducedMap γ β ((inducedAddHom β γ) a✝)
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
a✝ b✝ : β
h : (inducedOrderRingHom β γ).toRingHom a✝ ≤ (inducedOrderRingHom β γ).toRingHom b✝
⊢ b✝ =
    inducedMap γ β
      ({ toRingHom := (inducedAddHom β γ).mkRingHomOfMulSelfOfTwoNeZero ⋯ ⋯ ⋯, monotone' := ⋯ }.toRingHom b✝)

Tactic:
AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero,

Goal state after:
case e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
a✝ b✝ : β
h : (inducedOrderRingHom β γ).toRingHom a✝ ≤ (inducedOrderRingHom β γ).toRingHom b✝
⊢ b✝ = inducedMap γ β ((inducedAddHom β γ) b✝)
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
h : Function.Injective ⇑f
⊢ Function.Injective ⇑(orderHom f)

Tactic:
intro a b
  induction a using ind with | mk a
  induction b using ind with | mk b
  simp_rw [orderHom_mk, mk_eq_mk, ← map_mabs, ← map_pow]
  obtain hmono := (OrderHomClass.monotone f).strictMono_of_injective h
  intro ⟨⟨m, hm⟩, ⟨n, hn⟩⟩
  exact ⟨⟨m, hmono.le_iff_le.mp hm⟩, ⟨n, hmono.le_iff_le.mp hn⟩⟩

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

Goal state before:
pp: K : Type u_2
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
m n : ℕ
⊢ ⌊↑m / ↑n⌋₊ = m / n

Tactic:
convert! floor_div_natCast (m : K) n

Goal state after:
K : Type u_2
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
m n : ℕ
⊢ m = ⌊↑m⌋₊
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 : K
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋₊

Tactic:
refine mul_lt_floor ?_ ?_ ?_ <;> norm_num

Goal state after:
case refine_3
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ 1 ≤ a
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
n : ℕ∞
⊢ ⌊↑n + r⌋ₑ = n + ⌊r⌋ₑ

Tactic:
by
  simp [add_comm, floor_add_toENNReal]

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

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
p q : GroupCone G
h : (fun C ↦ C.carrier) p = (fun C ↦ C.carrier) q
⊢ p = q

Tactic:
cases p

Goal state after:
case mk
G : Type u_1
inst✝ : CommGroup G
q : GroupCone G
toSubmonoid✝ : Submonoid G
eq_one_of_mem_of_inv_mem'✝ : ∀ {a : G}, a ∈ toSubmonoid✝.carrier → a⁻¹ ∈ toSubmonoid✝.carrier → a = 1
h :
  (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ } =
    (fun C ↦ C.carrier) q
⊢ { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ } = q
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: α : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : Interval α
⊢ (s - t).length ≤ s.length + t.length

Tactic:
by
  simpa [sub_eq_add_neg] using length_add_le s (-t)

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
f : Γ → R
h : (Function.support f).IsPWO
⊢ (∀ (x : Γ), f x = coeff 0 x) ↔ ∀ (x : Γ), f x = 0 x

Tactic:
coeff_zero,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
f : Γ → R
h : (Function.support f).IsPWO
⊢ (∀ (x : Γ), f x = 0) ↔ ∀ (x : Γ), f x = 0 x
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ n ≤ (ofSuppBddBelow f ⋯).order

Tactic:
by
  rw [le_order_iff_forall]
  · exact hn
  · simpa

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ
inst✝ : DecidableLT Γ
c : Γ
x : R⟦Γ⟧
⊢ ((truncLT c) x).support = {y | y ∈ x.support ∧ y < c}

Tactic:
by
  simp [truncLT, Function.support, and_comm]

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

Goal state before:
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 : Γ
hg : g < i
⊢ g ∉ (ofLex x).support

Tactic:
simpa using (hj g hg).symm

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ Covariant α α (fun x1 x2 ↦ x1 * x2) fun x1 x2 ↦ x1 ≤ x2

Tactic:
intro _ _ _

Goal state after:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) n₁✝ n₂✝ → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 * x2) m✝ n₁✝) ((fun x1 x2 ↦ x1 * x2) m✝ n₂✝)
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ Covariant α α (swap fun x1 x2 ↦ x1 * x2) fun x1 x2 ↦ x1 ≤ x2

Tactic:
intro _ _ _

Goal state after:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) n₁✝ n₂✝ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 * x2) m✝ n₁✝) (swap (fun x1 x2 ↦ x1 * x2) m✝ n₂✝)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.support ⊆ s
b : Γ × Γ'
hb :
  (b.1 ∈ s ∧ ((of R).symm y).coeff b.2 ≠ 0 ∧ b.1 +ᵥ b.2 = a) ∧
    (((of R).symm y).coeff b.2 ≠ 0 ∧ b.1 +ᵥ b.2 = a → x.coeff b.1 = 0)
⊢ x.coeff b.1 • ((of R).symm y).coeff b.2 = 0

Tactic:
hb.2 ⟨hb.1.2.1, hb.1.2.2⟩,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.support ⊆ s
b : Γ × Γ'
hb :
  (b.1 ∈ s ∧ ((of R).symm y).coeff b.2 ≠ 0 ∧ b.1 +ᵥ b.2 = a) ∧
    (((of R).symm y).coeff b.2 ≠ 0 ∧ b.1 +ᵥ b.2 = a → x.coeff b.1 = 0)
⊢ 0 • ((of R).symm y).coeff b.2 = 0
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
⊢ FiniteArchimedeanClass (Lex R⟦Γ⟧) ≃o Lex (Γ × FiniteArchimedeanClass R)

Tactic:
apply OrderIso.ofHomInv (finiteArchimedeanClassOrderHomLex Γ R)
    (finiteArchimedeanClassOrderHomInvLex Γ R)
  · ext x
    cases x with | h x
    obtain ⟨order, coeff⟩ := x
    induction coeff using FiniteArchimedeanClass.ind with | mk a ha
    simp [finiteArchimedeanClassOrderHomLex, finiteArchimedeanClassOrderHomInvLex, ha]
  · ext x
    induction x using FiniteArchimedeanClass.ind with | mk a ha
    simp [finiteArchimedeanClassOrderHomLex, finiteArchimedeanClassOrderHomInvLex,
      archimedeanClassMk_eq_archimedeanClassMk_iff, ha]

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

Goal state before:
pp: K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h : ↑x = f.sum fun c ↦ ⇑(seed.stratum c).subtype
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), ↑x ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) := DFinsupp.mapRange (fun c x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩) ⋯ f
⊢ f c = (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (f' c)

Tactic:
set_option backward.isDefEq.respectTransparency false in
    apply Subtype.ext
    simp [f']

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p q : RingCone R
h : (fun C ↦ C.carrier) p = (fun C ↦ C.carrier) q
⊢ p = q

Tactic:
cases p

Goal state after:
case mk
R : Type u_1
inst✝ : Ring R
q : RingCone R
toSubsemiring✝ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝ : ∀ {a : R}, a ∈ toSubsemiring✝.carrier → -a ∈ toSubsemiring✝.carrier → a = 0
h :
  (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ } =
    (fun C ↦ C.carrier) q
⊢ { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ } = q
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p q : RingPreordering R
h : (fun P ↦ (↑P).carrier) p = (fun P ↦ (↑P).carrier) q
⊢ p = q

Tactic:
cases p

Goal state after:
case mk
R : Type u_1
inst✝ : CommRing R
q : RingPreordering R
toSubsemiring✝ : Subsemiring R
mem_of_isSquare'✝ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝.carrier
neg_one_notMem'✝ : -1 ∉ toSubsemiring✝.carrier
h :
  (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ } =
    (fun P ↦ (↑P).carrier) q
⊢ { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ } = q
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
q : R
hq₀ : 0 < f q
hq : f q * |y| ≤ |x|
hq₀' : 0 < q
⊢ mk x ≤ mk y

Tactic:
obtain ⟨n, hn⟩ := exists_lt_nsmul hq₀' 1

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
q : R
hq₀ : 0 < f q
hq : f q * |y| ≤ |x|
hq₀' : 0 < q
n : ℕ
hn : 1 < n • q
⊢ mk x ≤ mk y
Module: Mathlib.Algebra.Order.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : Rˣ
⊢ Xor (a * -1 ∈ posSubgroup R) (a ∈ posSubgroup R)

Tactic:
obtain h | h := lt_or_gt_of_ne a.ne_zero

Goal state after:
case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : Rˣ
h : ↑a < 0
⊢ Xor (a * -1 ∈ posSubgroup R) (a ∈ posSubgroup R)

case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : Rˣ
h : 0 < ↑a
⊢ Xor (a * -1 ∈ posSubgroup R) (a ∈ posSubgroup R)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : K
⊢ x✝ ∈ A.valuation.valuationSubring ↔ x✝ ∈ A

Tactic:
← A.valuation_le_one_iff

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : K
⊢ x✝ ∈ A.valuation.valuationSubring ↔ A.valuation x✝ ≤ 1
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (s * t)

Tactic:
rw [mul_comm]
  exact hs.mul_left

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ ∀ (x : α), x ∈ a • s ↔ x ∈ s

Tactic:
mem_smul_set_iff_inv_smul_mem

Goal state after:
case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ ∀ (x : α), a⁻¹ • x ∈ s ↔ x ∈ s