mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: case convert_2
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
inst✝ : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card (Free.ChooseBasisIndex ℤ ↥L) * F x

Tactic:
rwa [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ L]

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:
| append_singleton x xs ih =>

Goal state after:
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
n : ℕ
hn : finrank ℤ ↥L < n
⊢ Summable fun z ↦ ‖z‖⁻¹ ^ n

Tactic:
simpa using summable_norm_sub_inv_pow L n hn 0

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

Goal state before:
pp: α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + f b).succ * (f a + f b).choose (f a) = ((f a).succ + f b).choose (f a).succ * (f a).succ

Tactic:
succ_eq_add_one,

Goal state after:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + f b + 1) * (f a + f b).choose (f a) = ((f a).succ + f b).choose (f a).succ * (f a).succ
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case cons
α : 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
⊢ ↑((f a + p.1 + s.sum f).choose (f a + p.1)) * ↑(multinomial s (f + fun i ↦ if i = a then p.1 else 0)) *
      (f✝ a ^ (f a + p.1) * s.noncommProd (fun i ↦ f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯) =
    ↑(n.choose p.1) * ↑(multinomial s f) * (f✝ a ^ p.1 * s.noncommProd (fun i ↦ f✝ i ^ f i) ⋯)

Tactic:
rw [not_imp_comm.1 (hf.2 _) has, zero_add, hf.1]

Goal state after:
case cons
α : 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
⊢ ↑((p.1 + p.2).choose p.1) * ↑(multinomial s (f + fun i ↦ if i = a then p.1 else 0)) *
      (f✝ a ^ p.1 * s.noncommProd (fun i ↦ f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯) =
    ↑(n.choose p.1) * ↑(multinomial s f) * (f✝ a ^ p.1 * s.noncommProd (fun i ↦ f✝ i ^ f i) ⋯)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty.succ
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
n : ℕ
⊢ 0 ^ (n + 1) = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
_root_.pow_succ,

Goal state after:
case empty.succ
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
n : ℕ
⊢ 0 ^ n * 0 = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
p : ℕ
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : σ → A
⊢ (aeval f).comp (expand p) = aeval (f ^ p)

Tactic:
ext; simp

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : degree (ofDegLex x) = degree (ofDegLex y) ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y)
⊢ (fun x ↦ degree (ofDegLex x)) x ≤ (fun x ↦ degree (ofDegLex x)) y

Tactic:
apply le_of_eq h.1

Goal state after:
Module: Mathlib.Algebra.NonAssoc.PreLie.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : LeftPreLieRing L
x y z : Lᵐᵒᵖ
⊢ associator x y z = associator x z y

Tactic:
by
    simp [assoc_symm]

Goal state after:
Module: Mathlib.Algebra.NonAssoc.PreLie.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : RightPreLieRing L
x y z : Lᵐᵒᵖ
⊢ associator x y z = associator y x z

Tactic:
by
    simp [assoc_symm]

Goal state after:
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : RightPreLieRing L
x y z : L
⊢ associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y

Tactic:
by
    have assoc_xyz := RightPreLieRing.assoc_symm' x y z
    have assoc_zxy := RightPreLieRing.assoc_symm' z x y
    have assoc_yzx := RightPreLieRing.assoc_symm' y z x
    grind

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: n : ℕ
⊢ Associated (normalizedFactors (n + 1)).prod (↑(n + 1).primeFactorsList).prod

Tactic:
Multiset.prod_coe,

Goal state after:
n : ℕ
⊢ Associated (normalizedFactors (n + 1)).prod (n + 1).primeFactorsList.prod
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
⊢ m.degree (0 ^ n) = n • m.degree 0

Tactic:
degree_zero,

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
⊢ m.degree (0 ^ n) = n • 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ { toFun := fun x ↦ if x = 1 then ↑0 else 0, map_zero' := ⋯ } = 0

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ 0 * f = 0

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ f * 0 = 0

Tactic:
ext; simp

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

Goal state before:
pp: case inr.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ n / p ^ n.factorization p = 1

Tactic:
refine Nat.eq_of_factorization_eq (Nat.ordCompl_pos p hn0).ne' (by simp) fun q => ?_

Goal state after:
case inr.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ (n / p ^ n.factorization p).factorization q = (Nat.factorization 1) q
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ IsUnit f → IsUnit (f 1)

pp: case mpr
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ IsUnit (f 1) → IsUnit f

Tactic:
· rintro ⟨f, rfl⟩
    refine ⟨⟨f.val 1, f⁻¹.val 1, ?_, ?_⟩, rfl⟩
    · rw [← ArithmeticFunction.mul_apply_one, Units.mul_inv, one_one]
    · rw [← ArithmeticFunction.mul_apply_one, Units.inv_mul, one_one]

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ IsUnit (f 1) → IsUnit f
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h.h
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
hfg : f p hp ≠ g p hp
⊢ p ∣ ∏ p ∈ n.primeFactors.attach with f ↑p ⋯ = f p hp, ↑p

Tactic:
rw [Finset.prod_filter]
    convert! Finset.dvd_prod_of_mem _ (mem_attach (n.primeFactors) ⟨p, hp⟩)
    rw [if_pos rfl]

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

Goal state before:
pp: case refine_2
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ d.primeFactorsPiBij n f ⋯ i = t i

Tactic:
trans (∏ p ∈ n.primeFactors.attach, if p.1 ∣ t i then p else 1)

Goal state after:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ d.primeFactorsPiBij n f ⋯ i = ∏ p ∈ n.primeFactors.attach, if ↑p ∣ t i then ↑p else 1

d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ (∏ p ∈ n.primeFactors.attach, if ↑p ∣ t i then ↑p else 1) = t i
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
cop : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).Coprime (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2)
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (a1 * a2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1

Tactic:
rw [← hcd.1.1, h.1, gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one,
          mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
x : ℕ
hx : x ∈ hs.toFinset
⊢ s.indicator (fun x ↦ a) x = a

Tactic:
indicator_of_mem (hs.mem_toFinset.1 hx) (fun _ ↦ a)

Goal state after:
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
x : ℕ
hx : x ∈ hs.toFinset
⊢ a = a
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
cop : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).Coprime (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2)
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (b1 * b2).gcd (a1 * b1) = ((c1, c2), d1, d2).2.1

Tactic:
rw [← hcd.2.1, h.1, mul_comm c1 d1, gcd_mul_left,
          cop.coprime_mul_right.coprime_mul_left_right.symm.gcd_eq_one, mul_one]

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

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

Tactic:
by_cases hx : x = 0
  · simp only [hx, f.map_zero, zero_mul, lcm_zero_left, gcd_zero_left]
  by_cases hy : y = 0
  · simp only [hy, f.map_zero, mul_zero, lcm_zero_right, gcd_zero_right, zero_mul]
  have hgcd_ne_zero : x.gcd y ≠ 0 := gcd_ne_zero_left hx
  have hlcm_ne_zero : x.lcm y ≠ 0 := lcm_ne_zero hx hy
  have hfi_zero : ∀ {i}, f (i ^ 0) = 1 := by
    intro i; rw [pow_zero, hf.1]
  iterate 4 rw [hf.multiplicative_factorization f (by assumption),
    Finsupp.prod_of_support_subset _ _ _ (fun _ _ => hfi_zero)
      (s := (x.primeFactors ∪ y.primeFactors))]
  · rw [← prod_mul_distrib, ← prod_mul_distrib]
    apply prod_congr rfl
    intro p _
    rcases Nat.le_or_le (x.factorization p) (y.factorization p) with h | h <;>
      simp only [factorization_lcm hx hy, Finsupp.sup_apply, h, sup_of_le_right,
        sup_of_le_left, inf_of_le_right, factorization_gcd hx hy, Finsupp.inf_apply,
        inf_of_le_left, mul_comm]
  · apply subset_union_right
  · apply subset_union_left
  · rw [factorization_gcd hx hy, Finsupp.support_inf]
    apply inter_subset_union
  · simp [factorization_lcm hx hy]

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

Goal state before:
pp: case refine_2
ι : 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 : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ⇑σ⁻¹) ↑s
⊢ MonovaryOn (f ∘ ⇑σ) g ↑s

pp: case refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ⇑σ) g ↑s
⊢ MonovaryOn f (g ∘ ⇑σ⁻¹) ↑s

Tactic:
· convert! h.comp_right σ
    · rw [comp_assoc, inv_def, symm_comp_self, comp_id]
    · rw [σ.eq_preimage_iff_image_eq, Set.image_perm hσ]

Goal state after:
case refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ⇑σ) g ↑s
⊢ MonovaryOn f (g ∘ ⇑σ⁻¹) ↑s
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
⊢ mk (f 1) = mk 1

Tactic:
map_one

Goal state after:
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
⊢ mk 1 = mk 1
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r s : ℝ≥0∞
hrs : r ≤ s
⊢ ⌈r⌉ₑ ≤ ⌈s⌉ₑ

Tactic:
simpa using hrs.trans le_ceil_self

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

Goal state before:
pp: a : ℝ≥0∞
⊢ toENNReal ⁻¹' Ioi a = Ioi ⌊a⌋ₑ

Tactic:
ext; simp

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

Goal state before:
pp: a : ℝ≥0∞
⊢ toENNReal ⁻¹' Iio a = Iio ⌈a⌉ₑ

Tactic:
ext; simp

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

Goal state before:
pp: a : ℝ≥0∞
⊢ toENNReal ⁻¹' Iic a = Iic ⌊a⌋ₑ

Tactic:
ext; simp

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

Goal state before:
pp: a : ℝ≥0∞
⊢ toENNReal ⁻¹' Ici a = Ici ⌈a⌉ₑ

Tactic:
ext; simp

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Icc a b = Icc ⌈a⌉ₑ ⌊b⌋ₑ

Tactic:
ext; simp

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Ico a b = Ico ⌈a⌉ₑ ⌈b⌉ₑ

Tactic:
ext; simp

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Ioc a b = Ioc ⌊a⌋ₑ ⌊b⌋ₑ

Tactic:
ext; simp

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Ioo a b = Ioo ⌊a⌋ₑ ⌈b⌉ₑ

Tactic:
ext; simp

Goal state after:
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:
rw [mem_coe, mem_Ico] at mx

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.Hom.Lattice

Goal state before:
pp: case inl
ι : Type u_1
K : Type u_2
M : Type u_3
F : Type u_4
inst✝⁶ : Finite ι
inst✝⁵ : Zero K
inst✝⁴ : Zero M
inst✝³ : ConditionallyCompleteLattice M
inst✝² : FunLike F K M
inst✝¹ : ZeroHomClass F K M
inst✝ : NonnegHomClass F K M
x : ι → K
hx : x ≠ 0
v : F
i : ι
hi : x i ≠ 0
this✝ : Nonempty { j // x j ≠ 0 }
this : Nonempty ι
j : ι
h : x j = 0
⊢ 0 ≤ ⨆ i, v (x ↑i)

Tactic:
exact le_ciSup_of_le ⟨i, hi⟩ (apply_nonneg ..)

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

Goal state before:
pp: case neg
α : 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)
⊢ ⊥ ≤ some s

Tactic:
· exact bot_le

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

Goal state before:
pp: case neg
α : 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)
⊢ ⊥ ≤ some t

Tactic:
· exact bot_le

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

Goal state before:
pp: case neg.bot
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
h : ¬x✝ ⊆ {⊥}
ha : ⊥ ∈ x✝
⊢ ⊥ ≤ ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }

pp: case neg.coe
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
h : ¬x✝ ⊆ {⊥}
a✝ : NonemptyInterval α
ha : ↑a✝ ∈ x✝
⊢ ↑a✝ ≤ ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }

Tactic:
· exact bot_le

Goal state after:
case neg.coe
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
h : ¬x✝ ⊆ {⊥}
a✝ : NonemptyInterval α
ha : ↑a✝ ∈ x✝
⊢ ↑a✝ ≤ ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t✝ s t : NonemptyInterval α
h : s * t = 1
⊢ s⁻¹ = t

Tactic:
obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.mul_eq_one_iff.1 h

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : NonemptyInterval α
a b : α
hab : a * b = 1
h : pure a * pure b = 1
⊢ (pure a)⁻¹ = pure b
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✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ upperBounds x✝
h : x✝ ⊆ {⊥}
⊢ ⊥ ≤ s

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ upperBounds x✝
h : ¬x✝ ⊆ {⊥}
⊢ ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ } ≤ s

Tactic:
· exact bot_le

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ upperBounds x✝
h : ¬x✝ ⊆ {⊥}
⊢ ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ } ≤ s
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
h : ¬(⊥ ∉ s₁ ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2)
⊢ ⊥ ≤ s

Tactic:
· exact bot_le

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero S
f : ZeroHom R S
⊢ map 0 f = 0

Tactic:
ext; simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
V : Type u_8
inst✝² : Zero V
inst✝¹ : SMulZeroClass R V
inst✝ : Zero Γ
r : R
x : V⟦Γ⟧
h : r • x ≠ 0
⊢ ¬(r • x).order < x.order

Tactic:
have hx : x ≠ 0 := right_ne_zero_of_smul h

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
V : Type u_8
inst✝² : Zero V
inst✝¹ : SMulZeroClass R V
inst✝ : Zero Γ
r : R
x : V⟦Γ⟧
h : r • x ≠ 0
hx : x ≠ 0
⊢ ¬(r • x).order < x.order
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
V : Type u_8
inst✝² : Zero V
inst✝¹ : SMulZeroClass R V
inst✝ : DecidableLT Γ
c : Γ
r : R
x : V⟦Γ⟧
⊢ (truncLT c) (r • x) = r • (truncLT c) x

Tactic:
ext; simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : AddMonoid S
f : R →+ S
x y : R⟦Γ⟧
⊢ (x + y).map f = x.map f + y.map f

Tactic:
ext; simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
⊢ BddBelow (Function.support f)

Tactic:
refine ⟨n, fun _ ↦ ?_⟩

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
x✝ : Γ
⊢ x✝ ∈ Function.support f → n ≤ x✝
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : Zero R
inst✝¹ : PartialOrder Γ
inst✝ : DecidableLT Γ
c : Γ
⊢ { coeff := fun i ↦ if i < c then coeff 0 i else 0, isPWO_support' := ⋯ } = 0

Tactic:
ext; simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x : R⟦Γ⟧
⊢ (-x).map f = -x.map f

Tactic:
ext; simp

Goal state after: