harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Contraction.lean
theorem transpose_dualTensorHom (f : Module.Dual R M) (m : M) :
    Dual.transpose (R := R) (dualTensorHom R M M (f ⊗ₜ m)) =
    dualTensorHom R _ _ (Dual.eval R M m ⊗ₜ f)

Proof state:
case h.h
R : Type u
M : Type v₁
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : Dual R M
m : M
f' : Dual R M
m' : M
⊢ f m' * f' m = f' m * f m'

Tactic:
exact mul_comm _ _

Result:
no goals

Proof state:
case h.h
R : Type u
M : Type v₁
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : Dual R M
m : M
f' : Dual R M
m' : M
⊢ ((Dual.transpose ((dualTensorHom R M M) (f ⊗ₜ[R] m))) f') m' =
    (((dualTensorHom R (Dual R M) (Dual R M)) ((Dual.eval R M) m ⊗ₜ[R] f)) f') m'

Tactic:
simp only [Dual.transpose_apply, coe_comp, Function.comp_apply, dualTensorHom_apply,
  LinearMap.map_smulₛₗ, RingHom.id_apply, Algebra.id.smul_eq_mul, Dual.eval_apply,
  LinearMap.smul_apply]

Result:
case h.h
R : Type u
M : Type v₁
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : Dual R M
m : M
f' : Dual R M
m' : M
⊢ f m' * f' m = f' m * f m'

Proof state:
R : Type u
M : Type v₁
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : Dual R M
m : M
⊢ Dual.transpose ((dualTensorHom R M M) (f ⊗ₜ[R] m)) =
    (dualTensorHom R (Dual R M) (Dual R M)) ((Dual.eval R M) m ⊗ₜ[R] f)

Tactic:
ext f' m'

Result:
case h.h
R : Type u
M : Type v₁
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : Dual R M
m : M
f' : Dual R M
m' : M
⊢ ((Dual.transpose ((dualTensorHom R M M) (f ⊗ₜ[R] m))) f') m' =
    (((dualTensorHom R (Dual R M) (Dual R M)) ((Dual.eval R M) m ⊗ₜ[R] f)) f') m'
-- Mathlib/Data/Finset/Grade.lean
lemma covBy_iff_exists_cons : s ⋖ t ↔ ∃ a, ∃ ha : a ∉ s, s.cons a ha = t :=
  ⟨CovBy.exists_finset_cons, by rintro ⟨a, ha, rfl⟩; exact covBy_cons _⟩

Proof state:
case intro.intro
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
⊢ s ⋖ cons a s ha

Tactic:
exact covBy_cons _

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
⊢ (∃ a, ∃ (ha : a ∉ s), cons a s ha = t) → s ⋖ t

Tactic:
rintro ⟨a, ha, rfl⟩

Result:
case intro.intro
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
⊢ s ⋖ cons a s ha
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem interpolate_eq_sum_interpolate_insert_sdiff (hvt : Set.InjOn v t) (hs : s.Nonempty)
    (hst : s ⊆ t) :
    interpolate t v r = ∑ i ∈ s, interpolate (insert i (t \ s)) v r * Lagrange.basis s v i

Proof state:
case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = r i

Tactic:
rw [← add_sum_erase _ _ hi', eval_basis_self (hvt.mono hst) hi',
  eval_interpolate_at_node _
    (hvt.mono (coe_subset.mpr (insert_subset_iff.mpr ⟨hi, sdiff_subset⟩)))
    (mem_insert_self _ _),
  mul_one, add_right_eq_self]

Result:
case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ ∑ x ∈ s.erase i, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = 0
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma IsCycle.getVert_endpoint_iff {i : ℕ} {p : G.Walk u u} (hpc : p.IsCycle) (hl : i ≤ p.length) :
    p.getVert i = u ↔ i = 0 ∨ i = p.length

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ p.getVert i = u → i = 0 ∨ i = p.length

Tactic:
rw [or_iff_not_imp_left]

Result:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ p.getVert i = u → ¬i = 0 → i = p.length

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ p.getVert i = u ↔ i = 0 ∨ i = p.length

Tactic:
refine ⟨?_, by aesop⟩

Result:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ p.getVert i = u → i = 0 ∨ i = p.length

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ i = p.length

Tactic:
exact hpc.getVert_injOn (by simp only [Set.mem_setOf_eq]; omega)
  (by simp only [Set.mem_setOf_eq]; omega) (h.symm ▸ (Walk.getVert_length p).symm)

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ i ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
simp only [Set.mem_setOf_eq]

Result:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 1 ≤ i ∧ i ≤ p.length

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ i = 0 ∨ i = p.length → p.getVert i = u

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ p.length ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
simp only [Set.mem_setOf_eq]

Result:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 1 ≤ p.length ∧ p.length ≤ p.length

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 1 ≤ p.length ∧ p.length ≤ p.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 1 ≤ i ∧ i ≤ p.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ p.getVert i = u → ¬i = 0 → i = p.length

Tactic:
intro h hi

Result:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ i = p.length
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem exists_ne_zero_mem_ringOfIntegers_lt (h : minkowskiBound K ↑1 < volume (convexBodyLT K f)) :
    ∃ a : 𝓞 K, a ≠ 0 ∧ ∀ w : InfinitePlace K, w a < f w

Proof state:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
h : minkowskiBound K 1 < volume (convexBodyLT K f)
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_bd : ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) a) < ↑(f w)
⊢ ∃ a, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(f w)

Tactic:
exact ⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
h : minkowskiBound K 1 < volume (convexBodyLT K f)
⊢ ∃ a, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(f w)

Tactic:
obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_lt K ↑1 h

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
h : minkowskiBound K 1 < volume (convexBodyLT K f)
w✝ : K
h_mem : w✝ ∈ ↑1
h_nz : w✝ ≠ 0
h_bd : ∀ (w : InfinitePlace K), w w✝ < ↑(f w)
⊢ ∃ a, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(f w)

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
h : minkowskiBound K 1 < volume (convexBodyLT K f)
w✝ : K
h_mem : w✝ ∈ ↑1
h_nz : w✝ ≠ 0
h_bd : ∀ (w : InfinitePlace K), w w✝ < ↑(f w)
⊢ ∃ a, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(f w)

Tactic:
obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem

Result:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
h : minkowskiBound K 1 < volume (convexBodyLT K f)
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_bd : ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) a) < ↑(f w)
⊢ ∃ a, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(f w)
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem orthocenter_mem_altitude (t : Triangle ℝ P) {i₁ : Fin 3} :
    t.orthocenter ∈ t.altitude i₁

Proof state:
case intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ t.orthocenter ∈ altitude t i₁

Tactic:
rw [orthocenter_eq_mongePoint, t.altitude_eq_mongePlane h₁₂ h₁₃ h₂₃]

Result:
case intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ mongePoint t ∈ mongePlane t i₂ i₃

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ : Fin 3
⊢ t.orthocenter ∈ altitude t i₁

Tactic:
obtain ⟨i₂, i₃, h₁₂, h₂₃, h₁₃⟩ : ∃ i₂ i₃, i₁ ≠ i₂ ∧ i₂ ≠ i₃ ∧ i₁ ≠ i₃ := by
  decide +revert

Result:
case intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ t.orthocenter ∈ altitude t i₁

Proof state:
case intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ mongePoint t ∈ mongePlane t i₂ i₃

Tactic:
exact t.mongePoint_mem_mongePlane

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ : Fin 3
⊢ ∃ i₂ i₃, i₁ ≠ i₂ ∧ i₂ ≠ i₃ ∧ i₁ ≠ i₃

Tactic:
decide +revert

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem outerMeasure_caratheodory (A : Set G) :
    MeasurableSet[μ.outerMeasure.caratheodory] A ↔
      ∀ U : Opens G, μ.outerMeasure (U ∩ A) + μ.outerMeasure (U \ A) ≤ μ.outerMeasure U

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
A : Set G
⊢ MeasurableSet A ↔
    ∀ (U : Set G) (hU : IsOpen U),
      μ.outerMeasure (↑{ carrier := U, is_open' := hU } ∩ A) + μ.outerMeasure (↑{ carrier := U, is_open' := hU } \ A) ≤
        μ.outerMeasure ↑{ carrier := U, is_open' := hU }

Tactic:
apply inducedOuterMeasure_caratheodory

Result:
case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
A : Set G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    μ.innerContent { carrier := ⋃ i, f i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := f i, is_open' := ⋯ }

case m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
A : Set G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ → μ.innerContent { carrier := s₁, is_open' := hs₁ } ≤ μ.innerContent { carrier := s₂, is_open' := hs₂ }

case PU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
A : Set G
⊢ ∀ ⦃f : ℕ → Set G⦄, (∀ (i : ℕ), IsOpen (f i)) → IsOpen (⋃ i, f i)

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
A : Set G
⊢ MeasurableSet A ↔ ∀ (U : Opens G), μ.outerMeasure (↑U ∩ A) + μ.outerMeasure (↑U \ A) ≤ μ.outerMeasure ↑U

Tactic:
rw [Opens.forall]

Result:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
A : Set G
⊢ MeasurableSet A ↔
    ∀ (U : Set G) (hU : IsOpen U),
      μ.outerMeasure (↑{ carrier := U, is_open' := hU } ∩ A) + μ.outerMeasure (↑{ carrier := U, is_open' := hU } \ A) ≤
        μ.outerMeasure ↑{ carrier := U, is_open' := hU }

Proof state:
case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
A : Set G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    μ.innerContent { carrier := ⋃ i, f i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := f i, is_open' := ⋯ }

Tactic:
apply innerContent_iUnion_nat

Result:
no goals

Proof state:
case m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
A : Set G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ → μ.innerContent { carrier := s₁, is_open' := hs₁ } ≤ μ.innerContent { carrier := s₂, is_open' := hs₂ }

Tactic:
apply innerContent_mono'

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem abs_eq_zero_iff {x : EReal} : x.abs = 0 ↔ x = 0

Proof state:
x : EReal
⊢ x.abs = 0 ↔ x = 0

Tactic:
induction x

Result:
case h_bot

⊢ ⊥.abs = 0 ↔ ⊥ = 0

case h_real
a✝ : ℝ
⊢ (↑a✝).abs = 0 ↔ ↑a✝ = 0

case h_top

⊢ ⊤.abs = 0 ↔ ⊤ = 0

Proof state:
case h_real
a✝ : ℝ
⊢ (↑a✝).abs = 0 ↔ ↑a✝ = 0

Tactic:
simp only [abs_def, coe_eq_zero, ENNReal.ofReal_eq_zero, abs_nonpos_iff]

Result:
no goals

Proof state:
case h_bot

⊢ ⊥.abs = 0 ↔ ⊥ = 0

Tactic:
simp only [abs_bot, ENNReal.top_ne_zero, bot_ne_zero]

Result:
no goals

Proof state:
case h_top

⊢ ⊤.abs = 0 ↔ ⊤ = 0

Tactic:
simp only [abs_top, ENNReal.top_ne_zero, top_ne_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Basic.lean
@[to_additive zsmul_strictMono_right]
lemma zpow_left_strictMono (hn : 0 < n) : StrictMono ((· ^ n) : α → α) := fun a b hab => by
  rw [← one_lt_div', ← div_zpow]; exact one_lt_zpow (one_lt_div'.2 hab) hn

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ (fun x => x ^ n) a < (fun x => x ^ n) b

Tactic:
rw [← one_lt_div', ← div_zpow]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ 1 < (b / a) ^ n

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ 1 < (b / a) ^ n

Tactic:
exact one_lt_zpow (one_lt_div'.2 hab) hn

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_pos {p : ℝ} {x : ℝ≥0∞} (hx_pos : 0 < x) (hx_ne_top : x ≠ ⊤) : 0 < x ^ p

Proof state:
case inr
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ⊤
hp_nonpos : p ≤ 0
⊢ x ^ (-p) ≠ ⊤

Tactic:
exact rpow_ne_top_of_nonneg (Right.nonneg_neg_iff.mpr hp_nonpos) hx_ne_top

Result:
no goals

Proof state:
case inl
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ⊤
hp_pos : 0 < p
⊢ 0 < x ^ p

Tactic:
exact rpow_pos_of_nonneg hx_pos (le_of_lt hp_pos)

Result:
no goals

Proof state:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ⊤
⊢ 0 < x ^ p

Tactic:
rcases lt_or_le 0 p with hp_pos | hp_nonpos

Result:
case inl
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ⊤
hp_pos : 0 < p
⊢ 0 < x ^ p

case inr
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ⊤
hp_nonpos : p ≤ 0
⊢ 0 < x ^ p

Proof state:
case inr
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ⊤
hp_nonpos : p ≤ 0
⊢ 0 < x ^ p

Tactic:
rw [← neg_neg p, rpow_neg, ENNReal.inv_pos]

Result:
case inr
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ⊤
hp_nonpos : p ≤ 0
⊢ x ^ (-p) ≠ ⊤
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem X_sub_C_dvd_nodal (v : ι → R) {i : ι} (hi : i ∈ s) : X - C (v i) ∣ nodal s v

Proof state:
R : Type u_1
inst✝ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
i : ι
hi : i ∈ s
⊢ X - C (v i) ∣ nodal s v

Tactic:
exact ⟨nodal (s.erase i) v, nodal_eq_mul_nodal_erase hi⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
i : ι
hi : i ∈ s
⊢ X - C (v i) ∣ nodal s v

Tactic:
classical
exact ⟨nodal (s.erase i) v, nodal_eq_mul_nodal_erase hi⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem HasFTaylorSeriesUpToOn.zero_eq' (h : HasFTaylorSeriesUpToOn n f p s) {x : E} (hx : x ∈ s) :
    p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
x : E
hx : x ∈ s
⊢ p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)

Tactic:
rw [← h.zero_eq x hx]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
x : E
hx : x ∈ s
⊢ p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (p x 0).curry0

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
x : E
hx : x ∈ s
⊢ p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (p x 0).curry0

Tactic:
exact (p x 0).uncurry0_curry0.symm

Result:
no goals
-- Mathlib/Algebra/DirectSum/Basic.lean
theorem sum_univ_of [Fintype ι] (x : ⨁ i, β i) :
    ∑ i ∈ Finset.univ, of β i (x i) = x

Proof state:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : ⨁ (i : ι), β i
i : ι
⊢ (∑ i : ι, (of β i) (x i)) i = x i

Tactic:
rw [DFinsupp.finset_sum_apply]

Result:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : ⨁ (i : ι), β i
i : ι
⊢ ∑ a : ι, ((of β a) (x a)) i = x i

Proof state:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : ⨁ (i : ι), β i
⊢ ∑ i : ι, (of β i) (x i) = x

Tactic:
apply DFinsupp.ext (fun i ↦ ?_)

Result:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : ⨁ (i : ι), β i
i : ι
⊢ (∑ i : ι, (of β i) (x i)) i = x i

Proof state:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : ⨁ (i : ι), β i
i : ι
⊢ ∑ a : ι, ((of β a) (x a)) i = x i

Tactic:
simp [of_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_alter_of_beq_eq_false [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
    (h : m.WF) (he : (k == k') = false) : k' ∈ m.alter k f ↔ k' ∈ m

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
he : (k == k') = false
⊢ k' ∈ m.alter k f ↔ k' ∈ m

Tactic:
simp only [mem_iff_contains, contains_alter_of_beq_eq_false h, he]

Result:
no goals
-- Mathlib/Analysis/Analytic/Within.lean
/-- `f` is analytic within `s` at `x` iff some local extension of `f` is analytic at `x`. In this
version, we make sure that the extension coincides with `f` on all of `insert x s`. -/
lemma analyticWithinAt_iff_exists_analyticAt' [CompleteSpace F] {f : E → F} {s : Set E} {x : E} :
    AnalyticWithinAt 𝕜 f s x ↔
      ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
⊢ (∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) ↔ ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
⊢ (∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) → ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
⊢ (∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x) → ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x

Proof state:
case refine_1.intro.intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
g' : E → F := u.piecewise g f
y : E
hy : y ∈ insert x s
⊢ f y = g' y

Tactic:
by_cases h'y : y ∈ u

Result:
case pos
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
g' : E → F := u.piecewise g f
y : E
hy : y ∈ insert x s
h'y : y ∈ u
⊢ f y = g' y

case neg
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x => f x = g x) x}
g' : E → F := u.piecewise g f
y : E
hy : y ∈ insert x s
h'y : y ∉ u
⊢ f y = g' y
-- Mathlib/Order/Filter/Pi.lean
theorem pi_mem_pi {I : Set ι} (hI : I.Finite) (h : ∀ i ∈ I, s i ∈ f i) : I.pi s ∈ pi f

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
⊢ ⋂ x, eval ↑x ⁻¹' s ↑x ∈ pi f

Tactic:
refine mem_iInf_of_iInter hI (fun i => ?_) Subset.rfl

Result:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
i : ↑I
⊢ eval ↑i ⁻¹' s ↑i ∈ comap (eval ↑i) (f ↑i)

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
i : ↑I
⊢ eval ↑i ⁻¹' s ↑i ∈ comap (eval ↑i) (f ↑i)

Tactic:
exact preimage_mem_comap (h i i.2)

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
⊢ I.pi s ∈ pi f

Tactic:
rw [pi_def, biInter_eq_iInter]

Result:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
⊢ ⋂ x, eval ↑x ⁻¹' s ↑x ∈ pi f
-- Mathlib/Order/Max.lean
theorem not_isMax_iff : ¬IsMax a ↔ ∃ b, a < b

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ¬IsMax a ↔ ∃ b, a < b

Tactic:
simp [lt_iff_le_not_le, IsMax, not_forall, exists_prop]

Result:
no goals