mathlib-initiative/mathlib-tactics huggingface dataset:
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
ι : Type u_3
b : Basis ι ℤ ↥L
x : ↥L
i : ι
⊢ ↑|(b.repr x) i| ≤ (normBound b)⁻¹ * ‖x‖

Tactic:
rw [le_inv_mul_iff₀ (normBound_pos b)]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
b : Basis ι ℤ ↥L
x : ↥L
i : ι
⊢ normBound b * ↑|(b.repr x) i| ≤ ‖x‖
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
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
⊢ ∑ p ∈ Fintype.piFinset fun x ↦ Icc (-↑n) ↑n, ‖∑ i, p i • b i‖ ^ r ≤
    2 * ↑d * 3 ^ (d - 1) * normBound b ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

Tactic:
have hr' : r < 0 := hr.trans_le (by linarith)

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

Tactic:
by
        grw [Finset.sum_range_succ', Nat.cast_zero, ← Real.rpow_nonneg le_rfl, add_zero]

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

Goal state before:
pp: R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun i ↦ (xs ++ [x]).getD i 0 ≠ 0
inst✝ : DecidablePred fun i ↦ xs.getD i 0 ≠ 0
⊢ (xs ++ [x]).toFinsupp = xs.toFinsupp + Finsupp.single xs.length x

Tactic:
classical rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single,
    addLeftEmbedding_apply, add_zero]

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) ≠ n
⊢ coeff s ((linearCombination R X) a ^ n) = 0

Tactic:
simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum, ← map_pow,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_prod,
    coeff_prod_X_pow, mul_ite, mul_one, mul_zero]

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) ≠ n
⊢ (∑ x ∈ a.support.piAntidiag n,
      if s = indicator a.support fun i x_1 ↦ x i then ↑(Nat.multinomial a.support x) * ∏ x_1 ∈ a.support, a x_1 ^ x x_1
      else 0) =
    0
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case neg
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
ha : a ∉ s
⊢ 0! = ∏ x ∈ s, (Pi.single a n x)!

Tactic:
· rw [eq_comm, factorial_zero]
    apply Finset.prod_eq_one
    intro _ hb
    rw [Pi.single_apply, if_neg (ne_of_mem_of_not_mem hb ha), factorial_zero]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ
⊢ 1 ≤ (Finsupp.single j 1) i ↔ i = j

Tactic:
Nat.one_le_iff_ne_zero,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ
⊢ (Finsupp.single j 1) i ≠ 0 ↔ i = j
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
P✝ : MvPolynomial σ R
inst✝¹ : Finite σ
this : Fintype σ
α β : Type u_1
inst✝ : Fintype β
e : α ≃ β
h₁ : ∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)
P : MvPolynomial β R
⊢ (∀ (b : β →₀ ℕ), IsNilpotent (coeff ((Finsupp.equivCongrLeft e).symm b) ((rename ⇑e.symm) P))) ↔
    ∀ (i : β →₀ ℕ), IsNilpotent (coeff i P)

Tactic:
simp [Finsupp.equivMapDomain_eq_mapDomain, coeff_rename_mapDomain _ e.symm.injective]

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

Goal state before:
pp: case cons.e_a.e_a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ s.noncommProd (fun i ↦ f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯ = s.noncommProd (fun i ↦ f✝ i ^ f i) ⋯

Tactic:
refine noncommProd_congr rfl (fun t ht ↦ ?_) _

Goal state after:
case cons.e_a.e_a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
t : α
ht : t ∈ s
⊢ f✝ t ^ (f t + if t = a then p.1 else 0) = f✝ t ^ f t
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
⊢ p = q → ∀ x ∈ Set.univ.pi s, (eval x) p = (eval x) q

Tactic:
rintro rfl _ _

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
x✝ : σ → R
a✝ : x✝ ∈ Set.univ.pi s
⊢ (eval x✝) p = (eval x✝) p
Module: Mathlib.Data.Finsupp.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a : m.syn
⊢ 0 ≤ a

Tactic:
have := m.le_add_right 0 (m.toSyn.symm a)

Goal state after:
σ : Type u_1
m : MonomialOrder σ
a : m.syn
this : m.toSyn 0 ≤ m.toSyn 0 + m.toSyn (m.toSyn.symm a)
⊢ 0 ≤ a
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case mpr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
⊢ b ∣ r ∧ (p = C b ∨ p = b • (monomial (Finsupp.single i 1)) 1) → ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b

Tactic:
rintro ⟨hb, hp | hp⟩
    · use 0; simp [hb, hp]
    · use Finsupp.single i 1, le_rfl, hb
      simp [hp, smul_monomial]

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

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree (p ^ k)
⊢ Prime (p ^ k)

Tactic:
squarefree_pow_iff hp.ne_one hk.ne'

Goal state after:
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime (p ^ k)
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.toWithBotSyn (m.withBotDegree (f + g)) ≤
    max (m.toWithBotSyn (m.withBotDegree f)) (m.toWithBotSyn (m.withBotDegree g))

Tactic:
by_cases! h : f = 0 ∨ g = 0
  · rcases h with h | h <;> simp [h, m.toWithBotSyn_apply]
  simpa [withBotDegree_le_withBotDegree_iff, h] using degree_add_le (R := R)

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

Goal state before:
pp: case calc_2
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
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
⊢ ∑ i_1, ↑(i i_1) / ↑(#(S i_1.succ)) + ↑(degreeOf 0 p) / ↑(#(S 0)) ≤
    ∑ i_1, ↑((Finsupp.cons p'.natDegree i) i_1) / ↑(#(S i_1))

Tactic:
rw [Fin.sum_univ_succ, add_comm]

Goal state after:
case calc_2
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
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
⊢ ↑(degreeOf 0 p) / ↑(#(S 0)) + ∑ i_1, ↑(i i_1) / ↑(#(S i_1.succ)) ≤
    ↑((Finsupp.cons p'.natDegree i) 0) / ↑(#(S 0)) + ∑ i_1, ↑((Finsupp.cons p'.natDegree i) i_1.succ) / ↑(#(S i_1.succ))
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.sPolynomial f 0 = 0

Tactic:
sPolynomial_antisymm,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ -m.sPolynomial 0 f = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
⊢ ∀ {m n : ℕ},
    ¬m = 0 →
      ¬n = 0 →
        m.Coprime n →
          (ArithmeticFunction.prodPrimeFactors f) (m * n) =
            (ArithmeticFunction.prodPrimeFactors f) m * (ArithmeticFunction.prodPrimeFactors f) n

Tactic:
intro x y hx hy hxy

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hxy : x.Coprime y
⊢ (ArithmeticFunction.prodPrimeFactors f) (x * y) =
    (ArithmeticFunction.prodPrimeFactors f) x * (ArithmeticFunction.prodPrimeFactors f) y
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case inl
b : ℕ
hab : b = 1
⊢ {d ∈ (0 * b).divisors | IsPrimePow d} = {d ∈ divisors 0 ∪ b.divisors | IsPrimePow d}

Tactic:
simp [hab, Finset.filter_singleton, not_isPrimePow_one]

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

Goal state before:
pp: case inr.inl
a : ℕ
ha : a ≠ 0
hab : a = 1
⊢ {d ∈ (a * 0).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ divisors 0 | IsPrimePow d}

Tactic:
simp [hab, Finset.filter_singleton, not_isPrimePow_one]

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

Goal state before:
pp: case inr.inl
a : ℕ
ha : a ≠ 0
hab : a.Coprime 0
⊢ {d ∈ (a * 0).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ divisors 0 | IsPrimePow d}

pp: case inr.inr
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
⊢ {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}

Tactic:
· simp only [Nat.coprime_zero_right] at hab
    simp [hab, Finset.filter_singleton, not_isPrimePow_one]

Goal state after:
case inr.inr
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
⊢ {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case inr
k n : ℕ
hn : n ≠ 0
⊢ (σ k) n = 0 ↔ n = 0

Tactic:
simp only [ArithmeticFunction.sigma_apply]

Goal state after:
case inr
k n : ℕ
hn : n ≠ 0
⊢ ∑ d ∈ n.divisors, d ^ k = 0 ↔ n = 0
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: divisorsAntidiagonal : ℕ+ → Finset (ℕ+ × ℕ+) :=
  fun n ↦ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ x ∈ divisorsAntidiagonal n ↔ x.1 * x.2 = n

Tactic:
divisorsAntidiagonal,

Goal state after:
divisorsAntidiagonal : ℕ+ → Finset (ℕ+ × ℕ+) :=
  fun n ↦ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ x ∈ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach ↔ x.1 * x.2 = n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ a, ∏ i, Additive.toMul (a i) = ⟨n, h⟩ ∧ (fun x ↦ ↑(Additive.toMul (a x))) = f) ↔ ∏ i, f i = n ∧ n ≠ 0

Tactic:
(Equiv.piCongrRight fun _ => Additive.ofMul).surjective.exists,

Goal state after:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x,
      ∏ i, Additive.toMul ((Equiv.piCongrRight fun x ↦ Additive.ofMul) x i) = ⟨n, h⟩ ∧
        (fun x_1 ↦ ↑(Additive.toMul ((Equiv.piCongrRight fun x ↦ Additive.ofMul) x x_1))) = f) ↔
    ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
⊢ Ω (p ^ k) = k

Tactic:
by
  simp [cardFactors_pow, hp]

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

Goal state before:
pp: n : ℕ
⊢ Ω n = n.factorization.sum fun x k ↦ k

Tactic:
by
  simp [cardFactors_apply, ← List.sum_toFinset_count_eq_length, Finsupp.sum]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Field α
inst✝ : LinearOrder α
a : α
⊢ cutMap α a = Iio a ∩ range Rat.cast

Tactic:
by
  grind [mem_cutMap_iff]

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

Goal state before:
pp: case inl
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 : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x

Tactic:
convert! this (-x) (neg_pos.2 h) using 1

Goal state after:
case e'_2
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 : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) (-x * -x)

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 : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) x * (inducedAddHom α β) x = (inducedAddHom α β) (-x) * (inducedAddHom α β) (-x)
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 : ℚ
a✝ b✝ : β
h : (inducedOrderRingHom β γ).toRingHom a✝ ≤ (inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ ≤ b✝

Tactic:
convert! inducedMap_mono γ β h <;>
      · rw [inducedOrderRingHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero, inducedAddHom]
        dsimp
        rw [inducedMap_inv_self β γ _]

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

Goal state before:
pp: case mk
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b a : M
⊢ ∃ n, |1|ₘ ≤ |a|ₘ ^ n

Tactic:
exact ⟨1, by simp⟩

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

Goal state before:
pp: ι : 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✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f i • g i < ∑ i ∈ s, f i • g (σ i) ↔ ¬AntivaryOn f (g ∘ ⇑σ) ↑s

Tactic:
simp [← hfg.sum_smul_comp_perm_eq_sum_smul_iff hσ, lt_iff_le_and_ne, eq_comm,
    hfg.sum_smul_le_sum_smul_comp_perm hσ]

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

Goal state before:
pp: ι : 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✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i, f i • g i < ∑ i, f (σ i) • g i ↔ ¬Antivary (f ∘ ⇑σ) g

Tactic:
simp [(hfg.antivaryOn _).sum_smul_lt_sum_comp_perm_smul_iff fun _ _ ↦ mem_univ _]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert (a - 1) (Ico a b) = Ico (a - 1) b

Tactic:
simpa [pred_eq_sub_one] using insert_Ico_left_eq_Ico_pred_of_not_isMin h ha

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

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

Tactic:
rw [dif_pos, Interval.coe_le_coe]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ c✝ : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
⊢ s ≤ { fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ }

case hc
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ c✝ : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
⊢ t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = f g
⊢ (embDomain f ((single g) r)).coeff g' = ((single (f g)) r).coeff g'

Tactic:
embDomain_notin_image_support,

Goal state after:
case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = f g
⊢ 0 = ((single (f g)) r).coeff g'

case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = f g
⊢ g' ∉ ⇑f '' ((single g) r).support
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inl.mk.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a✝ b✝ : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h✝ : toLex (ao, FiniteArchimedeanClass.mk a ha) ≤ toLex (bo, FiniteArchimedeanClass.mk b hb)
h : (ofLex (toLex (ao, FiniteArchimedeanClass.mk a ha))).1 < (ofLex (toLex (bo, FiniteArchimedeanClass.mk b hb))).1
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, FiniteArchimedeanClass.mk a ha)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (bo, FiniteArchimedeanClass.mk b hb))

Tactic:
simp only [ne_eq, ofLex_toLex, FiniteArchimedeanClass.liftOrderHom_mk]

Goal state after:
case inl.mk.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a✝ b✝ : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h✝ : toLex (ao, FiniteArchimedeanClass.mk a ha) ≤ toLex (bo, FiniteArchimedeanClass.mk b hb)
h : (ofLex (toLex (ao, FiniteArchimedeanClass.mk a ha))).1 < (ofLex (toLex (bo, FiniteArchimedeanClass.mk b hb))).1
⊢ FiniteArchimedeanClass.mk (toLex ((single ao) a)) ⋯ ≤ FiniteArchimedeanClass.mk (toLex ((single bo) b)) ⋯
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) := ⋯
hf : f c = (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (f' c)
⊢ seed.baseDomain.subtype x = seed.baseDomain.subtype ((DirectSum.coeAddMonoidHom seed.stratum') f')

Tactic:
DirectSum.coeAddMonoidHom_eq_dfinsuppSum,

Goal state after:
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
hf : f c = (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (f' c)
⊢ seed.baseDomain.subtype x = seed.baseDomain.subtype (DFinsupp.sum f' fun i x ↦ ↑x)
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hi : (ofLex a).coeff i < (ofLex b).coeff i
k : Γ'
hki : k < f i
hkmem : k ∉ Set.range ⇑f
⊢ (embDomain f (ofLex a)).coeff k = (embDomain f (ofLex b)).coeff k

Tactic:
simp_rw [embDomain_of_notMem_range hkmem]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : LinearOrder R
inst✝⁴ : CommRing R
inst✝³ : IsStrictOrderedRing R
S : Type u_3
inst✝² : LinearOrder S
inst✝¹ : CommRing S
inst✝ : IsStrictOrderedRing S
f : S →+o R
⊢ (orderHom f) 0 = mk (f 1)

Tactic:
rw [← mk_one, orderHom_mk]

Goal state after: