mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: 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 with f ↑p ⋯ = i, ↑p = ∏ a ∈ n.primeFactors.attach with ↑a ∣ t i, ↑a

Tactic:
congr

Goal state after:
case e_s.e_p
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
⊢ (fun p ↦ f ↑p ⋯ = i) = fun a ↦ ↑a ∣ t i
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
ω : α
⊢ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, {n | ω ∈ s n}.indicator (fun x ↦ r) k) atTop atTop =
    Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun x ↦ r) ω) atTop atTop

Tactic:
congr

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

Goal state before:
pp: σ : 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))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = 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₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
this : -∑ i ∈ B, m.leadingCoeff (g i) = m.leadingCoeff (g b)
⊢ ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x + (m.leadingCoeff (g b) * ↑isunit_gb.unit⁻¹) • g b

Tactic:
isunit_gb.mul_val_inv,

Goal state after:
σ : 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))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = 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₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
this : -∑ i ∈ B, m.leadingCoeff (g i) = m.leadingCoeff (g b)
⊢ ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x + 1 • g b
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
d : m.syn
ι : Type u_3
B : Finset ι
g : ι → MvPolynomial σ R
hd : ∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0
hfd : m.toSyn (m.degree (∑ b ∈ B, g b)) < d
⊢ ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)

Tactic:
classical
  induction B using Finset.induction_on with
  | empty => simp
  | insert b B hb h =>
    by_cases hb0 : g b = 0
    · simp_all
    simp? [Finset.sum_insert hb, hb0] at hfd hd says
      simp only [Finset.sum_insert hb, Finset.mem_insert, forall_eq_or_imp, hb0, or_false]
        at hfd hd
    obtain ⟨⟨rfl, isunit_gb⟩, hd⟩ := hd
    use fun b₁ b₂ ↦ if b₂ = b then ↑isunit_gb.unit⁻¹ else 0
    simp? [Finset.sum_insert hb, hb] says
      simp only [Finset.sum_insert hb, ite_smul, zero_smul, ↓reduceIte, Finset.sum_ite_eq', hb,
        add_zero, sPolynomial_self, smul_zero, zero_add]
    simp only [m.toSyn.injective.eq_iff] at *
    trans ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * ↑isunit_gb.unit⁻¹) • g b)
    · suffices (-(∑ i ∈ B, m.leadingCoeff (g i))) = m.leadingCoeff (g b) by
        rw [add_comm, Finset.sum_sub_distrib, sub_eq_add_neg, ← Finset.sum_smul, ← Finset.sum_mul,
          ← neg_smul, ← neg_mul, this, isunit_gb.mul_val_inv, one_smul]
      rw [← add_eq_zero_iff_neg_eq']
      trans (g b).coeff (m.degree <| g b) + ∑ i ∈ B, (g i).coeff (m.degree <| g b)
      · unfold leadingCoeff
        congr 1
        apply Finset.sum_congr rfl
        intro b' hb'
        rcases hd b' hb' with h | h <;> simp [h]
      · rw [← coeff_sum, ← coeff_add, ← notMem_support_iff]
        exact m.notMem_support_of_degree_lt hfd
    · apply Finset.sum_congr rfl
      intro b' hb'
      rw [sPolynomial]
      obtain (⟨h, -⟩ | h) := hd b' hb' <;>
        simp [h, ← smul_eq_C_mul, smul_sub, ← mul_smul, mul_comm (m.leadingCoeff (g b'))]

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

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✝ : PosSMulMono α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
⊢ (∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ #s • ∑ i ∈ s, f i • g i

Tactic:
obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
σ : Perm ι
hσ : σ.IsCycleOn ↑s
hs : {x | σ x ≠ x} ⊆ ↑s
⊢ (∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ #s • ∑ i ∈ s, f i • g i
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case cons.inl
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (a i) < mk (∏ i ∈ s, a i)
⊢ mk (a i) = mk (a ((Finset.cons i s hi).min' ⋯))

Tactic:
congr

Goal state after:
case cons.inl
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (a i) < mk (∏ i ∈ s, a i)
⊢ i = (Finset.cons i s hi).min' ⋯
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case refine_1
ι : 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
⊢ ∑ x ∈ s, f x • g ((Equiv.symm σ) x) = ∑ i ∈ s, f i • g (σ⁻¹ i)

Tactic:
congr

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

Goal state before:
pp: case cons.inr
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a i)
⊢ mk ((∏ x ∈ s, a x) * a i) = mk (a ((Finset.cons i s hi).min' ⋯))

Tactic:
mk_mul_eq_mk_left hlt,

Goal state after:
case cons.inr
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a i)
⊢ mk (∏ i ∈ s, a i) = mk (a ((Finset.cons i s hi).min' ⋯))
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
ha : 1 < a
hab : mk a < mk (b / a)
⊢ 1 < b

Tactic:
suffices a⁻¹ < b / a by
    simpa using this

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
ha : 1 < a
hab : mk a < mk (b / a)
⊢ a⁻¹ < b / a
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: case mk.mk
G : Type u_1
inst✝ : CommGroup G
toSubmonoid✝¹ : Submonoid G
eq_one_of_mem_of_inv_mem'✝¹ : ∀ {a : G}, a ∈ toSubmonoid✝¹.carrier → a⁻¹ ∈ toSubmonoid✝¹.carrier → a = 1
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) { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ }
⊢ { toSubmonoid := toSubmonoid✝¹, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝¹ } =
    { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ }

Tactic:
congr

Goal state after:
case mk.mk
G : Type u_1
inst✝ : CommGroup G
toSubmonoid✝¹ : Submonoid G
eq_one_of_mem_of_inv_mem'✝¹ : ∀ {a : G}, a ∈ toSubmonoid✝¹.carrier → a⁻¹ ∈ toSubmonoid✝¹.carrier → a = 1
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) { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ }
⊢ toSubmonoid✝¹ = toSubmonoid✝
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ ∑ n ∈ range #s, (c - ↑n) = ∑ x ∈ Ioc (c - ↑(#s)) c, x

Tactic:
refine sum_nbij (c - ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ ∀ a ∈ range #s, c - ↑a ∈ Ioc (c - ↑(#s)) c

case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ Set.InjOn (fun x ↦ c - ↑x) ↑(range #s)

case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ Set.SurjOn (fun x ↦ c - ↑x) ↑(range #s) ↑(Ioc (c - ↑(#s)) c)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ ↑(range #s)
⊢ ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑(range #s) → (fun x ↦ c - ↑x) x = (fun x ↦ c - ↑x) x₂ → x = x₂

Tactic:
y

Goal state after:
case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ ↑(range #s)
y : ℕ
⊢ y ∈ ↑(range #s) → (fun x ↦ c - ↑x) x = (fun x ↦ c - ↑x) y → x = y
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 : (c ≤ x ∧ x < c + ↑(#s)) ∧ x ∉ s
⊢ x ≤ c + ↑(#s)

Tactic:
exact mx.1.2.le

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

Goal state before:
pp: case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ ↑(range #s)
⊢ ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑(range #s) → (fun x ↦ c + ↑x) x = (fun x ↦ c + ↑x) x₂ → x = x₂

Tactic:
y

Goal state after:
case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ ↑(range #s)
y : ℕ
⊢ y ∈ ↑(range #s) → (fun x ↦ c + ↑x) x = (fun x ↦ c + ↑x) y → x = y
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x : M₀
⊢ ∀ ⦃b : M₀⦄, x ≤ b → (ofClass WithZero.withZeroUnitsEquiv.symm) x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) b

Tactic:
y

Goal state after:
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : M₀
⊢ x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
x : N₀
⊢ ∀ ⦃b : N₀⦄, x ≤ b → (ofClass WithZero.withZeroUnitsEquiv.symm) x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) b

Tactic:
y

Goal state after:
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : N₀
⊢ x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
x : WithZero (Lex (αˣ × βˣ))
⊢ ∀ ⦃b : WithZero (Lex (αˣ × βˣ))⦄,
    x ≤ b →
      (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun x ≤
        (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun b

Tactic:
y

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
x y : WithZero (Lex (αˣ × βˣ))
⊢ x ≤ y →
    (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun x ≤
      (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun y
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b + 1
⊢ insert (b + 1) (Icc a b) = Icc a (b + 1)

Tactic:
simpa [← succ_eq_add_one] using insert_Icc_right_eq_Icc_succ (succ_eq_add_one b ▸ h)

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

Goal state before:
pp: case mk.mk
α : Type u_1
inst✝ : LE α
toProd✝¹ : α × α
fst_le_snd✝¹ : toProd✝¹.1 ≤ toProd✝¹.2
toProd✝ : α × α
fst_le_snd✝ : toProd✝.1 ≤ toProd✝.2
h : { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ }.toProd = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }.toProd
⊢ { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ } = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }

Tactic:
congr

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 α
inst✝ : NoMinOrder α
a b : α
⊢ Ioc (a - 1) (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_pred_eq_Ico a b

Goal state after:
Module: Mathlib.Data.Finset.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
x✝ : a ∈ {a | (mulAntidiagonal hs ht a).Nonempty}
b : α × α
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 * b.2 = a
⊢ a ∈ s * t

Tactic:
exact ⟨b.1, hb.1, b.2, hb.2⟩

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
H : ∀ (j : Γ), ↑j < i → x.coeff j = 0
⊢ i ≤ x.orderTop

Tactic:
by
    obtain rfl | h := eq_or_ne x 0
    · simp
    · by_contra! hi
      exact x.isWF_support.min_mem (support_nonempty_iff.2 h) (H _ (orderTop_of_ne_zero h ▸ hi))

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

Goal state before:
pp: R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
by_cases h : x + y = 0

Goal state after:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff

case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff
Module: Mathlib.Algebra.Order.Module.PositiveLinearMap

Goal state before:
pp: case mk.mk
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
E₃ : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid E₁
inst✝⁷ : PartialOrder E₁
inst✝⁶ : AddCommMonoid E₂
inst✝⁵ : PartialOrder E₂
inst✝⁴ : AddCommMonoid E₃
inst✝³ : PartialOrder E₃
inst✝² : Module R E₁
inst✝¹ : Module R E₂
inst✝ : Module R E₃
toLinearMap✝¹ : E₁ →ₗ[R] E₂
monotone'✝¹ : Monotone toLinearMap✝¹.toFun
toLinearMap✝ : E₁ →ₗ[R] E₂
monotone'✝ : Monotone toLinearMap✝.toFun
h :
  (fun f ↦ f.toFun) { toLinearMap := toLinearMap✝¹, monotone' := monotone'✝¹ } =
    (fun f ↦ f.toFun) { toLinearMap := toLinearMap✝, monotone' := monotone'✝ }
⊢ { toLinearMap := toLinearMap✝¹, monotone' := monotone'✝¹ } = { toLinearMap := toLinearMap✝, monotone' := monotone'✝ }

Tactic:
congr

Goal state after:
case mk.mk
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
E₃ : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid E₁
inst✝⁷ : PartialOrder E₁
inst✝⁶ : AddCommMonoid E₂
inst✝⁵ : PartialOrder E₂
inst✝⁴ : AddCommMonoid E₃
inst✝³ : PartialOrder E₃
inst✝² : Module R E₁
inst✝¹ : Module R E₂
inst✝ : Module R E₃
toLinearMap✝¹ : E₁ →ₗ[R] E₂
monotone'✝¹ : Monotone toLinearMap✝¹.toFun
toLinearMap✝ : E₁ →ₗ[R] E₂
monotone'✝ : Monotone toLinearMap✝.toFun
h :
  (fun f ↦ f.toFun) { toLinearMap := toLinearMap✝¹, monotone' := monotone'✝¹ } =
    (fun f ↦ f.toFun) { toLinearMap := toLinearMap✝, monotone' := monotone'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝
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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
⊢ ∀ ⦃b : FiniteArchimedeanClass M⦄,
    b ∈ ↑f.support → x < b → (fun i ↦ ArchimedeanClass.mk ↑(f i)) x < (fun i ↦ ArchimedeanClass.mk ↑(f i)) b

Tactic:
y

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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
y : FiniteArchimedeanClass M
⊢ y ∈ ↑f.support → x < y → (fun i ↦ ArchimedeanClass.mk ↑(f i)) x < (fun i ↦ ArchimedeanClass.mk ↑(f i)) y
Module: Mathlib.Algebra.Order.Ring.Cone

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : Ring R
toSubsemiring✝¹ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝¹ : ∀ {a : R}, a ∈ toSubsemiring✝¹.carrier → -a ∈ toSubsemiring✝¹.carrier → a = 0
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) { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ }
⊢ { toSubsemiring := toSubsemiring✝¹, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝¹ } =
    { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ }

Tactic:
congr

Goal state after:
case mk.mk
R : Type u_1
inst✝ : Ring R
toSubsemiring✝¹ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝¹ : ∀ {a : R}, a ∈ toSubsemiring✝¹.carrier → -a ∈ toSubsemiring✝¹.carrier → a = 0
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) { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝
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.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ 0 < ↑seed.baseEmbedding x

Tactic:
refine (HahnSeries.lt_iff _ _).mpr ⟨f.support.min' hsupport, ?_, ?_⟩

Goal state after:
case refine_1
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.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ ∀ j < f.support.min' hsupport, (ofLex 0).coeff j = (ofLex (↑seed.baseEmbedding x)).coeff j

case refine_2
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.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ (ofLex 0).coeff (f.support.min' hsupport) < (ofLex (↑seed.baseEmbedding x)).coeff (f.support.min' hsupport)
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
hne : f x ≠ f y
h_lt : f x < f y
⊢ f y = max (f x) (f y)

Tactic:
exact (max_eq_right_of_lt h_lt).symm

Goal state after: