harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Basic.lean
theorem min?_get_le_of_mem {l : List Nat} {a : Nat} (h : a ∈ l) :
    l.min?.get (isSome_min?_of_mem h) ≤ a

Proof state:
case cons.inl.none
a : Nat
t : List Nat
ih : ∀ (h : a ∈ t), t.min?.get ⋯ ≤ a
h : a ∈ a :: t
⊢ none.elim a (min a) ≤ a

Tactic:
simp

Result:
no goals

Proof state:
case cons
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), t.min?.get ⋯ ≤ a
h : a ∈ b :: t
⊢ t.min?.elim b (min b) ≤ a

Tactic:
rcases mem_cons.1 h with (rfl|h)

Result:
case cons.inl
a : Nat
t : List Nat
ih : ∀ (h : a ∈ t), t.min?.get ⋯ ≤ a
h : a ∈ a :: t
⊢ t.min?.elim a (min a) ≤ a

case cons.inr
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), t.min?.get ⋯ ≤ a
h✝ : a ∈ b :: t
h : a ∈ t
⊢ t.min?.elim b (min b) ≤ a

Proof state:
case cons.inl.some
a : Nat
t : List Nat
ih : ∀ (h : a ∈ t), t.min?.get ⋯ ≤ a
h : a ∈ a :: t
b : Nat
⊢ (some b).elim a (min a) ≤ a

Tactic:
simpa using Nat.min_le_left _ _

Result:
no goals

Proof state:
case cons.inr
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), t.min?.get ⋯ ≤ a
h✝ : a ∈ b :: t
h : a ∈ t
⊢ t.min?.elim b (min b) ≤ a

Tactic:
obtain ⟨q, hq⟩ := Option.isSome_iff_exists.1 (isSome_min?_of_mem h)

Result:
case cons.inr.intro
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), t.min?.get ⋯ ≤ a
h✝ : a ∈ b :: t
h : a ∈ t
q : Nat
hq : t.min? = some q
⊢ t.min?.elim b (min b) ≤ a

Proof state:
case cons.inr.intro
a b : Nat
t : List Nat
h✝ : a ∈ b :: t
h : a ∈ t
q : Nat
hq : t.min? = some q
ih : ∀ (h : a ∈ t), (some q).get ⋯ ≤ a
⊢ min b q ≤ a

Tactic:
exact Nat.le_trans (Nat.min_le_right _ _) (ih h)

Result:
no goals

Proof state:
case cons.inl
a : Nat
t : List Nat
ih : ∀ (h : a ∈ t), t.min?.get ⋯ ≤ a
h : a ∈ a :: t
⊢ t.min?.elim a (min a) ≤ a

Tactic:
cases t.min? with
| none => simp
| some b => simpa using Nat.min_le_left _ _

Result:
no goals

Proof state:
case nil
a : Nat
h : a ∈ []
⊢ [].min?.get ⋯ ≤ a

Tactic:
simp at h

Result:
no goals

Proof state:
case cons
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), t.min?.get ⋯ ≤ a
h : a ∈ b :: t
⊢ (b :: t).min?.get ⋯ ≤ a

Tactic:
simp only [min?_cons, Option.get_some] at ih ⊢

Result:
case cons
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), t.min?.get ⋯ ≤ a
h : a ∈ b :: t
⊢ t.min?.elim b (min b) ≤ a

Proof state:
case cons.inr.intro
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), t.min?.get ⋯ ≤ a
h✝ : a ∈ b :: t
h : a ∈ t
q : Nat
hq : t.min? = some q
⊢ t.min?.elim b (min b) ≤ a

Tactic:
simp only [hq, Option.elim_some] at ih ⊢

Result:
case cons.inr.intro
a b : Nat
t : List Nat
h✝ : a ∈ b :: t
h : a ∈ t
q : Nat
hq : t.min? = some q
ih : ∀ (h : a ∈ t), (some q).get ⋯ ≤ a
⊢ min b q ≤ a
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {fallback : β} :
    m.1.isEmpty = true → getD m a fallback = fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
fallback : β
⊢ m.val.isEmpty = true → getD m a fallback = fallback

Tactic:
simp_to_model

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
fallback : β
⊢ (toListModel m.val.buckets).isEmpty = true → getValueD a (toListModel m.val.buckets) fallback = fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
fallback : β
⊢ (toListModel m.val.buckets).isEmpty = true → getValueD a (toListModel m.val.buckets) fallback = fallback

Tactic:
empty

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insertMany_empty_list_of_contains_eq_false [LawfulBEq α]
    {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
    (h : (l.map Sigma.fst).contains k = false) :
    (insertMany empty l).1.get! k = default

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k : α
inst✝ : Inhabited (β k)
h : (List.map Sigma.fst l).contains k = false
⊢ empty.get! k = default

Tactic:
apply get!_empty

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k : α
inst✝ : Inhabited (β k)
h : (List.map Sigma.fst l).contains k = false
⊢ (empty.insertMany l).val.get! k = default

Tactic:
simp only [get!_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k : α
inst✝ : Inhabited (β k)
h : (List.map Sigma.fst l).contains k = false
⊢ empty.get! k = default
-- Mathlib/Data/Setoid/Basic.lean
theorem comap_eq {f : α → β} {r : Setoid β} : comap f r = ker (@Quotient.mk'' _ r ∘ f) :=
  ext fun x y => show _ ↔ ⟦_⟧ = ⟦_⟧ by rw [Quotient.eq]; rfl

Proof state:
α : Type u_1
β : Type u_2
f : α → β
r : Setoid β
x y : α
⊢ (comap f r) x y ↔ ⟦f x⟧ = ⟦f y⟧

Tactic:
rw [Quotient.eq]

Result:
α : Type u_1
β : Type u_2
f : α → β
r : Setoid β
x y : α
⊢ (comap f r) x y ↔ r (f x) (f y)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
r : Setoid β
x y : α
⊢ (comap f r) x y ↔ r (f x) (f y)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
lemma mem_Ioc_succ' (a : Ioc b (b + 1)) : a = ⟨b + 1, mem_Ioc.2 (by omega)⟩ :=
  Subtype.val_inj.1 (mem_Ioc_succ.1 a.2)

Proof state:
a✝ b c : ℕ
a : { x // x ∈ Ioc b (b + 1) }
⊢ b < b + 1 ∧ b + 1 ≤ b + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Catalan.lean
theorem catalan_succ (n : ℕ) : catalan (n + 1) = ∑ i : Fin n.succ, catalan i * catalan (n - i)

Proof state:
n : ℕ
⊢ catalan (n + 1) = ∑ i : Fin n.succ, catalan ↑i * catalan (n - ↑i)

Tactic:
rw [catalan]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem coe_ennreal_add (x y : ENNReal) : ((x + y : ℝ≥0∞) : EReal) = x + y

Proof state:
x y : ℝ≥0∞
⊢ ↑(x + y) = ↑x + ↑y

Tactic:
cases x <;> cases y <;> rfl

Result:
no goals
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem liftAux_id_apply (x : K) : liftAux (RingHom.id K) j p x = j x

Proof state:
K : Type u_1
M : Type u_3
inst✝³ : CommSemiring K
inst✝² : CommSemiring M
j : K →+* M
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : PerfectRing M p
x : K
this : (Classical.choose ⋯).2 = x ^ p ^ (Classical.choose ⋯).1
⊢ liftAux (RingHom.id K) j p x = j x

Tactic:
rw [liftAux, this, map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply,
  RingEquiv.symm_apply_apply]

Result:
no goals

Proof state:
K : Type u_1
M : Type u_3
inst✝³ : CommSemiring K
inst✝² : CommSemiring M
j : K →+* M
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : PerfectRing M p
x : K
⊢ liftAux (RingHom.id K) j p x = j x

Tactic:
have := RingHom.id_apply _ ▸ Classical.choose_spec (lift_aux (RingHom.id K) p x)

Result:
K : Type u_1
M : Type u_3
inst✝³ : CommSemiring K
inst✝² : CommSemiring M
j : K →+* M
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : PerfectRing M p
x : K
this : (Classical.choose ⋯).2 = x ^ p ^ (Classical.choose ⋯).1
⊢ liftAux (RingHom.id K) j p x = j x
-- Mathlib/Data/Finsupp/Fin.lean
theorem tail_update_succ : tail (update t i.succ y) = update (tail t) i y

Proof state:
case h
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
a✝ : Fin n
⊢ (t.update i.succ y).tail a✝ = (t.tail.update i y) a✝

Tactic:
simp [tail]

Result:
no goals

Proof state:
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
⊢ (t.update i.succ y).tail = t.tail.update i y

Tactic:
ext

Result:
case h
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
a✝ : Fin n
⊢ (t.update i.succ y).tail a✝ = (t.tail.update i y) a✝
-- Mathlib/Algebra/Algebra/Operations.lean
theorem map_op_one :
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (1 : Submodule R A) = 1

Proof state:
case h
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : Aᵐᵒᵖ
⊢ x ∈ map (↑(opLinearEquiv R)) 1 ↔ x ∈ 1

Tactic:
induction x

Result:
case h.h
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
X✝ : A
⊢ op X✝ ∈ map (↑(opLinearEquiv R)) 1 ↔ op X✝ ∈ 1

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ map (↑(opLinearEquiv R)) 1 = 1

Tactic:
ext x

Result:
case h
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : Aᵐᵒᵖ
⊢ x ∈ map (↑(opLinearEquiv R)) 1 ↔ x ∈ 1

Proof state:
case h.h
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
X✝ : A
⊢ op X✝ ∈ map (↑(opLinearEquiv R)) 1 ↔ op X✝ ∈ 1

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
lemma absorbent_iff_inv_smul {s : Set α} :
    Absorbent G₀ s ↔ ∀ x, ∀ᶠ c in cobounded G₀, c⁻¹ • x ∈ s :=
  forall_congr' fun x ↦ by simp only [absorbs_iff_eventually_cobounded_mapsTo, mapsTo_singleton]

Proof state:
G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s : Set α
x : α
⊢ Absorbs G₀ s {x} ↔ ∀ᶠ (c : G₀) in cobounded G₀, c⁻¹ • x ∈ s

Tactic:
simp only [absorbs_iff_eventually_cobounded_mapsTo, mapsTo_singleton]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem to_iso [h' : Epi f.base] : IsIso f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this : IsIso (forgetToPresheafedSpace.map f)
⊢ IsIso f

Tactic:
apply isIso_of_reflects_iso _ (SheafedSpace.forgetToPresheafedSpace)

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
⊢ IsIso f

Tactic:
haveI : IsIso (forgetToPresheafedSpace.map f) := PresheafedSpace.IsOpenImmersion.to_iso f

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this : IsIso (forgetToPresheafedSpace.map f)
⊢ IsIso f
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem eventually_nhdsGT_zero_mul_left {x : 𝕜} (hx : 0 < x) {p : 𝕜 → Prop}
    (h : ∀ᶠ ε in 𝓝[>] 0, p ε) : ∀ᶠ ε in 𝓝[>] 0, p (x * ε)

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
p : 𝕜 → Prop
h : ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p ε
⊢ ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p (x * ε)

Tactic:
rw [← comap_mulLeft_nhdsGT_zero hx]

Result:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
p : 𝕜 → Prop
h : ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p ε
⊢ ∀ᶠ (ε : 𝕜) in comap (fun x_1 => x * x_1) (𝓝[>] 0), p (x * ε)

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
p : 𝕜 → Prop
h : ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p ε
⊢ ∀ᶠ (ε : 𝕜) in comap (fun x_1 => x * x_1) (𝓝[>] 0), p (x * ε)

Tactic:
exact h.comap fun ε => x * ε

Result:
no goals
-- Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
theorem Integrable.exists_hasCompactSupport_lintegral_sub_le
    [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular]
    {f : α → E} (hf : Integrable f μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ g : α → E,
      HasCompactSupport g ∧ ∫⁻ x, ‖f x - g x‖ₑ ∂μ ≤ ε ∧ Continuous g ∧ Integrable g μ

Proof state:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, HasCompactSupport g ∧ ∫⁻ (x : α), ‖f x - g x‖ₑ ∂μ ≤ ε ∧ Continuous g ∧ Integrable g μ

Tactic:
simp only [← memLp_one_iff_integrable, ← eLpNorm_one_eq_lintegral_enorm] at hf ⊢

Result:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hf : MemLp f 1 μ
⊢ ∃ g, HasCompactSupport g ∧ eLpNorm (fun x => f x - g x) 1 μ ≤ ε ∧ Continuous g ∧ MemLp g 1 μ

Proof state:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hf : MemLp f 1 μ
⊢ ∃ g, HasCompactSupport g ∧ eLpNorm (fun x => f x - g x) 1 μ ≤ ε ∧ Continuous g ∧ MemLp g 1 μ

Tactic:
exact hf.exists_hasCompactSupport_eLpNorm_sub_le ENNReal.one_ne_top hε

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem mem_getLast?_append_of_mem_getLast? {l₁ l₂ : List α} {x : α} (h : x ∈ l₂.getLast?) :
    x ∈ (l₁ ++ l₂).getLast?

Proof state:
case cons
α : Type u
l₁ : List α
x head✝ : α
tail✝ : List α
h : x ∈ (head✝ :: tail✝).getLast?
⊢ x ∈ (l₁ ++ head✝ :: tail✝).getLast?

Tactic:
rw [List.getLast?_append_cons]

Result:
case cons
α : Type u
l₁ : List α
x head✝ : α
tail✝ : List α
h : x ∈ (head✝ :: tail✝).getLast?
⊢ x ∈ (head✝ :: tail✝).getLast?

Proof state:
case nil
α : Type u
l₁ : List α
x : α
h : x ∈ [].getLast?
⊢ x ∈ (l₁ ++ []).getLast?

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u
l₁ l₂ : List α
x : α
h : x ∈ l₂.getLast?
⊢ x ∈ (l₁ ++ l₂).getLast?

Tactic:
cases l₂

Result:
case nil
α : Type u
l₁ : List α
x : α
h : x ∈ [].getLast?
⊢ x ∈ (l₁ ++ []).getLast?

case cons
α : Type u
l₁ : List α
x head✝ : α
tail✝ : List α
h : x ∈ (head✝ :: tail✝).getLast?
⊢ x ∈ (l₁ ++ head✝ :: tail✝).getLast?

Proof state:
case cons
α : Type u
l₁ : List α
x head✝ : α
tail✝ : List α
h : x ∈ (head✝ :: tail✝).getLast?
⊢ x ∈ (head✝ :: tail✝).getLast?

Tactic:
exact h

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Integrability.lean
theorem HasIntegral.congr_ae {l : IntegrationParams} {I : Box ι} {y : E} {f g : (ι → ℝ) → E}
    {μ : Measure (ι → ℝ)} [IsLocallyFiniteMeasure μ]
    (hf : HasIntegral.{u, v, v} I l f μ.toBoxAdditive.toSMul y) (hfg : f =ᵐ[μ.restrict I] g)
    (hl : l.bRiemann = false) : HasIntegral.{u, v, v} I l g μ.toBoxAdditive.toSMul y

Proof state:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
y : E
f g : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hf : HasIntegral I l f μ.toBoxAdditive.toSMul y
hfg : f =ᶠ[ae (μ.restrict ↑I)] g
hl : l.bRiemann = false
this : g - f =ᶠ[ae (μ.restrict ↑I)] 0
⊢ HasIntegral I l g μ.toBoxAdditive.toSMul y

Tactic:
simpa using hf.add (HasIntegral.of_aeEq_zero this hl)

Result:
no goals

Proof state:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
y : E
f g : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hf : HasIntegral I l f μ.toBoxAdditive.toSMul y
hfg : f =ᶠ[ae (μ.restrict ↑I)] g
hl : l.bRiemann = false
⊢ HasIntegral I l g μ.toBoxAdditive.toSMul y

Tactic:
have : g - f =ᵐ[μ.restrict I] 0 := hfg.mono fun x hx => sub_eq_zero.2 hx.symm

Result:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
y : E
f g : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hf : HasIntegral I l f μ.toBoxAdditive.toSMul y
hfg : f =ᶠ[ae (μ.restrict ↑I)] g
hl : l.bRiemann = false
this : g - f =ᶠ[ae (μ.restrict ↑I)] 0
⊢ HasIntegral I l g μ.toBoxAdditive.toSMul y
-- Mathlib/RingTheory/Flat/Equalizer.lean
private lemma AlgHom.tensorEqualizerAux_mul (x y : T ⊗[R] AlgHom.equalizer f g) :
    AlgHom.tensorEqualizerAux S T f g (x * y) =
      AlgHom.tensorEqualizerAux S T f g x *
        AlgHom.tensorEqualizerAux S T f g y

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
x y : T ⊗[R] ↥(equalizer f g)
⊢ ↑((AlgHom.tensorEqualizerAux S T f g) (x * y)) =
    ↑((AlgHom.tensorEqualizerAux S T f g) x * (AlgHom.tensorEqualizerAux S T f g) y)

Tactic:
rw [AlgHom.coe_tensorEqualizerAux]

Result:
case a
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
x y : T ⊗[R] ↥(equalizer f g)
⊢ (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) (x * y) =
    ↑((AlgHom.tensorEqualizerAux S T f g) x * (AlgHom.tensorEqualizerAux S T f g) y)

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
x y : T ⊗[R] ↥(equalizer f g)
⊢ (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) (x * y) =
    ↑((AlgHom.tensorEqualizerAux S T f g) x * (AlgHom.tensorEqualizerAux S T f g) y)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
x y : T ⊗[R] ↥(equalizer f g)
⊢ (AlgHom.tensorEqualizerAux S T f g) (x * y) =
    (AlgHom.tensorEqualizerAux S T f g) x * (AlgHom.tensorEqualizerAux S T f g) y

Tactic:
apply Subtype.ext

Result:
case a
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
x y : T ⊗[R] ↥(equalizer f g)
⊢ ↑((AlgHom.tensorEqualizerAux S T f g) (x * y)) =
    ↑((AlgHom.tensorEqualizerAux S T f g) x * (AlgHom.tensorEqualizerAux S T f g) y)
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma δ_snd :
    δ 0 1 (snd φ) = -(fst φ).1.comp (Cochain.ofHom φ) (add_zero 1)

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ (δ 0 1 (snd φ)).v p q hpq = (-(↑(fst φ)).comp (Cochain.ofHom φ) ⋯).v p q hpq

Tactic:
simp [d_snd_v φ p q hpq]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
⊢ δ 0 1 (snd φ) = -(↑(fst φ)).comp (Cochain.ofHom φ) ⋯

Tactic:
ext p q hpq

Result:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ (δ 0 1 (snd φ)).v p q hpq = (-(↑(fst φ)).comp (Cochain.ofHom φ) ⋯).v p q hpq
-- Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean
lemma mk (hX : ∀ (i : ℕ) (_ : n ≤ i) ⦃Y : C⦄, ∀ (e : Ext X Y i), e = 0) :
    HasProjectiveDimensionLT X n where
  subsingleton' i hi Y

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
e₁ e₂ : Ext X Y i
⊢ e₁ = e₂

Tactic:
simp only [hX i hi]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
this✝ : Subsingleton (Ext X Y i)
this : HasExt C := HasExt.standard C
⊢ Subsingleton (Ext X Y i)

Tactic:
exact Ext.chgUniv.{max u v, w}.symm.subsingleton

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
⊢ Subsingleton (Ext X Y i)

Tactic:
have : Subsingleton (Ext X Y i) := ⟨fun e₁ e₂ ↦ by simp only [hX i hi]⟩

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
this : Subsingleton (Ext X Y i)
⊢ Subsingleton (Ext X Y i)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
this : Subsingleton (Ext X Y i)
⊢ Subsingleton (Ext X Y i)

Tactic:
letI := HasExt.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
this✝ : Subsingleton (Ext X Y i)
this : HasExt C := HasExt.standard C
⊢ Subsingleton (Ext X Y i)
-- Mathlib/Data/Real/EReal.lean
lemma mul_div (a b c : EReal) : a * (b / c) = (a * b) / c

Proof state:
a b c : EReal
⊢ a * (b / c) = a * b / c

Tactic:
change a * (b * c⁻¹) = (a * b) * c⁻¹

Result:
a b c : EReal
⊢ a * (b * c⁻¹) = a * b * c⁻¹

Proof state:
a b c : EReal
⊢ a * (b * c⁻¹) = a * b * c⁻¹

Tactic:
rw [mul_assoc]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
/-- A small family of pre-games is bounded below. -/
lemma bddBelow_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → PGame.{u}) :
    BddBelow (Set.range f)

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
x : PGame :=
  mk PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x =>
    (f ((equivShrink ι).symm x.fst)).moveRight x.snd
i : ι
⊢ (∀ (i_1 : x.LeftMoves), x.moveLeft i_1 ⧏ f ((equivShrink ι).symm ((equivShrink ι) i))) ∧
    ∀ (j : (f ((equivShrink ι).symm ((equivShrink ι) i))).RightMoves),
      x ⧏ (f ((equivShrink ι).symm ((equivShrink ι) i))).moveRight j

Tactic:
simpa [x] using fun j ↦ @lf_moveRight x ⟨equivShrink ι i, j⟩

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
x : PGame :=
  mk PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x =>
    (f ((equivShrink ι).symm x.fst)).moveRight x.snd
i : ι
⊢ x ≤ f i

Tactic:
rw [← (equivShrink ι).symm_apply_apply i, le_iff_forall_lf]

Result:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
x : PGame :=
  mk PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x =>
    (f ((equivShrink ι).symm x.fst)).moveRight x.snd
i : ι
⊢ (∀ (i_1 : x.LeftMoves), x.moveLeft i_1 ⧏ f ((equivShrink ι).symm ((equivShrink ι) i))) ∧
    ∀ (j : (f ((equivShrink ι).symm ((equivShrink ι) i))).RightMoves),
      x ⧏ (f ((equivShrink ι).symm ((equivShrink ι) i))).moveRight j

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
⊢ BddBelow (Set.range f)

Tactic:
let x : PGame.{u} := ⟨PEmpty, Σ i, (f <| (equivShrink.{u} ι).symm i).RightMoves, PEmpty.elim,
  fun x ↦ moveRight _ x.2⟩

Result:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
x : PGame :=
  mk PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x =>
    (f ((equivShrink ι).symm x.fst)).moveRight x.snd
⊢ BddBelow (Set.range f)

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
x : PGame :=
  mk PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x =>
    (f ((equivShrink ι).symm x.fst)).moveRight x.snd
⊢ BddBelow (Set.range f)

Tactic:
refine ⟨x, Set.forall_mem_range.2 fun i ↦ ?_⟩

Result:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → PGame
x : PGame :=
  mk PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x =>
    (f ((equivShrink ι).symm x.fst)).moveRight x.snd
i : ι
⊢ x ≤ f i