harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Instances/AddCircle.lean
theorem coe_eq_coe_iff_of_mem_Ico {x y : 𝕜} (hx : x ∈ Ico a (a + p)) (hy : y ∈ Ico a (a + p)) :
    (x : AddCircle p) = y ↔ x = y

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
⊢ x = y → ↑x = ↑y

Tactic:
tauto

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
⊢ x = y

Tactic:
suffices (⟨x, hx⟩ : Ico a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this

Result:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : (equivIco p a) ↑x = (equivIco p a) ↑y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
rw [← (equivIco p a).right_inv ⟨x, hx⟩, ← (equivIco p a).right_inv ⟨y, hy⟩]

Result:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : (equivIco p a) ↑x = (equivIco p a) ↑y
⊢ (equivIco p a).toFun ((equivIco p a).invFun ⟨x, hx⟩) = (equivIco p a).toFun ((equivIco p a).invFun ⟨y, hy⟩)

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
apply_fun equivIco p a at h

Result:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : (equivIco p a) ↑x = (equivIco p a) ↑y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
this : ⟨x, hx⟩ = ⟨y, hy⟩
⊢ x = y

Tactic:
exact Subtype.mk.inj this

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : (equivIco p a) ↑x = (equivIco p a) ↑y
⊢ (equivIco p a).toFun ((equivIco p a).invFun ⟨x, hx⟩) = (equivIco p a).toFun ((equivIco p a).invFun ⟨y, hy⟩)

Tactic:
exact h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
⊢ ↑x = ↑y ↔ x = y

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

Result:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
⊢ x = y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem getElem_enum (l : List α) (i : Nat) (h : i < l.enum.length) :
    l.enum[i] = (i, l[i]'(by simpa [enum_length] using h))

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.enum.length
⊢ l.enum[i] = (i, l[i])

Tactic:
simp [enum]

Result:
no goals

Proof state:
α : Type ?u.69157
l : List α
i : Nat
h : i < l.enum.length
⊢ i < l.length

Tactic:
simpa [enum_length] using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem resolve_left_inv_dvd (a c d p k : Int) (a_pos : 0 < a)
    (h₄ : a ∣ k + p) (h₅ : a * d ∣ c * k + c * p + a * s) :
    d ∣ c * resolve_left_inv a p k + s

Proof state:
s a c d p k : Int
a_pos : 0 < a
h₄ : a ∣ k + p
h₅ : a * d ∣ c * k + c * p + a * s
⊢ a * d ∣ c * k + c * p + a * s

Tactic:
exact h₅

Result:
no goals

Proof state:
s a c d p k : Int
a_pos : 0 < a
h₄ : a ∣ k + p
h₅ : a * d ∣ c * k + c * p + a * s
⊢ d ∣ c * resolve_left_inv a p k + s

Tactic:
suffices h : a * d ∣ a * ((c * ((k + p) / a)) + s) from dvd_of_mul_dvd h a_pos

Result:
s a c d p k : Int
a_pos : 0 < a
h₄ : a ∣ k + p
h₅ : a * d ∣ c * k + c * p + a * s
⊢ a * d ∣ a * (c * ((k + p) / a) + s)

Proof state:
s a c d p k : Int
a_pos : 0 < a
h₄ : a ∣ k + p
h₅ : a * d ∣ c * k + c * p + a * s
⊢ a * d ∣ a * (c * ((k + p) / a) + s)

Tactic:
rw [Int.mul_add, Int.mul_left_comm, Int.mul_ediv_cancel' h₄, Int.mul_add]

Result:
s a c d p k : Int
a_pos : 0 < a
h₄ : a ∣ k + p
h₅ : a * d ∣ c * k + c * p + a * s
⊢ a * d ∣ c * k + c * p + a * s
-- Mathlib/Analysis/Convex/StrictConvexBetween.lean
lemma eq_midpoint_of_dist_eq_half (hx : dist x y = dist x z / 2) (hy : dist y z = dist x z / 2) :
    y = midpoint ℝ x z

Proof state:
case hyz
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist y z = (1 - ⅟2) * dist x z

Tactic:
rwa [invOf_eq_inv, ← one_div, sub_half, one_div, ← div_eq_inv_mul]

Result:
no goals

Proof state:
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ y = midpoint ℝ x z

Tactic:
apply eq_lineMap_of_dist_eq_mul_of_dist_eq_mul

Result:
case hxy
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist x y = ⅟2 * dist x z

case hyz
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist y z = (1 - ⅟2) * dist x z

Proof state:
case hxy
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist x y = ⅟2 * dist x z

Tactic:
rwa [invOf_eq_inv, ← div_eq_inv_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean
/-- If the kernel comparison map for `G` at `f` is an isomorphism, then `G` preserves the
kernel of `f`.
-/
lemma PreservesKernel.of_iso_comparison [i : IsIso (kernelComparison f G)] :
    PreservesLimit (parallelPair f 0) G

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
i : IsIso (kernelComparison f G)
⊢ IsLimit (G.mapCone (Fork.ofι (kernel.ι f) ⋯))

Tactic:
apply (isLimitMapConeForkEquiv' G (kernel.condition f)).symm _

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
i : IsIso (kernelComparison f G)
⊢ IsLimit (KernelFork.ofι (G.map (kernel.ι f)) ⋯)

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
i : IsIso (kernelComparison f G)
⊢ IsLimit (KernelFork.ofι (G.map (kernel.ι f)) ⋯)

Tactic:
exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (kernelIsKernel (G.map f)) i

Result:
no goals

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
i : IsIso (kernelComparison f G)
⊢ PreservesLimit (parallelPair f 0) G

Tactic:
apply preservesLimit_of_preserves_limit_cone (kernelIsKernel f)

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
i : IsIso (kernelComparison f G)
⊢ IsLimit (G.mapCone (Fork.ofι (kernel.ι f) ⋯))
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem hasFiniteIntegral_iff_enorm {f : α → β} : HasFiniteIntegral f μ ↔ ∫⁻ a, ‖f a‖ₑ ∂μ < ∞

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤

Tactic:
simp only [HasFiniteIntegral, ofReal_norm_eq_enorm, enorm_eq_nnnorm]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_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:
rw [← isLittleO_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:
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
cne0 : ‖c‖ ≠ 0
⊢ (f =o[l] fun x => ‖c‖ * ‖f' x‖) ↔ f =o[l] f'

Tactic:
rw [isLittleO_const_mul_right_iff cne0, isLittleO_norm_right]

Result:
no goals

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'
-- Mathlib/Computability/Language.lean
theorem le_mul_congr {l₁ l₂ m₁ m₂ : Language α} : l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ * l₂ ≤ m₁ * m₂

Proof state:
α : Type u_1
l₁ l₂ m₁ m₂ : Language α
⊢ l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ * l₂ ≤ m₁ * m₂

Tactic:
intro h₁ h₂ x hx

Result:
α : Type u_1
l₁ l₂ m₁ m₂ : Language α
h₁ : l₁ ≤ m₁
h₂ : l₂ ≤ m₂
x : List α
hx : x ∈ l₁ * l₂
⊢ x ∈ m₁ * m₂

Proof state:
α : Type u_1
l₁ l₂ m₁ m₂ : Language α
h₁ : l₁ ≤ m₁
h₂ : l₂ ≤ m₂
x : List α
hx : x ∈ l₁ * l₂
⊢ x ∈ m₁ * m₂

Tactic:
simp only [mul_def, exists_and_left, mem_image2, image_prod] at hx ⊢

Result:
α : Type u_1
l₁ l₂ m₁ m₂ : Language α
h₁ : l₁ ≤ m₁
h₂ : l₂ ≤ m₂
x : List α
hx : ∃ a ∈ l₁, ∃ b ∈ l₂, a ++ b = x
⊢ ∃ a ∈ m₁, ∃ b ∈ m₂, a ++ b = x

Proof state:
α : Type u_1
l₁ l₂ m₁ m₂ : Language α
h₁ : l₁ ≤ m₁
h₂ : l₂ ≤ m₂
x : List α
hx : ∃ a ∈ l₁, ∃ b ∈ l₂, a ++ b = x
⊢ ∃ a ∈ m₁, ∃ b ∈ m₂, a ++ b = x

Tactic:
tauto

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem map_nhds_induced_of_surjective [T : TopologicalSpace α] {f : β → α} (hf : Surjective f)
    (a : β) : map f (@nhds β (TopologicalSpace.induced f T) a) = 𝓝 (f a)

Proof state:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
hf : Surjective f
a : β
⊢ map f (𝓝 a) = 𝓝 (f a)

Tactic:
rw [nhds_induced, map_comap_of_surjective hf]

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain'_append_cons_cons {b c : α} {l₁ l₂ : List α} :
    Chain' R (l₁ ++ b :: c :: l₂) ↔ Chain' R (l₁ ++ [b]) ∧ R b c ∧ Chain' R (c :: l₂)

Proof state:
α : Type u
R : α → α → Prop
b c : α
l₁ l₂ : List α
⊢ Chain' R (l₁ ++ b :: c :: l₂) ↔ Chain' R (l₁ ++ [b]) ∧ R b c ∧ Chain' R (c :: l₂)

Tactic:
rw [chain'_split, chain'_cons]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma setLIntegral_rnDeriv [HaveLebesgueDecomposition μ ν] [SFinite ν]
    (hμν : μ ≪ ν) (s : Set α) :
    ∫⁻ x in s, μ.rnDeriv ν x ∂ν = μ s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = μ s

Tactic:
rw [← withDensity_apply' _ s, Measure.withDensity_rnDeriv_eq _ _ hμν]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_unitOfList [EquivBEq α] [LawfulHashable α]
    {l : List α} {k : α} :
    get? (unitOfList l) k =
    if l.contains k then some () else none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
⊢ get? (unitOfList l) k = if l.contains k = true then some () else none

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

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem lt_isLUB_iff (h : IsLUB s a) : b < a ↔ ∃ c ∈ s, b < c

Proof state:
α : Type u
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ b < a ↔ ∃ c ∈ s, b < c

Tactic:
simp_rw [← not_le, isLUB_le_iff h, mem_upperBounds, not_forall, not_le, exists_prop]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk_eq_monoidOf_mk'_apply (x y) : mk x y = (monoidOf S).mk' x y :=
  show _ = _ * _ from
    (Submonoid.LocalizationMap.mul_inv_right (monoidOf S).map_units _ _ _).2 <| by
      rw [← mk_one_eq_monoidOf_mk, ← mk_one_eq_monoidOf_mk, mk_mul x y y 1, mul_comm y 1]
      conv => rhs; rw [← mul_one 1]; rw [← mul_one x]
      exact mk_eq_mk_iff.2 (Con.symm _ <| (Localization.r S).mul (Con.refl _ (x, 1)) <| one_rel _)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
⊢ mk (x * ↑y) (1 * y) = mk (x * 1) (1 * 1)

Tactic:
exact mk_eq_mk_iff.2 (Con.symm _ <| (Localization.r S).mul (Con.refl _ (x, 1)) <| one_rel _)

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
⊢ mk x y * (monoidOf S).toMap ↑y = (monoidOf S).toMap x

Tactic:
rw [← mk_one_eq_monoidOf_mk, ← mk_one_eq_monoidOf_mk, mk_mul x y y 1, mul_comm y 1]

Result:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
⊢ mk (x * ↑y) (1 * y) = mk x 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
⊢ mk (x * ↑y) (1 * y) = mk x 1

Tactic:
conv => rhs; rw [← mul_one 1]; rw [← mul_one x]

Result:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
⊢ mk (x * ↑y) (1 * y) = mk (x * 1) (1 * 1)
-- Mathlib/LinearAlgebra/Basis/Flag.lean
theorem flag_mono (b : Basis (Fin n) R M) : Monotone b.flag :=
  Fin.monotone_iff_le_succ.2 fun k ↦ by rw [flag_succ]; exact le_sup_right

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ b.flag k.castSucc ≤ b.flag k.succ

Tactic:
rw [flag_succ]

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ b.flag k.castSucc ≤ span R {b k} ⊔ b.flag k.castSucc

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ b.flag k.castSucc ≤ span R {b k} ⊔ b.flag k.castSucc

Tactic:
exact le_sup_right

Result:
no goals
-- Mathlib/Analysis/Convex/Uniform.lean
theorem exists_forall_closed_ball_dist_add_le_two_sub (hε : 0 < ε) :
    ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ

Proof state:
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := 1 / 2 ⊓ (ε / 3 ⊓ δ / 3)
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ 2 - δ + δ' + δ' ≤ 2 - δ'

Tactic:
suffices δ' ≤ δ / 3 by linarith

Result:
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := 1 / 2 ⊓ (ε / 3 ⊓ δ / 3)
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ δ' ≤ δ / 3

Proof state:
case intro.intro
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ

Tactic:
set δ' := min (1 / 2) (min (ε / 3) <| δ / 3)

Result:
case intro.intro
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := 1 / 2 ⊓ (ε / 3 ⊓ δ / 3)
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobject_arrow' :
    (imageSubobjectIso f).inv ≫ (imageSubobject f).arrow = image.ι f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
⊢ (imageSubobjectIso f).inv ≫ (imageSubobject f).arrow = image.ι f

Tactic:
simp [imageSubobjectIso]

Result:
no goals
-- Mathlib/Data/List/Indexes.lean
theorem oldMapIdxCore_eq (l : List α) (f : ℕ → α → β) (n : ℕ) :
    l.oldMapIdxCore f n = l.oldMapIdx fun i a ↦ f (i + n) a

Proof state:
case cons
α : Type u
β : Type v
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β) (n : ℕ), List.oldMapIdxCore f n tl = List.oldMapIdx (fun i a => f (i + n) a) tl
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n (hd :: tl) = List.oldMapIdx (fun i a => f (i + n) a) (hd :: tl)

Tactic:
rw [List.oldMapIdx]

Result:
case cons
α : Type u
β : Type v
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β) (n : ℕ), List.oldMapIdxCore f n tl = List.oldMapIdx (fun i a => f (i + n) a) tl
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n (hd :: tl) = List.oldMapIdxCore (fun i a => f (i + n) a) 0 (hd :: tl)

Proof state:
case nil
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n [] = List.oldMapIdx (fun i a => f (i + n) a) []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β) (n : ℕ), List.oldMapIdxCore f n tl = List.oldMapIdx (fun i a => f (i + n) a) tl
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n (hd :: tl) = List.oldMapIdxCore (fun i a => f (i + n) a) 0 (hd :: tl)

Tactic:
simp only [List.oldMapIdxCore, hl, Nat.add_left_comm, Nat.add_comm, Nat.add_zero]

Result:
no goals

Proof state:
α : Type u
β : Type v
l : List α
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n l = List.oldMapIdx (fun i a => f (i + n) a) l

Tactic:
induction' l with hd tl hl generalizing f n

Result:
case nil
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n [] = List.oldMapIdx (fun i a => f (i + n) a) []

case cons
α : Type u
β : Type v
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β) (n : ℕ), List.oldMapIdxCore f n tl = List.oldMapIdx (fun i a => f (i + n) a) tl
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n (hd :: tl) = List.oldMapIdx (fun i a => f (i + n) a) (hd :: tl)
-- Mathlib/Analysis/BoundedVariation.lean
theorem ae_differentiableWithinAt {f : ℝ → V} {s : Set ℝ} (h : LocallyBoundedVariationOn f s)
    (hs : MeasurableSet s) : ∀ᵐ x ∂volume.restrict s, DifferentiableWithinAt ℝ f s x

Proof state:
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict s, DifferentiableWithinAt ℝ f s x

Tactic:
rw [ae_restrict_iff' hs]

Result:
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Proof state:
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
exact h.ae_differentiableWithinAt_of_mem

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_eq_head_reverse {l : List α} (h : l ≠ []) :
    l.getLast h = l.reverse.head (by simp_all)

Proof state:
α : Type u_1
l : List α
h : l ≠ []
⊢ l.getLast h = l.reverse.head ⋯

Tactic:
rw [← head_reverse]

Result:
no goals

Proof state:
α : Type ?u.311322
l : List α
h : l ≠ []
⊢ l.reverse ≠ []

Tactic:
simp_all

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem HasDerivWithinAt.rpow (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x)
    (h : 0 < f x) : HasDerivWithinAt (fun x => f x ^ g x)
      (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) s x

Proof state:
case h.e'_9
f g : ℝ → ℝ
f' g' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    g x * f x ^ (g x - 1) * (1 * f') + f x ^ g x * Real.log (f x) * (1 * g')

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_9
f g : ℝ → ℝ
f' g' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    ((g x * f x ^ (g x - 1)) • ContinuousLinearMap.smulRight 1 f' +
        (f x ^ g x * Real.log (f x)) • ContinuousLinearMap.smulRight 1 g')
      1

Tactic:
dsimp

Result:
case h.e'_9
f g : ℝ → ℝ
f' g' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    g x * f x ^ (g x - 1) * (1 * f') + f x ^ g x * Real.log (f x) * (1 * g')

Proof state:
f g : ℝ → ℝ
f' g' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) s x

Tactic:
convert (hf.hasFDerivWithinAt.rpow hg.hasFDerivWithinAt h).hasDerivWithinAt using 1

Result:
case h.e'_9
f g : ℝ → ℝ
f' g' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    ((g x * f x ^ (g x - 1)) • ContinuousLinearMap.smulRight 1 f' +
        (f x ^ g x * Real.log (f x)) • ContinuousLinearMap.smulRight 1 g')
      1