harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_div_distrib [DivisionCommMonoid G] {f g : α → G} (hf : (mulSupport f).Finite)
    (hg : (mulSupport g).Finite) : ∏ᶠ i, f i / g i = (∏ᶠ i, f i) / ∏ᶠ i, g i

Proof state:
α : Type u_1
G : Type u_4
inst✝ : DivisionCommMonoid G
f g : α → G
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ ∏ᶠ (i : α), f i / g i = (∏ᶠ (i : α), f i) / ∏ᶠ (i : α), g i

Tactic:
simp only [div_eq_mul_inv, finprod_mul_distrib hf ((mulSupport_inv g).symm.rec hg),
  finprod_inv_distrib]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem out_dvd_iff (a : α) (b : Associates α) : b.out ∣ a ↔ b ≤ Associates.mk a :=
  Quotient.inductionOn b <| by
    simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
b : Associates α
⊢ ∀ (a_1 : α), Associates.out ⟦a_1⟧ ∣ a ↔ ⟦a_1⟧ ≤ Associates.mk a

Tactic:
simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_smul_id {S : Type*} [SMulZeroClass S R] [ContinuousConstSMul S R]
    [SMulZeroClass S A] [IsScalarTower S R A] [IsScalarTower S R (R → R)]
    (s : S) (a : A) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
S : Type u_3
inst✝⁴ : SMulZeroClass S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
a : A
ha : autoParam (p a) _auto✝
⊢ cfcₙ (fun x => s • x) a = s • a

Tactic:
rw [cfcₙ_smul s _ a, cfcₙ_id' R a]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem singleton_mul_subgroup {H : Subgroup G} {h : G} (hh : h ∈ H) : {h} * (H : Set G) = H

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ {h} * ↑H = ↑H

Tactic:
simp [preimage, mul_mem_cancel_left (inv_mem hh)]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem arrowCongr_comp {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂)
    (f : α₁ → β₁) (g : β₁ → γ₁) :
    arrowCongr ea ec (g ∘ f) = arrowCongr eb ec g ∘ arrowCongr ea eb f

Proof state:
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ → β₁
g : β₁ → γ₁
⊢ (ea.arrowCongr ec) (g ∘ f) = (eb.arrowCongr ec) g ∘ (ea.arrowCongr eb) f

Tactic:
ext

Result:
case h
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ → β₁
g : β₁ → γ₁
x✝ : α₂
⊢ (ea.arrowCongr ec) (g ∘ f) x✝ = ((eb.arrowCongr ec) g ∘ (ea.arrowCongr eb) f) x✝

Proof state:
case h
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ → β₁
g : β₁ → γ₁
x✝ : α₂
⊢ (ea.arrowCongr ec) (g ∘ f) x✝ = ((eb.arrowCongr ec) g ∘ (ea.arrowCongr eb) f) x✝

Tactic:
simp only [comp, arrowCongr_apply, eb.symm_apply_apply]

Result:
no goals
-- Mathlib/AlgebraicTopology/ModelCategory/IsCofibrant.lean
lemma isCofibrant_iff_of_isInitial [(cofibrations C).RespectsIso]
    {A X : C} (i : A ⟶ X) (hA : IsInitial A) :
    IsCofibrant X ↔ Cofibration i

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : CategoryWithCofibrations C
inst✝¹ : HasInitial C
inst✝ : (cofibrations C).RespectsIso
A X : C
i : A ⟶ X
hA : IsInitial A
⊢ cofibrations C (initial.to X) ↔ cofibrations C i

Tactic:
apply (cofibrations C).arrow_mk_iso_iff

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : CategoryWithCofibrations C
inst✝¹ : HasInitial C
inst✝ : (cofibrations C).RespectsIso
A X : C
i : A ⟶ X
hA : IsInitial A
⊢ Arrow.mk (initial.to X) ≅ Arrow.mk i

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : CategoryWithCofibrations C
inst✝¹ : HasInitial C
inst✝ : (cofibrations C).RespectsIso
A X : C
i : A ⟶ X
hA : IsInitial A
⊢ IsCofibrant X ↔ Cofibration i

Tactic:
simp only [isCofibrant_iff, cofibration_iff]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : CategoryWithCofibrations C
inst✝¹ : HasInitial C
inst✝ : (cofibrations C).RespectsIso
A X : C
i : A ⟶ X
hA : IsInitial A
⊢ cofibrations C (initial.to X) ↔ cofibrations C i

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : CategoryWithCofibrations C
inst✝¹ : HasInitial C
inst✝ : (cofibrations C).RespectsIso
A X : C
i : A ⟶ X
hA : IsInitial A
⊢ Arrow.mk (initial.to X) ≅ Arrow.mk i

Tactic:
exact Arrow.isoMk (IsInitial.uniqueUpToIso initialIsInitial hA) (Iso.refl _)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma natDegree_preΨ₄_le : W.preΨ₄.natDegree ≤ 6

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 +
          C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X +
        C (W.b₄ * W.b₈ - W.b₆ ^ 2)).natDegree ≤
    6

Tactic:
compute_degree

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.preΨ₄.natDegree ≤ 6

Tactic:
rw [preΨ₄]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 +
          C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X +
        C (W.b₄ * W.b₈ - W.b₆ ^ 2)).natDegree ≤
    6
-- Mathlib/Analysis/Convex/Function.lean
theorem StrictConvexOn.translate_left (hf : StrictConvexOn 𝕜 s f) (c : E) :
    StrictConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCancelCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
c : E
⊢ StrictConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)

Tactic:
simpa only [add_comm] using hf.translate_right c

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem isLittleO_log_rpow_rpow_atTop {s : ℝ} (r : ℝ) (hs : 0 < s) :
    (fun x => log x ^ r) =o[atTop] fun x => x ^ s :=
  let r' := max r 1
  have hr : 0 < r' := lt_max_iff.2 <| Or.inr one_pos
  have H : 0 < s / r' := div_pos hs hr
  calc
    (fun x => log x ^ r) =O[atTop] fun x => log x ^ r' :=
      .of_norm_eventuallyLE <| by
        filter_upwards [tendsto_log_atTop.eventually_ge_atTop 1] with x hx
        rw [Real.norm_of_nonneg (by positivity)]
        gcongr
        exacts [hx, le_max_left _ _]
    _ =o[atTop] fun x => (x ^ (s / r')) ^ r' :=
      ((isLittleO_log_rpow_atTop H).rpow hr <|
        (_root_.tendsto_rpow_atTop H).eventually <| eventually_ge_atTop 0)
    _ =ᶠ[atTop] fun x => x ^ s :=
      (eventually_ge_atTop 0).mono fun x hx ↦ by simp only [← rpow_mul hx, div_mul_cancel₀ _ hr.ne']

Proof state:
s r : ℝ
hs : 0 < s
r' : ℝ := r ⊔ 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ 0 ≤ log x ^ r

Tactic:
positivity

Result:
no goals

Proof state:
case h
s r : ℝ
hs : 0 < s
r' : ℝ := r ⊔ 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ log x ^ r ≤ log x ^ r'

Tactic:
gcongr

Result:
case h.hx
s r : ℝ
hs : 0 < s
r' : ℝ := r ⊔ 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ 1 ≤ log x

case h.hyz
s r : ℝ
hs : 0 < s
r' : ℝ := r ⊔ 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ r ≤ r'

Proof state:
case h
s r : ℝ
hs : 0 < s
r' : ℝ := r ⊔ 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ ‖log x ^ r‖ ≤ log x ^ r'

Tactic:
rw [Real.norm_of_nonneg (by positivity)]

Result:
case h
s r : ℝ
hs : 0 < s
r' : ℝ := r ⊔ 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ log x ^ r ≤ log x ^ r'

Proof state:
case h.hx
s r : ℝ
hs : 0 < s
r' : ℝ := r ⊔ 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ 1 ≤ log x

case h.hyz
s r : ℝ
hs : 0 < s
r' : ℝ := r ⊔ 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ r ≤ r'

Tactic:
exacts [hx, le_max_left _ _]

Result:
no goals

Proof state:
s r : ℝ
hs : 0 < s
r' : ℝ := r ⊔ 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 0 ≤ x
⊢ (fun x => (x ^ (s / r')) ^ r') x = (fun x => x ^ s) x

Tactic:
simp only [← rpow_mul hx, div_mul_cancel₀ _ hr.ne']

Result:
no goals

Proof state:
s r : ℝ
hs : 0 < s
r' : ℝ := r ⊔ 1
hr : 0 < r'
H : 0 < s / r'
⊢ (fun x => ‖log x ^ r‖) ≤ᶠ[atTop] fun x => log x ^ r'

Tactic:
filter_upwards [tendsto_log_atTop.eventually_ge_atTop 1] with x hx

Result:
case h
s r : ℝ
hs : 0 < s
r' : ℝ := r ⊔ 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ ‖log x ^ r‖ ≤ log x ^ r'
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_intCast_nonneg (n : ℤ) : 0 ≤ log n

Proof state:
case inl
n : ℤ
hn : 0 < n
⊢ 0 ≤ log ↑n

Tactic:
have : (1 : ℝ) ≤ n := mod_cast hn

Result:
case inl
n : ℤ
hn : 0 < n
this : 1 ≤ ↑n
⊢ 0 ≤ log ↑n

Proof state:
n : ℤ
hn : 0 < -n
⊢ 1 ≤ -↑n

Tactic:
exact mod_cast hn

Result:
no goals

Proof state:
case inl
n : ℤ
hn : 0 < n
this : 1 ≤ ↑n
⊢ 0 ≤ log ↑n

Tactic:
exact log_nonneg this

Result:
no goals

Proof state:
case inr.inr
n : ℤ
hn : n < 0
⊢ 0 ≤ log ↑n

Tactic:
have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn; exact mod_cast hn

Result:
case inr.inr
n : ℤ
hn : n < 0
this : 1 ≤ -↑n
⊢ 0 ≤ log ↑n

Proof state:
n : ℤ
⊢ 0 ≤ log ↑n

Tactic:
cases lt_trichotomy 0 n with
| inl hn =>
    have : (1 : ℝ) ≤ n := mod_cast hn
    exact log_nonneg this
| inr hn =>
    cases hn with
    | inl hn => simp [hn.symm]
    | inr hn =>
        have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn; exact mod_cast hn
        rw [← log_neg_eq_log]
        exact log_nonneg this

Result:
no goals

Proof state:
case inr
n : ℤ
hn : 0 = n ∨ n < 0
⊢ 0 ≤ log ↑n

Tactic:
cases hn with
| inl hn => simp [hn.symm]
| inr hn =>
    have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn; exact mod_cast hn
    rw [← log_neg_eq_log]
    exact log_nonneg this

Result:
no goals

Proof state:
n : ℤ
hn : n < 0
⊢ 1 ≤ -↑n

Tactic:
rw [← neg_zero, ← lt_neg] at hn

Result:
n : ℤ
hn : 0 < -n
⊢ 1 ≤ -↑n

Proof state:
case inr.inl
n : ℤ
hn : 0 = n
⊢ 0 ≤ log ↑n

Tactic:
simp [hn.symm]

Result:
no goals

Proof state:
case inr.inr
n : ℤ
hn : n < 0
this : 1 ≤ -↑n
⊢ 0 ≤ log (-↑n)

Tactic:
exact log_nonneg this

Result:
no goals

Proof state:
case inr.inr
n : ℤ
hn : n < 0
this : 1 ≤ -↑n
⊢ 0 ≤ log ↑n

Tactic:
rw [← log_neg_eq_log]

Result:
case inr.inr
n : ℤ
hn : n < 0
this : 1 ≤ -↑n
⊢ 0 ≤ log (-↑n)
-- Mathlib/CategoryTheory/Preadditive/Basic.lean
lemma epi_of_isZero_cokernel' {X Y : C} {f : X ⟶ Y} (c : CokernelCofork f) (hc : IsColimit c)
    (h : IsZero c.pt) : Epi f := epi_of_cancel_zero _ (fun g hg => by
  obtain ⟨a, ha⟩ := CokernelCofork.IsColimit.desc' hc _ hg
  rw [← ha, h.eq_of_src a 0, Limits.comp_zero])

Proof state:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero c.pt
R✝ : C
g : Y ⟶ R✝
hg : f ≫ g = 0
a : c.pt ⟶ R✝
ha : Cofork.π c ≫ a = g
⊢ g = 0

Tactic:
rw [← ha, h.eq_of_src a 0, Limits.comp_zero]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero c.pt
R✝ : C
g : Y ⟶ R✝
hg : f ≫ g = 0
⊢ g = 0

Tactic:
obtain ⟨a, ha⟩ := CokernelCofork.IsColimit.desc' hc _ hg

Result:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero c.pt
R✝ : C
g : Y ⟶ R✝
hg : f ≫ g = 0
a : c.pt ⟶ R✝
ha : Cofork.π c ≫ a = g
⊢ g = 0
-- Mathlib/Data/List/Sublists.lean
theorem sublists_eq_sublistsFast : @sublists = @sublistsFast

Proof state:
case H
α : Type u_1
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    (Array.foldl (fun r l => (r.push l).push (x :: l)) #[] y.toList.toArray).toList =
      (Array.foldl (fun r l => (r.push l).push (x :: l)) (Array.mkEmpty (y.size * 2)) y).toList

Tactic:
intros _ _

Result:
case H
α : Type u_1
l : List α
x✝ : α
y✝ : Array (List α)
⊢ (Array.foldl (fun r l => (r.push l).push (x✝ :: l)) #[] y✝.toList.toArray).toList =
    (Array.foldl (fun r l => (r.push l).push (x✝ :: l)) (Array.mkEmpty (y✝.size * 2)) y✝).toList

Proof state:
α : Type u_1
l : List α
⊢ foldr sublistsAux [[]] l = l.sublistsFast

Tactic:
simp only [sublistsFast, sublistsAux_eq_array_foldl, Array.foldr_toList]

Result:
α : Type u_1
l : List α
⊢ foldr (fun a r => (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] r.toArray).toList) [[]] l =
    (foldr (fun a arr => Array.foldl (fun r l => (r.push l).push (a :: l)) (Array.mkEmpty (arr.size * 2)) arr) #[[]]
        l).toList

Proof state:
α : Type u_1
l : List α
⊢ l.sublists = foldr sublistsAux [[]] l

Tactic:
rw [sublistsAux_eq_flatMap, sublists]

Result:
no goals

Proof state:
⊢ @sublists = @sublistsFast

Tactic:
ext α l : 2

Result:
case h.h
α : Type u_1
l : List α
⊢ l.sublists = l.sublistsFast

Proof state:
case H
α : Type u_1
l : List α
x✝ : α
y✝ : Array (List α)
⊢ (Array.foldl (fun r l => (r.push l).push (x✝ :: l)) #[] y✝.toList.toArray).toList =
    (Array.foldl (fun r l => (r.push l).push (x✝ :: l)) (Array.mkEmpty (y✝.size * 2)) y✝).toList

Tactic:
congr

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ foldr (fun a r => (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] r.toArray).toList) [[]] l =
    (foldr (fun a arr => Array.foldl (fun r l => (r.push l).push (a :: l)) (Array.mkEmpty (arr.size * 2)) arr) #[[]]
        l).toList

Tactic:
rw [← foldr_hom Array.toList]

Result:
case H
α : Type u_1
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    (Array.foldl (fun r l => (r.push l).push (x :: l)) #[] y.toList.toArray).toList =
      (Array.foldl (fun r l => (r.push l).push (x :: l)) (Array.mkEmpty (y.size * 2)) y).toList

Proof state:
case h.h
α : Type u_1
l : List α
⊢ l.sublists = l.sublistsFast

Tactic:
trans l.foldr sublistsAux [[]]

Result:
α : Type u_1
l : List α
⊢ l.sublists = foldr sublistsAux [[]] l

α : Type u_1
l : List α
⊢ foldr sublistsAux [[]] l = l.sublistsFast
-- Mathlib/Topology/Algebra/Module/Cardinality.lean
theorem cardinal_eq_of_isOpen
    {E : Type*} (𝕜 : Type*) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
    [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E}
    (hs : IsOpen s) (h's : s.Nonempty) : #s = #E

Proof state:
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen s
h's : s.Nonempty
⊢ #↑s = #E

Tactic:
rcases h's with ⟨x, hx⟩

Result:
case intro
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen s
x : E
hx : x ∈ s
⊢ #↑s = #E

Proof state:
case intro
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen s
x : E
hx : x ∈ s
⊢ #↑s = #E

Tactic:
exact cardinal_eq_of_mem_nhds 𝕜 (hs.mem_nhds hx)

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
/-- The Schnirelmann density of any finite set is `0`. -/
lemma schnirelmannDensity_finite {A : Set ℕ} [DecidablePred (· ∈ A)] (hA : A.Finite) :
    schnirelmannDensity A = 0

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : A.Finite
⊢ schnirelmannDensity A = 0

Tactic:
simpa using schnirelmannDensity_finset hA.toFinset

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma monic_polynomial : W'.polynomial.Monic

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
a✝ : Nontrivial R
⊢ W'.polynomial.Monic

Tactic:
simpa only [polynomial_eq] using Cubic.monic_of_b_eq_one'

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ W'.polynomial.Monic

Tactic:
nontriviality R

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
a✝ : Nontrivial R
⊢ W'.polynomial.Monic
-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
@[simp]
lemma klDiv_zero_left [IsFiniteMeasure ν] : klDiv 0 ν = ν univ

Proof state:
α : Type u_1
mα : MeasurableSpace α
ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ klDiv 0 ν = ν univ

Tactic:
convert klDiv_of_ac_of_integrable (Measure.AbsolutelyContinuous.zero _) integrable_zero_measure

Result:
case h.e'_3
α : Type u_1
mα : MeasurableSpace α
ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ν univ = ENNReal.ofReal (∫ (x : α), llr 0 ν x ∂0 + (ν univ).toReal - (0 univ).toReal)

Proof state:
case h.e'_3
α : Type u_1
mα : MeasurableSpace α
ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ν univ = ENNReal.ofReal (∫ (x : α), llr 0 ν x ∂0 + (ν univ).toReal - (0 univ).toReal)

Tactic:
simp [integral_zero_measure, EReal.coe_zero]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/LazyList.lean
theorem mem_nil {α} (x : α) : x ∈ @LazyList.nil α ↔ False

Proof state:
α : Type u_1
x : α
⊢ x ∈ nil ↔ False

Tactic:
simp [Membership.mem, LazyList.Mem]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem zeroLocus_eq_iff {I J : Ideal R} :
    zeroLocus (I : Set R) = zeroLocus J ↔ I.radical = J.radical

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : I.radical = J.radical
⊢ zeroLocus ↑I = zeroLocus ↑J

Tactic:
rw [← zeroLocus_radical, h, zeroLocus_radical]

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ zeroLocus ↑I = zeroLocus ↑J → I.radical = J.radical

Tactic:
intro h

Result:
case mp
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : zeroLocus ↑I = zeroLocus ↑J
⊢ I.radical = J.radical

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ zeroLocus ↑I = zeroLocus ↑J ↔ I.radical = J.radical

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ zeroLocus ↑I = zeroLocus ↑J → I.radical = J.radical

case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I.radical = J.radical → zeroLocus ↑I = zeroLocus ↑J

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I.radical = J.radical → zeroLocus ↑I = zeroLocus ↑J

Tactic:
intro h

Result:
case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : I.radical = J.radical
⊢ zeroLocus ↑I = zeroLocus ↑J

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : zeroLocus ↑I = zeroLocus ↑J
⊢ I.radical = J.radical

Tactic:
simp_rw [← vanishingIdeal_zeroLocus_eq_radical, h]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Intersecting.lean
theorem intersecting_iff_pairwise_not_disjoint :
    s.Intersecting ↔ (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}

Proof state:
case refine_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : ⊥ ∈ s
hab : b = ⊥
this : a = b
⊢ False

Tactic:
exact
  h.2
    (eq_singleton_iff_unique_mem.2
      ⟨hb, fun c hc => not_ne_iff.1 fun H => h.1 hb hc H.symm disjoint_bot_left⟩)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
⊢ False

Tactic:
have := h.1.eq ha hb (Classical.not_not.2 hab)

Result:
case refine_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
this : a = b
⊢ False

Proof state:
case refine_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
this : a = b
⊢ False

Tactic:
rw [this, disjoint_self] at hab

Result:
case refine_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : b = ⊥
this : a = b
⊢ False

Proof state:
case refine_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
h : {⊥}.Intersecting
⊢ False

Tactic:
exact intersecting_singleton.1 h rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
⊢ s.Intersecting ↔ (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}

Tactic:
refine ⟨fun h => ⟨fun a ha b hb _ => h ha hb, ?_⟩, fun h a ha b hb hab => ?_⟩

Result:
case refine_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : s.Intersecting
⊢ s ≠ {⊥}

case refine_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
⊢ False

Proof state:
case refine_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : b = ⊥
this : a = b
⊢ False

Tactic:
rw [hab] at hb

Result:
case refine_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : ⊥ ∈ s
hab : b = ⊥
this : a = b
⊢ False

Proof state:
case refine_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : s.Intersecting
⊢ s ≠ {⊥}

Tactic:
rintro rfl

Result:
case refine_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
h : {⊥}.Intersecting
⊢ False
-- Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
@[reassoc (attr := simp)]
lemma rightDerivedNatTrans_app (τ : F ⟶ F') (X : C) :
    α.app X ≫ (rightDerivedNatTrans RF RF' α α' W τ).app (L.obj X) =
    τ.app X ≫ α'.app X

Proof state:
C : Type u_1
D : Type u_6
H : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_6} D
inst✝² : Category.{u_2, u_3} H
RF RF' : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
X : C
⊢ α.app X ≫ (RF.rightDerivedNatTrans RF' α α' W τ).app (L.obj X) = τ.app X ≫ α'.app X

Tactic:
dsimp only [rightDerivedNatTrans]

Result:
C : Type u_1
D : Type u_6
H : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_6} D
inst✝² : Category.{u_2, u_3} H
RF RF' : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
X : C
⊢ α.app X ≫ (RF.rightDerivedDesc α W RF' (τ ≫ α')).app (L.obj X) = τ.app X ≫ α'.app X

Proof state:
C : Type u_1
D : Type u_6
H : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_6} D
inst✝² : Category.{u_2, u_3} H
RF RF' : D ⥤ H
F F' : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
X : C
⊢ α.app X ≫ (RF.rightDerivedDesc α W RF' (τ ≫ α')).app (L.obj X) = τ.app X ≫ α'.app X

Tactic:
simp

Result:
no goals