harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblU_of_Z_eq_zero {P : Fin 3 → R} (hPz : P z = 0) : W'.dblU P = -3 * P x ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.a₁ * P y * 0 - (3 * P x ^ 2 + 2 * W'.a₂ * P x * 0 ^ 2 + W'.a₄ * 0 ^ 4) = -3 * P x ^ 2

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.dblU P = -3 * P x ^ 2

Tactic:
rw [dblU_eq, hPz]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.a₁ * P y * 0 - (3 * P x ^ 2 + 2 * W'.a₂ * P x * 0 ^ 2 + W'.a₄ * 0 ^ 4) = -3 * P x ^ 2
-- Mathlib/Algebra/Group/Action/Pi.lean
@[to_additive]
lemma extend_smul {M α β : Type*} [SMul M β] (r : M) (f : ι → α) (g : ι → β) (e : α → β) :
    extend f (r • g) (r • e) = r • extend f g e

Proof state:
case h
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
⊢ extend f (r • g) (r • e) x = (r • extend f g e) x

Tactic:
classical
simp only [extend_def, Pi.smul_apply]
split_ifs <;> rfl

Result:
no goals

Proof state:
case h
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
⊢ (if h : ∃ a, f a = x then r • g (Classical.choose ⋯) else r • e x) =
    r • if h : ∃ a, f a = x then g (Classical.choose h) else e x

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
⊢ extend f (r • g) (r • e) = r • extend f g e

Tactic:
funext x

Result:
case h
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
⊢ extend f (r • g) (r • e) x = (r • extend f g e) x

Proof state:
case h
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
⊢ extend f (r • g) (r • e) x = (r • extend f g e) x

Tactic:
simp only [extend_def, Pi.smul_apply]

Result:
case h
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst✝ : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
⊢ (if h : ∃ a, f a = x then r • g (Classical.choose ⋯) else r • e x) =
    r • if h : ∃ a, f a = x then g (Classical.choose h) else e x
-- Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
/-- Whiskering commutes with the enriched composition. -/
@[reassoc]
lemma eComp_eHomWhiskerRight {X X' : C} (f : X ⟶ X') (Y Z : C) :
    eComp V X' Y Z ≫ eHomWhiskerRight V f Z =
      eHomWhiskerRight V f Y ▷ _ ≫ eComp V X Y Z

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ (λ_ (EnrichedCategory.Hom X' Y ⊗ EnrichedCategory.Hom Y Z)).inv ≫
      (eHomEquiv V) f ▷ (EnrichedCategory.Hom X' Y ⊗ EnrichedCategory.Hom Y Z) ≫
        EnrichedCategory.Hom X X' ◁ eComp V X' Y Z ≫ eComp V X X' Z =
    ((λ_ (EnrichedCategory.Hom X' Y)).inv ≫ (eHomEquiv V) f ▷ EnrichedCategory.Hom X' Y ≫ eComp V X X' Y) ▷
        EnrichedCategory.Hom Y Z ≫
      eComp V X Y Z

Tactic:
simp [e_assoc']

Result:
no goals

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ eComp V X' Y Z ≫ eHomWhiskerRight V f Z = eHomWhiskerRight V f Y ▷ EnrichedCategory.Hom Y Z ≫ eComp V X Y Z

Tactic:
dsimp [eHomWhiskerRight]

Result:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ eComp V X' Y Z ≫ (λ_ (EnrichedCategory.Hom X' Z)).inv ≫ (eHomEquiv V) f ▷ EnrichedCategory.Hom X' Z ≫ eComp V X X' Z =
    ((λ_ (EnrichedCategory.Hom X' Y)).inv ≫ (eHomEquiv V) f ▷ EnrichedCategory.Hom X' Y ≫ eComp V X X' Y) ▷
        EnrichedCategory.Hom Y Z ≫
      eComp V X Y Z

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ eComp V X' Y Z ≫ (λ_ (EnrichedCategory.Hom X' Z)).inv ≫ (eHomEquiv V) f ▷ EnrichedCategory.Hom X' Z ≫ eComp V X X' Z =
    ((λ_ (EnrichedCategory.Hom X' Y)).inv ≫ (eHomEquiv V) f ▷ EnrichedCategory.Hom X' Y ≫ eComp V X X' Y) ▷
        EnrichedCategory.Hom Y Z ≫
      eComp V X Y Z

Tactic:
rw [leftUnitor_inv_naturality_assoc, whisker_exchange_assoc]

Result:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ (λ_ (EnrichedCategory.Hom X' Y ⊗ EnrichedCategory.Hom Y Z)).inv ≫
      (eHomEquiv V) f ▷ (EnrichedCategory.Hom X' Y ⊗ EnrichedCategory.Hom Y Z) ≫
        EnrichedCategory.Hom X X' ◁ eComp V X' Y Z ≫ eComp V X X' Z =
    ((λ_ (EnrichedCategory.Hom X' Y)).inv ≫ (eHomEquiv V) f ▷ EnrichedCategory.Hom X' Y ≫ eComp V X X' Y) ▷
        EnrichedCategory.Hom Y Z ≫
      eComp V X Y Z
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.prod_nhdsSet_eq_biSup {K : Set Y} (hK : IsCompact K) {X} (l : Filter X) :
    l ×ˢ (𝓝ˢ K) = ⨆ y ∈ K, l ×ˢ 𝓝 y

Proof state:
Y : Type v
inst✝ : TopologicalSpace Y
K : Set Y
hK : IsCompact K
X : Type u_2
l : Filter X
⊢ l ×ˢ 𝓝ˢ K = ⨆ y ∈ K, l ×ˢ 𝓝 y

Tactic:
simp only [prod_comm (f := l), hK.nhdsSet_prod_eq_biSup, map_iSup]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_natCast_of_lt {n a : ℕ} (h : a < n) : (a : ZMod n).val = a

Proof state:
n a : ℕ
h : a < n
⊢ (↑a).val = a

Tactic:
rwa [val_natCast, Nat.mod_eq_of_lt]

Result:
no goals
-- Mathlib/Analysis/Meromorphic/Order.lean
theorem exists_order_ne_top_iff_forall (hU : IsConnected U) :
    (∃ u : U, (hf u u.2).order ≠ ⊤) ↔ (∀ u : U, (hf u u.2).order ≠ ⊤)

Proof state:
case mp.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
this : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = ∅
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

Tactic:
intro u

Result:
case mp.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
this : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = ∅
u : ↑U
⊢ ⋯.order ≠ ⊤

Proof state:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
this : PreconnectedSpace ↑U
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

Tactic:
rcases isClopen_iff.1 hf.isClopen_setOf_order_eq_top with h | h

Result:
case mp.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
this : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = ∅
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

case mp.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
this : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = univ
⊢ ∀ (u : ↑U), ⋯.order ≠ ⊤

Proof state:
case mp.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
this✝ : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = ∅
u : ↑U
this : u ∉ ∅
⊢ ⋯.order ≠ ⊤

Tactic:
rw [← h] at this

Result:
case mp.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, ⋯.order ≠ ⊤
this✝ : PreconnectedSpace ↑U
h : {u | ⋯.order = ⊤} = ∅
u : ↑U
this : u ∉ {u | ⋯.order = ⊤}
⊢ ⋯.order ≠ ⊤
-- Mathlib/Algebra/Group/Basic.lean
theorem div_eq_inv_mul : a / b = b⁻¹ * a

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ a / b = b⁻¹ * a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse

Proof state:
α : Type u_1
l : List α
⊢ l.toArray.toListRev = l.reverse

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem foldrM_attachWith [Monad m] [LawfulMonad m]
    (l : List α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x} → β → m β} {b} :
    (l.attachWith q H).foldrM f b = l.attach.foldrM (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
q : α → Prop
f : { x // q x } → β → m β
H : ∀ (a : α), a ∈ [] → q a
b : β
⊢ foldrM f b ([].attachWith q H) = foldrM (fun a acc => f ⟨a.val, ⋯⟩ acc) b [].attach

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : { x // q x } → β → m β
b : β
⊢ foldrM f b (l.attachWith q H) = foldrM (fun a acc => f ⟨a.val, ⋯⟩ acc) b l.attach

Tactic:
induction l generalizing b with
| nil => simp
| cons a l ih => simp [ih, foldrM_map]

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
q : α → Prop
f : { x // q x } → β → m β
a : α
l : List α
ih :
  ∀ (H : ∀ (a : α), a ∈ l → q a) {b : β},
    foldrM f b (l.attachWith q H) = foldrM (fun a acc => f ⟨a.val, ⋯⟩ acc) b l.attach
H : ∀ (a_1 : α), a_1 ∈ a :: l → q a_1
b : β
⊢ foldrM f b ((a :: l).attachWith q H) = foldrM (fun a_1 acc => f ⟨a_1.val, ⋯⟩ acc) b (a :: l).attach

Tactic:
simp [ih, foldrM_map]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
@[simp] lemma subsingleton_Icc_iff {α : Type*} [LinearOrder α] {a b : α} :
    Set.Subsingleton (Icc a b) ↔ b ≤ a

Proof state:
α : Type u_3
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (Icc a b).Nontrivial

Tactic:
exact ⟨a, ⟨le_refl _, h.le⟩, b, ⟨h.le, le_refl _⟩, h.ne⟩

Result:
no goals

Proof state:
α : Type u_3
inst✝ : LinearOrder α
a b : α
⊢ (Icc a b).Subsingleton ↔ b ≤ a

Tactic:
refine ⟨fun h ↦ ?_, subsingleton_Icc_of_ge⟩

Result:
α : Type u_3
inst✝ : LinearOrder α
a b : α
h : (Icc a b).Subsingleton
⊢ b ≤ a

Proof state:
α : Type u_3
inst✝ : LinearOrder α
a b : α
h : (Icc a b).Subsingleton
⊢ b ≤ a

Tactic:
contrapose! h

Result:
α : Type u_3
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ¬(Icc a b).Subsingleton

Proof state:
α : Type u_3
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ¬(Icc a b).Subsingleton

Tactic:
simp only [gt_iff_lt, not_subsingleton_iff]

Result:
α : Type u_3
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (Icc a b).Nontrivial
-- Mathlib/Data/Set/Basic.lean
theorem sep_eq_self_iff_mem_true : { x ∈ s | p x } = s ↔ ∀ x ∈ s, p x

Proof state:
α : Type u
s : Set α
p : α → Prop
⊢ {x | x ∈ s ∧ p x} = s ↔ ∀ x ∈ s, p x

Tactic:
simp_rw [Set.ext_iff, mem_sep_iff, and_iff_left_iff_imp]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem power_self_eq {c : Cardinal} (h : ℵ₀ ≤ c) : c ^ c = 2 ^ c

Proof state:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ 2 ^ c ≤ c ^ c

Tactic:
exact power_le_power_right ((nat_lt_aleph0 2).le.trans h)

Result:
no goals

Proof state:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ (2 ^ c) ^ c ≤ 2 ^ c

Tactic:
rw [← power_mul, mul_eq_self h]

Result:
no goals

Proof state:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^ c = 2 ^ c

Tactic:
apply ((power_le_power_right <| (cantor c).le).trans _).antisymm

Result:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ 2 ^ c ≤ c ^ c

c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ (2 ^ c) ^ c ≤ 2 ^ c
-- Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean
@[simp]
lemma map_self : IsCocartesian.map p f φ φ = 𝟙 b

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCocartesian (p.map φ) φ
⊢ 𝟙 b✝ = IsCocartesian.map p (p.map φ) φ φ

Tactic:
apply map_uniq

Result:
case map.hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCocartesian (p.map φ) φ
⊢ φ ≫ 𝟙 b✝ = φ

Proof state:
case map.hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCocartesian (p.map φ) φ
⊢ φ ≫ 𝟙 b✝ = φ

Tactic:
simp only [comp_id]

Result:
no goals

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCocartesian (p.map φ) φ
⊢ IsCocartesian.map p (p.map φ) φ φ = 𝟙 b✝

Tactic:
symm

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCocartesian (p.map φ) φ
⊢ 𝟙 b✝ = IsCocartesian.map p (p.map φ) φ φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsCocartesian f φ
⊢ IsCocartesian.map p f φ φ = 𝟙 b

Tactic:
subst_hom_lift p f φ

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCocartesian (p.map φ) φ
⊢ IsCocartesian.map p (p.map φ) φ φ = 𝟙 b✝
-- Mathlib/Algebra/Group/Nat/Even.lean
/-- If `m` and `n` are natural numbers, then the natural number `m^n` is even
if and only if `m` is even and `n` is positive. -/
@[parity_simps] lemma even_pow : Even (m ^ n) ↔ Even m ∧ n ≠ 0

Proof state:
m n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0

Tactic:
induction n <;> simp +contextual [*, pow_succ', even_mul]

Result:
no goals
-- Mathlib/Tactic/NormNum/Pow.lean
theorem isInt_pow {α} [Ring α] : ∀ {f : α → ℕ → α} {a : α} {b : ℕ} {a' : ℤ} {b' : ℕ} {c : ℤ},
    f = HPow.hPow → IsInt a a' → IsNat b b' → Int.pow a' b' = c → IsInt (f a b) c
  | _, _, _, _, _, _, rfl, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨by simp⟩

Proof state:
α : Type u_1
inst✝ : Ring α
n✝¹ : ℤ
n✝ : ℕ
⊢ ↑n✝¹ ^ ↑n✝ = ↑(n✝¹.pow n✝)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem add_one_le_exp (x : ℝ) : x + 1 ≤ Real.exp x

Proof state:
case inr
x : ℝ
hx : x ≠ 0
⊢ x + 1 ≤ rexp x

Tactic:
exact (add_one_lt_exp hx).le

Result:
no goals

Proof state:
x : ℝ
⊢ x + 1 ≤ rexp x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inl

⊢ 0 + 1 ≤ rexp 0

case inr
x : ℝ
hx : x ≠ 0
⊢ x + 1 ≤ rexp x

Proof state:
case inl

⊢ 0 + 1 ≤ rexp 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[simp] lemma not_odd_iff_even : ¬Odd n ↔ Even n

Proof state:
n : ℕ
⊢ ¬Odd n ↔ Even n

Tactic:
rw [not_odd_iff, even_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mem_mapFinIdx {b : β} {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
    b ∈ l.mapFinIdx f ↔ ∃ (i : Nat) (h : i < l.size), f i l[i] h = b

Proof state:
case mk
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
⊢ b ∈ { toList := l }.mapFinIdx f ↔ ∃ i h, f i { toList := l }[i] h = b

Tactic:
simp

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
b : β
l : Array α
f : (i : Nat) → α → i < l.size → β
⊢ b ∈ l.mapFinIdx f ↔ ∃ i h, f i l[i] h = b

Tactic:
rcases l with ⟨l⟩

Result:
case mk
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
⊢ b ∈ { toList := l }.mapFinIdx f ↔ ∃ i h, f i { toList := l }[i] h = b
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
lemma pushoutCocone_inl_eq_inr_iff_of_isColimit {c : PushoutCocone f g} (hc : IsColimit c)
    (h₁ : Function.Injective f) (x₁ : X₁) (x₂ : X₂) :
    c.inl x₁ = c.inr x₂ ↔ ∃ (s : S), f s = x₁ ∧ g s = x₂

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective f
x₁ : X₁
x₂ : X₂
⊢ ∀ (j : WalkingSpan),
    c.ι.app j ≫ (hc.coconePointUniqueUpToIso (Pushout.isColimitCocone f g)).hom = (Pushout.cocone f g).ι.app j

Tactic:
simp

Result:
no goals

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective f
x₁ : X₁
x₂ : X₂
this : Mono f
⊢ (Pushout.cocone f g).inl x₁ = (Pushout.cocone f g).inr x₂ ↔ ∃ s, f s = x₁ ∧ g s = x₂

Tactic:
apply Pushout.inl_eq_inr_iff

Result:
no goals

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective f
x₁ : X₁
x₂ : X₂
⊢ c.inl x₁ = c.inr x₂ ↔ ∃ s, f s = x₁ ∧ g s = x₂

Tactic:
rw [pushoutCocone_inl_eq_inr_iff_of_iso
  (Cocones.ext (IsColimit.coconePointUniqueUpToIso hc (Pushout.isColimitCocone f g))
  (by simp))]

Result:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective f
x₁ : X₁
x₂ : X₂
⊢ (Pushout.cocone f g).inl x₁ = (Pushout.cocone f g).inr x₂ ↔ ∃ s, f s = x₁ ∧ g s = x₂

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective f
x₁ : X₁
x₂ : X₂
⊢ (Pushout.cocone f g).inl x₁ = (Pushout.cocone f g).inr x₂ ↔ ∃ s, f s = x₁ ∧ g s = x₂

Tactic:
have := (mono_iff_injective f).2 h₁

Result:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective f
x₁ : X₁
x₂ : X₂
this : Mono f
⊢ (Pushout.cocone f g).inl x₁ = (Pushout.cocone f g).inr x₂ ↔ ∃ s, f s = x₁ ∧ g s = x₂
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[simp]
lemma map_id : map (𝟙 K) c₁₂ = 𝟙 _

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
⊢ map (𝟙 K) c₁₂ = 𝟙 (K.total c₁₂)

Tactic:
apply (HomologicalComplex.forget _ _).map_injective

Result:
case a
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
⊢ (HomologicalComplex.forget C c₁₂).map (map (𝟙 K) c₁₂) = (HomologicalComplex.forget C c₁₂).map (𝟙 (K.total c₁₂))

Proof state:
case a
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
⊢ (HomologicalComplex.forget C c₁₂).map (map (𝟙 K) c₁₂) = (HomologicalComplex.forget C c₁₂).map (𝟙 (K.total c₁₂))

Tactic:
apply GradedObject.mapMap_id

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem ext (map_unit : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x))
    ⦃j k : M' →ₗ[R] M''⦄ (h : j.comp f = k.comp f) : j = k

Proof state:
case hl
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
j k : M' →ₗ[R] M''
h : j ∘ₗ f = k ∘ₗ f
⊢ k ∘ₗ f = k ∘ₗ f

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
j k : M' →ₗ[R] M''
h : j ∘ₗ f = k ∘ₗ f
⊢ j = k

Tactic:
rw [← lift_unique S f (k.comp f) map_unit j h, lift_unique]

Result:
case hl
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
j k : M' →ₗ[R] M''
h : j ∘ₗ f = k ∘ₗ f
⊢ k ∘ₗ f = k ∘ₗ f
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem Nontrivial.le_infsep_iff {d} (hs : s.Nontrivial) :
    d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y

Tactic:
simp_rw [infsep, ← ENNReal.ofReal_le_iff_le_toReal hs.einfsep_ne_top, le_einfsep_iff, edist_dist,
  ENNReal.ofReal_le_ofReal_iff dist_nonneg]

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem part_iff₁ {f : ℕ →. ℕ} : (@Partrec' 1 fun v => f v.head) ↔ _root_.Partrec f :=
  part_iff.trans
    ⟨fun h =>
      (h.comp <| (Primrec.vector_ofFn fun _ => _root_.Primrec.id).to_comp).of_eq fun v => by
        simp only [id, head_ofFn],
      fun h => h.comp vector_head⟩

Proof state:
f : ℕ →. ℕ
h : _root_.Partrec fun v => f v.head
v : ℕ
⊢ f (ofFn fun i => id v).head = f v

Tactic:
simp only [id, head_ofFn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_false_left  : ∀(c f : Bool), cond c false f = (!c && f)

Proof state:
⊢ ∀ (c f : Bool), (bif c then false else f) = (!c && f)

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
lemma HasFPowerSeriesWithinAt.mono (hf : HasFPowerSeriesWithinAt f p s x) (h : t ⊆ s) :
    HasFPowerSeriesWithinAt f p t x

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
h : t ⊆ s
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt f p t x

Tactic:
exact ⟨r, hp.mono h⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
hf : HasFPowerSeriesWithinAt f p s x
h : t ⊆ s
⊢ HasFPowerSeriesWithinAt f p t x

Tactic:
obtain ⟨r, hp⟩ := hf

Result:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s t : Set E
x : E
h : t ⊆ s
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt f p t x
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCodetector_unop_iff (G : Cᵒᵖ) : IsCodetector (unop G) ↔ IsDetector G

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsCodetector (unop G) ↔ IsDetector G

Tactic:
rw [IsDetector, IsCodetector, ← isCodetecting_unop_iff, Set.singleton_unop]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem coe_normUnit_of_ne_zero [DecidableEq R] (hp : p ≠ 0) :
    (normUnit p : R[X]) = C p.leadingCoeff⁻¹

Proof state:
R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp : p ≠ 0
this : p.leadingCoeff ≠ 0
⊢ ↑(normUnit p) = C p.leadingCoeff⁻¹

Tactic:
simp [CommGroupWithZero.coe_normUnit _ this]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp : p ≠ 0
⊢ ↑(normUnit p) = C p.leadingCoeff⁻¹

Tactic:
have : p.leadingCoeff ≠ 0 := mt leadingCoeff_eq_zero.mp hp

Result:
R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp : p ≠ 0
this : p.leadingCoeff ≠ 0
⊢ ↑(normUnit p) = C p.leadingCoeff⁻¹