harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/Block.lean
lemma Matrix.comp_diagonal (d) :
    comp m m n n R (diagonal d) =
      (blockDiagonal d).reindex (.prodComm ..) (.prodComm ..)

Proof state:
m : Type u_2
n : Type u_3
R : Type u_14
inst✝¹ : Zero R
inst✝ : DecidableEq m
d : m → Matrix n n R
⊢ (comp m m n n R) (diagonal d) = (reindex (Equiv.prodComm n m) (Equiv.prodComm n m)) (blockDiagonal d)

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
R : Type u_14
inst✝¹ : Zero R
inst✝ : DecidableEq m
d : m → Matrix n n R
i✝ j✝ : m × n
⊢ (comp m m n n R) (diagonal d) i✝ j✝ = (reindex (Equiv.prodComm n m) (Equiv.prodComm n m)) (blockDiagonal d) i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
R : Type u_14
inst✝¹ : Zero R
inst✝ : DecidableEq m
d : m → Matrix n n R
i✝ j✝ : m × n
⊢ (comp m m n n R) (diagonal d) i✝ j✝ = (reindex (Equiv.prodComm n m) (Equiv.prodComm n m)) (blockDiagonal d) i✝ j✝

Tactic:
simp [diagonal, blockDiagonal, Matrix.ite_apply]

Result:
no goals
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom :
    (singleObjHomologySelfIso _ _ _).hom ≫ (singleObjOpcyclesSelfIso _ _ _).hom =
      ((single C c j).obj A).homologyι j

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ (singleObjHomologySelfIso c j A).hom ≫ (singleObjOpcyclesSelfIso c j A).hom = ((single C c j).obj A).homologyι j

Tactic:
rw [← cancel_epi (singleObjHomologySelfIso _ _ _).inv,
  Iso.inv_hom_id_assoc, singleObjHomologySelfIso_inv_homologyι]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le'
    [CompleteSpace E] [IsMeasurablyGenerated l']
    [TendstoIxxClass Ioc l l'] (hfm : StronglyMeasurableAtFilter f l' μ)
    (hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)) (hl : μ.FiniteAtFilter l') (hu : Tendsto u lt l)
    (hv : Tendsto v lt l) (huv : u ≤ᶠ[lt] v) :
    (fun t => (∫ x in u t..v t, f x ∂μ) - (μ (Ioc (u t) (v t))).toReal • c) =o[lt] fun t =>
      (μ <| Ioc (u t) (v t)).toReal :=
  (measure_integral_sub_linear_isLittleO_of_tendsto_ae' hfm hf hl hu hv).congr'
    (huv.mono fun x hx => by simp [integral_const', hx])
    (huv.mono fun x hx => by simp [integral_const', hx])

Proof state:
ι : Type u_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝² : CompleteSpace E
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
huv : u ≤ᶠ[lt] v
x : ι
hx : u x ≤ v x
⊢ (fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ) x = (fun t => (μ (Ioc (u t) (v t))).toReal) x

Tactic:
simp [integral_const', hx]

Result:
no goals

Proof state:
ι : Type u_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝² : CompleteSpace E
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
huv : u ≤ᶠ[lt] v
x : ι
hx : u x ≤ v x
⊢ (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) x =
    (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ (Ioc (u t) (v t))).toReal • c) x

Tactic:
simp [integral_const', hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem neg_mul_eq_mul_neg (a b : Int) : -(a * b) = a * -b :=
  Int.neg_eq_of_add_eq_zero <| by rw [← Int.mul_add, Int.add_right_neg, Int.mul_zero]

Proof state:
a b : Int
⊢ a * b + a * -b = 0

Tactic:
rw [← Int.mul_add, Int.add_right_neg, Int.mul_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Function/Floor.lean
theorem Int.measurable_floor [OpensMeasurableSpace R] : Measurable (Int.floor : R → ℤ) :=
  measurable_to_countable fun x => by
    simpa only [Int.preimage_floor_singleton] using measurableSet_Ico

Proof state:
R : Type u_2
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
x : R
⊢ MeasurableSet (floor ⁻¹' {⌊x⌋})

Tactic:
simpa only [Int.preimage_floor_singleton] using measurableSet_Ico

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem embDomain_notin_range (f : α ↪ β) (v : α →₀ M) (a : β) (h : a ∉ Set.range f) :
    embDomain f v a = 0

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ (embDomain f v) a = 0

Tactic:
classical
  refine dif_neg (mt (fun h => ?_) h)
  rcases Finset.mem_map.1 h with ⟨a, _h, rfl⟩
  exact Set.mem_range_self a

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
_h : a ∈ v.support
h✝ : f a ∉ Set.range ⇑f
h : f a ∈ map f v.support
⊢ f a ∈ Set.range ⇑f

Tactic:
exact Set.mem_range_self a

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ (embDomain f v) a = 0

Tactic:
refine dif_neg (mt (fun h => ?_) h)

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : β
h✝ : a ∉ Set.range ⇑f
h : a ∈ map f v.support
⊢ a ∈ Set.range ⇑f

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : β
h✝ : a ∉ Set.range ⇑f
h : a ∈ map f v.support
⊢ a ∈ Set.range ⇑f

Tactic:
rcases Finset.mem_map.1 h with ⟨a, _h, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
_h : a ∈ v.support
h✝ : f a ∉ Set.range ⇑f
h : f a ∈ map f v.support
⊢ f a ∈ Set.range ⇑f
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem restrict_le_restrict_of_subset_le {i : Set α}
    (h : ∀ ⦃j⦄, MeasurableSet j → j ⊆ i → v j ≤ w j) : v ≤[i] w

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑w j
hi : ¬MeasurableSet i
⊢ v ≤[i] w

Tactic:
rw [restrict_not_measurable v hi, restrict_not_measurable w hi]

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑w j
hi : MeasurableSet i
⊢ v ≤[i] w

Tactic:
exact (restrict_le_restrict_iff _ _ hi).2 h

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑w j
⊢ v ≤[i] w

Tactic:
by_cases hi : MeasurableSet i

Result:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑w j
hi : MeasurableSet i
⊢ v ≤[i] w

case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑w j
hi : ¬MeasurableSet i
⊢ v ≤[i] w
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem isRadical_iff_squarefree_or_zero : IsRadical x ↔ Squarefree x ∨ x = 0 :=
  ⟨fun hx ↦ (em <| x = 0).elim .inr fun h ↦ .inl <| hx.squarefree h,
    Or.rec Squarefree.isRadical <| by
      rintro rfl
      rw [zero_isRadical_iff]
      infer_instance⟩

Proof state:
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x : R
inst✝ : DecompositionMonoid R
⊢ x = 0 → IsRadical x

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : DecompositionMonoid R
⊢ IsRadical 0

Proof state:
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : DecompositionMonoid R
⊢ IsRadical 0

Tactic:
rw [zero_isRadical_iff]

Result:
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : DecompositionMonoid R
⊢ IsReduced R

Proof state:
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : DecompositionMonoid R
⊢ IsReduced R

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
lemma IsDynCoverOf.image (h : Semiconj φ S T) {F : Set X} {V : Set (Y × Y)} {n : ℕ} {s : Set X}
    (h' : IsDynCoverOf S F ((map φ φ) ⁻¹' V) n s) :
    IsDynCoverOf T (φ '' F) V n (φ '' s)

Proof state:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
s : Set X
h' : IsDynCoverOf S F (map φ φ ⁻¹' V) n s
⊢ F ⊆ ⋃ i ∈ s, φ ⁻¹' ball (φ i) (dynEntourage T V n)

Tactic:
refine h'.trans (iUnion₂_mono fun i _ ↦ subset_of_eq ?_)

Result:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
s : Set X
h' : IsDynCoverOf S F (map φ φ ⁻¹' V) n s
i : X
x✝ : i ∈ s
⊢ ball i (dynEntourage S (map φ φ ⁻¹' V) n) = φ ⁻¹' ball (φ i) (dynEntourage T V n)

Proof state:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
s : Set X
h' : IsDynCoverOf S F (map φ φ ⁻¹' V) n s
⊢ IsDynCoverOf T (φ '' F) V n (φ '' s)

Tactic:
simp only [IsDynCoverOf, image_subset_iff, preimage_iUnion₂, biUnion_image]

Result:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
s : Set X
h' : IsDynCoverOf S F (map φ φ ⁻¹' V) n s
⊢ F ⊆ ⋃ i ∈ s, φ ⁻¹' ball (φ i) (dynEntourage T V n)

Proof state:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
s : Set X
h' : IsDynCoverOf S F (map φ φ ⁻¹' V) n s
i : X
x✝ : i ∈ s
⊢ ball i (dynEntourage S (map φ φ ⁻¹' V) n) = φ ⁻¹' ball (φ i) (dynEntourage T V n)

Tactic:
rw [← h.preimage_dynEntourage V n, ball_preimage]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_cos {x : ℝ} (hx₁ : 0 ≤ x) (hx₂ : x ≤ π) : arccos (cos x) = x

Proof state:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ arccos (cos x) = x

Tactic:
rw [arccos, ← sin_pi_div_two_sub, arcsin_sin] <;> simp [sub_eq_add_neg] <;> linarith

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_right_eq_self {x y : Array α} : x ++ y = x ↔ y = #[]

Proof state:
α : Type u_1
x y : Array α
⊢ x ++ y = x ↔ y = #[]

Tactic:
rw [← append_right_inj (t₁ := y), append_empty]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/WithTop.lean
lemma mul_eq_bot_iff : a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
⊢ (if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 => x1 * x2) a b) = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
⊢ a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0

Tactic:
rw [mul_def]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
⊢ (if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 => x1 * x2) a b) = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0
-- Mathlib/NumberTheory/EulerProduct/Basic.lean
theorem eulerProduct_completely_multiplicative_hasProd {f : ℕ →*₀ F} (hsum : Summable (‖f ·‖)) :
    HasProd (fun p : Primes ↦ (1 - f p)⁻¹) (∑' n, f n)

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x => ‖f x‖
⊢ HasProd (fun p => (1 - f ↑p)⁻¹) (∑' (n : ℕ), f n)

Tactic:
have H : (fun p : Primes ↦ (1 - f p)⁻¹) = fun p : Primes ↦ ∑' (e : ℕ), f (p ^ e) :=
  funext <| fun p ↦ one_sub_inv_eq_geometric_of_summable_norm p.prop hsum

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x => ‖f x‖
H : (fun p => (1 - f ↑p)⁻¹) = fun p => ∑' (e : ℕ), f (↑p ^ e)
⊢ HasProd (fun p => (1 - f ↑p)⁻¹) (∑' (n : ℕ), f n)

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x => ‖f x‖
H : (fun p => (1 - f ↑p)⁻¹) = fun p => ∑' (e : ℕ), f (↑p ^ e)
⊢ HasProd (fun p => (1 - f ↑p)⁻¹) (∑' (n : ℕ), f n)

Tactic:
simpa only [map_pow, H]
  using eulerProduct_hasProd f.map_one (fun {m n} _ ↦ f.map_mul m n) hsum f.map_zero

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem EventuallyLE.congr {f f' g g' : α → β} (H : f ≤ᶠ[l] g) (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
    f' ≤ᶠ[l] g' :=
  H.mp <| hg.mp <| hf.mono fun x hf hg H => by rwa [hf, hg] at H

Proof state:
α : Type u
β : Type v
inst✝ : LE β
l : Filter α
f f' g g' : α → β
H✝ : f ≤ᶠ[l] g
hf✝ : f =ᶠ[l] f'
hg✝ : g =ᶠ[l] g'
x : α
hf : f x = f' x
hg : g x = g' x
H : f x ≤ g x
⊢ f' x ≤ g' x

Tactic:
rwa [hf, hg] at H

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
lemma liminf_top_eq_ciInf [Nonempty β] (hu : BddBelow (range u)) : liminf u ⊤ = ⨅ i, u i

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddBelow (range u)
⊢ liminf u ⊤ = ⨅ i, u i

Tactic:
rw [liminf, map_top, limsInf_principal_eq_csSup hu (range_nonempty _), sInf_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem unzip_zip {l₁ : List α} {l₂ : List β} (h : length l₁ = length l₂) :
    unzip (zip l₁ l₂) = (l₁, l₂)

Proof state:
case snd.h.a
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
h : l₁.length = l₂.length
i✝ : Nat
a✝ : β
⊢ a✝ ∈ (l₁.zip l₂).unzip.snd[i✝]? ↔ a✝ ∈ (l₁, l₂).snd[i✝]?

Tactic:
rw [unzip_zip_right (Nat.le_of_eq h.symm)]

Result:
no goals

Proof state:
case fst.h.a
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
h : l₁.length = l₂.length
i✝ : Nat
a✝ : α
⊢ a✝ ∈ (l₁.zip l₂).unzip.fst[i✝]? ↔ a✝ ∈ (l₁, l₂).fst[i✝]?

Tactic:
rw [unzip_zip_left (Nat.le_of_eq h)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
h : l₁.length = l₂.length
⊢ (l₁.zip l₂).unzip = (l₁, l₂)

Tactic:
ext

Result:
case fst.h.a
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
h : l₁.length = l₂.length
i✝ : Nat
a✝ : α
⊢ a✝ ∈ (l₁.zip l₂).unzip.fst[i✝]? ↔ a✝ ∈ (l₁, l₂).fst[i✝]?

case snd.h.a
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
h : l₁.length = l₂.length
i✝ : Nat
a✝ : β
⊢ a✝ ∈ (l₁.zip l₂).unzip.snd[i✝]? ↔ a✝ ∈ (l₁, l₂).snd[i✝]?
-- Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean
@[to_additive]
lemma inv_hom_apply {A B : ProfiniteGrp.{u}} (e : A ≅ B) (x : A) : e.inv (e.hom x) = x

Proof state:
A B : ProfiniteGrp.{u}
e : A ≅ B
x : ↑A.toProfinite.toTop
⊢ (Hom.hom e.inv) ((Hom.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem angle_eq_iff_oangle_eq_of_sign_eq {w x y z : V} (hw : w ≠ 0) (hx : x ≠ 0) (hy : y ≠ 0)
    (hz : z ≠ 0) (hs : (o.oangle w x).sign = (o.oangle y z).sign) :
    InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔
    o.oangle w x = o.oangle y z

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle y z).sign
h : o.oangle w x = o.oangle y z
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z

Tactic:
rw [o.angle_eq_abs_oangle_toReal hw hx, o.angle_eq_abs_oangle_toReal hy hz, h]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle y z).sign
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle y z

Tactic:
refine ⟨fun h => o.oangle_eq_of_angle_eq_of_sign_eq h hs, fun h => ?_⟩

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle y z).sign
h : o.oangle w x = o.oangle y z
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
theorem zeta_eq_tsum_one_div_nat_add_one_cpow {s : ℂ} (hs : 1 < re s) :
    riemannZeta s = ∑' n : ℕ, 1 / (n + 1 : ℂ) ^ s

Proof state:
s : ℂ
hs : 1 < s.re
this : riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s
⊢ Summable fun n => 1 / ↑n ^ s

Tactic:
rwa [Complex.summable_one_div_nat_cpow]

Result:
no goals

Proof state:
s : ℂ
hs : 1 < s.re
this : riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s
⊢ riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s

Tactic:
rw [tsum_eq_zero_add] at this

Result:
s : ℂ
hs : 1 < s.re
this : riemannZeta s = 1 / ↑0 ^ s + ∑' (b : ℕ), 1 / ↑(b + 1) ^ s
⊢ riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s

s : ℂ
hs : 1 < s.re
this : riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s
⊢ Summable fun n => 1 / ↑n ^ s

Proof state:
s : ℂ
hs : 1 < s.re
⊢ riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s

Tactic:
have := zeta_eq_tsum_one_div_nat_cpow hs

Result:
s : ℂ
hs : 1 < s.re
this : riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s
⊢ riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s

Proof state:
s : ℂ
hs : 1 < s.re
this : riemannZeta s = 1 / ↑0 ^ s + ∑' (b : ℕ), 1 / ↑(b + 1) ^ s
⊢ riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s

Tactic:
simpa [zero_cpow (Complex.ne_zero_of_one_lt_re hs)]

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem IsConnected.iUnion_of_chain [Nonempty β] {s : β → Set α} (H : ∀ n, IsConnected (s n))
    (K : ∀ n, (s n ∩ s (succ n)).Nonempty) : IsConnected (⋃ n, s n) :=
  IsConnected.iUnion_of_reflTransGen H fun _ _ =>
    reflTransGen_of_succ _ (fun i _ => K i) fun i _ => by
      rw [inter_comm]
      exact K i

Proof state:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder β
inst✝² : SuccOrder β
inst✝¹ : IsSuccArchimedean β
inst✝ : Nonempty β
s : β → Set α
H : ∀ (n : β), IsConnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x✝² x✝¹ i : β
x✝ : i ∈ Ico x✝¹ x✝²
⊢ (s i ∩ s (succ i)).Nonempty

Tactic:
exact K i

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder β
inst✝² : SuccOrder β
inst✝¹ : IsSuccArchimedean β
inst✝ : Nonempty β
s : β → Set α
H : ∀ (n : β), IsConnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x✝² x✝¹ i : β
x✝ : i ∈ Ico x✝¹ x✝²
⊢ (s (succ i) ∩ s i).Nonempty

Tactic:
rw [inter_comm]

Result:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder β
inst✝² : SuccOrder β
inst✝¹ : IsSuccArchimedean β
inst✝ : Nonempty β
s : β → Set α
H : ∀ (n : β), IsConnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x✝² x✝¹ i : β
x✝ : i ∈ Ico x✝¹ x✝²
⊢ (s i ∩ s (succ i)).Nonempty
-- Mathlib/Computability/Primrec.lean
theorem option_get {f : α → Option β} {h : ∀ a, (f a).isSome} :
    Primrec f → Primrec fun a => (f a).get (h a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
⊢ Primrec fun a => (f a).get ⋯

Tactic:
refine (Nat.Primrec.pred.comp hf).of_eq fun n => ?_

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
⊢ (encode (Option.map f (decode n))).pred = encode (Option.map (fun a => (f a).get ⋯) (decode n))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
⊢ (encode (Option.map f (decode n))).pred = encode (Option.map (fun a => (f a).get ⋯) (decode n))

Tactic:
generalize hx : @decode α _ n = x

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
x : Option α
hx : decode n = x
⊢ (encode (Option.map f x)).pred = encode (Option.map (fun a => (f a).get ⋯) x)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
x : Option α
hx : decode n = x
⊢ (encode (Option.map f x)).pred = encode (Option.map (fun a => (f a).get ⋯) x)

Tactic:
cases x <;> simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
⊢ Primrec f → Primrec fun a => (f a).get ⋯

Tactic:
intro hf

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
⊢ Primrec fun a => (f a).get ⋯
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right (g : G ≃ₗᵢ[𝕜] E) (f : E → F)
    (hs : UniqueDiffOn 𝕜 s) {x : G} (hx : g x ∈ s) (i : ℕ) :
    ‖iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : g x ∈ s
i : ℕ
⊢ ‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖

Tactic:
have : iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s) x =
    (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun _ => g :=
  g.toContinuousLinearEquiv.iteratedFDerivWithin_comp_right f hs hx i

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : g x ∈ s
i : ℕ
this :
  iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
    (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x =>
      ↑{ toLinearEquiv := g.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ ‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : g x ∈ s
i : ℕ
this :
  iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
    (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x =>
      ↑{ toLinearEquiv := g.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ ‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖

Tactic:
rw [this, ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem Filter.tendsto_nhds_max_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝[>] a)) :
    Tendsto (fun i => max a (f i)) l (𝓝[>] a)

Proof state:
case intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
h₁ : Tendsto f l (𝓝 a)
h₂ : ∀ᶠ (i : β) in l, f i ∈ Ioi a
⊢ Tendsto (fun i => a ⊔ f i) l (𝓝[>] a)

Tactic:
exact tendsto_nhdsWithin_iff.mpr ⟨h₁.max_right, h₂.mono fun i hi => lt_max_of_lt_right hi⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
⊢ Tendsto (fun i => a ⊔ f i) l (𝓝[>] a)

Tactic:
obtain ⟨h₁ : Tendsto f l (𝓝 a), h₂ : ∀ᶠ i in l, f i ∈ Ioi a⟩ := tendsto_nhdsWithin_iff.mp h

Result:
case intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
h₁ : Tendsto f l (𝓝 a)
h₂ : ∀ᶠ (i : β) in l, f i ∈ Ioi a
⊢ Tendsto (fun i => a ⊔ f i) l (𝓝[>] a)