harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Dynamics/BirkhoffSum/Average.lean
theorem birkhoffAverage_congr_ring' (S : Type*) [DivisionSemiring S] [Module S M] :
    birkhoffAverage (α := α) (M := M) R = birkhoffAverage S

Proof state:
case h.h.h.h
R : Type u_1
α : Type u_2
M : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : DivisionSemiring S
inst✝ : Module S M
x✝³ : α → α
x✝² : α → M
x✝¹ : ℕ
x✝ : α
⊢ birkhoffAverage R x✝³ x✝² x✝¹ x✝ = birkhoffAverage S x✝³ x✝² x✝¹ x✝

Tactic:
apply birkhoffAverage_congr_ring

Result:
no goals

Proof state:
R : Type u_1
α : Type u_2
M : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : DivisionSemiring S
inst✝ : Module S M
⊢ birkhoffAverage R = birkhoffAverage S

Tactic:
ext

Result:
case h.h.h.h
R : Type u_1
α : Type u_2
M : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : DivisionSemiring S
inst✝ : Module S M
x✝³ : α → α
x✝² : α → M
x✝¹ : ℕ
x✝ : α
⊢ birkhoffAverage R x✝³ x✝² x✝¹ x✝ = birkhoffAverage S x✝³ x✝² x✝¹ x✝
-- Mathlib/Data/Int/Interval.lean
theorem card_fintype_Ioc_of_le (h : a ≤ b) : (Fintype.card (Set.Ioc a b) : ℤ) = b - a

Proof state:
a b : ℤ
h : a ≤ b
⊢ ↑(Fintype.card ↑(Set.Ioc a b)) = b - a

Tactic:
rw [card_fintype_Ioc, toNat_sub_of_le h]

Result:
no goals
-- Mathlib/Data/List/GetD.lean
theorem getD_append (l l' : List α) (d : α) (n : ℕ) (h : n < l.length) :
    (l ++ l').getD n d = l.getD n d

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

Tactic:
rw [getD_eq_getElem _ _ (Nat.lt_of_lt_of_le h (length_append _ _ ▸ Nat.le_add_right _ _)),
  getElem_append_left h, getD_eq_getElem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem extractLsb_not_of_lt {x : BitVec w} {hi lo : Nat} (hlo : lo ≤ hi) (hhi : hi < w) :
   (~~~ x).extractLsb hi lo = ~~~ (x.extractLsb hi lo)

Proof state:
case pred
w : Nat
x : BitVec w
hi lo : Nat
hlo : lo ≤ hi
hhi : hi < w
k : Nat
hk : k < hi - lo + 1
⊢ (extractLsb hi lo (~~~x)).getLsbD k = (~~~extractLsb hi lo x).getLsbD k

Tactic:
simp [hk, show k ≤ hi - lo by omega]

Result:
case pred
w : Nat
x : BitVec w
hi lo : Nat
hlo : lo ≤ hi
hhi : hi < w
k : Nat
hk : k < hi - lo + 1
⊢ x.getLsbD (lo + k) = false → lo + k < w

Proof state:
w : Nat
x : BitVec w
hi lo : Nat
hlo : lo ≤ hi
hhi : hi < w
k : Nat
hk : k < hi - lo + 1
⊢ k ≤ hi - lo

Tactic:
omega

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
hi lo : Nat
hlo : lo ≤ hi
hhi : hi < w
k : Nat
hk : k < hi - lo + 1
⊢ x.getLsbD (lo + k) = false → lo + k < w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
hi lo : Nat
hlo : lo ≤ hi
hhi : hi < w
⊢ extractLsb hi lo (~~~x) = ~~~extractLsb hi lo x

Tactic:
ext k hk

Result:
case pred
w : Nat
x : BitVec w
hi lo : Nat
hlo : lo ≤ hi
hhi : hi < w
k : Nat
hk : k < hi - lo + 1
⊢ (extractLsb hi lo (~~~x)).getLsbD k = (~~~extractLsb hi lo x).getLsbD k
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma NatTrans.app_homology {F G : C ⥤ D} (τ : F ⟶ G)
    (S : ShortComplex C) [S.HasHomology] [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms]
    [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S]
    [G.PreservesRightHomologyOf S] :
    τ.app S.homology = (S.mapHomologyIso F).inv ≫
      ShortComplex.homologyMap (S.mapNatTrans τ) ≫ (S.mapHomologyIso G).hom

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} C
inst✝⁹ : Category.{u_4, u_2} D
inst✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
F G : C ⥤ D
τ : F ⟶ G
S : ShortComplex C
inst✝⁶ : S.HasHomology
inst✝⁵ : F.PreservesZeroMorphisms
inst✝⁴ : G.PreservesZeroMorphisms
inst✝³ : F.PreservesLeftHomologyOf S
inst✝² : G.PreservesLeftHomologyOf S
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : G.PreservesRightHomologyOf S
⊢ τ.app S.homology = (S.mapHomologyIso F).inv ≫ ShortComplex.homologyMap (S.mapNatTrans τ) ≫ (S.mapHomologyIso G).hom

Tactic:
rw [ShortComplex.homologyMap_mapNatTrans, assoc, assoc, Iso.inv_hom_id,
  comp_id, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma twoTorsionPolynomial_disc_of_char_three : W.twoTorsionPolynomial.disc = W.Δ

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.twoTorsionPolynomial.disc = W.Δ

Tactic:
linear_combination W.twoTorsionPolynomial_disc + 5 * W.Δ * CharP.cast_eq_zero R 3

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Power.lean
theorem mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi {a b c d p : P}
    (h : Cospherical ({a, b, c, d} : Set P)) (hapb : ∠ a p b = π) (hcpd : ∠ c p d = π) :
    dist a p * dist b p = dist c p * dist d p

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapb : ∠ a p b = π
hcpd : ∠ c p d = π
⊢ dist a p * dist b p = dist c p * dist d p

Tactic:
obtain ⟨-, k₁, _, hab⟩ := angle_eq_pi_iff.mp hapb

Result:
case intro.intro.intro
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapb : ∠ a p b = π
hcpd : ∠ c p d = π
k₁ : ℝ
left✝ : k₁ < 0
hab : b -ᵥ p = k₁ • (a -ᵥ p)
⊢ dist a p * dist b p = dist c p * dist d p

Proof state:
case intro.intro.intro
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapb : ∠ a p b = π
hcpd : ∠ c p d = π
k₁ : ℝ
left✝ : k₁ < 0
hab : b -ᵥ p = k₁ • (a -ᵥ p)
⊢ dist a p * dist b p = dist c p * dist d p

Tactic:
obtain ⟨-, k₂, _, hcd⟩ := angle_eq_pi_iff.mp hcpd

Result:
case intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapb : ∠ a p b = π
hcpd : ∠ c p d = π
k₁ : ℝ
left✝¹ : k₁ < 0
hab : b -ᵥ p = k₁ • (a -ᵥ p)
k₂ : ℝ
left✝ : k₂ < 0
hcd : d -ᵥ p = k₂ • (c -ᵥ p)
⊢ dist a p * dist b p = dist c p * dist d p

Proof state:
case intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapb : ∠ a p b = π
hcpd : ∠ c p d = π
k₁ : ℝ
left✝¹ : k₁ < 0
hab : b -ᵥ p = k₁ • (a -ᵥ p)
k₂ : ℝ
left✝ : k₂ < 0
hcd : d -ᵥ p = k₂ • (c -ᵥ p)
⊢ dist a p * dist b p = dist c p * dist d p

Tactic:
exact mul_dist_eq_mul_dist_of_cospherical h ⟨k₁, by linarith, hab⟩ ⟨k₂, by linarith, hcd⟩

Result:
no goals

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapb : ∠ a p b = π
hcpd : ∠ c p d = π
k₁ : ℝ
left✝¹ : k₁ < 0
hab : b -ᵥ p = k₁ • (a -ᵥ p)
k₂ : ℝ
left✝ : k₂ < 0
hcd : d -ᵥ p = k₂ • (c -ᵥ p)
⊢ k₁ ≠ 1

Tactic:
linarith

Result:
no goals

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapb : ∠ a p b = π
hcpd : ∠ c p d = π
k₁ : ℝ
left✝¹ : k₁ < 0
hab : b -ᵥ p = k₁ • (a -ᵥ p)
k₂ : ℝ
left✝ : k₂ < 0
hcd : d -ᵥ p = k₂ • (c -ᵥ p)
⊢ k₂ ≠ 1

Tactic:
linarith

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem isTopologicalBasis_pi {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
    {T : ∀ i, Set (Set (X i))} (cond : ∀ i, IsTopologicalBasis (T i)) :
    IsTopologicalBasis { S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι),
      (∀ i, i ∈ F → U i ∈ T i) ∧ S = (F : Set ι).pi U }

Proof state:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
⊢ IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = (↑F).pi U}

Tactic:
simpa only [Set.pi_def] using IsTopologicalBasis.iInf_induced cond eval

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
lemma Icc_insert_succ_right (h : a ≤ b + 1) : insert (b + 1) (Icc a b) = Icc a (b + 1)

Proof state:
case h
a b : ℕ
h : a ≤ b + 1
x : ℕ
⊢ x = b + 1 ∨ a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b + 1

Tactic:
omega

Result:
no goals

Proof state:
a b : ℕ
h : a ≤ b + 1
⊢ insert (b + 1) (Icc a b) = Icc a (b + 1)

Tactic:
ext x

Result:
case h
a b : ℕ
h : a ≤ b + 1
x : ℕ
⊢ x ∈ insert (b + 1) (Icc a b) ↔ x ∈ Icc a (b + 1)

Proof state:
case h
a b : ℕ
h : a ≤ b + 1
x : ℕ
⊢ x ∈ insert (b + 1) (Icc a b) ↔ x ∈ Icc a (b + 1)

Tactic:
simp only [mem_insert, mem_Icc]

Result:
case h
a b : ℕ
h : a ≤ b + 1
x : ℕ
⊢ x = b + 1 ∨ a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b + 1
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma IsGreatest.nnnorm_cfc [Nontrivial A] (f : 𝕜 → 𝕜) (a : A)
    (hf : ContinuousOn f (σ 𝕜 a)

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ IsGreatest ((fun x => ‖f x‖₊) '' σ 𝕜 a) ‖cfc f a‖₊

Tactic:
convert Real.toNNReal_mono.map_isGreatest (.norm_cfc f a)

Result:
case h.e'_3
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ (fun x => ‖f x‖₊) '' σ 𝕜 a = Real.toNNReal '' ((fun x => ‖f x‖) '' σ 𝕜 a)

case h.e'_4
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ ‖cfc f a‖₊ = ‖cfc f a‖.toNNReal

Proof state:
case h.e'_4
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ ‖cfc f a‖₊ = ‖cfc f a‖.toNNReal

Tactic:
simp [Set.image_image, norm_toNNReal]

Result:
no goals

Proof state:
case h.e'_3
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ (fun x => ‖f x‖₊) '' σ 𝕜 a = Real.toNNReal '' ((fun x => ‖f x‖) '' σ 𝕜 a)

case h.e'_4
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ ‖cfc f a‖₊ = ‖cfc f a‖.toNNReal

Tactic:
all_goals simp [Set.image_image, norm_toNNReal]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
lemma measurable_preCDF' {ρ : Measure (α × ℝ)} :
    Measurable fun a r ↦ (preCDF ρ r a).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ (a : ℚ), Measurable fun x => (preCDF ρ a x).toReal

Tactic:
exact fun _ ↦ measurable_preCDF.ennreal_toReal

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ Measurable fun a r => (preCDF ρ r a).toReal

Tactic:
rw [measurable_pi_iff]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ (a : ℚ), Measurable fun x => (preCDF ρ a x).toReal
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem exists_nonempty_inter_of_measure_univ_lt_tsum_measure {m : MeasurableSpace α}
    (μ : Measure α) {s : ι → Set α} (hs : ∀ i, NullMeasurableSet (s i) μ)
    (H : μ (univ : Set α) < ∑' i, μ (s i)) : ∃ i j, i ≠ j ∧ (s i ∩ s j).Nonempty

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : ∀ (i j : ι), i ≠ j → s i ∩ s j = ∅
i j : ι
hij : i ≠ j
⊢ (AEDisjoint μ on s) i j

Tactic:
exact (disjoint_iff_inter_eq_empty.mpr (H i j hij)).aedisjoint

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : ∀ (i j : ι), i ≠ j → s i ∩ s j = ∅
⊢ ∑' (i : ι), μ (s i) ≤ μ univ

Tactic:
apply tsum_measure_le_measure_univ hs

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : ∀ (i j : ι), i ≠ j → s i ∩ s j = ∅
⊢ Pairwise (AEDisjoint μ on s)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : ∀ (i j : ι), i ≠ j → s i ∩ s j = ∅
⊢ Pairwise (AEDisjoint μ on s)

Tactic:
intro i j hij

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : ∀ (i j : ι), i ≠ j → s i ∩ s j = ∅
i j : ι
hij : i ≠ j
⊢ (AEDisjoint μ on s) i j

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : μ univ < ∑' (i : ι), μ (s i)
⊢ ∃ i j, i ≠ j ∧ (s i ∩ s j).Nonempty

Tactic:
contrapose! H

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : ∀ (i j : ι), i ≠ j → s i ∩ s j = ∅
⊢ ∑' (i : ι), μ (s i) ≤ μ univ
-- Mathlib/Algebra/Ring/Ext.lean
theorem toSemiring_injective :
    Function.Injective (@toSemiring R)

Proof state:
R : Type u
a₁✝ a₂✝ : Ring R
h : toSemiring = toSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Result:
case h_add.h.h
R : Type u
a₁✝ a₂✝ : Ring R
h : toSemiring = toSemiring
x y : R
⊢ x + y = x + y

case h_mul.h.h
R : Type u
a₁✝ a₂✝ : Ring R
h : toSemiring = toSemiring
x y : R
⊢ x * y = x * y

Proof state:
R : Type u
⊢ Function.Injective (@toSemiring R)

Tactic:
intro _ _ h

Result:
R : Type u
a₁✝ a₂✝ : Ring R
h : toSemiring = toSemiring
⊢ a₁✝ = a₂✝
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem mem_closure_pair {x y z : C} :
    z ∈ closure ({x, y} : Set C) ↔ ∃ m n : ℤ, x ^ m * y ^ n = z

Proof state:
C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ z ∈ closure {x, y} ↔ ∃ m n, x ^ m * y ^ n = z

Tactic:
rw [← Set.singleton_union, Subgroup.closure_union, mem_sup]

Result:
C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ (∃ y_1 ∈ closure {x}, ∃ z_1 ∈ closure {y}, y_1 * z_1 = z) ↔ ∃ m n, x ^ m * y ^ n = z

Proof state:
C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ (∃ y_1 ∈ closure {x}, ∃ z_1 ∈ closure {y}, y_1 * z_1 = z) ↔ ∃ m n, x ^ m * y ^ n = z

Tactic:
simp_rw [mem_closure_singleton, exists_exists_eq_and]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem pbind_eq_none {f : ∀ a : α, a ∈ x → Option β}
    (h' : ∀ a (H : a ∈ x), f a H = none → x = none) : x.pbind f = none ↔ x = none

Proof state:
case some
α : Type u_1
β : Type u_2
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
h : f val✝ ⋯ = none
⊢ False

Tactic:
cases h' _ rfl h

Result:
no goals

Proof state:
case some
α : Type u_1
β : Type u_2
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
⊢ (some val✝).pbind f = none ↔ some val✝ = none

Tactic:
simp only [pbind, iff_false, reduceCtorEq]

Result:
case some
α : Type u_1
β : Type u_2
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
⊢ ¬f val✝ ⋯ = none

Proof state:
α : Type u_1
β : Type u_2
x : Option α
f : (a : α) → a ∈ x → Option β
h' : ∀ (a : α) (H : a ∈ x), f a H = none → x = none
⊢ x.pbind f = none ↔ x = none

Tactic:
cases x

Result:
case none
α : Type u_1
β : Type u_2
f : (a : α) → a ∈ none → Option β
h' : ∀ (a : α) (H : a ∈ none), f a H = none → none = none
⊢ none.pbind f = none ↔ none = none

case some
α : Type u_1
β : Type u_2
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
⊢ (some val✝).pbind f = none ↔ some val✝ = none

Proof state:
case some
α : Type u_1
β : Type u_2
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
⊢ ¬f val✝ ⋯ = none

Tactic:
intro h

Result:
case some
α : Type u_1
β : Type u_2
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
h : f val✝ ⋯ = none
⊢ False

Proof state:
case none
α : Type u_1
β : Type u_2
f : (a : α) → a ∈ none → Option β
h' : ∀ (a : α) (H : a ∈ none), f a H = none → none = none
⊢ none.pbind f = none ↔ none = none

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getThenInsertIfNew?_fst [LawfulBEq α] {k : α} {v : β k} :
    (m.getThenInsertIfNew? k v).1 = m.get? k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
k : α
v : β k
⊢ (m.getThenInsertIfNew? k v).fst = m.get? k

Tactic:
rw [getThenInsertIfNew?_eq_get?ₘ, get?_eq_get?ₘ]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
lemma le_induce_union_right : G'.induce s' ≤ G'.induce (s ∪ s')

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ G'.induce s' ≤ G'.induce (s ∪ s')

Tactic:
exact (sup_le_iff.mp le_induce_union).2

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
lemma Integrable.measure_le_integral {f : X → ℝ} (f_int : Integrable f μ) (f_nonneg : 0 ≤ᵐ[μ] f)
    {s : Set X} (hs : ∀ x ∈ s, 1 ≤ f x) :
    μ s ≤ ENNReal.ofReal (∫ x, f x ∂μ)

Proof state:
case hs
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
x : X
hx : x ∈ s
⊢ 1 ≤ ENNReal.ofReal (f x)

Tactic:
simpa using ENNReal.ofReal_le_ofReal (hs x hx)

Result:
no goals

Proof state:
case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ AEMeasurable (fun a => ENNReal.ofReal (f a)) μ

Tactic:
exact ENNReal.continuous_ofReal.measurable.comp_aemeasurable f_int.1.aemeasurable

Result:
no goals

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ μ s ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)

Tactic:
rw [ofReal_integral_eq_lintegral_ofReal f_int f_nonneg]

Result:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ μ s ≤ ∫⁻ (x : X), ENNReal.ofReal (f x) ∂μ

Proof state:
case hs
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ ∀ x ∈ s, 1 ≤ ENNReal.ofReal (f x)

Tactic:
intro x hx

Result:
case hs
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
x : X
hx : x ∈ s
⊢ 1 ≤ ENNReal.ofReal (f x)

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ μ s ≤ ∫⁻ (x : X), ENNReal.ofReal (f x) ∂μ

Tactic:
apply meas_le_lintegral₀

Result:
case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ AEMeasurable (fun a => ENNReal.ofReal (f a)) μ

case hs
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ ∀ x ∈ s, 1 ≤ ENNReal.ofReal (f x)
-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
@[aesop safe]
lemma mem_set_smul_of_mem_mem {r : S} {m : M} (mem1 : r ∈ s) (mem2 : m ∈ N) :
    r • m ∈ s • N

Proof state:
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N : Submodule R M
r : S
m : M
mem1 : r ∈ s
mem2 : m ∈ N
⊢ ∀ p ∈ {p | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p}, r • m ∈ p

Tactic:
exact fun _ h => h mem1 mem2

Result:
no goals

Proof state:
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N : Submodule R M
r : S
m : M
mem1 : r ∈ s
mem2 : m ∈ N
⊢ r • m ∈ s • N

Tactic:
rw [mem_set_smul_def, mem_sInf]

Result:
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N : Submodule R M
r : S
m : M
mem1 : r ∈ s
mem2 : m ∈ N
⊢ ∀ p ∈ {p | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p}, r • m ∈ p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem ne_empty_of_size_eq_add_one (h : l.size = n + 1) : l ≠ #[]

Proof state:
n : Nat
α✝ : Type u_1
l : Array α✝
h : l.size = n + 1
⊢ l ≠ #[]

Tactic:
cases l

Result:
case mk
n : Nat
α✝ : Type u_1
toList✝ : List α✝
h : { toList := toList✝ }.size = n + 1
⊢ { toList := toList✝ } ≠ #[]

Proof state:
case mk
n : Nat
α✝ : Type u_1
toList✝ : List α✝
h : { toList := toList✝ }.size = n + 1
⊢ { toList := toList✝ } ≠ #[]

Tactic:
simpa using List.ne_nil_of_length_eq_add_one h

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_comp_eq_of_range_subset {g : M → N} {f : α → M}
    (hg : ∀ {x}, x ∈ range f → (g x = 1 ↔ x = 1)) :
    mulSupport (g ∘ f) = mulSupport f :=
  Set.ext fun x ↦ not_congr <| by rw [Function.comp, hg (mem_range_self x)]

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : One M
inst✝ : One N
g : M → N
f : α → M
hg : ∀ {x : M}, x ∈ range f → (g x = 1 ↔ x = 1)
x : α
⊢ (g ∘ f) x = 1 ↔ f x = 1

Tactic:
rw [Function.comp, hg (mem_range_self x)]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem Filter.Tendsto.atBot_mul_neg {C : 𝕜} (hC : C < 0) (hf : Tendsto f l atBot)
    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => f x * g x) l atTop

Tactic:
have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_neg hC hg

Result:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x => (Neg.neg ∘ f) x * g x) l atBot
⊢ Tendsto (fun x => f x * g x) l atTop

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x => (Neg.neg ∘ f) x * g x) l atBot
⊢ Tendsto (fun x => f x * g x) l atTop

Tactic:
simpa [Function.comp_def] using tendsto_neg_atBot_atTop.comp this

Result:
no goals