harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma Sigma.map_comp_map' {f g : α → C} {h : β → C} [HasCoproduct f] [HasCoproduct g]
    [HasCoproduct h] (p : α → β) (q : ∀ (a : α), f a ⟶ g a) (q' : ∀ (a : α), g a ⟶ h (p a)) :
    Sigma.map q ≫ Sigma.map' p q' = Sigma.map' p (fun a => q a ≫ q' a)

Proof state:
case h
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g : α → C
h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h (p a)
b✝ : α
⊢ ι f b✝ ≫ map q ≫ map' p q' = ι f b✝ ≫ map' p fun a => q a ≫ q' a

Tactic:
simp

Result:
no goals

Proof state:
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g : α → C
h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h (p a)
⊢ map q ≫ map' p q' = map' p fun a => q a ≫ q' a

Tactic:
ext

Result:
case h
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g : α → C
h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h (p a)
b✝ : α
⊢ ι f b✝ ≫ map q ≫ map' p q' = ι f b✝ ≫ map' p fun a => q a ≫ q' a
-- Mathlib/CategoryTheory/Limits/FinallySmall.lean
theorem initiallySmall_of_small_weakly_initial_set [IsCofilteredOrEmpty J] (s : Set J) [Small.{v} s]
    (hs : ∀ i, ∃ j ∈ s, Nonempty (j ⟶ i)) : InitiallySmall.{v} J

Proof state:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
⊢ (fullSubcategoryInclusion fun x => x ∈ s).Initial

Tactic:
refine Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful _ (fun i => ?_)

Result:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
i : J
⊢ ∃ c, Nonempty ((fullSubcategoryInclusion fun x => x ∈ s).obj c ⟶ i)

Proof state:
case intro.intro
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
i j : J
hj₁ : j ∈ s
hj₂ : Nonempty (j ⟶ i)
⊢ ∃ c, Nonempty ((fullSubcategoryInclusion fun x => x ∈ s).obj c ⟶ i)

Tactic:
exact ⟨⟨j, hj₁⟩, hj₂⟩

Result:
no goals

Proof state:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
i : J
⊢ ∃ c, Nonempty ((fullSubcategoryInclusion fun x => x ∈ s).obj c ⟶ i)

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := hs i

Result:
case intro.intro
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
i j : J
hj₁ : j ∈ s
hj₂ : Nonempty (j ⟶ i)
⊢ ∃ c, Nonempty ((fullSubcategoryInclusion fun x => x ∈ s).obj c ⟶ i)
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem adjMatrix_mulVec_const_apply_of_regular [NonAssocSemiring α] {d : ℕ} {a : α}
    (hd : G.IsRegularOfDegree d) {v : V} : (G.adjMatrix α *ᵥ Function.const _ a) v = d * a

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
d : ℕ
a : α
hd : G.IsRegularOfDegree d
v : V
⊢ (adjMatrix α G *ᵥ Function.const V a) v = ↑d * a

Tactic:
simp [hd v]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem zero_mem_resolventSet_of_unit (a : Aˣ) : 0 ∈ resolventSet R (a : A)

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : Aˣ
⊢ 0 ∈ resolventSet R ↑a

Tactic:
simpa only [mem_resolventSet_iff, ← not_mem_iff, zero_not_mem_iff] using a.isUnit

Result:
no goals
-- Mathlib/Analysis/Convex/StrictConvexSpace.lean
theorem StrictConvexSpace.of_norm_add_ne_two
    (h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2) : StrictConvexSpace ℝ E

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
⊢ StrictConvexSpace ℝ E

Tactic:
refine
  StrictConvexSpace.of_norm_combo_ne_one fun x y hx hy hne =>
    ⟨1 / 2, 1 / 2, one_half_pos.le, one_half_pos.le, add_halves _, ?_⟩

Result:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hne : x ≠ y
⊢ ‖(1 / 2) • x + (1 / 2) • y‖ ≠ 1

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hne : x ≠ y
⊢ ¬‖x + y‖ = 2

Tactic:
exact h hx hy hne

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hne : x ≠ y
⊢ ‖(1 / 2) • x + (1 / 2) • y‖ ≠ 1

Tactic:
rw [← smul_add, norm_smul, Real.norm_of_nonneg one_half_pos.le, one_div, ← div_eq_inv_mul, Ne,
  div_eq_one_iff_eq (two_ne_zero' ℝ)]

Result:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hne : x ≠ y
⊢ ¬‖x + y‖ = 2
-- Mathlib/Order/Filter/Prod.lean
theorem mem_coprod_iff {s : Set (α × β)} {f : Filter α} {g : Filter β} :
    s ∈ f.coprod g ↔ (∃ t₁ ∈ f, Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂ ∈ g, Prod.snd ⁻¹' t₂ ⊆ s

Proof state:
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f.coprod g ↔ (∃ t₁ ∈ f, Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂ ∈ g, Prod.snd ⁻¹' t₂ ⊆ s

Tactic:
simp [Filter.coprod]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
@[simp] lemma equicontinuousWithinAt_univ (F : ι → X → α) (x₀ : X) :
    EquicontinuousWithinAt F univ x₀ ↔ EquicontinuousAt F x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousWithinAt F univ x₀ ↔ EquicontinuousAt F x₀

Tactic:
rw [EquicontinuousWithinAt, EquicontinuousAt, nhdsWithin_univ]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem smul_sphere' {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) :
    c • sphere x r = sphere (c • x) (‖c‖ * r)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ y ∈ c • sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ hc]

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)

Tactic:
conv_lhs => rw [← inv_smul_smul₀ hc x]

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ sphere (c⁻¹ • c • x) r ↔ y ∈ sphere (c • x) (‖c‖ * r)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ sphere (c⁻¹ • c • x) r ↔ y ∈ sphere (c • x) (‖c‖ * r)

Tactic:
simp only [mem_sphere, dist_smul₀, norm_inv, ← div_eq_inv_mul, div_eq_iff (norm_pos_iff.2 hc).ne',
  mul_comm r]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Tactic:
ext y

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ y ∈ c • sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.iff_congr_right {P Q R : Prop} [Decidable P] [Decidable Q] [Decidable R] :
    ((P ↔ Q) ↔ (P ↔ R)) ↔ (Q ↔ R) :=
  if h : P then by simp_all [Decidable.not_iff_not] else by simp_all [Decidable.not_iff_not]

Proof state:
P Q R : Prop
inst✝² : Decidable P
inst✝¹ : Decidable Q
inst✝ : Decidable R
h : ¬P
⊢ ((P ↔ Q) ↔ (P ↔ R)) ↔ (Q ↔ R)

Tactic:
simp_all [Decidable.not_iff_not]

Result:
no goals

Proof state:
P Q R : Prop
inst✝² : Decidable P
inst✝¹ : Decidable Q
inst✝ : Decidable R
h : P
⊢ ((P ↔ Q) ↔ (P ↔ R)) ↔ (Q ↔ R)

Tactic:
simp_all [Decidable.not_iff_not]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_mul_laverage [IsFiniteMeasure μ] (f : α → ℝ≥0∞) :
    μ univ * ⨍⁻ x, f x ∂μ = ∫⁻ x, f x ∂μ

Proof state:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ = 0
⊢ μ univ * ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
rw [hμ, lintegral_zero_measure, laverage_zero_measure, mul_zero]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
⊢ μ univ * ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
rcases eq_or_ne μ 0 with hμ | hμ

Result:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ = 0
⊢ μ univ * ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ

case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ ≠ 0
⊢ μ univ * ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ

Proof state:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ ≠ 0
⊢ μ univ * ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
rw [laverage_eq, ENNReal.mul_div_cancel (measure_univ_ne_zero.2 hμ) (measure_ne_top _ _)]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma nonsingular_neg {P : Fin 3 → F} (hP : W.Nonsingular P) : W.Nonsingular <| W.neg P

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
⊢ W.Nonsingular (W.neg P)

Tactic:
by_cases hPz : P z = 0

Result:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.Nonsingular (W.neg P)

case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ W.Nonsingular (W.neg P)

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ W.Nonsingular (W.neg P)

Tactic:
simp only [neg_of_Z_ne_zero hPz, nonsingular_smul _ <| Ne.isUnit hPz,
  nonsingular_neg_of_Z_ne_zero hP hPz]

Result:
no goals

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.Nonsingular (W.neg P)

Tactic:
simp only [neg_of_Z_eq_zero hP hPz, nonsingular_smul _
    ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg, nonsingular_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_foldlM_loop
    (f : γ → β → α → m β) (xs : Array α) (stop : Nat) (h : stop ≤ xs.size) (i j : Nat) (b : β)
    (hmono : monotone f) : monotone (fun x => Array.foldlM.loop (f x) xs stop h i j b)

Proof state:
case case2.hmono₂
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → β → α → m β
xs : Array α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ monotone fun x __do_lift => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift

Tactic:
apply monotone_of_monotone_apply

Result:
case case2.hmono₂.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → β → α → m β
xs : Array α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ ∀ (y : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) y

Proof state:
case case2.hmono₁.h.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → β → α → m β
xs : Array α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ monotone f

Tactic:
apply hmono

Result:
no goals

Proof state:
case case2.hmono₁
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → β → α → m β
xs : Array α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ monotone fun x => f x b✝ xs[j✝]

Tactic:
apply monotone_apply

Result:
case case2.hmono₁.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → β → α → m β
xs : Array α
stop : Nat
h : stop ≤ xs.size
hmono : monotone f
j✝ : Nat
b✝ : β
h✝ : j✝ < stop
i'✝ : Nat
this✝ : j✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.foldlM.loop (f x) xs stop h i'✝ (j✝ + 1) __do_lift
⊢ monotone fun x => f x b✝
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
/-- The **Four Functions Theorem**, aka **Ahlswede-Daykin Inequality**. -/
lemma four_functions_theorem [DecidableEq α] (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
    (h : ∀ a b, f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)) (s t : Finset α) :
    (∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a

Proof state:
case intro.intro.intro.intro.refine_1.inr
α : Type u_1
β✝ : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s✝ t✝ : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s✝ ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
t' : Finset ↥L
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
s' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
s t : Finset β
hs : ¬∃ a, g a = s
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 s * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (s ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (s ∪ t)

Tactic:
simpa [extend_apply' _ _ _ hs] using mul_nonneg
  (extend_nonneg (fun a : L ↦ h₃ a) le_rfl _) (extend_nonneg (fun a : L ↦ h₄ a) le_rfl _)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Gamma.lean
theorem Complex.integral_exp_neg_rpow {p : ℝ} (hp : 1 ≤ p) :
    ∫ x : ℂ, rexp (- ‖x‖ ^ p) = π * Real.Gamma (2 / p + 1)

Proof state:
p : ℝ
hp : 1 ≤ p
⊢ -2 < 0

Tactic:
linarith

Result:
no goals

Proof state:
case h.e'_3
p : ℝ
hp : 1 ≤ p
⊢ π * Real.Gamma (2 / p + 1) = 2 * π / p * Real.Gamma ((0 + 2) / p)

Tactic:
rw [zero_add, Real.Gamma_add_one (div_ne_zero two_ne_zero (by linarith))]

Result:
case h.e'_3
p : ℝ
hp : 1 ≤ p
⊢ π * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * Real.Gamma (2 / p)

Proof state:
p : ℝ
hp : 1 ≤ p
⊢ ∫ (x : ℂ), rexp (-‖x‖ ^ p) = π * Real.Gamma (2 / p + 1)

Tactic:
convert (integral_rpow_mul_exp_neg_rpow hp (by linarith : (-2 : ℝ) < 0)) using 1

Result:
case h.e'_2
p : ℝ
hp : 1 ≤ p
⊢ ∫ (x : ℂ), rexp (-‖x‖ ^ p) = ∫ (x : ℂ), ‖x‖ ^ 0 * rexp (-‖x‖ ^ p)

case h.e'_3
p : ℝ
hp : 1 ≤ p
⊢ π * Real.Gamma (2 / p + 1) = 2 * π / p * Real.Gamma ((0 + 2) / p)

Proof state:
case h.e'_2
p : ℝ
hp : 1 ≤ p
⊢ ∫ (x : ℂ), rexp (-‖x‖ ^ p) = ∫ (x : ℂ), ‖x‖ ^ 0 * rexp (-‖x‖ ^ p)

Tactic:
simp_rw [rpow_zero, one_mul]

Result:
no goals

Proof state:
case h.e'_3
p : ℝ
hp : 1 ≤ p
⊢ π * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * Real.Gamma (2 / p)

Tactic:
ring

Result:
no goals

Proof state:
p : ℝ
hp : 1 ≤ p
⊢ p ≠ 0

Tactic:
linarith

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem fix_fwd {f : α →. β ⊕ α} {b : β} {a a' : α} (hb : b ∈ f.fix a) (ha' : Sum.inr a' ∈ f a) :
    b ∈ f.fix a'

Proof state:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
b : β
a a' : α
hb : b ∈ f.fix a
ha' : Sum.inr a' ∈ f a
⊢ b ∈ f.fix a'

Tactic:
rwa [← fix_fwd_eq ha']

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem card_filter_mk_eq [NumberField K] (w : InfinitePlace K) : #{φ | mk φ = w} = mult w

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ #(Finset.filter (fun x => x = w.embedding ∨ x = star w.embedding) Finset.univ) = w.mult

Tactic:
simp_rw [Finset.filter_or, Finset.filter_eq' _ (embedding w),
  Finset.filter_eq' _ (ComplexEmbedding.conjugate (embedding w)),
  Finset.mem_univ, ite_true, mult]

Result:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ #({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = if w.IsReal then 1 else 2

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ #({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = if w.IsReal then 1 else 2

Tactic:
split_ifs with hw

Result:
case pos
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ #({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 1

case neg
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ #({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 2

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ #(Finset.filter (fun φ => mk φ = w) Finset.univ) = w.mult

Tactic:
conv_lhs =>
  congr; congr; ext
  rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]

Result:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ #(Finset.filter (fun x => x = w.embedding ∨ x = star w.embedding) Finset.univ) = w.mult

Proof state:
case pos
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ #({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 1

Tactic:
rw [ComplexEmbedding.isReal_iff.mp (isReal_iff.mp hw), Finset.union_idempotent,
  Finset.card_singleton]

Result:
no goals

Proof state:
case neg
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ w.embedding ≠ ComplexEmbedding.conjugate w.embedding

Tactic:
rwa [Ne, eq_comm, ← ComplexEmbedding.isReal_iff, ← isReal_iff]

Result:
no goals

Proof state:
case neg
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ #({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 2

Tactic:
refine Finset.card_pair ?_

Result:
case neg
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ w.embedding ≠ ComplexEmbedding.conjugate w.embedding
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem eqOn_of_preconnected_of_frequently_eq (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U)
    (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : EqOn f g U

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
⊢ EqOn f g U

Tactic:
have hfg' : ∃ᶠ z in 𝓝[≠] z₀, (f - g) z = 0 :=
  hfg.mono fun z h => by rw [Pi.sub_apply, h, sub_self]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
hfg' : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, (f - g) z = 0
⊢ EqOn f g U

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
hfg' : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, (f - g) z = 0
⊢ EqOn f g U

Tactic:
simpa [sub_eq_zero] using fun z hz =>
  (hf.sub hg).eqOn_zero_of_preconnected_of_frequently_eq_zero hU h₀ hfg' hz

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
z : 𝕜
h : f z = g z
⊢ (f - g) z = 0

Tactic:
rw [Pi.sub_apply, h, sub_self]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_neg (a : PadicSeq p) : (-a).norm = a.norm :=
  norm_eq <| by simp

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
⊢ ∀ (k : ℕ), padicNorm p (↑(-a) k) = padicNorm p (↑a k)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem mulExpNegMulSq_one_le_one (x : ℝ) : mulExpNegMulSq 1 x ≤ 1

Proof state:
x : ℝ
⊢ x ≤ x * x + 1

Tactic:
nlinarith

Result:
no goals

Proof state:
x : ℝ
⊢ x ≤ rexp (x * x)

Tactic:
apply le_trans _ (add_one_le_exp (x * x))

Result:
x : ℝ
⊢ x ≤ x * x + 1

Proof state:
x : ℝ
⊢ x * rexp (-(x * x)) ≤ 1

Tactic:
rw [← le_div_iff₀ (exp_pos (-(x * x))), exp_neg, div_inv_eq_mul, one_mul]

Result:
x : ℝ
⊢ x ≤ rexp (x * x)

Proof state:
x : ℝ
⊢ mulExpNegMulSq 1 x ≤ 1

Tactic:
simp [mulExpNegMulSq]

Result:
x : ℝ
⊢ x * rexp (-(x * x)) ≤ 1
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upcrossingsBefore_eq_sum (hab : a < b) : upcrossingsBefore a b f N ω =
    ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1
k : ℕ
hk : k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)
⊢ {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 0

Tactic:
rw [Finset.mem_Ico, Nat.succ_le_iff] at hk

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
⊢ {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 0

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
⊢ {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 0

Tactic:
rw [Set.indicator_of_not_mem]

Result:
case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
⊢ k ∉ {n | upperCrossingTime a b f N n ω < N}