harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem u_int_pos : 0 < ∫ x : E, u x ∂μ

Proof state:
case refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ 0 < μ (support u)

Tactic:
rw [u_support]

Result:
case refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ 0 < μ (ball 0 1)

Proof state:
case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ Integrable u μ

Tactic:
exact (u_continuous E).integrable_of_hasCompactSupport (u_compact_support E)

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ 0 < ∫ (x : E), u x ∂μ

Tactic:
refine (integral_pos_iff_support_of_nonneg u_nonneg ?_).mpr ?_

Result:
case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ Integrable u μ

case refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ 0 < μ (support u)

Proof state:
case refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ 0 < μ (ball 0 1)

Tactic:
exact measure_ball_pos _ _ zero_lt_one

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
theorem set_walk_length_zero_eq_of_ne {u v : V} (h : u ≠ v) :
    {p : G.Walk u v | p.length = 0} = ∅

Proof state:
case h
V : Type u
G : SimpleGraph V
u v : V
h : u ≠ v
p : G.Walk u v
⊢ p ∈ {p | p.length = 0} ↔ p ∈ ∅

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false]

Result:
case h
V : Type u
G : SimpleGraph V
u v : V
h : u ≠ v
p : G.Walk u v
⊢ ¬p.length = 0

Proof state:
V : Type u
G : SimpleGraph V
u v : V
h : u ≠ v
⊢ {p | p.length = 0} = ∅

Tactic:
ext p

Result:
case h
V : Type u
G : SimpleGraph V
u v : V
h : u ≠ v
p : G.Walk u v
⊢ p ∈ {p | p.length = 0} ↔ p ∈ ∅

Proof state:
case h
V : Type u
G : SimpleGraph V
u v : V
h : u ≠ v
p : G.Walk u v
⊢ ¬p.length = 0

Tactic:
exact fun h' => absurd (Walk.eq_of_length_eq_zero h') h

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem image_sphere (h : α ≃ᵢ β) (x : α) (r : ℝ) :
    h '' Metric.sphere x r = Metric.sphere (h x) r

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
⊢ ⇑h '' Metric.sphere x r = Metric.sphere (h x) r

Tactic:
rw [← h.preimage_symm, h.symm.preimage_sphere, symm_symm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.contains a = false → get? m a = none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
⊢ m.contains a = false → get? m a = none

Tactic:
simp_to_raw using Raw₀.Const.get?_eq_none

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Lemmas.lean
theorem minimalPeriod_prod_map (f : α → α) (g : β → β) (x : α × β) :
    minimalPeriod (Prod.map f g) x = (minimalPeriod f x.1).lcm (minimalPeriod g x.2) :=
  eq_of_forall_dvd <| by cases x; simp [← isPeriodicPt_iff_minimalPeriod_dvd, Nat.lcm_dvd_iff]

Proof state:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ ∀ (c : ℕ), minimalPeriod (Prod.map f g) x ∣ c ↔ (minimalPeriod f x.1).lcm (minimalPeriod g x.2) ∣ c

Tactic:
cases x

Result:
case mk
α : Type u_1
β : Type u_2
f : α → α
g : β → β
fst✝ : α
snd✝ : β
⊢ ∀ (c : ℕ),
    minimalPeriod (Prod.map f g) (fst✝, snd✝) ∣ c ↔
      (minimalPeriod f (fst✝, snd✝).1).lcm (minimalPeriod g (fst✝, snd✝).2) ∣ c

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → α
g : β → β
fst✝ : α
snd✝ : β
⊢ ∀ (c : ℕ),
    minimalPeriod (Prod.map f g) (fst✝, snd✝) ∣ c ↔
      (minimalPeriod f (fst✝, snd✝).1).lcm (minimalPeriod g (fst✝, snd✝).2) ∣ c

Tactic:
simp [← isPeriodicPt_iff_minimalPeriod_dvd, Nat.lcm_dvd_iff]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem functor_map_eq_inf {X : TopCat} (U V : Opens X) :
    U.isOpenEmbedding.isOpenMap.functor.obj ((Opens.map U.inclusion').obj V) = V ⊓ U

Proof state:
case h
X : TopCat
U V : Opens ↑X
⊢ ↑(⋯.functor.obj ((map U.inclusion').obj V)) = ↑(V ⊓ U)

Tactic:
simp only [IsOpenMap.coe_functor_obj, map_coe, coe_inf,
  Set.image_preimage_eq_inter_range, set_range_inclusion' U]

Result:
no goals

Proof state:
X : TopCat
U V : Opens ↑X
⊢ ⋯.functor.obj ((map U.inclusion').obj V) = V ⊓ U

Tactic:
ext1

Result:
case h
X : TopCat
U V : Opens ↑X
⊢ ↑(⋯.functor.obj ((map U.inclusion').obj V)) = ↑(V ⊓ U)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem countP_toList (p : α → Bool) (v : Vector α n) :
    v.toList.countP p = v.countP p

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.countP p { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    countP p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Bool
v : Vector α n
⊢ List.countP p v.toList = countP p v

Tactic:
cases v

Result:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.countP p { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    countP p { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/RingTheory/Artinian/Module.lean
lemma setOf_isPrime_finite : {I : Ideal R | I.IsPrime}.Finite

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
⊢ {I | I.IsPrime}.Finite

Tactic:
simpa only [isPrime_iff_isMaximal] using setOf_isMaximal_finite R

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem getElem_set_of_ne {l : List α} {i j : ℕ} (h : i ≠ j) (a : α)
    (hj : j < (l.set i a).length) :
    (l.set i a)[j] = l[j]'(by simpa using hj)

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ l : List α
i j : ℕ
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ j < l.length

Tactic:
simpa using hj

Result:
no goals

Proof state:
α : Type u
l : List α
i j : ℕ
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ (l.set i a)[j] = l[j]

Tactic:
rw [← Option.some_inj, ← List.getElem?_eq_getElem, List.getElem?_set_ne h,
  List.getElem?_eq_getElem]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem extend_eq {s : α} (h : P s) : extend m s = m s h

Proof state:
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : P s
⊢ extend m s = m s h

Tactic:
simp [extend, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem size_clearUnit (assignments : Array Assignment) (l : Literal (PosFin n)) :
    (clearUnit assignments l).size = assignments.size

Proof state:
n : Nat
assignments : Array Assignment
l : Literal (PosFin n)
⊢ (clearUnit assignments l).size = assignments.size

Tactic:
simp [clearUnit]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem mem_iInf {ι} (p : ι → LieSubmodule R L M) {x} : (x ∈ ⨅ i, p i) ↔ ∀ i, x ∈ p i

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
x : M
⊢ (∀ (i : ι), x ∈ ↑(p i)) ↔ ∀ (i : ι), x ∈ p i

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
x : M
⊢ x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i

Tactic:
rw [← SetLike.mem_coe, iInf_coe, Set.mem_iInter]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
x : M
⊢ (∀ (i : ι), x ∈ ↑(p i)) ↔ ∀ (i : ι), x ∈ p i
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
    ¬a ∈ m → m.getKey! a = default

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
a : α
⊢ ¬a ∈ m → m.getKey! a = default

Tactic:
simpa [mem_iff_contains] using getKey!_eq_default_of_contains_eq_false h

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.left_ne_right_of_ne_left {x y z : P} (h : Wbtw R x y z) (hne : y ≠ x) : x ≠ z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
hne : y ≠ x
⊢ x ≠ z

Tactic:
rintro rfl

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : y ≠ x
h : Wbtw R x y x
⊢ False

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : y ≠ x
h : Wbtw R x y x
⊢ False

Tactic:
rw [wbtw_self_iff] at h

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : y ≠ x
h : y = x
⊢ False

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : y ≠ x
h : y = x
⊢ False

Tactic:
exact hne h

Result:
no goals
-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem gluedCoverT'_fst_snd (x y z : 𝒰.J) :
    gluedCoverT' 𝒰 x y z ≫ pullback.fst _ _ ≫ pullback.snd _ _ =
      pullback.snd _ _ ≫ pullback.snd _ _

Proof state:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ ((pullbackRightPullbackFstIso (𝒰.map x) (𝒰.map z) (pullback.fst (𝒰.map x) (𝒰.map y))).hom ≫
        (pullback.map (pullback.fst (𝒰.map x) (𝒰.map y) ≫ 𝒰.map x) (𝒰.map z)
              (pullback.fst (𝒰.map y) (𝒰.map x) ≫ 𝒰.map y) (𝒰.map z) (pullbackSymmetry (𝒰.map x) (𝒰.map y)).hom
              (𝟙 (𝒰.obj z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.map y) (𝒰.map z) (pullback.fst (𝒰.map y) (𝒰.map x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.map y) (𝒰.map x)) (pullback.fst (𝒰.map y) (𝒰.map z))).hom) ≫
      pullback.fst (pullback.fst (𝒰.map y) (𝒰.map z)) (pullback.fst (𝒰.map y) (𝒰.map x)) ≫
        pullback.snd (𝒰.map y) (𝒰.map z) =
    pullback.snd (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) ≫
      pullback.snd (𝒰.map x) (𝒰.map z)

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ gluedCoverT' 𝒰 x y z ≫
      pullback.fst (pullback.fst (𝒰.map y) (𝒰.map z)) (pullback.fst (𝒰.map y) (𝒰.map x)) ≫
        pullback.snd (𝒰.map y) (𝒰.map z) =
    pullback.snd (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) ≫
      pullback.snd (𝒰.map x) (𝒰.map z)

Tactic:
delta gluedCoverT'

Result:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ ((pullbackRightPullbackFstIso (𝒰.map x) (𝒰.map z) (pullback.fst (𝒰.map x) (𝒰.map y))).hom ≫
        (pullback.map (pullback.fst (𝒰.map x) (𝒰.map y) ≫ 𝒰.map x) (𝒰.map z)
              (pullback.fst (𝒰.map y) (𝒰.map x) ≫ 𝒰.map y) (𝒰.map z) (pullbackSymmetry (𝒰.map x) (𝒰.map y)).hom
              (𝟙 (𝒰.obj z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.map y) (𝒰.map z) (pullback.fst (𝒰.map y) (𝒰.map x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.map y) (𝒰.map x)) (pullback.fst (𝒰.map y) (𝒰.map z))).hom) ≫
      pullback.fst (pullback.fst (𝒰.map y) (𝒰.map z)) (pullback.fst (𝒰.map y) (𝒰.map x)) ≫
        pullback.snd (𝒰.map y) (𝒰.map z) =
    pullback.snd (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) ≫
      pullback.snd (𝒰.map x) (𝒰.map z)
-- Mathlib/Order/KrullDimension.lean
lemma coheight_eq_krullDim_Ici {α : Type*} [Preorder α] (x : α) :
    (coheight x : ℕ∞) = krullDim (Set.Ici x)

Proof state:
α : Type u_3
inst✝ : Preorder α
x : α
⊢ ↑(coheight x) = krullDim ↑(Set.Ici x)

Tactic:
rw [coheight, ← krullDim_orderDual, Order.krullDim_eq_of_orderIso (OrderIso.refl _)]

Result:
α : Type u_3
inst✝ : Preorder α
x : α
⊢ ↑(height x) = krullDim (↑(Set.Ici x))ᵒᵈ

Proof state:
α : Type u_3
inst✝ : Preorder α
x : α
⊢ ↑(height x) = krullDim (↑(Set.Ici x))ᵒᵈ

Tactic:
exact height_eq_krullDim_Iic _

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_le_one_iff (f : R → R) (a : A)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.827386) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc f a ≤ 1 ↔ ∀ x ∈ spectrum R a, f x ≤ 1

Tactic:
simpa using cfc_le_algebraMap_iff f 1 a

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem idxOf_inj [DecidableEq α] {l : List α} {x y : α} (hx : x ∈ l) (hy : y ∈ l) :
    idxOf x l = idxOf y l ↔ x = y :=
  ⟨fun h => by
    have x_eq_y :
        get l ⟨idxOf x l, idxOf_lt_length_iff.2 hx⟩ =
        get l ⟨idxOf y l, idxOf_lt_length_iff.2 hy⟩

Proof state:
α : Type u
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : idxOf x l = idxOf y l
⊢ l.get ⟨idxOf x l, ⋯⟩ = l.get ⟨idxOf y l, ⋯⟩

Tactic:
simp only [h]

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : idxOf x l = idxOf y l
⊢ x = y

Tactic:
have x_eq_y :
    get l ⟨idxOf x l, idxOf_lt_length_iff.2 hx⟩ =
    get l ⟨idxOf y l, idxOf_lt_length_iff.2 hy⟩ := by
  simp only [h]

Result:
α : Type u
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : idxOf x l = idxOf y l
x_eq_y : l.get ⟨idxOf x l, ⋯⟩ = l.get ⟨idxOf y l, ⋯⟩
⊢ x = y

Proof state:
α : Type u
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : x = y
⊢ idxOf x l = idxOf y l

Tactic:
subst h

Result:
α : Type u
inst✝ : DecidableEq α
l : List α
x : α
hx hy : x ∈ l
⊢ idxOf x l = idxOf x l

Proof state:
α : Type u
inst✝ : DecidableEq α
l : List α
x : α
hx hy : x ∈ l
⊢ idxOf x l = idxOf x l

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : idxOf x l = idxOf y l
x_eq_y : x = y
⊢ x = y

Tactic:
exact x_eq_y

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : idxOf x l = idxOf y l
x_eq_y : l.get ⟨idxOf x l, ⋯⟩ = l.get ⟨idxOf y l, ⋯⟩
⊢ x = y

Tactic:
simp only [idxOf_get] at x_eq_y

Result:
α : Type u
inst✝ : DecidableEq α
l : List α
x y : α
hx : x ∈ l
hy : y ∈ l
h : idxOf x l = idxOf y l
x_eq_y : x = y
⊢ x = y
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mdifferentiableOn_prod_module_iff (f : M → F₁ × F₂) :
    MDifferentiableOn I 𝓘(𝕜, F₁ × F₂) f s ↔
      MDifferentiableOn I 𝓘(𝕜, F₁) (Prod.fst ∘ f) s
      ∧ MDifferentiableOn I 𝓘(𝕜, F₂) (Prod.snd ∘ f) s

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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
f : M → F₁ × F₂
⊢ MDifferentiableOn I 𝓘(𝕜, F₁ × F₂) f s ↔
    MDifferentiableOn I 𝓘(𝕜, F₁) (Prod.fst ∘ f) s ∧ MDifferentiableOn I 𝓘(𝕜, F₂) (Prod.snd ∘ f) s

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
f : M → F₁ × F₂
⊢ MDifferentiableOn I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) f s ↔
    MDifferentiableOn I 𝓘(𝕜, F₁) (Prod.fst ∘ f) s ∧ MDifferentiableOn I 𝓘(𝕜, F₂) (Prod.snd ∘ f) s

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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
f : M → F₁ × F₂
⊢ MDifferentiableOn I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) f s ↔
    MDifferentiableOn I 𝓘(𝕜, F₁) (Prod.fst ∘ f) s ∧ MDifferentiableOn I 𝓘(𝕜, F₂) (Prod.snd ∘ f) s

Tactic:
exact mdifferentiableOn_prod_iff f

Result:
no goals
-- Mathlib/CategoryTheory/Sites/SheafOfTypes.lean
theorem isSheaf_bot : IsSheaf (⊥ : GrothendieckTopology C) P := fun X => by
  simp [isSheafFor_top_sieve]

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X : C
⊢ ∀ S ∈ ⊥ X, IsSheafFor P S.arrows

Tactic:
simp [isSheafFor_top_sieve]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem prodMonoidal_rightUnitor_inv_fst (X : C₁ × C₂) :
    ((ρ_ X).inv : X ⟶ X ⊗ 𝟙_ _).1 = (ρ_ X.1).inv

Proof state:
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (ρ_ X).inv.1 = (ρ_ X.1).inv

Tactic:
cases X

Result:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (ρ_ (fst✝, snd✝)).inv.1 = (ρ_ (fst✝, snd✝).1).inv

Proof state:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (ρ_ (fst✝, snd✝)).inv.1 = (ρ_ (fst✝, snd✝).1).inv

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
lemma isEllSequence_id : IsEllSequence id :=
  fun _ _ _ => by simp only [id_eq]; ring1

Proof state:
x✝² x✝¹ x✝ : ℤ
⊢ (x✝² + x✝¹) * (x✝² - x✝¹) * x✝ ^ 2 = (x✝² + x✝) * (x✝² - x✝) * x✝¹ ^ 2 - (x✝¹ + x✝) * (x✝¹ - x✝) * x✝² ^ 2

Tactic:
ring1

Result:
no goals

Proof state:
x✝² x✝¹ x✝ : ℤ
⊢ id (x✝² + x✝¹) * id (x✝² - x✝¹) * id x✝ ^ 2 =
    id (x✝² + x✝) * id (x✝² - x✝) * id x✝¹ ^ 2 - id (x✝¹ + x✝) * id (x✝¹ - x✝) * id x✝² ^ 2

Tactic:
simp only [id_eq]

Result:
x✝² x✝¹ x✝ : ℤ
⊢ (x✝² + x✝¹) * (x✝² - x✝¹) * x✝ ^ 2 = (x✝² + x✝) * (x✝² - x✝) * x✝¹ ^ 2 - (x✝¹ + x✝) * (x✝¹ - x✝) * x✝² ^ 2
-- Mathlib/Data/Finset/Prod.lean
theorem product_biUnion [DecidableEq γ] (s : Finset α) (t : Finset β) (f : α × β → Finset γ) :
    (s ×ˢ t).biUnion f = s.biUnion fun a => t.biUnion fun b => f (a, b)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
s : Finset α
t : Finset β
f : α × β → Finset γ
⊢ (s ×ˢ t).biUnion f = s.biUnion fun a => t.biUnion fun b => f (a, b)

Tactic:
classical simp_rw [product_eq_biUnion, biUnion_biUnion, image_biUnion]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
s : Finset α
t : Finset β
f : α × β → Finset γ
⊢ (s ×ˢ t).biUnion f = s.biUnion fun a => t.biUnion fun b => f (a, b)

Tactic:
simp_rw [product_eq_biUnion, biUnion_biUnion, image_biUnion]

Result:
no goals
-- Mathlib/Algebra/QuadraticDiscriminant.lean
theorem quadratic_eq_zero_iff (ha : a ≠ 0) {s : K} (h : discrim a b c = s * s) (x : K) :
    a * (x * x) + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)

Tactic:
field_simp

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -b + -(2 * a * x) ↔ x * (2 * a) = -b + s ∨ x * (2 * a) = -b - s

Proof state:
case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = -b + -(2 * a * x) ↔ x * (2 * a) = -b - s

Tactic:
constructor <;> intro h' <;> linear_combination h'

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -b + -(2 * a * x) ↔ x * (2 * a) = -b + s ∨ x * (2 * a) = -b - s

Tactic:
apply or_congr

Result:
case h₁
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ↔ x * (2 * a) = -b + s

case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = -b + -(2 * a * x) ↔ x * (2 * a) = -b - s

Proof state:
case h₁
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ↔ x * (2 * a) = -b + s

Tactic:
constructor <;> intro h' <;> linear_combination -h'

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ a * (x * x) + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)

Tactic:
rw [quadratic_eq_zero_iff_discrim_eq_sq ha, h, sq, mul_self_eq_mul_self_iff]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_compl_of_infinite {α : Type*} [Infinite α] (s : Set α) (h2 : #s < #α) :
    #(sᶜ : Set α) = #α

Proof state:
α : Type u_1
inst✝ : Infinite α
s : Set α
h2 : #↑s < #α
⊢ #↑s + #↑sᶜ = #α

Tactic:
exact mk_sum_compl s

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Infinite α
s : Set α
h2 : #↑s < #α
⊢ #↑sᶜ = #α

Tactic:
refine eq_of_add_eq_of_aleph0_le ?_ h2 (aleph0_le_mk α)

Result:
α : Type u_1
inst✝ : Infinite α
s : Set α
h2 : #↑s < #α
⊢ #↑s + #↑sᶜ = #α
-- Mathlib/Data/Stream/Init.lean
lemma map_take (f : α → β) : (a.take n).map f = (a.map f).take n

Proof state:
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ List.map f (take n a) = take n (map f a)

Tactic:
apply List.ext_getElem <;> simp

Result:
no goals