harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem mul_right_inj (a : αˣ) {b c : α} : (a : α) * b = a * c ↔ b = c :=
  ⟨fun h => by simpa only [inv_mul_cancel_left] using congr_arg (fun x : α => ↑(a⁻¹ : αˣ) * x) h,
    congr_arg _⟩

Proof state:
α : Type u
inst✝ : Monoid α
a : αˣ
b c : α
h : ↑a * b = ↑a * c
⊢ b = c

Tactic:
simpa only [inv_mul_cancel_left] using congr_arg (fun x : α => ↑(a⁻¹ : αˣ) * x) h

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem inner_le_Lp_mul_Lq_of_nonneg (hpq : IsConjExponent p q) (hf : ∀ i ∈ s, 0 ≤ f i)
    (hg : ∀ i ∈ s, 0 ≤ g i) :
    ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.IsConjExponent q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
convert inner_le_Lp_mul_Lq s f g hpq using 3 <;> apply sum_congr rfl <;> intro i hi <;>
  simp only [abs_of_nonneg, hf i hi, hg i hi]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
lemma AnalyticWithinAt.mono (hf : AnalyticWithinAt 𝕜 f s x) (h : t ⊆ s) :
    AnalyticWithinAt 𝕜 f t x

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s t : Set E
x : E
h : t ⊆ s
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
exact ⟨p, hp.mono h⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s t : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
h : t ⊆ s
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
obtain ⟨p, hp⟩ := hf

Result:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s t : Set E
x : E
h : t ⊆ s
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f t x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zip_map' (f : α → β) (g : α → γ) (l : Vector α n) :
    zip (l.map f) (l.map g) = l.map fun a => (f a, g a)

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
l : Array α
⊢ (map f { toArray := l, size_toArray := ⋯ }).zip (map g { toArray := l, size_toArray := ⋯ }) =
    map (fun a => (f a, g a)) { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.zip_map']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β
g : α → γ
l : Vector α n
⊢ (map f l).zip (map g l) = map (fun a => (f a, g a)) l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
l : Array α
⊢ (map f { toArray := l, size_toArray := ⋯ }).zip (map g { toArray := l, size_toArray := ⋯ }) =
    map (fun a => (f a, g a)) { toArray := l, size_toArray := ⋯ }
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorComm_zero_hom_app (a : A) :
    (shiftFunctorComm C a 0).hom.app X =
      (shiftFunctorZero C A).hom.app (X⟦a⟧) ≫ ((shiftFunctorZero C A).inv.app X)⟦a⟧'

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
a : A
⊢ (shiftFunctorComm C a 0).hom.app X =
    (shiftFunctorZero C A).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor C a).map ((shiftFunctorZero C A).inv.app X)

Tactic:
simp only [shiftFunctorZero_hom_app_shift, Category.assoc, ← Functor.map_comp,
  Iso.hom_inv_id_app, Functor.map_id, Functor.comp_obj, Category.comp_id]

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
@[simp] lemma neg_one_pow_mul_eq_zero_iff : (-1) ^ n * a = 0 ↔ a = 0

Proof state:
R : Type u
inst✝ : Ring R
a : R
n : ℕ
⊢ (-1) ^ n * a = 0 ↔ a = 0

Tactic:
rcases neg_one_pow_eq_or R n with h | h <;> simp [h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_X_pow (H : ¬(1 : R) = 0) (n : ℕ) : (X ^ n : R[X]).support = singleton n

Proof state:
case h.e'_2.h.e'_3
R : Type u
inst✝ : Semiring R
H : ¬1 = 0
n : ℕ
⊢ X ^ n = (monomial n) 1

Tactic:
exact X_pow_eq_monomial n

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
H : ¬1 = 0
n : ℕ
⊢ (X ^ n).support = {n}

Tactic:
convert support_monomial n H

Result:
case h.e'_2.h.e'_3
R : Type u
inst✝ : Semiring R
H : ¬1 = 0
n : ℕ
⊢ X ^ n = (monomial n) 1
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.ι_map (j : J) : colimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
j : J
⊢ ι F j ≫ colim.map α = α.app j ≫ ι G j

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem quasiMeasurePreserving_inv_of_right_invariant [IsMulRightInvariant μ] :
    QuasiMeasurePreserving (Inv.inv : G → G) μ μ

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
⊢ QuasiMeasurePreserving Inv.inv μ.inv.inv μ.inv.inv

Tactic:
exact
  (quasiMeasurePreserving_inv μ.inv).mono (inv_absolutelyContinuous μ.inv)
    (absolutelyContinuous_inv μ.inv)

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
⊢ QuasiMeasurePreserving Inv.inv μ μ

Tactic:
rw [← μ.inv_inv]

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
⊢ QuasiMeasurePreserving Inv.inv μ.inv.inv μ.inv.inv
-- Mathlib/LinearAlgebra/TensorPower/Basic.lean
theorem gradedMonoid_eq_of_reindex_cast {ιι : Type*} {ι : ιι → Type*} :
    ∀ {a b : GradedMonoid fun ii => ⨂[R] _ : ι ii, M} (h : a.fst = b.fst),
      reindex R (fun _ ↦ M) (Equiv.cast <| congr_arg ι h) a.snd = b.snd → a = b
  | ⟨ai, a⟩, ⟨bi, b⟩ => fun (hi : ai = bi) (h : reindex R (fun _ ↦ M) _ a = b) => by
    subst hi
    simp_all

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ιι : Type u_3
ι : ιι → Type u_4
ai : ιι
a : ⨂[R] (x : ι ai), M
bi : ιι
b : ⨂[R] (x : ι bi), M
hi : ai = bi
h : (reindex R (fun x => M) (Equiv.cast ⋯)) a = b
⊢ ⟨ai, a⟩ = ⟨bi, b⟩

Tactic:
subst hi

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ιι : Type u_3
ι : ιι → Type u_4
ai : ιι
a b : ⨂[R] (x : ι ai), M
h : (reindex R (fun x => M) (Equiv.cast ⋯)) a = b
⊢ ⟨ai, a⟩ = ⟨ai, b⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ιι : Type u_3
ι : ιι → Type u_4
ai : ιι
a b : ⨂[R] (x : ι ai), M
h : (reindex R (fun x => M) (Equiv.cast ⋯)) a = b
⊢ ⟨ai, a⟩ = ⟨ai, b⟩

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/Homology/Double.lean
lemma double_d_eq_zero₀ (a b : ι) (ha : a ≠ i₀) :
    (double f hi₀₁).d a b = 0 :=
  dif_neg (by tauto)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
a b : ι
ha : a ≠ i₀
⊢ ¬(a = i₀ ∧ b = i₁ ∧ i₀ ≠ i₁)

Tactic:
tauto

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma add_emod_eq_add_mod_right {m n k : ℤ} (i : ℤ) (H : m % n = k % n) :
    (m + i) % n = (k + i) % n

Proof state:
m n k i : ℤ
H : m % n = k % n
⊢ (m + i) % n = (k + i) % n

Tactic:
rw [← emod_add_emod, ← emod_add_emod k, H]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem symm_apply_eq {α β} (e : α ≃ β) {x y} : e.symm x = y ↔ x = e y :=
  ⟨fun H => by simp [H.symm], fun H => by simp [H]⟩

Proof state:
α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : α
H : x = e y
⊢ e.symm x = y

Tactic:
simp [H]

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : α
H : e.symm x = y
⊢ x = e y

Tactic:
simp [H.symm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem upperBoundP?_exists {t : RBSet α cmp} [TransCmp cmp] [IsCut cmp cut] :
    (∃ x, t.upperBoundP? cut = some x) ↔ ∃ x ∈ t, cut x ≠ .gt

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBSet α cmp
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
⊢ (∃ x, t.upperBoundP? cut = some x) ↔ ∃ x, x ∈ t ∧ cut x ≠ Ordering.gt

Tactic:
simp [upperBoundP?, t.2.out.1.upperBound?_exists, mem_toList, mem_iff_mem_toList]

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBSet α cmp
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
⊢ (∃ x, x ∈ t.val ∧ ¬cut x = Ordering.gt) ↔ ∃ x, (∃ y, y ∈ t.val ∧ cmp x y = Ordering.eq) ∧ ¬cut x = Ordering.gt

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBSet α cmp
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
⊢ (∃ x, x ∈ t.val ∧ ¬cut x = Ordering.gt) ↔ ∃ x, (∃ y, y ∈ t.val ∧ cmp x y = Ordering.eq) ∧ ¬cut x = Ordering.gt

Tactic:
exact ⟨
  fun ⟨x, h1, h2⟩ => ⟨x, ⟨x, h1, OrientedCmp.cmp_refl⟩, h2⟩,
  fun ⟨x, ⟨y, h1, h2⟩, eq⟩ => ⟨y, h1, IsCut.congr (cut := cut) h2 ▸ eq⟩⟩

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
protected lemma existsUnique_congr (h : ∀ a, p a ↔ q (e a)) : (∃! a, p a) ↔ ∃! b, q b :=
  e.existsUnique_congr_left.trans <| by simp [h]

Proof state:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ (∃! b, p (e.symm b)) ↔ ∃! b, q b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Order/Bounded.lean
theorem unbounded_le_inter_le [LinearOrder α] (a : α) :
    Unbounded (· ≤ ·) (s ∩ { b | a ≤ b }) ↔ Unbounded (· ≤ ·) s

Proof state:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a ≤ b}) ↔ Bounded (fun x1 x2 => x1 ≤ x2) s

Tactic:
exact bounded_le_inter_le a

Result:
no goals

Proof state:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Unbounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a ≤ b}) ↔ Unbounded (fun x1 x2 => x1 ≤ x2) s

Tactic:
rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]

Result:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a ≤ b}) ↔ Bounded (fun x1 x2 => x1 ≤ x2) s
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@[simp]
lemma stalkMap_hom_inv_apply (e : X ≅ Y) (y : Y) (z) :
    e.inv.stalkMap y (e.hom.stalkMap (e.inv.base y) z) =
      Y.presheaf.stalkSpecializes (specializes_of_eq <| by simp) z :=
  DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkMap_hom_inv e y)) z

Proof state:
X✝ X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
y : ↑Y.toTopCat
z : ↑(Y.presheaf.stalk ((ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y)))
⊢ y = (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem iteratedFDeriv_add_apply {i : ℕ} {f g : E → F}
    (hf : ContDiffAt 𝕜 i f x) (hg : ContDiffAt 𝕜 i g x) :
    iteratedFDeriv 𝕜 i (f + g) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
i : ℕ
f g : E → F
hf : ContDiffAt 𝕜 (↑i) f x
hg : ContDiffAt 𝕜 (↑i) g x
⊢ iteratedFDerivWithin 𝕜 i (f + g) univ x = iteratedFDerivWithin 𝕜 i f univ x + iteratedFDerivWithin 𝕜 i g univ x

Tactic:
exact iteratedFDerivWithin_add_apply hf hg uniqueDiffOn_univ (Set.mem_univ _)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
i : ℕ
f g : E → F
hf : ContDiffAt 𝕜 (↑i) f x
hg : ContDiffAt 𝕜 (↑i) g x
⊢ iteratedFDeriv 𝕜 i (f + g) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x

Tactic:
simp_rw [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
i : ℕ
f g : E → F
hf : ContDiffAt 𝕜 (↑i) f x
hg : ContDiffAt 𝕜 (↑i) g x
⊢ iteratedFDerivWithin 𝕜 i (f + g) univ x = iteratedFDerivWithin 𝕜 i f univ x + iteratedFDerivWithin 𝕜 i g univ x
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem spanExt_app_one : (spanExt iX iY iZ wf wg).app WalkingSpan.zero = iX

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).app WalkingSpan.zero = iX

Tactic:
dsimp [spanExt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem add_nonnneg_iff_neg_le' {a b : Int} : 0 ≤ a + b ↔ -a ≤ b

Proof state:
a b : Int
⊢ 0 ≤ a + b ↔ -a ≤ b

Tactic:
rw [Int.add_comm, add_nonnneg_iff_neg_le]

Result:
no goals
-- Mathlib/Analysis/Calculus/Implicit.lean
theorem implicitFunctionOfComplemented_apply_image (hf : HasStrictFDerivAt f f' a)
    (hf' : range f' = ⊤) (hker : (ker f').ClosedComplemented) :
    hf.implicitFunctionOfComplemented f f' hf' hker (f a) 0 = a

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : (LinearMap.ker f').ClosedComplemented
⊢ implicitFunctionOfComplemented f f' hf hf' hker (f a) 0 = a

Tactic:
simpa only [implicitToPartialHomeomorphOfComplemented_self] using
    (hf.implicitToPartialHomeomorphOfComplemented f f' hf' hker).left_inv
    (hf.mem_implicitToPartialHomeomorphOfComplemented_source hf' hker)

Result:
no goals
-- Mathlib/Algebra/GradedMonoid.lean
theorem List.dProdIndex_eq_map_sum (l : List α) (fι : α → ι) :
    l.dProdIndex fι = (l.map fι).sum

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : AddMonoid ι
l : List α
fι : α → ι
⊢ [].dProdIndex fι = (map fι []).sum

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : AddMonoid ι
l : List α
fι : α → ι
head : α
tail : List α
⊢ (head :: tail).dProdIndex fι = (map fι (head :: tail)).sum

Tactic:
simp [List.dProdIndex_eq_map_sum tail fι]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : AddMonoid ι
l : List α
fι : α → ι
⊢ l.dProdIndex fι = (map fι l).sum

Tactic:
match l with
| [] => simp
| head::tail => simp [List.dProdIndex_eq_map_sum tail fι]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem lintegral_congr {f g : α →ₛ ℝ≥0∞} (h : f =ᵐ[μ] g) : f.lintegral μ = g.lintegral μ :=
  lintegral_eq_of_measure_preimage fun y =>
    measure_congr <| Eventually.set_eq <| h.mono fun x hx => by simp [hx]

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
h : ⇑f =ᶠ[ae μ] ⇑g
y : ℝ≥0∞
x : α
hx : f x = g x
⊢ x ∈ ⇑f ⁻¹' {y} ↔ x ∈ ⇑g ⁻¹' {y}

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem image2_iInter₂_subset_right (s : Set α) (t : ∀ i, κ i → Set β) :
    image2 f s (⋂ (i) (j), t i j) ⊆ ⋂ (i) (j), image2 f s (t i j)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ image2 f s (⋂ i, ⋂ j, t i j) ⊆ ⋂ i, ⋂ j, image2 f s (t i j)

Tactic:
simp_rw [image2_subset_iff, mem_iInter]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι) (i_1 : κ i), y ∈ t i i_1) → ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f s (t i i_1)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι) (i_1 : κ i), y ∈ t i i_1) → ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f s (t i i_1)

Tactic:
exact fun x hx y hy i j => mem_image2_of_mem hx (hy _ _)

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
theorem explicitCokernelDesc_normNoninc {X Y Z : SemiNormedGrp.{u}} {f : X ⟶ Y} {g : Y ⟶ Z}
    {cond : f ≫ g = 0} (hg : g.hom.NormNoninc) : (explicitCokernelDesc cond).hom.NormNoninc

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : (Hom.hom g).NormNoninc
⊢ (Hom.hom (explicitCokernelDesc cond)).NormNoninc

Tactic:
refine NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.2 ?_

Result:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : (Hom.hom g).NormNoninc
⊢ ‖Hom.hom (explicitCokernelDesc cond)‖ ≤ 1

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : (Hom.hom g).NormNoninc
⊢ ‖Hom.hom (explicitCokernelDesc cond)‖ ≤ ↑1

Tactic:
exact
  explicitCokernelDesc_norm_le_of_norm_le cond 1
    (NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.1 hg)

Result:
no goals

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : (Hom.hom g).NormNoninc
⊢ ‖Hom.hom (explicitCokernelDesc cond)‖ ≤ 1

Tactic:
rw [← NNReal.coe_one]

Result:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : (Hom.hom g).NormNoninc
⊢ ‖Hom.hom (explicitCokernelDesc cond)‖ ≤ ↑1
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem tensor_left_iff {X Y : C} (f g : X ⟶ Y) : 𝟙 (𝟙_ C) ⊗ f = 𝟙 (𝟙_ C) ⊗ g ↔ f = g

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
⊢ 𝟙 (𝟙_ C) ⊗ f = 𝟙 (𝟙_ C) ⊗ g ↔ f = g

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma glueDataObjι_ι (U : X.affineOpens) : I.glueDataObjι U ≫ U.1.ι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk _)) ≫ U.2.fromSpec

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv ≫ (↑U).ι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯

Tactic:
rfl

Result:
no goals

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ I.glueDataObjι U ≫ (↑U).ι = Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯

Tactic:
rw [glueDataObjι, Category.assoc]

Result:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv ≫ (↑U).ι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem weightedSMul_apply {m : MeasurableSpace α} (μ : Measure α) (s : Set α) (x : F) :
    weightedSMul μ s x = (μ s).toReal • x

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
x : F
⊢ (weightedSMul μ s) x = (μ s).toReal • x

Tactic:
simp [weightedSMul]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem ker_equiv {F' : Type*} [EquivLike F' R S] [RingEquivClass F' R S] (f : F') :
    ker f = ⊥

Proof state:
case h
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
F' : Type u_3
inst✝¹ : EquivLike F' R S
inst✝ : RingEquivClass F' R S
f : F'
x✝ : R
⊢ x✝ ∈ ker f ↔ x✝ ∈ ⊥

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
F' : Type u_3
inst✝¹ : EquivLike F' R S
inst✝ : RingEquivClass F' R S
f : F'
⊢ ker f = ⊥

Tactic:
ext

Result:
case h
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
F' : Type u_3
inst✝¹ : EquivLike F' R S
inst✝ : RingEquivClass F' R S
f : F'
x✝ : R
⊢ x✝ ∈ ker f ↔ x✝ ∈ ⊥
-- Mathlib/Data/Finset/Union.lean
@[simp]
lemma biUnion_singleton_eq_self [DecidableEq α] : s.biUnion (singleton : α → Finset α) = s :=
  ext fun x ↦ by simp only [mem_biUnion, mem_singleton, exists_prop, exists_eq_right']

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
x : α
⊢ x ∈ s.biUnion singleton ↔ x ∈ s

Tactic:
simp only [mem_biUnion, mem_singleton, exists_prop, exists_eq_right']

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_lt_pi_div_two_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2)
    (h0 : p₃ ≠ p₂) : ∠ p₂ p₃ p₁ < π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ < π / 2

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ < π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) < π / 2

Tactic:
exact angle_add_lt_pi_div_two_of_inner_eq_zero h h0

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ < π / 2

Tactic:
rw [ne_comm, ← @vsub_ne_zero V] at h0

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ ∠ p₂ p₃ p₁ < π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ ∠ p₂ p₃ p₁ < π / 2

Tactic:
rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) < π / 2
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_imp_distrib {f : Filter α} {p q : α → Prop} :
    (∃ᶠ x in f, p x → q x) ↔ (∀ᶠ x in f, p x) → ∃ᶠ x in f, q x

Proof state:
α : Type u
f : Filter α
p q : α → Prop
⊢ (∃ᶠ (x : α) in f, p x → q x) ↔ (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, q x

Tactic:
simp [imp_iff_not_or]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem principal_bind {s : Set α} {f : α → Filter β} : bind (𝓟 s) f = ⨆ x ∈ s, f x :=
  show join (map f (𝓟 s)) = ⨆ x ∈ s, f x by
    simp only [sSup_image, join_principal_eq_sSup, map_principal, eq_self_iff_true]

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → Filter β
⊢ (map f (𝓟 s)).join = ⨆ x ∈ s, f x

Tactic:
simp only [sSup_image, join_principal_eq_sSup, map_principal, eq_self_iff_true]

Result:
no goals