harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoUniformly_iff_seq_tendstoUniformly {l : Filter ι} [l.IsCountablyGenerated] :
    TendstoUniformly F f l ↔
      ∀ u : ℕ → ι, Tendsto u atTop l → TendstoUniformly (fun n => F (u n)) f atTop

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
l : Filter ι
inst✝ : l.IsCountablyGenerated
⊢ TendstoUniformly F f l ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformly (fun n => F (u n)) f atTop

Tactic:
simp_rw [← tendstoUniformlyOn_univ]

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
l : Filter ι
inst✝ : l.IsCountablyGenerated
⊢ TendstoUniformlyOn F f l univ ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop univ

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
l : Filter ι
inst✝ : l.IsCountablyGenerated
⊢ TendstoUniformlyOn F f l univ ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop univ

Tactic:
exact tendstoUniformlyOn_iff_seq_tendstoUniformlyOn

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem mapId_eq (Y : T) : map (𝟙 Y) = 𝟭 _

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x y : Under Y
u : x ⟶ y
⊢ (map (𝟙 Y)).map u = eqToHom ⋯ ≫ (𝟭 (Under Y)).map u ≫ eqToHom ⋯

Tactic:
dsimp [Under, Under.map, Comma.mapLeft]

Result:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x y : Under Y
u : x ⟶ y
⊢ { left := 𝟙 x.left, right := u.right, w := ⋯ } = eqToHom ⋯ ≫ u ≫ eqToHom ⋯

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
⊢ ∀ (X : Under Y), (map (𝟙 Y)).obj X = (𝟭 (Under Y)).obj X

Tactic:
intro x

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x : Under Y
⊢ (map (𝟙 Y)).obj x = (𝟭 (Under Y)).obj x

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x : Under Y
⊢ { left := x.left, right := x.right, hom := 𝟙 Y ≫ x.hom } = x

Tactic:
simp only [Category.id_comp]

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x : Under Y
⊢ { left := x.left, right := x.right, hom := x.hom } = x

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x : Under Y
⊢ { left := x.left, right := x.right, hom := x.hom } = x

Tactic:
exact rfl

Result:
no goals

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x : Under Y
⊢ (map (𝟙 Y)).obj x = (𝟭 (Under Y)).obj x

Tactic:
dsimp [Under, Under.map, Comma.mapLeft]

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x : Under Y
⊢ { left := x.left, right := x.right, hom := 𝟙 Y ≫ x.hom } = x

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
⊢ map (𝟙 Y) = 𝟭 (Under Y)

Tactic:
fapply Functor.ext

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
⊢ ∀ (X : Under Y), (map (𝟙 Y)).obj X = (𝟭 (Under Y)).obj X

case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
⊢ autoParam (∀ (X Y_1 : Under Y) (f : X ⟶ Y_1), (map (𝟙 Y)).map f = eqToHom ⋯ ≫ (𝟭 (Under Y)).map f ≫ eqToHom ⋯) _auto✝

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x y : Under Y
u : x ⟶ y
⊢ { left := 𝟙 x.left, right := u.right, w := ⋯ } = eqToHom ⋯ ≫ u ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
⊢ autoParam (∀ (X Y_1 : Under Y) (f : X ⟶ Y_1), (map (𝟙 Y)).map f = eqToHom ⋯ ≫ (𝟭 (Under Y)).map f ≫ eqToHom ⋯) _auto✝

Tactic:
intros x y u

Result:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x y : Under Y
u : x ⟶ y
⊢ (map (𝟙 Y)).map u = eqToHom ⋯ ≫ (𝟭 (Under Y)).map u ≫ eqToHom ⋯
-- Mathlib/Probability/CDF.lean
lemma cdf_eq_toReal [IsProbabilityMeasure μ] (x : ℝ) : cdf μ x = (μ (Iic x)).toReal

Proof state:
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
⊢ ↑(cdf μ) x = (μ (Iic x)).toReal

Tactic:
rw [← ofReal_cdf μ x, ENNReal.toReal_ofReal (cdf_nonneg μ x)]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem algebraMap_mem (r : R) : algebraMap R A r ∈ (1 : Submodule R A)

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (algebraMap R A) r ∈ 1

Tactic:
simp [one_eq_range]

Result:
no goals
-- Mathlib/Algebra/Group/WithOne/Basic.lean
theorem map_map (f : α →ₙ* β) (g : β →ₙ* γ) (x) : map g (map f x) = map (g.comp f) x

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
x : WithOne α
⊢ (map g) ((map f) x) = (map (g.comp f)) x

Tactic:
induction x <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem extractLsb'_not_of_lt {x : BitVec w} {start len : Nat} (h : start + len < w) :
   (~~~ x).extractLsb' start len = ~~~ (x.extractLsb' start len)

Proof state:
case pred
w : Nat
x : BitVec w
start len : Nat
h : start + len < w
i : Nat
hi : i < len
⊢ x.getLsbD (start + i) = false → start + i < w

Tactic:
omega

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
start len : Nat
h : start + len < w
i : Nat
hi : i < len
⊢ (extractLsb' start len (~~~x)).getLsbD i = (~~~extractLsb' start len x).getLsbD i

Tactic:
simp [hi]

Result:
case pred
w : Nat
x : BitVec w
start len : Nat
h : start + len < w
i : Nat
hi : i < len
⊢ x.getLsbD (start + i) = false → start + i < w

Proof state:
w : Nat
x : BitVec w
start len : Nat
h : start + len < w
⊢ extractLsb' start len (~~~x) = ~~~extractLsb' start len x

Tactic:
ext i hi

Result:
case pred
w : Nat
x : BitVec w
start len : Nat
h : start + len < w
i : Nat
hi : i < len
⊢ (extractLsb' start len (~~~x)).getLsbD i = (~~~extractLsb' start len x).getLsbD i
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_sum_compl {α} (s : Set α) : #s + #(sᶜ : Set α) = #α

Proof state:
α : Type u_1
s : Set α
⊢ #↑s + #↑sᶜ = #α

Tactic:
classical
exact mk_congr (Equiv.Set.sumCompl s)

Result:
no goals

Proof state:
α : Type u_1
s : Set α
⊢ #↑s + #↑sᶜ = #α

Tactic:
exact mk_congr (Equiv.Set.sumCompl s)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_flatMap (l : Array α) (f : α → Array β) :
    (l.flatMap f).toList = l.toList.flatMap fun a => (f a).toList

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
l : List α
⊢ (flatMap f { toList := l }).toList = List.flatMap (fun a => (f a).toList) { toList := l }.toList

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → Array β
⊢ (flatMap f l).toList = List.flatMap (fun a => (f a).toList) l.toList

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
l : List α
⊢ (flatMap f { toList := l }).toList = List.flatMap (fun a => (f a).toList) { toList := l }.toList
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem isRoot_prod {R} [CommRing R] [IsDomain R] {ι : Type*} (s : Finset ι) (p : ι → R[X])
    (x : R) : IsRoot (∏ j ∈ s, p j) x ↔ ∃ i ∈ s, IsRoot (p i) x

Proof state:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
ι : Type u_1
s : Finset ι
p : ι → R[X]
x : R
⊢ (∏ j ∈ s, p j).IsRoot x ↔ ∃ i ∈ s, (p i).IsRoot x

Tactic:
simp only [IsRoot, eval_prod, Finset.prod_eq_zero_iff]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem invApp_app (U : Opens X) :
    H.invApp _ U ≫ f.c.app (op (opensFunctor f |>.obj U)) = X.presheaf.map
      (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective])) :=
  PresheafedSpace.IsOpenImmersion.invApp_app f U

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X.toPresheafedSpace
⊢ op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))

Tactic:
simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem neg (a : ℤ) {b : ℕ} (hb : Odd b) : J(-a | b) = χ₄ b * J(a | b)

Proof state:
a : ℤ
b : ℕ
hb : Odd b
⊢ J(-a | b) = χ₄ ↑b * J(a | b)

Tactic:
rw [neg_eq_neg_one_mul, mul_left, at_neg_one hb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem guard_isSome [DecidablePred p] : (Option.guard p a).isSome ↔ p a :=
  if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]

Proof state:
α✝ : Type u_1
p : α✝ → Prop
a : α✝
inst✝ : DecidablePred p
h : ¬p a
⊢ (guard p a).isSome = true ↔ p a

Tactic:
simp [Option.guard, h]

Result:
no goals

Proof state:
α✝ : Type u_1
p : α✝ → Prop
a : α✝
inst✝ : DecidablePred p
h : p a
⊢ (guard p a).isSome = true ↔ p a

Tactic:
simp [Option.guard, h]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem singleton_eq_cons_iff {a b : α} (m : Multiset α) : {a} = b ::ₘ m ↔ a = b ∧ m = 0

Proof state:
α : Type u_1
a b : α
m : Multiset α
⊢ {a} = b ::ₘ m ↔ a = b ∧ m = 0

Tactic:
rw [← cons_zero, cons_eq_cons]

Result:
α : Type u_1
a b : α
m : Multiset α
⊢ (a = b ∧ 0 = m ∨ a ≠ b ∧ ∃ cs, 0 = b ::ₘ cs ∧ m = a ::ₘ cs) ↔ a = b ∧ m = 0

Proof state:
α : Type u_1
a b : α
m : Multiset α
⊢ (a = b ∧ 0 = m ∨ a ≠ b ∧ ∃ cs, 0 = b ::ₘ cs ∧ m = a ::ₘ cs) ↔ a = b ∧ m = 0

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem map_top_of_surjective (f : G →* N) (h : Function.Surjective f) : Subgroup.map f ⊤ = ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
⊢ map f ⊤ = ⊤

Tactic:
rw [eq_top_iff]

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
⊢ ⊤ ≤ map f ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
x : N
a✝ : x ∈ ⊤
⊢ x ∈ map f ⊤

Tactic:
obtain ⟨y, hy⟩ := h x

Result:
case intro
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
x : N
a✝ : x ∈ ⊤
y : G
hy : f y = x
⊢ x ∈ map f ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
⊢ ⊤ ≤ map f ⊤

Tactic:
intro x _

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
x : N
a✝ : x ∈ ⊤
⊢ x ∈ map f ⊤

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
x : N
a✝ : x ∈ ⊤
y : G
hy : f y = x
⊢ x ∈ map f ⊤

Tactic:
exact ⟨y, trivial, hy⟩

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_sup_edist_ne_top_aux [PseudoMetricSpace α] [PseudoMetricSpace β]
    (f g : WithLp ∞ (α × β)) :
    edist f.fst g.fst ⊔ edist f.snd g.snd ≠ ⊤ :=
  ne_of_lt <| by simp [edist, PseudoMetricSpace.edist_dist]

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp ⊤ (α × β)
⊢ edist f.1 g.1 ⊔ edist f.2 g.2 < ⊤

Tactic:
simp [edist, PseudoMetricSpace.edist_dist]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_udiv_eq_false_of {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
    (x / y).msb = false

Proof state:
w : Nat
x : BitVec w
h : x.msb = false
y : BitVec w
⊢ (x / y).msb = false

Tactic:
simp [msb_udiv, h]

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upperCrossingTime_succ_eq (ω : Ω) : upperCrossingTime a b f N (n + 1) ω =
    hitting f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : OrderBot ι
inst✝ : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ upperCrossingTime a b f N (n + 1) ω = hitting f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω

Tactic:
simp only [upperCrossingTime_succ]

Result:
Ω : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : OrderBot ι
inst✝ : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ hitting f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω =
    hitting f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : OrderBot ι
inst✝ : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ hitting f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω =
    hitting f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Action/Limits.lean
/-- `F : C ⥤ SingleObj G ⥤ V` preserves the limit of some `K : J ⥤ C` if it does
evaluated at `SingleObj.star G`. -/
private lemma SingleObj.preservesLimit (F : C ⥤ SingleObj G ⥤ V)
    {J : Type w₁} [Category.{w₂} J] (K : J ⥤ C)
    (h : PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))) :
    PreservesLimit K F

Proof state:
case H
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ SingleObj G ⥤ V
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
k✝ : SingleObj G
⊢ PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj k✝)

Tactic:
exact h

Result:
no goals

Proof state:
case H
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ SingleObj G ⥤ V
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ ∀ (k : SingleObj G), PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj k)

Tactic:
intro _

Result:
case H
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ SingleObj G ⥤ V
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
k✝ : SingleObj G
⊢ PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj k✝)

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ SingleObj G ⥤ V
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ PreservesLimit K F

Tactic:
apply preservesLimit_of_evaluation

Result:
case H
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ SingleObj G ⥤ V
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ ∀ (k : SingleObj G), PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj k)
-- Mathlib/Analysis/Convex/Segment.lean
theorem sameRay_of_mem_segment [StrictOrderedCommRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y z : E}
    (h : x ∈ [y -[𝕜] z]) : SameRay 𝕜 (x - y) (z - x)

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : StrictOrderedCommRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
θ : 𝕜
hθ₀ : 0 ≤ θ
hθ₁ : θ ≤ 1
⊢ SameRay 𝕜 ((fun θ => y + θ • (z - y)) θ - y) (z - (fun θ => y + θ • (z - y)) θ)

Tactic:
simpa only [add_sub_cancel_left, ← sub_sub, sub_smul, one_smul] using
  (SameRay.sameRay_nonneg_smul_left (z - y) hθ₀).nonneg_smul_right (sub_nonneg.2 hθ₁)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : StrictOrderedCommRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : x ∈ [y-[𝕜]z]
⊢ SameRay 𝕜 (x - y) (z - x)

Tactic:
rw [segment_eq_image'] at h

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : StrictOrderedCommRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : x ∈ (fun θ => y + θ • (z - y)) '' Icc 0 1
⊢ SameRay 𝕜 (x - y) (z - x)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : StrictOrderedCommRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : x ∈ (fun θ => y + θ • (z - y)) '' Icc 0 1
⊢ SameRay 𝕜 (x - y) (z - x)

Tactic:
rcases h with ⟨θ, ⟨hθ₀, hθ₁⟩, rfl⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : StrictOrderedCommRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
θ : 𝕜
hθ₀ : 0 ≤ θ
hθ₁ : θ ≤ 1
⊢ SameRay 𝕜 ((fun θ => y + θ • (z - y)) θ - y) (z - (fun θ => y + θ • (z - y)) θ)
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem toBilin'Aux_toMatrixAux [DecidableEq n] (B₂ : BilinForm R₁ (n → R₁)) :
    -- Porting note: had to hint the base ring even though it should be clear from context...
    Matrix.toBilin'Aux (BilinForm.toMatrixAux (R₁ := R₁) (fun j => Pi.single j 1) B₂) = B₂

Proof state:
R₁ : Type u_1
inst✝² : CommSemiring R₁
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
B₂ : BilinForm R₁ (n → R₁)
⊢ ((BilinForm.toMatrixAux fun j => Pi.single j 1) B₂).toBilin'Aux = B₂

Tactic:
rw [BilinForm.toMatrixAux, Matrix.toBilin'Aux, toLinearMap₂'Aux_toMatrix₂Aux]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
    as.contains a = decide (a ∈ as)

Proof state:
α : Type u_1
n : Nat
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : Vector α n
⊢ as.contains a = decide (a ∈ as)

Tactic:
rw [Bool.eq_iff_iff, contains_iff, decide_eq_true_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
theorem HasDerivAt.log (hf : HasDerivAt f f' x) (hx : f x ≠ 0) :
    HasDerivAt (fun y => log (f y)) (f' / f x) x

Proof state:
f : ℝ → ℝ
x f' : ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0
⊢ HasDerivAt (fun y => Real.log (f y)) (f' / f x) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Result:
f : ℝ → ℝ
x f' : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.log (f y)) (f' / f x) Set.univ x

Proof state:
f : ℝ → ℝ
x f' : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.log (f y)) (f' / f x) Set.univ x

Tactic:
exact hf.log hx

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma toReal_nonpos {x : EReal} (hx : x ≤ 0) : x.toReal ≤ 0

Proof state:
case h_top
hx : ⊤ ≤ 0
⊢ ⊤.toReal ≤ 0

Tactic:
norm_num

Result:
no goals

Proof state:
x : EReal
hx : x ≤ 0
⊢ x.toReal ≤ 0

Tactic:
cases x

Result:
case h_bot
hx : ⊥ ≤ 0
⊢ ⊥.toReal ≤ 0

case h_real
a✝ : ℝ
hx : ↑a✝ ≤ 0
⊢ (↑a✝).toReal ≤ 0

case h_top
hx : ⊤ ≤ 0
⊢ ⊤.toReal ≤ 0

Proof state:
case h_real
a✝ : ℝ
hx : ↑a✝ ≤ 0
⊢ (↑a✝).toReal ≤ 0

Tactic:
exact toReal_coe _ ▸ EReal.coe_nonpos.mp hx

Result:
no goals

Proof state:
case h_bot
hx : ⊥ ≤ 0
⊢ ⊥.toReal ≤ 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem one_mul' [NeZero n] (k : Fin n) : (1 : Fin n) * k = k

Proof state:
n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ 1 * k = k

Tactic:
rw [Fin.mul_comm, Fin.mul_one']

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem map_prod [CommMonoid β] [CommMonoid γ] {G : Type*} [FunLike G β γ] [MonoidHomClass G β γ]
    (g : G) (f : α → β) (s : Finset α) : g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
G : Type u_6
inst✝¹ : FunLike G β γ
inst✝ : MonoidHomClass G β γ
g : G
f : α → β
s : Finset α
⊢ g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)

Tactic:
simp only [Finset.prod_eq_multiset_prod, map_multiset_prod, Multiset.map_map]

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
G : Type u_6
inst✝¹ : FunLike G β γ
inst✝ : MonoidHomClass G β γ
g : G
f : α → β
s : Finset α
⊢ (Multiset.map (⇑g ∘ f) s.val).prod = (Multiset.map (fun x => g (f x)) s.val).prod

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
G : Type u_6
inst✝¹ : FunLike G β γ
inst✝ : MonoidHomClass G β γ
g : G
f : α → β
s : Finset α
⊢ (Multiset.map (⇑g ∘ f) s.val).prod = (Multiset.map (fun x => g (f x)) s.val).prod

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Group/AEStabilizer.lean
@[to_additive (attr := simp)]
lemma aestabilizer_empty : aestabilizer G μ ∅ = ⊤ := top_unique fun _ _ ↦ by simp

Proof state:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝² : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x✝¹ : G
x✝ : x✝¹ ∈ ⊤
⊢ x✝¹ ∈ aestabilizer G μ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Basic.lean
lemma Even.pow_pos_iff (hn : Even n) (h₀ : n ≠ 0) : 0 < a ^ n ↔ a ≠ 0

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ k ≠ 0

Tactic:
simpa using h₀

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Even n
h₀ : n ≠ 0
⊢ 0 < a ^ n ↔ a ≠ 0

Tactic:
obtain ⟨k, rfl⟩ := hn

Result:
case intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0

Proof state:
case intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0

Tactic:
rw [pow_add, mul_self_pos (α := R), pow_ne_zero_iff (by simpa using h₀)]

Result:
no goals
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem prime_X_sub_C (r : R) : Prime (X - C r) :=
  ⟨X_sub_C_ne_zero r, not_isUnit_X_sub_C r, fun _ _ => by
    simp_rw [dvd_iff_isRoot, IsRoot.def, eval_mul, mul_eq_zero]
    exact id⟩

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ eval r x✝¹ = 0 ∨ eval r x✝ = 0 → eval r x✝¹ = 0 ∨ eval r x✝ = 0

Tactic:
exact id

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ X - C r ∣ x✝¹ * x✝ → X - C r ∣ x✝¹ ∨ X - C r ∣ x✝

Tactic:
simp_rw [dvd_iff_isRoot, IsRoot.def, eval_mul, mul_eq_zero]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ eval r x✝¹ = 0 ∨ eval r x✝ = 0 → eval r x✝¹ = 0 ∨ eval r x✝ = 0
-- Mathlib/Data/Finset/Range.lean
theorem coe_notMemRangeEquiv_symm (k : ℕ) :
    ((notMemRangeEquiv k).symm : ℕ → { n // n ∉ range k }) = fun j => ⟨j + k, by simp⟩ :=
  rfl

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
k j : ℕ
⊢ j + k ∉ range k

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem nndist_eq_of_L2 (x y : PiLp 2 β) :
    nndist x y = NNReal.sqrt (∑ i, nndist (x i) (y i) ^ 2) :=
  NNReal.eq <| by
    push_cast
    exact dist_eq_of_L2 _ _

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ dist x y = √(∑ x_1 : ι, dist (x x_1) (y x_1) ^ 2)

Tactic:
exact dist_eq_of_L2 _ _

Result:
no goals

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ ↑(nndist x y) = ↑(NNReal.sqrt (∑ i : ι, nndist (x i) (y i) ^ 2))

Tactic:
push_cast

Result:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ dist x y = √(∑ x_1 : ι, dist (x x_1) (y x_1) ^ 2)
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_mul_Iio_of_neg (a : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Iio a = Ioi (a / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a c : α
h : c < 0
⊢ (fun x => c * x) ⁻¹' Iio a = Ioi (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Iio_of_neg a h

Result:
no goals