harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
@[reassoc (attr := simp)]
lemma πTruncGE_naturality (n : ℤ) :
    K.πTruncGE n ≫ truncGEMap φ n = φ ≫ L.πTruncGE n

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ K.πTruncGE n ≫ truncGEMap φ n = φ ≫ L.πTruncGE n

Tactic:
apply HomologicalComplex.πTruncGE_naturality

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem basisOf_reindex (i : ι') :
    (b.reindex e).basisOf i =
      (b.basisOf <| e.symm i).reindex (e.subtypeEquiv fun _ => e.eq_symm_apply.not)

Proof state:
case a
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
i : ι'
j : { j // j ≠ i }
⊢ ((b.reindex e).basisOf i) j = ((b.basisOf (e.symm i)).reindex (e.subtypeEquiv ⋯)) j

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
i : ι'
⊢ (b.reindex e).basisOf i = (b.basisOf (e.symm i)).reindex (e.subtypeEquiv ⋯)

Tactic:
ext j

Result:
case a
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
i : ι'
j : { j // j ≠ i }
⊢ ((b.reindex e).basisOf i) j = ((b.basisOf (e.symm i)).reindex (e.subtypeEquiv ⋯)) j
-- Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
theorem π_ιInvApp_eq_id (i : D.J) (U : Opens (D.U i).carrier) :
    D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 _

Proof state:
case w.h.left.mk
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
      limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (j, k))) =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (j, k)))

Tactic:
rw [← limit.w (componentwiseDiagram 𝖣.diagram.multispan _)
    (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))),
  ← Category.assoc, Category.id_comp]

Result:
case w.h.left.mk
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ ((D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
        limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
          (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))) ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))) =
    limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
        (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))) ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k)))
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem map_smul (f : V →ₗ[K] V₂) (p : Submodule K V) (a : K) (h : a ≠ 0) :
    p.map (a • f) = p.map f :=
  le_antisymm (by rw [map_le_iff_le_comap, comap_smul f _ a h, ← map_le_iff_le_comap])
    (by rw [map_le_iff_le_comap, ← comap_smul f _ a h, ← map_le_iff_le_comap])

Proof state:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a ≠ 0
⊢ map (a • f) p ≤ map f p

Tactic:
rw [map_le_iff_le_comap, comap_smul f _ a h, ← map_le_iff_le_comap]

Result:
no goals

Proof state:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a ≠ 0
⊢ map f p ≤ map (a • f) p

Tactic:
rw [map_le_iff_le_comap, ← comap_smul f _ a h, ← map_le_iff_le_comap]

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem prod_ofPNatList (l : List ℕ+) (h) : (ofPNatList l h).prod = l.prod

Proof state:
l : List ℕ+
h : ∀ p ∈ l, p.Prime
⊢ (ofPNatList l h).prod = l.prod

Tactic:
have := prod_ofPNatMultiset (l : Multiset ℕ+) h

Result:
l : List ℕ+
h : ∀ p ∈ l, p.Prime
this : (ofPNatMultiset (↑l) h).prod = (↑l).prod
⊢ (ofPNatList l h).prod = l.prod

Proof state:
l : List ℕ+
h : ∀ p ∈ l, p.Prime
this : (ofPNatMultiset (↑l) h).prod = l.prod
⊢ (ofPNatList l h).prod = l.prod

Tactic:
exact this

Result:
no goals

Proof state:
l : List ℕ+
h : ∀ p ∈ l, p.Prime
this : (ofPNatMultiset (↑l) h).prod = (↑l).prod
⊢ (ofPNatList l h).prod = l.prod

Tactic:
rw [Multiset.prod_coe] at this

Result:
l : List ℕ+
h : ∀ p ∈ l, p.Prime
this : (ofPNatMultiset (↑l) h).prod = l.prod
⊢ (ofPNatList l h).prod = l.prod
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem tan_zero : tan (0 : Angle) = 0

Proof state:
⊢ tan 0 = 0

Tactic:
rw [← coe_zero, tan_coe, Real.tan_zero]

Result:
no goals
-- Mathlib/AlgebraicTopology/ExtraDegeneracy.lean
theorem ExtraDegeneracy.s_comp_π_0 (n : ℕ) :
    ExtraDegeneracy.s f S n ≫ WidePullback.π _ 0 =
      @WidePullback.base _ _ _ f.right (fun _ : Fin (n + 1) => f.left) (fun _ => f.hom) _ ≫
        S.section_

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i =>
          if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
          else WidePullback.π (fun x => f.hom) (i.pred x))
        ⋯ ≫
      WidePullback.π (fun x => f.hom) 0 =
    (WidePullback.base fun x => f.hom) ≫ S.section_

Tactic:
simp only [WidePullback.lift_π]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ (if h : True then (WidePullback.base fun x => f.hom) ≫ S.section_
    else WidePullback.π (fun x => f.hom) (Fin.pred 0 ⋯)) =
    (WidePullback.base fun x => f.hom) ≫ S.section_

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ (if h : True then (WidePullback.base fun x => f.hom) ≫ S.section_
    else WidePullback.π (fun x => f.hom) (Fin.pred 0 ⋯)) =
    (WidePullback.base fun x => f.hom) ≫ S.section_

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ s f S n ≫ WidePullback.π (fun x => f.hom) 0 = (WidePullback.base fun x => f.hom) ≫ S.section_

Tactic:
dsimp [ExtraDegeneracy.s]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i =>
          if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
          else WidePullback.π (fun x => f.hom) (i.pred x))
        ⋯ ≫
      WidePullback.π (fun x => f.hom) 0 =
    (WidePullback.base fun x => f.hom) ≫ S.section_
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem coe_sSup {s : Set α} (hb : BddAbove s) : ↑(sSup s) = (⨆ a ∈ s, ↑a : WithTop α)

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hb : BddAbove s
⊢ ↑(sSup s) = ⨆ a ∈ s, ↑a

Tactic:
rw [coe_sSup' hb, sSup_image]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
theorem IsMatching.toEdge_eq_of_adj (h : M.IsMatching) (hv : v ∈ M.verts) (hvw : M.Adj v w) :
    h.toEdge ⟨v, hv⟩ = ⟨s(v, w), hvw⟩

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hv : v ∈ M.verts
hvw : M.Adj v w
⊢ s(v, Exists.choose ⋯) = s(v, w)

Tactic:
congr

Result:
case e_p.e_snd
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hv : v ∈ M.verts
hvw : M.Adj v w
⊢ Exists.choose ⋯ = w

Proof state:
case e_p.e_snd
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hv : v ∈ M.verts
hvw : M.Adj v w
⊢ Exists.choose ⋯ = w

Tactic:
exact ((h (M.edge_vert hvw)).choose_spec.2 w hvw).symm

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hv : v ∈ M.verts
hvw : M.Adj v w
⊢ h.toEdge ⟨v, hv⟩ = ⟨s(v, w), hvw⟩

Tactic:
simp only [IsMatching.toEdge, Subtype.mk_eq_mk]

Result:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hv : v ∈ M.verts
hvw : M.Adj v w
⊢ s(v, Exists.choose ⋯) = s(v, w)
-- Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean
lemma d_comp_desc_eq_zero_iff ⦃W : C⦄ (φ : W ⟶ cocone.pt) :
    φ ≫ hcocone.desc (CokernelCofork.ofπ (K.d j k) (K.d_comp_d i j k)) = 0 ↔
      φ ≫ ((isColimitCokernelCofork K e hj' hi hi' cocone hcocone).desc
      (CokernelCofork.ofπ ((K.extend e).d j' k') (d_comp_d _ _ _ _))) = 0 :=
  d_comp_desc_eq_zero_iff' K e hj' hk hk' cocone hcocone _ (hcocone.fac _ _) _ (by
    simpa using (isColimitCokernelCofork K e hj' hi hi' cocone hcocone).fac _
      WalkingParallelPair.one) _

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
φ : W ⟶ cocone.pt
⊢ (K.extendXIso e hj').hom ≫
      Cofork.π cocone ≫
        (isColimitCokernelCofork K e hj' hi hi' cocone hcocone).desc (CokernelCofork.ofπ ((K.extend e).d j' k') ⋯) =
    (K.extend e).d j' k'

Tactic:
simpa using (isColimitCokernelCofork K e hj' hi hi' cocone hcocone).fac _
  WalkingParallelPair.one

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isNClique_map_iff (hn : 1 < n) {t : Finset β} {f : α ↪ β} :
    (G.map f).IsNClique n t ↔ ∃ s : Finset α, G.IsNClique n s ∧ s.map f = t

Proof state:
case intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
t : Finset β
f : α ↪ β
h' : #t ≤ 1
hn : 1 < #t
⊢ False

Tactic:
exact h'.not_lt hn

Result:
no goals

Proof state:
case mp.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : G.IsClique ↑s
hn : 1 < #(map f s)
⊢ ∃ s_1, G.IsNClique (#(map f s)) s_1 ∧ map f s_1 = map f s

Tactic:
simp [isNClique_iff, hs]

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n → ∃ s, G.IsNClique n s ∧ map f s = t

Tactic:
rintro ⟨⟨s, hs, rfl⟩, rfl⟩

Result:
case mp.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : G.IsClique ↑s
hn : 1 < #(map f s)
⊢ ∃ s_1, G.IsNClique (#(map f s)) s_1 ∧ map f s_1 = map f s

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (SimpleGraph.map f G).IsNClique n t ↔ ∃ s, G.IsNClique n s ∧ map f s = t

Tactic:
rw [isNClique_iff, isClique_map_finset_iff, or_and_right,
  or_iff_right (by rintro ⟨h', rfl⟩; exact h'.not_lt hn)]

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n ↔ ∃ s, G.IsNClique n s ∧ map f s = t

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
f : α ↪ β
s : Finset α
hs : G.IsNClique n s
⊢ (∃ s_1, G.IsClique ↑s_1 ∧ map f s_1 = map f s) ∧ #(map f s) = n

Tactic:
simp [hs.card_eq, hs.isClique]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ ¬(#t ≤ 1 ∧ #t = n)

Tactic:
rintro ⟨h', rfl⟩

Result:
case intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
t : Finset β
f : α ↪ β
h' : #t ≤ 1
hn : 1 < #t
⊢ False

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n ↔ ∃ s, G.IsNClique n s ∧ map f s = t

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n → ∃ s, G.IsNClique n s ∧ map f s = t

case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ s, G.IsNClique n s ∧ map f s = t) → (∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n

Proof state:
case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ s, G.IsNClique n s ∧ map f s = t) → (∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n

Tactic:
rintro ⟨s, hs, rfl⟩

Result:
case mpr.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
f : α ↪ β
s : Finset α
hs : G.IsNClique n s
⊢ (∃ s_1, G.IsClique ↑s_1 ∧ map f s_1 = map f s) ∧ #(map f s) = n
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem sup_eq_prod_inf_factors [DecidableEq (Ideal T)] (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
    I ⊔ J = (normalizedFactors I ∩ normalizedFactors J).prod

Proof state:
case a
T : Type u_4
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain T
I J : Ideal T
inst✝ : DecidableEq (Ideal T)
hI : I ≠ ⊥
hJ : J ≠ ⊥
H : normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod = normalizedFactors I ∩ normalizedFactors J
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ∣ I ∧ (normalizedFactors I ∩ normalizedFactors J).prod ∣ J

Tactic:
constructor

Result:
case a.left
T : Type u_4
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain T
I J : Ideal T
inst✝ : DecidableEq (Ideal T)
hI : I ≠ ⊥
hJ : J ≠ ⊥
H : normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod = normalizedFactors I ∩ normalizedFactors J
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ∣ I

case a.right
T : Type u_4
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain T
I J : Ideal T
inst✝ : DecidableEq (Ideal T)
hI : I ≠ ⊥
hJ : J ≠ ⊥
H : normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod = normalizedFactors I ∩ normalizedFactors J
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ∣ J
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem _root_.BoundedVariationOn.sub_le {f : α → ℝ} {s : Set α} (h : BoundedVariationOn f s)
    {x y : α} (hx : x ∈ s) (hy : y ∈ s) : f x - f y ≤ (eVariationOn f s).toReal

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ dist (f x) (f y) ≤ (eVariationOn f s).toReal

Tactic:
exact h.dist_le hx hy

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ |f x - f y| ≤ (eVariationOn f s).toReal

Tactic:
rw [← Real.dist_eq]

Result:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ dist (f x) (f y) ≤ (eVariationOn f s).toReal

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ f x - f y ≤ (eVariationOn f s).toReal

Tactic:
apply (le_abs_self _).trans

Result:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ |f x - f y| ≤ (eVariationOn f s).toReal
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
lemma tendsto_rpow_atBot_of_base_lt_one (b : ℝ) (hb₀ : 0 < b) (hb₁ : b < 1) :
    Tendsto (b ^ · : ℝ → ℝ) atBot atTop

Proof state:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ Tendsto (fun x => b ^ x) atBot atTop

Tactic:
simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]

Result:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ Tendsto (fun x => rexp (log b * x)) atBot atTop

Proof state:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ log b < 0

Tactic:
exact (log_neg_iff hb₀).mpr hb₁

Result:
no goals

Proof state:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ 0 < b

Tactic:
positivity

Result:
no goals

Proof state:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ Tendsto (fun x => rexp (log b * x)) atBot atTop

Tactic:
refine tendsto_exp_atTop.comp <| (tendsto_const_mul_atTop_iff_neg <| tendsto_id (α := ℝ)).mpr ?_

Result:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ log b < 0
-- Mathlib/Computability/Language.lean
theorem kstar_eq_iSup_pow (l : Language α) : l∗ = ⨆ i : ℕ, l ^ i

Proof state:
α : Type u_1
l : Language α
⊢ l∗ = ⨆ i, l ^ i

Tactic:
ext x

Result:
case h
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ ⨆ i, l ^ i

Proof state:
case h.mpr.intro.intro.intro.intro
α : Type u_1
l : Language α
S : List (List α)
hS : ∀ y ∈ S, y ∈ l
⊢ ∃ L, S.flatten = L.flatten ∧ ∀ y ∈ L, y ∈ l

Tactic:
exact ⟨S, rfl, hS⟩

Result:
no goals

Proof state:
case h.mpr
α : Type u_1
l : Language α
x : List α
⊢ (∃ i S, x = S.flatten ∧ S.length = i ∧ ∀ y ∈ S, y ∈ l) → ∃ L, x = L.flatten ∧ ∀ y ∈ L, y ∈ l

Tactic:
rintro ⟨_, S, rfl, rfl, hS⟩

Result:
case h.mpr.intro.intro.intro.intro
α : Type u_1
l : Language α
S : List (List α)
hS : ∀ y ∈ S, y ∈ l
⊢ ∃ L, S.flatten = L.flatten ∧ ∀ y ∈ L, y ∈ l

Proof state:
case h
α : Type u_1
l : Language α
x : List α
⊢ (∃ L, x = L.flatten ∧ ∀ y ∈ L, y ∈ l) ↔ ∃ i S, x = S.flatten ∧ S.length = i ∧ ∀ y ∈ S, y ∈ l

Tactic:
constructor

Result:
case h.mp
α : Type u_1
l : Language α
x : List α
⊢ (∃ L, x = L.flatten ∧ ∀ y ∈ L, y ∈ l) → ∃ i S, x = S.flatten ∧ S.length = i ∧ ∀ y ∈ S, y ∈ l

case h.mpr
α : Type u_1
l : Language α
x : List α
⊢ (∃ i S, x = S.flatten ∧ S.length = i ∧ ∀ y ∈ S, y ∈ l) → ∃ L, x = L.flatten ∧ ∀ y ∈ L, y ∈ l

Proof state:
case h.mp.intro.intro
α : Type u_1
l : Language α
S : List (List α)
hS : ∀ y ∈ S, y ∈ l
⊢ ∃ i S_1, S.flatten = S_1.flatten ∧ S_1.length = i ∧ ∀ y ∈ S_1, y ∈ l

Tactic:
exact ⟨_, S, rfl, rfl, hS⟩

Result:
no goals

Proof state:
case h.mp
α : Type u_1
l : Language α
x : List α
⊢ (∃ L, x = L.flatten ∧ ∀ y ∈ L, y ∈ l) → ∃ i S, x = S.flatten ∧ S.length = i ∧ ∀ y ∈ S, y ∈ l

Tactic:
rintro ⟨S, rfl, hS⟩

Result:
case h.mp.intro.intro
α : Type u_1
l : Language α
S : List (List α)
hS : ∀ y ∈ S, y ∈ l
⊢ ∃ i S_1, S.flatten = S_1.flatten ∧ S_1.length = i ∧ ∀ y ∈ S_1, y ∈ l

Proof state:
case h
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ ⨆ i, l ^ i

Tactic:
simp only [mem_kstar, mem_iSup, mem_pow]

Result:
case h
α : Type u_1
l : Language α
x : List α
⊢ (∃ L, x = L.flatten ∧ ∀ y ∈ L, y ∈ l) ↔ ∃ i S, x = S.flatten ∧ S.length = i ∧ ∀ y ∈ S, y ∈ l
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem isCompactElement_iff.{u} {α : Type u} [CompleteLattice α] (k : α) :
    CompleteLattice.IsCompactElement k ↔
      ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t : Finset ι, k ≤ t.sup s

Proof state:
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
⊢ k ≤ iSup Subtype.val

Tactic:
delta iSup

Result:
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
⊢ k ≤ sSup (range Subtype.val)

Proof state:
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ t.sup Subtype.val
⊢ ↑(Finset.image Subtype.val t) ⊆ s

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem OrderIso.map_wcovBy {α β : Type*} [Preorder α] [Preorder β]
    (f : α ≃o β) {x y : α} : f x ⩿ f y ↔ x ⩿ y

Proof state:
case mpr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x y : α
⊢ x ⩿ y → f x ⩿ f y

Tactic:
conv_lhs => rw [← f.symm_apply_apply x, ← f.symm_apply_apply y]

Result:
case mpr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x y : α
⊢ f.symm (f x) ⩿ f.symm (f y) → f x ⩿ f y

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x y : α
⊢ f x ⩿ f y ↔ x ⩿ y

Tactic:
use f.toOrderEmbedding.wcovBy_of_apply

Result:
case mpr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x y : α
⊢ x ⩿ y → f x ⩿ f y

Proof state:
case mpr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x y : α
⊢ f.symm (f x) ⩿ f.symm (f y) → f x ⩿ f y

Tactic:
exact f.symm.toOrderEmbedding.wcovBy_of_apply

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem ofNat'_add [NeZero n] (x : Nat) (y : Fin n) :
    Fin.ofNat' n x + y = Fin.ofNat' n (x + y.val)

Proof state:
case a
n : Nat
inst✝ : NeZero n
x : Nat
y : Fin n
⊢ ↑(Fin.ofNat' n x + y) = ↑(Fin.ofNat' n (x + ↑y))

Tactic:
simp [Fin.ofNat', Fin.add_def]

Result:
no goals

Proof state:
n : Nat
inst✝ : NeZero n
x : Nat
y : Fin n
⊢ Fin.ofNat' n x + y = Fin.ofNat' n (x + ↑y)

Tactic:
apply Fin.eq_of_val_eq

Result:
case a
n : Nat
inst✝ : NeZero n
x : Nat
y : Fin n
⊢ ↑(Fin.ofNat' n x + y) = ↑(Fin.ofNat' n (x + ↑y))
-- Mathlib/RingTheory/RingHom/Unramified.lean
lemma ofLocalizationPrime :
    OfLocalizationPrime FormallyUnramified

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
⊢ x ∈ Algebra.unramifiedLocus R S

Tactic:
let Rₓ := Localization.AtPrime (x.asIdeal.comap f)

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
⊢ x ∈ Algebra.unramifiedLocus R S

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
⊢ f.FormallyUnramified

Tactic:
algebraize [f]

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.FormallyUnramified

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ (x : PrimeSpectrum S), x ∈ Algebra.unramifiedLocus R S

Tactic:
intro x

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
⊢ x ∈ Algebra.unramifiedLocus R S