harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/ModularForms/SlashActions.lean
theorem smul_slash (k : ℤ) (A : GL(2, ℝ)⁺) (f : ℍ → ℂ) (c : α) :
    (c • f) ∣[k]A = c • f ∣[k]A

Proof state:
case h
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
c : α
x✝ : ℍ
⊢ (((c • 1) • f) ∣[k]A) x✝ = ((c • 1) • f ∣[k]A) x✝

Tactic:
simp_rw [slash]

Result:
case h
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
c : α
x✝ : ℍ
⊢ ((c • 1) • f) (A • x✝) * ↑(↑↑A).det ^ (k - 1) * denom A x✝ ^ (-k) = ((c • 1) • f ∣[k]A) x✝

Proof state:
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
c : α
⊢ (c • f) ∣[k]A = c • f ∣[k]A

Tactic:
simp_rw [← smul_one_smul ℂ c f, ← smul_one_smul ℂ c (f ∣[k]A)]

Result:
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
c : α
⊢ ((c • 1) • f) ∣[k]A = (c • 1) • f ∣[k]A

Proof state:
case h
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
c : α
x✝ : ℍ
⊢ ((c • 1) • f) (A • x✝) * ↑(↑↑A).det ^ (k - 1) * denom A x✝ ^ (-k) = ((c • 1) • f ∣[k]A) x✝

Tactic:
simp only [slash, Algebra.id.smul_eq_mul, Matrix.GeneralLinearGroup.val_det_apply, Pi.smul_apply]

Result:
case h
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
c : α
x✝ : ℍ
⊢ c • 1 * f (A • x✝) * ↑(↑↑A).det ^ (k - 1) * denom A x✝ ^ (-k) =
    c • 1 * (f (A • x✝) * ↑(↑↑A).det ^ (k - 1) * denom A x✝ ^ (-k))

Proof state:
case h
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
c : α
x✝ : ℍ
⊢ c • 1 * f (A • x✝) * ↑(↑↑A).det ^ (k - 1) * denom A x✝ ^ (-k) =
    c • 1 * (f (A • x✝) * ↑(↑↑A).det ^ (k - 1) * denom A x✝ ^ (-k))

Tactic:
ring

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
c : α
⊢ ((c • 1) • f) ∣[k]A = (c • 1) • f ∣[k]A

Tactic:
ext1

Result:
case h
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
c : α
x✝ : ℍ
⊢ (((c • 1) • f) ∣[k]A) x✝ = ((c • 1) • f ∣[k]A) x✝
-- Mathlib/Topology/Maps/Basic.lean
lemma isClosed_iff_image_isClosed (hf : IsClosedEmbedding f) {s : Set X} :
    IsClosed s ↔ IsClosed (f '' s) :=
  ⟨hf.isClosedMap s, fun h => by
    rw [← preimage_image_eq s hf.injective]
    exact h.preimage hf.continuous⟩

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsClosedEmbedding f
s : Set X
h : IsClosed (f '' s)
⊢ IsClosed (f ⁻¹' (f '' s))

Tactic:
exact h.preimage hf.continuous

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsClosedEmbedding f
s : Set X
h : IsClosed (f '' s)
⊢ IsClosed s

Tactic:
rw [← preimage_image_eq s hf.injective]

Result:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsClosedEmbedding f
s : Set X
h : IsClosed (f '' s)
⊢ IsClosed (f ⁻¹' (f '' s))
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem isOpenMap_of_ne_zero [TopologicalSpace R] [DivisionRing R] [ContinuousSub R]
    [AddCommGroup M] [TopologicalSpace M] [ContinuousAdd M] [Module R M] [ContinuousSMul R M]
    (f : M →L[R] R) (hf : f ≠ 0) : IsOpenMap f :=
  let ⟨x, hx⟩ := exists_ne_zero hf
  IsOpenMap.of_sections fun y =>
    ⟨fun a => y + (a - f y) • (f x)⁻¹ • x, Continuous.continuousAt <| by continuity, by simp,
      fun a => by simp [hx]⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝⁷ : TopologicalSpace R
inst✝⁶ : DivisionRing R
inst✝⁵ : ContinuousSub R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
f : M →L[R] R
hf : f ≠ 0
x : M
hx : f x ≠ 0
y : M
a : R
⊢ f ((fun a => y + (a - f y) • (f x)⁻¹ • x) a) = a

Tactic:
simp [hx]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁷ : TopologicalSpace R
inst✝⁶ : DivisionRing R
inst✝⁵ : ContinuousSub R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
f : M →L[R] R
hf : f ≠ 0
x : M
hx : f x ≠ 0
y : M
⊢ Continuous fun a => y + (a - f y) • (f x)⁻¹ • x

Tactic:
continuity

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁷ : TopologicalSpace R
inst✝⁶ : DivisionRing R
inst✝⁵ : ContinuousSub R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
f : M →L[R] R
hf : f ≠ 0
x : M
hx : f x ≠ 0
y : M
⊢ (fun a => y + (a - f y) • (f x)⁻¹ • x) (f y) = y

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Equiv/Fin.lean
theorem finSuccEquiv'_last_apply_castSucc (i : Fin n) :
    finSuccEquiv' (Fin.last n) (Fin.castSucc i) = i

Proof state:
n : ℕ
i : Fin n
⊢ (finSuccEquiv' (Fin.last n)) i.castSucc = some i

Tactic:
rw [← Fin.succAbove_last, finSuccEquiv'_succAbove]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translationNumber_mul_of_commute {f g : CircleDeg1Lift} (h : Commute f g) :
    τ (f * g) = τ f + τ g

Proof state:
f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x => f.transnumAuxSeq x + g.transnumAuxSeq x) atTop (𝓝 (τ (f * g)))

Tactic:
simp only [transnumAuxSeq, ← add_div]

Result:
f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x => ((f ^ 2 ^ x) 0 + (g ^ 2 ^ x) 0) / 2 ^ x) atTop (𝓝 (τ (f * g)))

Proof state:
f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x => ((f ^ 2 ^ x) 0 + (g ^ 2 ^ x) 0) / 2 ^ x) atTop (𝓝 (τ (f * g)))

Tactic:
refine (f * g).tendsto_translationNumber_of_dist_bounded_aux
  (fun n ↦ (f ^ n) 0 + (g ^ n) 0) 1 fun n ↦ ?_

Result:
f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist (((f * g) ^ n) 0) ((fun n => (f ^ n) 0 + (g ^ n) 0) n) ≤ 1

Proof state:
f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist (((f * g) ^ n) 0) ((fun n => (f ^ n) 0 + (g ^ n) 0) n) ≤ 1

Tactic:
rw [h.mul_pow, dist_comm]

Result:
f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist ((fun n => (f ^ n) 0 + (g ^ n) 0) n) ((f ^ n * g ^ n) 0) ≤ 1

Proof state:
f g : CircleDeg1Lift
h : Commute f g
⊢ τ (f * g) = τ f + τ g

Tactic:
refine tendsto_nhds_unique ?_
  (f.tendsto_translationNumber_aux.add g.tendsto_translationNumber_aux)

Result:
f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x => f.transnumAuxSeq x + g.transnumAuxSeq x) atTop (𝓝 (τ (f * g)))

Proof state:
f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist ((fun n => (f ^ n) 0 + (g ^ n) 0) n) ((f ^ n * g ^ n) 0) ≤ 1

Tactic:
exact le_of_lt ((f ^ n).dist_map_map_zero_lt (g ^ n))

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Complemented.lean
theorem ker_closedComplemented_of_finiteDimensional_range (f : E →L[𝕜] F)
    [FiniteDimensional 𝕜 (range f)] : (ker f).ClosedComplemented

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(range f)
f' : E →L[𝕜] ↥(range f) := f.codRestrict (range f) ⋯
⊢ (ker f).ClosedComplemented

Tactic:
rcases f'.exists_right_inverse_of_surjective (f : E →ₗ[𝕜] F).range_rangeRestrict with ⟨g, hg⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(range f)
f' : E →L[𝕜] ↥(range f) := f.codRestrict (range f) ⋯
g : ↥(range f) →L[𝕜] E
hg : f'.comp g = id 𝕜 ↥(range f)
⊢ (ker f).ClosedComplemented

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(range f)
f' : E →L[𝕜] ↥(range f) := f.codRestrict (range f) ⋯
g : ↥(range f) →L[𝕜] E
hg : f'.comp g = id 𝕜 ↥(range f)
⊢ (ker f).ClosedComplemented

Tactic:
simpa only [f', ker_codRestrict]
  using f'.closedComplemented_ker_of_rightInverse g (ContinuousLinearMap.ext_iff.1 hg)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(range f)
⊢ (ker f).ClosedComplemented

Tactic:
set f' : E →L[𝕜] range f := f.codRestrict _ (LinearMap.mem_range_self (f : E →ₗ[𝕜] F))

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(range f)
f' : E →L[𝕜] ↥(range f) := f.codRestrict (range f) ⋯
⊢ (ker f).ClosedComplemented
-- Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
/-- Multiplication on the left by `m` tends to `𝓝 m` if and only if multiplication on the right
does, provided the elements are eventually selfadjoint along the filter `l`. -/
lemma tendsto_mul_left_iff_tendsto_mul_right {l : Filter A} (hl : ∀ᶠ x in l, IsSelfAdjoint x) :
    (∀ m, Tendsto (m * ·) l (𝓝 m)) ↔ (∀ m, Tendsto (· * m) l (𝓝 m))

Proof state:
case refine_1
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x => m * x) l (𝓝 m)
m : A
⊢ Tendsto (fun x => x * m) l (𝓝 m)

case refine_2
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x => x * m) l (𝓝 m)
m : A
⊢ Tendsto (fun x => m * x) l (𝓝 m)

Tactic:
all_goals
  apply (star_star m ▸ (continuous_star.tendsto _ |>.comp <| h (star m))).congr'
  filter_upwards [hl] with x hx
  simp [hx.star_eq]

Result:
no goals

Proof state:
case refine_2
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x => x * m) l (𝓝 m)
m : A
⊢ (star ∘ fun x => x * star m) =ᶠ[l] fun x => m * x

Tactic:
filter_upwards [hl] with x hx

Result:
case h
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x => x * m) l (𝓝 m)
m x : A
hx : IsSelfAdjoint x
⊢ (star ∘ fun x => x * star m) x = m * x

Proof state:
case refine_2
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x => x * m) l (𝓝 m)
m : A
⊢ Tendsto (fun x => m * x) l (𝓝 m)

Tactic:
apply (star_star m ▸ (continuous_star.tendsto _ |>.comp <| h (star m))).congr'

Result:
case refine_2
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x => x * m) l (𝓝 m)
m : A
⊢ (star ∘ fun x => x * star m) =ᶠ[l] fun x => m * x

Proof state:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
⊢ (∀ (m : A), Tendsto (fun x => m * x) l (𝓝 m)) ↔ ∀ (m : A), Tendsto (fun x => x * m) l (𝓝 m)

Tactic:
refine ⟨fun h m ↦ ?_, fun h m ↦ ?_⟩

Result:
case refine_1
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x => m * x) l (𝓝 m)
m : A
⊢ Tendsto (fun x => x * m) l (𝓝 m)

case refine_2
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x => x * m) l (𝓝 m)
m : A
⊢ Tendsto (fun x => m * x) l (𝓝 m)

Proof state:
case h
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x => x * m) l (𝓝 m)
m x : A
hx : IsSelfAdjoint x
⊢ (star ∘ fun x => x * star m) x = m * x

Tactic:
simp [hx.star_eq]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioc_subset_Ioi_self : Ioc a b ⊆ Ioi a

Proof state:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Ioi a

Tactic:
simpa [← coe_subset] using Set.Ioc_subset_Ioi_self

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem NodupKeys.eq_of_mk_mem {a : α} {b b' : β a} {l : List (Sigma β)} (nd : NodupKeys l)
    (h : Sigma.mk a b ∈ l) (h' : Sigma.mk a b' ∈ l) : b = b'

Proof state:
case refl
α : Type u
β : α → Type v
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h h' : ⟨a, b⟩ ∈ l
⊢ b = b

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
a : α
b b' : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
h' : ⟨a, b'⟩ ∈ l
⊢ b = b'

Tactic:
cases nd.eq_of_fst_eq h h' rfl

Result:
case refl
α : Type u
β : α → Type v
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h h' : ⟨a, b⟩ ∈ l
⊢ b = b
-- Mathlib/Order/Hom/Basic.lean
theorem OrderIso.map_bot' [LE α] [PartialOrder β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ x', x ≤ x')
    (hy : ∀ y', y ≤ y') : f x = y

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ f x ≤ y

Tactic:
rw [← f.apply_symm_apply y, f.map_rel_iff]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ x ≤ f.symm y

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ f x = y

Tactic:
refine le_antisymm ?_ (hy _)

Result:
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ f x ≤ y

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ x ≤ f.symm y

Tactic:
apply hx

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_add_add_self (x y : F) : ⟪x + y, x + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x, x⟫_𝕜 + ⟪y, x⟫_𝕜 + (⟪x, y⟫_𝕜 + ⟪y, y⟫_𝕜) = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x + y, x + y⟫_𝕜 = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

Tactic:
simp only [inner_add_left, inner_add_right]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x, x⟫_𝕜 + ⟪y, x⟫_𝕜 + (⟪x, y⟫_𝕜 + ⟪y, y⟫_𝕜) = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜
-- Mathlib/Data/Fin/VecNotation.lean
theorem range_cons_empty (x : α) (u : Fin 0 → α) : Set.range (Matrix.vecCons x u) = {x}

Proof state:
α : Type u
x : α
u : Fin 0 → α
⊢ Set.range (vecCons x u) = {x}

Tactic:
rw [range_cons, range_empty, Set.union_empty]

Result:
no goals
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem tendsto_atTop_zero_of_summable {f : ℕ → ℝ≥0} (hf : Summable f) : Tendsto f atTop (𝓝 0)

Proof state:
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
exact tendsto_cofinite_zero_of_summable hf

Result:
no goals

Proof state:
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f atTop (𝓝 0)

Tactic:
rw [← Nat.cofinite_eq_atTop]

Result:
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_eq_neg_pi_div_two_iff {θ : Angle} : θ.toReal = -π / 2 ↔ θ = (-π / 2 : ℝ)

Proof state:
θ : Angle
⊢ θ.toReal = -π / 2 ↔ θ = ↑(-π / 2)

Tactic:
rw [← toReal_inj, toReal_neg_pi_div_two]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem mul_inv_cancel_left (a b : G) : a * (a⁻¹ * b) = b

Proof state:
G : Type u_1
inst✝ : Group G
a b : G
⊢ a * (a⁻¹ * b) = b

Tactic:
rw [← mul_assoc, mul_inv_cancel, one_mul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem tendsto_const_mul_rpow_nhds_zero_of_pos {c : ℝ≥0∞} (hc : c ≠ ∞) {y : ℝ} (hy : 0 < y) :
    Tendsto (fun x : ℝ≥0∞ => c * x ^ y) (𝓝 0) (𝓝 0)

Proof state:
case h.e'_5.h.e'_3
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ 0 = c * 0 ^ y

Tactic:
simp [hy]

Result:
no goals

Proof state:
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x => c * x ^ y) (𝓝 0) (𝓝 0)

Tactic:
convert ENNReal.Tendsto.const_mul (ENNReal.continuous_rpow_const.tendsto 0) _

Result:
case h.e'_5.h.e'_3
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ 0 = c * 0 ^ y

case convert_3
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ 0 ^ y ≠ 0 ∨ c ≠ ⊤

Proof state:
case convert_3
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ 0 ^ y ≠ 0 ∨ c ≠ ⊤

Tactic:
exact Or.inr hc

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem pred_eq_iff_eq_succ {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) {j : Fin n} :
    i.pred hi = j ↔ i = j.succ :=
  ⟨fun h => by simp only [← h, Fin.succ_pred], fun h => by simp only [h, Fin.pred_succ]⟩

Proof state:
n : Nat
i : Fin (n + 1)
hi : i ≠ 0
j : Fin n
h : i.pred hi = j
⊢ i = j.succ

Tactic:
simp only [← h, Fin.succ_pred]

Result:
no goals

Proof state:
n : Nat
i : Fin (n + 1)
hi : i ≠ 0
j : Fin n
h : i = j.succ
⊢ i.pred hi = j

Tactic:
simp only [h, Fin.pred_succ]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem map_lt_add_floor_translationNumber_add_one (x : ℝ) : f x < x + ⌊τ f⌋ + 1

Proof state:
f : CircleDeg1Lift
x : ℝ
⊢ f x < x + ↑(⌊τ f⌋ + 1)

Tactic:
refine map_lt_of_translationNumber_lt_int _ ?_ _

Result:
f : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑(⌊τ f⌋ + 1)

Proof state:
f : CircleDeg1Lift
x : ℝ
⊢ f x < x + ↑⌊τ f⌋ + 1

Tactic:
rw [add_assoc]

Result:
f : CircleDeg1Lift
x : ℝ
⊢ f x < x + (↑⌊τ f⌋ + 1)

Proof state:
f : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑(⌊τ f⌋ + 1)

Tactic:
push_cast

Result:
f : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑⌊τ f⌋ + 1

Proof state:
f : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑⌊τ f⌋ + 1

Tactic:
exact lt_floor_add_one _

Result:
no goals

Proof state:
f : CircleDeg1Lift
x : ℝ
⊢ f x < x + (↑⌊τ f⌋ + 1)

Tactic:
norm_cast

Result:
f : CircleDeg1Lift
x : ℝ
⊢ f x < x + ↑(⌊τ f⌋ + 1)
-- Mathlib/Algebra/Polynomial/Degree/Domain.lean
lemma natDegree_smul (ha : a ≠ 0) : (a • p).natDegree = p.natDegree

Proof state:
R : Type u
a : R
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
ha : a ≠ 0
⊢ (a • p).natDegree = p.natDegree

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
a : R
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
ha : a ≠ 0
hp : p = 0
⊢ (a • p).natDegree = p.natDegree

case neg
R : Type u
a : R
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).natDegree = p.natDegree

Proof state:
case neg.p1
R : Type u
a : R
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).coeff p.natDegree ≠ 0

Tactic:
simpa only [coeff_smul, coeff_natDegree, smul_eq_mul, ne_eq, mul_eq_zero,
  leadingCoeff_eq_zero, not_or] using ⟨ha, hp⟩

Result:
no goals

Proof state:
case pos
R : Type u
a : R
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
ha : a ≠ 0
hp : p = 0
⊢ (a • p).natDegree = p.natDegree

Tactic:
simp only [hp, smul_zero]

Result:
no goals

Proof state:
case neg.pn
R : Type u
a : R
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).natDegree ≤ p.natDegree

Tactic:
exact (natDegree_smul_le _ _).trans (le_refl _)

Result:
no goals

Proof state:
case neg
R : Type u
a : R
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).natDegree = p.natDegree

Tactic:
apply natDegree_eq_of_le_of_coeff_ne_zero

Result:
case neg.pn
R : Type u
a : R
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).natDegree ≤ p.natDegree

case neg.p1
R : Type u
a : R
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).coeff p.natDegree ≠ 0
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem uniformEquicontinuousOn_iff_range {F : ι → β → α} {S : Set β} :
    UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((↑) : range F → β → α) S :=
  ⟨fun h => by rw [← comp_rangeSplitting F]; exact h.comp _, fun h =>
    h.comp (rangeFactorization F)⟩

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
h : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn (F ∘ rangeSplitting F) S

Tactic:
exact h.comp _

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
h : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn Subtype.val S

Tactic:
rw [← comp_rangeSplitting F]

Result:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
h : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn (F ∘ rangeSplitting F) S
-- Mathlib/Analysis/Polynomial/CauchyBound.lean
@[simp]
lemma cauchyBound_X_sub_C (x : K) : cauchyBound (X - C x) = ‖x‖₊ + 1

Proof state:
K : Type u_1
inst✝ : NormedDivisionRing K
x : K
⊢ (X - C x).cauchyBound = ‖x‖₊ + 1

Tactic:
simp [cauchyBound]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
@[simp] lemma snocCases_snoc
    {P : (∀ i : Fin (n+1), α i) → Sort*} (h : ∀ x x₀, P (Fin.snoc x x₀))
    (x : ∀ i : Fin n, (Fin.init α) i) (x₀ : α (Fin.last _)) :
    snocCases h (Fin.snoc x x₀) = h x x₀

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
P : ((i : Fin (n + 1)) → α i) → Sort u_2
h : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → P (snoc x x₀)
x : (i : Fin n) → init α i
x₀ : α (last n)
⊢ snocCases h (snoc x x₀) = h x x₀

Tactic:
rw [snocCases, cast_eq_iff_heq, Fin.init_snoc, Fin.snoc_last]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem le_mul_iff_eq_zero_of_nonneg_of_neg_of_nonneg {α} [LinearOrderedSemiring α]
    {a b c : α} (ha : 0 ≤ a) (hb : b < 0) (hc : 0 ≤ c) : a ≤ b * c ↔ a = 0 ∧ c = 0

Proof state:
case mp
α : Type u_6
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
h : a ≤ b * c
⊢ a = 0 ∧ c = 0

Tactic:
exact
  ⟨(h.trans (mul_nonpos_of_nonpos_of_nonneg hb.le hc)).antisymm ha,
    (nonpos_of_mul_nonneg_right (ha.trans h) hb).antisymm hc⟩

Result:
no goals

Proof state:
case mpr
α : Type u_6
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a = 0 ∧ c = 0 → a ≤ b * c

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case mpr.intro
α : Type u_6
inst✝ : LinearOrderedSemiring α
b : α
hb : b < 0
ha hc : 0 ≤ 0
⊢ 0 ≤ b * 0

Proof state:
α : Type u_6
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a ≤ b * c ↔ a = 0 ∧ c = 0

Tactic:
constructor

Result:
case mp
α : Type u_6
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a ≤ b * c → a = 0 ∧ c = 0

case mpr
α : Type u_6
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a = 0 ∧ c = 0 → a ≤ b * c

Proof state:
case mpr.intro
α : Type u_6
inst✝ : LinearOrderedSemiring α
b : α
hb : b < 0
ha hc : 0 ≤ 0
⊢ 0 ≤ b * 0

Tactic:
rw [mul_zero]

Result:
no goals

Proof state:
case mp
α : Type u_6
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a ≤ b * c → a = 0 ∧ c = 0

Tactic:
intro h

Result:
case mp
α : Type u_6
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
h : a ≤ b * c
⊢ a = 0 ∧ c = 0