harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_left_comm {γ : Type*} {u : Finset γ} {f : α → δ → ε} {g : β → γ → δ}
    {f' : α → γ → δ'} {g' : β → δ' → ε} (h_left_comm : ∀ a b c, f a (g b c) = g' b (f' a c)) :
    image₂ f s (image₂ g t u) = image₂ g' t (image₂ f' s u) :=
  coe_injective <| by
    push_cast
    exact image2_left_comm h_left_comm

Proof state:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 f (↑s) (image2 g ↑t ↑u) = image2 g' (↑t) (image2 f' ↑s ↑u)

Tactic:
exact image2_left_comm h_left_comm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ ↑(image₂ f s (image₂ g t u)) = ↑(image₂ g' t (image₂ f' s u))

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 f (↑s) (image2 g ↑t ↑u) = image2 g' (↑t) (image2 f' ↑s ↑u)
-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem map_wittPolynomial (f : R →+* S) (n : ℕ) : map f (W n) = W n

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ (map f) ((monomial (single i (p ^ (n - i)))) (↑p ^ i)) = (monomial (single i (p ^ (n - i)))) (↑p ^ i)

Tactic:
rw [map_monomial, RingHom.map_pow, map_natCast]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ (map f) (W_ R n) = W_ S n

Tactic:
rw [wittPolynomial, map_sum, wittPolynomial]

Result:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ ∑ x ∈ range (n + 1), (map f) ((monomial (single x (p ^ (n - x)))) (↑p ^ x)) =
    ∑ i ∈ range (n + 1), (monomial (single i (p ^ (n - i)))) (↑p ^ i)

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ ∑ x ∈ range (n + 1), (map f) ((monomial (single x (p ^ (n - x)))) (↑p ^ x)) =
    ∑ i ∈ range (n + 1), (monomial (single i (p ^ (n - i)))) (↑p ^ i)

Tactic:
refine sum_congr rfl fun i _ => ?_

Result:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ (map f) ((monomial (single i (p ^ (n - i)))) (↑p ^ i)) = (monomial (single i (p ^ (n - i)))) (↑p ^ i)
-- Mathlib/CategoryTheory/Presentable/Basic.lean
lemma isCardinalPresentable_of_equivalence
    {C' : Type u₃} [Category.{v₃} C'] [IsCardinalPresentable X κ] (e : C ≌ C') :
    IsCardinalPresentable (e.functor.obj X) κ

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)))

Tactic:
suffices PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁}) from
  ⟨fun {c} hc ↦ ⟨isColimitOfReflects uliftFunctor.{v₁}
      (isColimitOfPreserves (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁}) hc)⟩⟩

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})

Proof state:
case h.up
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
X✝ Y✝ : C'
f : X✝ ⟶ Y✝
g : (coyoneda.obj (op (e.functor.obj X))).obj X✝
⊢ ((coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
        ((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) Y✝).hom)
      { down := g } =
    (((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) X✝).hom ≫
        (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f)
      { down := g }

Tactic:
apply Equiv.ulift.injective

Result:
case h.up.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
X✝ Y✝ : C'
f : X✝ ⟶ Y✝
g : (coyoneda.obj (op (e.functor.obj X))).obj X✝
⊢ Equiv.ulift
      (((coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
          ((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) Y✝).hom)
        { down := g }) =
    Equiv.ulift
      ((((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) X✝).hom ≫
          (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f)
        { down := g })
-- Mathlib/Combinatorics/SetFamily/KruskalKatona.lean
theorem kruskal_katona_lovasz_form (hir : i ≤ r) (hrk : r ≤ k) (hkn : k ≤ n)
    (h₁ : (𝒜 : Set (Finset (Fin n))).Sized r) (h₂ : k.choose r ≤ #𝒜) :
    k.choose (r - i) ≤ #(∂^[i] 𝒜)

Proof state:
case h.e'_2.h.mpr.intro.intro.intro
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ B ⊆ range'k ∧ #B = r - i

Tactic:
refine ⟨hBA.trans Ah.1, eq_tsub_of_add_eq ?_⟩

Result:
case h.e'_2.h.mpr.intro.intro.intro
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ #B + i = r

Proof state:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
⊢ #(powersetCard (r - i) range'k) = #(∂ ^[i] 𝒞)

Tactic:
congr!

Result:
case h.e'_2
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
⊢ powersetCard (r - i) range'k = ∂ ^[i] 𝒞
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₆_of_isCharTwoJNeZeroNF : W.b₆ = 4 * W.a₆

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 0 ^ 2 + 4 * W.a₆ = 4 * W.a₆

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₆ = 4 * W.a₆

Tactic:
rw [b₆, a₃_of_isCharTwoJNeZeroNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 0 ^ 2 + 4 * W.a₆ = 4 * W.a₆
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_congr_measure_of_integrable {μ' : Measure α} (c' : ℝ≥0∞) (hc' : c' ≠ ∞)
    (hμ'_le : μ' ≤ c' • μ) (hT : DominatedFinMeasAdditive μ T C)
    (hT' : DominatedFinMeasAdditive μ' T C') (f : α → E) (hfμ : Integrable f μ) :
    setToFun μ T hT f = setToFun μ' T hT' f

Proof state:
case h_ind
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ setToFun μ T hT (s.indicator fun x => c) = setToFun μ' T hT' (s.indicator fun x => c)

Tactic:
have hμ's : μ' s ≠ ∞ := by
  refine ((hμ'_le s).trans_lt ?_).ne
  rw [Measure.smul_apply, smul_eq_mul]
  exact ENNReal.mul_lt_top hc'.lt_top hμs

Result:
case h_ind
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
hμ's : μ' s ≠ ⊤
⊢ setToFun μ T hT (s.indicator fun x => c) = setToFun μ' T hT' (s.indicator fun x => c)
-- Mathlib/RingTheory/Presentation.lean
private lemma aux_surjective : Function.Surjective (Q.aux P) := fun p ↦ by
  induction' p using MvPolynomial.induction_on with a p q hp hq p i h
  · use rename Sum.inr <| P.σ a
    simp only [aux, aeval_rename, Sum.elim_comp_inr]
    have (p : MvPolynomial P.vars R) :
        aeval (C ∘ P.val) p = (C (aeval P.val p) : MvPolynomial Q.vars S)

Proof state:
case h_X.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
i : Q.vars
a : MvPolynomial (Q.vars ⊕ P.vars) R
⊢ ∃ a_1, (Algebra.Presentation.aux Q P) a_1 = (Algebra.Presentation.aux Q P) a * X i

Tactic:
exact ⟨(a * X (Sum.inl i)), by simp⟩

Result:
no goals

Proof state:
case h_add.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
q : MvPolynomial Q.vars S
hq : ∃ a, (Algebra.Presentation.aux Q P) a = q
a : MvPolynomial (Q.vars ⊕ P.vars) R
⊢ ∃ a_1, (Algebra.Presentation.aux Q P) a_1 = (Algebra.Presentation.aux Q P) a + q

Tactic:
obtain ⟨b, rfl⟩ := hq

Result:
case h_add.intro.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
a b : MvPolynomial (Q.vars ⊕ P.vars) R
⊢ ∃ a_1, (Algebra.Presentation.aux Q P) a_1 = (Algebra.Presentation.aux Q P) a + (Algebra.Presentation.aux Q P) b
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem le_hasProd (hf : HasProd f a) (i : ι) (hb : ∀ j, j ≠ i → 1 ≤ f j) : f i ≤ a :=
  calc
    f i = ∏ i ∈ {i}, f i

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
hf : HasProd f a
i : ι
hb : ∀ (j : ι), j ≠ i → 1 ≤ f j
⊢ ∀ i_1 ∉ {i}, 1 ≤ f i_1

Tactic:
simpa

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
hf : HasProd f a
i : ι
hb : ∀ (j : ι), j ≠ i → 1 ≤ f j
⊢ f i = ∏ i ∈ {i}, f i

Tactic:
rw [prod_singleton]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
/-- Give a bound on `‖(1 + t * z)⁻¹‖` for `0 ≤ t ≤ 1` and `‖z‖ < 1`. -/
lemma norm_one_add_mul_inv_le {t : ℝ} (ht : t ∈ Set.Icc 0 1) {z : ℂ} (hz : ‖z‖ < 1) :
    ‖(1 + t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹

Proof state:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖z‖ ≤ ‖1 + ↑t * z‖

Tactic:
calc 1 - ‖z‖
  _ ≤ 1 - t * ‖z‖ := by
    nlinarith [norm_nonneg z]
  _ = 1 - ‖t * z‖ := by
    rw [norm_mul, Complex.norm_of_nonneg ht.1]
  _ ≤ ‖1 + t * z‖ := by
    rw [← norm_neg (t * z), ← sub_neg_eq_add]
    convert norm_sub_norm_le 1 (-(t * z))
    exact norm_one.symm

Result:
no goals

Proof state:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖↑t * z‖ ≤ ‖1 + ↑t * z‖

Tactic:
rw [← norm_neg (t * z), ← sub_neg_eq_add]

Result:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖-(↑t * z)‖ ≤ ‖1 - -(↑t * z)‖

Proof state:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖z‖ ≤ 1 - t * ‖z‖

Tactic:
nlinarith [norm_nonneg z]

Result:
no goals

Proof state:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ ‖(1 + ↑t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹

Tactic:
rw [norm_inv]

Result:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ ‖1 + ↑t * z‖⁻¹ ≤ (1 - ‖z‖)⁻¹

Proof state:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖-(↑t * z)‖ ≤ ‖1 - -(↑t * z)‖

Tactic:
convert norm_sub_norm_le 1 (-(t * z))

Result:
case h.e'_3.h.e'_5
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 = ‖1‖

Proof state:
t : ℝ
ht : t ∈ Set.Icc 0 1
z : ℂ
hz : ‖z‖ < 1
⊢ ‖(1 + ↑t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹

Tactic:
rw [Set.mem_Icc] at ht

Result:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ ‖(1 + ↑t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹

Proof state:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - t * ‖z‖ = 1 - ‖↑t * z‖

Tactic:
rw [norm_mul, Complex.norm_of_nonneg ht.1]

Result:
no goals

Proof state:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 0 < 1 - ‖z‖

Tactic:
linarith

Result:
no goals

Proof state:
case h.e'_3.h.e'_5
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 = ‖1‖

Tactic:
exact norm_one.symm

Result:
no goals

Proof state:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ ‖1 + ↑t * z‖⁻¹ ≤ (1 - ‖z‖)⁻¹

Tactic:
refine inv_anti₀ (by linarith) ?_

Result:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖z‖ ≤ ‖1 + ↑t * z‖
-- Mathlib/Order/CompleteLattice.lean
lemma sSup_eq_bot' {s : Set α} : sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥}

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥}

Tactic:
rw [sSup_eq_bot, ← subset_singleton_iff_eq, subset_singleton_iff]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Basic.lean
theorem totalSpaceMk_isClosedEmbedding [T1Space B] (x : B) :
    IsClosedEmbedding (@TotalSpace.mk B F E x) :=
  ⟨totalSpaceMk_isEmbedding F E x, by
    rw [TotalSpace.range_mk]
    exact isClosed_singleton.preimage <| continuous_proj F E⟩

Proof state:
B : Type u_2
F : Type u_3
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
E : B → Type u_5
inst✝³ : TopologicalSpace (TotalSpace F E)
inst✝² : (b : B) → TopologicalSpace (E b)
inst✝¹ : FiberBundle F E
inst✝ : T1Space B
x : B
⊢ IsClosed (TotalSpace.proj ⁻¹' {x})

Tactic:
exact isClosed_singleton.preimage <| continuous_proj F E

Result:
no goals

Proof state:
B : Type u_2
F : Type u_3
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
E : B → Type u_5
inst✝³ : TopologicalSpace (TotalSpace F E)
inst✝² : (b : B) → TopologicalSpace (E b)
inst✝¹ : FiberBundle F E
inst✝ : T1Space B
x : B
⊢ IsClosed (range (TotalSpace.mk x))

Tactic:
rw [TotalSpace.range_mk]

Result:
B : Type u_2
F : Type u_3
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
E : B → Type u_5
inst✝³ : TopologicalSpace (TotalSpace F E)
inst✝² : (b : B) → TopologicalSpace (E b)
inst✝¹ : FiberBundle F E
inst✝ : T1Space B
x : B
⊢ IsClosed (TotalSpace.proj ⁻¹' {x})
-- Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean
theorem exists_lt_lowerSemicontinuous_integral_gt_nnreal [SigmaFinite μ] (f : α → ℝ≥0)
    (fint : Integrable (fun x => (f x : ℝ)) μ) {ε : ℝ} (εpos : 0 < ε) :
    ∃ g : α → ℝ≥0∞,
      (∀ x, (f x : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
      (∀ᵐ x ∂μ, g x < ⊤) ∧
      Integrable (fun x => (g x).toReal) μ ∧ (∫ x, (g x).toReal ∂μ) < (∫ x, ↑(f x) ∂μ) + ε

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (fun x => ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ ≠ ⊤

Tactic:
simpa using int_f_ne_top

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (fun x => ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (a : α), ↑(f a) ∂μ + ↑δ).toReal = (∫⁻ (a : α), ↑(f a) ∂μ).toReal + ↑δ

Tactic:
rw [ENNReal.toReal_add int_f_ne_top ENNReal.coe_ne_top, ENNReal.coe_toReal]

Result:
no goals

Proof state:
case h.e'_5.h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (fun x => ↑(f x)) μ
ε : ℝ
εpos : 0 < ε
x✝ : α
⊢ f x✝ = (↑(f x✝)).toNNReal

Tactic:
simp only [Real.toNNReal_coe]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.refine_2.hfm
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (fun x => ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ⊤
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ⊤
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ AEStronglyMeasurable (fun x => (g x).toReal) μ

Tactic:
apply gcont.measurable.ennreal_toReal.aemeasurable.aestronglyMeasurable

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem eq_one_of_prod_eq_one {s : Finset α} {f : α → β} {a : α} (hp : ∏ x ∈ s, f x = 1)
    (h1 : ∀ x ∈ s, x ≠ a → f x = 1) : ∀ x ∈ s, f x = 1

Proof state:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : f a = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : α
hx : a ∈ s
h : x = a
⊢ f a = 1

Tactic:
exact hp

Result:
no goals

Proof state:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : α
hx : a ∈ s
h : x = a
⊢ f a = 1

Tactic:
rw [← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (not_mem_singleton.1 ha),
  prod_singleton] at hp

Result:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : f a = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : α
hx : a ∈ s
h : x = a
⊢ f a = 1

Proof state:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : α
hx : x ∈ s
h : x = a
⊢ f a = 1

Tactic:
rw [h] at hx

Result:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : α
hx : a ∈ s
h : x = a
⊢ f a = 1

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : α
hx : x ∈ s
h : ¬x = a
⊢ f x = 1

Tactic:
exact h1 x hx h

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
⊢ ∀ x ∈ s, f x = 1

Tactic:
intro x hx

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : α
hx : x ∈ s
⊢ f x = 1

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : α
hx : x ∈ s
⊢ f x = 1

Tactic:
by_cases h : x = a

Result:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : α
hx : x ∈ s
h : x = a
⊢ f x = 1

case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : α
hx : x ∈ s
h : ¬x = a
⊢ f x = 1

Proof state:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : α
hx : x ∈ s
h : x = a
⊢ f x = 1

Tactic:
rw [h]

Result:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : α
hx : x ∈ s
h : x = a
⊢ f a = 1
-- Mathlib/Analysis/Convex/Strong.lean
lemma UniformConcaveOn.neg (hf : UniformConcaveOn s φ f) : UniformConvexOn s φ (-f)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
⊢ UniformConvexOn s φ (-f)

Tactic:
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ le_of_neg_le_neg ?_⟩

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ -(a • (-f) x + b • (-f) y - a * b * φ ‖x - y‖) ≤ -(-f) (a • x + b • y)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ -(a • (-f) x + b • (-f) y - a * b * φ ‖x - y‖) ≤ -(-f) (a • x + b • y)

Tactic:
simpa [add_comm, -neg_le_neg_iff, ← le_sub_iff_add_le', sub_eq_add_neg, neg_add]
  using hf.2 hx hy ha hb hab

Result:
no goals