harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean
theorem extensiveTopology.isSheaf_yoneda_obj (W : C) : Presieve.IsSheaf (extensiveTopology C)
    (yoneda.obj W)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : FinitaryPreExtensive C
W X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
⊢ IsSheafFor (yoneda.obj W) R

Tactic:
have : IsIso (Sigma.desc (Cofan.inj (Cofan.mk X π))) := hi

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : FinitaryPreExtensive C
W X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
this : IsIso (Sigma.desc (Cofan.mk X π).inj)
⊢ IsSheafFor (yoneda.obj W) R

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : FinitaryPreExtensive C
W : C
⊢ IsSheaf (extensiveTopology C) (yoneda.obj W)

Tactic:
rw [extensiveTopology, isSheaf_coverage]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : FinitaryPreExtensive C
W : C
⊢ ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor (yoneda.obj W) R

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : FinitaryPreExtensive C
W X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
this✝ : IsIso (Sigma.desc (Cofan.mk X π).inj)
this : R.Extensive
⊢ IsSheafFor (yoneda.obj W) R

Tactic:
exact isSheafFor_extensive_of_preservesFiniteProducts _ _

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : FinitaryPreExtensive C
W : C
⊢ ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor (yoneda.obj W) R

Tactic:
intro X R ⟨Y, α, Z, π, hR, hi⟩

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : FinitaryPreExtensive C
W X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
⊢ IsSheafFor (yoneda.obj W) R

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : FinitaryPreExtensive C
W X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
this : IsIso (Sigma.desc (Cofan.mk X π).inj)
⊢ IsSheafFor (yoneda.obj W) R

Tactic:
have : R.Extensive := ⟨Y, α, Z, π, hR, ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩⟩

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : FinitaryPreExtensive C
W X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
this✝ : IsIso (Sigma.desc (Cofan.mk X π).inj)
this : R.Extensive
⊢ IsSheafFor (yoneda.obj W) R
-- Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean
theorem toLp_norm_le :
    ‖(toLp p μ 𝕜 : C(α, E) →L[𝕜] Lp E p μ)‖ ≤ measureUnivNNReal μ ^ p.toReal⁻¹

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : CompactSpace α
inst✝³ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝² : Fact (1 ≤ p)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
⊢ ‖toLp p μ 𝕜‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹

Tactic:
rw [toLp_norm_eq_toLp_norm_coe]

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : CompactSpace α
inst✝³ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝² : Fact (1 ≤ p)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
⊢ ‖BoundedContinuousFunction.toLp p μ 𝕜‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : CompactSpace α
inst✝³ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝² : Fact (1 ≤ p)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
⊢ ‖BoundedContinuousFunction.toLp p μ 𝕜‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹

Tactic:
exact BoundedContinuousFunction.toLp_norm_le μ

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
lemma exp_eq_one {r : ℝ} : exp r = 1 ↔ ∃ n : ℤ, r = n * (2 * π)

Proof state:
r : ℝ
⊢ exp r = 1 ↔ ∃ n, r = ↑n * (2 * π)

Tactic:
simp [Circle.ext_iff, Complex.exp_eq_one_iff, ← mul_assoc, Complex.I_ne_zero,
  ← Complex.ofReal_inj]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma le_sub_one_iff : m ≤ n - 1 ↔ m < n

Proof state:
m n : ℤ
⊢ m ≤ n - 1 ↔ m < n

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_eq_none [LawfulBEq α] (h : m.1.WF) {a : α} :
    m.contains a = false → m.get? a = none

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a : α
⊢ m.contains a = false → m.get? a = none

Tactic:
simp_to_model using List.getValueCast?_eq_none

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
@[simp]
lemma Fin.nndist_insertNth_insertNth {n : ℕ} {α : Fin (n + 1) → Type*}
    [∀ i, PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x y : α i) (f g : ∀ j, α (i.succAbove j)) :
    nndist (i.insertNth x f) (i.insertNth y g) = max (nndist x y) (nndist f g) :=
  eq_of_forall_ge_iff fun c => by simp [nndist_pi_le_iff, i.forall_iff_succAbove]

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_4
inst✝ : (i : Fin (n + 1)) → PseudoMetricSpace (α i)
i : Fin (n + 1)
x y : α i
f g : (j : Fin n) → α (i.succAbove j)
c : ℝ≥0
⊢ nndist (i.insertNth x f) (i.insertNth y g) ≤ c ↔ nndist x y ⊔ nndist f g ≤ c

Tactic:
simp [nndist_pi_le_iff, i.forall_iff_succAbove]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_erase [LawfulBEq α] (h : m.1.WF) {k a : α} [Inhabited (β a)] :
    (m.erase k).get! a = if k == a then default else m.get! a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
k a : α
inst✝ : Inhabited (β a)
⊢ (m.erase k).get! a = if (k == a) = true then default else m.get! a

Tactic:
simp_to_model [erase] using List.getValueCast!_eraseKey

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
@[simp] lemma map_fst_prod : Measure.map Prod.fst (μ.prod ν) = (ν univ) • μ

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
⊢ map Prod.fst (μ.prod ν) = ν univ • μ

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
hs : MeasurableSet s
⊢ (map Prod.fst (μ.prod ν)) s = (ν univ • μ) s

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
hs : MeasurableSet s
⊢ (map Prod.fst (μ.prod ν)) s = (ν univ • μ) s

Tactic:
simp [Measure.map_apply measurable_fst hs, ← prod_univ, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_mem {l : Vector α n} {i : Nat} (h : i < n) : l[i] ∈ l

Proof state:
case mk
α : Type u_1
i : Nat
l : Array α
h : i < l.size
⊢ { toArray := l, size_toArray := ⋯ }[i] ∈ { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
⊢ l[i] ∈ l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
i : Nat
l : Array α
h : i < l.size
⊢ { toArray := l, size_toArray := ⋯ }[i] ∈ { toArray := l, size_toArray := ⋯ }
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_eq_zero_iff : ⌊a⌋ = 0 ↔ a ∈ Ico (0 : α) 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ⌊a⌋ = 0 ↔ a ∈ Ico 0 1

Tactic:
simp [floor_eq_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Basic.lean
theorem all_iff {t : RBNode α} : t.all p ↔ t.All (p ·)

Proof state:
α : Type u_1
p : α → Bool
t : RBNode α
⊢ all p t = true ↔ All (fun x => p x = true) t

Tactic:
induction t <;> simp [*, all, All, and_assoc]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_const_one : (∏ _x ∈ s, (1 : β)) = 1

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
inst✝ : CommMonoid β
⊢ ∏ _x ∈ s, 1 = 1

Tactic:
simp only [Finset.prod, Multiset.map_const', Multiset.prod_replicate, one_pow]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma toQuotient_relation (r : relations.R) :
    relations.toQuotient (relations.relation r) = 0

Proof state:
A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ relations.relation r ∈ Set.range relations.relation

Tactic:
simp

Result:
no goals

Proof state:
A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ relations.toQuotient (relations.relation r) = 0

Tactic:
dsimp only [toQuotient, Quotient]

Result:
A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ (Submodule.span A (Set.range relations.relation)).mkQ (relations.relation r) = 0

Proof state:
A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ relations.relation r ∈ Submodule.span A (Set.range relations.relation)

Tactic:
exact Submodule.subset_span (by simp)

Result:
no goals

Proof state:
A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ (Submodule.span A (Set.range relations.relation)).mkQ (relations.relation r) = 0

Tactic:
rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]

Result:
A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ relations.relation r ∈ Submodule.span A (Set.range relations.relation)
-- Mathlib/Order/Bounds/Image.lean
lemma bddAbove_range_pi {F : ι → ∀ a, π a} :
    BddAbove (range F) ↔ ∀ a, BddAbove (range fun i ↦ F i a)

Proof state:
α : Type u
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
⊢ BddAbove (range F) ↔ ∀ (a : α), BddAbove (range fun i => F i a)

Tactic:
simp only [bddAbove_pi, ← range_comp]

Result:
α : Type u
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
⊢ (∀ (a : α), BddAbove (range (eval a ∘ F))) ↔ ∀ (a : α), BddAbove (range fun i => F i a)

Proof state:
α : Type u
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
⊢ (∀ (a : α), BddAbove (range (eval a ∘ F))) ↔ ∀ (a : α), BddAbove (range fun i => F i a)

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Lemmas.lean
/-- Two multiplicative characters on a monoid whose unit group is generated by `g`
are equal if and only if they agree on `g`. -/
lemma eq_iff {R R' : Type*} [CommMonoid R] [CommMonoidWithZero R'] {g : Rˣ}
    (hg : ∀ x, x ∈ Subgroup.zpowers g) (χ₁ χ₂ : MulChar R R') :
    χ₁ = χ₂ ↔ χ₁ g.val = χ₂ g.val

Proof state:
R : Type u_1
R' : Type u_2
inst✝¹ : CommMonoid R
inst✝ : CommMonoidWithZero R'
g : Rˣ
hg : ∀ (x : Rˣ), x ∈ Subgroup.zpowers g
χ₁ χ₂ : MulChar R R'
⊢ χ₁ = χ₂ ↔ χ₁ ↑g = χ₂ ↑g

Tactic:
rw [← Equiv.apply_eq_iff_eq equivToUnitHom, MonoidHom.eq_iff_eq_on_generator hg,
  ← coe_equivToUnitHom, ← coe_equivToUnitHom, Units.ext_iff]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem biSup_const {a : α} {s : Set β} (hs : s.Nonempty) : ⨆ i ∈ s, a = a

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
this : Nonempty ↑s
⊢ ⨆ i ∈ s, a = a

Tactic:
rw [← iSup_subtype'', iSup_const]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
⊢ ⨆ i ∈ s, a = a

Tactic:
haveI : Nonempty s := Set.nonempty_coe_sort.mpr hs

Result:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
this : Nonempty ↑s
⊢ ⨆ i ∈ s, a = a
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem smulTower_leftMulMatrix_algebraMap_eq (x : S) (i j k) :
    leftMulMatrix (b.smulTower c) (algebraMap _ _ x) (i, k) (j, k) = leftMulMatrix b x i j

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i j : m
k : n
⊢ (leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k) = (leftMulMatrix b) x i j

Tactic:
rw [smulTower_leftMulMatrix_algebraMap, blockDiagonal_apply_eq]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc (attr := simp)]
lemma liftCycles_comp_cyclesMap (φ : S ⟶ S₁) [S₁.HasLeftHomology] :
    S.liftCycles k hk ≫ cyclesMap φ =
      S₁.liftCycles (k ≫ φ.τ₂) (by rw [assoc, φ.comm₂₃, reassoc_of% hk, zero_comp])

Proof state:
C : Type u_1
inst✝³ : Category.{?u.212328, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝¹ : S.HasLeftHomology
φ : S ⟶ S₁
inst✝ : S₁.HasLeftHomology
⊢ (k ≫ φ.τ₂) ≫ S₁.g = 0

Tactic:
rw [assoc, φ.comm₂₃, reassoc_of% hk, zero_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ : ShortComplex C
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝¹ : S.HasLeftHomology
φ : S ⟶ S₁
inst✝ : S₁.HasLeftHomology
⊢ S.liftCycles k hk ≫ cyclesMap φ = S₁.liftCycles (k ≫ φ.τ₂) ⋯

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem projIci_eq_self : projIci a x = ⟨a, le_rfl⟩ ↔ x ≤ a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a x : α
⊢ projIci a x = ⟨a, ⋯⟩ ↔ x ≤ a

Tactic:
simp [projIci, Subtype.ext_iff]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem _root_.Disjoint.exists_cthickenings (hst : Disjoint s t) (hs : IsCompact s)
    (ht : IsClosed t) :
    ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
⊢ ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)

Tactic:
obtain ⟨δ, hδ, h⟩ := hst.exists_thickenings hs ht

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)

Tactic:
refine ⟨δ / 2, half_pos hδ, h.mono ?_ ?_⟩ <;>
  exact cthickening_subset_thickening' hδ (half_lt_self hδ) _

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem forall₂_true_iff {β : α → Sort*} : (∀ a, β a → True) ↔ True

Proof state:
α : Sort u_1
β : α → Sort u_3
⊢ (∀ (a : α), β a → True) ↔ True

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    (m.alter k f).getKey? k = if (f (m.get? k)).isSome then some k else none

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).getKey? k = if (f (m.get? k)).isSome = true then some k else none

Tactic:
simp [getKey?_alter h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/TakeDrop.lean
theorem exists_of_uset (self : Array α) (i d h) :
    ∃ l₁ l₂, self.toList = l₁ ++ self[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
      (self.uset i d h).toList = l₁ ++ d :: l₂

Proof state:
α : Type u_1
self : Array α
i : USize
d : α
h : i.toNat < self.size
⊢ ∃ l₁ l₂, self.toList = l₁ ++ self[i] :: l₂ ∧ l₁.length = i.toNat ∧ (self.uset i d h).toList = l₁ ++ d :: l₂

Tactic:
simpa only [ugetElem_eq_getElem, ← getElem_toList, uset, toList_set] using
  List.exists_of_set _

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem norm_add_eq_add_norm_of_angle_eq_zero {x y : V} (h : angle x y = 0) :
    ‖x + y‖ = ‖x‖ + ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x + y‖ = ‖x‖ + ‖y‖

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg (x + y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
  norm_add_pow_two_real, inner_eq_mul_norm_of_angle_eq_zero h]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x‖ ^ 2 + 2 * (‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x‖ ^ 2 + 2 * (‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive (attr := simp) abs_nonneg] lemma one_le_mabs (a : α) : 1 ≤ |a|ₘ

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ mabs a

Tactic:
apply pow_two_semiclosed _

Result:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ mabs a ^ 2

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ mabs a ^ 2

Tactic:
rw [mabs, pow_two, mul_sup,  sup_mul, ← pow_two, inv_mul_cancel, sup_comm, ← sup_assoc]

Result:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ (a ⊔ a⁻¹) * a⁻¹ ⊔ a ^ 2 ⊔ 1

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ (a ⊔ a⁻¹) * a⁻¹ ⊔ a ^ 2 ⊔ 1

Tactic:
apply le_sup_right

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem _root_.Polynomial.toLaurent_C_mul_X_pow (n : ℕ) (r : R) :
    toLaurent (Polynomial.C r * X ^ n) = C r * T n

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ toLaurent (Polynomial.C r * X ^ n) = C r * T ↑n

Tactic:
simp only [_root_.map_mul, Polynomial.toLaurent_C, Polynomial.toLaurent_X_pow]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem delta_lt_false {a b : ℕ} (h₁ : delta * a < b) (h₂ : delta * b < a) : False :=
  not_le_of_lt (lt_trans ((mul_lt_mul_left (by decide)).2 h₁) h₂) <| by
    simpa [mul_assoc] using Nat.mul_le_mul_right a (by decide : 1 ≤ delta * delta)

Proof state:
a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ 0 < delta

Tactic:
decide

Result:
no goals

Proof state:
a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ a ≤ delta * (delta * a)

Tactic:
simpa [mul_assoc] using Nat.mul_le_mul_right a (by decide : 1 ≤ delta * delta)

Result:
no goals

Proof state:
a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ 1 ≤ delta * delta

Tactic:
decide

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem eval_bicategoricalComp
    {η η' : f ⟶ g} {α : g ≅ h} {θ θ' : h ⟶ i} {αθ : g ⟶ i} {ηαθ : f ⟶ i}
    (e_η : η = η') (e_θ : θ = θ') (e_αθ : α.hom ≫ θ' = αθ) (e_ηαθ : η' ≫ αθ = ηαθ) :
    η ≫ α.hom ≫ θ = ηαθ

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g h i : a ⟶ b
η η' : f ⟶ g
α : g ≅ h
θ θ' : h ⟶ i
αθ : g ⟶ i
ηαθ : f ⟶ i
e_η : η = η'
e_θ : θ = θ'
e_αθ : α.hom ≫ θ' = αθ
e_ηαθ : η' ≫ αθ = ηαθ
⊢ η ≫ α.hom ≫ θ = ηαθ

Tactic:
simp [e_η, e_θ, e_αθ, e_ηαθ]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.map_desc {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j)
    {P : C} (k : ∀ j, g j ⟶ P) :
    biproduct.map p ≫ biproduct.desc k = biproduct.desc fun j => p j ≫ k j

Proof state:
case w
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
P : C
k : (j : J) → g j ⟶ P
j✝ : J
⊢ ι f j✝ ≫ map p ≫ desc k = ι f j✝ ≫ desc fun j => p j ≫ k j

Tactic:
simp

Result:
no goals

Proof state:
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
P : C
k : (j : J) → g j ⟶ P
⊢ map p ≫ desc k = desc fun j => p j ≫ k j

Tactic:
ext

Result:
case w
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
P : C
k : (j : J) → g j ⟶ P
j✝ : J
⊢ ι f j✝ ≫ map p ≫ desc k = ι f j✝ ≫ desc fun j => p j ≫ k j
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_indicatorConstLp [CompleteSpace E]
    {p : ℝ≥0∞} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμt : μ t ≠ ∞) (e : E) :
    ∫ x in s, indicatorConstLp p ht hμt e x ∂μ = (μ (t ∩ s)).toReal • e :=
  calc
    ∫ x in s, indicatorConstLp p ht hμt e x ∂μ = ∫ x in s, t.indicator (fun _ => e) x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Set X
μ : Measure X
inst✝ : CompleteSpace E
p : ℝ≥0∞
hs : MeasurableSet s
ht : MeasurableSet t
hμt : μ t ≠ ⊤
e : E
⊢ ∫ (x : X) in s, t.indicator (fun x => e) x ∂μ = (μ (t ∩ s)).toReal • e

Tactic:
rw [integral_indicator_const _ ht, Measure.restrict_apply ht]

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Set X
μ : Measure X
inst✝ : CompleteSpace E
p : ℝ≥0∞
hs : MeasurableSet s
ht : MeasurableSet t
hμt : μ t ≠ ⊤
e : E
⊢ ∫ (x : X) in s, ↑↑(indicatorConstLp p ht hμt e) x ∂μ = ∫ (x : X) in s, t.indicator (fun x => e) x ∂μ

Tactic:
rw [setIntegral_congr_ae hs (indicatorConstLp_coeFn.mono fun x hx _ => hx)]

Result:
no goals
-- Mathlib/RingTheory/RingHom/Locally.lean
/-- If `P` respects isomorphisms, to check `P` holds locally for `f : R →+* S`, it suffices
to check `P` holds on a standard open cover. -/
lemma locally_of_exists (hP : RespectsIso P) (f : R →+* S) {ι : Type*} (s : ι → S)
    (hsone : Ideal.span (Set.range s) = ⊤)
    (Sₜ : ι → Type u) [∀ i, CommRing (Sₜ i)] [∀ i, Algebra S (Sₜ i)]
    [∀ i, IsLocalization.Away (s i) (Sₜ i)] (hf : ∀ i, P ((algebraMap S (Sₜ i)).comp f)) :
    Locally P f

Proof state:
case h.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
ι : Type u_1
s : ι → S
hsone : Ideal.span (Set.range s) = ⊤
Sₜ : ι → Type u
inst✝² : (i : ι) → CommRing (Sₜ i)
inst✝¹ : (i : ι) → Algebra S (Sₜ i)
inst✝ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)
hf : ∀ (i : ι), P ((algebraMap S (Sₜ i)).comp f)
i : ι
e : Localization.Away (s i) ≃+* Sₜ i :=
  (IsLocalization.algEquiv (Submonoid.powers (s i)) (Localization.Away (s i)) (Sₜ i)).toRingEquiv
this : algebraMap S (Localization.Away (s i)) = e.symm.toRingHom.comp (algebraMap S (Sₜ i))
⊢ P (e.symm.toRingHom.comp ((algebraMap S (Sₜ i)).comp f))

Tactic:
exact hP.left _ _ (hf i)

Result:
no goals