harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem true_cons_zero : cons true 0#w = twoPow (w + 1) w

Proof state:
case pred
w i✝ : Nat
a✝ : i✝ < w + 1
⊢ (cons true 0#w).getLsbD i✝ = (twoPow (w + 1) w).getLsbD i✝

Tactic:
simp [getLsbD_cons]

Result:
case pred
w i✝ : Nat
a✝ : i✝ < w + 1
⊢ i✝ = w ↔ w = i✝

Proof state:
w : Nat
⊢ cons true 0#w = twoPow (w + 1) w

Tactic:
ext

Result:
case pred
w i✝ : Nat
a✝ : i✝ < w + 1
⊢ (cons true 0#w).getLsbD i✝ = (twoPow (w + 1) w).getLsbD i✝

Proof state:
case pred
w i✝ : Nat
a✝ : i✝ < w + 1
⊢ i✝ = w ↔ w = i✝

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem decompId (P : Karoubi C) : 𝟙 P = decompId_i P ≫ decompId_p P

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ 𝟙 P = P.decompId_i ≫ P.decompId_p

Tactic:
ext

Result:
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ (𝟙 P).f = (P.decompId_i ≫ P.decompId_p).f

Proof state:
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ (𝟙 P).f = (P.decompId_i ≫ P.decompId_p).f

Tactic:
simp only [comp_f, id_f, P.idem, decompId_i, decompId_p]

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem Set.EqOn.of_subset_closure [T2Space Y] {s t : Set X} {f g : X → Y} (h : EqOn f g s)
    (hf : ContinuousOn f t) (hg : ContinuousOn g t) (hst : s ⊆ t) (hts : t ⊆ closure s) :
    EqOn f g t

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
s t : Set X
f g : X → Y
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure s
⊢ EqOn f g t

Tactic:
intro x hx

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
s t : Set X
f g : X → Y
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure s
x : X
hx : x ∈ t
⊢ f x = g x

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
s t : Set X
f g : X → Y
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure s
x : X
hx : x ∈ t
⊢ f x = g x

Tactic:
have : (𝓝[s] x).NeBot := mem_closure_iff_clusterPt.mp (hts hx)

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
s t : Set X
f g : X → Y
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure s
x : X
hx : x ∈ t
this : (𝓝[s] x).NeBot
⊢ f x = g x

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
s t : Set X
f g : X → Y
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure s
x : X
hx : x ∈ t
this : (𝓝[s] x).NeBot
⊢ f x = g x

Tactic:
exact
  tendsto_nhds_unique_of_eventuallyEq ((hf x hx).mono_left <| nhdsWithin_mono _ hst)
    ((hg x hx).mono_left <| nhdsWithin_mono _ hst) (h.eventuallyEq_of_mem self_mem_nhdsWithin)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem headD_eq_head?_getD {l : List α} : headD l a = (head? l).getD a

Proof state:
α : Type u_1
a : α
l : List α
⊢ l.headD a = l.head?.getD a

Tactic:
cases l <;> simp [headD]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/AdeleRing.lean
theorem mixedEmbedding_eq_algebraMap_comp {x : K} :
    mixedEmbedding K x = ringEquiv_mixedSpace K (algebraMap K _ x)

Proof state:
case fst.h
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsReal }
⊢ ((mixedEmbedding K) x).1 v = UniformSpace.Completion.extension ⇑(embedding_of_isReal ⋯) ↑x

Tactic:
rw [UniformSpace.Completion.extension_coe
  (WithAbs.isUniformInducing_of_comp <| v.1.norm_embedding_of_isReal v.2).uniformContinuous x]

Result:
case fst.h
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsReal }
⊢ ((mixedEmbedding K) x).1 v = (embedding_of_isReal ⋯) x

Proof state:
case snd.h
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsComplex }
⊢ ((mixedEmbedding K) x).2 v = (↑v).embedding x

Tactic:
exact mixedEmbedding.mixedEmbedding_apply_isComplex _ _ _

Result:
no goals

Proof state:
case snd.h
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsComplex }
⊢ ((mixedEmbedding K) x).2 v = UniformSpace.Completion.extension ⇑(↑v).embedding ↑x

Tactic:
rw [UniformSpace.Completion.extension_coe
  (WithAbs.isUniformInducing_of_comp <| v.1.norm_embedding_eq).uniformContinuous x]

Result:
case snd.h
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsComplex }
⊢ ((mixedEmbedding K) x).2 v = (↑v).embedding x

Proof state:
K : Type u_1
inst✝ : Field K
x : K
⊢ (mixedEmbedding K) x = (ringEquiv_mixedSpace K) ((algebraMap K (InfiniteAdeleRing K)) x)

Tactic:
ext v <;> simp only [ringEquiv_mixedSpace_apply, algebraMap_apply,
  ringEquivRealOfIsReal, ringEquivComplexOfIsComplex, extensionEmbedding,
  extensionEmbeddingOfIsReal, extensionEmbedding_of_comp, RingEquiv.coe_ofBijective,
  RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, UniformSpace.Completion.extensionHom]

Result:
case fst.h
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsReal }
⊢ ((mixedEmbedding K) x).1 v = UniformSpace.Completion.extension ⇑(embedding_of_isReal ⋯) ↑x

case snd.h
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsComplex }
⊢ ((mixedEmbedding K) x).2 v = UniformSpace.Completion.extension ⇑(↑v).embedding ↑x

Proof state:
case fst.h
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsReal }
⊢ ((mixedEmbedding K) x).1 v = (embedding_of_isReal ⋯) x

Tactic:
exact mixedEmbedding.mixedEmbedding_apply_isReal _ _ _

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem card_iSup_Iio_le_sum_card {o : Ordinal.{u}} (f : Iio o → Ordinal.{max u v}) :
    (⨆ a : Iio o, f a).card ≤ Cardinal.sum fun i ↦ (f ((enumIsoToType o).symm i)).card

Proof state:
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ (⨆ a, f a).card ≤ sum fun i => (f (o.enumIsoToType.symm i)).card

Tactic:
apply le_of_eq_of_le (congr_arg _ _).symm (card_iSup_le_sum_card _)

Result:
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ ⨆ i, f (o.enumIsoToType.symm i) = ⨆ a, f a

Proof state:
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ ⨆ i, f (o.enumIsoToType.symm i) = ⨆ a, f a

Tactic:
simpa using (enumIsoToType o).symm.iSup_comp (g := fun x ↦ f x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_filter_of_pos {p : α → Bool} {l : List α} (w : l ≠ []) (h : p (l.head w)) :
    (filter p l).head ((ne_nil_of_mem (mem_filter.2 ⟨head_mem w, h⟩))) = l.head w

Proof state:
case cons
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
w : head✝ :: tail✝ ≠ []
h : p head✝ = true
⊢ (filter p (head✝ :: tail✝)).head ⋯ = (head✝ :: tail✝).head w

Tactic:
simp [filter_cons, h]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
w : head✝ :: tail✝ ≠ []
h : p ((head✝ :: tail✝).head w) = true
⊢ (filter p (head✝ :: tail✝)).head ⋯ = (head✝ :: tail✝).head w

Tactic:
simp only [head_cons] at h

Result:
case cons
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
w : head✝ :: tail✝ ≠ []
h : p head✝ = true
⊢ (filter p (head✝ :: tail✝)).head ⋯ = (head✝ :: tail✝).head w

Proof state:
α : Type u_1
p : α → Bool
l : List α
w : l ≠ []
h : p (l.head w) = true
⊢ (filter p l).head ⋯ = l.head w

Tactic:
cases l with
| nil => simp
| cons =>
  simp only [head_cons] at h
  simp [filter_cons, h]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
w : [] ≠ []
h : p ([].head w) = true
⊢ (filter p []).head ⋯ = [].head w

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/LocallyConstant/Basic.lean
theorem comp {f : X → Y} (hf : IsLocallyConstant f) (g : Y → Z) :
    IsLocallyConstant (g ∘ f) := fun s => by
  rw [Set.preimage_comp]
  exact hf _

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
g : Y → Z
s : Set Z
⊢ IsOpen (f ⁻¹' (g ⁻¹' s))

Tactic:
exact hf _

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
g : Y → Z
s : Set Z
⊢ IsOpen (g ∘ f ⁻¹' s)

Tactic:
rw [Set.preimage_comp]

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
g : Y → Z
s : Set Z
⊢ IsOpen (f ⁻¹' (g ⁻¹' s))
-- Mathlib/Algebra/Group/Invertible/Defs.lean
theorem Invertible.congr [Monoid α] (a b : α) [Invertible a] [Invertible b] (h : a = b) :
    ⅟a = ⅟b

Proof state:
α : Type u
inst✝² : Monoid α
a : α
inst✝¹ inst✝ : Invertible a
⊢ ⅟a = ⅟a

Tactic:
congr

Result:
case h.e_5.h
α : Type u
inst✝² : Monoid α
a : α
inst✝¹ inst✝ : Invertible a
⊢ inst✝¹ = inst✝

Proof state:
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
h : a = b
⊢ ⅟a = ⅟b

Tactic:
subst h

Result:
α : Type u
inst✝² : Monoid α
a : α
inst✝¹ inst✝ : Invertible a
⊢ ⅟a = ⅟a

Proof state:
case h.e_5.h
α : Type u
inst✝² : Monoid α
a : α
inst✝¹ inst✝ : Invertible a
⊢ inst✝¹ = inst✝

Tactic:
apply Subsingleton.allEq

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblenWith_of_ne_zero (f : Ordinal → Ordinal) (h : o ≠ 0) :
    veblenWith f o = derivFamily fun x : Set.Iio o ↦ veblenWith f x.1

Proof state:
o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ veblenWith f o = derivFamily fun x => veblenWith f ↑x

Tactic:
rw [veblenWith, if_neg h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean
/-- If the terminal comparison map for `G` is an isomorphism, then `G` preserves terminal objects.
-/
lemma PreservesTerminal.of_iso_comparison [i : IsIso (terminalComparison G)] :
    PreservesLimit (Functor.empty.{0} C) G

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ IsLimit (G.mapCone (asEmptyCone (⊤_ C)))

Tactic:
apply (isLimitMapConeEmptyConeEquiv _ _).symm _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ IsTerminal (G.obj (⊤_ C))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ PreservesLimit (Functor.empty C) G

Tactic:
apply preservesLimit_of_preserves_limit_cone terminalIsTerminal

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ IsLimit (G.mapCone (asEmptyCone (⊤_ C)))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ IsTerminal (G.obj (⊤_ C))

Tactic:
exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (Functor.empty.{0} D)) i

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
lemma image_preimage_eq_preimage_image_of_isPullback {X Y U V : Scheme.{u}}
    {f : X ⟶ Y} {f' : U ⟶ V} {iU : U ⟶ X} {iV : V ⟶ Y} [IsOpenImmersion iV] [IsOpenImmersion iU]
    (H : IsPullback f' iU iV f) (W : V.Opens) : iU ''ᵁ f' ⁻¹ᵁ W = f ⁻¹ᵁ iV ''ᵁ W

Proof state:
case neg.mpr.intro.intro.intro
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
y : ↑↑V.toPresheafedSpace
hy : y ∈ ↑W
x : ↑↑(pullback iV f).toPresheafedSpace
hx : (ConcreteCategory.hom (pullback.snd iV f).base) x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
e : (ConcreteCategory.hom iV.base) y = (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.snd iV f).base) x)
⊢ (ConcreteCategory.hom (pullback.snd iV f).base) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Tactic:
rw [← H.isoPullback_inv_snd] at hx

Result:
case neg.mpr.intro.intro.intro
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
y : ↑↑V.toPresheafedSpace
hy : y ∈ ↑W
x : ↑↑(pullback iV f).toPresheafedSpace
hx : (ConcreteCategory.hom (H.isoPullback.inv ≫ iU).base) x ∉ Set.range ⇑(ConcreteCategory.hom iU.base)
e : (ConcreteCategory.hom iV.base) y = (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.snd iV f).base) x)
⊢ (ConcreteCategory.hom (pullback.snd iV f).base) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Proof state:
case pos.intro
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑U.toPresheafedSpace
⊢ (ConcreteCategory.hom iU.base) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) ↔ (ConcreteCategory.hom iU.base) x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

Tactic:
simp only [IsOpenMap.coe_functor_obj, TopologicalSpace.Opens.map_coe,
  iU.isOpenEmbedding.injective.mem_set_image, Set.mem_preimage, SetLike.mem_coe,
  ← Scheme.comp_base_apply, ← H.w]

Result:
case pos.intro
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↑↑U.toPresheafedSpace
⊢ (ConcreteCategory.hom f'.base) x ∈ W ↔
    (ConcreteCategory.hom (f' ≫ iV).base) x ∈ (fun a => (ConcreteCategory.hom (Scheme.Hom.toLRSHom iV).base) a) '' ↑W
-- Mathlib/LinearAlgebra/Prod.lean
theorem range_snd : range (snd R M M₂) = ⊤

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ range (snd R M M₂) = ⊤

Tactic:
rw [range_eq_map, ← prod_top, prod_map_snd]

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem ListBlank.tail_map {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ')
    (l : ListBlank Γ) : (l.map f).tail = l.tail.map f

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f l).tail = map f l.tail

Tactic:
conv => lhs; rw [← ListBlank.cons_head_tail l]

Result:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f (cons l.head l.tail)).tail = map f l.tail

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f (cons l.head l.tail)).tail = map f l.tail

Tactic:
exact Quotient.inductionOn' l fun a ↦ rfl

Result:
no goals
-- Mathlib/ModelTheory/Definability.lean
theorem Definable.map_expansion {L' : FirstOrder.Language} [L'.Structure M] (h : A.Definable L s)
    (φ : L →ᴸ L') [φ.IsExpansionOn M] : A.Definable L' s

Proof state:
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
s : Set (α → M)
L' : Language
inst✝¹ : L'.Structure M
h : A.Definable L s
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
⊢ A.Definable L' s

Tactic:
obtain ⟨ψ, rfl⟩ := h

Result:
case intro
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L[[↑A]].Formula α
⊢ A.Definable L' (setOf ψ.Realize)

Proof state:
case intro.h
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L[[↑A]].Formula α
x : α → M
⊢ x ∈ setOf ψ.Realize ↔ x ∈ setOf ((LHom.addConstants (↑A) φ).onFormula ψ).Realize

Tactic:
simp only [mem_setOf_eq, LHom.realize_onFormula]

Result:
no goals

Proof state:
case intro
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L[[↑A]].Formula α
⊢ A.Definable L' (setOf ψ.Realize)

Tactic:
refine ⟨(φ.addConstants A).onFormula ψ, ?_⟩

Result:
case intro
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L[[↑A]].Formula α
⊢ setOf ψ.Realize = setOf ((LHom.addConstants (↑A) φ).onFormula ψ).Realize

Proof state:
case intro
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L[[↑A]].Formula α
⊢ setOf ψ.Realize = setOf ((LHom.addConstants (↑A) φ).onFormula ψ).Realize

Tactic:
ext x

Result:
case intro.h
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L[[↑A]].Formula α
x : α → M
⊢ x ∈ setOf ψ.Realize ↔ x ∈ setOf ((LHom.addConstants (↑A) φ).onFormula ψ).Realize
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.trans_isLittleO (hfg : IsBigOWith c l f g) (hgk : g =o[l] k) (hc : 0 < c) :
    f =o[l] k

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f k

Tactic:
intro c' c'pos

Result:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
c' : ℝ
c'pos : 0 < c'
⊢ IsBigOWith c' l f k

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
c' : ℝ
c'pos : 0 < c'
⊢ IsBigOWith c' l f k

Tactic:
have : 0 < c' / c := div_pos c'pos hc

Result:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
c' : ℝ
c'pos : 0 < c'
this : 0 < c' / c
⊢ IsBigOWith c' l f k

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
c' : ℝ
c'pos : 0 < c'
this : 0 < c' / c
⊢ IsBigOWith c' l f k

Tactic:
exact (hfg.trans (hgk this) hc.le).congr_const (mul_div_cancel₀ _ hc.ne')

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hgk : g =o[l] k
hc : 0 < c
⊢ f =o[l] k

Tactic:
simp only [IsLittleO_def] at *

Result:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f k
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem IsBlock.stabilizer_le (hB : IsBlock G B) {a : X} (ha : a ∈ B) :
    stabilizer G a ≤ stabilizer G B :=
  fun g hg ↦ hB.smul_eq_of_nonempty ⟨a, by rwa [← hg, smul_mem_smul_set_iff], ha⟩

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g ∈ stabilizer G a
⊢ a ∈ g • B

Tactic:
rwa [← hg, smul_mem_smul_set_iff]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma Odd.neg (hp : Odd a) : Odd (-a)

Proof state:
α : Type u_2
inst✝ : Ring α
a : α
hp : Odd a
⊢ Odd (-a)

Tactic:
obtain ⟨k, hk⟩ := hp

Result:
case intro
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ Odd (-a)

Proof state:
case intro
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ Odd (-a)

Tactic:
use -(k + 1)

Result:
case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = 2 * -(k + 1) + 1

Proof state:
case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = 2 * -(k + 1) + 1

Tactic:
rw [mul_neg, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add, neg_add_cancel_right,
  ← neg_add, hk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem mul_assoc (a b c : Fin n) : a * b * c = a * (b * c)

Proof state:
case a
n : Nat
a b c : Fin n
⊢ ↑a * ↑b % n * ↑c % n = ↑a * (↑b * ↑c % n) % n

Tactic:
rw [← Nat.mod_eq_of_lt a.isLt, ← Nat.mod_eq_of_lt b.isLt, ← Nat.mod_eq_of_lt c.isLt]

Result:
case a
n : Nat
a b c : Fin n
⊢ ↑a % n * (↑b % n) % n * (↑c % n) % n = ↑a % n * (↑b % n * (↑c % n) % n) % n

Proof state:
case a
n : Nat
a b c : Fin n
⊢ ↑a % n * (↑b % n) % n * (↑c % n) % n = ↑a % n * (↑b % n * (↑c % n) % n) % n

Tactic:
simp only [← Nat.mul_mod, Nat.mul_assoc]

Result:
no goals

Proof state:
case a
n : Nat
a b c : Fin n
⊢ ↑(a * b * c) = ↑(a * (b * c))

Tactic:
simp only [val_mul]

Result:
case a
n : Nat
a b c : Fin n
⊢ ↑a * ↑b % n * ↑c % n = ↑a * (↑b * ↑c % n) % n

Proof state:
n : Nat
a b c : Fin n
⊢ a * b * c = a * (b * c)

Tactic:
apply eq_of_val_eq

Result:
case a
n : Nat
a b c : Fin n
⊢ ↑(a * b * c) = ↑(a * (b * c))
-- Mathlib/Order/Birkhoff.lean
@[simp] lemma coe_birkhoffFinset (a : α) : birkhoffFinset a = birkhoffSet a

Proof state:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a : α
⊢ ↑(Fintype.finsetEquivSet.symm (birkhoffSet a)) = birkhoffSet a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a : α
⊢ ↑(Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet a)) = birkhoffSet a

Tactic:
rw [OrderIso.coe_toOrderEmbedding, Fintype.coe_finsetOrderIsoSet_symm]

Result:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a : α
⊢ ↑(Fintype.finsetEquivSet.symm (birkhoffSet a)) = birkhoffSet a

Proof state:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a : α
⊢ ↑(birkhoffFinset a) = birkhoffSet a

Tactic:
classical
simp [birkhoffFinset]
rw [OrderIso.coe_toOrderEmbedding, Fintype.coe_finsetOrderIsoSet_symm]
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a : α
⊢ ↑(birkhoffFinset a) = birkhoffSet a

Tactic:
simp [birkhoffFinset]

Result:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a : α
⊢ ↑(Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet a)) = birkhoffSet a