harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Comma/Basic.lean
theorem eqToHom_left (X Y : Comma L R) (H : X = Y) :
    CommaMorphism.left (eqToHom H) = eqToHom (by cases H; rfl)

Proof state:
case refl
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ X.left = X.left

Tactic:
rfl

Result:
no goals

Proof state:
case refl
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ (eqToHom ⋯).left = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ X.left = Y.left

Tactic:
cases H

Result:
case refl
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ X.left = X.left

Proof state:
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ (eqToHom H).left = eqToHom ⋯

Tactic:
cases H

Result:
case refl
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ (eqToHom ⋯).left = eqToHom ⋯
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sup_sum {α : Type u} {β : Type v} (f : α ⊕ β → Ordinal) :
    sup.{max u v, w} f =
      max (sup.{u, max v w} fun a => f (Sum.inl a)) (sup.{v, max u w} fun b => f (Sum.inr b))

Proof state:
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
⊢ (sup fun b => f (Sum.inr b)) ≤ sup f

Tactic:
apply sup_le_of_range_subset.{_, max u v, w}

Result:
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
⊢ (range fun b => f (Sum.inr b)) ⊆ range f

Proof state:
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
⊢ (sup fun a => f (Sum.inl a)) ≤ sup f

α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
⊢ (sup fun b => f (Sum.inr b)) ≤ sup f

Tactic:
all_goals
  apply sup_le_of_range_subset.{_, max u v, w}
  rintro i ⟨a, rfl⟩
  apply mem_range_self

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
⊢ sup f = (sup fun a => f (Sum.inl a)) ⊔ sup fun b => f (Sum.inr b)

Tactic:
apply (sup_le_iff.2 _).antisymm (max_le_iff.2 ⟨_, _⟩)

Result:
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
⊢ ∀ (i : α ⊕ β), f i ≤ (sup fun a => f (Sum.inl a)) ⊔ sup fun b => f (Sum.inr b)

α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
⊢ (sup fun a => f (Sum.inl a)) ≤ sup f

α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
⊢ (sup fun b => f (Sum.inr b)) ≤ sup f

Proof state:
case inr
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
i : β
⊢ f (Sum.inr i) ≤ (sup fun a => f (Sum.inl a)) ⊔ sup fun b => f (Sum.inr b)

Tactic:
exact le_max_of_le_right (le_sup _ i)

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
⊢ ∀ (i : α ⊕ β), f i ≤ (sup fun a => f (Sum.inl a)) ⊔ sup fun b => f (Sum.inr b)

Tactic:
rintro (i | i)

Result:
case inl
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
i : α
⊢ f (Sum.inl i) ≤ (sup fun a => f (Sum.inl a)) ⊔ sup fun b => f (Sum.inr b)

case inr
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
i : β
⊢ f (Sum.inr i) ≤ (sup fun a => f (Sum.inl a)) ⊔ sup fun b => f (Sum.inr b)

Proof state:
case inl
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
i : α
⊢ f (Sum.inl i) ≤ (sup fun a => f (Sum.inl a)) ⊔ sup fun b => f (Sum.inr b)

Tactic:
exact le_max_of_le_left (le_sup _ i)

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
⊢ (range fun b => f (Sum.inr b)) ⊆ range f

Tactic:
rintro i ⟨a, rfl⟩

Result:
case intro
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
a : β
⊢ (fun b => f (Sum.inr b)) a ∈ range f

Proof state:
case intro
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
a : β
⊢ (fun b => f (Sum.inr b)) a ∈ range f

Tactic:
apply mem_range_self

Result:
no goals
-- Mathlib/CategoryTheory/Quotient.lean
theorem comp_right {a b c : C} (g : b ⟶ c) :
    ∀ (f₁ f₂ : a ⟶ b) (_ : CompClosure r f₁ f₂), CompClosure r (f₁ ≫ g) (f₂ ≫ g)
  | _, _, ⟨x, m₁, m₂, y, h⟩ => by simpa using CompClosure.intro x m₁ m₂ (y ≫ g) h

Proof state:
C : Type u_2
inst✝ : Category.{u_1, u_2} C
r : HomRel C
a b c : C
g : b ⟶ c
a✝ b✝ : C
x : a ⟶ a✝
m₁ m₂ : a✝ ⟶ b✝
y : b✝ ⟶ b
h : r m₁ m₂
⊢ CompClosure r ((x ≫ m₁ ≫ y) ≫ g) ((x ≫ m₂ ≫ y) ≫ g)

Tactic:
simpa using CompClosure.intro x m₁ m₂ (y ≫ g) h

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Cartesian.lean
theorem initial_mono {I : C} (B : C) (t : IsInitial I) [CartesianClosed C] : Mono (t.to B) :=
  ⟨fun g h _ => by
    haveI := strict_initial t g
    haveI := strict_initial t h
    exact eq_of_inv_eq_inv (t.hom_ext _ _)⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ t.to B = h ≫ t.to B
this : IsIso g
⊢ g = h

Tactic:
haveI := strict_initial t h

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ t.to B = h ≫ t.to B
this✝ : IsIso g
this : IsIso h
⊢ g = h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ t.to B = h ≫ t.to B
⊢ g = h

Tactic:
haveI := strict_initial t g

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ t.to B = h ≫ t.to B
this : IsIso g
⊢ g = h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ t.to B = h ≫ t.to B
this✝ : IsIso g
this : IsIso h
⊢ g = h

Tactic:
exact eq_of_inv_eq_inv (t.hom_ext _ _)

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_mul_eq_mul_denom_iff {x : RatFunc K} {p q : K[X]} (hq : q ≠ 0) :
    x.num * q = p * x.denom ↔ x = algebraMap _ _ p / algebraMap _ _ q

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) x.denom ≠ 0

Tactic:
exact algebraMap_ne_zero (denom_ne_zero x)

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) (x.num * q) = (algebraMap K[X] (RatFunc K)) (p * x.denom) ↔
    (algebraMap K[X] (RatFunc K)) x.num / (algebraMap K[X] (RatFunc K)) x.denom * (algebraMap K[X] (RatFunc K)) q =
      (algebraMap K[X] (RatFunc K)) p

Tactic:
rw [RingHom.map_mul, RingHom.map_mul, div_eq_mul_inv, mul_assoc, mul_comm (Inv.inv _), ←
  mul_assoc, ← div_eq_mul_inv, div_eq_iff]

Result:
K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) x.denom ≠ 0

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) (x.num * q) = (algebraMap K[X] (RatFunc K)) (p * x.denom) ↔
    x * (algebraMap K[X] (RatFunc K)) q = (algebraMap K[X] (RatFunc K)) p

Tactic:
conv_rhs => rw [← num_div_denom x]

Result:
K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) (x.num * q) = (algebraMap K[X] (RatFunc K)) (p * x.denom) ↔
    (algebraMap K[X] (RatFunc K)) x.num / (algebraMap K[X] (RatFunc K)) x.denom * (algebraMap K[X] (RatFunc K)) q =
      (algebraMap K[X] (RatFunc K)) p

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ x.num * q = p * x.denom ↔ x = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q

Tactic:
rw [← (algebraMap_injective K).eq_iff, eq_div_iff (algebraMap_ne_zero hq)]

Result:
K : Type u
inst✝ : Field K
x : RatFunc K
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] (RatFunc K)) (x.num * q) = (algebraMap K[X] (RatFunc K)) (p * x.denom) ↔
    x * (algebraMap K[X] (RatFunc K)) q = (algebraMap K[X] (RatFunc K)) p
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iio_subset_Iio_iff : Iio a ⊆ Iio b ↔ a ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Iio a ⊆ Iio b ↔ a ≤ b

Tactic:
refine ⟨fun h => ?_, fun h => Iio_subset_Iio h⟩

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Iio a ⊆ Iio b
⊢ a ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Iio a ⊆ Iio b
ab : ¬a ≤ b
⊢ False

Tactic:
exact lt_irrefl _ (h (not_le.mp ab))

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Iio a ⊆ Iio b
⊢ a ≤ b

Tactic:
by_contra ab

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Iio a ⊆ Iio b
ab : ¬a ≤ b
⊢ False
-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem restrict_map_withDensity_abs_det_fderiv_eq_addHaar (hs : MeasurableSet s)
    (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) :
    Measure.map (s.restrict f) (comap (↑) (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) =
      μ.restrict (f '' s)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A : Measure.map F (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)
⊢ F = s.restrict f

Tactic:
ext x

Result:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A : Measure.map F (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)
x : ↑s
⊢ F x = s.restrict f x

Proof state:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A : Measure.map F (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)
x : ↑s
⊢ F x = s.restrict f x

Tactic:
exact uf x.2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem mem_of_find?_eq_some {xs : Array α} (h : find? p xs = some a) : a ∈ xs

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
toList✝ : List α
h : List.find? p toList✝ = some a
⊢ a ∈ { toList := toList✝ }

Tactic:
simpa using List.mem_of_find?_eq_some h

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
xs : Array α
h : find? p xs = some a
⊢ a ∈ xs

Tactic:
cases xs

Result:
case mk
α : Type u_1
p : α → Bool
a : α
toList✝ : List α
h : find? p { toList := toList✝ } = some a
⊢ a ∈ { toList := toList✝ }

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
toList✝ : List α
h : find? p { toList := toList✝ } = some a
⊢ a ∈ { toList := toList✝ }

Tactic:
simp at h

Result:
case mk
α : Type u_1
p : α → Bool
a : α
toList✝ : List α
h : List.find? p toList✝ = some a
⊢ a ∈ { toList := toList✝ }
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem intCast_inj {a b : Int} : (a : Rat) = (b : Rat) ↔ a = b

Proof state:
a b : Int
⊢ ↑a = ↑b ↔ a = b

Tactic:
constructor

Result:
case mp
a b : Int
⊢ ↑a = ↑b → a = b

case mpr
a b : Int
⊢ a = b → ↑a = ↑b

Proof state:
case mp.refl
a : Int
⊢ a = a

Tactic:
rfl

Result:
no goals

Proof state:
case mp
a b : Int
⊢ ↑a = ↑b → a = b

Tactic:
rintro ⟨⟩

Result:
case mp.refl
a : Int
⊢ a = a

Proof state:
case mpr
a b : Int
⊢ a = b → ↑a = ↑b

Tactic:
simp_all

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousWithinAt.comp_of_eq {g : β → γ} {t : Set β} {y : β}
    (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (h : MapsTo f s t)
    (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
h : MapsTo f s t
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
exact hg.comp hf h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
h : MapsTo f s t
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
subst hy

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
h : MapsTo f s t
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) s x
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem cancel_mono_assoc_iff (f : X ⟶ Y) [Mono f] {g h : Z ⟶ X} {W : C} {k l : W ⟶ Z} :
    k ≫ (g ≫ f) = l ≫ (h ≫ f) ↔ k ≫ g = l ≫ h :=
  ⟨fun p => (cancel_mono f).1 <| by simpa using p, fun p => by simp only [← Category.assoc, p]⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Mono f
g h : Z ⟶ X
W : C
k l : W ⟶ Z
p : k ≫ g = l ≫ h
⊢ k ≫ g ≫ f = l ≫ h ≫ f

Tactic:
simp only [← Category.assoc, p]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Mono f
g h : Z ⟶ X
W : C
k l : W ⟶ Z
p : k ≫ g ≫ f = l ≫ h ≫ f
⊢ (k ≫ g) ≫ f = (l ≫ h) ≫ f

Tactic:
simpa using p

Result:
no goals
-- Mathlib/Order/Filter/SmallSets.lean
theorem smallSets_eq_generate {f : Filter α} : f.smallSets = generate (powerset '' f.sets)

Proof state:
α : Type u_1
f : Filter α
⊢ f.smallSets = generate (powerset '' f.sets)

Tactic:
simp_rw [generate_eq_biInf, smallSets, iInf_image, Filter.lift', Filter.lift, Function.comp_apply,
  Filter.mem_sets]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem foldr_attach (l : Vector α n) (f : α → β → β) (b : β) :
    l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l : Array α
⊢ foldr (fun t acc => f t.val acc) b { toArray := l, size_toArray := ⋯ }.attach =
    foldr f b { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.foldr_attach]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : α → β → β
b : β
⊢ foldr (fun t acc => f t.val acc) b l.attach = foldr f b l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l : Array α
⊢ foldr (fun t acc => f t.val acc) b { toArray := l, size_toArray := ⋯ }.attach =
    foldr f b { toArray := l, size_toArray := ⋯ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatten_mkVector_mkVector : (mkVector n (mkVector m a)).flatten = mkVector (n * m) a

Proof state:
case h
n m : Nat
α✝ : Type u_1
a : α✝
i : Nat
h : i < n * m
⊢ (mkVector n (mkVector m a)).flatten[i] = (mkVector (n * m) a)[i]

Tactic:
simp [h]

Result:
no goals

Proof state:
n m : Nat
α✝ : Type u_1
a : α✝
⊢ (mkVector n (mkVector m a)).flatten = mkVector (n * m) a

Tactic:
ext i h

Result:
case h
n m : Nat
α✝ : Type u_1
a : α✝
i : Nat
h : i < n * m
⊢ (mkVector n (mkVector m a)).flatten[i] = (mkVector (n * m) a)[i]
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_eq_prod {β : Type*} [CommMonoid β] (s : Finset α) (f : α → β) :
    (noncommProd s f fun _ _ _ _ _ => Commute.all _ _) = s.prod f

Proof state:
α : Type u_3
β : Type u_6
inst✝ : CommMonoid β
s : Finset α
f : α → β
⊢ s.noncommProd f ⋯ = s.prod f

Tactic:
induction' s using Finset.cons_induction_on with a s ha IH

Result:
case h₁
α : Type u_3
β : Type u_6
inst✝ : CommMonoid β
f : α → β
⊢ ∅.noncommProd f ⋯ = ∅.prod f

case h₂
α : Type u_3
β : Type u_6
inst✝ : CommMonoid β
f : α → β
a : α
s : Finset α
ha : a ∉ s
IH : s.noncommProd f ⋯ = s.prod f
⊢ (cons a s ha).noncommProd f ⋯ = (cons a s ha).prod f

Proof state:
case h₁
α : Type u_3
β : Type u_6
inst✝ : CommMonoid β
f : α → β
⊢ ∅.noncommProd f ⋯ = ∅.prod f

Tactic:
simp

Result:
no goals

Proof state:
case h₂
α : Type u_3
β : Type u_6
inst✝ : CommMonoid β
f : α → β
a : α
s : Finset α
ha : a ∉ s
IH : s.noncommProd f ⋯ = s.prod f
⊢ (cons a s ha).noncommProd f ⋯ = (cons a s ha).prod f

Tactic:
simp [ha, IH]

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem isConnected_univ_pi [∀ i, TopologicalSpace (π i)] {s : ∀ i, Set (π i)} :
    IsConnected (pi univ s) ↔ ∀ i, IsConnected (s i)

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
⊢ IsConnected (univ.pi s) ↔ ∀ (i : ι), IsConnected (s i)

Tactic:
simp only [IsConnected, ← univ_pi_nonempty_iff, forall_and, and_congr_right_iff]

Result:
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
⊢ (univ.pi s).Nonempty → (IsPreconnected (univ.pi s) ↔ ∀ (x : ι), IsPreconnected (s x))

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hne : (univ.pi s).Nonempty
hc : IsPreconnected (univ.pi s)
i : ι
⊢ IsPreconnected ((fun f => f i) '' univ.pi s)

Tactic:
exact hc.image _ (continuous_apply _).continuousOn

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hne : (univ.pi s).Nonempty
hc : IsPreconnected (univ.pi s)
i : ι
⊢ IsPreconnected (s i)

Tactic:
rw [← eval_image_univ_pi hne]

Result:
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hne : (univ.pi s).Nonempty
hc : IsPreconnected (univ.pi s)
i : ι
⊢ IsPreconnected ((fun f => f i) '' univ.pi s)

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
⊢ (univ.pi s).Nonempty → (IsPreconnected (univ.pi s) ↔ ∀ (x : ι), IsPreconnected (s x))

Tactic:
refine fun hne => ⟨fun hc i => ?_, isPreconnected_univ_pi⟩

Result:
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hne : (univ.pi s).Nonempty
hc : IsPreconnected (univ.pi s)
i : ι
⊢ IsPreconnected (s i)
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_sub_eq_toIcoDiv_add' (a b c : α) :
    toIcoDiv hp (a - c) b = toIcoDiv hp a (b + c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoDiv hp (a - c) b = toIcoDiv hp a (b + c)

Tactic:
rw [← sub_neg_eq_add, toIcoDiv_sub_eq_toIcoDiv_add, sub_eq_add_neg]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
lemma restrict (h : μ ⟂ₘ ν) (s : Set α) : μ.restrict s ⟂ₘ ν

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
⊢ μ (h.nullSet ∩ s) = 0

Tactic:
exact measure_mono_null Set.inter_subset_left h.measure_nullSet

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
⊢ μ.restrict s ⟂ₘ ν

Tactic:
refine ⟨h.nullSet, h.measurableSet_nullSet, ?_, h.measure_compl_nullSet⟩

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
⊢ (μ.restrict s) h.nullSet = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
⊢ (μ.restrict s) h.nullSet = 0

Tactic:
rw [Measure.restrict_apply h.measurableSet_nullSet]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
⊢ μ (h.nullSet ∩ s) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_map {f : α → β} {l : Vector α n} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
b : β
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ b ∈ map f { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    ∃ a, a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∧ f a = b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
b : β
f : α → β
l : Vector α n
⊢ b ∈ map f l ↔ ∃ a, a ∈ l ∧ f a = b

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
b : β
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ b ∈ map f { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    ∃ a, a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∧ f a = b
-- Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
theorem Integrable.exists_boundedContinuous_integral_sub_le [μ.WeaklyRegular] {f : α → E}
    (hf : Integrable f μ) {ε : ℝ} (hε : 0 < ε) :
    ∃ g : α →ᵇ E, (∫ x, ‖f x - g x‖ ∂μ) ≤ ε ∧ Integrable g μ

Proof state:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
ε : ℝ
hε : 0 < ε
hf : MemLp f (ENNReal.ofReal 1) μ
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ MemLp (⇑g) (ENNReal.ofReal 1) μ

Tactic:
simpa using hf.exists_boundedContinuous_integral_rpow_sub_le zero_lt_one hε

Result:
no goals

Proof state:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Integrable (⇑g) μ

Tactic:
simp only [← memLp_one_iff_integrable, ← eLpNorm_one_eq_lintegral_enorm, ← ENNReal.ofReal_one]
  at hf ⊢

Result:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
ε : ℝ
hε : 0 < ε
hf : MemLp f (ENNReal.ofReal 1) μ
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ MemLp (⇑g) (ENNReal.ofReal 1) μ
-- Mathlib/Topology/Algebra/Order/Field.lean
@[simp]
lemma inv_atTop₀ : (atTop : Filter 𝕜)⁻¹ = 𝓝[>] 0 :=
  (((atTop_basis_Ioi' (0 : 𝕜)).map _).comp_surjective inv_surjective).eq_of_same_basis <|
    (nhdsGT_basis _).congr (by simp) fun a ha ↦ by simp [inv_Ioi₀ (inv_pos.2 ha)]

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
a : 𝕜
ha : 0 < a
⊢ Ioo 0 a = ((fun i => Inv.inv '' Ioi i) ∘ Inv.inv) a

Tactic:
simp [inv_Ioi₀ (inv_pos.2 ha)]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ ∀ (i : 𝕜), 0 < i ↔ ((fun x => 0 < x) ∘ Inv.inv) i

Tactic:
simp

Result:
no goals