harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma Scheme.map_basicOpen (r : Γ(U, ⊤)) :
    U.ι ''ᵁ U.toScheme.basicOpen r = X.basicOpen
      (X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top.symm).op r)

Proof state:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (𝟙 (X.presheaf.obj (op (⋯.functor.obj ⊤))))) r)

Tactic:
congr

Result:
case e_f.e_a.e_a
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ (Hom.appIso (X.ofRestrict ⋯) ⊤).inv = 𝟙 (X.presheaf.obj (op (⋯.functor.obj ⊤)))

Proof state:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)

Tactic:
refine (Scheme.image_basicOpen (X.ofRestrict U.isOpenEmbedding) r).trans ?_

Result:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)

Proof state:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)

Tactic:
rw [← Scheme.basicOpen_res_eq _ _ (eqToHom U.isOpenEmbedding_obj_top).op]

Result:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen
      ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op))
        ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r))

Proof state:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen
      ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op))
        ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r))

Tactic:
rw [← CommRingCat.comp_apply, ← CategoryTheory.Functor.map_comp, ← op_comp, eqToHom_trans,
  eqToHom_refl, op_id, CategoryTheory.Functor.map_id]

Result:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (𝟙 (X.presheaf.obj (op (⋯.functor.obj ⊤))))) r)

Proof state:
case e_f.e_a.e_a
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ (Hom.appIso (X.ofRestrict ⋯) ⊤).inv = 𝟙 (X.presheaf.obj (op (⋯.functor.obj ⊤)))

Tactic:
exact PresheafedSpace.IsOpenImmersion.ofRestrict_invApp _ _ _

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem single_add_erase (i : ι) (f : Π₀ i, β i) : single i (f i) + f.erase i = f :=
  ext fun i' =>
    if h : i = i' then by
      subst h; simp only [add_apply, single_apply, erase_apply, add_zero, dite_eq_ite, if_true]
    else by
      simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (Ne.symm h), zero_add]

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
i' : ι
h : ¬i = i'
⊢ (single i (f i) + erase i f) i' = f i'

Tactic:
simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (Ne.symm h), zero_add]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
i' : ι
h : i = i'
⊢ (single i (f i) + erase i f) i' = f i'

Tactic:
subst h

Result:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
⊢ (single i (f i) + erase i f) i = f i

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
⊢ (single i (f i) + erase i f) i = f i

Tactic:
simp only [add_apply, single_apply, erase_apply, add_zero, dite_eq_ite, if_true]

Result:
no goals
-- Mathlib/Topology/UrysohnsLemma.lean
theorem approx_of_mem_C (c : CU P) (n : ℕ) {x : X} (hx : x ∈ c.C) : c.approx n x = 0

Proof state:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
c : CU P
hx : x ∈ c.C
⊢ approx 0 c x = 0

Tactic:
exact indicator_of_not_mem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _

Result:
no goals

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ approx (n + 1) c x = 0

Tactic:
simp only [approx]

Result:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ midpoint ℝ (approx n c.left x) (approx n c.right x) = 0

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
n : ℕ
x : X
hx : x ∈ c.C
⊢ approx n c x = 0

Tactic:
induction n generalizing c with
| zero => exact indicator_of_not_mem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _
| succ n ihn =>
  simp only [approx]
  rw [ihn, ihn, midpoint_self]
  exacts [c.subset_right_C hx, hx]

Result:
no goals

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ midpoint ℝ (approx n c.left x) (approx n c.right x) = 0

Tactic:
rw [ihn, ihn, midpoint_self]

Result:
case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ x ∈ c.right.C

case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ x ∈ c.left.C

Proof state:
case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ x ∈ c.right.C

case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ x ∈ c.left.C

Tactic:
exacts [c.subset_right_C hx, hx]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma sqrt_eq_cfc {a : A} : sqrt a = cfc NNReal.sqrt a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
⊢ sqrt a = cfc (⇑NNReal.sqrt) a

Tactic:
unfold sqrt

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
⊢ cfcₙ (⇑NNReal.sqrt) a = cfc (⇑NNReal.sqrt) a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
⊢ cfcₙ (⇑NNReal.sqrt) a = cfc (⇑NNReal.sqrt) a

Tactic:
rw [cfcₙ_eq_cfc]

Result:
no goals
-- Mathlib/Data/List/ProdSigma.lean
theorem mem_map_swap (x : α) (y : β) (xs : List (α × β)) :
    (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs

Proof state:
α : Type u_1
β : Type u_2
x : α
y : β
xs : List (α × β)
⊢ (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs

Tactic:
induction' xs with x xs xs_ih

Result:
case nil
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (y, x) ∈ map Prod.swap [] ↔ (x, y) ∈ []

case cons
α : Type u_1
β : Type u_2
x✝ : α
y : β
x : α × β
xs : List (α × β)
xs_ih : (y, x✝) ∈ map Prod.swap xs ↔ (x✝, y) ∈ xs
⊢ (y, x✝) ∈ map Prod.swap (x :: xs) ↔ (x✝, y) ∈ x :: xs

Proof state:
case cons.mk
α : Type u_1
β : Type u_2
x : α
y : β
xs : List (α × β)
xs_ih : (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs
a : α
b : β
⊢ (y, x) ∈ map Prod.swap ((a, b) :: xs) ↔ (x, y) ∈ (a, b) :: xs

Tactic:
simp only [mem_cons, Prod.mk.inj_iff, map, Prod.swap_prod_mk, Prod.exists, xs_ih, and_comm]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (y, x) ∈ map Prod.swap [] ↔ (x, y) ∈ []

Tactic:
simp only [not_mem_nil, map_nil]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
x✝ : α
y : β
x : α × β
xs : List (α × β)
xs_ih : (y, x✝) ∈ map Prod.swap xs ↔ (x✝, y) ∈ xs
⊢ (y, x✝) ∈ map Prod.swap (x :: xs) ↔ (x✝, y) ∈ x :: xs

Tactic:
obtain ⟨a, b⟩ := x

Result:
case cons.mk
α : Type u_1
β : Type u_2
x : α
y : β
xs : List (α × β)
xs_ih : (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs
a : α
b : β
⊢ (y, x) ∈ map Prod.swap ((a, b) :: xs) ↔ (x, y) ∈ (a, b) :: xs
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_lt_iff_lt_exp (hx : 0 < x) : log x < y ↔ x < exp y

Proof state:
x y : ℝ
hx : 0 < x
⊢ log x < y ↔ x < rexp y

Tactic:
rw [← exp_lt_exp, exp_log hx]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Compare.lean
theorem commutes_symm {m : ℕ} (hm : n ≤ m) :
    (zmodEquivTrunc p n).symm.toRingHom.comp (truncate hm) =
      (ZMod.castHom (pow_dvd_pow p hm) _).comp (zmodEquivTrunc p m).symm.toRingHom

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
⊢ (zmodEquivTrunc p n).symm.toRingHom.comp (truncate hm) =
    (ZMod.castHom ⋯ (ZMod (p ^ n))).comp (zmodEquivTrunc p m).symm.toRingHom

Tactic:
ext

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x✝ : TruncatedWittVector p m (ZMod p)
⊢ ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate hm)) x✝ =
    ((ZMod.castHom ⋯ (ZMod (p ^ n))).comp (zmodEquivTrunc p m).symm.toRingHom) x✝

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x✝ : TruncatedWittVector p m (ZMod p)
⊢ ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate hm)) x✝ =
    ((ZMod.castHom ⋯ (ZMod (p ^ n))).comp (zmodEquivTrunc p m).symm.toRingHom) x✝

Tactic:
apply commutes_symm'

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma coeIdeal_differentIdeal [NoZeroSMulDivisors A B] :
    ↑(differentIdeal A B) = (FractionalIdeal.dual A K (1 : FractionalIdeal B⁰ L))⁻¹

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁹ : CommRing A
inst✝¹⁸ : Field K
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : Algebra B L
inst✝¹³ : Algebra A B
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsDomain A
inst✝⁷ : IsFractionRing A K
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra.IsSeparable K L
inst✝⁴ : IsIntegralClosure B A L
inst✝³ : IsIntegrallyClosed A
inst✝² : IsDedekindDomain B
inst✝¹ : IsFractionRing B L
inst✝ : NoZeroSMulDivisors A B
⊢ ↑(differentIdeal A B) = (FractionalIdeal.dual A K 1)⁻¹

Tactic:
apply FractionalIdeal.coeToSubmodule_injective

Result:
case a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁹ : CommRing A
inst✝¹⁸ : Field K
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : Algebra B L
inst✝¹³ : Algebra A B
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsDomain A
inst✝⁷ : IsFractionRing A K
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra.IsSeparable K L
inst✝⁴ : IsIntegralClosure B A L
inst✝³ : IsIntegrallyClosed A
inst✝² : IsDedekindDomain B
inst✝¹ : IsFractionRing B L
inst✝ : NoZeroSMulDivisors A B
⊢ (fun I => ↑I) ↑(differentIdeal A B) = (fun I => ↑I) (FractionalIdeal.dual A K 1)⁻¹

Proof state:
case a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁹ : CommRing A
inst✝¹⁸ : Field K
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : Algebra B L
inst✝¹³ : Algebra A B
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsDomain A
inst✝⁷ : IsFractionRing A K
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra.IsSeparable K L
inst✝⁴ : IsIntegralClosure B A L
inst✝³ : IsIntegrallyClosed A
inst✝² : IsDedekindDomain B
inst✝¹ : IsFractionRing B L
inst✝ : NoZeroSMulDivisors A B
⊢ (fun I => ↑I) ↑(differentIdeal A B) = (fun I => ↑I) (FractionalIdeal.dual A K 1)⁻¹

Tactic:
simp only [FractionalIdeal.coe_div
  (FractionalIdeal.dual_ne_zero _ _ (@one_ne_zero (FractionalIdeal B⁰ L) _ _ _)),
  FractionalIdeal.coe_coeIdeal, coeSubmodule_differentIdeal A K, inv_eq_one_div,
  FractionalIdeal.coe_dual_one, FractionalIdeal.coe_one]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/End.lean
@[simp]
lemma smulRight_zero (f : M₁ →ₗ[R] S) : f.smulRight (0 : M) = 0

Proof state:
case h
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x✝ : M₁
⊢ (f.smulRight 0) x✝ = 0 x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : M₁ →ₗ[R] S
⊢ f.smulRight 0 = 0

Tactic:
ext

Result:
case h
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x✝ : M₁
⊢ (f.smulRight 0) x✝ = 0 x✝
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem submodule_span_le_lieSpan : Submodule.span R s ≤ lieSpan R L s

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
⊢ Submodule.span R s ≤ (lieSpan R L s).toSubmodule

Tactic:
rw [Submodule.span_le]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
⊢ s ⊆ ↑(lieSpan R L s).toSubmodule

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
⊢ s ⊆ ↑(lieSpan R L s).toSubmodule

Tactic:
apply subset_lieSpan

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Completion.lean
theorem lim_eq_zero_iff (f : CauSeq β abv) : lim f = 0 ↔ LimZero f :=
  ⟨fun h => by
    have hf := equiv_lim f
    rw [h] at hf
    exact (limZero_congr hf).mpr (const_limZero.mpr rfl),
   fun h => by
    have h₁ : f = f - const abv 0 := ext fun n => by simp [sub_apply, const_apply]
    rw [h₁] at h
    exact lim_eq_of_equiv_const h⟩

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.LimZero
h₁ : f = f - const abv 0
⊢ f.lim = 0

Tactic:
rw [h₁] at h

Result:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : (f - const abv 0).LimZero
h₁ : f = f - const abv 0
⊢ f.lim = 0

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : (f - const abv 0).LimZero
h₁ : f = f - const abv 0
⊢ f.lim = 0

Tactic:
exact lim_eq_of_equiv_const h

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
hf : f ≈ const abv 0
⊢ f.LimZero

Tactic:
exact (limZero_congr hf).mpr (const_limZero.mpr rfl)

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
⊢ f.LimZero

Tactic:
have hf := equiv_lim f

Result:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
hf : f ≈ const abv f.lim
⊢ f.LimZero

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.LimZero
n : ℕ
⊢ ↑f n = ↑(f - const abv 0) n

Tactic:
simp [sub_apply, const_apply]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
hf : f ≈ const abv f.lim
⊢ f.LimZero

Tactic:
rw [h] at hf

Result:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
hf : f ≈ const abv 0
⊢ f.LimZero

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.LimZero
⊢ f.lim = 0

Tactic:
have h₁ : f = f - const abv 0 := ext fun n => by simp [sub_apply, const_apply]

Result:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.LimZero
h₁ : f = f - const abv 0
⊢ f.lim = 0
-- Mathlib/FieldTheory/RatFunc/Degree.lean
theorem intDegree_neg (x : RatFunc K) : intDegree (-x) = intDegree x

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
⊢ (-x).intDegree = x.intDegree

Tactic:
by_cases hx : x = 0

Result:
case pos
K : Type u
inst✝ : Field K
x : RatFunc K
hx : x = 0
⊢ (-x).intDegree = x.intDegree

case neg
K : Type u
inst✝ : Field K
x : RatFunc K
hx : ¬x = 0
⊢ (-x).intDegree = x.intDegree

Proof state:
case pos
K : Type u
inst✝ : Field K
x : RatFunc K
hx : x = 0
⊢ (-x).intDegree = x.intDegree

Tactic:
rw [hx, neg_zero]

Result:
no goals

Proof state:
case neg
K : Type u
inst✝ : Field K
x : RatFunc K
hx : ¬x = 0
⊢ ↑(-x).num.natDegree - ↑(-x).denom.natDegree = ↑(-x.num).natDegree - ↑x.denom.natDegree

Tactic:
exact
  natDegree_sub_eq_of_prod_eq (num_ne_zero (neg_ne_zero.mpr hx)) (denom_ne_zero (-x))
    (neg_ne_zero.mpr (num_ne_zero hx)) (denom_ne_zero x) (num_denom_neg x)

Result:
no goals

Proof state:
case neg
K : Type u
inst✝ : Field K
x : RatFunc K
hx : ¬x = 0
⊢ (-x).intDegree = x.intDegree

Tactic:
rw [intDegree, intDegree, ← natDegree_neg x.num]

Result:
case neg
K : Type u
inst✝ : Field K
x : RatFunc K
hx : ¬x = 0
⊢ ↑(-x).num.natDegree - ↑(-x).denom.natDegree = ↑(-x.num).natDegree - ↑x.denom.natDegree
-- Mathlib/GroupTheory/PGroup.lean
theorem of_injective {H : Type*} [Group H] (ϕ : H →* G) (hϕ : Function.Injective ϕ) :
    IsPGroup p H

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ⇑ϕ
⊢ IsPGroup p H

Tactic:
simp_rw [IsPGroup, ← hϕ.eq_iff, ϕ.map_pow, ϕ.map_one]

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ⇑ϕ
⊢ ∀ (g : H), ∃ k, ϕ g ^ p ^ k = 1

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ⇑ϕ
⊢ ∀ (g : H), ∃ k, ϕ g ^ p ^ k = 1

Tactic:
exact fun h => hG (ϕ h)

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Real.lean
theorem closure_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
    closure { y : PiLp p (fun _ : Fin n ↦ ℝ) | a ≤ y i } = { y | a ≤ y i }

Proof state:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ closure {y | a ≤ y i} = {y | a ≤ y i}

Tactic:
change closure (f ⁻¹' Ici a) = f ⁻¹' Ici a

Result:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ closure (⇑f ⁻¹' Ici a) = ⇑f ⁻¹' Ici a

Proof state:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
⊢ closure {y | a ≤ y i} = {y | a ≤ y i}

Tactic:
let f : (Π _ : Fin n, ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i

Result:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ closure {y | a ≤ y i} = {y | a ≤ y i}

Proof state:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ closure (⇑f ⁻¹' Ici a) = ⇑f ⁻¹' Ici a

Tactic:
rw [f.closure_preimage, closure_Ici]

Result:
case hsurj
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ Surjective ⇑f

Proof state:
case hsurj
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ Surjective ⇑f

Tactic:
apply Function.surjective_eval

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem minimalPeriod_apply_iterate (hx : x ∈ periodicPts f) (n : ℕ) :
    minimalPeriod f (f^[n] x) = minimalPeriod f x

Proof state:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ IsPeriodicPt f (minimalPeriod f x) (f^[n] x)

Tactic:
exact (isPeriodicPt_minimalPeriod f x).apply_iterate n

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
f : α → α
x : α
n m : ℕ
hm : m > 0
hx : IsPeriodicPt f m x
⊢ f^[n] x ∈ periodicPts f

Tactic:
exact ⟨m, hm, hx.apply_iterate n⟩

Result:
no goals

Proof state:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ minimalPeriod f (f^[n] x) = minimalPeriod f x

Tactic:
apply
  (IsPeriodicPt.minimalPeriod_le (minimalPeriod_pos_of_mem_periodicPts hx) _).antisymm
    ((isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate hx
          (isPeriodicPt_minimalPeriod f _)).minimalPeriod_le
      (minimalPeriod_pos_of_mem_periodicPts _))

Result:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ IsPeriodicPt f (minimalPeriod f x) (f^[n] x)

α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicPts f

Proof state:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicPts f

Tactic:
rcases hx with ⟨m, hm, hx⟩

Result:
case intro.intro
α : Type u_1
f : α → α
x : α
n m : ℕ
hm : m > 0
hx : IsPeriodicPt f m x
⊢ f^[n] x ∈ periodicPts f
-- Mathlib/Data/Matrix/Notation.lean
theorem vec3_add [Add α] (a₀ a₁ a₂ b₀ b₁ b₂ : α) :
    ![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂]

Proof state:
α : Type u
inst✝ : Add α
a₀ a₁ a₂ b₀ b₁ b₂ : α
⊢ ![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂]

Tactic:
rw [cons_add_cons, cons_add_cons, cons_add_cons, empty_add_empty]

Result:
no goals
-- Mathlib/Analysis/Complex/Positivity.lean
theorem apply_le_of_iteratedDeriv_nonneg {f : ℂ → ℂ} {c : ℂ} (hf : Differentiable ℂ f)
    (h : ∀ n ≠ 0, 0 ≤ iteratedDeriv n f c) ⦃z : ℂ⦄ (hz : c ≤ z) :
    f c ≤ f z

Proof state:
case succ
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
z : ℂ
hz : c ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv (n + 1) f c
⊢ 0 ≤ iteratedDeriv (n + 1) (fun x => f x - f c) c

Tactic:
rw [iteratedDeriv_succ'] at h ⊢

Result:
case succ
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
z : ℂ
hz : c ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) c
⊢ 0 ≤ iteratedDeriv n (deriv fun x => f x - f c) c

Proof state:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
h' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (fun x => f x - f c) c
⊢ f c ≤ f z

Tactic:
exact sub_nonneg.mp <| nonneg_of_iteratedDeriv_nonneg (hf.sub_const _) h' hz

Result:
no goals

Proof state:
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
n : ℕ
⊢ 0 ≤ iteratedDeriv n (fun x => f x - f c) c

Tactic:
cases n with
| zero => simp only [iteratedDeriv_zero, sub_self, le_refl]
| succ n =>
  specialize h (n + 1) n.succ_ne_zero
  rw [iteratedDeriv_succ'] at h ⊢
  rwa [funext fun x ↦ deriv_sub_const (f := f) (x := x) (f c)]

Result:
no goals

Proof state:
case zero
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ 0 ≤ iteratedDeriv 0 (fun x => f x - f c) c

Tactic:
simp only [iteratedDeriv_zero, sub_self, le_refl]

Result:
no goals

Proof state:
case succ
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
n : ℕ
⊢ 0 ≤ iteratedDeriv (n + 1) (fun x => f x - f c) c

Tactic:
specialize h (n + 1) n.succ_ne_zero

Result:
case succ
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
z : ℂ
hz : c ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv (n + 1) f c
⊢ 0 ≤ iteratedDeriv (n + 1) (fun x => f x - f c) c

Proof state:
case succ
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
z : ℂ
hz : c ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) c
⊢ 0 ≤ iteratedDeriv n (deriv fun x => f x - f c) c

Tactic:
rwa [funext fun x ↦ deriv_sub_const (f := f) (x := x) (f c)]

Result:
no goals