harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem mem_resolventSet_of_norm_lt [NormOneClass A] {a : A} {k : 𝕜} (h : ‖a‖ < ‖k‖) : k ∈ ρ a :=
  mem_resolventSet_of_norm_lt_mul (by rwa [norm_one, mul_one])

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
a : A
k : 𝕜
h : ‖a‖ < ‖k‖
⊢ ‖a‖ * ‖1‖ < ‖k‖

Tactic:
rwa [norm_one, mul_one]

Result:
no goals
-- Mathlib/Data/Real/Pi/Irrational.lean
/--
Auxiliary for the proof that `π` is irrational.
The second base case for the induction on `n`, giving an explicit formula for `I 1 θ`.
-/
private lemma I_one : I 1 θ * θ ^ 3 = 4 * sin θ - 4 * θ * cos θ

Proof state:
θ : ℝ
⊢ I 1 θ * θ ^ 3 = 4 * sin θ - 4 * θ * cos θ

Tactic:
rw [_root_.pow_succ, ← mul_assoc, recursion' 0, sub_mul, add_mul, mul_assoc _ (I 0 θ), I_zero]

Result:
θ : ℝ
⊢ -(2 * 2 * ((↑0 + 1) * (0 ^ 0 * cos θ))) * θ + 2 * (↑0 + 1) * (2 * ↑0 + 1) * (2 * sin θ) -
      4 * (↑0 + 1) * ↑0 * I (0 - 1) θ * θ =
    4 * sin θ - 4 * θ * cos θ

Proof state:
θ : ℝ
⊢ -(2 * 2 * ((↑0 + 1) * (0 ^ 0 * cos θ))) * θ + 2 * (↑0 + 1) * (2 * ↑0 + 1) * (2 * sin θ) -
      4 * (↑0 + 1) * ↑0 * I (0 - 1) θ * θ =
    4 * sin θ - 4 * θ * cos θ

Tactic:
ring

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem lift_eq_prod_map {β : Type v} [Group β] {f : α → β} {x} : lift f x = prod (map f x)

Proof state:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ (lift f) x = prod ((map f) x)

Tactic:
rw [← lift.unique (prod.comp (map f))]

Result:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ (prod.comp (map f)) x = prod ((map f) x)

case hg
α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ ∀ (x : α), (prod.comp (map f)) (of x) = f x

Proof state:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ (prod.comp (map f)) x = prod ((map f) x)

Tactic:
rfl

Result:
no goals

Proof state:
case hg
α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ ∀ (x : α), (prod.comp (map f)) (of x) = f x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem find?_isSome_iff {p : Fin n → Bool} : (find? p).isSome ↔ ∃ i, p i

Proof state:
n : Nat
p : Fin n → Bool
⊢ (find? p).isSome = true ↔ ∃ i, p i = true

Tactic:
simp [find?, findSome?_isSome_iff]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem coe_smul {S : Type*} [Semiring S] [Module R S] (r : R) (x : S⟦X⟧) :
    ((r • x : S⟦X⟧) : S⸨X⸩) = r • (ofPowerSeries ℤ S x)

Proof state:
R : Type u_1
inst✝² : Semiring R
S : Type u_3
inst✝¹ : Semiring S
inst✝ : Module R S
r : R
x : S⟦X⟧
⊢ (ofPowerSeries ℤ S) (r • x) = r • (ofPowerSeries ℤ S) x

Tactic:
ext

Result:
case coeff.h
R : Type u_1
inst✝² : Semiring R
S : Type u_3
inst✝¹ : Semiring S
inst✝ : Module R S
r : R
x : S⟦X⟧
x✝ : ℤ
⊢ ((ofPowerSeries ℤ S) (r • x)).coeff x✝ = (r • (ofPowerSeries ℤ S) x).coeff x✝

Proof state:
case coeff.h
R : Type u_1
inst✝² : Semiring R
S : Type u_3
inst✝¹ : Semiring S
inst✝ : Module R S
r : R
x : S⟦X⟧
x✝ : ℤ
⊢ ((ofPowerSeries ℤ S) (r • x)).coeff x✝ = (r • (ofPowerSeries ℤ S) x).coeff x✝

Tactic:
simp [coeff_coe, coeff_smul, smul_ite]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem isEquivalent_const_iff_tendsto {c : β} (h : c ≠ 0) :
    u ~[l] const _ c ↔ Tendsto u l (𝓝 c)

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
⊢ Tendsto (u - fun x => c) l (𝓝 0)

Tactic:
have := h.sub (tendsto_const_nhds (x := c))

Result:
case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
this : Tendsto (fun x => u x - c) l (𝓝 (c - c))
⊢ Tendsto (u - fun x => c) l (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h : c ≠ 0
⊢ u ~[l] const α c ↔ Tendsto u l (𝓝 c)

Tactic:
simp (config := { unfoldPartialApp := true }) only [IsEquivalent, const, isLittleO_const_iff h]

Result:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h : c ≠ 0
⊢ Tendsto (u - fun x => c) l (𝓝 0) ↔ Tendsto u l (𝓝 c)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h : c ≠ 0
⊢ Tendsto (u - fun x => c) l (𝓝 0) ↔ Tendsto u l (𝓝 c)

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x => c) l (𝓝 0)
⊢ Tendsto u l (𝓝 c)

case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
⊢ Tendsto (u - fun x => c) l (𝓝 0)

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x => c) l (𝓝 0)
this : Tendsto (fun x => (u - fun x => c) x - -c) l (𝓝 (0 - -c))
⊢ Tendsto u l (𝓝 c)

Tactic:
simp only [Pi.sub_apply, sub_neg_eq_add, sub_add_cancel, zero_add] at this

Result:
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x => c) l (𝓝 0)
this : Tendsto (fun x => u x) l (𝓝 c)
⊢ Tendsto u l (𝓝 c)

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x => c) l (𝓝 0)
this : Tendsto (fun x => u x) l (𝓝 c)
⊢ Tendsto u l (𝓝 c)

Tactic:
exact this

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x => c) l (𝓝 0)
⊢ Tendsto u l (𝓝 c)

Tactic:
have := h.sub (tendsto_const_nhds (x := -c))

Result:
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x => c) l (𝓝 0)
this : Tendsto (fun x => (u - fun x => c) x - -c) l (𝓝 (0 - -c))
⊢ Tendsto u l (𝓝 c)

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
this : Tendsto (fun x => u x - c) l (𝓝 (c - c))
⊢ Tendsto (u - fun x => c) l (𝓝 0)

Tactic:
rwa [sub_self] at this

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem coeff_map (n : ℕ) : coeff (p.map f) n = f (coeff p n)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ ∑ n_1 ∈ p.support, ((C.comp f) (p.coeff n_1) * X ^ n_1).coeff n = ∑ x ∈ p.support, f ((C (p.coeff x) * X ^ x).coeff n)

Tactic:
refine Finset.sum_congr rfl fun x _hx => ?_

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n x : ℕ
_hx : x ∈ p.support
⊢ ((C.comp f) (p.coeff x) * X ^ x).coeff n = f ((C (p.coeff x) * X ^ x).coeff n)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ ∑ n_1 ∈ p.support, ((C.comp f) (p.coeff n_1) * X ^ n_1).coeff n = f (p.coeff n)

Tactic:
conv_rhs => rw [← sum_C_mul_X_pow_eq p, coeff_sum, sum, map_sum]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ ∑ n_1 ∈ p.support, ((C.comp f) (p.coeff n_1) * X ^ n_1).coeff n = ∑ x ∈ p.support, f ((C (p.coeff x) * X ^ x).coeff n)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n x : ℕ
_hx : x ∈ p.support
⊢ ((C.comp f) (p.coeff x) * X ^ x).coeff n = f ((C (p.coeff x) * X ^ x).coeff n)

Tactic:
simp only [RingHom.coe_comp, Function.comp, coeff_C_mul_X_pow]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n x : ℕ
_hx : x ∈ p.support
⊢ (if n = x then f (p.coeff x) else 0) = f (if n = x then p.coeff x else 0)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ (map f p).coeff n = f (p.coeff n)

Tactic:
rw [map, eval₂_def, coeff_sum, sum]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ ∑ n_1 ∈ p.support, ((C.comp f) (p.coeff n_1) * X ^ n_1).coeff n = f (p.coeff n)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n x : ℕ
_hx : x ∈ p.support
⊢ (if n = x then f (p.coeff x) else 0) = f (if n = x then p.coeff x else 0)

Tactic:
split_ifs <;> simp [f.map_zero]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Division.lean
theorem of'_mul_divOf (a : G) (x : k[G]) : of' k G a * x /ᵒᶠ a = x

Proof state:
case H.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : k[G]
x✝ c : G
hc : c ∈ x.support
⊢ a + c = a + x✝ ↔ c = x✝

Tactic:
exact add_right_inj _

Result:
no goals

Proof state:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : k[G]
x✝ : G
⊢ (of' k G a * x /ᵒᶠ a) x✝ = x x✝

Tactic:
rw [AddMonoidAlgebra.divOf_apply, of'_apply, single_mul_apply_aux, one_mul]

Result:
case H.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : k[G]
x✝ : G
⊢ ∀ a_1 ∈ x.support, a + a_1 = a + x✝ ↔ a_1 = x✝

Proof state:
case H.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : k[G]
x✝ : G
⊢ ∀ a_1 ∈ x.support, a + a_1 = a + x✝ ↔ a_1 = x✝

Tactic:
intro c hc

Result:
case H.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : k[G]
x✝ c : G
hc : c ∈ x.support
⊢ a + c = a + x✝ ↔ c = x✝

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : k[G]
⊢ of' k G a * x /ᵒᶠ a = x

Tactic:
ext

Result:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : k[G]
x✝ : G
⊢ (of' k G a * x /ᵒᶠ a) x✝ = x x✝
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
lemma mk_comp_mk [HasSmallLocalizedHom.{w} W X Y] [HasSmallLocalizedHom.{w} W Y Z]
    [HasSmallLocalizedHom.{w} W X Z] (f : X ⟶ Y) (g : Y ⟶ Z) :
    (mk W f).comp (mk W g) = mk W (f ≫ g) :=
  (equiv W W.Q).injective (by simp [equiv_comp])

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Z : C
inst✝² : HasSmallLocalizedHom W X Y
inst✝¹ : HasSmallLocalizedHom W Y Z
inst✝ : HasSmallLocalizedHom W X Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (equiv W W.Q) ((mk W f).comp (mk W g)) = (equiv W W.Q) (mk W (f ≫ g))

Tactic:
simp [equiv_comp]

Result:
no goals
-- Mathlib/Topology/LocallyConstant/Basic.lean
lemma comap_injective (f : C(X, Y)) (hfs : f.1.Surjective) :
    (comap (Z := Z) f).Injective

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
hfs : Function.Surjective f.toFun
⊢ Function.Injective (comap f)

Tactic:
intro a b h

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
hfs : Function.Surjective f.toFun
a b : LocallyConstant Y Z
h : comap f a = comap f b
⊢ a = b

Proof state:
case h.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
hfs : Function.Surjective f.toFun
a b : LocallyConstant Y Z
h : comap f a = comap f b
y : Y
x : X
hx : f.toFun x = y
⊢ a y = b y

Tactic:
simpa [← hx] using LocallyConstant.congr_fun h x

Result:
no goals

Proof state:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
hfs : Function.Surjective f.toFun
a b : LocallyConstant Y Z
h : comap f a = comap f b
y : Y
⊢ a y = b y

Tactic:
obtain ⟨x, hx⟩ := hfs y

Result:
case h.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
hfs : Function.Surjective f.toFun
a b : LocallyConstant Y Z
h : comap f a = comap f b
y : Y
x : X
hx : f.toFun x = y
⊢ a y = b y

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
hfs : Function.Surjective f.toFun
a b : LocallyConstant Y Z
h : comap f a = comap f b
⊢ a = b

Tactic:
ext y

Result:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
hfs : Function.Surjective f.toFun
a b : LocallyConstant Y Z
h : comap f a = comap f b
y : Y
⊢ a y = b y
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
@[reassoc]
lemma extend_op_d (i' j' : ι') :
    (K.op.extend e.op).d i' j' =
      (K.extendOpIso e).hom.f i' ≫ ((K.extend e).d j' i').op ≫
        (K.extendOpIso e).inv.f j'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
this : (K.extendOpIso e).inv.f i' ≫ (K.op.extend e.op).d i' j' = ((K.extend e).d j' i').op ≫ (K.extendOpIso e).inv.f j'
⊢ (K.op.extend e.op).d i' j' = (K.extendOpIso e).hom.f i' ≫ ((K.extend e).d j' i').op ≫ (K.extendOpIso e).inv.f j'

Tactic:
rw [← this, ← comp_f_assoc, Iso.hom_inv_id, id_f, id_comp]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
this : (K.extendOpIso e).inv.f i' ≫ (K.op.extend e.op).d i' j' = (K.extend e).op.d i' j' ≫ (K.extendOpIso e).inv.f j'
⊢ (K.op.extend e.op).d i' j' = (K.extendOpIso e).hom.f i' ≫ ((K.extend e).d j' i').op ≫ (K.extendOpIso e).inv.f j'

Tactic:
dsimp at this

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
this : (K.extendOpIso e).inv.f i' ≫ (K.op.extend e.op).d i' j' = ((K.extend e).d j' i').op ≫ (K.extendOpIso e).inv.f j'
⊢ (K.op.extend e.op).d i' j' = (K.extendOpIso e).hom.f i' ≫ ((K.extend e).d j' i').op ≫ (K.extendOpIso e).inv.f j'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
⊢ (K.op.extend e.op).d i' j' = (K.extendOpIso e).hom.f i' ≫ ((K.extend e).d j' i').op ≫ (K.extendOpIso e).inv.f j'

Tactic:
have := (K.extendOpIso e).inv.comm i' j'

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
this : (K.extendOpIso e).inv.f i' ≫ (K.op.extend e.op).d i' j' = (K.extend e).op.d i' j' ≫ (K.extendOpIso e).inv.f j'
⊢ (K.op.extend e.op).d i' j' = (K.extendOpIso e).hom.f i' ≫ ((K.extend e).d j' i').op ≫ (K.extendOpIso e).inv.f j'
-- Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
theorem geometric_hahn_banach_point_open (ht₁ : Convex ℝ t) (ht₂ : IsOpen t) (disj : x ∉ t) :
    ∃ f : E →L[𝕜] 𝕜, ∀ b ∈ t, re (f x) < re (f b) :=
  let ⟨f, hf⟩ := geometric_hahn_banach_open_point ht₁ ht₂ disj
  ⟨-f, by simpa⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
t : Set E
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
ht₁ : Convex ℝ t
ht₂ : IsOpen t
disj : x ∉ t
f : E →L[𝕜] 𝕜
hf : ∀ a ∈ t, re (f a) < re (f x)
⊢ ∀ b ∈ t, re ((-f) x) < re ((-f) b)

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem neg_divInt_neg (num den) : -num /. -den = num /. den

Proof state:
num den : Int
n : Nat
⊢ inline (mkRat (-num) n.succ) = normalize (-num) n.succ ⋯

Tactic:
simp [normalize_eq_mkRat, Int.neg_neg]

Result:
no goals

Proof state:
num den : Int
⊢ -num /. -den = num /. den

Tactic:
match den with
| Nat.succ n =>
  simp only [divInt, Int.neg_ofNat_succ]
  simp [normalize_eq_mkRat, Int.neg_neg]
| 0 => rfl
| Int.negSucc n =>
  simp only [divInt, Int.neg_negSucc]
  simp [normalize_eq_mkRat, Int.neg_neg]

Result:
no goals

Proof state:
num den : Int
n : Nat
⊢ -num /. -Int.negSucc n = num /. Int.negSucc n

Tactic:
simp only [divInt, Int.neg_negSucc]

Result:
num den : Int
n : Nat
⊢ inline (mkRat (-num) n.succ) = normalize (-num) n.succ ⋯

Proof state:
num den : Int
n : Nat
⊢ -num /. -↑n.succ = num /. ↑n.succ

Tactic:
simp only [divInt, Int.neg_ofNat_succ]

Result:
num den : Int
n : Nat
⊢ normalize (- -num) n.succ ⋯ = inline (mkRat num n.succ)

Proof state:
num den : Int
n : Nat
⊢ normalize (- -num) n.succ ⋯ = inline (mkRat num n.succ)

Tactic:
simp [normalize_eq_mkRat, Int.neg_neg]

Result:
no goals

Proof state:
num den : Int
⊢ -num /. -0 = num /. 0

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem zero_prod (ν : Measure β) : (0 : Measure α).prod ν = 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ν : Measure β
⊢ (bind 0 fun x => map (Prod.mk x) ν) = 0

Tactic:
exact bind_zero_left _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ν : Measure β
⊢ Measure.prod 0 ν = 0

Tactic:
rw [Measure.prod]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ν : Measure β
⊢ (bind 0 fun x => map (Prod.mk x) ν) = 0
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
lemma isIso_inl_of_isIso (h : IsPushout f g inl inr) [IsIso g] : IsIso inl

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : IsIso g
this : HasPushout f g
⊢ IsIso (pushout.inl f g ≫ h.isoPushout.inv)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : IsIso g
this : HasPushout f g
⊢ IsIso inl

Tactic:
rw [← h.inl_isoPushout_inv]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : IsIso g
this : HasPushout f g
⊢ IsIso (pushout.inl f g ≫ h.isoPushout.inv)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : IsIso g
⊢ IsIso inl

Tactic:
have := h.hasPushout

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : IsIso g
this : HasPushout f g
⊢ IsIso inl
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem Measurable.map_prod_mk_left [SFinite ν] :
    Measurable fun x : α => map (Prod.mk x) ν

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
⊢ Measurable fun x => map (Prod.mk x) ν

Tactic:
apply measurable_of_measurable_coe

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
⊢ ∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b => (map (Prod.mk b) ν) s

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b => ν (Prod.mk b ⁻¹' s)

Tactic:
exact measurable_measure_prod_mk_left hs

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
⊢ ∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b => (map (Prod.mk b) ν) s

Tactic:
intro s hs

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b => (map (Prod.mk b) ν) s

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b => (map (Prod.mk b) ν) s

Tactic:
simp_rw [map_apply measurable_prod_mk_left hs]

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b => ν (Prod.mk b ⁻¹' s)
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem t1Space (M : Type*) [TopologicalSpace M] [ChartedSpace H M] : T1Space M

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ T1Space M

Tactic:
have : T2Space H := I.isClosedEmbedding.toIsEmbedding.t2Space

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
this : T2Space H
⊢ T1Space M

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
this : T2Space H
⊢ T1Space M

Tactic:
exact ChartedSpace.t1Space H M

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem full_univ : full Set.univ = (⊤ : Subgroupoid C)

Proof state:
C : Type u
inst✝ : Groupoid C
⊢ full univ = ⊤

Tactic:
ext

Result:
case arrows.h.h.h
C : Type u
inst✝ : Groupoid C
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ x✝ ∈ (full univ).arrows x✝² x✝¹ ↔ x✝ ∈ ⊤.arrows x✝² x✝¹

Proof state:
case arrows.h.h.h
C : Type u
inst✝ : Groupoid C
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ x✝ ∈ (full univ).arrows x✝² x✝¹ ↔ x✝ ∈ ⊤.arrows x✝² x✝¹

Tactic:
simp only [mem_full_iff, mem_univ, and_self, mem_top]

Result:
no goals
-- Mathlib/Data/Matrix/DMatrix.lean
theorem map_sub [∀ i j, AddGroup (α i j)] {β : m → n → Type w} [∀ i j, AddGroup (β i j)]
    (f : ∀ ⦃i j⦄, α i j →+ β i j) (M N : DMatrix m n α) :
    ((M - N).map fun i j => @f i j) = (M.map fun i j => @f i j) - N.map fun i j => @f i j

Proof state:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
⊢ ((M - N).map fun i j => ⇑f) = (M.map fun i j => ⇑f) - N.map fun i j => ⇑f

Tactic:
ext

Result:
case a
m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ (M - N).map (fun i j => ⇑f) i✝ j✝ = ((M.map fun i j => ⇑f) - N.map fun i j => ⇑f) i✝ j✝

Proof state:
case a
m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ (M - N).map (fun i j => ⇑f) i✝ j✝ = ((M.map fun i j => ⇑f) - N.map fun i j => ⇑f) i✝ j✝

Tactic:
simp

Result:
no goals