harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem integrable_iff_integrableAtFilter_atBot [LinearOrder X] [OrderTop X] [CompactIccSpace X] :
    Integrable f μ ↔ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ

Proof state:
case mp
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ Integrable f μ → IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ

Tactic:
exact fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩

Result:
no goals

Proof state:
case mpr
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
h : IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ

Tactic:
exact h.1.filter_mono cocompact_le_atBot

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ Integrable f μ ↔ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ

Tactic:
constructor

Result:
case mp
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ Integrable f μ → IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ

case mpr
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ → Integrable f μ

Proof state:
case mpr
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ → Integrable f μ

Tactic:
refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩

Result:
case mpr
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
h : IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
@[simp]
lemma S_smul_four (A : Δ m) : S • S • S • S • A = A

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
⊢ S • S • S • S • A = A

Tactic:
simp only [smul_def, ← mul_assoc, S_mul_S_eq, neg_mul, one_mul, mul_neg, neg_neg, Subtype.coe_eta]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem map (f : M →ₗ[R] N) (h : SameRay R x y) : SameRay R (f x) (f y) :=
  (h.imp fun hx => by rw [hx, map_zero]) <|
    Or.imp (fun hy => by rw [hy, map_zero]) fun ⟨r₁, r₂, hr₁, hr₂, h⟩ =>
      ⟨r₁, r₂, hr₁, hr₂, by rw [← f.map_smul, ← f.map_smul, h]⟩

Proof state:
R : Type u_1
inst✝⁴ : StrictOrderedCommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hx : x = 0
⊢ f x = 0

Tactic:
rw [hx, map_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : StrictOrderedCommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
x y : M
f : M →ₗ[R] N
h✝ : SameRay R x y
x✝ : ∃ r₁ r₂, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ r₁ • f x = r₂ • f y

Tactic:
rw [← f.map_smul, ← f.map_smul, h]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : StrictOrderedCommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hy : y = 0
⊢ f y = 0

Tactic:
rw [hy, map_zero]

Result:
no goals
-- Mathlib/Order/RelSeries.lean
lemma append_apply_left (p q : RelSeries r) (connect : r p.last q.head)
    (i : Fin (p.length + 1)) :
    p.append q connect ((i.castAdd (q.length + 1)).cast (by dsimp; omega)) = p i

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (p.length + 1)
⊢ Fin.append p.toFun q.toFun (Fin.cast ⋯ (Fin.cast ⋯ (Fin.castAdd (q.length + 1) i))) = p.toFun i

Tactic:
convert Fin.append_left _ _ _

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
β : Type u_2
s : Rel β β
p q : RelSeries r
connect : r p.last q.head
i : Fin (p.length + 1)
⊢ p.length + 1 + (q.length + 1) = p.length + q.length + 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (p.length + 1)
⊢ { length := p.length + q.length + 1, toFun := Fin.append p.toFun q.toFun ∘ Fin.cast ⋯, step := ⋯ }.toFun
      (Fin.cast ⋯ (Fin.castAdd (q.length + 1) i)) =
    p.toFun i

Tactic:
simp only [Function.comp_apply]

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (p.length + 1)
⊢ Fin.append p.toFun q.toFun (Fin.cast ⋯ (Fin.cast ⋯ (Fin.castAdd (q.length + 1) i))) = p.toFun i

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (p.length + 1)
⊢ (p.append q connect).toFun (Fin.cast ⋯ (Fin.castAdd (q.length + 1) i)) = p.toFun i

Tactic:
delta append

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
i : Fin (p.length + 1)
⊢ { length := p.length + q.length + 1, toFun := Fin.append p.toFun q.toFun ∘ Fin.cast ⋯, step := ⋯ }.toFun
      (Fin.cast ⋯ (Fin.castAdd (q.length + 1) i)) =
    p.toFun i

Proof state:
α : Type u_1
r : Rel α α
β : Type u_2
s : Rel β β
p q : RelSeries r
connect : r p.last q.head
i : Fin (p.length + 1)
⊢ p.length + 1 + (q.length + 1) = (p.append q connect).length + 1

Tactic:
dsimp

Result:
α : Type u_1
r : Rel α α
β : Type u_2
s : Rel β β
p q : RelSeries r
connect : r p.last q.head
i : Fin (p.length + 1)
⊢ p.length + 1 + (q.length + 1) = p.length + q.length + 1 + 1
-- Mathlib/Algebra/DirectSum/Ring.lean
theorem list_prod_ofFn_of_eq_dProd (n : ℕ) (fι : Fin n → ι) (fA : ∀ a, A (fι a)) :
    (List.ofFn fun a => of A (fι a) (fA a)).prod = of A _ ((List.finRange n).dProd fι fA)

Proof state:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
n : ℕ
fι : Fin n → ι
fA : (a : Fin n) → A (fι a)
⊢ (List.ofFn fun a => (of A (fι a)) (fA a)).prod =
    (of A ((List.finRange n).dProdIndex fι)) ((List.finRange n).dProd fι fA)

Tactic:
rw [List.ofFn_eq_map, ofList_dProd]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma isUnramified_iff :
    IsUnramified k w ↔ IsReal w ∨ IsComplex (w.comap (algebraMap k K))

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ IsUnramified k w ↔ w.IsReal ∨ (w.comap (algebraMap k K)).IsComplex

Tactic:
rw [← not_iff_not, not_isUnramified_iff, not_or,
  not_isReal_iff_isComplex, not_isComplex_iff_isReal]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem gc : GaloisConnection lowerAdjoint fun 𝓕 => UniformFun.filter α β 𝓕

Proof state:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) 𝓐 ≤ 𝓕 ↔ 𝓐 ≤ (fun 𝓕 => UniformFun.filter α β 𝓕) 𝓕

Tactic:
symm

Result:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ 𝓐 ≤ (fun 𝓕 => UniformFun.filter α β 𝓕) 𝓕 ↔ (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) 𝓐 ≤ 𝓕

Proof state:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ 𝓐 ≤ (fun 𝓕 => UniformFun.filter α β 𝓕) 𝓕 ↔ (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) 𝓐 ≤ 𝓕

Tactic:
calc
  𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets := by
    rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]
  _ ↔ ∀ U ∈ 𝓕, UniformFun.gen α β U ∈ 𝓐 := image_subset_iff
  _ ↔ ∀ U ∈ 𝓕,
        { uv | ∀ x, (uv, x) ∈ { t : ((α →ᵤ β) × (α →ᵤ β)) × α | (t.1.1 t.2, t.1.2 t.2) ∈ U } } ∈
          𝓐 :=
    Iff.rfl
  _ ↔ ∀ U ∈ 𝓕,
        { uvx : ((α →ᵤ β) × (α →ᵤ β)) × α | (uvx.1.1 uvx.2, uvx.1.2 uvx.2) ∈ U } ∈
          𝓐 ×ˢ (⊤ : Filter α) :=
    forall₂_congr fun U _hU => mem_prod_top.symm
  _ ↔ lowerAdjoint 𝓐 ≤ 𝓕 := Iff.rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
⊢ GaloisConnection (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕

Tactic:
intro 𝓐 𝓕

Result:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) 𝓐 ≤ 𝓕 ↔ 𝓐 ≤ (fun 𝓕 => UniformFun.filter α β 𝓕) 𝓕

Proof state:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ 𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets

Tactic:
rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem isEmpty : ∀ {s}, Valid s → (s.isEmpty ↔ s.toString = "")
  | _, h => let ⟨l, m, r, h⟩ := h.validFor; by simp [h.isEmpty, h.toString, ext_iff]

Proof state:
x✝ : Substring
h✝ : x✝.Valid
l m r : List Char
h : ValidFor l m r x✝
⊢ x✝.isEmpty = true ↔ x✝.toString = ""

Tactic:
simp [h.isEmpty, h.toString, ext_iff]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
lemma sup_set_smul (s t : Set S) :
    (s ⊔ t) • N = s • N ⊔ t • N :=
  set_smul_eq_of_le _ _ _
    (by rintro _ _ (hr|hr) hn
        · exact Submodule.mem_sup_left (mem_set_smul_of_mem_mem hr hn)
        · exact Submodule.mem_sup_right (mem_set_smul_of_mem_mem hr hn))
    (sup_le (set_smul_mono_left _ le_sup_left) (set_smul_mono_left _ le_sup_right))

Proof state:
case inl
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
s t : Set S
r✝ : S
n✝ : M
hr : r✝ ∈ s
hn : n✝ ∈ N
⊢ r✝ • n✝ ∈ s • N ⊔ t • N

Tactic:
exact Submodule.mem_sup_left (mem_set_smul_of_mem_mem hr hn)

Result:
no goals

Proof state:
case inr
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
s t : Set S
r✝ : S
n✝ : M
hr : r✝ ∈ t
hn : n✝ ∈ N
⊢ r✝ • n✝ ∈ s • N ⊔ t • N

Tactic:
exact Submodule.mem_sup_right (mem_set_smul_of_mem_mem hr hn)

Result:
no goals

Proof state:
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
s t : Set S
⊢ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s ⊔ t → n ∈ N → r • n ∈ s • N ⊔ t • N

Tactic:
rintro _ _ (hr|hr) hn

Result:
case inl
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
s t : Set S
r✝ : S
n✝ : M
hr : r✝ ∈ s
hn : n✝ ∈ N
⊢ r✝ • n✝ ∈ s • N ⊔ t • N

case inr
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
s t : Set S
r✝ : S
n✝ : M
hr : r✝ ∈ t
hn : n✝ ∈ N
⊢ r✝ • n✝ ∈ s • N ⊔ t • N
-- Mathlib/Data/Finset/Image.lean
theorem filter_mem_image_eq_image (f : α → β) (s : Finset α) (t : Finset β) (h : ∀ x ∈ s, f x ∈ t) :
    (t.filter fun y => y ∈ s.image f) = s.image f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
h : ∀ x ∈ s, f x ∈ t
⊢ filter (fun y => y ∈ image f s) t = image f s

Tactic:
rwa [filter_mem_eq_inter, inter_eq_right, image_subset_iff]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem relations_liftable {G : Type*} [Group G] {f : B → G} (hf : IsLiftable M f)
    (r : FreeGroup B) (hr : r ∈ M.relationsSet) : (FreeGroup.lift f) r = 1

Proof state:
B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst✝ : Group G
f : B → G
hf : M.IsLiftable f
r : FreeGroup B
hr : r ∈ M.relationsSet
⊢ (FreeGroup.lift f) r = 1

Tactic:
rcases hr with ⟨⟨i, i'⟩, rfl⟩

Result:
case intro.mk
B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst✝ : Group G
f : B → G
hf : M.IsLiftable f
i i' : B
⊢ (FreeGroup.lift f) (uncurry M.relation (i, i')) = 1

Proof state:
case intro.mk
B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst✝ : Group G
f : B → G
hf : M.IsLiftable f
i i' : B
⊢ (FreeGroup.lift f) (uncurry M.relation (i, i')) = 1

Tactic:
rw [uncurry, relation, map_pow, _root_.map_mul, FreeGroup.lift.of, FreeGroup.lift.of]

Result:
case intro.mk
B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst✝ : Group G
f : B → G
hf : M.IsLiftable f
i i' : B
⊢ (f (i, i').1 * f (i, i').2) ^ M.M (i, i').1 (i, i').2 = 1

Proof state:
case intro.mk
B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst✝ : Group G
f : B → G
hf : M.IsLiftable f
i i' : B
⊢ (f (i, i').1 * f (i, i').2) ^ M.M (i, i').1 (i, i').2 = 1

Tactic:
exact hf i i'

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem four_zero_nine_six_lt_exp_sixteen : 4096 < exp 16

Proof state:
⊢ 4096 = 2 ^ 12

Tactic:
norm_cast

Result:
no goals

Proof state:
⊢ 0 < 4096

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ 4096 < rexp 16

Tactic:
rw [← log_lt_iff_lt_exp (show (0 : ℝ) < 4096 by norm_num), show (4096 : ℝ) = 2 ^ 12 by norm_cast,
  ← rpow_natCast, log_rpow zero_lt_two, cast_ofNat]

Result:
⊢ 12 * log 2 < 16

Proof state:
⊢ 12 * log 2 < 16

Tactic:
linarith [log_two_lt_d9]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem Bool.imp_to_or (a b : Bool) : ((a = true) → (b = true)) = (((!a) || b) = true)

Proof state:
a b : Bool
⊢ (a = true → b = true) = ((!a || b) = true)

Tactic:
revert a b

Result:
⊢ ∀ (a b : Bool), (a = true → b = true) = ((!a || b) = true)

Proof state:
⊢ ∀ (a b : Bool), (a = true → b = true) = ((!a || b) = true)

Tactic:
decide

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem BddAbove.union [IsDirected α (· ≤ ·)] {s t : Set α} :
    BddAbove s → BddAbove t → BddAbove (s ∪ t)

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
c : α
hca : a ≤ c
hcb : b ≤ c
⊢ (upperBounds s ∩ upperBounds t).Nonempty

Tactic:
exact ⟨c, upperBounds_mono_mem hca ha, upperBounds_mono_mem hcb hb⟩

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
s t : Set α
⊢ BddAbove s → BddAbove t → BddAbove (s ∪ t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Result:
case intro.intro
α : Type u
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
⊢ BddAbove (s ∪ t)

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
c : α
hca : a ≤ c
hcb : b ≤ c
⊢ BddAbove (s ∪ t)

Tactic:
rw [BddAbove, upperBounds_union]

Result:
case intro.intro.intro.intro
α : Type u
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
c : α
hca : a ≤ c
hcb : b ≤ c
⊢ (upperBounds s ∩ upperBounds t).Nonempty

Proof state:
case intro.intro
α : Type u
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
⊢ BddAbove (s ∪ t)

Tactic:
obtain ⟨c, hca, hcb⟩ := exists_ge_ge a b

Result:
case intro.intro.intro.intro
α : Type u
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
c : α
hca : a ≤ c
hcb : b ≤ c
⊢ BddAbove (s ∪ t)
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem map_mem_nthRootsFinset {S F : Type*} [CommRing S] [IsDomain S] [FunLike F R S]
    [RingHomClass F R S] {x : R} (hx : x ∈ nthRootsFinset n R) (f : F) :
    f x ∈ nthRootsFinset n S

Proof state:
case neg
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
x : R
hx : x ∈ nthRootsFinset n R
f : F
hn : ¬n = 0
⊢ f x ∈ nthRootsFinset n S

Tactic:
rw [mem_nthRootsFinset <| Nat.pos_of_ne_zero hn, ← map_pow, (mem_nthRootsFinset <|
  Nat.pos_of_ne_zero hn).1 hx, map_one]

Result:
no goals

Proof state:
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
x : R
hx : x ∈ nthRootsFinset n R
f : F
⊢ f x ∈ nthRootsFinset n S

Tactic:
by_cases hn : n = 0

Result:
case pos
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
x : R
hx : x ∈ nthRootsFinset n R
f : F
hn : n = 0
⊢ f x ∈ nthRootsFinset n S

case neg
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
x : R
hx : x ∈ nthRootsFinset n R
f : F
hn : ¬n = 0
⊢ f x ∈ nthRootsFinset n S

Proof state:
case pos
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
x : R
hx : x ∈ nthRootsFinset n R
f : F
hn : n = 0
⊢ f x ∈ nthRootsFinset n S

Tactic:
simp [hn] at hx

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem Real.LogDeriv_exp : logDeriv (Real.exp) = 1

Proof state:
case h
x✝ : ℝ
⊢ logDeriv rexp x✝ = 1 x✝

Tactic:
rw [logDeriv, Real.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]

Result:
no goals

Proof state:
⊢ logDeriv rexp = 1

Tactic:
ext

Result:
case h
x✝ : ℝ
⊢ logDeriv rexp x✝ = 1 x✝
-- Mathlib/Algebra/Group/Even.lean
@[to_additive]
lemma IsSquare.div [DivisionCommMonoid α] {a b : α} (ha : IsSquare a) (hb : IsSquare b) :
    IsSquare (a / b)

Proof state:
α : Type u_2
inst✝ : DivisionCommMonoid α
a b : α
ha : IsSquare a
hb : IsSquare b
⊢ IsSquare (a * b⁻¹)

Tactic:
exact ha.mul hb.inv

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DivisionCommMonoid α
a b : α
ha : IsSquare a
hb : IsSquare b
⊢ IsSquare (a / b)

Tactic:
rw [div_eq_mul_inv]

Result:
α : Type u_2
inst✝ : DivisionCommMonoid α
a b : α
ha : IsSquare a
hb : IsSquare b
⊢ IsSquare (a * b⁻¹)
-- Mathlib/Data/List/Forall2.lean
theorem forall₂_nil_left_iff {l} : Forall₂ R nil l ↔ l = nil :=
  ⟨fun H => by cases H; rfl, by rintro rfl; exact Forall₂.nil⟩

Proof state:
case nil
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ [] = []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List β
⊢ l = [] → Forall₂ R [] l

Tactic:
rintro rfl

Result:
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ Forall₂ R [] []

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List β
H : Forall₂ R [] l
⊢ l = []

Tactic:
cases H

Result:
case nil
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ [] = []

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ Forall₂ R [] []

Tactic:
exact Forall₂.nil

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem factors_mk (a : α) (h : a ≠ 0) : (Associates.mk a).factors = factors' a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
h : a ≠ 0
⊢ (Associates.mk a).factors = ↑(factors' a)

Tactic:
apply dif_neg

Result:
case hnc
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
h : a ≠ 0
⊢ ¬Associates.mk a = 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
h : a ≠ 0
⊢ (Associates.mk a).factors = ↑(factors' a)

Tactic:
classical
  apply dif_neg
  apply mt mk_eq_zero.1 h

Result:
no goals

Proof state:
case hnc
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
h : a ≠ 0
⊢ ¬Associates.mk a = 0

Tactic:
apply mt mk_eq_zero.1 h

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Iio : (some : α → WithBot α) '' Iio a = Ioo (⊥ : WithBot α) a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Iio a = Ioo ⊥ ↑a

Tactic:
rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe, inter_comm, Ioi_inter_Iio]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem fst_inf_snd : Submodule.fst R M M₂ ⊓ Submodule.snd R M M₂ = ⊥

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ fst R M M₂ ⊓ snd R M M₂ = ⊥

Tactic:
rw [eq_bot_iff]

Result:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ fst R M M₂ ⊓ snd R M M₂ ≤ ⊥

Proof state:
case mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M
y : M₂
⊢ (x, y) ∈ fst R M M₂ ⊓ snd R M M₂ → (x, y) ∈ ⊥

Tactic:
simp only [fst, comap_bot, snd, mem_inf, mem_ker, snd_apply, fst_apply, mem_bot,
  Prod.mk_eq_zero, and_comm, imp_self]

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ fst R M M₂ ⊓ snd R M M₂ ≤ ⊥

Tactic:
rintro ⟨x, y⟩

Result:
case mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M
y : M₂
⊢ (x, y) ∈ fst R M M₂ ⊓ snd R M M₂ → (x, y) ∈ ⊥