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

Goal state before:
pp: ι : Type u_2
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ |(LinearMap.det ↑((Basis.ofZLatticeBasis ℝ L b).equiv (Pi.basisFun ℝ ι) (Equiv.refl ι)))⁻¹| =
    |(LinearMap.det ↑(Basis.ofZLatticeBasis ℝ L b).equivFun)⁻¹|

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
m✝ n✝ : ℕ
a✝¹ : 0 < m✝
a✝ : m✝ ≤ n✝
⊢ ∀ n_1 ≥ n + m, f (n_1 + 1) ≤ f n_1

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
m✝ n✝ : ℕ
a✝¹ : 0 < m✝
a✝ : m✝ ≤ n✝
⊢ max m✝ (n + m) ≤ max n✝ (n + m)

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
⊢ ∑ k ∈ Ioc k n, (↑k ^ 2)⁻¹ + (↑(n + 1) ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑(n + 1))⁻¹

Tactic:
grw [IH]

Goal state after:
case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
⊢ (↑k)⁻¹ - (↑n)⁻¹ + (↑(n + 1) ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑(n + 1))⁻¹
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹ ≤ 1 / (↑k + 1) + 1 / (↑k + 1)

Tactic:
have A : (1 : α) ≤ k + 1 := by simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]
      simp_rw [← one_div]
      gcongr
      simpa using pow_right_mono₀ A one_le_two

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n ↦ 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
⊢ ¬Summable fun n ↦ if n + 1 ∈ {n | ↑n = k} then 1 / ↑(n + 1) else 0

Tactic:
mem_ofPred,

Goal state after:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n ↦ 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
⊢ ¬Summable fun n ↦ if ↑(n + 1) = k then 1 / ↑(n + 1) else 0
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}
a b : ℕ
ha : a ≤ b
⊢ s a ⊆ s b

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Ring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f - g).toAddMonoidAlgebra = f.toAddMonoidAlgebra - g.toAddMonoidAlgebra

Tactic:
ext : 1; exact DFinsupp.toFinsupp_sub ..

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: case inj
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.Injective AddMonoidAlgebra.toDirectSum

Tactic:
· apply Function.LeftInverse.injective
    apply AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra

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

Goal state before:
pp: α : Type u
l : List α
d : α
n : ℕ
hn : n < l.length
⊢ l.getD n d = l[n]

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
d : α
n : ℕ
hn : l.length ≤ n
⊢ l.getD n d = d

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
i : ℕ
h : i < l.length
⊢ l.reverse.getD i = l.getD (l.length - 1 - i)

Tactic:
grind

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

Goal state before:
pp: α : Type u
d : α
n : ℕ
⊢ [d][n]?.getD d = d

Tactic:
grind

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

Goal state before:
pp: α : Type u
d : α
r n : ℕ
⊢ (replicate r d)[n]?.getD d = d

Tactic:
grind

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

Goal state before:
pp: α : Type u
x y : α
i n : ℕ
h : i < n
⊢ (replicate n x).getD i y = x

Tactic:
grind

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

Goal state before:
pp: α : Type u
l l' : List α
d : α
n : ℕ
h : n < l.length
⊢ (l ++ l').getD n d = l.getD n d

Tactic:
grind

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

Goal state before:
pp: α : Type u
l l' : List α
d : α
n : ℕ
h : l.length ≤ n
⊢ (l ++ l').getD n d = l'.getD (n - l.length) d

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
d : α
this : ∃ x, l.length ≤ x
⊢ ∀ (a : α), (∃ x h, l[x] = a) ∨ True ∧ d = a ↔ a = d ∨ ∃ x h, l[x] = a

Tactic:
grind

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
⊢ (2 * n + 2)‼ = (2 * n + 2) * (2 * n)‼

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
⊢ (2 * n + 1 + 2)‼ = (2 * n + 1 + 2) * (2 * n + 1)‼

Tactic:
rfl

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

Goal state before:
pp: case h₀
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
b✝ : σ → ℕ
a✝² : a.support.sum b✝ = n
a✝¹ : ∀ (i : σ), ¬b✝ i = 0 → ¬a i = 0
a✝ : ¬b✝ = ⇑s
hed : ∀ (a_1 : σ), s a_1 = if a a_1 = 0 then 0 else b✝ a_1
⊢ ↑(Nat.multinomial a.support b✝) * ∏ x ∈ a.support, a x ^ b✝ x = 0

Tactic:
grind

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

Goal state before:
pp: case h₁.inr
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs'' : s.support ⊆ a.support
hs' : ¬∀ (i : σ), s i ≠ 0 → i ∈ a.support
⊢ False

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ ∀ a ∈ s, a ∉ t → f a = 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ ∀ a ∈ t, a ∉ s → g a = 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ ∀ a ∈ s, a ∈ t → f a = g a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hst : s ⊆ t
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s, f a = g a
⊢ ∀ a ∈ s \ t, f a = 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hst : s ⊆ t
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s, f a = g a
⊢ ∀ a ∈ s ∩ t, f a = g a

Tactic:
grind

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
this : (d.sum fun x m ↦ m) = d 0 + d 1
hd : ¬d 0 + d 1 = n
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: a b c : ℕ
⊢ (![a, b, c] 0 + ![a, b, c] 1 + ![a, b, c] 2)! / ((![a, b, c] 0)! * (![a, b, c] 1)! * (![a, b, c] 2)!) =
    (a + b + c)! / (a ! * b ! * c !)

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
ε0' : 0 < ε / 2
⊢ ∃ ia,
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε

Tactic:
have H0 : 0 < (2 : ℝ) ^ Fintype.card ι := pow_pos zero_lt_two _

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
ε0' : 0 < ε / 2
H0 : 0 < 2 ^ Fintype.card ι
⊢ ∃ ia,
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
i : σ
inst✝¹ : IsCancelMulZero R
inst✝ : Nontrivial R
⊢ Prime (X i)

Tactic:
by
  refine ⟨X_ne_zero i, ?_, fun p q ↦ X_dvd_mul_iff.mp⟩
  intro h
  rw [isUnit_iff_exists] at h
  rcases h with ⟨u, hu, -⟩
  apply_fun constantCoeff at hu
  simp at hu

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

Goal state before:
pp: case mp.f
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * (X i * r)
this : X i ∣ p ∨ X i ∣ X i * r
⊢ p ∣ q

Tactic:
obtain rfl : q = p * r := by rw [← X_mul_cancel_left_iff (i := i), hp, mul_left_comm]

Goal state after:
case mp.f
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p : MvPolynomial σ R
inst✝ : IsCancelMulZero R
r : MvPolynomial σ R
this : X i ∣ p ∨ X i ∣ X i * r
hp : X i * (p * r) = p * (X i * r)
⊢ p ∣ p * r
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case insert.e_a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
m : ↥((insert a s).sym n)
⊢ x a ^ Multiset.count a ↑↑m * ↑(Multiset.filter (fun x ↦ a ≠ x) ↑↑m).countPerms *
      (Multiset.map x (Multiset.filter (fun a_1 ↦ ¬a = a_1) ↑↑m)).noncommProd ⋯ =
    x a ^ ↑((symInsertEquiv ha) m).fst * ↑(↑↑((symInsertEquiv ha) m).snd).countPerms *
      (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
rα : α → α → Prop
fst✝¹ snd✝¹ fst✝ snd✝ : α
⊢ GameAdd rα s((fst✝¹, snd✝¹).1, (fst✝¹, snd✝¹).2) s((fst✝, snd✝).1, (fst✝, snd✝).2) ↔
    Prod.GameAdd rα rα (fst✝¹, snd✝¹) (fst✝, snd✝) ∨ Prod.GameAdd rα rα (fst✝¹, snd✝¹).swap (fst✝, snd✝)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) a
⊢ Acc (InvImage (DFinsupp.Lex r fun x ↦ s) toDFinsupp) x

Tactic:
refine InvImage.accessible toDFinsupp (DFinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ ?_)

Goal state after:
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) a
⊢ ∀ i ∈ x.toDFinsupp.support, Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) i
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

Tactic:
rfl

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
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : r j i → j ∈ p
h₂ : ¬r j i
⊢ x j = x j

Tactic:
rfl

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

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : ¬(r j i → j ∈ p)
⊢ x₂ j = x j

Tactic:
rfl

Goal state after:
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : ¬(r j i → j ∈ p)
⊢ x₂ j = x j
Module: Mathlib.Data.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

Tactic:
rfl

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
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

Tactic:
rfl

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
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : ¬r j i
⊢ x j = x j

Tactic:
rfl

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a b : σ →₀ ℕ
⊢ m.toSyn a ≤ m.toSyn a + m.toSyn b

Tactic:
by
  rw [← map_add]
  exact m.toSyn_monotone le_self_add

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ (monomial n) a = C a * (monomial n) 1

Tactic:
C_mul_monomial,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ (monomial n) a = (monomial n) (a * 1)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case right
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
h : p = (monomial m) 1 * r
b : R
hb : b ∣ a
hr : r = C b
⊢ C b * (monomial m) 1 = (monomial m) b

Tactic:
C_mul_monomial,

Goal state after:
case right
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
h : p = (monomial m) 1 * r
b : R
hb : b ∣ a
hr : r = C b
⊢ (monomial m) (b * 1) = (monomial m) b
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case right
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
b : R
hmn : m ≤ n
hb : b ∣ a
h : p = (monomial m) b
⊢ p = C b * (monomial m) 1

Tactic:
C_mul_monomial,

Goal state after:
case right
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
b : R
hmn : m ≤ n
hb : b ∣ a
h : p = (monomial m) b
⊢ p = (monomial m) (b * 1)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

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

Tactic:
dvd_monomial_iff_exists hr,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
⊢ (∃ m b, m ≤ Finsupp.single i 1 ∧ b ∣ r ∧ p = (monomial m) b) ↔
    ∃ s, s ∣ r ∧ (p = C s ∨ p = s • (monomial (Finsupp.single i 1)) 1)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ m.toSyn (m.degree ((monomial d) c)) ≤ m.toSyn d

Tactic:
simp only [degree, AddEquiv.apply_symm_apply]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ ((monomial d) c).support.sup ⇑m.toSyn ≤ m.toSyn d
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ m.degree ((monomial 0) 1) = 0

Tactic:
degree_monomial

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ (if 1 = 0 then 0 else 0) = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
⊢ m.degree (C r) = 0

Tactic:
degree_eq_zero_iff_totalDegree_eq_zero,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).totalDegree = 0
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : LeftPreLieRing L
x y z : L
assoc_xyz : associator x y z = associator y x z
assoc_zxy : associator z x y = associator x z y
assoc_yzx : associator y z x = associator z y x
⊢ 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:
grind

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✝ : LeftPreLieRing 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:
have assoc_xyz := LeftPreLieRing.assoc_symm' x y z
    have assoc_zxy := LeftPreLieRing.assoc_symm' z x y
    have assoc_yzx := LeftPreLieRing.assoc_symm' y z x
    grind

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
assoc_xyz : associator x y z = associator x z y
assoc_zxy : associator z x y = associator z y x
assoc_yzx : associator y z x = associator y x z
⊢ 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:
grind

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

Goal state before:
pp: 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
⊢ #({x ∈ piFinset (tail S) | ¬(eval x) pₖ = 0}.biUnion fun a ↦
        image (fun a_1 ↦ (a_1, a)) ({a_1 ∈ S 0 | (eval ((consEquiv fun i ↦ R) (a_1, a))) p = 0})) =
    #({x ∈ piFinset fun i ↦ tail S i | ¬(eval x) pₖ = 0}.biUnion fun xₜ ↦
        image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}))

Tactic:
rfl

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

Goal state before:
pp: case mp.none
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
e : n.minSqFac = none
⊢ none = none

Tactic:
rfl

Goal state after: