harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem reachable_iff_reflTransGen (u v : V) :
    G.Reachable u v ↔ Relation.ReflTransGen G.Adj u v

Proof state:
case mpr
V : Type u
G : SimpleGraph V
u v : V
⊢ Relation.ReflTransGen G.Adj u v → G.Reachable u v

Tactic:
intro h

Result:
case mpr
V : Type u
G : SimpleGraph V
u v : V
h : Relation.ReflTransGen G.Adj u v
⊢ G.Reachable u v

Proof state:
case mpr.refl
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u u

Tactic:
rfl

Result:
no goals

Proof state:
case mp.intro.cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : Relation.ReflTransGen G.Adj v✝ w✝
⊢ Relation.ReflTransGen G.Adj u✝ w✝

Tactic:
exact (Relation.ReflTransGen.single h').trans ih

Result:
no goals

Proof state:
case mp.intro.nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ Relation.ReflTransGen G.Adj u✝ u✝

Tactic:
rfl

Result:
no goals

Proof state:
case mp
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v → Relation.ReflTransGen G.Adj u v

Tactic:
rintro ⟨h⟩

Result:
case mp.intro
V : Type u
G : SimpleGraph V
u v : V
h : G.Walk u v
⊢ Relation.ReflTransGen G.Adj u v

Proof state:
case mpr
V : Type u
G : SimpleGraph V
u v : V
h : Relation.ReflTransGen G.Adj u v
⊢ G.Reachable u v

Tactic:
induction h with
| refl => rfl
| tail _ ha hr => exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩

Result:
no goals

Proof state:
case mp.intro
V : Type u
G : SimpleGraph V
u v : V
h : G.Walk u v
⊢ Relation.ReflTransGen G.Adj u v

Tactic:
induction h with
| nil => rfl
| cons h' _ ih => exact (Relation.ReflTransGen.single h').trans ih

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v ↔ Relation.ReflTransGen G.Adj u v

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v → Relation.ReflTransGen G.Adj u v

case mpr
V : Type u
G : SimpleGraph V
u v : V
⊢ Relation.ReflTransGen G.Adj u v → G.Reachable u v

Proof state:
case mpr.tail
V : Type u
G : SimpleGraph V
u v b✝ c✝ : V
a✝ : Relation.ReflTransGen G.Adj u b✝
ha : G.Adj b✝ c✝
hr : G.Reachable u b✝
⊢ G.Reachable u c✝

Tactic:
exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem associated_generator_span_self [IsPrincipalIdealRing R] [IsDomain R] (r : R) :
    Associated (generator <| Ideal.span {r}) r

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
r : R
⊢ Ideal.span {generator (Ideal.span {r})} = Ideal.span {r}

Tactic:
exact Ideal.span_singleton_generator _

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
r : R
⊢ Associated (generator (Ideal.span {r})) r

Tactic:
rw [← Ideal.span_singleton_eq_span_singleton]

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
r : R
⊢ Ideal.span {generator (Ideal.span {r})} = Ideal.span {r}
-- Mathlib/Order/JordanHolder.lean
theorem exists_last_eq_snoc_equivalent (s : CompositionSeries X) (x : X) (hm : IsMaximal x s.last)
    (hb : s.head ≤ x) :
    ∃ t : CompositionSeries X,
      t.head = s.head ∧ t.length + 1 = s.length ∧
      ∃ htx : t.last = x,
        Equivalent s (snoc t s.last (show IsMaximal t.last _ from htx.symm ▸ hm))

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
t : CompositionSeries X
htb : head t = (eraseLast s).head
htl : t.length + 1 = n
htt : last t = x ⊓ (eraseLast s).last
hteqv : Equivalent (eraseLast s) (snoc t (eraseLast s).last ⋯)
hmtx : IsMaximal (last t) x
⊢ (snoc t x hmtx).head = head s

Tactic:
simp [htb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_attach (l : Vector α n) {p : {x // x ∈ l} → Prop} (f : ∀ a, p a → β) (H) :
    pmap f l.attach H =
      l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩)

Proof state:
α : Type ?u.32223
n : Nat
β : Type ?u.32269
l : Vector α n
p : { x // x ∈ l } → Prop
f : (a : { x // x ∈ l }) → p a → β
H : ∀ (a : { x // x ∈ l }), a ∈ l.attach → p a
a : α
h : a ∈ l
⊢ ⟨a, h⟩ ∈ l.attach

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
p : { x // x ∈ l } → Prop
f : (a : { x // x ∈ l }) → p a → β
H : ∀ (a : { x // x ∈ l }), a ∈ l.attach → p a
⊢ pmap f l.attach H = pmap (fun a h => f ⟨a, ⋯⟩ ⋯) l ⋯

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/Part.lean
theorem bind_le {α} (x : Part α) (f : α → Part β) (y : Part β) :
    x >>= f ≤ y ↔ ∀ a, a ∈ x → f a ≤ y

Proof state:
case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ a ∈ x, f a ≤ y
b : β
h' : ∃ a ∈ x, b ∈ f a
⊢ b ∈ y

Tactic:
rcases h' with ⟨a, h₀, h₁⟩

Result:
case mpr.intro.intro
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ a ∈ x, f a ≤ y
b : β
a : α
h₀ : a ∈ x
h₁ : b ∈ f a
⊢ b ∈ y

Proof state:
case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ a ∈ x, f a ≤ y
b : β
h' : b ∈ x >>= f
⊢ b ∈ y

Tactic:
simp only [exists_prop, bind_eq_bind, mem_bind_iff] at h'

Result:
case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ a ∈ x, f a ≤ y
b : β
h' : ∃ a ∈ x, b ∈ f a
⊢ b ∈ y

Proof state:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
⊢ ∀ a ∈ x, f a ≤ y

Tactic:
intro a h' b

Result:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
⊢ b ∈ f a → b ∈ y

Proof state:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : ∀ x_1 ∈ x, b ∈ f x_1 → b ∈ y
⊢ b ∈ f a → b ∈ y

Tactic:
apply h _ h'

Result:
no goals

Proof state:
case mpr.intro.intro
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ a ∈ x, f a ≤ y
b : β
a : α
h₀ : a ∈ x
h₁ : b ∈ f a
⊢ b ∈ y

Tactic:
apply h _ h₀ _ h₁

Result:
no goals

Proof state:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ x >>= f ≤ y ↔ ∀ a ∈ x, f a ≤ y

Tactic:
constructor <;> intro h

Result:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
⊢ ∀ a ∈ x, f a ≤ y

case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ a ∈ x, f a ≤ y
⊢ x >>= f ≤ y

Proof state:
case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ a ∈ x, f a ≤ y
⊢ x >>= f ≤ y

Tactic:
intro b h'

Result:
case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ a ∈ x, f a ≤ y
b : β
h' : b ∈ x >>= f
⊢ b ∈ y

Proof state:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : b ∈ x >>= f → b ∈ y
⊢ b ∈ f a → b ∈ y

Tactic:
simp only [and_imp, exists_prop, bind_eq_bind, mem_bind_iff, exists_imp] at h

Result:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : ∀ x_1 ∈ x, b ∈ f x_1 → b ∈ y
⊢ b ∈ f a → b ∈ y

Proof state:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
⊢ b ∈ f a → b ∈ y

Tactic:
have h := h b

Result:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : b ∈ x >>= f → b ∈ y
⊢ b ∈ f a → b ∈ y
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
lemma quasiSeparatedSpace_iff_quasiCompact_prod_lift :
    QuasiSeparatedSpace X ↔ QuasiCompact (prod.lift (𝟙 X) (𝟙 X))

Proof state:
X : Scheme
⊢ autoParam (QuasiCompact (pullback.diagonal (terminal.from X))) _auto✝ ↔
    QuasiCompact (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)

Tactic:
congr!

Result:
case a.h.e'_3
X : Scheme
⊢ pullback.diagonal (terminal.from X) = prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom

Proof state:
X : Scheme
⊢ QuasiSeparatedSpace ↑↑X.toPresheafedSpace ↔ QuasiCompact (prod.lift (𝟙 X) (𝟙 X))

Tactic:
rw [← MorphismProperty.cancel_right_of_respectsIso @QuasiCompact _ (prodIsoPullback X X).hom,
  ← HasAffineProperty.iff_of_isAffine (f := terminal.from X) (P := @QuasiSeparated),
  quasiSeparated_iff]

Result:
X : Scheme
⊢ autoParam (QuasiCompact (pullback.diagonal (terminal.from X))) _auto✝ ↔
    QuasiCompact (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)

Proof state:
case a.h.e'_3
X : Scheme
⊢ pullback.diagonal (terminal.from X) = prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom

Tactic:
ext : 1 <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem monotoneOn_posLog : MonotoneOn log⁺ (Set.Ici 0)

Proof state:
case neg.h
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
h : ¬log x ≤ 0
⊢ 0 ≤ log y ∧ log x ≤ log y

Tactic:
have := log_le_log (lt_trans Real.zero_lt_one ((log_pos_iff hx).1 (not_le.1 h))) hxy

Result:
case neg.h
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
h : ¬log x ≤ 0
this : log x ≤ log y
⊢ 0 ≤ log y ∧ log x ≤ log y

Proof state:
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y

Tactic:
by_cases h : log x ≤ 0

Result:
case pos
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
h : log x ≤ 0
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y

case neg
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
h : ¬log x ≤ 0
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y

Proof state:
case neg.h
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
h : ¬log x ≤ 0
this : log x ≤ log y
⊢ 0 ≤ log y

Tactic:
linarith

Result:
no goals

Proof state:
case pos
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
h : log x ≤ 0
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y

Tactic:
tauto

Result:
no goals

Proof state:
⊢ MonotoneOn log⁺ (Set.Ici 0)

Tactic:
intro x hx y hy hxy

Result:
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
⊢ log⁺ x ≤ log⁺ y

Proof state:
case neg.h
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
h : ¬log x ≤ 0
this : log x ≤ log y
⊢ 0 ≤ log y ∧ log x ≤ log y

Tactic:
simp only [this, and_true, ge_iff_le]

Result:
case neg.h
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
h : ¬log x ≤ 0
this : log x ≤ log y
⊢ 0 ≤ log y

Proof state:
case neg
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
h : ¬log x ≤ 0
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y

Tactic:
right

Result:
case neg.h
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
h : ¬log x ≤ 0
⊢ 0 ≤ log y ∧ log x ≤ log y

Proof state:
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
⊢ log⁺ x ≤ log⁺ y

Tactic:
simp only [posLog, le_sup_iff, sup_le_iff, le_refl, true_and]

Result:
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
hxy : x ≤ y
⊢ log x ≤ 0 ∨ 0 ≤ log y ∧ log x ≤ log y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_push {l : Vector α n} {a : α} {f : (i : Nat) → α → (h : i < n + 1) → β} :
    mapFinIdx (l.push a) f =
      (mapFinIdx l (fun i a h => f i a (by omega))).push (f l.size a (by simp))

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
a : α
f : (i : Nat) → α → i < n + 1 → β
⊢ (l.push a).mapFinIdx f = (l.mapFinIdx fun i a h => f i a ⋯).push (f l.size a ⋯)

Tactic:
simp [← append_singleton, mapFinIdx_append]

Result:
no goals

Proof state:
α : Type ?u.25125
n : Nat
β : Type ?u.25177
l : Vector α n
a : α
f : (i : Nat) → α → i < n + 1 → β
⊢ l.size < n + 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.25125
n : Nat
β : Type ?u.25177
l : Vector α n
a✝ : α
f : (i : Nat) → α → i < n + 1 → β
i : Nat
a : α
h : i < n
⊢ i < n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem univ_pi_Ioc_ae_eq_Icc {f g : ∀ i, α i} :
    (pi univ fun i => Ioc (f i) (g i)) =ᵐ[Measure.pi μ] Icc f g

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i => Ioc (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Icc f g

Tactic:
rw [← pi_univ_Icc]

Result:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i => Ioc (f i) (g i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Icc (f i) (g i)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i => Ioc (f i) (g i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Icc (f i) (g i)

Tactic:
exact pi_Ioc_ae_eq_pi_Icc

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem harm_mean_le_geom_mean_weighted (w z : ι → ℝ) (hs : s.Nonempty) (hw : ∀ i ∈ s, 0 < w i)
    (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 < z i) :
    (∑ i ∈ s, w i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 < z i
p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i
s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹
this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : 0 < (∏ i ∈ s, z i ^ w i)⁻¹
⊢ ∏ x ∈ s, (z x ^ w x)⁻¹ ≤ ∏ i ∈ s, (z i)⁻¹ ^ w i

Tactic:
gcongr

Result:
case h0
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 < z i
p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i
s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹
this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : 0 < (∏ i ∈ s, z i ^ w i)⁻¹
⊢ ∀ i ∈ s, 0 ≤ (z i ^ w i)⁻¹

case h1
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 < z i
p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i
s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹
this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : 0 < (∏ i ∈ s, z i ^ w i)⁻¹
i✝ : ι
a✝ : i✝ ∈ s
⊢ (z i✝ ^ w i✝)⁻¹ ≤ (z i✝)⁻¹ ^ w i✝

Proof state:
case h1
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 < z i
p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i
s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹
this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : 0 < (∏ i ∈ s, z i ^ w i)⁻¹
i✝ : ι
a✝ : i✝ ∈ s
⊢ (z i✝ ^ w i✝)⁻¹ ≤ (z i✝)⁻¹ ^ w i✝

Tactic:
rw [Real.inv_rpow]

Result:
case h1.hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 < z i
p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i
s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹
this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : 0 < (∏ i ∈ s, z i ^ w i)⁻¹
i✝ : ι
a✝ : i✝ ∈ s
⊢ 0 ≤ z i✝
-- Mathlib/Analysis/Calculus/Deriv/Polynomial.lean
theorem derivWithin_aeval (hxs : UniqueDiffWithinAt 𝕜 s x) :
    derivWithin (fun x => aeval x q) s x = aeval x (derivative q)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R 𝕜
q : R[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x => (aeval x) q) s x = (aeval x) (derivative q)

Tactic:
simpa only [aeval_def, eval₂_eq_eval_map, derivative_map] using
  (q.map (algebraMap R 𝕜)).derivWithin hxs

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
lemma hurwitzZetaEven_eq (a : UnitAddCircle) (s : ℂ) :
    hurwitzZetaEven a s = (hurwitzZeta a s + hurwitzZeta (-a) s) / 2

Proof state:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaEven a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s + (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2

Tactic:
ring_nf

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaEven a s = (hurwitzZeta a s + hurwitzZeta (-a) s) / 2

Tactic:
simp only [hurwitzZeta, hurwitzZetaEven_neg, hurwitzZetaOdd_neg]

Result:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaEven a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s + (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2
-- Mathlib/MeasureTheory/PiSystem.lean
theorem has_diff {s₁ s₂ : Set α} (h₁ : d.Has s₁) (h₂ : d.Has s₂) (h : s₂ ⊆ s₁) :
    d.Has (s₁ \ s₂)

Proof state:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ \ s₂)ᶜ

Tactic:
simp only [diff_eq, compl_inter, compl_compl]

Result:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ᶜ ∪ s₂)

Proof state:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ \ s₂)

Tactic:
apply d.has_compl_iff.1

Result:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ \ s₂)ᶜ

Proof state:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ᶜ ∪ s₂)

Tactic:
exact d.has_union (d.has_compl h₁) h₂ (disjoint_compl_left.mono_right h)

Result:
no goals
-- Mathlib/RingTheory/Ideal/Span.lean
theorem span_singleton_eq_span_singleton {α : Type u} [CommRing α] [IsDomain α] {x y : α} :
    span ({x} : Set α) = span ({y} : Set α) ↔ Associated x y

Proof state:
α : Type u
inst✝¹ : CommRing α
inst✝ : IsDomain α
x y : α
⊢ span {x} = span {y} ↔ Associated x y

Tactic:
rw [← dvd_dvd_iff_associated, le_antisymm_iff, and_comm]

Result:
α : Type u
inst✝¹ : CommRing α
inst✝ : IsDomain α
x y : α
⊢ span {y} ≤ span {x} ∧ span {x} ≤ span {y} ↔ x ∣ y ∧ y ∣ x

Proof state:
α : Type u
inst✝¹ : CommRing α
inst✝ : IsDomain α
x y : α
⊢ span {y} ≤ span {x} ∧ span {x} ≤ span {y} ↔ x ∣ y ∧ y ∣ x

Tactic:
apply and_congr <;> rw [span_singleton_le_span_singleton]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ici_inter_Ici {a b : α} : Ici a ∩ Ici b = Ici (a ⊔ b)

Proof state:
α : Type u_1
inst✝ : SemilatticeSup α
a b : α
⊢ Ici a ∩ Ici b = Ici (a ⊔ b)

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : SemilatticeSup α
a b x : α
⊢ x ∈ Ici a ∩ Ici b ↔ x ∈ Ici (a ⊔ b)

Proof state:
case h
α : Type u_1
inst✝ : SemilatticeSup α
a b x : α
⊢ x ∈ Ici a ∩ Ici b ↔ x ∈ Ici (a ⊔ b)

Tactic:
simp [Ici]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_some_fun : filterMap (some : α → Option α) = id

Proof state:
α : Type u_1
⊢ filterMap some = id

Tactic:
funext l

Result:
case h
α : Type u_1
l : List α
⊢ filterMap some l = id l

Proof state:
case h
α : Type u_1
l : List α
⊢ map (fun x => x) l = id l

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
l : List α
⊢ filterMap some l = id l

Tactic:
erw [filterMap_eq_map]

Result:
case h
α : Type u_1
l : List α
⊢ map (fun x => x) l = id l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem findSome?_subtype {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.findSome? f = l.unattach.findSome? g

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ List.findSome? f toList✝ = List.findSome? g toList✝.unattach

Tactic:
rw [List.findSome?_subtype hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : Array { x // p x }
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findSome? f l = findSome? g l.unattach

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ findSome? f { toList := toList✝ } = findSome? g { toList := toList✝ }.unattach

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ findSome? f { toList := toList✝ } = findSome? g { toList := toList✝ }.unattach

Tactic:
simp

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ List.findSome? f toList✝ = List.findSome? g toList✝.unattach
-- Mathlib/Logic/Relation.lean
theorem cases_head (h : ReflTransGen r a b) : a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b

Proof state:
α : Type u_1
r : α → α → Prop
a b a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ r a✝¹ ?m.15591

Tactic:
assumption

Result:
no goals

Proof state:
case refl.h
α : Type u_1
r : α → α → Prop
a b : α
⊢ b = b

Tactic:
rfl

Result:
no goals

Proof state:
case refl
α : Type u_1
r : α → α → Prop
a b : α
⊢ b = b ∨ ∃ c, r b c ∧ ReflTransGen r c b

Tactic:
left

Result:
case refl.h
α : Type u_1
r : α → α → Prop
a b : α
⊢ b = b

Proof state:
case head
α : Type u_1
r : α → α → Prop
a b a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ a✝¹ = b ∨ ∃ c, r a✝¹ c ∧ ReflTransGen r c b

Tactic:
right

Result:
case head.h
α : Type u_1
r : α → α → Prop
a b a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ ∃ c, r a✝¹ c ∧ ReflTransGen r c b

Proof state:
α : Type u_1
r : α → α → Prop
a b a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ ReflTransGen r c✝ b

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
⊢ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b

Tactic:
induction h using Relation.ReflTransGen.head_induction_on

Result:
case refl
α : Type u_1
r : α → α → Prop
a b : α
⊢ b = b ∨ ∃ c, r b c ∧ ReflTransGen r c b

case head
α : Type u_1
r : α → α → Prop
a b a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ a✝¹ = b ∨ ∃ c, r a✝¹ c ∧ ReflTransGen r c b

Proof state:
case head.h
α : Type u_1
r : α → α → Prop
a b a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ ∃ c, r a✝¹ c ∧ ReflTransGen r c b

Tactic:
exact ⟨_, by assumption, by assumption⟩

Result:
no goals