harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_mul_cpow_one_add_sq {t : ℂ} (ht : t ≠ -1) :
    (∫ x : ℝ in a..b, (x : ℂ) * ((1 : ℂ) + ↑x ^ 2) ^ t) =
      ((1 : ℂ) + (b : ℂ) ^ 2) ^ (t + 1) / (2 * (t + ↑1)) -
      ((1 : ℂ) + (a : ℂ) ^ 2) ^ (t + 1) / (2 * (t + ↑1))

Proof state:
case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + y ^ 2) (2 * ↑x) ↑x
⊢ HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x

Tactic:
have g :
  ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z := by
  intro z hz
  convert (HasDerivAt.cpow_const (c := t + 1) (hasDerivAt_id _)
    (Or.inl hz)).div_const (2 * (t + 1)) using 1
  field_simp
  ring

Result:
case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + y ^ 2) (2 * ↑x) ↑x
g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
⊢ HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x

Proof state:
case h.e'_9
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + y ^ 2) (2 * ↑x) ↑x
g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
⊢ ↑x * (1 + ↑x ^ 2) ^ t * 2 = (1 + ↑x ^ 2) ^ t * (2 * ↑x)

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_9
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
hz : 0 < z.re
⊢ z ^ t / 2 = (t + 1) * id z ^ (t + 1 - 1) * 1 / (2 * (t + 1))

Tactic:
field_simp

Result:
case h.e'_9
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => 1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
hz : 0 < z.re
⊢ z ^ t * (2 * (t + 1)) = (t + 1) * z ^ t * 2

Proof state:
a b : ℝ
t : ℂ
ht : t ≠ -1
⊢ t + 1 ≠ 0

Tactic:
contrapose! ht

Result:
a b : ℝ
t : ℂ
ht : t + 1 = 0
⊢ t = -1
-- Mathlib/Analysis/Convex/Combination.lean
theorem centerMass_le_sup {s : Finset ι} {f : ι → α} {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i)
    (hw₁ : 0 < ∑ i ∈ s, w i) :
    s.centerMass w f ≤ s.sup' (nonempty_of_ne_empty <| by rintro rfl; simp at hw₁) f

Proof state:
R : Type u_1
ι : Type u_5
α : Type u_7
inst✝³ : LinearOrderedField R
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ s, w i
⊢ s.centerMass w f ≤ s.sup' ⋯ f

Tactic:
rw [centerMass, inv_smul_le_iff_of_pos hw₁, sum_smul]

Result:
R : Type u_1
ι : Type u_5
α : Type u_7
inst✝³ : LinearOrderedField R
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ s, w i
⊢ ∑ i ∈ s, w i • f i ≤ ∑ i ∈ s, w i • s.sup' ⋯ f

Proof state:
R : Type u_1
ι : Type u_5
α : Type u_7
inst✝³ : LinearOrderedField R
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ s, w i
⊢ ∑ i ∈ s, w i • f i ≤ ∑ i ∈ s, w i • s.sup' ⋯ f

Tactic:
exact sum_le_sum fun i hi => smul_le_smul_of_nonneg_left (le_sup' _ hi) <| hw₀ i hi

Result:
no goals

Proof state:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
ι : Type u_5
ι' : Type u_6
α : Type u_7
inst✝⁸ : LinearOrderedField R
inst✝⁷ : LinearOrderedField R'
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ ∅, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ ∅, w i
⊢ False

Tactic:
simp at hw₁

Result:
no goals

Proof state:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
ι : Type u_5
ι' : Type u_6
α : Type u_7
inst✝⁸ : LinearOrderedField R
inst✝⁷ : LinearOrderedField R'
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ s, w i
⊢ s ≠ ∅

Tactic:
rintro rfl

Result:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
ι : Type u_5
ι' : Type u_6
α : Type u_7
inst✝⁸ : LinearOrderedField R
inst✝⁷ : LinearOrderedField R'
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ ∅, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ ∅, w i
⊢ False
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_erase_mul [DecidableEq α] (s : Finset α) {a : α} (h : a ∈ s) (f : α → β) (comm)
    (comm' := fun _ hx _ hy hxy ↦ comm (s.mem_of_mem_erase hx) (s.mem_of_mem_erase hy) hxy) :
    (s.erase a).noncommProd f comm' * f a = s.noncommProd f comm

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s).Pairwise (Commute on f)
comm' : optParam (∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → (Commute on f) x x_1) ⋯
⊢ (s.erase a).noncommProd f comm' * f a = s.noncommProd f comm

Tactic:
classical
simpa only [← Multiset.map_erase_of_mem _ _ h] using
  Multiset.noncommProd_erase_mul (s.1.map f) (Multiset.mem_map_of_mem f h) _

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s).Pairwise (Commute on f)
comm' : optParam (∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → (Commute on f) x x_1) ⋯
⊢ (s.erase a).noncommProd f comm' * f a = s.noncommProd f comm

Tactic:
simpa only [← Multiset.map_erase_of_mem _ _ h] using
  Multiset.noncommProd_erase_mul (s.1.map f) (Multiset.mem_map_of_mem f h) _

Result:
no goals
-- Mathlib/Topology/Perfect.lean
theorem Preperfect.open_inter {U : Set α} (hC : Preperfect C) (hU : IsOpen U) :
    Preperfect (U ∩ C)

Proof state:
case intro
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen U
x : α
xU : x ∈ U
xC : x ∈ C
⊢ AccPt x (𝓟 (U ∩ C))

Tactic:
apply (hC _ xC).nhds_inter

Result:
case intro
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen U
x : α
xU : x ∈ U
xC : x ∈ C
⊢ U ∈ 𝓝 x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen U
⊢ Preperfect (U ∩ C)

Tactic:
rintro x ⟨xU, xC⟩

Result:
case intro
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen U
x : α
xU : x ∈ U
xC : x ∈ C
⊢ AccPt x (𝓟 (U ∩ C))

Proof state:
case intro
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen U
x : α
xU : x ∈ U
xC : x ∈ C
⊢ U ∈ 𝓝 x

Tactic:
exact hU.mem_nhds xU

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
lemma collapse_modular [ExistsAddOfLE β]
    (hu : a ∉ u) (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
    (h : ∀ ⦃s⦄, s ⊆ insert a u → ∀ ⦃t⦄, t ⊆ insert a u →  f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t))
    (𝒜 ℬ : Finset (Finset α)) :
    ∀ ⦃s⦄, s ⊆ u → ∀ ⦃t⦄, t ⊆ u → collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤
      collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : LinearOrderedCommSemiring β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝¹ : s ⊆ insert a u
this✝ : t ⊆ insert a u
this : insert a s ⊆ insert a u
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
have := insert_subset_insert a htu

Result:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : LinearOrderedCommSemiring β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝² : s ⊆ insert a u
this✝¹ : t ⊆ insert a u
this✝ : insert a s ⊆ insert a u
this : insert a t ⊆ insert a u
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem adjoint_comp (A : F →L[𝕜] G) (B : E →L[𝕜] F) : (A ∘L B)† = B† ∘L A†

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
w : E
⊢ ⟪w, (adjoint (A.comp B)) v⟫_𝕜 = ⟪w, ((adjoint B).comp (adjoint A)) v⟫_𝕜

Tactic:
simp only [adjoint_inner_right, ContinuousLinearMap.coe_comp', Function.comp_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
⊢ adjoint (A.comp B) = (adjoint B).comp (adjoint A)

Tactic:
ext v

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
⊢ (adjoint (A.comp B)) v = ((adjoint B).comp (adjoint A)) v

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
⊢ (adjoint (A.comp B)) v = ((adjoint B).comp (adjoint A)) v

Tactic:
refine ext_inner_left 𝕜 fun w => ?_

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
w : E
⊢ ⟪w, (adjoint (A.comp B)) v⟫_𝕜 = ⟪w, ((adjoint B).comp (adjoint A)) v⟫_𝕜
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem crossing_eq_crossing_of_lowerCrossingTime_lt {M : ℕ} (hNM : N ≤ M)
    (h : lowerCrossingTime a b f N n ω < N) :
    upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧
      lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : upperCrossingTime a b f N (k + 1) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
⊢ upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω

Tactic:
rw [upperCrossingTime_succ_eq, hitting_lt_iff] at h'

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
⊢ upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω

case hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
⊢ N ≤ N

Proof state:
case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : ∃ j ∈ Set.Ico (upperCrossingTime a b f N 0 ω) N, f j ω ∈ Set.Iic a
h' : upperCrossingTime a b f N 0 ω < N
⊢ ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := h

Result:
case zero.intro.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h' : upperCrossingTime a b f N 0 ω < N
j : ℕ
hj₁ : j ∈ Set.Ico (upperCrossingTime a b f N 0 ω) N
hj₂ : f j ω ∈ Set.Iic a
⊢ ∃ j ∈ Set.Icc 0 N, f j ω ∈ Set.Iic a

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω

Tactic:
have h' : upperCrossingTime a b f N n ω < N :=
  lt_of_le_of_lt upperCrossingTime_le_lowerCrossingTime h

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N n ω < N
h' : upperCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem Continuous.integrableAt_nhds [TopologicalSpace α] [SecondCountableTopologyEither α E]
    [OpensMeasurableSpace α] {μ : Measure α} [IsLocallyFiniteMeasure μ] {f : α → E}
    (hf : Continuous f) (a : α) : IntegrableAtFilter f (𝓝 a) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Continuous f
a : α
⊢ IntegrableAtFilter f (𝓝[univ] a) μ

Tactic:
exact hf.continuousOn.integrableAt_nhdsWithin MeasurableSet.univ (mem_univ a)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Continuous f
a : α
⊢ IntegrableAtFilter f (𝓝 a) μ

Tactic:
rw [← nhdsWithin_univ]

Result:
α : Type u_1
E : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Continuous f
a : α
⊢ IntegrableAtFilter f (𝓝[univ] a) μ
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
lemma boundaryLE {k' : ι'} {j : ι} (hj : c'.Rel (e.f j) k') (hk' : ∀ i, e.f i ≠ k') :
    e.BoundaryLE j

Proof state:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
k : ι
hk : c'.Rel (e.f j) (e.f k)
⊢ e.f k = k'

Tactic:
rw [← c'.next_eq' hj, c'.next_eq' hk]

Result:
no goals

Proof state:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
k : ι
hk : c'.Rel (e.f j) (e.f k)
⊢ False

Tactic:
apply hk' k

Result:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
k : ι
hk : c'.Rel (e.f j) (e.f k)
⊢ e.f k = k'

Proof state:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ ∀ (k : ι), ¬c'.Rel (e.f j) (e.f k)

Tactic:
intro k hk

Result:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
k : ι
hk : c'.Rel (e.f j) (e.f k)
⊢ False

Proof state:
case left
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ c'.Rel (e.f j) (c'.next (e.f j))

Tactic:
simpa only [c'.next_eq' hj] using hj

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ e.BoundaryLE j

Tactic:
constructor

Result:
case left
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ c'.Rel (e.f j) (c'.next (e.f j))

case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ ∀ (k : ι), ¬c'.Rel (e.f j) (e.f k)
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem map_of_mul_left_rel_one [Monoid M] (c : Con M)
    (f : M → M) (hf : ∀ x, c (f x * x) 1) {x y} (h : c x y) : c (f x) (f y)

Proof state:
M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x✝ y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x✝ = ↑y
x : M
⊢ ↑(f (f x)) * ↑(f x) * (↑x * ↑(f x)) = ↑(f (f x)) * (↑(f x) * ↑x) * ↑(f x)

Tactic:
ac_rfl

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x = ↑y
hf' : ∀ (x : M), ↑x * ↑(f x) = 1
this :
  { val := ↑x, inv := ↑(f x), val_inv := ⋯, inv_val := ⋯ } = { val := ↑y, inv := ↑(f y), val_inv := ⋯, inv_val := ⋯ }
⊢ ↑(f x) = ↑(f y)

Tactic:
exact congr_arg Units.inv this

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x✝ y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x✝ = ↑y
x : M
⊢ ↑x * ↑(f x) = ↑(f (f x)) * ↑(f x) * (↑x * ↑(f x))

Tactic:
simp [hf]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x = ↑y
hf' : ∀ (x : M), ↑x * ↑(f x) = 1
⊢ ↑(f x) = ↑(f y)

Tactic:
have : (⟨_, _, hf' x, hf x⟩ : c.Quotientˣ) = ⟨_, _, hf' y, hf y⟩ := Units.ext h

Result:
M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x = ↑y
hf' : ∀ (x : M), ↑x * ↑(f x) = 1
this :
  { val := ↑x, inv := ↑(f x), val_inv := ⋯, inv_val := ⋯ } = { val := ↑y, inv := ↑(f y), val_inv := ⋯, inv_val := ⋯ }
⊢ ↑(f x) = ↑(f y)

Proof state:
M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x = ↑y
⊢ ↑(f x) = ↑(f y)

Tactic:
have hf' : ∀ x : M, (x : c.Quotient) * f x = 1 := fun x ↦
  calc
    (x : c.Quotient) * f x = f (f x) * f x * (x * f x) := by simp [hf]
    _ = f (f x) * (f x * x) * f x := by ac_rfl
    _ = 1 := by simp [hf]

Result:
M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x = ↑y
hf' : ∀ (x : M), ↑x * ↑(f x) = 1
⊢ ↑(f x) = ↑(f y)

Proof state:
M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x✝ y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x✝ = ↑y
x : M
⊢ ↑(f (f x)) * (↑(f x) * ↑x) * ↑(f x) = 1

Tactic:
simp [hf]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
hf : ∀ (x : M), c (f x * x) 1
x y : M
h : c x y
⊢ c (f x) (f y)

Tactic:
simp only [← Con.eq, coe_one, coe_mul] at *

Result:
M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x = ↑y
⊢ ↑(f x) = ↑(f y)
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem map_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) :
    (p.append q).map f = (p.map f).append (q.map f)

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ Walk.map f (p.append q) = (Walk.map f p).append (Walk.map f q)

Tactic:
induction p <;> simp [*]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Sites/Small.lean
lemma mem_toGrothendieck_smallPretopology (X : Q.Over ⊤ S) (R : Sieve X) :
    R ∈ (S.smallPretopology P Q).toGrothendieck _ X ↔
      ∀ x : X.left, ∃ (Y : Q.Over ⊤ S) (f : Y ⟶ X) (y : Y.left),
        R f ∧ P f.left ∧ f.left.base y = x

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁶ : P.IsMultiplicative
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : IsJointlySurjectivePreserving P
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
x : ↑↑X.left.toPresheafedSpace
y : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace
hy : (ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) y = x
⊢ ∃ Y f y, R.arrows f ∧ P f.left ∧ (ConcreteCategory.hom f.left.base) y = x

Tactic:
refine ⟨(𝒰.obj (𝒰.f x)).asOverProp S (p _), (𝒰.map (𝒰.f x)).asOverProp S, y, hle _ ?_,
  𝒰.map_prop _, hy⟩

Result:
case refine_1.intro.intro.intro.intro.intro.intro
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁶ : P.IsMultiplicative
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : IsJointlySurjectivePreserving P
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover P X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
x : ↑↑X.left.toPresheafedSpace
y : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace
hy : (ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) y = x
⊢ Hom.asOverProp (𝒰.map (𝒰.f x)) S ∈ 𝒰.toPresieveOverProp p
-- Mathlib/.lake/packages/batteries/Batteries/Control/Lawful/MonadLift.lean
theorem monadLift_seq [LawfulMonad m] [LawfulMonad n] (mf : m (α → β)) (ma : m α) :
    monadLift (mf <*> ma) = monadLift mf <*> (monadLift ma : n α)

Proof state:
m : Type u_1 → Type u_2
n : Type u_1 → Type u_3
inst✝⁵ : Monad m
inst✝⁴ : Monad n
inst✝³ : MonadLiftT m n
inst✝² : LawfulMonadLiftT m n
α β : Type u_1
inst✝¹ : LawfulMonad m
inst✝ : LawfulMonad n
mf : m (α → β)
ma : m α
⊢ monadLift (mf <*> ma) = monadLift mf <*> monadLift ma

Tactic:
simp only [seq_eq_bind, monadLift_map, monadLift_bind]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_eq_size {p} : countP p l = l.size ↔ ∀ a ∈ l, p a

Proof state:
case mk
α✝ : Type u_1
p : α✝ → Bool
toList✝ : List α✝
⊢ countP p { toList := toList✝ } = { toList := toList✝ }.size ↔ ∀ (a : α✝), a ∈ { toList := toList✝ } → p a = true

Tactic:
simp

Result:
no goals

Proof state:
α✝ : Type u_1
l : Array α✝
p : α✝ → Bool
⊢ countP p l = l.size ↔ ∀ (a : α✝), a ∈ l → p a = true

Tactic:
cases l

Result:
case mk
α✝ : Type u_1
p : α✝ → Bool
toList✝ : List α✝
⊢ countP p { toList := toList✝ } = { toList := toList✝ }.size ↔ ∀ (a : α✝), a ∈ { toList := toList✝ } → p a = true