harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (l : List γ) (l' : List δ) :
    map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l'

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
l' : List δ
⊢ map f (zipWith g (hd :: tl) l') = zipWith (fun x y => f (g x y)) (hd :: tl) l'

Tactic:
cases l'

Result:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
⊢ map f (zipWith g (hd :: tl) []) = zipWith (fun x y => f (g x y)) (hd :: tl) []

case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
head✝ : δ
tail✝ : List δ
⊢ map f (zipWith g (hd :: tl) (head✝ :: tail✝)) = zipWith (fun x y => f (g x y)) (hd :: tl) (head✝ :: tail✝)

Proof state:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
⊢ map f (zipWith g (hd :: tl) []) = zipWith (fun x y => f (g x y)) (hd :: tl) []

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
l' : List δ
⊢ map f (zipWith g [] l') = zipWith (fun x y => f (g x y)) [] l'

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
hd : γ
tl : List γ
hl : ∀ (l' : List δ), map f (zipWith g tl l') = zipWith (fun x y => f (g x y)) tl l'
head✝ : δ
tail✝ : List δ
⊢ map f (zipWith g (hd :: tl) (head✝ :: tail✝)) = zipWith (fun x y => f (g x y)) (hd :: tl) (head✝ :: tail✝)

Tactic:
simp [hl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_extract (as : Array α) (start stop : Nat) :
    (as.extract start stop).size = min stop as.size - start

Proof state:
α : Type u_1
as : Array α
start stop : Nat
⊢ (as.extract start stop).size = min stop as.size - start

Tactic:
simp only [extract, Nat.sub_eq, mkEmpty_eq]

Result:
α : Type u_1
as : Array α
start stop : Nat
⊢ (extract.loop as (min stop as.size - start) start #[]).size = min stop as.size - start

Proof state:
α : Type u_1
as : Array α
start stop : Nat
⊢ (extract.loop as (min stop as.size - start) start #[]).size = min stop as.size - start

Tactic:
rw [size_extract_loop, size_empty, Nat.zero_add, Nat.sub_min_sub_right, Nat.min_assoc,
  Nat.min_self]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/EssSurj.lean
private lemma functorToAction_map_quotientToEndObjectHom
    (m : SingleObj.star (V ⧸ Subgroup.subgroupOf U.toSubgroup V.toSubgroup) ⟶
      SingleObj.star (V ⧸ Subgroup.subgroupOf U.toSubgroup V.toSubgroup)) :
    (functorToAction F).map (quotientToEndObjectHom V h u m) =
      u.hom ≫ quotientToEndHom V.toSubgroup U.toSubgroup m ≫ u.inv

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
m : SingleObj.star (↥V ⧸ (↑U).subgroupOf ↑V) ⟶ SingleObj.star (↥V ⧸ (↑U).subgroupOf ↑V)
⊢ (functorToAction F).map ((CategoryTheory.PreGaloisCategory.quotientToEndObjectHom V h u) m) =
    u.hom ≫ (quotientToEndHom ↑V ↑U) m ≫ u.inv

Tactic:
simp [← cancel_epi u.inv, ← cancel_mono u.hom, ← Iso.conj_apply, quotientToEndObjectHom]

Result:
no goals
-- Mathlib/Order/SuccPred/LinearLocallyFinite.lean
theorem le_succFn (i : ι) : i ≤ succFn i

Proof state:
ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ ∀ x ∈ Set.Ioi i, i ≤ x

Tactic:
exact fun x hx ↦ le_of_lt hx

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ i ≤ succFn i

Tactic:
rw [le_isGLB_iff (succFn_spec i), mem_lowerBounds]

Result:
ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ ∀ x ∈ Set.Ioi i, i ≤ x
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
/-- A functor between preadditive categories that preserves (zero morphisms and) binary products
    preserves binary biproducts. -/
lemma preservesBinaryBiproduct_of_preservesBinaryProduct {X Y : C} [PreservesLimit (pair X Y) F] :
    PreservesBinaryBiproduct X Y F where
  preserves {b} hb := ⟨isBinaryBilimitOfIsLimit _ <| IsLimit.ofIsoLimit
          ((IsLimit.postcomposeHomEquiv (diagramIsoPair _) (F.mapCone b.toCone)).symm
            (isLimitOfPreserves F hb.isLimit)) <|
        Cones.ext (by dsimp; rfl) fun j => by
          rcases j with ⟨⟨⟩⟩ <;> simp⟩

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ F.obj b.pt ≅ F.obj b.pt

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).pt ≅
    (F.mapBinaryBicone b).toCone.pt

Tactic:
dsimp

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ F.obj b.pt ≅ F.obj b.pt

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app j =
    (id (Iso.refl (F.obj b.pt))).hom ≫ (F.mapBinaryBicone b).toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem MemLp.re (hf : MemLp f p μ) : MemLp (fun x => RCLike.re (f x)) p μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
⊢ ∀ (x : α), ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖

Tactic:
intro x

Result:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
⊢ MemLp (fun x => RCLike.re (f x)) p μ

Tactic:
have : ∀ x, ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖ := by
  intro x
  rw [one_mul]
  exact RCLike.norm_re_le_norm (f x)

Result:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖
⊢ MemLp (fun x => RCLike.re (f x)) p μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ ‖RCLike.re (f x)‖ ≤ ‖f x‖

Tactic:
exact RCLike.norm_re_le_norm (f x)

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖
⊢ AEStronglyMeasurable (fun x => RCLike.re (f x)) μ

Tactic:
exact RCLike.continuous_re.comp_aestronglyMeasurable hf.1

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖
⊢ MemLp (fun x => RCLike.re (f x)) p μ

Tactic:
refine hf.of_le_mul ?_ (Eventually.of_forall this)

Result:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖
⊢ AEStronglyMeasurable (fun x => RCLike.re (f x)) μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖

Tactic:
rw [one_mul]

Result:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ ‖RCLike.re (f x)‖ ≤ ‖f x‖
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_inter_left [DecidableEq α] (hf : Injective2 f) :
    image₂ f (s ∩ s') t = image₂ f s t ∩ image₂ f s' t :=
  coe_injective <| by
    push_cast
    exact image2_inter_left hf

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
hf : Injective2 f
⊢ image2 f (↑s ∩ ↑s') ↑t = image2 f ↑s ↑t ∩ image2 f ↑s' ↑t

Tactic:
exact image2_inter_left hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
hf : Injective2 f
⊢ ↑(image₂ f (s ∩ s') t) = ↑(image₂ f s t ∩ image₂ f s' t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
hf : Injective2 f
⊢ image2 f (↑s ∩ ↑s') ↑t = image2 f ↑s ↑t ∩ image2 f ↑s' ↑t
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem isUnit_inr_iff {m : M} : IsUnit (inr m : tsze R M) ↔ Subsingleton R

Proof state:
R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
m : M
⊢ IsUnit (inr m) ↔ Subsingleton R

Tactic:
simp_rw [isUnit_iff_isUnit_fst, fst_inr, isUnit_zero_iff, subsingleton_iff_zero_eq_one]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem conj_eq_re_sub_im (z : K) : conj z = re z - im z * I :=
  (congr_arg conj (re_add_im z).symm).trans <| by
    rw [map_add, map_mul, conj_I, conj_ofReal, conj_ofReal, mul_neg, sub_eq_add_neg]

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (starRingEnd K) (↑(re z) + ↑(im z) * I) = ↑(re z) - ↑(im z) * I

Tactic:
rw [map_add, map_mul, conj_I, conj_ofReal, conj_ofReal, mul_neg, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoUniformlyOn_singleton_iff_tendsto :
    TendstoUniformlyOn F f p {x} ↔ Tendsto (fun n : ι => F n x) p (𝓝 (f x))

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
⊢ (∀ s ∈ 𝓤 β, (fun q => (f q.2, F q.1 q.2)) ⁻¹' s ∈ p ×ˢ 𝓟 {x}) ↔ ∀ s ∈ 𝓤 β, (fun x_1 => (f x, F x_1 x)) ⁻¹' s ∈ p

Tactic:
exact forall₂_congr fun u _ => by simp [mem_prod_principal, preimage]

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
⊢ TendstoUniformlyOn F f p {x} ↔ Tendsto (fun n => F n x) p (𝓝 (f x))

Tactic:
simp_rw [tendstoUniformlyOn_iff_tendsto, Uniform.tendsto_nhds_right, tendsto_def]

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
⊢ (∀ s ∈ 𝓤 β, (fun q => (f q.2, F q.1 q.2)) ⁻¹' s ∈ p ×ˢ 𝓟 {x}) ↔ ∀ s ∈ 𝓤 β, (fun x_1 => (f x, F x_1 x)) ⁻¹' s ∈ p

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
u : Set (β × β)
x✝ : u ∈ 𝓤 β
⊢ (fun q => (f q.2, F q.1 q.2)) ⁻¹' u ∈ p ×ˢ 𝓟 {x} ↔ (fun x_1 => (f x, F x_1 x)) ⁻¹' u ∈ p

Tactic:
simp [mem_prod_principal, preimage]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
/-- The series `∑ z^n/n` converges to `-log (1-z)` on the open unit disk. -/
lemma hasSum_taylorSeries_neg_log {z : ℂ} (hz : ‖z‖ < 1) :
    HasSum (fun n : ℕ ↦ z ^ n / n) (-log (1 - z))

Proof state:
case h.e'_5.h.inr.hb
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ↑n ≠ 0

case h.e'_5.h.inr.hd
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ↑n ≠ 0

Tactic:
all_goals {norm_cast; exact hn.ne'}

Result:
no goals

Proof state:
case h.e'_5.h
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ -(z ^ n / ↑n) = (-1) ^ (n + 1) * (-z) ^ n / ↑n

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Result:
case h.e'_5.h.inl
z : ℂ
hz : ‖z‖ < 1
⊢ -(z ^ 0 / ↑0) = (-1) ^ (0 + 1) * (-z) ^ 0 / ↑0

case h.e'_5.h.inr
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ -(z ^ n / ↑n) = (-1) ^ (n + 1) * (-z) ^ n / ↑n

Proof state:
case h.e'_5.h.inr.hd
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ↑n ≠ 0

Tactic:
norm_cast

Result:
case h.e'_5.h.inr.hd
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ¬n = 0

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n => -(z ^ n / ↑n)) (log (1 - z))

Tactic:
convert hasSum_taylorSeries_log (z := -z) (norm_neg z ▸ hz) using 2 with n

Result:
case h.e'_5.h
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ -(z ^ n / ↑n) = (-1) ^ (n + 1) * (-z) ^ n / ↑n

Proof state:
case h.e'_5.h.inr.hd
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ¬n = 0

Tactic:
exact hn.ne'

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n => - -(z ^ n / ↑n)) (-log (1 - z))

Tactic:
refine HasSum.neg ?_

Result:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n => -(z ^ n / ↑n)) (log (1 - z))

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n => z ^ n / ↑n) (-log (1 - z))

Tactic:
conv => enter [1, n]; rw [← neg_neg (z ^ n / n)]

Result:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n => - -(z ^ n / ↑n)) (-log (1 - z))

Proof state:
case h.e'_5.h.inr
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ -z ^ n / ↑n = (-1) ^ (n + 1) * (-z) ^ n / ↑n

Tactic:
rw [div_eq_div_iff, pow_succ', mul_assoc (-1), ← mul_pow, neg_mul_neg, neg_one_mul, one_mul]

Result:
case h.e'_5.h.inr.hb
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ↑n ≠ 0

case h.e'_5.h.inr.hd
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ↑n ≠ 0

Proof state:
case h.e'_5.h.inl
z : ℂ
hz : ‖z‖ < 1
⊢ -(z ^ 0 / ↑0) = (-1) ^ (0 + 1) * (-z) ^ 0 / ↑0

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_5.h.inr
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ -(z ^ n / ↑n) = (-1) ^ (n + 1) * (-z) ^ n / ↑n

Tactic:
field_simp

Result:
case h.e'_5.h.inr
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ -z ^ n / ↑n = (-1) ^ (n + 1) * (-z) ^ n / ↑n
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem invOf_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸}
    (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) [Invertible (exp 𝕂 x)] :
    ⅟ (exp 𝕂 x) = exp 𝕂 (-x)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : CompleteSpace 𝔸
inst✝¹ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
inst✝ : Invertible (exp 𝕂 x)
this : Invertible (exp 𝕂 x) := invertibleExpOfMemBall hx
⊢ ⅟(exp 𝕂 x) = exp 𝕂 (-x)

Tactic:
convert (rfl : ⅟ (exp 𝕂 x) = _)

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : CompleteSpace 𝔸
inst✝¹ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
inst✝ : Invertible (exp 𝕂 x)
⊢ ⅟(exp 𝕂 x) = exp 𝕂 (-x)

Tactic:
letI := invertibleExpOfMemBall hx

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : CompleteSpace 𝔸
inst✝¹ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
inst✝ : Invertible (exp 𝕂 x)
this : Invertible (exp 𝕂 x) := invertibleExpOfMemBall hx
⊢ ⅟(exp 𝕂 x) = exp 𝕂 (-x)
-- Mathlib/Topology/Order/Basic.lean
theorem tendsto_order_unbounded [OrderTopology α] {f : β → α} {a : α} {x : Filter β}
    (hu : ∃ u, a < u) (hl : ∃ l, l < a) (h : ∀ l u, l < a → a < u → ∀ᶠ b in x, l < f b ∧ f b < u) :
    Tendsto f x (𝓝 a)

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
f : β → α
a : α
x : Filter β
hu : ∃ u, a < u
hl : ∃ l, l < a
h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u
⊢ Tendsto f x (𝓝 a)

Tactic:
simp only [nhds_order_unbounded hu hl, tendsto_iInf, tendsto_principal]

Result:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
f : β → α
a : α
x : Filter β
hu : ∃ u, a < u
hl : ∃ l, l < a
h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u
⊢ ∀ i < a, ∀ (i_2 : α), a < i_2 → ∀ᶠ (a : β) in x, f a ∈ Ioo i i_2

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
f : β → α
a : α
x : Filter β
hu : ∃ u, a < u
hl : ∃ l, l < a
h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u
⊢ ∀ i < a, ∀ (i_2 : α), a < i_2 → ∀ᶠ (a : β) in x, f a ∈ Ioo i i_2

Tactic:
exact fun l hl u => h l u hl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
lemma hasCardinalLT_iff_cardinal_mk_lt (X : Type u) (κ : Cardinal.{u}) :
    HasCardinalLT X κ ↔ Cardinal.mk X < κ

Proof state:
X : Type u
κ : Cardinal.{u}
⊢ HasCardinalLT X κ ↔ Cardinal.mk X < κ

Tactic:
simp [HasCardinalLT]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem perfect_iff_sum_divisors_eq_two_mul (h : 0 < n) :
    Perfect n ↔ ∑ i ∈ divisors n, i = 2 * n

Proof state:
n : ℕ
h : 0 < n
⊢ n.Perfect ↔ ∑ i ∈ n.divisors, i = 2 * n

Tactic:
rw [perfect_iff_sum_properDivisors h, sum_divisors_eq_sum_properDivisors_add_self, two_mul]

Result:
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.properDivisors, i + n = n + n

Proof state:
case mp
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i = n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n

Tactic:
rw [h]

Result:
no goals

Proof state:
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.properDivisors, i + n = n + n

Tactic:
constructor <;> intro h

Result:
case mp
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i = n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n

case mpr
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i + n = n + n
⊢ ∑ i ∈ n.properDivisors, i = n

Proof state:
case mpr
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i + n = n + n
⊢ ∑ i ∈ n.properDivisors, i = n

Tactic:
apply add_right_cancel h

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean
lemma directLimitLeft_rTensor_of {i : ι} (x : G i ⊗[R] M) :
    directLimitLeft f M (LinearMap.rTensor M (of ..) x) = of _ _ _ (f ▷ M) _ x :=
  x.induction_on (by simp) (by simp+contextual) (by simp+contextual)

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
x : G i ⊗[R] M
⊢ ∀ (x y : G i ⊗[R] M),
    (directLimitLeft f M) ((LinearMap.rTensor M (of R ι G f i)) x) =
        (of R ι (fun i => G i ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) x →
      (directLimitLeft f M) ((LinearMap.rTensor M (of R ι G f i)) y) =
          (of R ι (fun i => G i ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) y →
        (directLimitLeft f M) ((LinearMap.rTensor M (of R ι G f i)) (x + y)) =
          (of R ι (fun i => G i ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) (x + y)

Tactic:
simp+contextual

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
x : G i ⊗[R] M
⊢ ∀ (x : G i) (y : M),
    (directLimitLeft f M) ((LinearMap.rTensor M (of R ι G f i)) (x ⊗ₜ[R] y)) =
      (of R ι (fun i => G i ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) (x ⊗ₜ[R] y)

Tactic:
simp+contextual

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
x : G i ⊗[R] M
⊢ (directLimitLeft f M) ((LinearMap.rTensor M (of R ι G f i)) 0) =
    (of R ι (fun i => G i ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
@[simp] lemma get_append_right : (x ++ₛ a).get (x.length + n) = a.get n

Proof state:
α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ (x ++ₛ a).get (x.length + n) = a.get n

Tactic:
induction' x <;> simp [Nat.succ_add, *, cons_append_stream]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem data_dropWhile (p) : ∀ {s}, Valid s →
    (s.dropWhile p).toString.1 = s.toString.1.dropWhile p
  | _, h => let ⟨_, _, _, h⟩ := h.validFor; by simp [(h.dropWhile _).toString, h.toString]

Proof state:
p : Char → Bool
x✝ : Substring
h✝ : x✝.Valid
w✝² w✝¹ w✝ : List Char
h : ValidFor w✝² w✝¹ w✝ x✝
⊢ (x✝.dropWhile p).toString.data = List.dropWhile p x✝.toString.data

Tactic:
simp [(h.dropWhile _).toString, h.toString]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_eq_nat_iff_fintype {n : ℕ} : #α = n ↔ ∃ h : Fintype α, @Fintype.card α h = n

Proof state:
case mpr.intro.mk
α : Type u
n : ℕ
t : Finset α
ht : ∀ (x : α), x ∈ t
hn : Fintype.card α = n
⊢ ∃ t, ↑t = univ ∧ t.card = n

Tactic:
exact ⟨t, eq_univ_iff_forall.2 ht, hn⟩

Result:
no goals

Proof state:
case mpr
α : Type u
n : ℕ
⊢ (∃ h, Fintype.card α = n) → ∃ t, ↑t = univ ∧ t.card = n

Tactic:
rintro ⟨⟨t, ht⟩, hn⟩

Result:
case mpr.intro.mk
α : Type u
n : ℕ
t : Finset α
ht : ∀ (x : α), x ∈ t
hn : Fintype.card α = n
⊢ ∃ t, ↑t = univ ∧ t.card = n

Proof state:
case mp.intro.intro
α : Type u
n : ℕ
t : Finset α
ht : ↑t = univ
hn : t.card = n
⊢ ∃ h, Fintype.card α = n

Tactic:
exact ⟨⟨t, eq_univ_iff_forall.1 ht⟩, hn⟩

Result:
no goals

Proof state:
case mp
α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) → ∃ h, Fintype.card α = n

Tactic:
rintro ⟨t, ht, hn⟩

Result:
case mp.intro.intro
α : Type u
n : ℕ
t : Finset α
ht : ↑t = univ
hn : t.card = n
⊢ ∃ h, Fintype.card α = n

Proof state:
α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) ↔ ∃ h, Fintype.card α = n

Tactic:
constructor

Result:
case mp
α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) → ∃ h, Fintype.card α = n

case mpr
α : Type u
n : ℕ
⊢ (∃ h, Fintype.card α = n) → ∃ t, ↑t = univ ∧ t.card = n

Proof state:
α : Type u
n : ℕ
⊢ #α = ↑n ↔ ∃ h, Fintype.card α = n

Tactic:
rw [mk_eq_nat_iff_finset]

Result:
α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) ↔ ∃ h, Fintype.card α = n
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem inv_mul_mul_self (a : G₀) : a⁻¹ * a * a = a

Proof state:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ a⁻¹ * a * a = a

Tactic:
rw [h, inv_zero, mul_zero]

Result:
no goals

Proof state:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a⁻¹ * a * a = a

Tactic:
rw [inv_mul_cancel₀ h, one_mul]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a⁻¹ * a * a = a

Tactic:
by_cases h : a = 0

Result:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ a⁻¹ * a * a = a

case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a⁻¹ * a * a = a
-- Mathlib/Order/Filter/Lift.lean
theorem comap_lift_eq {m : γ → β} : comap m (f.lift g) = f.lift (comap m ∘ g)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
⊢ comap m (f.lift g) = f.lift (comap m ∘ g)

Tactic:
simp only [Filter.lift, comap_iInf]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
⊢ ⨅ i ∈ f, comap m (g i) = ⨅ s ∈ f, (comap m ∘ g) s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
⊢ ⨅ i ∈ f, comap m (g i) = ⨅ s ∈ f, (comap m ∘ g) s

Tactic:
rfl

Result:
no goals