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| * |↑((b.repr x) i)| < ‖x‖ * 1
⊢ ε / 2 * ↑|(b.repr x) i| ≤ ‖x‖

Tactic:
mul_one,

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.Module.ZLattice.Covolume

Goal state before:
pp: 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
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ Tendsto (fun n ↦ ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ finrank ℝ E) atTop (𝓝 (volume.real s / covolume L volume))

Tactic:
let b := Module.Free.chooseBasis ℤ L

Goal state after:
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
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ Tendsto (fun n ↦ ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ finrank ℝ E) atTop (𝓝 (volume.real s / covolume L volume))
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: 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
⊢ Tendsto (fun c ↦ ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) atTop
    (𝓝 (volume.real {x | x ∈ X ∧ F x ≤ 1} / covolume L volume))

Tactic:
let b := Module.Free.chooseBasis ℤ L

Goal state after:
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
⊢ Tendsto (fun c ↦ ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) atTop
    (𝓝 (volume.real {x | x ∈ X ∧ F x ≤ 1} / covolume L volume))
Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul

Goal state before:
pp: G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
h₁ : Set.InjOn Prod.fst s
⊢ (f • x) p = ∑ i ∈ f.coeff.support, f.coeff i • x (i⁻¹ • p)

Tactic:
have h₂ : s.MapsTo Prod.fst ↑f.coeff.support := fun g hg ↦ by aesop

Goal state after:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s ↑f.coeff.support
⊢ (f • x) p = ∑ i ∈ f.coeff.support, f.coeff i • x (i⁻¹ • p)
Module: Mathlib.Data.Nat.Factorial.DoubleFactorial

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

Tactic:
mul_one,

Goal state after:
n : ℕ
⊢ (2 * n + 2)‼ = 2 ^ (n + 1) * (n + 1)!
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (∑ x ∈ s, f x + 1) * (∑ x ∈ s, f x)! / (1! * ∏ x ∈ s, (f x)!) = (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)

Tactic:
simp only [factorial, succ_eq_add_one, zero_add, mul_one, one_mul]

Goal state after:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (∑ x ∈ s, f x + 1) * (∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)! = (s.sum f + 1) * ((∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)!)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ (∏ x ∈ ?m.17, (?m.26 x)!) * multinomial s (Pi.single a n) = (∏ x ∈ ?m.17, (?m.26 x)!) * 1

pp: α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ Type ?u.20

pp: α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ Finset ?m.13

pp: α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ ?m.13 → ℕ

Tactic:
mul_one,

Goal state after:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ (∏ x ∈ ?m.17, (?m.26 x)!) * multinomial s (Pi.single a n) = ∏ x ∈ ?m.17, (?m.26 x)!

α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ Type ?u.20

α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ Finset ?m.13

α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ ?m.13 → ℕ
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
P : MvPolynomial σ R
H : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
i : σ
hi : n i ≠ 0
e : Polynomial (MvPolynomial { b // b ≠ i } R) ≃ₐ[R] MvPolynomial σ R :=
  (optionEquivLeft R { b // b ≠ i }).symm.trans (renameEquiv R (Equiv.optionSubtypeNe i))
⊢ IsNilpotent (coeff n P)

Tactic:
have H := (Polynomial.coeff_isUnit_isNilpotent_of_isUnit (H.map e.symm)).2 (n i) hi

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
P : MvPolynomial σ R
H✝ : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
i : σ
hi : n i ≠ 0
e : Polynomial (MvPolynomial { b // b ≠ i } R) ≃ₐ[R] MvPolynomial σ R :=
  (optionEquivLeft R { b // b ≠ i }).symm.trans (renameEquiv R (Equiv.optionSubtypeNe i))
H : IsNilpotent ((e.symm P).coeff (n i))
⊢ IsNilpotent (coeff n P)
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
P : MvPolynomial σ R
inst✝ : IsReduced R
⊢ (∃ r, IsUnit r ∧ P = C r) → IsUnit (coeff 0 P) ∧ P = C (coeff 0 P)

Tactic:
rintro ⟨r, hr, rfl⟩

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsReduced R
r : R
hr : IsUnit r
⊢ IsUnit (coeff 0 (C r)) ∧ C r = C (coeff 0 (C r))
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case inr.succ.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
x✝ : ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hrq : r ∣ q
hp : p = (monomial m) 1 * r
⊢ (monomial m) (1 * 1) * r ∣ (monomial m) 1 * (monomial (n - m)) 1 * q

Tactic:
mul_one,

Goal state after:
case inr.succ.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
x✝ : ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hrq : r ∣ q
hp : p = (monomial m) 1 * r
⊢ (monomial m) 1 * r ∣ (monomial m) 1 * (monomial (n - m)) 1 * q
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: case e'_3
ι : 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 : 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 ι
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : B I * ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := ⋯
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
hsne : s.Nonempty
J : Box ι
hJ : J ∈ π.boxes
hJs : π.tag J ∈ s
e_2✝ : (fun a ↦ 0 < a) = fun x ↦ x ∈ Set.Ioi 0
⊢ δ₁ c (π.tag J) (εs (π.tag J)) = δ c (π.tag J)

Tactic:
exact (if_pos hJs).symm

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

Goal state before:
pp: case insert
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i), x.support = t → (∀ i ∈ t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : x.support = insert b t
h : ∀ i ∈ insert b t, Acc (DFinsupp.Lex r s) (single i (x i))
a : ι
ha : a ∈ t
⊢ Acc (DFinsupp.Lex r s) (single a ((erase b x) a))

Tactic:
rw [erase_ne (ha.ne_of_notMem hb)]

Goal state after:
case insert
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i), x.support = t → (∀ i ∈ t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : x.support = insert b t
h : ∀ i ∈ insert b t, Acc (DFinsupp.Lex r s) (single i (x i))
a : ι
ha : a ∈ t
⊢ Acc (DFinsupp.Lex r s) (single a (x a))
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 * 1) ↔ ∃ s, s ∣ r ∧ (p = C s ∨ p = s • (monomial (Finsupp.single i 1)) 1)

Tactic:
mul_one,

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
⊢ p ∣ (monomial (Finsupp.single i 1)) r ↔ ∃ s, s ∣ r ∧ (p = C s ∨ p = s • (monomial (Finsupp.single i 1)) 1)
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst✝ : DecidablePred P
⊢ {r ∈ piFinset S | P (tail r)} = map (consEquiv α).toEmbedding (S 0 ×ˢ {r ∈ piFinset (tail S) | P r})

Tactic:
by
  simp [← map_consEquiv_filter_piFinset, map_map]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (monomial (m.degree p)) (m.leadingCoeff p * 1) = m.leadingTerm p

Tactic:
mul_one,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (monomial (m.degree p)) (m.leadingCoeff p) = m.leadingTerm p
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #(image (uncurry Sym2.mk) s.offDiag) = (#s * #s - #s * 1) / 2

Tactic:
mul_one,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #(image (uncurry Sym2.mk) s.offDiag) = (#s * #s - #s) / 2
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: case e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ image (uncurry Sym2.mk) (univ ×ˢ univ) ∧ ¬x.IsDiag ↔ ¬x.IsDiag

Tactic:
univ_product_univ,

Goal state after:
case e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ image (uncurry Sym2.mk) univ ∧ ¬x.IsDiag ↔ ¬x.IsDiag
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: case zero
b : ℕ
h : DvdNotUnit 0 b
⊢ (if 0 = 0 then ⊤ else ↑0) < if b = 0 then ⊤ else ↑b

Tactic:
exfalso
      revert h
      simp [DvdNotUnit]

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

Goal state before:
pp: n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
⊢ ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))

Tactic:
nk

Goal state after:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
⊢ n'.MinSqFacProp (n'.minSqFacAux (k + 2))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
⊢ ∀ x_1 ∈ x.val, Irreducible x_1

Tactic:
intro z hz
      apply irreducible_of_normalized_factor z
      · rw [← Multiset.mem_toFinset]
        apply hx hz

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

Goal state before:
pp: case mpr
n p k : ℕ
⊢ 0 < k ∧ n.factorization = Finsupp.single p k → Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rintro ⟨hk, hn⟩
    have hn0 : n ≠ 0 := by
      rintro rfl
      simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
    rw [Nat.eq_pow_of_factorization_eq_single hn0 hn]
    exact ⟨Nat.prime_of_mem_primeFactors <|
      Finsupp.mem_support_iff.2 (by simp [hn, hk.ne'] : n.factorization p ≠ 0), hk, rfl⟩

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

Goal state before:
pp: case refine_1
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : b₁ ^ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ (b₁.pred + 1) ^ 2 * (a₁.pred + 1) = n

Tactic:
simpa only [add_one, succ_pred_eq_of_pos, ha₁, hb₁]

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

Goal state before:
pp: case refine_2
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : b₁ ^ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ Squarefree (a₁.pred + 1)

Tactic:
simpa only [add_one, succ_pred_eq_of_pos, ha₁, hb₁]

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

Goal state before:
pp: n : { n // IsPrimePow n }
⊢ (↑n).minFac ^ ((↑n).factorization (↑n).minFac - 1 + 1) = ↑n

Tactic:
rw [sub_one_add_one (Nat.factorization_minFac_ne_zero n.prop.one_lt),
      n.prop.minFac_pow_factorization_eq]

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

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ a ∈ finAntidiagonal d (Additive.ofMul ⟨n, h⟩),
      (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight a = f) ↔
    ∏ i, f i = n ∧ n ≠ 0

Tactic:
mem_finAntidiagonal,

Goal state after:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ a,
      ∑ i, a i = Additive.ofMul ⟨n, h⟩ ∧
        (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight a = f) ↔
    ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: N : ℕ
⊢ #({x ∈ Ioc 0 N | ¬x = 0}) = N

Tactic:
show {x ∈ Ioc 0 N | ¬x = 0} = Ioc 0 N by ext; simp; lia

Goal state after:
N : ℕ
⊢ #(Ioc 0 N) = N
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ False

Tactic:
apply Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp.1, hi, hj⟩

Goal state after:
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ (f i).Coprime (f j)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ f i * f j ∣ n

Tactic:
rw [← hf.1, ← Finset.mul_prod_erase _ _ his,
    ← Finset.mul_prod_erase _ _ (mem_erase.mpr ⟨hij, mem_univ _⟩), ← mul_assoc]

Goal state after:
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ f i * f j ∣ f i * f j * ∏ x ∈ (univ.erase i).erase j, f x
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
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
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.1.1, ← hcd.2.1] at cop
        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.Algebra.Order.CompleteField

Goal state before:
pp: case e'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) (-(x * -x))

Tactic:
mul_neg,

Goal state after:
case e'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) (- -(x * x))
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) x * (inducedAddHom α β) x = -((inducedAddHom α β) x * -(inducedAddHom α β) x)

Tactic:
mul_neg,

Goal state after:
case e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) x * (inducedAddHom α β) x = - -((inducedAddHom α β) x * (inducedAddHom α β) x)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b : MulArchimedeanOrder M
h : ∀ (n : ℕ), |val b|ₘ ^ n < |val a|ₘ
⊢ ∃ n, |val b|ₘ ≤ |val a|ₘ ^ n

Tactic:
obtain h := (h 1).le

Goal state after:
M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b : MulArchimedeanOrder M
h✝ : ∀ (n : ℕ), |val b|ₘ ^ n < |val a|ₘ
h : |val b|ₘ ^ 1 ≤ |val a|ₘ
⊢ ∃ n, |val b|ₘ ≤ |val a|ₘ ^ n
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: case coe
n : ℕ
x✝ : ℝ≥0
hn₀ : ¬n = 0
⊢ n ≤ ⌈x✝⌉₊ ↔ ↑(n - 1) < x✝

Tactic:
rw [← Nat.add_one_le_ceil_iff, Nat.sub_add_cancel]

Goal state after:
case coe
n : ℕ
x✝ : ℝ≥0
hn₀ : ¬n = 0
⊢ 1 ≤ n
Module: Mathlib.Algebra.Order.Group.Ideal

Goal state before:
pp: case mpr
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
x : M
⊢ (∃ y z, Minimal (fun x ↦ x ∈ I) z ∧ y * z = x) → x ∈ I

Tactic:
· rintro ⟨y, z, hz, rfl⟩
    apply SubMulAction.smul_mem
    exact hz.1

Goal state after: