harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Binomial.lean
theorem descPochhammer_smeval_eq_descFactorial (n k : ℕ) :
    (descPochhammer ℤ k).smeval (n : R) = n.descFactorial k

Proof state:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * ↑(n - k)

Tactic:
by_cases h : n < k

Result:
case pos
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
h : n < k
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * ↑(n - k)

case neg
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
h : ¬n < k
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * ↑(n - k)

Proof state:
case neg
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
h : ¬n < k
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * ↑(n - k)

Tactic:
rw [Nat.cast_sub <| not_lt.mp h]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
⊢ (descPochhammer ℤ (k + 1)).smeval ↑n = ↑(n.descFactorial (k + 1))

Tactic:
rw [descPochhammer_succ_right, Nat.descFactorial_succ, smeval_mul, ih, mul_comm, Nat.cast_mul,
  smeval_sub, smeval_X, smeval_natCast, npow_one, npow_zero, nsmul_one]

Result:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * ↑(n - k)

Proof state:
case pos
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
h : n < k
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * ↑(n - k)

Tactic:
simp only [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, zero_mul]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℕ
⊢ (descPochhammer ℤ 0).smeval ↑n = ↑(n.descFactorial 0)

Tactic:
rw [descPochhammer_zero, Nat.descFactorial_zero, Nat.cast_one, smeval_one, npow_zero, one_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.eq_true_of_and_eq_true_left {a b : Bool} (h : (a && b) = true) : a = true

Proof state:
a b : Bool
h : (a && b) = true
⊢ a = true

Tactic:
simp_all

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/PureCoherence.lean
theorem naturality_whiskerRight {p : a ⟶ b} {f g : b ⟶ c} {h : c ⟶ d} {pf : a ⟶ c} {pfh : a ⟶ d}
    {η : f ≅ g} (η_f : p ≫ f ≅ pf) (η_g : p ≫ g ≅ pf) (η_fh : pf ≫ h ≅ pfh)
    (ih_η : p ◁ η ≪≫ η_g = η_f) :
    p ◁ (η ▷ h) ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp η_f η_fh

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
p : a ⟶ b
f g : b ⟶ c
h : c ⟶ d
pf : a ⟶ c
pfh : a ⟶ d
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_fh : pf ≫ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh).hom = (normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh).hom

Tactic:
simp

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
p : a ⟶ b
f g : b ⟶ c
h : c ⟶ d
pf : a ⟶ c
pfh : a ⟶ d
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_fh : pf ≫ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp η_f η_fh

Tactic:
rw [← ih_η]

Result:
B : Type u
inst✝ : Bicategory B
a b c d : B
p : a ⟶ b
f g : b ⟶ c
h : c ⟶ d
pf : a ⟶ c
pfh : a ⟶ d
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_fh : pf ≫ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
p : a ⟶ b
f g : b ⟶ c
h : c ⟶ d
pf : a ⟶ c
pfh : a ⟶ d
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_fh : pf ≫ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh

Tactic:
apply Iso.ext (by simp)

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem restrict_biUnion (πi : ∀ J, Prepartition J) (hJ : J ∈ π) :
    (π.biUnion πi).restrict J = πi J

Proof state:
case refine_2.intro.intro.intro
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
h₁ : J ∈ π
hx : x ∈ (πi J).iUnion
⊢ x ∈ (πi J).iUnion

Tactic:
exact hx

Result:
no goals

Proof state:
case refine_1
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ J₁ ∈ ((π.biUnion πi).restrict J).boxes

Tactic:
refine (mem_restrict _).2 ⟨J₁, π.mem_biUnion.2 ⟨J, hJ, h₁⟩, (inf_of_le_right ?_).symm⟩

Result:
case refine_1
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ ↑J₁ ≤ ↑J

Proof state:
case refine_2
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ ∀ (x : ι → ℝ), (x ∈ ↑J ∧ ∃ i, ∃ (_ : i ∈ π), x ∈ (πi i).iUnion) → x ∈ (πi J).iUnion

Tactic:
rintro x ⟨hxJ, J₁, h₁, hx⟩

Result:
case refine_2.intro.intro.intro
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
J₁ : Box ι
h₁ : J₁ ∈ π
hx : x ∈ (πi J₁).iUnion
⊢ x ∈ (πi J).iUnion

Proof state:
case refine_2.intro.intro.intro
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
J₁ : Box ι
h₁ : J₁ ∈ π
hx : x ∈ (πi J₁).iUnion
⊢ x ∈ (πi J).iUnion

Tactic:
obtain rfl : J = J₁ := π.eq_of_mem_of_mem hJ h₁ hxJ (iUnion_subset _ hx)

Result:
case refine_2.intro.intro.intro
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
h₁ : J ∈ π
hx : x ∈ (πi J).iUnion
⊢ x ∈ (πi J).iUnion

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ (π.biUnion πi).restrict J = πi J

Tactic:
refine (eq_of_boxes_subset_iUnion_superset (fun J₁ h₁ => ?_) ?_).symm

Result:
case refine_1
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ J₁ ∈ ((π.biUnion πi).restrict J).boxes

case refine_2
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ ((π.biUnion πi).restrict J).iUnion ⊆ (πi J).iUnion

Proof state:
case refine_2
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ ((π.biUnion πi).restrict J).iUnion ⊆ (πi J).iUnion

Tactic:
simp only [iUnion_restrict, iUnion_biUnion, Set.subset_def, Set.mem_inter_iff, Set.mem_iUnion]

Result:
case refine_2
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ ∀ (x : ι → ℝ), (x ∈ ↑J ∧ ∃ i, ∃ (_ : i ∈ π), x ∈ (πi i).iUnion) → x ∈ (πi J).iUnion

Proof state:
case refine_1
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ ↑J₁ ≤ ↑J

Tactic:
exact WithBot.coe_le_coe.2 (le_of_mem _ h₁)

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
lemma homMk'_comp (f : CostructuredArrow S T) (g : Y' ⟶ f.left) (g' : Y'' ⟶ Y') :
    homMk' f (g' ≫ g) = eqToHom (by simp) ≫ homMk' (mk (S.map g ≫ f.hom)) g' ≫ homMk' f g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
Y' Y'' : C
S : C ⥤ D
f : CostructuredArrow S T
g : Y' ⟶ f.left
g' : Y'' ⟶ Y'
⊢ f.homMk' (g' ≫ g) = eqToHom ⋯ ≫ (mk (S.map g ≫ f.hom)).homMk' g' ≫ f.homMk' g

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
Y' Y'' : C
S : C ⥤ D
f : CostructuredArrow S T
g : Y' ⟶ f.left
g' : Y'' ⟶ Y'
⊢ (f.homMk' (g' ≫ g)).left = (eqToHom ⋯ ≫ (mk (S.map g ≫ f.hom)).homMk' g' ≫ f.homMk' g).left

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f : CostructuredArrow S T
g : Y' ⟶ f.left
g' : Y'' ⟶ Y'
⊢ mk (S.map (g' ≫ g) ≫ f.hom) = mk (S.map g' ≫ (mk (S.map g ≫ f.hom)).hom)

Tactic:
simp

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
Y' Y'' : C
S : C ⥤ D
f : CostructuredArrow S T
g : Y' ⟶ f.left
g' : Y'' ⟶ Y'
⊢ (f.homMk' (g' ≫ g)).left = (eqToHom ⋯ ≫ (mk (S.map g ≫ f.hom)).homMk' g' ≫ f.homMk' g).left

Tactic:
simp [eqToHom_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem set_getElem_self {v : Vector α n} {i : Nat} (hi : i < n) :
    v.set i v[i] hi = v

Proof state:
case mk
α : Type u_1
n i : Nat
hi : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.set i { toArray := toArray✝, size_toArray := size_toArray✝ }[i]
      hi =
    { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
⊢ v.set i v[i] hi = v

Tactic:
cases v

Result:
case mk
α : Type u_1
n i : Nat
hi : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.set i { toArray := toArray✝, size_toArray := size_toArray✝ }[i]
      hi =
    { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Data/Set/Card.lean
theorem finite_of_encard_le_coe {k : ℕ} (h : s.encard ≤ k) : s.Finite

Proof state:
α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ s.Finite

Tactic:
rw [← encard_lt_top_iff]

Result:
α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ s.encard < ⊤

Proof state:
α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ s.encard < ⊤

Tactic:
exact h.trans_lt (WithTop.coe_lt_top _)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem pair_mem_product {xs : List α} {ys : List β} {x : α} {y : β} :
    (x, y) ∈ product xs ys ↔ x ∈ xs ∧ y ∈ ys

Proof state:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
x : α
y : β
⊢ (x, y) ∈ xs.product ys ↔ x ∈ xs ∧ y ∈ ys

Tactic:
simp only [product, and_imp, mem_map, Prod.mk.injEq,
  exists_eq_right_right, mem_flatMap, iff_self]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Stalk.lean
lemma germ_stalkClosedPointTo_Spec {R S : CommRingCat} [IsLocalRing S] (φ : R ⟶ S):
    (Spec R).presheaf.germ ⊤ _ trivial ≫ stalkClosedPointTo (Spec.map φ) =
      (ΓSpecIso R).hom ≫ φ

Proof state:
R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ φ ≫
      (ΓSpecIso S).inv ≫
        (Spec S).presheaf.germ (Spec.map φ ⁻¹ᵁ ⊤) (closedPoint ↑S) trivial ≫ (stalkClosedPointIso S).hom =
    φ

Tactic:
simp_rw [Opens.map_top]

Result:
R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ φ ≫ (ΓSpecIso S).inv ≫ (Spec S).presheaf.germ ⊤ (closedPoint ↑S) trivial ≫ (stalkClosedPointIso S).hom = φ

Proof state:
R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ (Spec R).presheaf.germ ⊤ ((ConcreteCategory.hom (Spec.map φ).base) (closedPoint ↑S)) trivial ≫
      stalkClosedPointTo (Spec.map φ) =
    (ΓSpecIso R).hom ≫ φ

Tactic:
rw [stalkClosedPointTo, Scheme.stalkMap_germ_assoc, ← Iso.inv_comp_eq,
  ← ΓSpecIso_inv_naturality_assoc]

Result:
R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ φ ≫
      (ΓSpecIso S).inv ≫
        (Spec S).presheaf.germ (Spec.map φ ⁻¹ᵁ ⊤) (closedPoint ↑S) trivial ≫ (stalkClosedPointIso S).hom =
    φ

Proof state:
R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ φ ≫ (ΓSpecIso S).inv ≫ (Spec S).presheaf.germ ⊤ (closedPoint ↑S) trivial ≫ (stalkClosedPointIso S).hom = φ

Tactic:
rw [germ_stalkClosedPointIso_hom, Iso.inv_hom_id, Category.comp_id]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_approx_start (x a b : ℝ) (h : |exp x - expNear 0 x a| ≤ |x| ^ 0 / Nat.factorial 0 * b) :
    |exp x - a| ≤ b

Proof state:
x a b : ℝ
h : |rexp x - expNear 0 x a| ≤ |x| ^ 0 / ↑(Nat.factorial 0) * b
⊢ |rexp x - a| ≤ b

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Ici {a : α} : (Nat.cast : ℕ → α) ⁻¹' Set.Ici a = Set.Ici ⌈a⌉₊

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ici a ↔ x✝ ∈ Ici ⌈a⌉₊

Tactic:
simp [ceil_le]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ Nat.cast ⁻¹' Ici a = Ici ⌈a⌉₊

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ici a ↔ x✝ ∈ Ici ⌈a⌉₊
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem summable_toNNReal_of_tsum_ne_top {α : Type*} {f : α → ℝ≥0∞} (hf : ∑' i, f i ≠ ∞) :
    Summable (ENNReal.toNNReal ∘ f)

Proof state:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (i : α), f i ≠ ⊤
⊢ Summable (ENNReal.toNNReal ∘ f)

Tactic:
simpa only [← tsum_coe_ne_top_iff_summable, toNNReal_apply_of_tsum_ne_top hf] using hf

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean
theorem isCompact_closedBall {x : E} {r : ℝ} : IsCompact (closedBall x r)

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ IsCompact (⇑toEuclidean.symm '' Metric.closedBall (toEuclidean x) r)

Tactic:
exact (isCompact_closedBall _ _).image toEuclidean.symm.continuous

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ IsCompact (closedBall x r)

Tactic:
rw [closedBall_eq_image]

Result:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ IsCompact (⇑toEuclidean.symm '' Metric.closedBall (toEuclidean x) r)
-- Mathlib/Data/Set/Basic.lean
theorem ite_right (s t : Set α) : s.ite t s = t ∩ s

Proof state:
α : Type u
s t : Set α
⊢ s.ite t s = t ∩ s

Tactic:
simp [Set.ite]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem swap_mem_divisorsAntidiagonal {x : ℕ × ℕ} :
    x.swap ∈ divisorsAntidiagonal n ↔ x ∈ divisorsAntidiagonal n

Proof state:
n : ℕ
x : ℕ × ℕ
⊢ x.swap ∈ n.divisorsAntidiagonal ↔ x ∈ n.divisorsAntidiagonal

Tactic:
rw [mem_divisorsAntidiagonal, mem_divisorsAntidiagonal, mul_comm, Prod.swap]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem singularPart_add (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ]
    [t.HaveLebesgueDecomposition μ] :
    (s + t).singularPart μ = s.singularPart μ + t.singularPart μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
⊢ (s + t).singularPart μ = s.singularPart μ + t.singularPart μ

Tactic:
refine
  (eq_singularPart _ (s.rnDeriv μ + t.rnDeriv μ)
      ((mutuallySingular_singularPart s μ).add_left (mutuallySingular_singularPart t μ))
      ?_).symm

Result:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
⊢ s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
⊢ s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)

Tactic:
rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), add_assoc,
  add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
  singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
  singularPart_add_withDensity_rnDeriv_eq]

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
lemma expect_apply_eq_zero_iff_ne_zero [Finite α] : 𝔼 ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0

Proof state:
case intro
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
val✝ : Fintype α
⊢ 𝔼 ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0

Tactic:
rw [expect_apply_eq_ite, one_ne_zero.ite_eq_right_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ 𝔼 ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0

Tactic:
classical
cases nonempty_fintype α
rw [expect_apply_eq_ite, one_ne_zero.ite_eq_right_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ 𝔼 ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
val✝ : Fintype α
⊢ 𝔼 ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0
-- Mathlib/Data/Set/Basic.lean
theorem inclusion_self (x : s) : inclusion Subset.rfl x = x

Proof state:
α : Type u_1
s : Set α
x : ↑s
⊢ inclusion ⋯ x = x

Tactic:
cases x

Result:
case mk
α : Type u_1
s : Set α
val✝ : α
property✝ : val✝ ∈ s
⊢ inclusion ⋯ ⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Proof state:
case mk
α : Type u_1
s : Set α
val✝ : α
property✝ : val✝ ∈ s
⊢ inclusion ⋯ ⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Complex/Schwarz.lean
theorem dist_le_div_mul_dist_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
    (h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) :
    dist (f z) (f c) ≤ R₂ / R₁ * dist z c

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c

Tactic:
simpa only [dslope_of_ne _ hne, slope_def_module, norm_smul, norm_inv, ← div_eq_inv_mul, ←
  dist_eq_norm, div_le_iff₀ (dist_pos.2 hne)] using norm_dslope_le_div_of_mapsTo_ball hd h_maps hz

Result:
no goals

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f (ball z R₁)
h_maps : MapsTo f (ball z R₁) (ball (f z) R₂)
hz : z ∈ ball z R₁
⊢ dist (f z) (f z) ≤ R₂ / R₁ * dist z z

Tactic:
simp only [dist_self, mul_zero, le_rfl]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c

Tactic:
rcases eq_or_ne z c with (rfl | hne)

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f (ball z R₁)
h_maps : MapsTo f (ball z R₁) (ball (f z) R₂)
hz : z ∈ ball z R₁
⊢ dist (f z) (f z) ≤ R₂ / R₁ * dist z z

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem r_iff_exists {x y : M × S} : r S x y ↔ ∃ c : S, ↑c * (↑y.2 * x.1) = c * (x.2 * y.1)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (r S) x y ↔ ∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)

Tactic:
rw [r_eq_r' S]

Result:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (r' S) x y ↔ ∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (r' S) x y ↔ ∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
theorem uIcc_prod_eq (a b : α × β) : [[a, b]] = [[a.1, b.1]] ×ˢ [[a.2, b.2]]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Lattice α
inst✝ : Lattice β
a b : α × β
⊢ [[a, b]] = [[a.1, b.1]] ×ˢ [[a.2, b.2]]

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Quotient.lean
theorem quotient_map_C_eq_zero {I : Ideal R} :
    ∀ a ∈ I, ((Quotient.mk (map (C : R →+* R[X]) I : Ideal R[X])).comp C) a = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ a ∈ I, ((Quotient.mk (map C I)).comp C) a = 0

Tactic:
intro a ha

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ ((Quotient.mk (map C I)).comp C) a = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ C a ∈ map C I

Tactic:
exact mem_map_of_mem _ ha

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ ((Quotient.mk (map C I)).comp C) a = 0

Tactic:
rw [RingHom.comp_apply, Quotient.eq_zero_iff_mem]

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ C a ∈ map C I
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma norm_natCast_cpow_of_re_ne_zero (n : ℕ) {s : ℂ} (hs : s.re ≠ 0) :
    ‖(n : ℂ) ^ s‖ = (n : ℝ) ^ (s.re)

Proof state:
n : ℕ
s : ℂ
hs : s.re ≠ 0
⊢ ‖↑n ^ s‖ = ↑n ^ s.re

Tactic:
rw [← ofReal_natCast, norm_cpow_eq_rpow_re_of_nonneg n.cast_nonneg hs]

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean
theorem isFiltered_of_isFiltered_costructuredArrow (L : A ⥤ T) (R : B ⥤ T)
    [IsFiltered B] [Final R] [∀ b, IsFiltered (CostructuredArrow L (R.obj b))] : IsFiltered A

Proof state:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
⊢ IsFiltered A

Tactic:
let sB : B ≌ AsSmall.{max u₁ u₂ u₃ v₁ v₂ v₃} B := AsSmall.equiv

Result:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
⊢ IsFiltered A
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg (x : P) (v : V) {r₁ r₂ : R} (hr₁ : r₁ ≤ 0)
    (hr₂ : 0 ≤ r₂) : Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : 0 ≤ r₂
⊢ Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)

Tactic:
convert wbtw_smul_vadd_smul_vadd_of_nonneg_of_le (r₁ • v +ᵥ x) v (Left.nonneg_neg_iff.2 hr₁)
    (neg_le_sub_iff_le_add.2 ((le_add_iff_nonneg_left r₁).2 hr₂)) using 1 <;>
  simp [sub_smul, ← add_vadd]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_mulIndicator_eq_prod_filter (s : Finset ι) (f : ι → κ → β) (t : ι → Set κ) (g : ι → κ)
    [DecidablePred fun i ↦ g i ∈ t i] :
    ∏ i ∈ s, mulIndicator (t i) (f i) (g i) = ∏ i ∈ s with g i ∈ t i, f i (g i)

Proof state:
case refine_2
ι : Type u_1
β : Type u_4
inst✝¹ : CommMonoid β
κ : Type u_6
s : Finset ι
f : ι → κ → β
t : ι → Set κ
g : ι → κ
inst✝ : DecidablePred fun i => g i ∈ t i
⊢ ∏ x ∈ filter (fun x => g x ∉ t x) s, (t x).mulIndicator (f x) (g x) = 1

Tactic:
exact prod_eq_one fun x hx ↦ mulIndicator_of_not_mem (mem_filter.1 hx).2 _

Result:
no goals

Proof state:
case refine_1
ι : Type u_1
β : Type u_4
inst✝¹ : CommMonoid β
κ : Type u_6
s : Finset ι
f : ι → κ → β
t : ι → Set κ
g : ι → κ
inst✝ : DecidablePred fun i => g i ∈ t i
⊢ ∏ x ∈ filter (fun x => g x ∈ t x) s, (t x).mulIndicator (f x) (g x) = ∏ i ∈ filter (fun i => g i ∈ t i) s, f i (g i)

Tactic:
exact prod_congr rfl fun x hx ↦ mulIndicator_of_mem (mem_filter.1 hx).2 _

Result:
no goals