harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem coconePointsIsoOfNatIso_hom_desc {F G : J ⥤ C} {s : Cocone F} {r t : Cocone G}
    (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) :
    (coconePointsIsoOfNatIso P Q w).hom ≫ Q.desc r = P.map _ w.hom :=
  P.hom_ext (by simp)

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F G : J ⥤ C
s : Cocone F
r t : Cocone G
P : IsColimit s
Q : IsColimit t
w : F ≅ G
⊢ ∀ (j : J), s.ι.app j ≫ (P.coconePointsIsoOfNatIso Q w).hom ≫ Q.desc r = s.ι.app j ≫ P.map r w.hom

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem emem_iff_mem_toList {x : α} {t} : Emem x t ↔ x ∈ toList t

Proof state:
α : Type u_1
x : α
t : Ordnode α
⊢ Emem x t ↔ x ∈ t.toList

Tactic:
unfold Emem

Result:
α : Type u_1
x : α
t : Ordnode α
⊢ Any (Eq x) t ↔ x ∈ t.toList

Proof state:
α : Type u_1
x : α
t : Ordnode α
⊢ Any (Eq x) t ↔ x ∈ t.toList

Tactic:
induction t <;> simp [Any, *, or_assoc]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem ind {β : X[S⁻¹] → Prop}
    (c : ∀ (r : X) (s : S), β (r /ₒ s)) : ∀ q, β q

Proof state:
case a
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
β : OreLocalization S X → Prop
c : ∀ (r : X) (s : ↥S), β (r /ₒ s)
⊢ ∀ (a : X × ↥S), β ⟦a⟧

Tactic:
rintro ⟨r, s⟩

Result:
case a.mk
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
β : OreLocalization S X → Prop
c : ∀ (r : X) (s : ↥S), β (r /ₒ s)
r : X
s : ↥S
⊢ β ⟦(r, s)⟧

Proof state:
case a.mk
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
β : OreLocalization S X → Prop
c : ∀ (r : X) (s : ↥S), β (r /ₒ s)
r : X
s : ↥S
⊢ β ⟦(r, s)⟧

Tactic:
exact c r s

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
β : OreLocalization S X → Prop
c : ∀ (r : X) (s : ↥S), β (r /ₒ s)
⊢ ∀ (q : OreLocalization S X), β q

Tactic:
apply Quotient.ind

Result:
case a
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
β : OreLocalization S X → Prop
c : ∀ (r : X) (s : ↥S), β (r /ₒ s)
⊢ ∀ (a : X × ↥S), β ⟦a⟧
-- Mathlib/Order/SupClosed.lean
protected lemma InfClosed.supClosure (hs : InfClosed s) : InfClosed (supClosure s)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : InfClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ t.sup' ht id ⊓ u.sup' hu id ∈ supClosure s

Tactic:
rw [sup'_inf_sup']

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : InfClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ((t ×ˢ u).sup' ⋯ fun i => id i.1 ⊓ id i.2) ∈ supClosure s

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : InfClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ((t ×ˢ u).sup' ⋯ fun i => id i.1 ⊓ id i.2) ∈ supClosure s

Tactic:
exact finsetSup'_mem_supClosure _
  fun i hi ↦ hs (hts (mem_product.1 hi).1) (hus (mem_product.1 hi).2)

Result:
no goals

Proof state:
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : InfClosed s
⊢ InfClosed (supClosure s)

Tactic:
rintro _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : InfClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ t.sup' ht id ⊓ u.sup' hu id ∈ supClosure s
-- Mathlib/Data/Option/NAry.lean
theorem map₂_def {α β γ : Type u} (f : α → β → γ) (a : Option α) (b : Option β) :
    map₂ f a b = f <$> a <*> b

Proof state:
α β γ : Type u
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = f <$> a <*> b

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem Chain.imp' {R S : α → α → Prop} (HRS : ∀ ⦃a b⦄, R a b → S a b) {a b : α}
    (Hab : ∀ ⦃c⦄, R a c → S b c) {l : List α} (p : Chain R a l) : Chain S b l

Proof state:
case nil
α : Type u_1
R S : α → α → Prop
HRS : ∀ ⦃a b : α⦄, R a b → S a b
a : α
l : List α
a✝ b : α
Hab : ∀ ⦃c : α⦄, R a✝ c → S b c
⊢ Chain S b []

Tactic:
constructor

Result:
no goals

Proof state:
case cons
α : Type u_1
R S : α → α → Prop
HRS : ∀ ⦃a b : α⦄, R a b → S a b
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
ih : ∀ {b : α}, (∀ ⦃c : α⦄, R b✝ c → S b c) → Chain S b l✝
b : α
Hab : ∀ ⦃c : α⦄, R a✝¹ c → S b c
⊢ Chain S b (b✝ :: l✝)

Tactic:
constructor

Result:
case cons.a
α : Type u_1
R S : α → α → Prop
HRS : ∀ ⦃a b : α⦄, R a b → S a b
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
ih : ∀ {b : α}, (∀ ⦃c : α⦄, R b✝ c → S b c) → Chain S b l✝
b : α
Hab : ∀ ⦃c : α⦄, R a✝¹ c → S b c
⊢ S b b✝

case cons.a
α : Type u_1
R S : α → α → Prop
HRS : ∀ ⦃a b : α⦄, R a b → S a b
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
ih : ∀ {b : α}, (∀ ⦃c : α⦄, R b✝ c → S b c) → Chain S b l✝
b : α
Hab : ∀ ⦃c : α⦄, R a✝¹ c → S b c
⊢ Chain S b✝ l✝

Proof state:
case cons.a
α : Type u_1
R S : α → α → Prop
HRS : ∀ ⦃a b : α⦄, R a b → S a b
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
ih : ∀ {b : α}, (∀ ⦃c : α⦄, R b✝ c → S b c) → Chain S b l✝
b : α
Hab : ∀ ⦃c : α⦄, R a✝¹ c → S b c
⊢ S b b✝

Tactic:
exact Hab r

Result:
no goals

Proof state:
case cons.a
α : Type u_1
R S : α → α → Prop
HRS : ∀ ⦃a b : α⦄, R a b → S a b
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
ih : ∀ {b : α}, (∀ ⦃c : α⦄, R b✝ c → S b c) → Chain S b l✝
b : α
Hab : ∀ ⦃c : α⦄, R a✝¹ c → S b c
⊢ Chain S b✝ l✝

Tactic:
exact ih (@HRS _)

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
lemma condExp_nonneg (hf : 0 ≤ᵐ[μ] f) : 0 ≤ᵐ[μ] μ[f|m]

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : 0 ≤ᶠ[ae μ] f
⊢ 0 ≤ᶠ[ae μ] μ[f|m]

Tactic:
by_cases hfint : Integrable f μ

Result:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : 0 ≤ᶠ[ae μ] f
hfint : Integrable f μ
⊢ 0 ≤ᶠ[ae μ] μ[f|m]

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : 0 ≤ᶠ[ae μ] f
hfint : ¬Integrable f μ
⊢ 0 ≤ᶠ[ae μ] μ[f|m]

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : 0 ≤ᶠ[ae μ] f
hfint : Integrable f μ
⊢ μ[0|m] ≤ᶠ[ae μ] μ[f|m]

Tactic:
exact condExp_mono (integrable_zero _ _ _) hfint hf

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : 0 ≤ᶠ[ae μ] f
hfint : Integrable f μ
⊢ 0 ≤ᶠ[ae μ] μ[f|m]

Tactic:
rw [(condExp_zero.symm : (0 : α → E) = μ[0|m])]

Result:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : 0 ≤ᶠ[ae μ] f
hfint : Integrable f μ
⊢ μ[0|m] ≤ᶠ[ae μ] μ[f|m]

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : 0 ≤ᶠ[ae μ] f
hfint : ¬Integrable f μ
⊢ 0 ≤ᶠ[ae μ] μ[f|m]

Tactic:
rw [condExp_of_not_integrable hfint]

Result:
no goals
-- Mathlib/RingTheory/Trace/Basic.lean
lemma Algebra.trace_eq_of_algEquiv {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
    [Algebra A B] [Algebra A C] (e : B ≃ₐ[A] C) (x) :
    Algebra.trace A C (e x) = Algebra.trace A B x

Proof state:
case h.e_6.h
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
⊢ (lmul A C) (e x) = e.toLinearEquiv.conj ((lmul A B) x)

Tactic:
ext

Result:
case h.e_6.h.h
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
x✝ : C
⊢ ((lmul A C) (e x)) x✝ = (e.toLinearEquiv.conj ((lmul A B) x)) x✝

Proof state:
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
⊢ (trace A C) (e x) = (trace A B) x

Tactic:
simp_rw [Algebra.trace_apply, ← LinearMap.trace_conj' _ e.toLinearEquiv]

Result:
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
⊢ (LinearMap.trace A C) ((lmul A C) (e x)) = (LinearMap.trace A C) (e.toLinearEquiv.conj ((lmul A B) x))

Proof state:
case h.e_6.h.h
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
x✝ : C
⊢ ((lmul A C) (e x)) x✝ = (e.toLinearEquiv.conj ((lmul A B) x)) x✝

Tactic:
simp [LinearEquiv.conj_apply]

Result:
no goals

Proof state:
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
⊢ (LinearMap.trace A C) ((lmul A C) (e x)) = (LinearMap.trace A C) (e.toLinearEquiv.conj ((lmul A B) x))

Tactic:
congr

Result:
case h.e_6.h
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
⊢ (lmul A C) (e x) = e.toLinearEquiv.conj ((lmul A B) x)
-- Mathlib/RingTheory/PowerBasis.lean
theorem adjoin_gen_eq_top (B : PowerBasis R S) : adjoin R ({B.gen} : Set S) = ⊤

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
⊢ Set.range ⇑B.basis ⊆ ↑(Subalgebra.toSubmodule (adjoin R {B.gen}))

Tactic:
rintro x ⟨i, rfl⟩

Result:
case intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
i : Fin B.dim
⊢ B.basis i ∈ ↑(Subalgebra.toSubmodule (adjoin R {B.gen}))

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
i : Fin B.dim
⊢ B.gen ^ ↑i ∈ ↑(Subalgebra.toSubmodule (adjoin R {B.gen}))

Tactic:
exact Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
⊢ adjoin R {B.gen} = ⊤

Tactic:
rw [← toSubmodule_eq_top, _root_.eq_top_iff, ← B.basis.span_eq, Submodule.span_le]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
⊢ Set.range ⇑B.basis ⊆ ↑(Subalgebra.toSubmodule (adjoin R {B.gen}))

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
i : Fin B.dim
⊢ B.basis i ∈ ↑(Subalgebra.toSubmodule (adjoin R {B.gen}))

Tactic:
rw [B.basis_eq_pow i]

Result:
case intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
i : Fin B.dim
⊢ B.gen ^ ↑i ∈ ↑(Subalgebra.toSubmodule (adjoin R {B.gen}))
-- Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
theorem ContMDiffWithinAt.div {f g : M → G} {s : Set M} {x₀ : M}
    (hf : ContMDiffWithinAt I' I n f s x₀) (hg : ContMDiffWithinAt I' I n g s x₀) :
    ContMDiffWithinAt I' I n (fun x => f x / g x) s x₀

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : WithTop ℕ∞
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : LieGroup I n G
f g : M → G
s : Set M
x₀ : M
hf : ContMDiffWithinAt I' I n f s x₀
hg : ContMDiffWithinAt I' I n g s x₀
⊢ ContMDiffWithinAt I' I n (fun x => f x / g x) s x₀

Tactic:
simp_rw [div_eq_mul_inv]

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : WithTop ℕ∞
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : LieGroup I n G
f g : M → G
s : Set M
x₀ : M
hf : ContMDiffWithinAt I' I n f s x₀
hg : ContMDiffWithinAt I' I n g s x₀
⊢ ContMDiffWithinAt I' I n (fun x => f x * (g x)⁻¹) s x₀

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : WithTop ℕ∞
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : LieGroup I n G
f g : M → G
s : Set M
x₀ : M
hf : ContMDiffWithinAt I' I n f s x₀
hg : ContMDiffWithinAt I' I n g s x₀
⊢ ContMDiffWithinAt I' I n (fun x => f x * (g x)⁻¹) s x₀

Tactic:
exact hf.mul hg.inv

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_eq_one_iff_eq_X_pow_sub_C : (minpoly F x).natSepDegree = 1 ↔
    ∃ (n : ℕ) (y : F), minpoly F x = X ^ q ^ n - C y

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ (minpoly F x).natSepDegree = 1 ↔ ∃ n y, minpoly F x = X ^ q ^ n - C y

Tactic:
simp only [minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C q, map_sub, expand_X, expand_C]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/LinearMap.lean
theorem inner_map_polarization' (T : V →ₗ[ℂ] V) (x y : V) :
    ⟪T x, y⟫_ℂ =
      (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ -
            Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ +
          Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
        4

Proof state:
V : Type u_4
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ - Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ +
        Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
      4

Tactic:
simp only [map_add, map_sub, inner_add_left, inner_add_right, LinearMap.map_smul, inner_smul_left,
  inner_smul_right, Complex.conj_I, ← pow_two, Complex.I_sq, inner_sub_left, inner_sub_right,
  mul_add, ← mul_assoc, mul_neg, neg_neg, sub_neg_eq_add, one_mul, neg_one_mul, mul_sub, sub_sub]

Result:
V : Type u_4
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (⟪T x, x⟫_ℂ + ⟪T y, x⟫_ℂ + (⟪T x, y⟫_ℂ + ⟪T y, y⟫_ℂ) -
          (⟪T x, x⟫_ℂ - (⟪T y, x⟫_ℂ + (⟪T x, y⟫_ℂ - ⟪T y, y⟫_ℂ)) +
            (Complex.I * ⟪T x, x⟫_ℂ + ⟪T y, x⟫_ℂ + (-⟪T x, y⟫_ℂ + Complex.I * ⟪T y, y⟫_ℂ))) +
        (Complex.I * ⟪T x, x⟫_ℂ - (⟪T y, x⟫_ℂ + (-⟪T x, y⟫_ℂ - Complex.I * ⟪T y, y⟫_ℂ)))) /
      4

Proof state:
V : Type u_4
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (⟪T x, x⟫_ℂ + ⟪T y, x⟫_ℂ + (⟪T x, y⟫_ℂ + ⟪T y, y⟫_ℂ) -
          (⟪T x, x⟫_ℂ - (⟪T y, x⟫_ℂ + (⟪T x, y⟫_ℂ - ⟪T y, y⟫_ℂ)) +
            (Complex.I * ⟪T x, x⟫_ℂ + ⟪T y, x⟫_ℂ + (-⟪T x, y⟫_ℂ + Complex.I * ⟪T y, y⟫_ℂ))) +
        (Complex.I * ⟪T x, x⟫_ℂ - (⟪T y, x⟫_ℂ + (-⟪T x, y⟫_ℂ - Complex.I * ⟪T y, y⟫_ℂ)))) /
      4

Tactic:
ring

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Bousfield.lean
lemma W_eq_inverseImage_isomorphisms :
    W (· ∈ Set.range F.obj) = (MorphismProperty.isomorphisms _).inverseImage G

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (W fun x => x ∈ Set.range F.obj) = (MorphismProperty.isomorphisms C).inverseImage G

Tactic:
ext P₁ P₂ f

Result:
case h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
P₁ P₂ : D
f : P₁ ⟶ P₂
⊢ W (fun x => x ∈ Set.range F.obj) f ↔ (MorphismProperty.isomorphisms C).inverseImage G f

Proof state:
case h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
P₁ P₂ : D
f : P₁ ⟶ P₂
⊢ W (fun x => x ∈ Set.range F.obj) f ↔ (MorphismProperty.isomorphisms C).inverseImage G f

Tactic:
rw [W_iff_isIso_map adj]

Result:
case h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
P₁ P₂ : D
f : P₁ ⟶ P₂
⊢ IsIso (G.map f) ↔ (MorphismProperty.isomorphisms C).inverseImage G f

Proof state:
case h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
P₁ P₂ : D
f : P₁ ⟶ P₂
⊢ IsIso (G.map f) ↔ (MorphismProperty.isomorphisms C).inverseImage G f

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem rel_map_right {s : Multiset α} {t : Multiset γ} {f : γ → β} :
    Rel r s (t.map f) ↔ Rel (fun a b => r a (f b)) s t

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel r s (map f t) ↔ Rel (fun a b => r a (f b)) s t

Tactic:
rw [← rel_flip, rel_map_left, ← rel_flip]

Result:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel (flip fun a b => flip r (f a) b) s t ↔ Rel (fun a b => r a (f b)) s t

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel (flip fun a b => flip r (f a) b) s t ↔ Rel (fun a b => r a (f b)) s t

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma upperBounds_supClosure (s : Set α) : upperBounds (supClosure s) = upperBounds s :=
  (upperBounds_mono_set subset_supClosure).antisymm <| by
    rintro a ha _ ⟨t, ht, hts, rfl⟩
    exact sup'_le _ _ fun b hb ↦ ha <| hts hb

Proof state:
case intro.intro.intro
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
ha : a ∈ upperBounds s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
⊢ t.sup' ht id ≤ a

Tactic:
exact sup'_le _ _ fun b hb ↦ ha <| hts hb

Result:
no goals

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
⊢ upperBounds s ⊆ upperBounds (supClosure s)

Tactic:
rintro a ha _ ⟨t, ht, hts, rfl⟩

Result:
case intro.intro.intro
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
ha : a ∈ upperBounds s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
⊢ t.sup' ht id ≤ a
-- Mathlib/Data/Real/Irrational.lean
theorem rat_add (h : Irrational x) : Irrational (q + x) :=
  of_rat_add (-q) <| by rwa [cast_neg, neg_add_cancel_left]

Proof state:
q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (↑(-q) + (↑q + x))

Tactic:
rwa [cast_neg, neg_add_cancel_left]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive] lemma mabs_sup_div_sup_le_mabs (a b c : α) : |(a ⊔ c) / (b ⊔ c)|ₘ ≤ |a / b|ₘ

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ mabs ((a ⊔ c) / (b ⊔ c)) ≤ mabs (a / b)

Tactic:
apply le_of_mul_le_of_one_le_left _ (one_le_mabs _)

Result:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ mabs ((a ⊔ c) / (b ⊔ c)) * mabs ?m.23207 ≤ mabs (a / b)

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ mabs ((a ⊔ c) / (b ⊔ c)) * mabs ?m.23207 ≤ mabs (a / b)

Tactic:
rw [mabs_div_sup_mul_mabs_div_inf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
theorem denote_blastShiftConcat_eq_shiftConcat (aig : AIG α) (target : ShiftConcatInput aig w)
  (x : BitVec w) (b : Bool) (assign : α → Bool)
  (hx : ∀ idx hidx, ⟦aig, target.lhs.get idx hidx, assign⟧ = x.getLsbD idx)
  (hb : ⟦aig, target.bit, assign⟧ = b) :
  ∀ (idx : Nat) (hidx : idx < w),
      ⟦(blastShiftConcat aig target).aig, (blastShiftConcat aig target).vec.get idx hidx, assign⟧
        =
      (BitVec.shiftConcat x b).getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : ShiftConcatInput aig w
x : BitVec w
b : Bool
assign : α → Bool
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.lhs.get idx hidx }⟧ = x.getLsbD idx
hb : ⟦assign, { aig := aig, ref := target.bit }⟧ = b
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (blastShiftConcat aig target).aig, ref := (blastShiftConcat aig target).vec.get idx hidx }⟧ =
    (x.shiftConcat b).getLsbD idx

Tactic:
simp [BitVec.getLsbD_shiftConcat, hidx, denote_blastShiftConcat, hx, hb]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : ShiftConcatInput aig w
x : BitVec w
b : Bool
assign : α → Bool
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.lhs.get idx hidx }⟧ = x.getLsbD idx
hb : ⟦assign, { aig := aig, ref := target.bit }⟧ = b
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := (blastShiftConcat aig target).aig, ref := (blastShiftConcat aig target).vec.get idx hidx }⟧ =
      (x.shiftConcat b).getLsbD idx

Tactic:
intro idx hidx

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : ShiftConcatInput aig w
x : BitVec w
b : Bool
assign : α → Bool
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.lhs.get idx hidx }⟧ = x.getLsbD idx
hb : ⟦assign, { aig := aig, ref := target.bit }⟧ = b
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (blastShiftConcat aig target).aig, ref := (blastShiftConcat aig target).vec.get idx hidx }⟧ =
    (x.shiftConcat b).getLsbD idx
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem le_mul_right (a : Ordinal) {b : Ordinal} (hb : 0 < b) : a ≤ b * a

Proof state:
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a ≤ b * a

Tactic:
convert mul_le_mul_right' (one_le_iff_pos.2 hb) a

Result:
case h.e'_3
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a = 1 * a

Proof state:
case h.e'_3
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a = 1 * a

Tactic:
rw [one_mul a]

Result:
no goals
-- Mathlib/Order/Filter/Finite.lean
theorem eventually_all_finite {ι} {I : Set ι} (hI : I.Finite) {l} {p : ι → α → Prop} :
    (∀ᶠ x in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ x in l, p i x

Proof state:
α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
⊢ (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x

Tactic:
simpa only [Filter.Eventually, setOf_forall] using biInter_mem hI

Result:
no goals