harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/DFinsupp/Defs.lean
theorem support_eq_empty {f : Π₀ i, β i} : f.support = ∅ ↔ f = 0 :=
  ⟨fun H => ext <| by simpa [Finset.ext_iff] using H, by simp +contextual⟩

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
H : f.support = ∅
⊢ ∀ (i : ι), f i = 0 i

Tactic:
simpa [Finset.ext_iff] using H

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ f = 0 → f.support = ∅

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
theorem real_algHom_eq_id_or_conj (f : ℂ →ₐ[ℝ] ℂ) : f = AlgHom.id ℝ ℂ ∨ f = conjAe

Proof state:
case refine_1
f : ℂ →ₐ[ℝ] ℂ
h : f I = I
⊢ f I = (AlgHom.id ℝ ℂ) I

case refine_2
f : ℂ →ₐ[ℝ] ℂ
h : f I = -I
⊢ f I = ↑conjAe I

Tactic:
exacts [h, conj_I.symm ▸ h]

Result:
no goals

Proof state:
f : ℂ →ₐ[ℝ] ℂ
⊢ f I ^ 2 = I ^ 2

Tactic:
rw [← map_pow, I_sq, map_neg, map_one]

Result:
no goals

Proof state:
f : ℂ →ₐ[ℝ] ℂ
⊢ f = AlgHom.id ℝ ℂ ∨ f = ↑conjAe

Tactic:
refine
    (eq_or_eq_neg_of_sq_eq_sq (f I) I <| by rw [← map_pow, I_sq, map_neg, map_one]).imp ?_ ?_ <;>
  refine fun h => algHom_ext ?_

Result:
case refine_1
f : ℂ →ₐ[ℝ] ℂ
h : f I = I
⊢ f I = (AlgHom.id ℝ ℂ) I

case refine_2
f : ℂ →ₐ[ℝ] ℂ
h : f I = -I
⊢ f I = ↑conjAe I
-- Mathlib/Algebra/DirectSum/Ring.lean
theorem mulHom_of_of {i j} (a : A i) (b : A j) :
    mulHom A (of A i a) (of A j b) = of A (i + j) (GradedMonoid.GMul.mul a b)

Proof state:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ((mulHom A) ((of A i) a)) ((of A j) b) = (of A (i + j)) (GradedMonoid.GMul.mul a b)

Tactic:
unfold mulHom

Result:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ((toAddMonoid fun x => (toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip) ((of A i) a))
      ((of A j) b) =
    (of A (i + j)) (GradedMonoid.GMul.mul a b)

Proof state:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ((compHom (of A (i + j))) ((gMulHom A) a)) b = (of A (i + j)) (GradedMonoid.GMul.mul a b)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ((toAddMonoid fun x => (toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip) ((of A i) a))
      ((of A j) b) =
    (of A (i + j)) (GradedMonoid.GMul.mul a b)

Tactic:
simp only [toAddMonoid_of, flip_apply, coe_comp, Function.comp_apply]

Result:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ((compHom (of A (i + j))) ((gMulHom A) a)) b = (of A (i + j)) (GradedMonoid.GMul.mul a b)
-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_Ioo_right (f : ∀ i, α i) (i : ι) (b : α i) :
    update f i '' Ioo (f i) b = Ioo f (update f i b)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' Ioo (f i) b = Ioo f (update f i b)

Tactic:
simpa using image_update_Ioo f i (f i) b

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem zero_testBit (i : Nat) : testBit 0 i = false

Proof state:
i : Nat
⊢ testBit 0 i = false

Tactic:
simp only [testBit, zero_shiftRight, and_zero, bne_self_eq_false]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean
lemma sheafCondition_of_sheaf {A : Type u'} [Category.{v} A]
    (F : Sheaf J A) : S.SheafCondition F.val

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
A : Type u'
inst✝ : Category.{v, u'} A
F : Sheaf J A
⊢ S.SheafCondition F.val

Tactic:
rw [sheafCondition_iff_comp_coyoneda]

Result:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
A : Type u'
inst✝ : Category.{v, u'} A
F : Sheaf J A
⊢ ∀ (X : Aᵒᵖ), S.SheafCondition (F.val ⋙ coyoneda.obj X)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
A : Type u'
inst✝ : Category.{v, u'} A
F : Sheaf J A
X : Aᵒᵖ
⊢ S.SheafCondition (F.val ⋙ coyoneda.obj X)

Tactic:
exact (Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff _ S.toSquare).1
  (S.isPushout.op.map
    (yoneda.obj ⟨_, (isSheaf_iff_isSheaf_of_type _ _).2 (F.cond X.unop)⟩))

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
A : Type u'
inst✝ : Category.{v, u'} A
F : Sheaf J A
⊢ ∀ (X : Aᵒᵖ), S.SheafCondition (F.val ⋙ coyoneda.obj X)

Tactic:
intro X

Result:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
A : Type u'
inst✝ : Category.{v, u'} A
F : Sheaf J A
X : Aᵒᵖ
⊢ S.SheafCondition (F.val ⋙ coyoneda.obj X)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head? = some a

Proof state:
case cons
α : Type u_1
a x : α
xs : List α
h : x :: xs ≠ []
⊢ (x :: xs).head h = a ↔ (x :: xs).head? = some a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
xs : List α
h : xs ≠ []
⊢ xs.head h = a ↔ xs.head? = some a

Tactic:
cases xs with
| nil => simp at h
| cons x xs => simp

Result:
no goals

Proof state:
case nil
α : Type u_1
a : α
h : [] ≠ []
⊢ [].head h = a ↔ [].head? = some a

Tactic:
simp at h

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem cons_ndinter_of_mem {a : α} (s : Multiset α) {t : Multiset α} (h : a ∈ t) :
    ndinter (a ::ₘ s) t = a ::ₘ ndinter s t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : a ∈ t
⊢ (a ::ₘ s).ndinter t = a ::ₘ s.ndinter t

Tactic:
simp [ndinter, h]

Result:
no goals
-- Mathlib/RingTheory/Frobenius.lean
lemma isArithFrobAt_localize [Q.IsPrime] : H.localize.IsArithFrobAt (maximalIdeal _)

Proof state:
case e_α.e_b
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q)) = Ideal.under R Q

Tactic:
rw [IsScalarTower.algebraMap_eq R S (Localization.AtPrime Q), ← Ideal.comap_comap,
  Localization.AtPrime.comap_maximalIdeal]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
lemma log_nz_of_isRat {n : ℤ} : (NormNum.IsRat e n d) → (decide ((0 : ℚ) < n / d))
    → (decide (n / d < (1 : ℚ))) → (Real.log (e : ℝ) ≠ 0)
  | ⟨inv, eq⟩, h₁, h₂ => by
    rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
    have h₁' : 0 < (n : ℝ) / d

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ 0 < ↑n / ↑d

Tactic:
exact_mod_cast of_decide_eq_true h₁

Result:
no goals

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ Real.log (↑n / ↑d) ≠ 0

Tactic:
have h₁' : 0 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h₁

Result:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
⊢ Real.log (↑n / ↑d) ≠ 0

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
⊢ Real.log (↑n / ↑d) ≠ 0

Tactic:
have h₂' : (n : ℝ) / d < 1 := by exact_mod_cast of_decide_eq_true h₂

Result:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
h₂' : ↑n / ↑d < 1
⊢ Real.log (↑n / ↑d) ≠ 0

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
⊢ ↑n / ↑d < 1

Tactic:
exact_mod_cast of_decide_eq_true h₂

Result:
no goals

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ Real.log e ≠ 0

Tactic:
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]

Result:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ Real.log (↑n / ↑d) ≠ 0

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
h₁' : 0 < ↑n / ↑d
h₂' : ↑n / ↑d < 1
⊢ Real.log (↑n / ↑d) ≠ 0

Tactic:
exact ne_of_lt <| Real.log_neg h₁' h₂'

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem colorable_of_chromaticNumber_ne_top (h : G.chromaticNumber ≠ ⊤) :
    G.Colorable (ENat.toNat G.chromaticNumber)

Proof state:
V : Type u
G : SimpleGraph V
h : ∃ n, G.Colorable n
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
obtain ⟨n, hn⟩ := h

Result:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
hn : G.Colorable n
⊢ G.Colorable G.chromaticNumber.toNat

Proof state:
V : Type u
G : SimpleGraph V
h : G.chromaticNumber ≠ ⊤
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
rw [chromaticNumber_ne_top_iff_exists] at h

Result:
V : Type u
G : SimpleGraph V
h : ∃ n, G.Colorable n
⊢ G.Colorable G.chromaticNumber.toNat

Proof state:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
hn : G.Colorable n
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
exact colorable_chromaticNumber hn

Result:
no goals
-- Mathlib/Data/Nat/Dist.lean
theorem dist_tri_right' (n m : ℕ) : n ≤ m + dist n m

Proof state:
n m : ℕ
⊢ n ≤ m + n.dist m

Tactic:
rw [dist_comm]

Result:
n m : ℕ
⊢ n ≤ m + m.dist n

Proof state:
n m : ℕ
⊢ n ≤ m + m.dist n

Tactic:
apply dist_tri_right

Result:
no goals
-- Mathlib/RepresentationTheory/Basic.lean
theorem dualTensorHom_comm (g : G) :
    dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g) =
      (linHom ρV ρW) g ∘ₗ dualTensorHom k V W

Proof state:
case a.h.h.h
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
x✝² : Module.Dual k V
x✝¹ : W
x✝ : V
⊢ (((TensorProduct.AlgebraTensorModule.curry (dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g))) x✝²) x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry ((ρV.linHom ρW) g ∘ₗ dualTensorHom k V W)) x✝²) x✝¹) x✝

Tactic:
simp [Module.Dual.transpose_apply]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
⊢ dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g) = (ρV.linHom ρW) g ∘ₗ dualTensorHom k V W

Tactic:
ext

Result:
case a.h.h.h
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
x✝² : Module.Dual k V
x✝¹ : W
x✝ : V
⊢ (((TensorProduct.AlgebraTensorModule.curry (dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g))) x✝²) x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry ((ρV.linHom ρW) g ∘ₗ dualTensorHom k V W)) x✝²) x✝¹) x✝
-- Mathlib/Topology/Instances/Real/Lemmas.lean
theorem Real.totallyBounded_ball (x ε : ℝ) : TotallyBounded (ball x ε)

Proof state:
x ε : ℝ
⊢ TotallyBounded (Ioo (x - ε) (x + ε))

Tactic:
apply totallyBounded_Ioo

Result:
no goals

Proof state:
x ε : ℝ
⊢ TotallyBounded (ball x ε)

Tactic:
rw [Real.ball_eq_Ioo]

Result:
x ε : ℝ
⊢ TotallyBounded (Ioo (x - ε) (x + ε))
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem add_choose_mul_factorial_mul_factorial (i j : ℕ) :
    (i + j).choose j * i ! * j ! = (i + j)!

Proof state:
i j : ℕ
⊢ (i + j).choose j * i ! * j ! = (i + j)!

Tactic:
rw [← choose_mul_factorial_mul_factorial (Nat.le_add_left _ _), Nat.add_sub_cancel_right,
  Nat.mul_right_comm]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Limits.lean
/-- A functor `F : J ⥤ CommGrp.{u}` has a limit iff `(F ⋙ forget CommGrp).sections` is
`u`-small. -/
@[to_additive "A functor `F : J ⥤ AddCommGrp.{u}` has a limit iff
`(F ⋙ forget AddCommGrp).sections` is `u`-small."]
lemma hasLimit_iff_small_sections :
    HasLimit F ↔ Small.{u} (F ⋙ forget CommGrp).sections

Proof state:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrp
⊢ HasLimit F → Small.{u, max u v} ↑(F ⋙ forget CommGrp).sections

Tactic:
apply Concrete.small_sections_of_hasLimit

Result:
no goals

Proof state:
case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrp
a✝ : Small.{u, max u v} ↑(F ⋙ forget CommGrp).sections
⊢ HasLimit F

Tactic:
infer_instance

Result:
no goals

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrp
⊢ HasLimit F ↔ Small.{u, max u v} ↑(F ⋙ forget CommGrp).sections

Tactic:
constructor

Result:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrp
⊢ HasLimit F → Small.{u, max u v} ↑(F ⋙ forget CommGrp).sections

case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrp
⊢ Small.{u, max u v} ↑(F ⋙ forget CommGrp).sections → HasLimit F

Proof state:
case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrp
⊢ Small.{u, max u v} ↑(F ⋙ forget CommGrp).sections → HasLimit F

Tactic:
intro

Result:
case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrp
a✝ : Small.{u, max u v} ↑(F ⋙ forget CommGrp).sections
⊢ HasLimit F
-- Mathlib/Data/Real/EReal.lean
theorem add_pos {a b : EReal} (ha : 0 < a) (hb : 0 < b) : 0 < a + b

Proof state:
case h_real
b : EReal
hb : 0 < b
a✝ : ℝ
ha : 0 < ↑a✝
⊢ 0 < ↑a✝ + b

Tactic:
induction b

Result:
case h_real.h_bot
a✝ : ℝ
ha : 0 < ↑a✝
hb : 0 < ⊥
⊢ 0 < ↑a✝ + ⊥

case h_real.h_real
a✝¹ : ℝ
ha : 0 < ↑a✝¹
a✝ : ℝ
hb : 0 < ↑a✝
⊢ 0 < ↑a✝¹ + ↑a✝

case h_real.h_top
a✝ : ℝ
ha : 0 < ↑a✝
hb : 0 < ⊤
⊢ 0 < ↑a✝ + ⊤

Proof state:
case h_real.h_real
a✝¹ a✝ : ℝ
ha : 0 < a✝¹
hb : 0 < a✝
⊢ 0 < a✝¹ + a✝

Tactic:
exact Left.add_pos ha hb

Result:
no goals

Proof state:
case h_top
b : EReal
hb : 0 < b
ha : 0 < ⊤
⊢ 0 < ⊤ + b

Tactic:
rw [top_add_of_ne_bot (bot_lt_zero.trans hb).ne']

Result:
case h_top
b : EReal
hb : 0 < b
ha : 0 < ⊤
⊢ 0 < ⊤

Proof state:
case h_real.h_bot
a✝ : ℝ
ha : 0 < ↑a✝
hb : 0 < ⊥
⊢ 0 < ↑a✝ + ⊥

Tactic:
exfalso

Result:
case h_real.h_bot
a✝ : ℝ
ha : 0 < ↑a✝
hb : 0 < ⊥
⊢ False

Proof state:
case h_real.h_bot
a✝ : ℝ
ha : 0 < ↑a✝
hb : 0 < ⊥
⊢ False

Tactic:
exact not_lt_bot hb

Result:
no goals

Proof state:
case h_real.h_real
a✝¹ : ℝ
ha : 0 < ↑a✝¹
a✝ : ℝ
hb : 0 < ↑a✝
⊢ 0 < ↑a✝¹ + ↑a✝

Tactic:
norm_cast at *

Result:
case h_real.h_real
a✝¹ a✝ : ℝ
ha : 0 < a✝¹
hb : 0 < a✝
⊢ 0 < a✝¹ + a✝

Proof state:
case h_bot
b : EReal
hb : 0 < b
ha : 0 < ⊥
⊢ 0 < ⊥ + b

Tactic:
exfalso

Result:
case h_bot
b : EReal
hb : 0 < b
ha : 0 < ⊥
⊢ False

Proof state:
a b : EReal
ha : 0 < a
hb : 0 < b
⊢ 0 < a + b

Tactic:
induction a

Result:
case h_bot
b : EReal
hb : 0 < b
ha : 0 < ⊥
⊢ 0 < ⊥ + b

case h_real
b : EReal
hb : 0 < b
a✝ : ℝ
ha : 0 < ↑a✝
⊢ 0 < ↑a✝ + b

case h_top
b : EReal
hb : 0 < b
ha : 0 < ⊤
⊢ 0 < ⊤ + b

Proof state:
case h_bot
b : EReal
hb : 0 < b
ha : 0 < ⊥
⊢ False

Tactic:
exact not_lt_bot ha

Result:
no goals

Proof state:
case h_top
b : EReal
hb : 0 < b
ha : 0 < ⊤
⊢ 0 < ⊤

Tactic:
exact ha

Result:
no goals

Proof state:
case h_real.h_top
a✝ : ℝ
ha : 0 < ↑a✝
hb : 0 < ⊤
⊢ 0 < ↑a✝ + ⊤

Tactic:
exact add_top_of_ne_bot (bot_lt_zero.trans ha).ne' ▸ hb

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem linearIndependent_iff_range : LinearIndependent ℤ (GoodProducts.eval C) ↔
    LinearIndependent ℤ (fun (p : range C) ↦ p.1)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
⊢ LinearIndependent ℤ (eval C) ↔ LinearIndependent ℤ fun (p : ↑(range C)) => ↑p

Tactic:
rw [← @Set.rangeFactorization_eq _ _ (GoodProducts.eval C), ← equiv_toFun_eq_eval C]

Result:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
⊢ LinearIndependent ℤ (Subtype.val ∘ (equiv_range C).toFun) ↔ LinearIndependent ℤ fun (p : ↑(range C)) => ↑p

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
⊢ LinearIndependent ℤ (Subtype.val ∘ (equiv_range C).toFun) ↔ LinearIndependent ℤ fun (p : ↑(range C)) => ↑p

Tactic:
exact linearIndependent_equiv (equiv_range C)

Result:
no goals
-- Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean
lemma ext {x y : P.obj (op S.X₄)}
    (h₁ : P.map S.f₂₄.op x = P.map S.f₂₄.op y)
    (h₂ : P.map S.f₃₄.op x = P.map S.f₃₄.op y) : x = y :=
  h.bijective_toPullbackObj.injective (by ext <;> assumption)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ : P.map S.f₂₄.op x = P.map S.f₂₄.op y
h₂ : P.map S.f₃₄.op x = P.map S.f₃₄.op y
⊢ S.toPullbackObj P x = S.toPullbackObj P y

Tactic:
ext <;> assumption

Result:
no goals
-- Mathlib/Analysis/Polynomial/Basic.lean
theorem tendsto_atTop_iff_leadingCoeff_nonneg :
    Tendsto (fun x => eval x P) atTop atTop ↔ 0 < P.degree ∧ 0 ≤ P.leadingCoeff

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff

Tactic:
have : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop atTop :=
  (isEquivalent_atTop_lead P).tendsto_atTop h

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
this : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop atTop
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
this : 0 < P.degree ∧ 0 < P.leadingCoeff
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff

Tactic:
exact ⟨this.1, this.2.le⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ Tendsto (fun x => eval x P) atTop atTop ↔ 0 < P.degree ∧ 0 ≤ P.leadingCoeff

Tactic:
refine ⟨fun h => ?_, fun h => tendsto_atTop_of_leadingCoeff_nonneg P h.1 h.2⟩

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
this : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop atTop
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff

Tactic:
rw [tendsto_const_mul_pow_atTop_iff, ← pos_iff_ne_zero, natDegree_pos_iff_degree_pos] at this

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
this : 0 < P.degree ∧ 0 < P.leadingCoeff
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff
-- Mathlib/Data/Nat/Init.lean
lemma decreasingInduction_trans {motive : (m : ℕ) → m ≤ k → Sort*} (hmn : m ≤ n) (hnk : n ≤ k)
    (of_succ self) :
    (decreasingInduction (motive := motive) of_succ self (Nat.le_trans hmn hnk) : motive m _) =
    decreasingInduction (fun _ _ => of_succ _ _) (decreasingInduction of_succ self hnk) hmn

Proof state:
case refl
m n k : ℕ
hmn : m ≤ n
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ decreasingInduction of_succ self ⋯ =
    decreasingInduction (fun x x_1 => of_succ x ⋯) (decreasingInduction of_succ self ⋯) hmn

Tactic:
rw [decreasingInduction_self]

Result:
no goals

Proof state:
case step
m n k : ℕ
hmn : m ≤ n
m✝ : ℕ
hnk : n.le m✝
ih :
  ∀ {motive : (m : ℕ) → m ≤ m✝ → Sort u_1} (of_succ : (k : ℕ) → (h : k < m✝) → motive (k + 1) h → motive k ⋯)
    (self : motive m✝ ⋯),
    decreasingInduction of_succ self ⋯ =
      decreasingInduction (fun x x_1 => of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m✝.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m✝.succ) → motive (k + 1) h → motive k ⋯
self : motive m✝.succ ⋯
⊢ decreasingInduction of_succ self ⋯ =
    decreasingInduction (fun x x_1 => of_succ x ⋯) (decreasingInduction of_succ self ⋯) hmn

Tactic:
rw [decreasingInduction_succ _ _ (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]

Result:
no goals

Proof state:
m n k : ℕ
motive : (m : ℕ) → m ≤ k → Sort u_1
hmn : m ≤ n
hnk : n ≤ k
of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯
self : motive k ⋯
⊢ decreasingInduction of_succ self ⋯ =
    decreasingInduction (fun x x_1 => of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn

Tactic:
induction hnk with
| refl => rw [decreasingInduction_self]
| step hnk ih =>
    rw [decreasingInduction_succ _ _ (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]

Result:
no goals
-- Mathlib/Algebra/Group/Semiconj/Units.lean
theorem units_inv_symm_left {a : Mˣ} {x y : M} (h : SemiconjBy (↑a) x y) : SemiconjBy (↑a⁻¹) y x :=
  calc
    ↑a⁻¹ * y = ↑a⁻¹ * (y * a * ↑a⁻¹)

Proof state:
M : Type u_1
inst✝ : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a) x y
⊢ ↑a⁻¹ * (y * ↑a * ↑a⁻¹) = x * ↑a⁻¹

Tactic:
rw [← h.eq, ← mul_assoc, Units.inv_mul_cancel_left]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a) x y
⊢ ↑a⁻¹ * y = ↑a⁻¹ * (y * ↑a * ↑a⁻¹)

Tactic:
rw [Units.mul_inv_cancel_right]

Result:
no goals