harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem mapPiLocalization_naturality :
    (mapPiLocalization f).comp (toPiLocalization R) = (toPiLocalization S).comp f

Proof state:
case a.h
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
⊢ (Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f ⋯)
      ((algebraMap R (Localization.AtPrime (Ideal.comap f I.asIdeal))) r) =
    (algebraMap S (Localization.AtPrime I.asIdeal)) (f r)

Tactic:
simp_rw [← IsLocalization.mk'_one (M := (I.1.comap f).primeCompl), Localization.localRingHom_mk',
  ← IsLocalization.mk'_one (M := I.1.primeCompl), Submonoid.coe_one, map_one f]

Result:
case a.h
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
⊢ IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) ⟨1, ⋯⟩ =
    IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) 1

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ (mapPiLocalization f).comp (toPiLocalization R) = (toPiLocalization S).comp f

Tactic:
ext r I

Result:
case a.h
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
⊢ ((mapPiLocalization f).comp (toPiLocalization R)) r I = ((toPiLocalization S).comp f) r I

Proof state:
case a.h
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
⊢ ((mapPiLocalization f).comp (toPiLocalization R)) r I = ((toPiLocalization S).comp f) r I

Tactic:
show Localization.localRingHom _ _ _ rfl (algebraMap _ _ r) = algebraMap _ _ (f r)

Result:
case a.h
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
⊢ (Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f ⋯)
      ((algebraMap R (Localization.AtPrime (Ideal.comap f I.asIdeal))) r) =
    (algebraMap S (Localization.AtPrime I.asIdeal)) (f r)

Proof state:
case a.h
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
⊢ IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) ⟨1, ⋯⟩ =
    IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) 1

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_singleton (l : List α) : [l].flatten = l

Proof state:
α : Type u_1
l : List α
⊢ [l].flatten = l

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
lemma mul_add_one_le_add_one_pow {a : ℝ} (ha : 0 ≤ a) (b : ℕ) : a * b + 1 ≤ (a + 1) ^ b

Proof state:
case inr
a : ℝ
ha : 0 ≤ a
b : ℕ
ha' : 0 < a
⊢ a * ↑b + 1 ≤ (a + 1) ^ b

Tactic:
clear ha

Result:
case inr
a : ℝ
b : ℕ
ha' : 0 < a
⊢ a * ↑b + 1 ≤ (a + 1) ^ b

Proof state:
case h₂
b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ a * ↑b + 1 ≤ (a + 1) ^ b

Tactic:
exact hb ha'

Result:
no goals

Proof state:
case h₁.h.ha
b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ 0 ≤ 0 + 1

Tactic:
norm_num

Result:
no goals

Proof state:
a : ℝ
ha : 0 ≤ a
b : ℕ
⊢ a * ↑b + 1 ≤ (a + 1) ^ b

Tactic:
rcases ha.eq_or_lt with rfl|ha'

Result:
case inl
b : ℕ
ha : 0 ≤ 0
⊢ 0 * ↑b + 1 ≤ (0 + 1) ^ b

case inr
a : ℝ
ha : 0 ≤ a
b : ℕ
ha' : 0 < a
⊢ a * ↑b + 1 ≤ (a + 1) ^ b

Proof state:
b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ a * ↑(b + 1) + 1 = (0 + 1) ^ b * a + (a * ↑b + 1)

Tactic:
simp [mul_add, add_assoc, add_left_comm]

Result:
no goals

Proof state:
b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ (a + 1) ^ b * a + (a + 1) ^ b = (a + 1) ^ (b + 1)

Tactic:
simp [pow_succ, mul_add]

Result:
no goals

Proof state:
case inl
b : ℕ
ha : 0 ≤ 0
⊢ 0 * ↑b + 1 ≤ (0 + 1) ^ b

Tactic:
simp

Result:
no goals

Proof state:
case inr.zero
a : ℝ
ha' : 0 < a
⊢ a * ↑0 + 1 ≤ (a + 1) ^ 0

Tactic:
simp

Result:
no goals

Proof state:
b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ (0 + 1) ^ b * a + (a * ↑b + 1) ≤ (a + 1) ^ b * a + (a + 1) ^ b

Tactic:
gcongr

Result:
case h₁.h.ha
b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ 0 ≤ 0 + 1

case h₂
b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ a * ↑b + 1 ≤ (a + 1) ^ b
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem integral_smul {𝕜 : Type*} [RCLike 𝕜] [NormedSpace 𝕜 E] [SMulCommClass 𝕜 ℂ E] (a : 𝕜)
    (f : ℂ → E) (c : ℂ) (R : ℝ) : (∮ z in C(c, R), a • f z) = a • ∮ z in C(c, R), f z

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass 𝕜 ℂ E
a : 𝕜
f : ℂ → E
c : ℂ
R : ℝ
⊢ (∮ (z : ℂ) in C(c, R), a • f z) = a • ∮ (z : ℂ) in C(c, R), f z

Tactic:
simp only [circleIntegral, ← smul_comm a (_ : ℂ) (_ : E), intervalIntegral.integral_smul]

Result:
no goals
-- Mathlib/Data/List/Scan.lean
theorem getElem_scanl_zero {h : 0 < (scanl f b l).length} : (scanl f b l)[0] = b

Proof state:
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : List α
h : 0 < (scanl f b l).length
⊢ (scanl f b l)[0] = b

Tactic:
cases l

Result:
case nil
α : Type u_1
β : Type u_2
f : β → α → β
b : β
h : 0 < (scanl f b []).length
⊢ (scanl f b [])[0] = b

case cons
α : Type u_1
β : Type u_2
f : β → α → β
b : β
head✝ : α
tail✝ : List α
h : 0 < (scanl f b (head✝ :: tail✝)).length
⊢ (scanl f b (head✝ :: tail✝))[0] = b

Proof state:
case cons
α : Type u_1
β : Type u_2
f : β → α → β
b : β
head✝ : α
tail✝ : List α
h : 0 < (scanl f b (head✝ :: tail✝)).length
⊢ (scanl f b (head✝ :: tail✝))[0] = b

Tactic:
simp [scanl_cons, singleton_append]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : β → α → β
b : β
h : 0 < (scanl f b []).length
⊢ (scanl f b [])[0] = b

Tactic:
simp [scanl_nil]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem isSimpleGroup_of_prime_card {p : ℕ} [hp : Fact p.Prime]
    (h : Nat.card α = p) : IsSimpleGroup α

Proof state:
α : Type u_1
inst✝ : Group α
hp : Fact (Nat.Prime (Nat.card α))
⊢ IsSimpleGroup α

Tactic:
have : Finite α := Nat.finite_of_card_ne_zero hp.1.ne_zero

Result:
α : Type u_1
inst✝ : Group α
hp : Fact (Nat.Prime (Nat.card α))
this : Finite α
⊢ IsSimpleGroup α

Proof state:
α : Type u_1
inst✝ : Group α
hp : Fact (Nat.Prime (Nat.card α))
this : Finite α
⊢ IsSimpleGroup α

Tactic:
have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp hp.1.one_lt

Result:
α : Type u_1
inst✝ : Group α
hp : Fact (Nat.Prime (Nat.card α))
this✝ : Finite α
this : Nontrivial α
⊢ IsSimpleGroup α

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
⊢ IsSimpleGroup α

Tactic:
subst h

Result:
α : Type u_1
inst✝ : Group α
hp : Fact (Nat.Prime (Nat.card α))
⊢ IsSimpleGroup α

Proof state:
α : Type u_1
inst✝ : Group α
hp : Fact (Nat.Prime (Nat.card α))
this✝ : Finite α
this : Nontrivial α
⊢ IsSimpleGroup α

Tactic:
exact ⟨fun H _ => H.eq_bot_or_eq_top_of_prime_card⟩

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_inter_mulSupport_eq (f : α → M) (s t : Set α)
    (h : s ∩ mulSupport f = t ∩ mulSupport f) : ∏ᶠ i ∈ s, f i = ∏ᶠ i ∈ t, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : s ∩ mulSupport f = t ∩ mulSupport f
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
rw [← finprod_mem_inter_mulSupport, h, finprod_mem_inter_mulSupport]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem enumFrom_append (xs ys : List α) (n : Nat) :
    enumFrom n (xs ++ ys) = enumFrom n xs ++ enumFrom (n + xs.length) ys

Proof state:
case nil
α : Type u_1
ys : List α
n : Nat
⊢ enumFrom n ([] ++ ys) = enumFrom n [] ++ enumFrom (n + [].length) ys

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
x : α
xs : List α
IH : ∀ (ys : List α) (n : Nat), enumFrom n (xs ++ ys) = enumFrom n xs ++ enumFrom (n + xs.length) ys
ys : List α
n : Nat
⊢ enumFrom n (x :: xs ++ ys) = enumFrom n (x :: xs) ++ enumFrom (n + (x :: xs).length) ys

Tactic:
rw [cons_append, enumFrom_cons, IH, ← cons_append, ← enumFrom_cons, length, Nat.add_right_comm,
  Nat.add_assoc]

Result:
no goals

Proof state:
α : Type u_1
xs ys : List α
n : Nat
⊢ enumFrom n (xs ++ ys) = enumFrom n xs ++ enumFrom (n + xs.length) ys

Tactic:
induction xs generalizing ys n with
| nil => simp
| cons x xs IH =>
  rw [cons_append, enumFrom_cons, IH, ← cons_append, ← enumFrom_cons, length, Nat.add_right_comm,
    Nat.add_assoc]

Result:
no goals
-- Mathlib/RingTheory/Fintype.lean
lemma Finset.univ_of_card_le_two (h : Fintype.card R ≤ 2) :
    (univ : Finset R) = {0, 1}

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 2
h✝ : Subsingleton R
a : R
x✝ : a ∈ univ
⊢ a ∈ {0, 1}

Tactic:
simp [Subsingleton.elim a 0]

Result:
no goals

Proof state:
case h.e'_4
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 2
h✝ : Nontrivial R
⊢ #{0, 1} = 2

Tactic:
simp

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 2
h✝ : Nontrivial R
⊢ #univ ≤ #{0, 1}

Tactic:
convert h

Result:
case h.e'_4
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 2
h✝ : Nontrivial R
⊢ #{0, 1} = 2

Proof state:
case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 2
h✝ : Subsingleton R
⊢ univ = {0, 1}

Tactic:
exact le_antisymm (fun a _ ↦ by simp [Subsingleton.elim a 0]) (Finset.subset_univ _)

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 2
h✝ : Nontrivial R
⊢ univ = {0, 1}

Tactic:
refine (eq_of_subset_of_card_le (subset_univ _) ?_).symm

Result:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 2
h✝ : Nontrivial R
⊢ #univ ≤ #{0, 1}

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 2
⊢ univ = {0, 1}

Tactic:
rcases subsingleton_or_nontrivial R

Result:
case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 2
h✝ : Subsingleton R
⊢ univ = {0, 1}

case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 2
h✝ : Nontrivial R
⊢ univ = {0, 1}
-- Mathlib/Algebra/ModEq.lean
theorem sub_modEq_zero : a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b : α
⊢ a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p]

Tactic:
simp [sub_modEq_iff_modEq_add]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem coord_apply_centroid [CharZero k] (b : AffineBasis ι k P) {s : Finset ι} {i : ι}
    (hi : i ∈ s) : b.coord i (s.centroid k b) = (s.card : k)⁻¹

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : DivisionRing k
inst✝¹ : Module k V
inst✝ : CharZero k
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
⊢ (b.coord i) (Finset.centroid k s ⇑b) = (↑s.card)⁻¹

Tactic:
rw [Finset.centroid,
  b.coord_apply_combination_of_mem hi (s.sum_centroidWeights_eq_one_of_nonempty _ ⟨i, hi⟩),
  Finset.centroidWeights, Function.const_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Action/Limits.lean
/-- `F : C ⥤ Action V G` preserves limits of some shape `J`
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
lemma preservesLimitsOfShape_of_preserves (F : C ⥤ Action V G) {J : Type w₁}
    [Category.{w₂} J] (h : PreservesLimitsOfShape J (F ⋙ Action.forget V G)) :
    PreservesLimitsOfShape J F

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesLimitsOfShape J (F ⋙ forget V G)
⊢ PreservesLimitsOfShape J F

Tactic:
constructor

Result:
case preservesLimit
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesLimitsOfShape J (F ⋙ forget V G)
⊢ autoParam (∀ {K : J ⥤ C}, PreservesLimit K F) _auto✝

Proof state:
case preservesLimit
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesLimitsOfShape J (F ⋙ forget V G)
⊢ autoParam (∀ {K : J ⥤ C}, PreservesLimit K F) _auto✝

Tactic:
intro K

Result:
case preservesLimit
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesLimitsOfShape J (F ⋙ forget V G)
K : J ⥤ C
⊢ PreservesLimit K F

Proof state:
case preservesLimit
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesLimitsOfShape J (F ⋙ forget V G)
K : J ⥤ C
⊢ PreservesLimit K F

Tactic:
apply Action.preservesLimit_of_preserves

Result:
case preservesLimit.h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesLimitsOfShape J (F ⋙ forget V G)
K : J ⥤ C
⊢ PreservesLimit K (F ⋙ forget V G)

Proof state:
case preservesLimit.h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
J : Type w₁
inst✝ : Category.{w₂, w₁} J
h : PreservesLimitsOfShape J (F ⋙ forget V G)
K : J ⥤ C
⊢ PreservesLimit K (F ⋙ forget V G)

Tactic:
exact PreservesLimitsOfShape.preservesLimit

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem mk_algebraMap {A : Type*} [CommSemiring A] [Algebra A R] (m : A) :
    mk (algebraMap A R m) 1 = algebraMap A (Localization M) m

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ (algebraMap R (Localization M)) ((algebraMap A R) m) = (algebraMap A (Localization M)) m

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ mk ((algebraMap A R) m) 1 = (algebraMap A (Localization M)) m

Tactic:
rw [mk_eq_mk', mk'_eq_iff_eq_mul, Submonoid.coe_one, map_one, mul_one]

Result:
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ (algebraMap R (Localization M)) ((algebraMap A R) m) = (algebraMap A (Localization M)) m
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_dite (f : ∀ i, p i → α) (g : ∀ i, ¬p i → α) :
    ⨆ i, (if h : p i then f i h else g i h) = (⨆ (i) (h : p i), f i h) ⊔ ⨆ (i) (h : ¬p i),
    g i h

Proof state:
case e_s.h
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
⊢ (if h : p i then f i h else g i h) = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ i, if h : p i then f i h else g i h) = ⨆ x, (⨆ (h : p x), f x h) ⊔ ⨆ (h : ¬p x), g x h

Tactic:
congr 1 with i

Result:
case e_s.h
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
⊢ (if h : p i then f i h else g i h) = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ i, if h : p i then f i h else g i h) = (⨆ i, ⨆ (h : p i), f i h) ⊔ ⨆ i, ⨆ (h : ¬p i), g i h

Tactic:
rw [← iSup_sup_eq]

Result:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ i, if h : p i then f i h else g i h) = ⨆ x, (⨆ (h : p x), f x h) ⊔ ⨆ (h : ¬p x), g x h
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem iUnion_Ioc_zsmul : ⋃ n : ℤ, Ioc (n • p) ((n + 1) • p) = univ

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
⊢ ⋃ n, Ioc (n • p) ((n + 1) • p) = univ

Tactic:
simpa only [zero_add] using iUnion_Ioc_add_zsmul hp 0

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem isLUB_norm [Nonempty α] (f : lp E ∞) : IsLUB (Set.range fun i => ‖f i‖) ‖f‖

Proof state:
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : ↥(lp E ⊤)
⊢ IsLUB (Set.range fun i => ‖↑f i‖) ‖f‖

Tactic:
rw [lp.norm_eq_ciSup]

Result:
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : ↥(lp E ⊤)
⊢ IsLUB (Set.range fun i => ‖↑f i‖) (⨆ i, ‖↑f i‖)

Proof state:
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : ↥(lp E ⊤)
⊢ IsLUB (Set.range fun i => ‖↑f i‖) (⨆ i, ‖↑f i‖)

Tactic:
exact isLUB_ciSup (lp.memℓp f)

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
theorem testBit_eq_inth (n i : ℕ) : n.testBit i = n.bits.getI i

Proof state:
case succ
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ (bit n.bodd n.div2).testBit (i + 1) = n.bits.getI (i + 1)

Tactic:
rw [testBit_bit_succ, ih n.div2, div2_bits_eq_tail]

Result:
case succ
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ n.bits.tail.getI i = n.bits.getI (i + 1)

Proof state:
case succ
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ n.testBit (i + 1) = n.bits.getI (i + 1)

Tactic:
conv_lhs => rw [← bit_decomp n]

Result:
case succ
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ (bit n.bodd n.div2).testBit (i + 1) = n.bits.getI (i + 1)

Proof state:
case succ
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ n.bits.tail.getI i = n.bits.getI (i + 1)

Tactic:
cases n.bits <;> simp

Result:
no goals

Proof state:
case zero
n : ℕ
⊢ n.testBit 0 = n.bits.getI 0

Tactic:
simp only [testBit, zero_eq, shiftRight_zero, one_and_eq_mod_two, mod_two_of_bodd,
  bodd_eq_bits_head, List.getI_zero_eq_headI]

Result:
case zero
n : ℕ
⊢ (n.bits.headI.toNat != 0) = n.bits.headI

Proof state:
case zero
n : ℕ
⊢ (n.bits.headI.toNat != 0) = n.bits.headI

Tactic:
cases List.headI (bits n) <;> rfl

Result:
no goals

Proof state:
n i : ℕ
⊢ n.testBit i = n.bits.getI i

Tactic:
induction' i with i ih generalizing n

Result:
case zero
n : ℕ
⊢ n.testBit 0 = n.bits.getI 0

case succ
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ n.testBit (i + 1) = n.bits.getI (i + 1)
-- Mathlib/MeasureTheory/Integral/Asymptotics.lean
theorem LocallyIntegrable.integrable_of_isBigO_cocompact [IsMeasurablyGenerated (cocompact α)]
    (hf : LocallyIntegrable f μ) (ho : f =O[cocompact α] g)
    (hg : IntegrableAtFilter g (cocompact α) μ) : Integrable f μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : (cocompact α).IsMeasurablyGenerated
hf : LocallyIntegrable f μ
ho : f =O[cocompact α] g
hg : IntegrableAtFilter g (cocompact α) μ
⊢ Integrable f μ

Tactic:
refine integrable_iff_integrableAtFilter_cocompact.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : (cocompact α).IsMeasurablyGenerated
hf : LocallyIntegrable f μ
ho : f =O[cocompact α] g
hg : IntegrableAtFilter g (cocompact α) μ
⊢ StronglyMeasurableAtFilter f (cocompact α) μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : (cocompact α).IsMeasurablyGenerated
hf : LocallyIntegrable f μ
ho : f =O[cocompact α] g
hg : IntegrableAtFilter g (cocompact α) μ
⊢ StronglyMeasurableAtFilter f (cocompact α) μ

Tactic:
exact hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_Iic_of_hasDerivAt_of_tendsto'
    (hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x) (f'int : IntegrableOn f' (Iic a))
    (hf : Tendsto f atBot (𝓝 m)) : ∫ x in Iic a, f' x = f a - m

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
⊢ ContinuousWithinAt f (Iic a) a

Tactic:
exact (hderiv a right_mem_Iic).continuousAt.continuousWithinAt

Result:
no goals

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
⊢ ∫ (x : ℝ) in Iic a, f' x = f a - m

Tactic:
refine integral_Iic_of_hasDerivAt_of_tendsto ?_ (fun x hx => hderiv x hx.out.le)
  f'int hf

Result:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
⊢ ContinuousWithinAt f (Iic a) a
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem weightedSMul_zero_measure {m : MeasurableSpace α} :
    weightedSMul (0 : Measure α) = (0 : Set α → F →L[ℝ] F)

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
x✝ : Set α
⊢ weightedSMul 0 x✝ = 0 x✝

Tactic:
simp [weightedSMul]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
⊢ weightedSMul 0 = 0

Tactic:
ext1

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
x✝ : Set α
⊢ weightedSMul 0 x✝ = 0 x✝
-- Mathlib/Topology/PartialHomeomorph.lean
lemma lift_openEmbedding_apply (e : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) {x : X} :
    (lift_openEmbedding e hf) (f x) = e x

Proof state:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : PartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X
⊢ ↑(e.lift_openEmbedding hf) (f x) = ↑e x

Tactic:
simp_rw [e.lift_openEmbedding_toFun]

Result:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : PartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X
⊢ extend f (↑e) (fun x => Classical.arbitrary Z) (f x) = ↑e x

Proof state:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : PartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X
⊢ extend f (↑e) (fun x => Classical.arbitrary Z) (f x) = ↑e x

Tactic:
apply hf.injective.extend_apply

Result:
no goals