harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Finset/Defs.lean
theorem Set.finite_iff_bddBelow_bddAbove [Nonempty α] [Lattice α] [LocallyFiniteOrder α] :
    s.Finite ↔ BddBelow s ∧ BddAbove s

Proof state:
case inr
α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
hs : s.Nonempty
⊢ s.Finite ↔ BddBelow s ∧ BddAbove s

Tactic:
exact ⟨fun h ↦ ⟨⟨h.toFinset.inf' ((Finite.toFinset_nonempty h).mpr hs) id,
  fun x hx ↦ Finset.inf'_le id ((Finite.mem_toFinset h).mpr hx)⟩,
  ⟨h.toFinset.sup' ((Finite.toFinset_nonempty h).mpr hs) id, fun x hx ↦ Finset.le_sup' id
  ((Finite.mem_toFinset h).mpr hx)⟩⟩,
  fun ⟨h₀, h₁⟩ ↦ BddBelow.finite_of_bddAbove h₀ h₁⟩

Result:
no goals

Proof state:
α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
⊢ s.Finite ↔ BddBelow s ∧ BddAbove s

Tactic:
obtain (rfl | hs) := s.eq_empty_or_nonempty

Result:
case inl
α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
⊢ ∅.Finite ↔ BddBelow ∅ ∧ BddAbove ∅

case inr
α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
hs : s.Nonempty
⊢ s.Finite ↔ BddBelow s ∧ BddAbove s

Proof state:
case inl
α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
⊢ ∅.Finite ↔ BddBelow ∅ ∧ BddAbove ∅

Tactic:
simp only [Set.finite_empty, bddBelow_empty, bddAbove_empty, and_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_map_hom' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : Array α)
    (h : ∀ x y, f' (g x) (g y) = g (f x y)) (w : stop = l.size) :
    (l.map g).foldl f' (g a) 0 stop = g (l.foldl f a)

Proof state:
α : Type u_1
β : Type u_2
stop : Nat
g : α → β
f : α → α → α
f' : β → β → β
a : α
l : Array α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
w : stop = l.size
⊢ foldl f' (g a) (map g l) 0 stop = g (foldl f a l)

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
l : Array α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
⊢ foldl f' (g a) (map g l) 0 l.size = g (foldl f a l)

Proof state:
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
l : Array α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
⊢ foldl f' (g a) (map g l) 0 l.size = g (foldl f a l)

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ foldl f' (g a) (map g { toList := toList✝ }) 0 { toList := toList✝ }.size = g (foldl f a { toList := toList✝ })

Proof state:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ foldl f' (g a) (map g { toList := toList✝ }) 0 { toList := toList✝ }.size = g (foldl f a { toList := toList✝ })

Tactic:
simp

Result:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ List.foldl f' (g a) (List.map g toList✝) = g (List.foldl f a toList✝)

Proof state:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ List.foldl f' (g a) (List.map g toList✝) = g (List.foldl f a toList✝)

Tactic:
rw [List.foldl_map_hom _ _ _ _ _ h]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem eq_zero_of_zero_eq_one (h : (0 : M₀) = 1) (a : M₀) : a = 0

Proof state:
M₀ : Type u_1
inst✝ : MulZeroOneClass M₀
h : 0 = 1
a : M₀
⊢ a = 0

Tactic:
rw [← mul_one a, ← h, mul_zero]

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem isLeft_congr (h : LiftRel r s x y) : x.isLeft ↔ y.isLeft

Proof state:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
⊢ x.isLeft = true ↔ y.isLeft = true

Tactic:
cases h <;> rfl

Result:
no goals
-- Mathlib/Geometry/Manifold/WhitneyEmbedding.lean
theorem embeddingPiTangent_injOn : InjOn f.embeddingPiTangent s

Proof state:
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
⊢ x = y

Tactic:
obtain ⟨h₁, h₂⟩ := Prod.mk.inj_iff.1 (h (f.ind x hx))

Result:
case intro
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ :
  ↑(f.toFun (f.ind x hx)) x • ↑(extChartAt I (f.c (f.ind x hx))) x =
    ↑(f.toFun (f.ind x hx)) y • ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : ↑(f.toFun (f.ind x hx)) x = ↑(f.toFun (f.ind x hx)) y
⊢ x = y
-- Mathlib/Analysis/Normed/Algebra/Norm.lean
theorem extends_norm (f : MulAlgebraNorm R S) (a : R) : f (algebraMap R S a) = ‖a‖

Proof state:
R : outParam (Type u_1)
S : outParam (Type u_2)
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ f ((algebraMap R S) a) = ‖a‖

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Result:
R : outParam (Type u_1)
S : outParam (Type u_2)
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ f (a • 1) = ‖a‖

Proof state:
R : outParam (Type u_1)
S : outParam (Type u_2)
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ f (a • 1) = ‖a‖

Tactic:
exact extends_norm' _ _

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Completion.lean
theorem lim_add (f g : CauSeq β abv) : lim f + lim g = lim (f + g) :=
  eq_lim_of_const_equiv <|
    show LimZero (const abv (lim f + lim g) - (f + g)) by
      rw [const_add, add_sub_add_comm]
      exact add_limZero (Setoid.symm (equiv_lim f)) (Setoid.symm (equiv_lim g))

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

Tactic:
exact add_limZero (Setoid.symm (equiv_lim f)) (Setoid.symm (equiv_lim g))

Result:
no goals

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

Tactic:
rw [const_add, add_sub_add_comm]

Result:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ (const abv f.lim - f + (const abv g.lim - g)).LimZero
-- Mathlib/Topology/Category/TopCat/OpenNhds.lean
theorem op_map_id_obj (x : X) (U : (OpenNhds x)ᵒᵖ) : (map (𝟙 X) x).op.obj U = U

Proof state:
X : TopCat
x : ↑X
U : (OpenNhds x)ᵒᵖ
⊢ (map (𝟙 X) x).op.obj U = U

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem lt_mul_inv_iff_lt : 1 < a * b⁻¹ ↔ b < a

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ 1 < a * b⁻¹ ↔ b < a

Tactic:
rw [← mul_lt_mul_iff_right b, one_mul, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/CategoryTheory/Action/Limits.lean
/-- `F : C ⥤ Action V G` preserves colimits of some shape `J`
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
lemma preservesColimitsOfShape_of_preserves (F : C ⥤ Action V G) {J : Type w₁}
    [Category.{w₂} J] (h : PreservesColimitsOfShape J (F ⋙ Action.forget V G)) :
    PreservesColimitsOfShape J F

Proof state:
case preservesColimit
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesColimitsOfShape J (F ⋙ forget V G)
K : J ⥤ C
⊢ PreservesColimit K F

Tactic:
apply Action.preservesColimit_of_preserves

Result:
case preservesColimit.h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesColimitsOfShape J (F ⋙ forget V G)
K : J ⥤ C
⊢ PreservesColimit K (F ⋙ forget V G)

Proof state:
case preservesColimit.h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesColimitsOfShape J (F ⋙ forget V G)
K : J ⥤ C
⊢ PreservesColimit K (F ⋙ forget V G)

Tactic:
exact PreservesColimitsOfShape.preservesColimit

Result:
no goals

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesColimitsOfShape J (F ⋙ forget V G)
⊢ PreservesColimitsOfShape J F

Tactic:
constructor

Result:
case preservesColimit
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesColimitsOfShape J (F ⋙ forget V G)
⊢ autoParam (∀ {K : J ⥤ C}, PreservesColimit K F) _auto✝

Proof state:
case preservesColimit
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesColimitsOfShape J (F ⋙ forget V G)
⊢ autoParam (∀ {K : J ⥤ C}, PreservesColimit K F) _auto✝

Tactic:
intro K

Result:
case preservesColimit
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesColimitsOfShape J (F ⋙ forget V G)
K : J ⥤ C
⊢ PreservesColimit K F
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem map_exp : map (f : A →+* A') (exp A) = exp A'

Proof state:
case h
A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
n✝ : ℕ
⊢ (coeff A' n✝) ((map f) (exp A)) = (coeff A' n✝) (exp A')

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
⊢ (map f) (exp A) = exp A'

Tactic:
ext

Result:
case h
A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
n✝ : ℕ
⊢ (coeff A' n✝) ((map f) (exp A)) = (coeff A' n✝) (exp A')
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem relabel_congr {f : CNF α} {r1 r2 : α → β} (hw : ∀ v, Mem v f → r1 v = r2 v) :
    relabel r1 f = relabel r2 f

Proof state:
α : Type u_1
β : Type u_2
f : CNF α
r1 r2 : α → β
hw : ∀ (v : α), Mem v f → r1 v = r2 v
⊢ relabel r1 f = relabel r2 f

Tactic:
dsimp only [relabel]

Result:
α : Type u_1
β : Type u_2
f : CNF α
r1 r2 : α → β
hw : ∀ (v : α), Mem v f → r1 v = r2 v
⊢ List.map (Clause.relabel r1) f = List.map (Clause.relabel r2) f

Proof state:
α : Type u_1
β : Type u_2
f : CNF α
r1 r2 : α → β
hw : ∀ (v : α), Mem v f → r1 v = r2 v
⊢ ∀ (a : Clause α), a ∈ f → Clause.relabel r1 a = Clause.relabel r2 a

Tactic:
intro c h

Result:
α : Type u_1
β : Type u_2
f : CNF α
r1 r2 : α → β
hw : ∀ (v : α), Mem v f → r1 v = r2 v
c : Clause α
h : c ∈ f
⊢ Clause.relabel r1 c = Clause.relabel r2 c

Proof state:
case hw
α : Type u_1
β : Type u_2
f : CNF α
r1 r2 : α → β
hw : ∀ (v : α), Mem v f → r1 v = r2 v
c : Clause α
h : c ∈ f
v : α
m : Clause.Mem v c
⊢ r1 v = r2 v

Tactic:
exact hw _ (mem_of h m)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : CNF α
r1 r2 : α → β
hw : ∀ (v : α), Mem v f → r1 v = r2 v
⊢ List.map (Clause.relabel r1) f = List.map (Clause.relabel r2) f

Tactic:
rw [List.map_congr_left]

Result:
α : Type u_1
β : Type u_2
f : CNF α
r1 r2 : α → β
hw : ∀ (v : α), Mem v f → r1 v = r2 v
⊢ ∀ (a : Clause α), a ∈ f → Clause.relabel r1 a = Clause.relabel r2 a

Proof state:
case hw
α : Type u_1
β : Type u_2
f : CNF α
r1 r2 : α → β
hw : ∀ (v : α), Mem v f → r1 v = r2 v
c : Clause α
h : c ∈ f
⊢ ∀ (v : α), Clause.Mem v c → r1 v = r2 v

Tactic:
intro v m

Result:
case hw
α : Type u_1
β : Type u_2
f : CNF α
r1 r2 : α → β
hw : ∀ (v : α), Mem v f → r1 v = r2 v
c : Clause α
h : c ∈ f
v : α
m : Clause.Mem v c
⊢ r1 v = r2 v

Proof state:
α : Type u_1
β : Type u_2
f : CNF α
r1 r2 : α → β
hw : ∀ (v : α), Mem v f → r1 v = r2 v
c : Clause α
h : c ∈ f
⊢ Clause.relabel r1 c = Clause.relabel r2 c

Tactic:
apply Clause.relabel_congr

Result:
case hw
α : Type u_1
β : Type u_2
f : CNF α
r1 r2 : α → β
hw : ∀ (v : α), Mem v f → r1 v = r2 v
c : Clause α
h : c ∈ f
⊢ ∀ (v : α), Clause.Mem v c → r1 v = r2 v
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_map {l : List α} {p : β → Bool} : (l.map f).any p = l.any (p ∘ f)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
p : β → Bool
⊢ (map f l).any p = l.any (p ∘ f)

Tactic:
induction l with simp | cons _ _ ih => rw [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
p : β → Bool
head✝ : α
tail✝ : List α
ih : (map f tail✝).any p = tail✝.any (p ∘ f)
⊢ (p (f head✝) || (map f tail✝).any p) = (p (f head✝) || tail✝.any (p ∘ f))

Tactic:
rw [ih]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem nat_sqrt_le_real_sqrt {a : ℕ} : ↑(Nat.sqrt a) ≤ √(a : ℝ)

Proof state:
a : ℕ
⊢ ↑a.sqrt ≤ √↑a

Tactic:
rw [Real.le_sqrt (Nat.cast_nonneg _) (Nat.cast_nonneg _)]

Result:
a : ℕ
⊢ ↑a.sqrt ^ 2 ≤ ↑a

Proof state:
a : ℕ
⊢ a.sqrt ^ 2 ≤ a

Tactic:
exact Nat.sqrt_le' a

Result:
no goals

Proof state:
a : ℕ
⊢ ↑a.sqrt ^ 2 ≤ ↑a

Tactic:
norm_cast

Result:
a : ℕ
⊢ a.sqrt ^ 2 ≤ a
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualRestrict_leftInverse (W : Subspace K V) :
    Function.LeftInverse W.dualRestrict W.dualLift := fun x =>
  show W.dualRestrict.comp W.dualLift x = x by
    rw [dualRestrict_comp_dualLift]
    rfl

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
x : Dual K ↥W
⊢ (dualRestrict W ∘ₗ W.dualLift) x = x

Tactic:
rw [dualRestrict_comp_dualLift]

Result:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
x : Dual K ↥W
⊢ 1 x = x

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
x : Dual K ↥W
⊢ 1 x = x

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem IsEquivalent.tendsto_nhds {c : β} (huv : u ~[l] v) (hu : Tendsto u l (𝓝 c)) :
    Tendsto v l (𝓝 c)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
⊢ Tendsto v l (𝓝 c)

Tactic:
by_cases h : c = 0

Result:
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : c = 0
⊢ Tendsto v l (𝓝 c)

case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : ¬c = 0
⊢ Tendsto v l (𝓝 c)

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : c = 0
⊢ Tendsto v l (𝓝 c)

Tactic:
subst c

Result:
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
hu : Tendsto u l (𝓝 0)
⊢ Tendsto v l (𝓝 0)

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
hu : Tendsto u l (𝓝 0)
⊢ Tendsto v l (𝓝 0)

Tactic:
rw [← isLittleO_one_iff ℝ] at hu ⊢

Result:
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
hu : u =o[l] fun _x => 1
⊢ v =o[l] fun _x => 1

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : u ~[l] const α c
h : ¬c = 0
⊢ v ~[l] const α c

Tactic:
exact huv.symm.trans hu

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
hu : u =o[l] fun _x => 1
⊢ v =o[l] fun _x => 1

Tactic:
simpa using (huv.symm.isLittleO.trans hu).add hu

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : ¬c = 0
⊢ Tendsto v l (𝓝 c)

Tactic:
rw [← isEquivalent_const_iff_tendsto h] at hu ⊢

Result:
case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : u ~[l] const α c
h : ¬c = 0
⊢ v ~[l] const α c
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem min_dist_le_dist_pi (x y : ∀ i, F i) (i : ι) :
    min ((1 / 2) ^ encode i : ℝ) (dist (x i) (y i)) ≤ dist x y :=
  le_tsum (dist_summable x y) i fun j _ => le_min (by simp) dist_nonneg

Proof state:
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → MetricSpace (F i)
x y : (i : ι) → F i
i j : ι
x✝ : j ≠ i
⊢ 0 ≤ (1 / 2) ^ encode j

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem ker_map (f : R →+* S) :
    RingHom.ker (map f : MvPolynomial σ R →+* MvPolynomial σ S) =
    Ideal.map (C : R →+* MvPolynomial σ R) (RingHom.ker f)

Proof state:
R : Type u
S : Type u_1
σ : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ RingHom.ker (map f) = Ideal.map C (RingHom.ker f)

Tactic:
ext

Result:
case h
R : Type u
S : Type u_1
σ : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝ : MvPolynomial σ R
⊢ x✝ ∈ RingHom.ker (map f) ↔ x✝ ∈ Ideal.map C (RingHom.ker f)

Proof state:
case h
R : Type u
S : Type u_1
σ : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝ : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m ((map f) x✝) = coeff m 0) ↔ ∀ (m : σ →₀ ℕ), coeff m x✝ ∈ RingHom.ker f

Tactic:
simp_rw [coeff_map, coeff_zero, RingHom.mem_ker]

Result:
no goals

Proof state:
case h
R : Type u
S : Type u_1
σ : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝ : MvPolynomial σ R
⊢ x✝ ∈ RingHom.ker (map f) ↔ x✝ ∈ Ideal.map C (RingHom.ker f)

Tactic:
rw [MvPolynomial.mem_map_C_iff, RingHom.mem_ker, MvPolynomial.ext_iff]

Result:
case h
R : Type u
S : Type u_1
σ : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝ : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m ((map f) x✝) = coeff m 0) ↔ ∀ (m : σ →₀ ℕ), coeff m x✝ ∈ RingHom.ker f
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc (attr := simp)]
lemma opcyclesOpIso_hom_toCycles_op [S.HasLeftHomology] :
    S.opcyclesOpIso.hom ≫ S.toCycles.op = S.op.fromOpcycles

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.opcyclesOpIso.hom ≫ S.toCycles.op = S.op.fromOpcycles

Tactic:
dsimp [opcyclesOpIso, toCycles]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.leftHomologyData.op.opcyclesIso.hom ≫ S.leftHomologyData.f'.op = S.op.fromOpcycles

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.leftHomologyData.op.opcyclesIso.hom ≫ S.leftHomologyData.f'.op = S.op.fromOpcycles

Tactic:
rw [← cancel_epi S.op.pOpcycles, p_fromOpcycles,
  RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc,
  LeftHomologyData.op_p, ← op_comp, LeftHomologyData.f'_i, op_g]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Tower.lean
theorem map_add_left (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) :
    map (f₁ + f₂) g = map f₁ g + map f₂ g

Proof state:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ map (f₁ + f₂) g = map f₁ g + map f₂ g

Tactic:
ext

Result:
case a.h.h
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map (f₁ + f₂) g)) x✝¹) x✝ = ((curry (map f₁ g + map f₂ g)) x✝¹) x✝

Proof state:
case a.h.h
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map (f₁ + f₂) g)) x✝¹) x✝ = ((curry (map f₁ g + map f₂ g)) x✝¹) x✝

Tactic:
simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul,
  add_apply, add_tmul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List ((a : α) × β a)} :
    (m.insertMany l).isEmpty = (m.isEmpty && l.isEmpty)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
⊢ (m.insertMany l).isEmpty = (m.isEmpty && l.isEmpty)

Tactic:
simp_to_raw using Raw₀.isEmpty_insertMany_list

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
lemma mk_iUnion_Ordinal_le_of_le {β : Type*} {o : Ordinal} {c : Cardinal}
    (ho : o.card ≤ c) (hc : ℵ₀ ≤ c) (A : Ordinal → Set β)
    (hA : ∀ j < o, #(A j) ≤ c) : #(⋃ j < o, A j) ≤ c

Proof state:
β : Type u_1
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o.card ≤ c
hc : ℵ₀ ≤ c
A : Ordinal.{u_1} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ #↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c

Tactic:
apply mk_iUnion_Ordinal_lift_le_of_le _ hc A hA

Result:
β : Type u_1
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o.card ≤ c
hc : ℵ₀ ≤ c
A : Ordinal.{u_1} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{u_1, u_1} o.card ≤ lift.{u_1, u_1} c

Proof state:
β : Type u_1
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o.card ≤ c
hc : ℵ₀ ≤ c
A : Ordinal.{u_1} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{u_1, u_1} o.card ≤ lift.{u_1, u_1} c

Tactic:
rwa [Cardinal.lift_le]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
lemma monic_X_sub_C {ι : Type*} (m : MonomialOrder ι) (i : ι) (r : R) :
    m.Monic (X i - C r)

Proof state:
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.Monic (X i - C r)

Tactic:
rw [sub_eq_add_neg, ← map_neg]

Result:
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.Monic (X i + C (-r))

Proof state:
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.Monic (X i + C (-r))

Tactic:
apply monic_X_add_C

Result:
no goals