harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma add_of_Y_ne' {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3) :
    W.add P Q = W.dblZ P •
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ W.add P Q =
    W.dblZ P •
      ![(toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        (toAffine W).addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Tactic:
rw [add, if_pos <| equiv_of_X_eq_of_Y_eq hPz hQz hx <| Y_eq_of_Y_ne' hP hQ hx hy,
  dblXYZ_of_Z_ne_zero hP hQ hPz hQz hx hy]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem getLeft?_swap (x : α ⊕ β) : x.swap.getLeft? = x.getRight?

Proof state:
α : Type u_1
β : Type u_2
x : α ⊕ β
⊢ x.swap.getLeft? = x.getRight?

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem norm_eq_of_nonempty [h : Nonempty α] : ‖f‖ = sInf { C : ℝ | ∀ x : α, ‖f x‖ ≤ C }

Proof state:
case intro.e_a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
⊢ {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C} = {C | ∀ (x : α), ‖f x‖ ≤ C}

Tactic:
ext

Result:
case intro.e_a.h
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
x✝ : ℝ
⊢ x✝ ∈ {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C} ↔ x✝ ∈ {C | ∀ (x : α), ‖f x‖ ≤ C}

Proof state:
case intro.e_a.h
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
x✝ : ℝ
⊢ x✝ ∈ {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C} ↔ x✝ ∈ {C | ∀ (x : α), ‖f x‖ ≤ C}

Tactic:
simp only [mem_setOf_eq, and_iff_right_iff_imp]

Result:
case intro.e_a.h
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
x✝ : ℝ
⊢ (∀ (x : α), ‖f x‖ ≤ x✝) → 0 ≤ x✝

Proof state:
case intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C} = sInf {C | ∀ (x : α), ‖f x‖ ≤ C}

Tactic:
congr

Result:
case intro.e_a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
⊢ {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C} = {C | ∀ (x : α), ‖f x‖ ≤ C}

Proof state:
case intro.e_a.h
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
x✝ : ℝ
⊢ (∀ (x : α), ‖f x‖ ≤ x✝) → 0 ≤ x✝

Tactic:
exact fun h' => le_trans (norm_nonneg (f a)) (h' a)

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
h : Nonempty α
⊢ ‖f‖ = sInf {C | ∀ (x : α), ‖f x‖ ≤ C}

Tactic:
obtain ⟨a⟩ := h

Result:
case intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
⊢ ‖f‖ = sInf {C | ∀ (x : α), ‖f x‖ ≤ C}

Proof state:
case intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
⊢ ‖f‖ = sInf {C | ∀ (x : α), ‖f x‖ ≤ C}

Tactic:
rw [norm_eq]

Result:
case intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C} = sInf {C | ∀ (x : α), ‖f x‖ ≤ C}
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
theorem toLin_restrict_ker_eq_inf_orthogonal (B : BilinForm K V) (W : Subspace K V) (b : B.IsRefl) :
    (B.domRestrict W).ker.map W.subtype = (W ⊓ B.orthogonal ⊤ : Subspace K V)

Proof state:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
⊢ Submodule.map (Submodule.subtype W) (ker (domRestrict B W)) = W ⊓ B.orthogonal ⊤

Tactic:
ext x

Result:
case h
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
⊢ x ∈ Submodule.map (Submodule.subtype W) (ker (domRestrict B W)) ↔ x ∈ W ⊓ B.orthogonal ⊤

Proof state:
case h.mp.intro.mk.intro.right
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
y : V
a✝ : y ∈ ⊤
⊢ B.IsOrtho y ((Submodule.subtype W) ⟨x, hx⟩)

Tactic:
rw [IsOrtho, b]

Result:
case h.mp.intro.mk.intro.right.a
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
y : V
a✝ : y ∈ ⊤
⊢ (B ((Submodule.subtype W) ⟨x, hx⟩)) y = 0

Proof state:
case h.mp.intro.mk.intro.left
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
x : V
hx : x ∈ W
hker : (domRestrict B W) ⟨x, hx⟩ = 0
⊢ (Submodule.subtype W) ⟨x, hx⟩ ∈ ↑W

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma map_comp_cotangentComplex_baseChange :
    (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom).liftBaseChange T ∘ₗ
      P.toExtension.cotangentComplex.baseChange T =
    (Q.comp P).toExtension.cotangentComplex ∘ₗ
      (Extension.Cotangent.map (Q.toComp P).toExtensionHom).liftBaseChange T

Proof state:
case a.h.h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : P.toExtension.Cotangent
⊢ ((AlgebraTensorModule.curry
          (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) ∘ₗ
            LinearMap.baseChange T P.toExtension.cotangentComplex))
        1)
      x =
    ((AlgebraTensorModule.curry
          ((Q.comp P).toExtension.cotangentComplex ∘ₗ
            LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)))
        1)
      x

Tactic:
simp [Extension.CotangentSpace.map_cotangentComplex]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) ∘ₗ
      LinearMap.baseChange T P.toExtension.cotangentComplex =
    (Q.comp P).toExtension.cotangentComplex ∘ₗ
      LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)

Tactic:
ext x

Result:
case a.h.h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : P.toExtension.Cotangent
⊢ ((AlgebraTensorModule.curry
          (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) ∘ₗ
            LinearMap.baseChange T P.toExtension.cotangentComplex))
        1)
      x =
    ((AlgebraTensorModule.curry
          ((Q.comp P).toExtension.cotangentComplex ∘ₗ
            LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)))
        1)
      x
-- Mathlib/Data/Nat/BinaryRec.lean
theorem bit_div_two (b n) : bit b n / 2 = n

Proof state:
b : Bool
n : Nat
⊢ b.toNat < 2

Tactic:
cases b <;> decide

Result:
no goals

Proof state:
case H
b : Bool
n : Nat
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
b : Bool
n : Nat
⊢ bit b n / 2 = n

Tactic:
rw [bit_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]

Result:
b : Bool
n : Nat
⊢ b.toNat < 2

case H
b : Bool
n : Nat
⊢ 0 < 2
-- Mathlib/Topology/Constructions.lean
theorem map_snd_nhdsWithin (x : X × Y) : map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x) = 𝓝 x.2

Proof state:
case mk
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.fst ⁻¹' {(x, y).1} → x_1 ∈ Prod.snd ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).2

Tactic:
rcases hs with ⟨u, hu, v, hv, H⟩

Result:
case mk.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H : u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.fst ⁻¹' {(x, y).1} → x_1 ∈ Prod.snd ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).2

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X × Y
s : Set Y
hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x)
⊢ s ∈ 𝓝 x.2

Tactic:
rcases x with ⟨x, y⟩

Result:
case mk
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {(x, y).1}] (x, y))
⊢ s ∈ 𝓝 (x, y).2

Proof state:
case mk
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {(x, y).1}] (x, y))
⊢ s ∈ 𝓝 (x, y).2

Tactic:
rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs

Result:
case mk
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.fst ⁻¹' {(x, y).1} → x_1 ∈ Prod.snd ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).2

Proof state:
case mk.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H : ∀ x_1 ∈ u, ∀ y ∈ v, x_1 = x → y ∈ s
⊢ s ∈ 𝓝 (x, y).2

Tactic:
exact mem_of_superset hv fun z hz => H _ (mem_of_mem_nhds hu) _ hz rfl

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X × Y
⊢ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x) = 𝓝 x.2

Tactic:
refine le_antisymm (continuousAt_snd.mono_left inf_le_left) fun s hs => ?_

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X × Y
s : Set Y
hs : s ∈ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x)
⊢ s ∈ 𝓝 x.2

Proof state:
case mk.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H : u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.fst ⁻¹' {(x, y).1} → x_1 ∈ Prod.snd ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).2

Tactic:
simp only [prod_subset_iff, mem_singleton_iff, mem_setOf_eq, mem_preimage] at H

Result:
case mk.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H : ∀ x_1 ∈ u, ∀ y ∈ v, x_1 = x → y ∈ s
⊢ s ∈ 𝓝 (x, y).2
-- Mathlib/Analysis/RCLike/Basic.lean
theorem inv_def (z : K) : z⁻¹ = conj z * ((‖z‖ ^ 2)⁻¹ : ℝ)

Proof state:
case inr.a
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ ↑‖z‖ ^ 2 ≠ 0

Tactic:
simpa

Result:
no goals

Proof state:
case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹

Tactic:
apply inv_eq_of_mul_eq_one_right

Result:
case inr.a
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z * ((starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹) = 1

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹

Tactic:
rcases eq_or_ne z 0 with (rfl | h₀)

Result:
case inl
K : Type u_1
inst✝ : RCLike K
⊢ 0⁻¹ = (starRingEnd K) 0 * ↑(‖0‖ ^ 2)⁻¹

case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹

Proof state:
case inr.a
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z * ((starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹) = 1

Tactic:
rw [← mul_assoc, mul_conj, ofReal_inv, ofReal_pow, mul_inv_cancel₀]

Result:
case inr.a
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ ↑‖z‖ ^ 2 ≠ 0

Proof state:
case inl
K : Type u_1
inst✝ : RCLike K
⊢ 0⁻¹ = (starRingEnd K) 0 * ↑(‖0‖ ^ 2)⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem filter_cons {a : α} (s : Multiset α) :
    filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s

Proof state:
case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ filter p (a ::ₘ s) = {a} + filter p s

Tactic:
rw [filter_cons_of_pos _ h, singleton_add]

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ filter p (a ::ₘ s) = {a} + filter p s

case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ filter p (a ::ₘ s) = 0 + filter p s

Proof state:
case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ filter p (a ::ₘ s) = 0 + filter p s

Tactic:
rw [filter_cons_of_neg _ h, Multiset.zero_add]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean
theorem starLift_range (f : A →⋆ₙₐ[R] C) :
    (starLift f).range = StarAlgebra.adjoin R (NonUnitalStarAlgHom.range f : Set C) :=
  eq_of_forall_ge_iff fun c ↦ by
    rw [starLift_range_le, StarAlgebra.adjoin_le_iff]
    rfl

Proof state:
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
c : StarSubalgebra R C
⊢ (starLift f).range ≤ c ↔ StarAlgebra.adjoin R ↑(NonUnitalStarAlgHom.range f) ≤ c

Tactic:
rw [starLift_range_le, StarAlgebra.adjoin_le_iff]

Result:
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
c : StarSubalgebra R C
⊢ NonUnitalStarAlgHom.range f ≤ c.toNonUnitalStarSubalgebra ↔ ↑(NonUnitalStarAlgHom.range f) ⊆ ↑c

Proof state:
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
c : StarSubalgebra R C
⊢ NonUnitalStarAlgHom.range f ≤ c.toNonUnitalStarSubalgebra ↔ ↑(NonUnitalStarAlgHom.range f) ⊆ ↑c

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1)

Proof state:
case zero.inr
x : Nat
xz : x % 2 = 1
⊢ (1 &&& x >>> 0 != 0) = decide (x / 2 ^ 0 % 2 = 1)

Tactic:
simp [xz]

Result:
no goals

Proof state:
case zero
x : Nat
⊢ (1 &&& x >>> 0 != 0) = decide (x / 2 ^ 0 % 2 = 1)

Tactic:
cases mod_two_eq_zero_or_one x with | _ xz => simp [xz]

Result:
no goals

Proof state:
case zero
x : Nat
⊢ x.testBit 0 = decide (x / 2 ^ 0 % 2 = 1)

Tactic:
unfold testBit

Result:
case zero
x : Nat
⊢ (1 &&& x >>> 0 != 0) = decide (x / 2 ^ 0 % 2 = 1)

Proof state:
i x : Nat
⊢ x.testBit i = decide (x / 2 ^ i % 2 = 1)

Tactic:
induction i generalizing x with
| zero =>
  unfold testBit
  cases mod_two_eq_zero_or_one x with | _ xz => simp [xz]
| succ i hyp =>
  simp [hyp, Nat.div_div_eq_div_mul, Nat.pow_succ']

Result:
no goals

Proof state:
case succ
i : Nat
hyp : ∀ {x : Nat}, x.testBit i = decide (x / 2 ^ i % 2 = 1)
x : Nat
⊢ x.testBit (i + 1) = decide (x / 2 ^ (i + 1) % 2 = 1)

Tactic:
simp [hyp, Nat.div_div_eq_div_mul, Nat.pow_succ']

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem prod_dirac (y : β) : μ.prod (dirac y) = map (fun x => (x, y)) μ

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
i : ℕ
⊢ (sfiniteSeq μ i).prod (dirac y) = map (fun x => (x, y)) (sfiniteSeq μ i)

Tactic:
refine prod_eq fun s t hs ht => ?_

Result:
case e_f.h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (map (fun x => (x, y)) (sfiniteSeq μ i)) (s ×ˢ t) = (sfiniteSeq μ i) s * (dirac y) t

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
⊢ μ.prod (dirac y) = map (fun x => (x, y)) μ

Tactic:
classical
rw [← sum_sfiniteSeq μ, prod_sum_left, map_sum measurable_prod_mk_right.aemeasurable]
congr
ext1 i
refine prod_eq fun s t hs ht => ?_
simp_rw [map_apply measurable_prod_mk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
  dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, mul_one]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
⊢ μ.prod (dirac y) = map (fun x => (x, y)) μ

Tactic:
rw [← sum_sfiniteSeq μ, prod_sum_left, map_sum measurable_prod_mk_right.aemeasurable]

Result:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
⊢ (sum fun i => (sfiniteSeq μ i).prod (dirac y)) = sum fun i => map (fun x => (x, y)) (sfiniteSeq μ i)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
⊢ (sum fun i => (sfiniteSeq μ i).prod (dirac y)) = sum fun i => map (fun x => (x, y)) (sfiniteSeq μ i)

Tactic:
congr

Result:
case e_f
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
⊢ (fun i => (sfiniteSeq μ i).prod (dirac y)) = fun i => map (fun x => (x, y)) (sfiniteSeq μ i)

Proof state:
case e_f
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
⊢ (fun i => (sfiniteSeq μ i).prod (dirac y)) = fun i => map (fun x => (x, y)) (sfiniteSeq μ i)

Tactic:
ext1 i

Result:
case e_f.h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
i : ℕ
⊢ (sfiniteSeq μ i).prod (dirac y) = map (fun x => (x, y)) (sfiniteSeq μ i)

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (map (fun x => (x, y)) (sfiniteSeq μ i)) (s ×ˢ t) = (sfiniteSeq μ i) s * (dirac y) t

Tactic:
simp_rw [map_apply measurable_prod_mk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
  dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, mul_one]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem inf_mem_closed_subalgebra (A : Subalgebra ℝ C(X, ℝ)) (h : IsClosed (A : Set C(X, ℝ)))
    (f g : A) : (f : C(X, ℝ)) ⊓ (g : C(X, ℝ)) ∈ A

Proof state:
case h.e'_4.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑A.topologicalClosure = ↑A

Tactic:
erw [closure_eq_iff_isClosed]

Result:
case h.e'_4.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ IsClosed ↑A.toSubsemiring

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑f ⊓ ↑g ∈ A

Tactic:
convert inf_mem_subalgebra_closure A f g

Result:
case h.e'_4
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ A = A.topologicalClosure

Proof state:
case h.e'_4.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑A = ↑A.topologicalClosure

Tactic:
symm

Result:
case h.e'_4.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑A.topologicalClosure = ↑A

Proof state:
case h.e'_4
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ A = A.topologicalClosure

Tactic:
apply SetLike.ext'

Result:
case h.e'_4.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑A = ↑A.topologicalClosure

Proof state:
case h.e'_4.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ IsClosed ↑A.toSubsemiring

Tactic:
exact h

Result:
no goals