harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem closure_reProdIm (s t : Set ℝ) : closure (s ×ℂ t) = closure s ×ℂ closure t

Proof state:
s t : Set ℝ
⊢ closure (s ×ℂ t) = closure s ×ℂ closure t

Tactic:
simpa only [← preimage_eq_preimage equivRealProdCLM.symm.toHomeomorph.surjective,
  equivRealProdCLM.symm.toHomeomorph.preimage_closure] using @closure_prod_eq _ _ _ _ s t

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem isSuccLimit_aleph0 : IsSuccLimit ℵ₀

Proof state:
⊢ ℵ₀ ≠ 0 ∧ IsSuccPrelimit ℵ₀

Tactic:
exact ⟨aleph0_ne_zero, isSuccPrelimit_aleph0⟩

Result:
no goals

Proof state:
⊢ IsSuccLimit ℵ₀

Tactic:
rw [Cardinal.isSuccLimit_iff]

Result:
⊢ ℵ₀ ≠ 0 ∧ IsSuccPrelimit ℵ₀
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem Metric.uniformity_edist : 𝓤 α = ⨅ ε > 0, 𝓟 { p : α × α | edist p.1 p.2 < ε }

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
simp only [PseudoMetricSpace.uniformity_dist, dist_nndist, edist_nndist,
  Metric.uniformity_edist_aux]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma hasHomology_of_isIsoLeftRightHomologyComparison [S.HasLeftHomology]
    [S.HasRightHomology] [h : IsIso S.leftRightHomologyComparison] :
    S.HasHomology

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasLeftHomology
inst✝ : S.HasRightHomology
h : IsIso S.leftRightHomologyComparison
⊢ S.HasHomology

Tactic:
haveI : IsIso (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData) := h

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasLeftHomology
inst✝ : S.HasRightHomology
h : IsIso S.leftRightHomologyComparison
this : IsIso (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData)
⊢ S.HasHomology

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasLeftHomology
inst✝ : S.HasRightHomology
h : IsIso S.leftRightHomologyComparison
this : IsIso (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData)
⊢ S.HasHomology

Tactic:
exact hasHomology_of_isIso_leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_eq_zero_iff_of_pos {x : ℝ≥0∞} {y : ℝ} (hy : 0 < y) : x ^ y = 0 ↔ x = 0

Proof state:
x : ℝ≥0∞
y : ℝ
hy : 0 < y
⊢ x ^ y = 0 ↔ x = 0

Tactic:
simp [hy, hy.not_lt]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma toOpen_eq (U) :
    (by exact StructureSheaf.toOpen R U) =
    (ΓSpecIso R).inv ≫ (Spec R).presheaf.map (homOfLE le_top).op := rfl

Proof state:
R : CommRingCat
U : ?m.151854
⊢ R ⟶ Γ(Spec R, ?m.152902)

Tactic:
exact StructureSheaf.toOpen R U

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_star_id : cfc (star · : R → R) a = star a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => star x) a = star a

Tactic:
rw [cfc_star .., cfc_id' ..]

Result:
no goals
-- Mathlib/Order/BooleanSubalgebra.lean
@[simp] lemma top_mem : ⊤ ∈ L

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ ⊤ ∈ L

Tactic:
simpa using compl_mem L.bot_mem

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma ofHom_v (φ : F ⟶ G) (p : ℤ) : (ofHom φ).v p p (add_zero p) = φ.f p

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
p : ℤ
⊢ (ofHom φ).v p p ⋯ = φ.f p

Tactic:
simp only [ofHom, ofHoms_v]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
lemma mk_lt_mk_of_comm {X A₁ A₂ : C} {i₁ : A₁ ⟶ X} {i₂ : A₂ ⟶ X} [Mono i₁] [Mono i₂]
    (f : A₁ ⟶ A₂) (fac : f ≫ i₂ = i₁) (hf : ¬ IsIso f) :
    Subobject.mk i₁ < Subobject.mk i₂

Proof state:
case inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ IsIso f

Tactic:
convert (isoOfMkEqMk i₁ i₂ h).isIso_hom

Result:
case h.e'_5
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ f = (isoOfMkEqMk i₁ i₂ h).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
⊢ mk i₁ < mk i₂

Tactic:
obtain _ | h := (mk_le_mk_of_comm _ fac).lt_or_eq

Result:
case inl
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h✝ : mk i₁ < mk i₂
⊢ mk i₁ < mk i₂

case inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ mk i₁ < mk i₂

Proof state:
case h.e'_5
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ f = (isoOfMkEqMk i₁ i₂ h).hom

Tactic:
rw [← cancel_mono i₂, isoOfMkEqMk_hom, ofMkLEMk_comp, fac]

Result:
no goals

Proof state:
case inl
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h✝ : mk i₁ < mk i₂
⊢ mk i₁ < mk i₂

Tactic:
assumption

Result:
no goals

Proof state:
case inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ False

Tactic:
apply hf

Result:
case inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ IsIso f

Proof state:
case inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ mk i₁ < mk i₂

Tactic:
exfalso

Result:
case inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.max_ult' (a : BitVec w) : (BitVec.ult (-1#w) a) = false

Proof state:
w : Nat
a : BitVec w
⊢ (-1#w).ult a = false

Tactic:
rw [BitVec.negOne_eq_allOnes, ← Bool.not_eq_true, ← @lt_ult]

Result:
w : Nat
a : BitVec w
⊢ ¬BitVec.allOnes w < a

Proof state:
w : Nat
a : BitVec w
⊢ ¬BitVec.allOnes w < a

Tactic:
exact BitVec.not_allOnes_lt

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval_geom_sum {R} [CommSemiring R] {n : ℕ} {x : R} :
    eval x (∑ i ∈ range n, X ^ i) = ∑ i ∈ range n, x ^ i

Proof state:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ eval x (∑ i ∈ range n, X ^ i) = ∑ i ∈ range n, x ^ i

Tactic:
simp [eval_finset_sum]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_of_perm [BEq α] [PartialEquivBEq α] [Inhabited α] {l l' : List ((a : α) × β a)}
    {a : α} (hl : DistinctKeys l) (h : Perm l l') :
    getKey! a l = getKey! a l'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : PartialEquivBEq α
inst✝ : Inhabited α
l l' : List ((a : α) × β a)
a : α
hl : DistinctKeys l
h : l.Perm l'
⊢ getKey! a l = getKey! a l'

Tactic:
simp only [getKey!_eq_getKey?, getKey?_of_perm hl h]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean
theorem exists_mul_lt_of_lt_opNorm (f : E →SL[σ₁₂] F) {r : ℝ} (hr₀ : 0 ≤ r) (hr : r < ‖f‖) :
    ∃ x, r * ‖x‖ < ‖f x‖

Proof state:
case intro
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : ↑r < ‖f‖
⊢ ∃ x, ↑r * ‖x‖ < ‖f x‖

Tactic:
exact f.exists_mul_lt_apply_of_lt_opNNNorm hr

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr₀ : 0 ≤ r
hr : r < ‖f‖
⊢ ∃ x, r * ‖x‖ < ‖f x‖

Tactic:
lift r to ℝ≥0 using hr₀

Result:
case intro
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : ↑r < ‖f‖
⊢ ∃ x, ↑r * ‖x‖ < ‖f x‖
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem mem_rightCoset_rightCoset {a : α} (ha : op a • (s : Set α) = s) : a ∈ s

Proof state:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : op a • ↑s = ↑s
⊢ a ∈ op a • ↑s

Tactic:
exact mem_own_rightCoset s a

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : op a • ↑s = ↑s
⊢ a ∈ s

Tactic:
rw [← SetLike.mem_coe, ← ha]

Result:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : op a • ↑s = ↑s
⊢ a ∈ op a • ↑s
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_const_smul_right {c : 𝕜} (hc : c ≠ 0) :
    (f =O[l] fun x => c • f' x) ↔ f =O[l] f'

Proof state:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x => ‖c • f' x‖) ↔ f =O[l] f'

Tactic:
simp only [norm_smul]

Result:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x => ‖c‖ * ‖f' x‖) ↔ f =O[l] f'

Proof state:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
⊢ (f =O[l] fun x => c • f' x) ↔ f =O[l] f'

Tactic:
have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc

Result:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x => c • f' x) ↔ f =O[l] f'

Proof state:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x => c • f' x) ↔ f =O[l] f'

Tactic:
rw [← isBigO_norm_right]

Result:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x => ‖c • f' x‖) ↔ f =O[l] f'

Proof state:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x => ‖c‖ * ‖f' x‖) ↔ f =O[l] f'

Tactic:
rw [isBigO_const_mul_right_iff cne0, isBigO_norm_right]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma sqrt_mul_self (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ sqrt (a * a) = a

Tactic:
rw [← nnrpow_two _, sqrt_nnrpow_two _]

Result:
no goals
-- Mathlib/Data/Matroid/Loop.lean
@[simp]
lemma restrict_isLoop_iff {R : Set α} : (M ↾ R).IsLoop e ↔ e ∈ R ∧ (M.IsLoop e ∨ e ∉ M.E)

Proof state:
α : Type u_1
M : Matroid α
e : α
R : Set α
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.loops ∨ e ∉ M.E)

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
e : α
R : Set α
⊢ (M ↾ R).IsLoop e ↔ e ∈ R ∧ (M.IsLoop e ∨ e ∉ M.E)

Tactic:
simp only [isLoop_iff, restrict_closure_eq', empty_inter, mem_union, mem_inter_iff, mem_diff]

Result:
α : Type u_1
M : Matroid α
e : α
R : Set α
⊢ e ∈ M.closure ∅ ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E ↔ e ∈ R ∧ (e ∈ M.loops ∨ e ∉ M.E)
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem mul_nonneg (a b : ℤ√d) : 0 ≤ a → 0 ≤ b → 0 ≤ a * b

Proof state:
d : ℕ
a b : ℤ√↑d
⊢ a.Nonneg → b.Nonneg → (a * b).Nonneg

Tactic:
exact nonneg_mul

Result:
no goals

Proof state:
d : ℕ
a b : ℤ√↑d
⊢ 0 ≤ a → 0 ≤ b → 0 ≤ a * b

Tactic:
simp_rw [← nonneg_iff_zero_le]

Result:
d : ℕ
a b : ℤ√↑d
⊢ a.Nonneg → b.Nonneg → (a * b).Nonneg
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem _root_.Multiset.aestronglyMeasurable_prod' (l : Multiset (α → M))
    (hl : ∀ f ∈ l, AEStronglyMeasurable f μ) : AEStronglyMeasurable l.prod μ

Proof state:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, AEStronglyMeasurable f μ
⊢ ∀ f ∈ l, AEStronglyMeasurable f μ

Tactic:
simpa using hl

Result:
no goals

Proof state:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l : Multiset (α → M)
hl : ∀ f ∈ l, AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable l.prod μ

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (Multiset.prod (Quot.mk (⇑(List.isSetoid (α → M))) l)) μ

Proof state:
case mk
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (Multiset.prod (Quot.mk (⇑(List.isSetoid (α → M))) l)) μ

Tactic:
simpa using l.aestronglyMeasurable_prod' (by simpa using hl)

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma Monic.mul
    (hD : D.Injective) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2)
    (hp : p.Monic D) (hq : q.Monic D) : (p * q).Monic D

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : Monic D q
⊢ leadingCoeff D p = 1

Tactic:
exact hp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : Monic D q
⊢ Monic D (p * q)

Tactic:
rw [Monic, hq.leadingCoeff_mul_eq_left hD hadd]

Result:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : Monic D q
⊢ leadingCoeff D p = 1
-- Mathlib/Topology/Algebra/Module/Alternating/Basic.lean
theorem alternatization_apply_toAlternatingMap :
    (alternatization f).toAlternatingMap = MultilinearMap.alternatization f.1

Proof state:
case H
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ContinuousMultilinearMap R (fun x => M) N
v : ι → M
⊢ (alternatization f).toAlternatingMap v = (MultilinearMap.alternatization f.toMultilinearMap) v

Tactic:
simp [alternatization_apply_apply, MultilinearMap.alternatization_apply, Function.comp_def]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ContinuousMultilinearMap R (fun x => M) N
⊢ (alternatization f).toAlternatingMap = MultilinearMap.alternatization f.toMultilinearMap

Tactic:
ext v

Result:
case H
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ContinuousMultilinearMap R (fun x => M) N
v : ι → M
⊢ (alternatization f).toAlternatingMap v = (MultilinearMap.alternatization f.toMultilinearMap) v
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem coe_stream'_rat_eq (v_eq_q : v = (↑q : K)) :
    ((IntFractPair.stream q).map (Option.map (mapFr (↑))) : Stream' <| Option <| IntFractPair K) =
      IntFractPair.stream v

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) = IntFractPair.stream v

Tactic:
funext n

Result:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) n = IntFractPair.stream v n

Proof state:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) n = IntFractPair.stream v n

Tactic:
exact IntFractPair.coe_stream_nth_rat_eq v_eq_q n

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) :
    MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f t x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
h : s =ᶠ[𝓝 x] t
⊢ (∃ f', HasMFDerivWithinAt I I' f s x f') ↔ ∃ f', HasMFDerivWithinAt I I' f t x f'

Tactic:
exact exists_congr fun _ => hasMFDerivWithinAt_congr_set h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
h : s =ᶠ[𝓝 x] t
⊢ MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f t x

Tactic:
simp only [mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
h : s =ᶠ[𝓝 x] t
⊢ (∃ f', HasMFDerivWithinAt I I' f s x f') ↔ ∃ f', HasMFDerivWithinAt I I' f t x f'
-- Mathlib/Topology/Order.lean
theorem isClosed_iSup_iff {s : Set α} : IsClosed[⨆ i, t i] s ↔ ∀ i, IsClosed[t i] s

Proof state:
α : Type u
ι : Sort v
t : ι → TopologicalSpace α
s : Set α
⊢ IsClosed s ↔ ∀ (i : ι), IsClosed s

Tactic:
simp only [← @isOpen_compl_iff _ _ (⨆ i, t i), ← @isOpen_compl_iff _ _ (t _), isOpen_iSup_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem toDual_apply (i j : ι) : b.toDual (b i) (b j) = if i = j then 1 else 0

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ (b.toDual (b i)) (b j) = if i = j then 1 else 0

Tactic:
erw [constr_basis b, constr_basis b]

Result:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ (if j = i then 1 else 0) = if i = j then 1 else 0

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ (if j = i then 1 else 0) = if i = j then 1 else 0

Tactic:
simp only [eq_comm]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_image_right (f : α → γ → δ) (g : β → γ) :
    image2 f s (g '' t) = image2 (fun a b => f a (g b)) s t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → γ → δ
g : β → γ
⊢ image2 f s (g '' t) = image2 (fun a b => f a (g b)) s t

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → γ → δ
g : β → γ
x✝ : δ
⊢ x✝ ∈ image2 f s (g '' t) ↔ x✝ ∈ image2 (fun a b => f a (g b)) s t

Proof state:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → γ → δ
g : β → γ
x✝ : δ
⊢ x✝ ∈ image2 f s (g '' t) ↔ x✝ ∈ image2 (fun a b => f a (g b)) s t

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.const_sub [AddCommGroup α] (h : Periodic f c) (a : α) :
    Periodic (fun x => f (a - x)) c := fun x => by
  simp only [← sub_sub, h.sub_eq]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommGroup α
h : Periodic f c
a x : α
⊢ (fun x => f (a - x)) (x + c) = (fun x => f (a - x)) x

Tactic:
simp only [← sub_sub, h.sub_eq]

Result:
no goals