harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Functor/EpiMono.lean
theorem mono_map_iff_mono [hF₁ : PreservesMonomorphisms F] [hF₂ : ReflectsMonomorphisms F] :
    Mono (F.map f) ↔ Mono f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
⊢ Mono (F.map f) ↔ Mono f

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
⊢ Mono (F.map f) → Mono f

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
⊢ Mono f → Mono (F.map f)

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
⊢ Mono f → Mono (F.map f)

Tactic:
intro h

Result:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
h : Mono f
⊢ Mono (F.map f)

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
⊢ Mono (F.map f) → Mono f

Tactic:
exact F.mono_of_mono_map

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
h : Mono f
⊢ Mono (F.map f)

Tactic:
exact F.map_mono f

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_setIfInBounds {f : α → β} {l : Array α} {i : Nat} {a : α} :
    (l.setIfInBounds i a).map f = (l.map f).setIfInBounds i (f a)

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
i : Nat
a : α
toList✝ : List α
⊢ map f ({ toList := toList✝ }.setIfInBounds i a) = (map f { toList := toList✝ }).setIfInBounds i (f a)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
i : Nat
a : α
⊢ map f (l.setIfInBounds i a) = (map f l).setIfInBounds i (f a)

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
i : Nat
a : α
toList✝ : List α
⊢ map f ({ toList := toList✝ }.setIfInBounds i a) = (map f { toList := toList✝ }).setIfInBounds i (f a)
-- Mathlib/Logic/Function/Basic.lean
theorem LeftInverse.comp {f : α → β} {g : β → α} {h : β → γ} {i : γ → β} (hf : LeftInverse f g)
    (hh : LeftInverse h i) : LeftInverse (h ∘ f) (g ∘ i) :=
  fun a ↦ show h (f (g (i a))) = a by rw [hf (i a), hh a]

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : β → α
h : β → γ
i : γ → β
hf : LeftInverse f g
hh : LeftInverse h i
a : γ
⊢ h (f (g (i a))) = a

Tactic:
rw [hf (i a), hh a]

Result:
no goals
-- Mathlib/Algebra/Algebra/Unitization.lean
lemma algHom_ext'' {F : Type*}
    [FunLike F (Unitization R A) C] [AlgHomClass F R (Unitization R A) C] {φ ψ : F}
    (h : ∀ a : A, φ a = ψ a) : φ = ψ :=
  algHom_ext h (fun r => by simp only [AlgHomClass.commutes])

Proof state:
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
C : Type u_5
inst✝³ : Semiring C
inst✝² : Algebra R C
F : Type u_6
inst✝¹ : FunLike F (Unitization R A) C
inst✝ : AlgHomClass F R (Unitization R A) C
φ ψ : F
h : ∀ (a : A), φ ↑a = ψ ↑a
r : R
⊢ φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)

Tactic:
simp only [AlgHomClass.commutes]

Result:
no goals
-- Mathlib/Analysis/Convex/Jensen.lean
/-- Canonical form of the **equality case of Jensen's equality**.

For a strictly concave function `f` and positive weights `w`, we have
`f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)` if and only if the points `p` are all equal
(and in fact all equal to their center of mass wrt `w`). -/
lemma StrictConcaveOn.map_sum_eq_iff (hf : StrictConcaveOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 < w i)
    (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) :
    f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConcaveOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i

Tactic:
simpa using hf.neg.map_sum_eq_iff h₀ h₁ hmem

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
lemma piecewise_same : s.piecewise f f = f

Proof state:
case h
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
⊢ s.piecewise f f i = f i

Tactic:
by_cases h : i ∈ s <;> simp [h]

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
⊢ s.piecewise f f = f

Tactic:
ext i

Result:
case h
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
⊢ s.piecewise f f i = f i
-- Mathlib/CategoryTheory/Bicategory/Modification/Oplax.lean
theorem whiskerLeft_naturality (f : a' ⟶ F.obj b) (g : b ⟶ c) :
    f ◁ F.map g ◁ Γ.app c ≫ f ◁ θ.naturality g = f ◁ η.naturality g ≫ f ◁ Γ.app b ▷ G.map g

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η θ : F ⟶ G
Γ : Modification η θ
b c : B
a' : C
f : a' ⟶ F.obj b
g : b ⟶ c
⊢ f ◁ F.map g ◁ Γ.app c ≫ f ◁ θ.naturality g = f ◁ η.naturality g ≫ f ◁ Γ.app b ▷ G.map g

Tactic:
simp_rw [← Bicategory.whiskerLeft_comp, naturality]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_one_zero_iff {x : R} : Wbtw R 1 x 0 ↔ x ∈ Set.Icc (0 : R) 1

Proof state:
R : Type u_1
inst✝ : OrderedRing R
x : R
⊢ Wbtw R 1 x 0 ↔ x ∈ Set.Icc 0 1

Tactic:
rw [wbtw_comm, wbtw_zero_one_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem map_update_add [DecidableEq ι] (i : ι) (u v : s i →ₗ[R] t i) :
    map (update f i (u + v)) = map (update f i u) + map (update f i v)

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁵ : CommSemiring R
s : ι → Type u_7
inst✝⁴ : (i : ι) → AddCommMonoid (s i)
inst✝³ : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
inst✝ : DecidableEq ι
i : ι
u v : s i →ₗ[R] t i
⊢ map (update f i (u + v)) = map (update f i u) + map (update f i v)

Tactic:
ext x

Result:
case H.H
ι : Type u_1
R : Type u_4
inst✝⁵ : CommSemiring R
s : ι → Type u_7
inst✝⁴ : (i : ι) → AddCommMonoid (s i)
inst✝³ : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
inst✝ : DecidableEq ι
i : ι
u v : s i →ₗ[R] t i
x : (i : ι) → s i
⊢ ((map (update f i (u + v))).compMultilinearMap (tprod R)) x =
    ((map (update f i u) + map (update f i v)).compMultilinearMap (tprod R)) x

Proof state:
case H.H
ι : Type u_1
R : Type u_4
inst✝⁵ : CommSemiring R
s : ι → Type u_7
inst✝⁴ : (i : ι) → AddCommMonoid (s i)
inst✝³ : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
inst✝ : DecidableEq ι
i : ι
u v : s i →ₗ[R] t i
x : (i : ι) → s i
⊢ ((map (update f i (u + v))).compMultilinearMap (tprod R)) x =
    ((map (update f i u) + map (update f i v)).compMultilinearMap (tprod R)) x

Tactic:
simp only [LinearMap.compMultilinearMap_apply, map_tprod, map_add_smul_aux, LinearMap.add_apply,
  MultilinearMap.map_update_add]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem leftUnitor_inv_whiskerRight (X Y : C) :
    (λ_ X).inv ▷ Y = (λ_ (X ⊗ Y)).inv ≫ (α_ (𝟙_ C) X Y).inv :=
  eq_of_inv_eq_inv (by simp)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ inv ((λ_ X).inv ▷ Y) = inv ((λ_ (X ⊗ Y)).inv ≫ (α_ (𝟙_ C) X Y).inv)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem push_append_toArray {as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a ::bs).toArray

Proof state:
α : Type u_1
as : Array α
a : α
bs : List α
⊢ as.push a ++ bs.toArray = as ++ (a :: bs).toArray

Tactic:
cases as

Result:
case mk
α : Type u_1
a : α
bs toList✝ : List α
⊢ { toList := toList✝ }.push a ++ bs.toArray = { toList := toList✝ } ++ (a :: bs).toArray

Proof state:
case mk
α : Type u_1
a : α
bs toList✝ : List α
⊢ { toList := toList✝ }.push a ++ bs.toArray = { toList := toList✝ } ++ (a :: bs).toArray

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Function.lean
@[simp] lemma bijOn_singleton : BijOn f {a} {b} ↔ f a = b

Proof state:
α : Type u_1
β : Type u_2
f : α → β
a : α
b : β
⊢ BijOn f {a} {b} ↔ f a = b

Tactic:
simp [BijOn, eq_comm]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem sum_int_mod (s : Multiset ℤ) (n : ℤ) : s.sum % n = (s.map (· % n)).sum % n

Proof state:
s : Multiset ℤ
n : ℤ
⊢ s.sum % n = (map (fun x => x % n) s).sum % n

Tactic:
induction s using Multiset.induction <;> simp [Int.add_emod, *]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem expand_eq_C {p : ℕ} (hp : 0 < p) {f : R[X]} {r : R} : expand R p f = C r ↔ f = C r

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
r : R
⊢ (expand R p) f = C r ↔ f = C r

Tactic:
rw [← expand_C, expand_inj hp, expand_C]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem j_of_isCharTwoJNeZeroNF_of_char_two : W.j = 1 / W.a₆

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
⊢ W.j = 1 / W.a₆

Tactic:
rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
  c₄_of_isCharTwoJNeZeroNF_of_char_two, Δ_of_isCharTwoJNeZeroNF_of_char_two, one_pow]

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fast_fib_eq (n : ℕ) : fastFib n = fib n

Proof state:
n : ℕ
⊢ n.fastFib = fib n

Tactic:
rw [fastFib, fast_fib_aux_eq]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem inits_cons (a : α) (l : List α) : inits (a :: l) = [] :: l.inits.map fun t => a :: t

Proof state:
α : Type u_1
a : α
l : List α
⊢ (a :: l).inits = [] :: map (fun t => a :: t) l.inits

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigO_neg_left : (fun x => -f' x) =O[l] g ↔ f' =O[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x => -f' x) =O[l] g ↔ f' =O[l] g

Tactic:
simp only [IsBigO_def]

Result:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∃ c, IsBigOWith c l (fun x => -f' x) g) ↔ ∃ c, IsBigOWith c l f' g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∃ c, IsBigOWith c l (fun x => -f' x) g) ↔ ∃ c, IsBigOWith c l f' g

Tactic:
exact exists_congr fun _ => isBigOWith_neg_left

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_unused_input_right [Inhabited β] (f : α → β → σ → σ × γ)
    (h : ∀ a b s, f a default s = f a b s) :
    mapAccumr₂ f xs ys s = mapAccumr (fun a s => f a default s) xs s

Proof state:
case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr (fun a s => f a default s) xs s
s : σ
⊢ mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = mapAccumr (fun a s => f a default s) (xs.snoc x) s

Tactic:
simp [h x y s, ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
⊢ mapAccumr₂ f xs ys s = mapAccumr (fun a s => f a default s) xs s

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s with
| nil => rfl
| snoc xs ys x y ih => simp [h x y s, ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun a s => f a default s) nil s

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Iic_erase [DecidableEq α] (b : α) : (Iic b).erase b = Iio b

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b : α
⊢ (Iic b).erase b = Iio b

Tactic:
ext

Result:
case h
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ (Iic b).erase b ↔ a✝ ∈ Iio b

Proof state:
case h
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ (Iic b).erase b ↔ a✝ ∈ Iio b

Tactic:
simp_rw [Finset.mem_erase, mem_Iic, mem_Iio, lt_iff_le_and_ne, and_comm]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem map_top : LieSubmodule.map f ⊤ = f.range

Proof state:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ LieSubmodule.map f ⊤ = f.range

Tactic:
ext

Result:
case h
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
m✝ : N
⊢ m✝ ∈ LieSubmodule.map f ⊤ ↔ m✝ ∈ f.range

Proof state:
case h
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
m✝ : N
⊢ m✝ ∈ LieSubmodule.map f ⊤ ↔ m✝ ∈ f.range

Tactic:
simp [LieSubmodule.mem_map]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem ne_bmex {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) {i} (hi) :
    f i hi ≠ bmex.{_, v} o f

Proof state:
case h.e'_2.h.e'_1
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
⊢ i = (typein fun x1 x2 => x1 < x2).toRelEmbedding ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩)

Tactic:
rw [typein_enum]

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
i : Ordinal.{u}
hi : i < o
⊢ i ∈ Iio (type fun x1 x2 => x1 < x2)

Tactic:
rwa [type_lt]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem edist_le_infEdist_add_ediam (hy : y ∈ s) : edist x y ≤ infEdist x s + diam s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
⊢ edist x y ≤ infEdist x s + diam s

Tactic:
simp_rw [infEdist, ENNReal.iInf_add]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
⊢ edist x y ≤ ⨅ i ∈ s, edist x i + diam s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
i : α
hi : i ∈ s
⊢ edist x y ≤ edist x i + diam s

Tactic:
calc
  edist x y ≤ edist x i + edist i y := edist_triangle _ _ _
  _ ≤ edist x i + diam s := add_le_add le_rfl (edist_le_diam_of_mem hi hy)

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
⊢ edist x y ≤ ⨅ i ∈ s, edist x i + diam s

Tactic:
refine le_iInf₂ fun i hi => ?_

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
i : α
hi : i ∈ s
⊢ edist x y ≤ edist x i + diam s
-- Mathlib/RingTheory/EisensteinCriterion.lean
theorem le_natDegree_of_map_eq_mul_X_pow {n : ℕ} {P : Ideal R} (hP : P.IsPrime) {q : R[X]}
    {c : Polynomial (R ⧸ P)} (hq : map (mk P) q = c * X ^ n) (hc0 : c.degree = 0) :
    n ≤ q.natDegree :=
  Nat.cast_le.1
    (calc
      ↑n = degree (q.map (mk P))

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
P : Ideal R
hP : P.IsPrime
q : R[X]
c : (R ⧸ P)[X]
hq : map (mk P) q = c * X ^ n
hc0 : c.degree = 0
⊢ ↑n = (map (mk P) q).degree

Tactic:
rw [hq, degree_mul, hc0, zero_add, degree_pow, degree_X, nsmul_one]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_two (x : ℝ) : x ^ (2 : ℝ) = x ^ 2

Proof state:
x : ℝ
⊢ x ^ 2 = x ^ ↑2

Tactic:
simp only [Nat.cast_ofNat]

Result:
no goals

Proof state:
x : ℝ
⊢ x ^ 2 = x ^ 2

Tactic:
rw [← rpow_natCast]

Result:
x : ℝ
⊢ x ^ 2 = x ^ ↑2
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
    getKey? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some k else getKey? m a

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ m.contains k = false then some k else m.getKey? a

Tactic:
exact Raw₀.getKey?_insertIfNew ⟨m.1, _⟩ m.2

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ ¬k ∈ m then some k else m.getKey? a

Tactic:
simp [mem_iff_contains, contains_insertIfNew]

Result:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ m.contains k = false then some k else m.getKey? a
-- Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
lemma sectionCotangent_comp :
    sectionCotangent P ∘ₗ P.toExtension.cotangentComplex = LinearMap.id

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x✝ : P.toExtension.Cotangent
i : P.rels
⊢ (P.cotangentSpaceBasis.repr (P.toExtension.cotangentComplex x✝)) (P.map i) = P.cotangentComplexAux x✝ i

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
⊢ P.sectionCotangent ∘ₗ P.toExtension.cotangentComplex = LinearMap.id

Tactic:
ext : 1

Result:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x✝ : P.toExtension.Cotangent
⊢ (P.sectionCotangent ∘ₗ P.toExtension.cotangentComplex) x✝ = LinearMap.id x✝

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x✝ : P.toExtension.Cotangent
⊢ P.sectionCotangent (P.toExtension.cotangentComplex x✝) = x✝

Tactic:
rw [sectionCotangent_eq_iff]

Result:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x✝ : P.toExtension.Cotangent
⊢ ∀ (i : P.rels),
    (P.cotangentSpaceBasis.repr (P.toExtension.cotangentComplex x✝)) (P.map i) = P.cotangentComplexAux x✝ i

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x✝ : P.toExtension.Cotangent
⊢ ∀ (i : P.rels),
    (P.cotangentSpaceBasis.repr (P.toExtension.cotangentComplex x✝)) (P.map i) = P.cotangentComplexAux x✝ i

Tactic:
intro i

Result:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x✝ : P.toExtension.Cotangent
i : P.rels
⊢ (P.cotangentSpaceBasis.repr (P.toExtension.cotangentComplex x✝)) (P.map i) = P.cotangentComplexAux x✝ i

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x✝ : P.toExtension.Cotangent
⊢ (P.sectionCotangent ∘ₗ P.toExtension.cotangentComplex) x✝ = LinearMap.id x✝

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq]

Result:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x✝ : P.toExtension.Cotangent
⊢ P.sectionCotangent (P.toExtension.cotangentComplex x✝) = x✝
-- Mathlib/Order/PrimeIdeal.lean
theorem IsPrime.mem_or_compl_mem (hI : IsPrime I) : x ∈ I ∨ xᶜ ∈ I

Proof state:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
⊢ x ⊓ xᶜ ∈ I

Tactic:
rw [inf_compl_eq_bot]

Result:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
⊢ ⊥ ∈ I

Proof state:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
⊢ x ∈ I ∨ xᶜ ∈ I

Tactic:
apply hI.mem_or_mem

Result:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
⊢ x ⊓ xᶜ ∈ I

Proof state:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
⊢ ⊥ ∈ I

Tactic:
exact I.bot_mem

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem exp_re : (exp x).re = Real.exp x.re * Real.cos x.im

Proof state:
x : ℂ
⊢ (cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)).re = Real.exp x.re * Real.cos x.im

Tactic:
simp [exp_ofReal_re, cos_ofReal_re]

Result:
no goals

Proof state:
x : ℂ
⊢ (cexp x).re = Real.exp x.re * Real.cos x.im

Tactic:
rw [exp_eq_exp_re_mul_sin_add_cos]

Result:
x : ℂ
⊢ (cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)).re = Real.exp x.re * Real.cos x.im
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_biUnion {ι} {I : Set ι} (hI : I.Finite) (s : ι → Set α) (a : α) :
    𝓝[⋃ i ∈ I, s i] a = ⨆ i ∈ I, 𝓝[s i] a :=
  Set.Finite.induction_on _ hI (by simp) fun _ _ hT ↦ by
    simp only [hT, nhdsWithin_union, iSup_insert, biUnion_insert]

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_5
I : Set ι
hI : I.Finite
s : ι → Set α
a : α
⊢ 𝓝[⋃ i ∈ ∅, s i] a = ⨆ i ∈ ∅, 𝓝[s i] a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_5
I : Set ι
hI : I.Finite
s : ι → Set α
a : α
a✝ : ι
s✝ : Set ι
x✝¹ : a✝ ∉ s✝
x✝ : s✝.Finite
hT : 𝓝[⋃ i ∈ s✝, s i] a = ⨆ i ∈ s✝, 𝓝[s i] a
⊢ 𝓝[⋃ i ∈ insert a✝ s✝, s i] a = ⨆ i ∈ insert a✝ s✝, 𝓝[s i] a

Tactic:
simp only [hT, nhdsWithin_union, iSup_insert, biUnion_insert]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_assoc {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'}
    (h_assoc : ∀ a b c, f (g a b) c = f' a (g' b c)) :
    image2 f (image2 g s t) u = image2 f' s (image2 g' t u) :=
  eq_of_forall_subset_iff fun _ ↦ by simp only [image2_subset_iff, forall_mem_image2, h_assoc]

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
x✝ : Set ε
⊢ image2 f (image2 g s t) u ⊆ x✝ ↔ image2 f' s (image2 g' t u) ⊆ x✝

Tactic:
simp only [image2_subset_iff, forall_mem_image2, h_assoc]

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem add_one_mul [RightDistribClass α] (a b : α) : (a + 1) * b = a * b + b

Proof state:
α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ (a + 1) * b = a * b + b

Tactic:
rw [add_mul, one_mul]

Result:
no goals