harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_le_ofReal_iff {p q : ℝ} (h : 0 ≤ q) :
    ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q

Proof state:
p q : ℝ
h : 0 ≤ q
⊢ ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, coe_le_coe, Real.toNNReal_le_toNNReal_iff h]

Result:
no goals
-- Mathlib/Analysis/MellinTransform.lean
theorem mellin_comp_inv (f : ℝ → E) (s : ℂ) : mellin (fun t => f t⁻¹) s = mellin f (-s)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ mellin (fun t => f t⁻¹) s = mellin f (-s)

Tactic:
simp_rw [← rpow_neg_one, mellin_comp_rpow _ _ _, abs_neg, abs_one,
  inv_one, one_smul, ofReal_neg, ofReal_one, div_neg, div_one]

Result:
no goals
-- Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
lemma continuous_from_compactlyGenerated [TopologicalSpace X] [t : TopologicalSpace Y] (f : X → Y)
    (h : ∀ (S : CompHaus.{u}) (g : C(S, X)), Continuous (f ∘ g)) :
        Continuous[compactlyGenerated.{u} X, t] f

Proof state:
X : Type w
Y : Type x
inst✝ : TopologicalSpace X
t : TopologicalSpace Y
f : X → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)
⊢ Continuous
    (f ∘ fun x =>
      match x with
      | ⟨⟨fst, i⟩, s⟩ => i s)

Tactic:
continuity

Result:
no goals

Proof state:
X : Type w
Y : Type x
inst✝ : TopologicalSpace X
t : TopologicalSpace Y
f : X → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)
⊢ Continuous f

Tactic:
rw [continuous_coinduced_dom]

Result:
X : Type w
Y : Type x
inst✝ : TopologicalSpace X
t : TopologicalSpace Y
f : X → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)
⊢ Continuous
    (f ∘ fun x =>
      match x with
      | ⟨⟨fst, i⟩, s⟩ => i s)
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_eq_pi_iff_sbtw {p₁ p₂ p₃ : P} : ∡ p₁ p₂ p₃ = π ↔ Sbtw ℝ p₁ p₂ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ p₁ p₂ p₃ = ↑π ↔ Sbtw ℝ p₁ p₂ p₃

Tactic:
rw [oangle_eq_pi_iff_angle_eq_pi, angle_eq_pi_iff_sbtw]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem lt_inv_iff_mul_lt_one' : a < b⁻¹ ↔ b * a < 1 :=
  (mul_lt_mul_iff_left b).symm.trans <| by rw [mul_inv_cancel]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b : α
⊢ b * a < b * b⁻¹ ↔ b * a < 1

Tactic:
rw [mul_inv_cancel]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_sUnion {S : Set (Set α)} (hs : S.Countable) (hd : S.Pairwise Disjoint)
    (h : ∀ s ∈ S, MeasurableSet s) : μ (⋃₀ S) = ∑' s : S, μ s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hs : S.Countable
hd : S.Pairwise Disjoint
h : ∀ s ∈ S, MeasurableSet s
⊢ μ (⋃₀ S) = ∑' (s : ↑S), μ ↑s

Tactic:
rw [sUnion_eq_biUnion, measure_biUnion hs hd h]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem contDiff_infty_iff_deriv :
    ContDiff 𝕜 ∞ f₂ ↔ Differentiable 𝕜 f₂ ∧ ContDiff 𝕜 ∞ (deriv f₂)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
⊢ Differentiable 𝕜 f₂ ∧ (∞ = ω → AnalyticOn 𝕜 f₂ univ) ∧ ContDiff 𝕜 ∞ (deriv f₂) ↔
    Differentiable 𝕜 f₂ ∧ ContDiff 𝕜 (∞ + 1) (deriv f₂)

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
⊢ ContDiff 𝕜 ∞ f₂ ↔ Differentiable 𝕜 f₂ ∧ ContDiff 𝕜 ∞ (deriv f₂)

Tactic:
rw [show (∞ : WithTop ℕ∞) = ∞ + 1 from rfl, contDiff_succ_iff_deriv]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
⊢ Differentiable 𝕜 f₂ ∧ (∞ = ω → AnalyticOn 𝕜 f₂ univ) ∧ ContDiff 𝕜 ∞ (deriv f₂) ↔
    Differentiable 𝕜 f₂ ∧ ContDiff 𝕜 (∞ + 1) (deriv f₂)
-- Mathlib/CategoryTheory/Galois/Decomposition.lean
private lemma selfProdProj_fiber (x : F.obj X) :
    F.map (selfProdProj u x) a = x

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
x : (F.obj X).carrier
⊢ F.map (Pi.π (fun x => X) x) (CategoryTheory.PreGaloisCategory.mkSelfProdFib F X) = x

Tactic:
rw [mkSelfProdFib_map_π F X x]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
x : (F.obj X).carrier
⊢ F.map (CategoryTheory.PreGaloisCategory.selfProdProj u x) a = x

Tactic:
simp only [selfProdProj, selfProd, F.map_comp, FintypeCat.comp_apply, h]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
x : (F.obj X).carrier
⊢ F.map (Pi.π (fun x => X) x) (CategoryTheory.PreGaloisCategory.mkSelfProdFib F X) = x
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_add_right_smul_rotation_pi_div_two {x : V} (h : x ≠ 0) (r : ℝ) :
    Real.Angle.tan (o.oangle x (x + r • o.rotation (π / 2 : ℝ) x)) = r

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ (o.oangle x (x + r • (o.rotation ↑(π / 2)) x)).tan = r

Tactic:
rw [o.oangle_add_right_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_reverse {l : Vector α n} {f : Nat → α → β} :
    l.reverse.mapIdx f = (mapIdx (fun i => f (l.size - 1 - i)) l).reverse

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : Nat → α → β
⊢ mapIdx f l.reverse = (mapIdx (fun i => f (l.size - 1 - i)) l).reverse

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : Array α
⊢ mapIdx f { toArray := l, size_toArray := ⋯ }.reverse =
    (mapIdx (fun i => f ({ toArray := l, size_toArray := ⋯ }.size - 1 - i)) { toArray := l, size_toArray := ⋯ }).reverse

Proof state:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : Array α
⊢ mapIdx f { toArray := l, size_toArray := ⋯ }.reverse =
    (mapIdx (fun i => f ({ toArray := l, size_toArray := ⋯ }.size - 1 - i)) { toArray := l, size_toArray := ⋯ }).reverse

Tactic:
simp [Array.mapIdx_reverse]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.not_iff_comm [Decidable a] [Decidable b] : (¬a ↔ b) ↔ (¬b ↔ a)

Proof state:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (¬a ↔ b) ↔ (¬b ↔ a)

Tactic:
rw [@iff_def (¬a), @iff_def (¬b)]

Result:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (¬a → b) ∧ (b → ¬a) ↔ (¬b → a) ∧ (a → ¬b)

Proof state:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (¬a → b) ∧ (b → ¬a) ↔ (¬b → a) ∧ (a → ¬b)

Tactic:
exact and_congr not_imp_comm imp_not_comm

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem isUnit_fromBlocks_zero₁₂ {A : Matrix m m α} {C : Matrix n m α} {D : Matrix n n α} :
    IsUnit (fromBlocks A 0 C D) ↔ IsUnit A ∧ IsUnit D

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
⊢ IsUnit (fromBlocks A 0 C D) ↔ IsUnit A ∧ IsUnit D

Tactic:
simp only [← nonempty_invertible_iff_isUnit, ← nonempty_prod,
  (fromBlocksZero₁₂InvertibleEquiv _ _ _).nonempty_congr]

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Basic.lean
lemma eventually_exists_iff [Finite β] {P : β → α → Prop} :
    (∀ᶠ i in f, ∃ a, P a i) ↔ ∃ a, ∀ᶠ i in f, P a i

Proof state:
α : Type u
β : Type v
f : Ultrafilter α
inst✝ : Finite β
P : β → α → Prop
⊢ (∀ᶠ (i : α) in ↑f, ∃ a, P a i) ↔ ∃ a, ∀ᶠ (i : α) in ↑f, P a i

Tactic:
simpa using eventually_exists_mem_iff (f := f) (P := P) Set.finite_univ

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
theorem contMDiff_prod_module_iff (f : M → F₁ × F₂) :
    ContMDiff I 𝓘(𝕜, F₁ × F₂) n f ↔
      ContMDiff I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) ∧ ContMDiff I 𝓘(𝕜, F₂) n (Prod.snd ∘ f)

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiff I 𝓘(𝕜, F₁ × F₂) n f ↔ ContMDiff I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) ∧ ContMDiff I 𝓘(𝕜, F₂) n (Prod.snd ∘ f)

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

Result:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiff I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) n f ↔
    ContMDiff I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) ∧ ContMDiff I 𝓘(𝕜, F₂) n (Prod.snd ∘ f)

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiff I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) n f ↔
    ContMDiff I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) ∧ ContMDiff I 𝓘(𝕜, F₂) n (Prod.snd ∘ f)

Tactic:
exact contMDiff_prod_iff f

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma traceForm_cartan_nondegenerate
    [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] :
    (LieModule.traceForm R H L).Nondegenerate

Proof state:
R : Type u_1
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : IsKilling R L
inst✝² : IsNoetherian R L
inst✝¹ : IsArtinian R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
⊢ (LieModule.traceForm R (↥H) L).Nondegenerate

Tactic:
simp [LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem closedBall_eq_empty : closedBall x ε = ∅ ↔ ε < 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε = ∅ ↔ ε < 0

Tactic:
rw [← not_nonempty_iff_eq_empty, nonempty_closedBall, not_le]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Compare.lean
theorem card_zmod : Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n

Tactic:
rw [card, ZMod.card]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem not_isLeftDescent_one (i : B) : ¬cs.IsLeftDescent 1 i

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ ¬cs.IsLeftDescent 1 i

Tactic:
simp [IsLeftDescent]

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
@[simp] lemma mem_Ioc : x ∈ Ioc a b ↔ a < x ∧ x ≤ b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioc a b ↔ a < x ∧ x ≤ b

Tactic:
rw [Ioc, ← Finset.mem_def, Finset.mem_Ioc]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem comp_eqToHom_heq {C} [Category C] {X Y Z : C}
    (f : X ⟶ Y) (h : Y = Z) : HEq (f ≫ eqToHom h) f

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y Z : C
f : X ⟶ Y
h : Y = Z
⊢ HEq (f ≫ eqToHom h) f

Tactic:
rw [← conj_eqToHom_iff_heq' _ _ rfl h, eqToHom_refl, Category.id_comp]

Result:
no goals
-- Mathlib/Data/Complex/FiniteDimensional.lean
theorem Complex.nonempty_linearEquiv_real : Nonempty (ℂ ≃ₗ[ℚ] ℝ) :=
  LinearEquiv.nonempty_equiv_iff_rank_eq.mpr <| by simp

Proof state:
⊢ Module.rank ℚ ℂ = Module.rank ℚ ℝ

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem map_leftUnitor (X : C) :
    F.map (λ_ X).hom = δ F (𝟙_ C) X ≫ η F ▷ F.obj X ≫ (λ_ (F.obj X)).hom

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X : C
⊢ F.map (λ_ X).hom = δ F (𝟙_ C) X ≫ η F ▷ F.obj X ≫ (λ_ (F.obj X)).hom

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem FractionRing.p_nonzero [Nontrivial R] [CharP R p] : (p : FractionRing (𝕎 R)) ≠ 0

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
⊢ ↑p ≠ 0

Tactic:
simpa using (IsFractionRing.injective (𝕎 R) (FractionRing (𝕎 R))).ne (WittVector.p_nonzero _ _)

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem inner_eq_zero_iff_angle_eq_pi_div_two (x y : V) : ⟪x, y⟫ = 0 ↔ angle x y = π / 2 :=
  Iff.symm <| by simp +contextual [angle, or_imp]

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle x y = π / 2 ↔ inner x y = 0

Tactic:
simp +contextual [angle, or_imp]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem of_sub_rat (h : Irrational (x - q)) : Irrational x :=
  of_add_rat (-q) <| by simpa only [cast_neg, sub_eq_add_neg] using h

Proof state:
q : ℚ
x : ℝ
h : Irrational (x - ↑q)
⊢ Irrational (x + ↑(-q))

Tactic:
simpa only [cast_neg, sub_eq_add_neg] using h

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem coe_zeta_mul_coe_moebius [Ring R] : (ζ * μ : ArithmeticFunction R) = 1

Proof state:
R : Type u_1
inst✝ : Ring R
⊢ ↑ζ * ↑μ = 1

Tactic:
rw [← coe_coe, ← intCoe_mul, coe_zeta_mul_moebius, intCoe_one]

Result:
no goals
-- Mathlib/Data/Setoid/Basic.lean
theorem eqvGen_of_setoid (r : Setoid α) : EqvGen.setoid r.r = r :=
  le_antisymm (by rw [eqvGen_eq]; exact sInf_le fun _ _ => id) EqvGen.rel

Proof state:
α : Type u_1
r : Setoid α
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → s x y} ≤ r

Tactic:
exact sInf_le fun _ _ => id

Result:
no goals

Proof state:
α : Type u_1
r : Setoid α
⊢ EqvGen.setoid ⇑r ≤ r

Tactic:
rw [eqvGen_eq]

Result:
α : Type u_1
r : Setoid α
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → s x y} ≤ r
-- Mathlib/Data/Complex/Basic.lean
theorem I_mul_I : I * I = -1 :=
  Complex.ext_iff.2 <| by simp

Proof state:
⊢ (I * I).re = (-1).re ∧ (I * I).im = (-1).im

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Lax.lean
@[reassoc, to_app]
lemma map₂_leftUnitor_hom {a b : B} (f : a ⟶ b) :
    (λ_ (F.map f)).hom = F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f ≫ F.map₂ (λ_ f).hom

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : LaxFunctor B C
a b : B
f : a ⟶ b
⊢ (F.map₂Iso (λ_ f)).inv = (λ_ (F.map f)).inv ≫ F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f

Tactic:
simp only [Functor.mapIso_inv, PrelaxFunctor.mapFunctor_map, map₂_leftUnitor]

Result:
no goals

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : LaxFunctor B C
a b : B
f : a ⟶ b
⊢ (λ_ (F.map f)).hom = F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f ≫ F.map₂ (λ_ f).hom

Tactic:
rw [← PrelaxFunctor.map₂Iso_hom, ← assoc, ← Iso.comp_inv_eq, ← Iso.eq_inv_comp]

Result:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : LaxFunctor B C
a b : B
f : a ⟶ b
⊢ (F.map₂Iso (λ_ f)).inv = (λ_ (F.map f)).inv ≫ F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f
-- Mathlib/Topology/ContinuousOn.lean
theorem mem_closure_ne_iff_frequently_within {z : α} {s : Set α} :
    z ∈ closure (s \ {z}) ↔ ∃ᶠ x in 𝓝[≠] z, x ∈ s

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
z : α
s : Set α
⊢ z ∈ closure (s \ {z}) ↔ ∃ᶠ (x : α) in 𝓝[≠] z, x ∈ s

Tactic:
simp [mem_closure_iff_frequently, frequently_nhdsWithin_iff]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
theorem lift_unique (F : k[G] →ₐ[k] A) (f : MonoidAlgebra k G) :
    F f = f.sum fun a b => b • F (single a 1)

Proof state:
k : Type u₁
G : Type u₂
inst✝³ : CommSemiring k
inst✝² : AddMonoid G
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra k A
F : k[G] →ₐ[k] A
f : MonoidAlgebra k G
⊢ F f = sum f fun a b => b • F (single a 1)

Tactic:
conv_lhs =>
  rw [lift_unique' F]
  simp [lift_apply]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem comap_smul' (f : V →ₗ[K] V₂) (p : Submodule K V₂) (a : K) :
    p.comap (a • f) = ⨅ _ : a ≠ 0, p.comap f

Proof state:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

Tactic:
classical by_cases h : a = 0 <;> simp [h, comap_smul]

Result:
no goals

Proof state:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

Tactic:
by_cases h : a = 0 <;> simp [h, comap_smul]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem norm_sq_re_conj_add (x : K) : ‖conj x + x‖ ^ 2 = re (conj x + x) ^ 2

Proof state:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ ‖(starRingEnd K) x + x‖ ^ 2 = re ((starRingEnd K) x + x) ^ 2

Tactic:
rw [add_comm, norm_sq_re_add_conj]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biprod.lift_eq {T : C} {f : T ⟶ X} {g : T ⟶ Y} :
    biprod.lift f g = f ≫ biprod.inl + g ≫ biprod.inr

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g = f ≫ inl + g ≫ inr

Tactic:
ext <;> simp [add_comp]

Result:
no goals
-- Mathlib/Data/Set/Subsingleton.lean
theorem Nontrivial.ne_singleton {x} (hs : s.Nontrivial) : s ≠ {x} := fun H => by
  rw [H] at hs
  exact not_nontrivial_singleton hs

Proof state:
α : Type u
s : Set α
x : α
hs : s.Nontrivial
H : s = {x}
⊢ False

Tactic:
rw [H] at hs

Result:
α : Type u
s : Set α
x : α
hs : {x}.Nontrivial
H : s = {x}
⊢ False

Proof state:
α : Type u
s : Set α
x : α
hs : {x}.Nontrivial
H : s = {x}
⊢ False

Tactic:
exact not_nontrivial_singleton hs

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
@[simp]
lemma linearEquiv_apply [IsLocalizedModule S g] (x : M) :
    (linearEquiv S f g) (f x) = g x

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M''
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
x : M
⊢ (linearEquiv S f g) (f x) = g x

Tactic:
simp [linearEquiv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_erase [LawfulBEq α] (h : m.WF) {k a : α} {h'} :
    (m.erase a).get k h' = m.get k (mem_of_mem_erase h h')

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
h' : k ∈ m.erase a
⊢ (m.erase a).get k h' = m.get k ⋯

Tactic:
simp_to_raw using Raw₀.get_erase ⟨m, _⟩

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem Filter.Tendsto.neg_mul_atTop {C : 𝕜} (hC : C < 0) (hf : Tendsto f l (𝓝 C))
    (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atBot

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * g x) l atBot

Tactic:
simpa only [mul_comm] using hg.atTop_mul_neg hC hf

Result:
no goals
-- Mathlib/CategoryTheory/Localization/HomEquiv.lean
lemma homEquiv_eq (G : D₁ ⥤ D₂) (e : L₁ ⋙ G ≅ L₂) (f : L₁.obj X ⟶ L₁.obj Y) :
    homEquiv W L₁ L₂ f = e.inv.app X ≫ G.map f ≫ e.hom.app Y

Proof state:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{u_10, u_1} C
inst✝³ : Category.{u_8, u_5} D₁
inst✝² : Category.{u_9, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X Y : C
G : D₁ ⥤ D₂
e : L₁ ⋙ G ≅ L₂
f : L₁.obj X ⟶ L₁.obj Y
⊢ (homEquiv W L₁ L₂) f = e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
rw [homEquiv_apply, LocalizerMorphism.homMap_apply (LocalizerMorphism.id W) L₁ L₂ G e.symm,
  Iso.symm_hom, Iso.symm_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_modifyKey [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
    getKey! k' (modifyKey k f l) =
      if k == k' then
        if containsKey k l then k else default
      else
        getKey! k' l

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getKey! k' (modifyKey k f l) =
    if (k == k') = true then if containsKey k l = true then k else default else getKey! k' l

Tactic:
simp [modifyKey_eq_alterKey, getKey!_alterKey, containsKey_eq_isSome_getValueCast?, hl]

Result:
no goals
-- Mathlib/Topology/Instances/Sign.lean
theorem continuousAt_sign_of_pos {a : α} (h : 0 < a) : ContinuousAt SignType.sign a

Proof state:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ ContinuousAt (⇑SignType.sign) a

Tactic:
refine (continuousAt_const : ContinuousAt (fun _ => (1 : SignType)) a).congr ?_

Result:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ (fun x => 1) =ᶠ[nhds a] ⇑SignType.sign

Proof state:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ ∃ t, (∀ y ∈ t, 1 = SignType.sign y) ∧ IsOpen t ∧ a ∈ t

Tactic:
exact ⟨{ x | 0 < x }, fun x hx => (sign_pos hx).symm, isOpen_lt' 0, h⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ (fun x => 1) =ᶠ[nhds a] ⇑SignType.sign

Tactic:
rw [Filter.EventuallyEq, eventually_nhds_iff]

Result:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ ∃ t, (∀ y ∈ t, 1 = SignType.sign y) ∧ IsOpen t ∧ a ∈ t
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_ofReal_re (x : ℝ) : (log (x : ℂ)).re = Real.log x

Proof state:
x : ℝ
⊢ (log ↑x).re = Real.log x

Tactic:
simp [log_re]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalComp_nil_nil {f g h : C} (α : f ≅ g) (β : g ≅ h) :
    (α ≪≫ β).hom = (α ≪≫ β).hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
f g h : C
α : f ≅ g
β : g ≅ h
⊢ (α ≪≫ β).hom = (α ≪≫ β).hom

Tactic:
simp

Result:
no goals