harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Sieves.lean
lemma pullback_ofObjects_eq_top
    {I : Type*} (Y : I → C) {X : C} {i : I} (g : X ⟶ Y i) :
    ofObjects Y X = ⊤

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
Z : C
h : Z ⟶ X
⊢ ∃ i, Nonempty (Z ⟶ Y i)

Tactic:
exact ⟨i, ⟨h ≫ g⟩⟩

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
Z : C
h : Z ⟶ X
⊢ (ofObjects Y X).arrows h ↔ ⊤.arrows h

Tactic:
simp only [top_apply, iff_true]

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
Z : C
h : Z ⟶ X
⊢ (ofObjects Y X).arrows h

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
⊢ ofObjects Y X = ⊤

Tactic:
ext Z h

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
Z : C
h : Z ⟶ X
⊢ (ofObjects Y X).arrows h ↔ ⊤.arrows h

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
Z : C
h : Z ⟶ X
⊢ (ofObjects Y X).arrows h

Tactic:
rw [mem_ofObjects_iff ]

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
Z : C
h : Z ⟶ X
⊢ ∃ i, Nonempty (Z ⟶ Y i)
-- Mathlib/Tactic/Ring/Basic.lean
theorem of_eq {α} {a b c : α} (_ : (a : α) = c) (_ : b = c) : a = b

Proof state:
α : Sort u_2
a b c : α
x✝¹ : a = c
x✝ : b = c
⊢ a = b

Tactic:
subst_vars

Result:
α : Sort u_2
c : α
⊢ c = c

Proof state:
α : Sort u_2
c : α
⊢ c = c

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem HasFTaylorSeriesUpTo.zero_eq' (h : HasFTaylorSeriesUpTo n f p) (x : E) :
    p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
x : E
⊢ p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (p x 0).curry0

Tactic:
exact (p x 0).uncurry0_curry0.symm

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
x : E
⊢ p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)

Tactic:
rw [← h.zero_eq x]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
x : E
⊢ p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (p x 0).curry0
-- Mathlib/Data/Set/Image.lean
theorem forall_set_subtype {t : Set α} (p : Set α → Prop) :
    (∀ s : Set t, p (((↑) : t → α) '' s)) ↔ ∀ s : Set α, s ⊆ t → p s

Proof state:
α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∀ (s : Set ↑t), p (val '' s)) ↔ ∀ s ⊆ t, p s

Tactic:
rw [← forall_subset_range_iff, range_coe]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
lemma Union_closure_singleton_eq_iff {s : Set X} :
    (⋃ x ∈ s, closure {x}) = s ↔ StableUnderSpecialization s :=
  show _ ↔ IsLowerSet s by simp only [closure_singleton_eq_Iic, ← lowerClosure_eq, coe_lowerClosure]

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ ⋃ x ∈ s, closure {x} = s ↔ IsLowerSet s

Tactic:
simp only [closure_singleton_eq_Iic, ← lowerClosure_eq, coe_lowerClosure]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem memLp_finset_sum' {ι} (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, MemLp (f i) p μ) :
    MemLp (∑ i ∈ s, f i) p μ

Proof state:
case h.e'_6.h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
x : α
⊢ (∑ i ∈ s, f i) x = ∑ i ∈ s, f i x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
⊢ MemLp (∑ i ∈ s, f i) p μ

Tactic:
convert memLp_finset_sum s hf using 1

Result:
case h.e'_6
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
⊢ ∑ i ∈ s, f i = fun a => ∑ i ∈ s, f i a

Proof state:
case h.e'_6
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
⊢ ∑ i ∈ s, f i = fun a => ∑ i ∈ s, f i a

Tactic:
ext x

Result:
case h.e'_6.h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
x : α
⊢ (∑ i ∈ s, f i) x = ∑ i ∈ s, f i x
-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem mem_supported' {s : Set α} (p : α →₀ M) :
    p ∈ supported M R s ↔ ∀ x ∉ s, p x = 0

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set α
p : α →₀ M
this : DecidablePred fun x => x ∈ s
⊢ p ∈ supported M R s ↔ ∀ x ∉ s, p x = 0

Tactic:
simp [mem_supported, Set.subset_def, not_imp_comm]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set α
p : α →₀ M
⊢ p ∈ supported M R s ↔ ∀ x ∉ s, p x = 0

Tactic:
haveI := Classical.decPred fun x : α => x ∈ s

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set α
p : α →₀ M
this : DecidablePred fun x => x ∈ s
⊢ p ∈ supported M R s ↔ ∀ x ∉ s, p x = 0
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem hom_ext {P Q : Karoubi C} (f g : P ⟶ Q) (h : f.f = g.f) : f = g

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
h : f.f = g.f
⊢ f = g

Tactic:
simpa [hom_ext_iff] using h

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
theorem a_one_pow_n : (a 1 : QuaternionGroup n) ^ (2 * n) = 1

Proof state:
n : ℕ
⊢ a 1 ^ (2 * n) = 1

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem iInf_apply {ι} [Nonempty ι] (m : ι → OuterMeasure α) (s : Set α) :
    (⨅ i, m i) s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, ⨅ i, m i (t n)

Proof state:
α : Type u_1
ι : Sort u_2
inst✝ : Nonempty ι
m : ι → OuterMeasure α
s : Set α
⊢ (⨅ i, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)

Tactic:
rw [iInf, sInf_apply (range_nonempty m)]

Result:
α : Type u_1
ι : Sort u_2
inst✝ : Nonempty ι
m : ι → OuterMeasure α
s : Set α
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ range m, μ (t n) =
    ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)

Proof state:
α : Type u_1
ι : Sort u_2
inst✝ : Nonempty ι
m : ι → OuterMeasure α
s : Set α
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ range m, μ (t n) =
    ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)

Tactic:
simp only [iInf_range]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem hom_bind₁ (f : MvPolynomial τ R →+* S) (g : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
    f (bind₁ g φ) = eval₂Hom (f.comp C) (fun i => f (g i)) φ

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : MvPolynomial τ R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ f ((bind₁ g) φ) = (eval₂Hom (f.comp C) fun i => f (g i)) φ

Tactic:
rw [bind₁, map_aeval, algebraMap_eq]

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma mem_stabilizer_set {s : Set α} : a ∈ stabilizer G s ↔ ∀ b, a • b ∈ s ↔ b ∈ s

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
⊢ a ∈ stabilizer G s ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s

Tactic:
refine mem_stabilizer_iff.trans ⟨fun h b ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : a • s = s
b : α
⊢ a • b ∈ s ↔ b ∈ s

case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ a • s = s

Proof state:
case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ a • s = s

Tactic:
simp_rw [Set.ext_iff, mem_smul_set_iff_inv_smul_mem]

Result:
case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ ∀ (x : α), a⁻¹ • x ∈ s ↔ x ∈ s

Proof state:
case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ ∀ (x : α), a⁻¹ • x ∈ s ↔ x ∈ s

Tactic:
exact ((MulAction.toPerm a).forall_congr' <| by simp [Iff.comm]).1 h

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ ∀ (b : α), (a • (Equiv.symm (toPerm a)) b ∈ s ↔ (Equiv.symm (toPerm a)) b ∈ s) ↔ (a⁻¹ • b ∈ s ↔ b ∈ s)

Tactic:
simp [Iff.comm]

Result:
no goals

Proof state:
case refine_1
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : a • s = s
b : α
⊢ a • b ∈ s ↔ b ∈ s

Tactic:
rw [← (smul_mem_smul_set_iff : a • b ∈ _ ↔ _), h]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem IsLUB.mul_right {s : Set α} (ha : 0 ≤ a) (hs : IsLUB s b) :
    IsLUB ((fun b => b * a) '' s) (b * a)

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
s : Set α
ha : 0 ≤ a
hs : IsLUB s b
⊢ IsLUB ((fun b => b * a) '' s) (b * a)

Tactic:
simpa [mul_comm] using hs.mul_left ha

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem opNorm_zero : ‖(0 : ContinuousMultilinearMap 𝕜 E G)‖ = 0 :=
  (opNorm_nonneg _).antisymm' <| opNorm_le_bound le_rfl fun m => by simp

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
m : (i : ι) → E i
⊢ ‖0 m‖ ≤ 0 * ∏ i : ι, ‖m i‖

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMax.fderiv_eq_zero (h : IsLocalMax f a) : fderiv ℝ f a = 0

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
h : IsLocalMax f a
⊢ fderiv ℝ f a = 0

Tactic:
exact if hf : DifferentiableAt ℝ f a then h.hasFDerivAt_eq_zero hf.hasFDerivAt
else fderiv_zero_of_not_differentiableAt hf

Result:
no goals

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
h : IsLocalMax f a
⊢ fderiv ℝ f a = 0

Tactic:
classical
exact if hf : DifferentiableAt ℝ f a then h.hasFDerivAt_eq_zero hf.hasFDerivAt
else fderiv_zero_of_not_differentiableAt hf

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem normalizedFactors_eq_of_dvd (a : α) :
    ∀ᵉ (p ∈ normalizedFactors a) (q ∈ normalizedFactors a), p ∣ q → p = q

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ p = q

Tactic:
convert normalize_eq_normalize hdvd
        ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
          (prime_of_normalized_factor _ hq).irreducible hdvd) <;>
  apply (normalize_normalized_factor _ ‹_›).symm

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ p ∈ normalizedFactors a, ∀ q ∈ normalizedFactors a, p ∣ q → p = q

Tactic:
intro p hp q hq hdvd

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ p = q
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatMap_eq_empty_iff {l : Array α} {f : α → Array β} : l.flatMap f = #[] ↔ ∀ x ∈ l, f x = #[]

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → Array β
⊢ flatMap f l = #[] ↔ ∀ (x : α), x ∈ l → f x = #[]

Tactic:
rw [flatMap_def, flatten_eq_empty_iff]

Result:
α : Type u_1
β : Type u_2
l : Array α
f : α → Array β
⊢ (∀ (l_1 : Array β), l_1 ∈ map f l → l_1 = #[]) ↔ ∀ (x : α), x ∈ l → f x = #[]

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → Array β
⊢ (∀ (l_1 : Array β), l_1 ∈ map f l → l_1 = #[]) ↔ ∀ (x : α), x ∈ l → f x = #[]

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isOpen_sigma_iff {s : Set (Sigma σ)} : IsOpen s ↔ ∀ i, IsOpen (Sigma.mk i ⁻¹' s)

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set (Sigma σ)
⊢ (∀ (i : ι), IsOpen s) ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set (Sigma σ)
⊢ IsOpen s ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)

Tactic:
rw [isOpen_iSup_iff]

Result:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set (Sigma σ)
⊢ (∀ (i : ι), IsOpen s) ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem productMap_right_apply (b : B) :
    productMap f g (1 ⊗ₜ b) = g b

Proof state:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
b : B
⊢ (productMap f g) (1 ⊗ₜ[R] b) = g b

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Inverse.lean
theorem HasDerivAt.eventually_ne (h : HasDerivAt f f' x) (hf' : f' ≠ 0) :
    ∀ᶠ z in 𝓝[≠] x, f z ≠ f x :=
  (hasDerivAt_iff_hasFDerivAt.1 h).eventually_ne
    ⟨‖f'‖⁻¹, fun z => by field_simp [norm_smul, mt norm_eq_zero.1 hf']⟩

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
h : HasDerivAt f f' x
hf' : f' ≠ 0
z : 𝕜
⊢ ‖z‖ ≤ ‖f'‖⁻¹ * ‖(ContinuousLinearMap.smulRight 1 f') z‖

Tactic:
field_simp [norm_smul, mt norm_eq_zero.1 hf']

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/BigOperators.lean
theorem list_prod_mem {l : List M} (hl : ∀ x ∈ l, x ∈ S) : l.prod ∈ S

Proof state:
case intro
M : Type u_1
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List ↥S
⊢ ↑l.prod ∈ S

Tactic:
exact l.prod.coe_prop

Result:
no goals

Proof state:
M : Type u_1
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List M
hl : ∀ x ∈ l, x ∈ S
⊢ l.prod ∈ S

Tactic:
lift l to List S using hl

Result:
case intro
M : Type u_1
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List ↥S
⊢ (List.map Subtype.val l).prod ∈ S

Proof state:
case intro
M : Type u_1
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List ↥S
⊢ (List.map Subtype.val l).prod ∈ S

Tactic:
rw [← coe_list_prod]

Result:
case intro
M : Type u_1
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List ↥S
⊢ ↑l.prod ∈ S
-- Mathlib/Order/Filter/AtTopBot/Field.lean
/-- If `r` is a positive constant, `x ↦ f x / r` tends to infinity along a filter
if and only if `f` tends to infinity along the same filter. -/
lemma tendsto_div_const_atTop_of_pos (hr : 0 < r) :
    Tendsto (fun x ↦ f x / r) l atTop ↔ Tendsto f l atTop

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x => f x / r) l atTop ↔ Tendsto f l atTop

Tactic:
simpa only [div_eq_mul_inv] using tendsto_mul_const_atTop_of_pos (inv_pos.2 hr)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₄_of_isCharTwoJEqZeroNF : W.b₄ = 2 * W.a₄

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 2 * W.a₄ + 0 * W.a₃ = 2 * W.a₄

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.b₄ = 2 * W.a₄

Tactic:
rw [b₄, a₁_of_isCharTwoJEqZeroNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 2 * W.a₄ + 0 * W.a₃ = 2 * W.a₄
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@[simp]
lemma fromRows_fromCols_eq_fromBlocks (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R)
    (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
    fromRows (fromCols B₁₁ B₁₂) (fromCols B₂₁ B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

Tactic:
ext (_ | _) (_ | _) <;> simp

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem const_lt_const : const β a < const β b ↔ a < b

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a < const β b ↔ a < b

Tactic:
simpa [Pi.lt_def] using le_of_lt

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma map₂_fst {Y : C} (f : X ⟶ Y) (p : YonedaCollection F Y) :
    (YonedaCollection.map₂ F f p).fst = yoneda.map f ≫ p.fst

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (map₂ F f p).fst = yoneda.map f ≫ p.fst

Tactic:
simp [map₂]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem isIntegralClosure_adjoin_singleton_of_prime [hcycl : IsCyclotomicExtension {p} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑p) : IsIntegralClosure (adjoin ℤ ({ζ} : Set K)) ℤ K

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ 1} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ 1)
⊢ IsIntegralClosure ↥(adjoin ℤ {ζ}) ℤ K

Tactic:
exact isIntegralClosure_adjoin_singleton_of_prime_pow hζ

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsIntegralClosure ↥(adjoin ℤ {ζ}) ℤ K

Tactic:
rw [← pow_one p] at hζ hcycl

Result:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ 1} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ 1)
⊢ IsIntegralClosure ↥(adjoin ℤ {ζ}) ℤ K
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_ne_nil_iff {l : List α} :
    List.mapIdx f l ≠ [] ↔ l ≠ []

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
⊢ mapIdx f l ≠ [] ↔ l ≠ []

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem toNNReal_mul_nnnorm {x : ℝ} (y : ℝ) (hx : 0 ≤ x) : x.toNNReal * ‖y‖₊ = ‖x * y‖₊

Proof state:
x y : ℝ
hx : 0 ≤ x
⊢ x.toNNReal * ‖y‖₊ = ‖x * y‖₊

Tactic:
ext

Result:
case a
x y : ℝ
hx : 0 ≤ x
⊢ ↑(x.toNNReal * ‖y‖₊) = ↑‖x * y‖₊

Proof state:
case a
x y : ℝ
hx : 0 ≤ x
⊢ ↑(x.toNNReal * ‖y‖₊) = ↑‖x * y‖₊

Tactic:
simp only [NNReal.coe_mul, nnnorm_mul, coe_nnnorm, Real.toNNReal_of_nonneg, norm_of_nonneg, hx,
  NNReal.coe_mk]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValNat_dvd_iff_le [hp : Fact p.Prime] {a n : ℕ} (ha : a ≠ 0) :
    p ^ n ∣ a ↔ n ≤ padicValNat p a

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a n : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ n ≤ padicValNat p a

Tactic:
rw [pow_dvd_iff_le_emultiplicity, ← padicValNat_eq_emultiplicity (Nat.pos_of_ne_zero ha),
  Nat.cast_le]

Result:
no goals
-- Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
theorem IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential [Nontrivial S] (n : ℕ)
    [IsStandardSmoothOfRelativeDimension n R S] :
    Module.rank S (Ω[S⁄R]) = n

Proof state:
case mk.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial S
n : ℕ
inst✝ : IsStandardSmoothOfRelativeDimension n R S
P : SubmersivePresentation R S
hP : P.dimension = n
⊢ Module.rank S (Ω[S⁄R]) = ↑n

Tactic:
rw [P.rank_kaehlerDifferential, hP]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial S
n : ℕ
inst✝ : IsStandardSmoothOfRelativeDimension n R S
⊢ Module.rank S (Ω[S⁄R]) = ↑n

Tactic:
obtain ⟨⟨P, hP⟩⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›

Result:
case mk.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial S
n : ℕ
inst✝ : IsStandardSmoothOfRelativeDimension n R S
P : SubmersivePresentation R S
hP : P.dimension = n
⊢ Module.rank S (Ω[S⁄R]) = ↑n
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMinOn.hasFDerivWithinAt_eq_zero (h : IsLocalMinOn f s a)
    (hf : HasFDerivWithinAt f f' s a) (hy : y ∈ posTangentConeAt s a)
    (hy' : -y ∈ posTangentConeAt s a) : f' y = 0

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ f' y = 0

Tactic:
simpa using h.neg.hasFDerivWithinAt_eq_zero hf.neg hy hy'

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_restrict_iff_subtype {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α}
    (hs : MeasurableSet s) {p : α → Prop} :
    (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ (x : s) ∂comap ((↑) : s → α) μ, p x

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : ↑s) ∂Measure.comap Subtype.val μ, p ↑x

Tactic:
rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).ae_map_iff]

Result:
no goals
-- Mathlib/Probability/CondVar.lean
lemma condVar_bot [IsProbabilityMeasure μ] (hX : AEMeasurable X μ) :
    Var[X; μ | ⊥] = fun _ω ↦ Var[X; μ]

Proof state:
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : AEMeasurable X μ
⊢ Var[X; μ | ⊥] = fun _ω => Var[X; μ]

Tactic:
simp [condVar_bot', average_eq_integral, variance_eq_integral hX]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem univ_prod_univ : @univ α ×ˢ @univ β = univ

Proof state:
α : Type u_1
β : Type u_2
⊢ univ ×ˢ univ = univ

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
x✝ : α × β
⊢ x✝ ∈ univ ×ˢ univ ↔ x✝ ∈ univ

Proof state:
case h
α : Type u_1
β : Type u_2
x✝ : α × β
⊢ x✝ ∈ univ ×ˢ univ ↔ x✝ ∈ univ

Tactic:
exact iff_of_eq (true_and _)

Result:
no goals