harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem symm_trans_source_eq (e e' : Pretrivialization F proj) :
    (e.toPartialEquiv.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ univ

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
⊢ (e.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ univ

Tactic:
rw [PartialEquiv.trans_source, e'.source_eq, PartialEquiv.symm_source, e.target_eq, inter_comm,
  e.preimage_symm_proj_inter, inter_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean
lemma iff_of_isAffine [IsAffine X] [IsAffine Y] :
    SurjectiveOnStalks f ↔ RingHom.SurjectiveOnStalks (f.app ⊤).hom

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ SurjectiveOnStalks f ↔ (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)).SurjectiveOnStalks

Tactic:
rw [← Spec_iff, MorphismProperty.arrow_mk_iso_iff @SurjectiveOnStalks (arrowIsoSpecΓOfIsAffine f)]

Result:
no goals
-- Mathlib/Data/Finset/Disjoint.lean
theorem disjoint_iff_ne : Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b

Proof state:
α : Type u_1
s t : Finset α
⊢ Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b

Tactic:
simp only [disjoint_left, imp_not_comm, forall_eq']

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_ne_zero_iff {x : ℝ} : sin x ≠ 0 ↔ ∀ n : ℤ, (n : ℝ) * π ≠ x

Proof state:
x : ℝ
⊢ sin x ≠ 0 ↔ ∀ (n : ℤ), ↑n * π ≠ x

Tactic:
rw [← not_exists, not_iff_not, sin_eq_zero_iff]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem areaForm_rightAngleRotation_right (x y : E) : ω x (J y) = ⟪x, y⟫

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.areaForm x) (o.rightAngleRotation y) = inner x y

Tactic:
rw [← o.inner_rightAngleRotation_left, o.inner_comp_rightAngleRotation]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem card_toMultiset (s : Cycle α) : Multiset.card s.toMultiset = s.length :=
  Quotient.inductionOn' s (by simp)

Proof state:
α : Type u_1
s : Cycle α
⊢ ∀ (a : List α), (toMultiset (Quotient.mk'' a)).card = length (Quotient.mk'' a)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem add_one (n : PosNum) : n + 1 = succ n

Proof state:
n : PosNum
⊢ n + 1 = n.succ

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
theorem biprod.map_lift_mapBiprod (f : W ⟶ X) (g : W ⟶ Y) :
    F.map (biprod.lift f g) ≫ (F.mapBiprod X Y).hom = biprod.lift (F.map f) (F.map g)

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ F.map (lift f g) ≫ (F.mapBiprod X Y).hom = lift (F.map f) (F.map g)

Tactic:
ext <;> simp [mapBiprod, ← F.map_comp]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem continuous_sup_dom {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} :
    Continuous[t₁ ⊔ t₂, t₃] f ↔ Continuous[t₁, t₃] f ∧ Continuous[t₂, t₃] f

Proof state:
α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
⊢ Continuous f ↔ Continuous f ∧ Continuous f

Tactic:
simp only [continuous_iff_le_induced, sup_le_iff]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean
@[reassoc (attr := simp)]
lemma mappingConeCompHomotopyEquiv_hom_inv_id :
    (mappingConeCompHomotopyEquiv f g).hom ≫
      (mappingConeCompHomotopyEquiv f g).inv = 𝟙 _

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ (mappingConeCompHomotopyEquiv f g).hom ≫ (mappingConeCompHomotopyEquiv f g).inv = 𝟙 (mappingCone g)

Tactic:
simp [mappingConeCompHomotopyEquiv]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem LeftInverse.preimage_preimage {g : β → α} (h : LeftInverse g f) (s : Set α) :
    f ⁻¹' (g ⁻¹' s) = s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ f ⁻¹' (g ⁻¹' s) = s

Tactic:
rw [← preimage_comp, h.comp_eq_id, preimage_id]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_restrict_biUnion_finset_iff (s : ι → Set α) (t : Finset ι) (p : α → Prop) :
    (∀ᵐ x ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ x ∂μ.restrict (s i), p x

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Finset ι
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x

Tactic:
simp_rw [Filter.Eventually, ae_restrict_biUnion_finset_eq s, mem_iSup]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_not : eval .not = ((~~~ ·) : BitVec w → BitVec w)

Proof state:
w : Nat
⊢ not.eval = fun x => ~~~x

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_sub_two (n : ℤ) : U R (n - 2) = 2 * X * U R (n - 1) - U R n

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R (n - 2) = 2 * X * U R (n - 1) - U R n

Tactic:
linear_combination (norm := ring_nf) U_add_two R (n - 2)

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_pos [StrictOrderedSemiring α] (hx : 0 ≤ x) (hn : n ≠ 0) :
    0 < ∑ i ∈ range n, x ^ i :=
  sum_pos' (fun _ _ => pow_nonneg hx _) ⟨0, mem_range.2 hn.bot_lt, by simp⟩

Proof state:
α : Type u
n : ℕ
x : α
inst✝ : StrictOrderedSemiring α
hx : 0 ≤ x
hn : n ≠ 0
⊢ 0 < x ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
theorem commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_left
    {i₂ : ZMod 2} (hm₁ : m₁ ∈ evenOdd Q₁ 0) (hm₂ : m₂ ∈ evenOdd Q₂ i₂) :
    Commute (map f₁ m₁) (map f₂ m₂) :=
  (map_mul_map_of_isOrtho_of_mem_evenOdd _ _ hf _ _ hm₁ hm₂).trans <| by simp

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₂ : ZMod 2
hm₁ : m₁ ∈ evenOdd Q₁ 0
hm₂ : m₂ ∈ evenOdd Q₂ i₂
⊢ (-1) ^ (i₂ * 0) • ((map f₂) m₂ * (map f₁) m₁) = (map f₂) m₂ * (map f₁) m₁

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem same_sub_div {a b : K} (h : b ≠ 0) : (b - a) / b = 1 - a / b

Proof state:
K : Type u_1
inst✝ : DivisionRing K
a b : K
h : b ≠ 0
⊢ (b - a) / b = 1 - a / b

Tactic:
simpa only [← @div_self _ _ b h] using (div_sub_div_same b a b).symm

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem multipliable_iff_tprod_vanishing : Multipliable f ↔
    ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t : Set β, Disjoint t s → (∏' b : t, f b) ∈ e

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
f : β → α
inst✝ : CompleteSpace α
⊢ Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_tprod_vanishing]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldr_loop_zero (f : Fin n → α → α) (x) :
    foldr.loop n f 0 (Nat.zero_le _) x = x

Proof state:
n : Nat
α : Sort u_1
f : Fin n → α → α
x : α
⊢ foldr.loop n f 0 ⋯ x = x

Tactic:
rw [foldr.loop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_le_count_push (a b : α) (l : Array α) : count a l ≤ count a (l.push b)

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l : Array α
⊢ count a l ≤ count a (l.push b)

Tactic:
simp [count_push]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem toSubgraph_map (f : G →g G') (p : G.Walk u v) :
    (p.map f).toSubgraph = p.toSubgraph.map f

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
p : G.Walk u v
⊢ (Walk.map f p).toSubgraph = Subgraph.map f p.toSubgraph

Tactic:
induction p <;> simp [*, Subgraph.map_sup]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem symm_self_id_assoc (α : X ≅ Y) (β : Y ≅ Z) : α.symm ≪≫ α ≪≫ β = β

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
⊢ α.symm ≪≫ α ≪≫ β = β

Tactic:
rw [← trans_assoc, symm_self_id, refl_trans]

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem prod_zero : (0 : PrimeMultiset).prod = 1

Proof state:
⊢ prod 0 = 1

Tactic:
exact Multiset.prod_zero

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_eq_one_of_forall_eq_one {f : α → M} {s : Set α} (h : ∀ x ∈ s, f x = 1) :
    ∏ᶠ i ∈ s, f i = 1

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

Tactic:
simp +contextual [h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zeroIsoIsInitial_inv {X : C} (t : IsInitial X) : (zeroIsoIsInitial t).inv = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsInitial X
⊢ (zeroIsoIsInitial t).inv = 0

Tactic:
ext

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
lemma measurable_cylinderEvents_iff {g : α → ∀ i, π i} :
    @Measurable _ _ _ (cylinderEvents Δ) g ↔ ∀ ⦃i⦄, i ∈ Δ → Measurable fun a ↦ g a i

Proof state:
α : Type u_1
ι : Type u_2
π : ι → Type u_3
mα : MeasurableSpace α
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
g : α → (i : ι) → π i
⊢ Measurable g ↔ ∀ ⦃i : ι⦄, i ∈ Δ → Measurable fun a => g a i

Tactic:
simp_rw [measurable_iff_comap_le, cylinderEvents, MeasurableSpace.comap_iSup,
  MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem coeff_root (h : IsAdjoinRootMonic S f) (hdeg : 1 < natDegree f) :
    h.coeff h.root = Pi.single 1 1

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
hdeg : 1 < f.natDegree
⊢ h.coeff h.root = Pi.single 1 1

Tactic:
rw [← h.coeff_root_pow hdeg, pow_one]

Result:
no goals
-- Mathlib/Algebra/Module/BigOperators.lean
theorem Finset.cast_card [CommSemiring R] (s : Finset α) : (#s : R) = ∑ _ ∈ s, 1

Proof state:
α : Type u_3
R : Type u_5
inst✝ : CommSemiring R
s : Finset α
⊢ ↑(#s) = ∑ x ∈ s, 1

Tactic:
rw [Finset.sum_const, Nat.smul_one_eq_cast]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
theorem biprod.mapBiprod_hom_desc (f : X ⟶ W) (g : Y ⟶ W) :
    (F.mapBiprod X Y).hom ≫ biprod.desc (F.map f) (F.map g) = F.map (biprod.desc f g)

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ (F.mapBiprod X Y).hom ≫ desc (F.map f) (F.map g) = F.map (desc f g)

Tactic:
rw [← biprod.mapBiprod_inv_map_desc, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Cardinality.lean
theorem cardinalMk_le : #(OreLocalization S R) ≤ #R

Proof state:
R : Type u
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
⊢ #(OreLocalization S R) ≤ #R

Tactic:
convert ← cardinalMk_le_max S R

Result:
case h.e'_4
R : Type u
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
⊢ lift.{u, u} #↥S ⊔ lift.{u, u} #R = #R

Proof state:
case h.e'_4
R : Type u
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
⊢ lift.{u, u} #↥S ⊔ lift.{u, u} #R = #R

Tactic:
simp_rw [lift_id, max_eq_right_iff, mk_subtype_le]

Result:
no goals
-- Mathlib/Data/Rat/Sqrt.lean
theorem sqrt_eq (q : ℚ) : Rat.sqrt (q * q) = |q|

Proof state:
q : ℚ
⊢ sqrt (q * q) = |q|

Tactic:
rw [sqrt, mul_self_num, mul_self_den, Int.sqrt_eq, Nat.sqrt_eq, abs_def, divInt_ofNat]

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
lemma skewAdjointPart_eq_I_smul_imaginaryPart (x : A) :
    (skewAdjointPart ℝ x : A) = I • (imaginaryPart x : A)

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
⊢ ↑((skewAdjointPart ℝ) x) = I • ↑(ℑ x)

Tactic:
simp [imaginaryPart_apply_coe, smul_smul]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Diam.lean
theorem diam_insert : diam (insert x s) = max (⨆ y ∈ s, edist x y) (diam s) :=
  eq_of_forall_ge_iff fun d => by
    simp only [diam_le_iff, forall_mem_insert, edist_self, edist_comm x, max_le_iff, iSup_le_iff,
      zero_le, true_and, forall_and, and_self_iff, ← and_assoc]

Proof state:
α : Type u_1
s : Set α
x : α
inst✝ : PseudoEMetricSpace α
d : ℝ≥0∞
⊢ diam (insert x s) ≤ d ↔ (⨆ y ∈ s, edist x y) ⊔ diam s ≤ d

Tactic:
simp only [diam_le_iff, forall_mem_insert, edist_self, edist_comm x, max_le_iff, iSup_le_iff,
  zero_le, true_and, forall_and, and_self_iff, ← and_assoc]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem two_zsmul_oangle_neg_self_right (x : V) : (2 : ℤ) • o.oangle x (-x) = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ 2 • o.oangle x (-x) = 0

Tactic:
by_cases hx : x = 0 <;> simp [hx]

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem _root_.LieHom.range_eq_map : f.range = map f ⊤

Proof state:
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x✝ : L₂
⊢ x✝ ∈ f.range ↔ x✝ ∈ map f ⊤

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
⊢ f.range = map f ⊤

Tactic:
ext

Result:
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x✝ : L₂
⊢ x✝ ∈ f.range ↔ x✝ ∈ map f ⊤
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem neg_sub {X Y : C} (a b : X ⟶ Y) : -a - b = -b - a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ -a - b = -b - a

Tactic:
conv_lhs => rw [neg_def, ← sub_zero b, sub_sub_sub, sub_zero, ← neg_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_extract : eval assign (.extract start len expr) = BitVec.extractLsb' start len (eval assign expr)

Proof state:
assign : Assignment
start len a✝ : Nat
expr : BVExpr a✝
⊢ eval assign (extract start len expr) = BitVec.extractLsb' start len (eval assign expr)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem measurePreserving_div_right (μ : Measure G) [IsMulRightInvariant μ] (g : G) :
    MeasurePreserving (· / g) μ μ

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ MeasurePreserving (fun x => x / g) μ μ

Tactic:
simp_rw [div_eq_mul_inv, measurePreserving_mul_right μ g⁻¹]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.le_of_eq_1 (u v : Nat) : u = v → u ≤ v

Proof state:
u v : Nat
⊢ u = v → u ≤ v

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem isCauSeq_re (f : CauSeq K norm) : IsCauSeq abs fun n => re (f n) := fun _ ε0 =>
  (f.cauchy ε0).imp fun i H j ij =>
    lt_of_le_of_lt (by simpa only [map_sub] using abs_re_le_norm (f j - f i)) (H _ ij)

Proof state:
K : Type u_1
inst✝ : RCLike K
f : CauSeq K norm
x✝ : ℝ
ε0 : x✝ > 0
i : ℕ
H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < x✝
j : ℕ
ij : j ≥ i
⊢ |(fun n => re (↑f n)) j - (fun n => re (↑f n)) i| ≤ ‖↑f j - ↑f i‖

Tactic:
simpa only [map_sub] using abs_re_le_norm (f j - f i)

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_neg_set_eq_gauge_neg (x : E) : gauge (-s) x = gauge s (-x)

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
⊢ gauge (-s) x = gauge s (-x)

Tactic:
rw [← gauge_neg_set_neg, neg_neg]

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem iSup_iInf_of_monotone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [Nonempty ι']
    [IsDirected ι' (· ≤ ·)] [Order.Frame α] {f : ι → ι' → α} (hf : ∀ i, Monotone (f i)) :
    ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j

Proof state:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝⁴ : Finite ι
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x1 x2 => x1 ≤ x2
inst✝ : Order.Frame α
f : ι → ι' → α
hf : ∀ (i : ι), Monotone (f i)
⊢ ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j

Tactic:
simpa only [iInf_univ] using finite_univ.iSup_biInf_of_monotone fun i _ => hf i

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem b_ne_one : b ≠ 1

Proof state:
b : ℝ
b_lt_one : b < 1
⊢ b ≠ 1

Tactic:
linarith

Result:
no goals
-- Mathlib/Data/Holor.lean
theorem drop_take : ∀ t : HolorIndex (ds₁ ++ ds₂ ++ ds₃), t.assocRight.drop.take = t.take.drop
  | ⟨is, h⟩ => Subtype.eq (by simp [assocRight, take, drop, cast_type, List.drop_take])

Proof state:
ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun x1 x2 => x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)
⊢ ↑(assocRight ⟨is, h⟩).drop.take = ↑(take ⟨is, h⟩).drop

Tactic:
simp [assocRight, take, drop, cast_type, List.drop_take]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/LinearMap.lean
theorem ContinuousLinearMap.reApplyInnerSelf_smul (T : E →L[𝕜] E) (x : E) {c : 𝕜} :
    T.reApplyInnerSelf (c • x) = ‖c‖ ^ 2 * T.reApplyInnerSelf x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
⊢ T.reApplyInnerSelf (c • x) = ‖c‖ ^ 2 * T.reApplyInnerSelf x

Tactic:
simp only [ContinuousLinearMap.map_smul, ContinuousLinearMap.reApplyInnerSelf_apply,
  inner_smul_left, inner_smul_right, ← mul_assoc, mul_conj, ← ofReal_pow, ← smul_re,
  Algebra.smul_def (‖c‖ ^ 2) ⟪T x, x⟫, algebraMap_eq_ofReal]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem over_right (U : Over X) : U.right = ⟨⟨⟩⟩

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U : Over X
⊢ U.right = { as := PUnit.unit }

Tactic:
simp only

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_sInf_le (h : μ ∈ m) : sInf m ≤ μ :=
  have : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure := sInf_le (mem_image_of_mem _ h)
  le_iff.2 fun s hs => by rw [sInf_apply hs]; exact this s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure
s : Set α
hs : MeasurableSet s
⊢ (sInf (toOuterMeasure '' m)) s ≤ μ s

Tactic:
exact this s

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure
s : Set α
hs : MeasurableSet s
⊢ (sInf m) s ≤ μ s

Tactic:
rw [sInf_apply hs]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure
s : Set α
hs : MeasurableSet s
⊢ (sInf (toOuterMeasure '' m)) s ≤ μ s
-- Mathlib/Analysis/RCLike/Basic.lean
@[simp, rclike_simps, norm_cast]
lemma nnnorm_nnratCast (q : ℚ≥0) : ‖(q : K)‖₊ = q

Proof state:
K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ ‖↑q‖₊ = ↑q

Tactic:
simp [nnnorm]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma _root_.MonotoneOn.mapsTo_uIcc (hf : MonotoneOn f (uIcc a b)) :
    MapsTo f (uIcc a b) (uIcc (f a) (f b))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]

Tactic:
rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf] <;>
  apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
lemma le_egauge_closedBall_one (x : E) : ‖x‖ₑ ≤ egauge 𝕜 (closedBall 0 1) x

Proof state:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ‖x‖ₑ ≤ egauge 𝕜 (closedBall 0 1) x

Tactic:
simpa using div_le_egauge_closedBall 𝕜 1 x

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
@[simp, norm_cast] lemma coe_eq_one : (r : ℝ) = 1 ↔ r = 1

Proof state:
r : ℝ≥0
⊢ ↑r = 1 ↔ r = 1

Tactic:
rw [← coe_one, coe_inj]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_comp_linearIsometryEquiv (φ : E ≃ₗᵢ[ℝ] E)
    (hφ : 0 < LinearMap.det (φ.toLinearEquiv : E →ₗ[ℝ] E)) (x y : E) :
    o.kahler (φ x) (φ y) = o.kahler x y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ (o.kahler (φ x)) (φ y) = (o.kahler x) y

Tactic:
simp [kahler_apply_apply, o.areaForm_comp_linearIsometryEquiv φ hφ]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
@[simp]
lemma linearEquiv_symm_apply [IsLocalizedModule S g] (x : M) :
    (linearEquiv S f g).symm (g x) = f 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).symm (g x) = f x

Tactic:
simp [linearEquiv]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem closure_prod_eq {s : Set X} {t : Set Y} : closure (s ×ˢ t) = closure s ×ˢ closure t :=
  ext fun ⟨a, b⟩ => by
    simp_rw [mem_prod, mem_closure_iff_nhdsWithin_neBot, nhdsWithin_prod_eq, prod_neBot]

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
x✝ : X × Y
a : X
b : Y
⊢ (a, b) ∈ closure (s ×ˢ t) ↔ (a, b) ∈ closure s ×ˢ closure t

Tactic:
simp_rw [mem_prod, mem_closure_iff_nhdsWithin_neBot, nhdsWithin_prod_eq, prod_neBot]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Tendsto.lean
theorem tendsto_atTop_embedding [Preorder β] [Preorder γ] {f : α → β} {e : β → γ} {l : Filter α}
    (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ c, ∃ b, c ≤ e b) :
    Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
e : β → γ
l : Filter α
hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂
hu : ∀ (c : γ), ∃ b, c ≤ e b
⊢ Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop

Tactic:
rw [← comap_embedding_atTop hm hu, tendsto_comap_iff]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem headI_mul_tail_prod_of_ne_nil [Inhabited M] (l : List M) (h : l ≠ []) :
    l.headI * l.tail.prod = l.prod

Proof state:
M : Type u_4
inst✝¹ : Monoid M
inst✝ : Inhabited M
l : List M
h : l ≠ []
⊢ l.headI * l.tail.prod = l.prod

Tactic:
cases l <;> [contradiction; simp]

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem pointReflection_symm (x : P) : (pointReflection x).symm = pointReflection x :=
  ext <| by simp [pointReflection]

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x : P
⊢ ∀ (x_1 : P), (Equiv.symm (pointReflection x)) x_1 = (pointReflection x) x_1

Tactic:
simp [pointReflection]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem mem_segment_translate (a : E) {x b c} : a + x ∈ [a + b -[𝕜] a + c] ↔ x ∈ [b -[𝕜] c]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a x b c : E
⊢ a + x ∈ [a + b-[𝕜]a + c] ↔ x ∈ [b-[𝕜]c]

Tactic:
simp_rw [← vadd_eq_add, ← vadd_segment, vadd_mem_vadd_set_iff]

Result:
no goals