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

Goal state before:
pp: case neg
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this✝¹ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this✝ : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
ε : ℝ
hε : ε > 0
hε' : Metric.ball 0 ε ⊆ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1
x : ↥L
i : ι
hx✝ : ¬x = 0
hx : ‖↑x‖ ≠ 0
this : |ε / 2 * (‖x‖⁻¹ * ↑((b.repr x) i))| < 1
⊢ ε / 2 * ↑|(b.repr x) i| ≤ ‖x‖

Tactic:
rw [abs_mul, abs_mul, abs_inv, mul_left_comm, abs_norm, inv_mul_lt_iff₀ (by positivity),
    mul_one, abs_eq_self.mpr (by positivity), ← Int.cast_abs] at this

Goal state after:
case neg
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this✝¹ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this✝ : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
ε : ℝ
hε : ε > 0
hε' : Metric.ball 0 ε ⊆ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1
x : ↥L
i : ι
hx✝ : ¬x = 0
hx : ‖↑x‖ ≠ 0
this : ε / 2 * ↑|(b.repr x) i| < ‖x‖
⊢ ε / 2 * ↑|(b.repr x) i| ≤ ‖x‖
Module: Mathlib.Algebra.MvPolynomial.Cardinal

Goal state before:
pp: case inl
σ : Type u
R : Type v
inst✝ : CommSemiring R
a✝ : Nontrivial R
h✝ : IsEmpty σ
⊢ #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀

pp: case inr
σ : Type u
R : Type v
inst✝ : CommSemiring R
a✝ : Nontrivial R
h✝ : Nonempty σ
⊢ #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀

Tactic:
<;>

Goal state after:
case inl
σ : Type u
R : Type v
inst✝ : CommSemiring R
a✝ : Nontrivial R
h✝ : IsEmpty σ
⊢ #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀

case inr
σ : Type u
R : Type v
inst✝ : CommSemiring R
a✝ : Nontrivial R
h✝ : Nonempty σ
⊢ #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
Module: Mathlib.Data.List.GetD

Goal state before:
pp: case nil
α : Type u
inst✝ : Inhabited α
⊢ [].getI 0 = [].headI

pp: case cons
α : Type u
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).getI 0 = (head✝ :: tail✝).headI

Tactic:
<;>

Goal state after:
case nil
α : Type u
inst✝ : Inhabited α
⊢ [].getI 0 = [].headI

case cons
α : Type u
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).getI 0 = (head✝ :: tail✝).headI
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: case zero
M : Type u_1
inst✝¹ : Zero M
x : M
inst✝ : DecidablePred fun x_1 ↦ [x].getD x_1 0 ≠ 0
⊢ [x].toFinsupp 0 = (Finsupp.single 0 x) 0

pp: case succ
M : Type u_1
inst✝¹ : Zero M
x : M
inst✝ : DecidablePred fun x_1 ↦ [x].getD x_1 0 ≠ 0
n✝ : ℕ
⊢ [x].toFinsupp (n✝ + 1) = (Finsupp.single 0 x) (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
M : Type u_1
inst✝¹ : Zero M
x : M
inst✝ : DecidablePred fun x_1 ↦ [x].getD x_1 0 ≠ 0
⊢ [x].toFinsupp 0 = (Finsupp.single 0 x) 0

case succ
M : Type u_1
inst✝¹ : Zero M
x : M
inst✝ : DecidablePred fun x_1 ↦ [x].getD x_1 0 ≠ 0
n✝ : ℕ
⊢ [x].toFinsupp (n✝ + 1) = (Finsupp.single 0 x) (n✝ + 1)
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: case inr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
⊢ Summable fun z ↦ ‖↑z - x‖ ^ r

Tactic:
refine Summable.of_norm_bounded_eventually
    (.mul_left ((1 / 2) ^ r) (summable_norm_rpow L r hr)) ?_

Goal state after:
case inr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
⊢ ∀ᶠ (i : ↥L) in Filter.cofinite, ‖‖↑i - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ 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
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
H : IsClosed ↑L
t : ↥L
ht : t ∈ {x_1 | (fun i ↦ ‖‖↑i - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ
ht₁ : ¬‖t‖ = 0
ht₂ : ‖↑t - x‖ = 0
⊢ ↑t = x

Tactic:
simpa [sub_eq_zero] using ht₂

Goal state after:
Module: Mathlib.Data.Nat.Factorial.DoubleFactorial

Goal state before:
pp: case zero
⊢ (0 + 1)‼ = (0 + 1) * (0 - 1)‼

pp: case succ
n✝ : ℕ
⊢ (n✝ + 1 + 1)‼ = (n✝ + 1 + 1) * (n✝ + 1 - 1)‼

Tactic:
<;>

Goal state after:
case zero
⊢ (0 + 1)‼ = (0 + 1) * (0 - 1)‼

case succ
n✝ : ℕ
⊢ (n✝ + 1 + 1)‼ = (n✝ + 1 + 1) * (n✝ + 1 - 1)‼
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
a : σ →₀ R
s : σ →₀ ℕ
n : ℕ
⊢ coeff s ((linearCombination R X) a ^ n) =
    if (s.sum fun x m ↦ m) = n then ↑s.multinomial * s.prod fun r m ↦ a r ^ m else 0

Tactic:
split_ifs with hs

Goal state after:
case pos
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
a : σ →₀ R
s : σ →₀ ℕ
n : ℕ
hs : (s.sum fun x m ↦ m) = n
⊢ coeff s ((linearCombination R X) a ^ n) = ↑s.multinomial * s.prod fun r m ↦ a r ^ m

case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
a : σ →₀ R
s : σ →₀ ℕ
n : ℕ
hs : ¬(s.sum fun x m ↦ m) = n
⊢ coeff s ((linearCombination R X) a ^ n) = 0
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty.zero
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
hc : (↑∅).Pairwise (Commute on f)
⊢ (∑ i ∈ ∅, f i) ^ 0 = ∑ k ∈ ∅.piAntidiag 0, ↑(multinomial ∅ k) * ∅.noncommProd (fun i ↦ f i ^ k i) ⋯

pp: case empty.succ
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
hc : (↑∅).Pairwise (Commute on f)
n✝ : ℕ
⊢ (∑ i ∈ ∅, f i) ^ (n✝ + 1) = ∑ k ∈ ∅.piAntidiag (n✝ + 1), ↑(multinomial ∅ k) * ∅.noncommProd (fun i ↦ f i ^ k i) ⋯

Tactic:
<;>

Goal state after:
case empty.zero
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
hc : (↑∅).Pairwise (Commute on f)
⊢ (∑ i ∈ ∅, f i) ^ 0 = ∑ k ∈ ∅.piAntidiag 0, ↑(multinomial ∅ k) * ∅.noncommProd (fun i ↦ f i ^ k i) ⋯

case empty.succ
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
hc : (↑∅).Pairwise (Commute on f)
n✝ : ℕ
⊢ (∑ i ∈ ∅, f i) ^ (n✝ + 1) = ∑ k ∈ ∅.piAntidiag (n✝ + 1), ↑(multinomial ∅ k) * ∅.noncommProd (fun i ↦ f i ^ k i) ⋯
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: case hc
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ μ ((Box.Icc I)ᶜ ∩ Box.Icc I) = 0

pp: case hc
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ MeasurableSet (Box.Icc I)ᶜ

Tactic:
<;>

Goal state after:
case hc
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ μ ((Box.Icc I)ᶜ ∩ Box.Icc I) = 0

case hc
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ MeasurableSet (Box.Icc I)ᶜ
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

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

pp: case neg.h
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
H✝ : ∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)
i : σ →₀ ℕ
H : i ∉ Set.range (Finsupp.embDomain f)
⊢ ∀ (u : Fin n →₀ ℕ), Finsupp.mapDomain (⇑f) u = i → coeff u P = 0

Tactic:
<;>

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
H✝ : ∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)
i : σ →₀ ℕ
H : i ∉ Set.range (Finsupp.embDomain f)
⊢ IsNilpotent 0

case neg.h
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
H✝ : ∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)
i : σ →₀ ℕ
H : i ∉ Set.range (Finsupp.embDomain f)
⊢ ∀ (u : Fin n →₀ ℕ), Finsupp.mapDomain (⇑f) u = i → coeff u P = 0
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
P : MvPolynomial σ R
⊢ ∀ (a : R), IsUnit (C a) → IsUnit a

Tactic:
by simp +contextual [isUnit_iff]

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

Goal state before:
pp: case monomial
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
m u✝ : σ →₀ ℕ
a✝ : R
⊢ coeff (p • m) ((expand p) ((monomial u✝) a✝)) = coeff m ((monomial u✝) a✝)

pp: case add
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
m : σ →₀ ℕ
p✝ q✝ : MvPolynomial σ R
a✝¹ : coeff (p • m) ((expand p) p✝) = coeff m p✝
a✝ : coeff (p • m) ((expand p) q✝) = coeff m q✝
⊢ coeff (p • m) ((expand p) (p✝ + q✝)) = coeff m (p✝ + q✝)

Tactic:
<;>

Goal state after:
case monomial
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
m u✝ : σ →₀ ℕ
a✝ : R
⊢ coeff (p • m) ((expand p) ((monomial u✝) a✝)) = coeff m ((monomial u✝) a✝)

case add
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
m : σ →₀ ℕ
p✝ q✝ : MvPolynomial σ R
a✝¹ : coeff (p • m) ((expand p) p✝) = coeff m p✝
a✝ : coeff (p • m) ((expand p) q✝) = coeff m q✝
⊢ coeff (p • m) ((expand p) (p✝ + q✝)) = coeff m (p✝ + q✝)
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: case hC
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
x✝ : R
⊢ (((eval₂Hom f g).comp ↑(expand p)).comp C) x✝ = ((eval₂Hom f (g ^ p)).comp C) x✝

pp: case hX
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
i✝ : σ
⊢ ((eval₂Hom f g).comp ↑(expand p)) (X i✝) = (eval₂Hom f (g ^ p)) (X i✝)

Tactic:
<;>

Goal state after:
case hC
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
x✝ : R
⊢ (((eval₂Hom f g).comp ↑(expand p)).comp C) x✝ = ((eval₂Hom f (g ^ p)).comp C) x✝

case hX
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
i✝ : σ
⊢ ((eval₂Hom f g).comp ↑(expand p)) (X i✝) = (eval₂Hom f (g ^ p)) (X i✝)
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
⊢ ∀ (p : MvPolynomial σ R), (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0

Tactic:
intro p h

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
p : MvPolynomial σ R
h : ∀ x ∈ Set.univ.pi s, (eval x) p = 0
⊢ p = 0
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case neg
x : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
i : ℕ
hi : ¬i = 0
⊢ ((Finsupp.single 0 x + Finsupp.embDomain succEmb l.toFinsupp).update 0 0) i =
    ((Finsupp.embDomain succEmb l.toFinsupp).update 0 0) i

Tactic:
· simp [Finsupp.update_apply, if_neg hi, Finsupp.single_eq_of_ne hi]

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos.refine_1
ι : 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 : ι
hj : r j i
⊢ (x₁.piecewise x {j | r j i}) j = x₁ j

pp: case pos.refine_2
ι : 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)
⊢ (fun {i} ↦ s i) ((x₁.piecewise x {j | r j i}) i) (x₁ i)

pp: case pos.refine_3
ι : 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)
⊢ (fun x ↦ x.2.1.piecewise x.2.2 x.1) ({j | r j i → j ∈ p}, x₁.piecewise x {j | r j i}, x₂) = x

Tactic:
<;>

Goal state after:
case pos.refine_1
ι : 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 : ι
hj : r j i
⊢ (x₁.piecewise x {j | r j i}) j = x₁ j

case pos.refine_2
ι : 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)
⊢ (fun {i} ↦ s i) ((x₁.piecewise x {j | r j i}) i) (x₁ i)

case pos.refine_3
ι : 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)
⊢ (fun x ↦ x.2.1.piecewise x.2.2 x.1) ({j | r j i → j ∈ p}, x₁.piecewise x {j | r j i}, x₂) = x
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : 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
h₂ : r j i
⊢ x₁ j = x j

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
h₂ : ¬r j i
⊢ x j = x j

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 = x j

Tactic:
<;>

Goal state after:
case pos
ι : 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
h₂ : r j i
⊢ x₁ j = x j

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
h₂ : ¬r j i
⊢ x j = x j

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.DFinsupp.WellFounded

Goal state before:
pp: case neg.refine_1
ι : 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 : ι
hj : r j i
⊢ (x₂.piecewise x {j | r j i}) j = x₂ j

pp: case neg.refine_2
ι : 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)
⊢ (fun {i} ↦ s i) ((x₂.piecewise x {j | r j i}) i) (x₂ i)

pp: case neg.refine_3
ι : 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)
⊢ (fun x ↦ x.2.1.piecewise x.2.2 x.1) ({j | r j i ∧ j ∈ p}, x₁, x₂.piecewise x {j | r j i}) = x

Tactic:
<;>

Goal state after:
case neg.refine_1
ι : 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 : ι
hj : r j i
⊢ (x₂.piecewise x {j | r j i}) j = x₂ j

case neg.refine_2
ι : 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)
⊢ (fun {i} ↦ s i) ((x₂.piecewise x {j | r j i}) i) (x₂ i)

case neg.refine_3
ι : 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)
⊢ (fun x ↦ x.2.1.piecewise x.2.2 x.1) ({j | r j i ∧ j ∈ p}, x₁, x₂.piecewise x {j | r j i}) = x
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : 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

pp: case pos
ι : 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)
h₂ : r j i
⊢ x₂ j = x j

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)
h₂ : ¬r j i
⊢ x j = x j

Tactic:
<;>

Goal state after:
case pos
ι : 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

case pos
ι : 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)
h₂ : r j i
⊢ x₂ j = x j

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)
h₂ : ¬r j i
⊢ x j = x j
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case hp
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ (optionEquivLeft R { b // b ≠ n }) ((renameEquiv R (optionSubtypeNe n).symm) p) ≠ 0

pp: case hq
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ (optionEquivLeft R { b // b ≠ n }) ((renameEquiv R (optionSubtypeNe n).symm) q) ≠ 0

Tactic:
<;>

Goal state after:
case hp
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ (optionEquivLeft R { b // b ≠ n }) ((renameEquiv R (optionSubtypeNe n).symm) p) ≠ 0

case hq
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ (optionEquivLeft R { b // b ≠ n }) ((renameEquiv R (optionSubtypeNe n).symm) q) ≠ 0
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
⊢ degree a < degree b ∨ degree a = degree b ∧ toLex a ≤ toLex b

Tactic:
by_cases! ha : a.degree < b.degree

Goal state after:
case pos
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree a < degree b
⊢ degree a < degree b ∨ degree a = degree b ∧ toLex a ≤ toLex b

case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a < degree b ∨ degree a = degree b ∧ toLex a ≤ toLex b
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case f
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
this : m = 0 ∨ m = Finsupp.single i 1
⊢ m = 0 → (monomial m) b = C b

pp: case g
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
this : m = 0 ∨ m = Finsupp.single i 1
⊢ m = Finsupp.single i 1 → (monomial m) b = b • (monomial (Finsupp.single i 1)) 1

Tactic:
<;>

Goal state after:
case f
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
this : m = 0 ∨ m = Finsupp.single i 1
⊢ m = 0 → (monomial m) b = C b

case g
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
this : m = 0 ∨ m = Finsupp.single i 1
⊢ m = Finsupp.single i 1 → (monomial m) b = b • (monomial (Finsupp.single i 1)) 1