harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/RCLike/Inner.lean
lemma wInner_smul_right {𝕝 : Type*} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝 𝕜] [StarModule 𝕝 𝕜]
    [SMulCommClass ℝ 𝕝 𝕜] [∀ i, Module 𝕝 (E i)] [∀ i, IsScalarTower 𝕝 𝕜 (E i)] (c : 𝕝)
    (w : ι → ℝ) (f g : ∀ i, E i) : ⟪f, c • g⟫_[𝕜, w] = c • ⟪f, g⟫_[𝕜, w]

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝¹⁰ : Fintype ι
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → InnerProductSpace 𝕜 (E i)
𝕝 : Type u_5
inst✝⁶ : CommSemiring 𝕝
inst✝⁵ : StarRing 𝕝
inst✝⁴ : Algebra 𝕝 𝕜
inst✝³ : StarModule 𝕝 𝕜
inst✝² : SMulCommClass ℝ 𝕝 𝕜
inst✝¹ : (i : ι) → Module 𝕝 (E i)
inst✝ : ∀ (i : ι), IsScalarTower 𝕝 𝕜 (E i)
c : 𝕝
w : ι → ℝ
f g : (i : ι) → E i
⊢ wInner w f (c • g) = c • wInner w f g

Tactic:
simp_rw [wInner, Pi.smul_apply, inner_smul_right_eq_smul, smul_sum, smul_comm]

Result:
no goals
-- Mathlib/Order/MinMax.lean
theorem min_choice (a b : α) : min a b = a ∨ min a b = b

Proof state:
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ a ⊓ b = a ∨ a ⊓ b = b

Tactic:
cases le_total a b <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem mrange_inl : mrange (inl M N) = prod ⊤ ⊥

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mrange (inl M N) = ⊤.prod ⊥

Tactic:
simpa only [mrange_eq_map] using map_inl ⊤

Result:
no goals
-- Mathlib/Computability/TMConfig.lean
theorem nil_eval (v) : nil.eval v = pure []

Proof state:
v : List ℕ
⊢ nil.eval v = pure []

Tactic:
simp [nil]

Result:
no goals
-- Mathlib/Algebra/Module/SpanRank.lean
lemma Basis.mk_eq_spanRank [RankCondition R] {ι : Type*} (v : Basis ι R M) :
    #(Set.range v) = (⊤ : Submodule R M).spanRank

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
ι : Type u_1
v : Basis ι R M
⊢ #↑(Set.range ⇑v) = ⊤.spanRank

Tactic:
rw [spanRank]

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
ι : Type u_1
v : Basis ι R M
⊢ #↑(Set.range ⇑v) = ⨅ s, #↑↑s

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
ι : Type u_1
v : Basis ι R M
x : { s // span R s = ⊤ } := ⟨Set.range ⇑v, ⋯⟩
⊢ #↑(Set.range ⇑v) = ⨅ s, #↑↑s

Tactic:
exact le_antisymm (le_ciInf fun s ↦ v.le_span s.2) (ciInf_le' _ x)

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
ι : Type u_1
v : Basis ι R M
⊢ #↑(Set.range ⇑v) = ⨅ s, #↑↑s

Tactic:
let x : {s : Set M // span R s = ⊤} := ⟨Set.range v, Basis.span_eq v⟩

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
ι : Type u_1
v : Basis ι R M
x : { s // span R s = ⊤ } := ⟨Set.range ⇑v, ⋯⟩
⊢ #↑(Set.range ⇑v) = ⨅ s, #↑↑s
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem continuous_of_continuousAt_one {M hom : Type*} [MulOneClass M] [TopologicalSpace M]
    [ContinuousMul M] [FunLike hom G M] [MonoidHomClass hom G M] (f : hom)
    (hf : ContinuousAt f 1) :
    Continuous f :=
  continuous_iff_continuousAt.2 fun x => by
    simpa only [ContinuousAt, ← map_mul_left_nhds_one x, tendsto_map'_iff, Function.comp_def,
      map_mul, map_one, mul_one] using hf.tendsto.const_mul (f x)

Proof state:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
M : Type u_1
hom : Type u_2
inst✝⁴ : MulOneClass M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
f : hom
hf : ContinuousAt (⇑f) 1
x : G
⊢ ContinuousAt (⇑f) x

Tactic:
simpa only [ContinuousAt, ← map_mul_left_nhds_one x, tendsto_map'_iff, Function.comp_def,
  map_mul, map_one, mul_one] using hf.tendsto.const_mul (f x)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_nonneg (x : ℝ) : 0 ≤ arccos x

Proof state:
x : ℝ
⊢ 0 ≤ arccos x

Tactic:
unfold arccos

Result:
x : ℝ
⊢ 0 ≤ π / 2 - arcsin x

Proof state:
x : ℝ
⊢ 0 ≤ π / 2 - arcsin x

Tactic:
linarith [arcsin_le_pi_div_two x]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_eq_some' : x.map f = some b ↔ ∃ a, x = some a ∧ f a = b

Proof state:
α✝¹ : Type u_1
b : α✝¹
α✝ : Type u_2
x : Option α✝
f : α✝ → α✝¹
⊢ Option.map f x = some b ↔ ∃ a, x = some a ∧ f a = b

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem lookup_replicate_ne {k : α} (h : !k == a) :
    (replicate n (a, b)).lookup k = none

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
n : Nat
α✝ : Type u_1
b : α✝
k : α
h : (!k == a) = true
⊢ lookup k (replicate n (a, b)) = none

Tactic:
simp_all [lookup_replicate]

Result:
no goals
-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem Cofix.ext_mk {α : TypeVec n} (x y : F (α ::: Cofix F α)) (h : Cofix.mk x = Cofix.mk y) :
    x = y

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : F (α ::: Cofix F α)
h : mk x = mk y
⊢ x = y

Tactic:
rw [← Cofix.dest_mk x, h, Cofix.dest_mk]

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
lemma bddAbove_range_prod {F : ι → α × β} :
    BddAbove (range F) ↔ BddAbove (range <| Prod.fst ∘ F) ∧ BddAbove (range <| Prod.snd ∘ F)

Proof state:
ι : Sort x
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
F : ι → α × β
⊢ BddAbove (range F) ↔ BddAbove (range (Prod.fst ∘ F)) ∧ BddAbove (range (Prod.snd ∘ F))

Tactic:
simp only [bddAbove_prod, ← range_comp]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_insert [MeasurableSingletonClass α] {a : α} {s : Set α} (h : a ∉ s)
    (f : α → ℝ≥0∞) : ∫⁻ x in insert a s, f x ∂μ = f a * μ {a} + ∫⁻ x in s, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ Disjoint s {a}

Tactic:
rwa [disjoint_singleton_right]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in insert a s, f x ∂μ = f a * μ {a} + ∫⁻ (x : α) in s, f x ∂μ

Tactic:
rw [← union_singleton, lintegral_union (measurableSet_singleton a), lintegral_singleton,
  add_comm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ Disjoint s {a}
-- Mathlib/Data/Set/Prod.lean
theorem mk_preimage_prod_left (hb : b ∈ t) : (fun a => (a, b)) ⁻¹' s ×ˢ t = s

Proof state:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∈ t
a : α
⊢ a ∈ (fun a => (a, b)) ⁻¹' s ×ˢ t ↔ a ∈ s

Tactic:
simp [hb]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∈ t
⊢ (fun a => (a, b)) ⁻¹' s ×ˢ t = s

Tactic:
ext a

Result:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∈ t
a : α
⊢ a ∈ (fun a => (a, b)) ⁻¹' s ×ˢ t ↔ a ∈ s
-- Mathlib/Tactic/Ring/RingNF.lean
theorem mul_neg {R} [Ring R] (a b : R) : a * -b = -(a * b)

Proof state:
R : Type u_2
inst✝ : Ring R
a b : R
⊢ a * -b = -(a * b)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
theorem Convex.combo_interior_closure_subset_interior {s : Set E} (hs : Convex 𝕜 s) {a b : 𝕜}
    (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) : a • interior s + b • closure s ⊆ interior s :=
  interior_smul₀ ha.ne' s ▸
    calc
      interior (a • s) + b • closure s ⊆ interior (a • s) + closure (b • s) :=
        add_subset_add Subset.rfl (smul_closure_subset b s)
      _ = interior (a • s) + b • s

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
⊢ interior (a • s) + closure (b • s) = interior (a • s) + b • s

Tactic:
rw [isOpen_interior.add_closure (b • s)]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
lemma div_re (z w : ℂ) : (z / w).re = z.re * w.re / normSq w + z.im * w.im / normSq w

Proof state:
z w : ℂ
⊢ (z / w).re = z.re * w.re / normSq w + z.im * w.im / normSq w

Tactic:
simp [div_eq_mul_inv, mul_assoc, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Ioi : ((↑) : ℤ → α) ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ioi a ↔ x✝ ∈ Ioi ⌊a⌋

Tactic:
simp [floor_lt]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ Int.cast ⁻¹' Ioi a = Ioi ⌊a⌋

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ioi a ↔ x✝ ∈ Ioi ⌊a⌋
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_one_div_of_mul_eq_one_right (h : a * b = 1) : b = 1 / a

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ b = 1 / a

Tactic:
rw [eq_inv_of_mul_eq_one_right h, one_div]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem modelWithCornersSelf_prod : 𝓘(𝕜, E × F) = 𝓘(𝕜, E).prod 𝓘(𝕜, F)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ 𝓘(𝕜, E × F) = 𝓘(𝕜, E).prod 𝓘(𝕜, F)

Tactic:
ext1 <;> simp

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean
@[simp]
lemma d_mul (b b' : B) : D.d (b * b') = b • D.d b' + b' • D.d b

Proof state:
A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
D : M.Derivation f
b b' : ↑B
⊢ D.d (b * b') = b • D.d b' + b' • D.d b

Tactic:
simp [d]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
lemma piTensorHomMap_tprod_eq_map (f : Π i, s i →ₗ[R] t i) :
    piTensorHomMap (tprod R f) = map f

Proof state:
case H.H
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
x✝ : (i : ι) → s i
⊢ ((piTensorHomMap ((tprod R) f)).compMultilinearMap (tprod R)) x✝ = ((map f).compMultilinearMap (tprod R)) x✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
⊢ piTensorHomMap ((tprod R) f) = map f

Tactic:
ext

Result:
case H.H
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
x✝ : (i : ι) → s i
⊢ ((piTensorHomMap ((tprod R) f)).compMultilinearMap (tprod R)) x✝ = ((map f).compMultilinearMap (tprod R)) x✝
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractLeft_one : d⌋(1 : CliffordAlgebra Q) = 0

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
⊢ (contractLeft d) 1 = 0

Tactic:
simpa only [map_one] using contractLeft_algebraMap Q d 1

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem init_update_last : init (update q (last n) z) = init q

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
z : α (last n)
j : Fin n
⊢ init (update q (last n) z) j = init q j

Tactic:
simp [init, Fin.ne_of_lt, castSucc_lt_last]

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
z : α (last n)
⊢ init (update q (last n) z) = init q

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
z : α (last n)
j : Fin n
⊢ init (update q (last n) z) j = init q j
-- Mathlib/Analysis/Convex/Side.lean
theorem sOppSide_comm {s : AffineSubspace R P} {x y : P} : s.SOppSide x y ↔ s.SOppSide y x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ s.SOppSide x y ↔ s.SOppSide y x

Tactic:
rw [SOppSide, SOppSide, wOppSide_comm, and_comm (b := x ∉ s)]

Result:
no goals
-- Mathlib/RingTheory/Extension.lean
@[simp]
lemma Cotangent.map_mk (f : Hom P P') (x) :
    Cotangent.map f (.mk x) =
      .mk ⟨f.toAlgHom x, by simpa [-map_aeval] using RingHom.congr_arg (algebraMap S S') x.2⟩ :=
  rfl

Proof state:
R : Type u
S : Type v
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
P : Extension R S
R' : Type ?u.330734
S' : Type ?u.330737
inst✝¹³ : CommRing R'
inst✝¹² : CommRing S'
inst✝¹¹ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.331043
S'' : Type ?u.331046
inst✝¹⁰ : CommRing R''
inst✝⁹ : CommRing S''
inst✝⁸ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra R' S''
inst✝⁴ : Algebra S S'
inst✝³ : Algebra S' S''
inst✝² : Algebra S S''
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : ↥P.ker
⊢ f.toAlgHom ↑x ∈ P'.ker

Tactic:
simpa [-map_aeval] using RingHom.congr_arg (algebraMap S S') x.2

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
lemma essSup_piecewise {s : Set α} [DecidablePred (· ∈ s)] {g} (hs : MeasurableSet s) :
    essSup (s.piecewise f g) μ = max (essSup f (μ.restrict s)) (essSup g (μ.restrict sᶜ))

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → ℝ≥0∞
hs : MeasurableSet s
⊢ essSup (s.piecewise f g) μ = essSup f (μ.restrict s) ⊔ essSup g (μ.restrict sᶜ)

Tactic:
simp only [essSup, limsup_piecewise, blimsup_eq_limsup, ae_restrict_eq, hs, hs.compl]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → ℝ≥0∞
hs : MeasurableSet s
⊢ limsup f (ae μ ⊓ 𝓟 {x | x ∈ s}) ⊔ limsup g (ae μ ⊓ 𝓟 {x | x ∉ s}) = limsup f (ae μ ⊓ 𝓟 s) ⊔ limsup g (ae μ ⊓ 𝓟 sᶜ)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → ℝ≥0∞
hs : MeasurableSet s
⊢ limsup f (ae μ ⊓ 𝓟 {x | x ∈ s}) ⊔ limsup g (ae μ ⊓ 𝓟 {x | x ∉ s}) = limsup f (ae μ ⊓ 𝓟 s) ⊔ limsup g (ae μ ⊓ 𝓟 sᶜ)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem Polynomial.isRoot_cos_pi_div_five :
    (4 • X ^ 2 - 2 • X - C 1 : ℝ[X]).IsRoot (cos (π / 5))

Proof state:
⊢ (4 • X ^ 2 - 2 • X - C 1).IsRoot (cos (π / 5))

Tactic:
simpa using quadratic_root_cos_pi_div_five

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem two_div_one_sub_two_div_e_le_eight : 2 / (1 - 2 / exp 1) ≤ 8

Proof state:
⊢ 8 * 2 ≤ (8 - 2) * rexp 1

Tactic:
linarith [exp_one_gt_d9]

Result:
no goals

Proof state:
⊢ 0 < 1 - 2 / rexp 1

Tactic:
rw [sub_pos, div_lt_one] <;> exact exp_one_gt_d9.trans' (by norm_num)

Result:
no goals

Proof state:
⊢ 0 < 2.7182818283

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ 2 / (1 - 2 / rexp 1) ≤ 8

Tactic:
rw [div_le_iff₀, mul_sub, mul_one, mul_div_assoc', le_sub_comm, div_le_iff₀ (exp_pos _)]

Result:
⊢ 8 * 2 ≤ (8 - 2) * rexp 1


⊢ 0 < 1 - 2 / rexp 1
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem ultrafilter_le_nhds_infty {f : Ultrafilter (OnePoint X)} :
    (f : Filter (OnePoint X)) ≤ 𝓝 ∞ ↔ ∀ s : Set X, IsClosed s → IsCompact s → (↑) '' s ∉ f

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
f : Ultrafilter (OnePoint X)
⊢ ↑f ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed s → IsCompact s → some '' s ∉ f

Tactic:
simp only [le_nhds_infty, ← compl_image_coe, Ultrafilter.mem_coe,
  Ultrafilter.compl_mem_iff_not_mem]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
lemma self_comp_coPolarization_eq_corootForm :
    P.toLin ∘ₗ P.CoPolarization = P.CorootForm

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
⊢ P.toLin ∘ₗ P.CoPolarization = P.CorootForm

Tactic:
ext

Result:
case h.h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x✝¹ x✝ : N
⊢ ((P.toLin ∘ₗ P.CoPolarization) x✝¹) x✝ = (P.CorootForm x✝¹) x✝

Proof state:
case h.h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x✝¹ x✝ : N
⊢ ((P.toLin ∘ₗ P.CoPolarization) x✝¹) x✝ = (P.CorootForm x✝¹) x✝

Tactic:
simp [corootForm_apply_apply]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem mem_Ici_Ioi_of_subset_of_subset {s : Set α} (ho : Ioi a ⊆ s) (hc : s ⊆ Ici a) :
    s ∈ ({Ici a, Ioi a} : Set (Set α)) :=
  by_cases
    (fun h : a ∈ s =>
      Or.inl <| Subset.antisymm hc <| by rw [← Ioi_union_left, union_subset_iff]; simp [*])
    fun h =>
    Or.inr <| Subset.antisymm (fun _ hx => lt_of_le_of_ne (hc hx) fun heq => h <| heq.symm ▸ hx) ho

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
ho : Ioi a ⊆ s
hc : s ⊆ Ici a
h : a ∈ s
⊢ Ici a ⊆ s

Tactic:
rw [← Ioi_union_left, union_subset_iff]

Result:
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
ho : Ioi a ⊆ s
hc : s ⊆ Ici a
h : a ∈ s
⊢ Ioi a ⊆ s ∧ {a} ⊆ s

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
ho : Ioi a ⊆ s
hc : s ⊆ Ici a
h : a ∈ s
⊢ Ioi a ⊆ s ∧ {a} ⊆ s

Tactic:
simp [*]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
/-- Right-exactness of tensor product -/
lemma lTensor_mkQ (N : Submodule R M) :
    ker (lTensor Q (N.mkQ)) = range (lTensor Q N.subtype)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
N : Submodule R M
⊢ ker (lTensor Q N.mkQ) = range (lTensor Q N.subtype)

Tactic:
rw [← exact_iff]

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
N : Submodule R M
⊢ Exact ⇑(lTensor Q N.subtype) ⇑(lTensor Q N.mkQ)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
N : Submodule R M
⊢ Exact ⇑(lTensor Q N.subtype) ⇑(lTensor Q N.mkQ)

Tactic:
exact lTensor_exact Q (LinearMap.exact_subtype_mkQ N) (Submodule.mkQ_surjective N)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem State.eval_eq : State.eval assign state = state.cnf.eval assign

Proof state:
aig✝ : AIG Nat
assign : aig✝.CNFVar → Bool
state : State aig✝
⊢ eval assign state = CNF.eval assign state.cnf

Tactic:
simp [State.eval]

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Basic.lean
theorem pointReflection_fixed_iff_of_injective_two_nsmul {x y : P} (h : Injective (2 • · : G → G)) :
    pointReflection x y = y ↔ y = x

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
h : Injective fun x => 2 • x
⊢ (pointReflection x) y = y ↔ y = x

Tactic:
rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
  neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem wSameSide_vadd_right_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
    s.WSameSide x (v +ᵥ y) ↔ s.WSameSide x y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WSameSide x (v +ᵥ y) ↔ s.WSameSide x y

Tactic:
rw [wSameSide_comm, wSameSide_vadd_left_iff hv, wSameSide_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@[simp] lemma rpow_rpow_inv {y : ℝ} (hy : y ≠ 0) (x : ℝ≥0) : (x ^ y) ^ y⁻¹ = x

Proof state:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ y) ^ y⁻¹ = x

Tactic:
rw [← rpow_mul, mul_inv_cancel₀ hy, rpow_one]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_eq_one_iff_exists : Nat.card α = 1 ↔ ∃ x : α, ∀ y : α, y = x

Proof state:
α : Type u_1
⊢ Nat.card α = 1 ↔ ∃ x, ∀ (y : α), y = x

Tactic:
rw [card_eq_one_iff_unique]

Result:
α : Type u_1
⊢ Subsingleton α ∧ Nonempty α ↔ ∃ x, ∀ (y : α), y = x

Proof state:
α : Type u_1
⊢ Subsingleton α ∧ Nonempty α ↔ ∃ x, ∀ (y : α), y = x

Tactic:
exact ⟨fun ⟨s, ⟨a⟩⟩ ↦ ⟨a, fun x ↦ s.elim x a⟩, fun ⟨x, h⟩ ↦ ⟨subsingleton_of_forall_eq x h, ⟨x⟩⟩⟩

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

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

Tactic:
rw [← inner_conj_symm, conj_re]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Slope.lean
theorem range_deriv_subset_closure_span_image
    (f : 𝕜 → F) {t : Set 𝕜} (h : Dense t) :
    range (deriv f) ⊆ closure (Submodule.span 𝕜 (f '' t))

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
h : Dense t
⊢ range (deriv f) ⊆ closure ↑(Submodule.span 𝕜 (f '' t))

Tactic:
rw [← derivWithin_univ]

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
h : Dense t
⊢ range (derivWithin f univ) ⊆ closure ↑(Submodule.span 𝕜 (f '' t))

Proof state:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
h : Dense t
⊢ univ ⊆ closure (univ ∩ t)

Tactic:
simp [dense_iff_closure_eq.1 h]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
h : Dense t
⊢ range (derivWithin f univ) ⊆ closure ↑(Submodule.span 𝕜 (f '' t))

Tactic:
apply range_derivWithin_subset_closure_span_image

Result:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
h : Dense t
⊢ univ ⊆ closure (univ ∩ t)
-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
theorem Summable.ofStar (hf : Summable fun b ↦ Star.star (f b)) : Summable f

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : StarAddMonoid α
inst✝ : ContinuousStar α
f : β → α
hf : Summable fun b => Star.star (f b)
⊢ Summable f

Tactic:
simpa only [star_star] using hf.star

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem if_false_left  (p : Prop) [h : Decidable p] (f : Bool) :
    (ite p false f) = (!p && f)

Proof state:
p : Prop
h : Decidable p
f : Bool
⊢ (if p then false else f) = (!decide p && f)

Tactic:
cases h with | _ p => simp [p]

Result:
no goals

Proof state:
case isTrue
p✝ : Prop
f : Bool
p : p✝
⊢ (if p✝ then false else f) = (!decide p✝ && f)

Tactic:
simp [p]

Result:
no goals