harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_right_hasFDerivWithinAt_iff {f : F → G} {s : Set F} {x : E} {f' : F →L[𝕜] G} :
    HasFDerivWithinAt (f ∘ iso) (f'.comp (iso : E →L[𝕜] F)) (iso ⁻¹' s) x ↔
      HasFDerivWithinAt f f' s (iso x)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm
B : f' = (f'.comp ↑iso).comp ↑iso.symm
⊢ MapsTo (⇑iso.symm) s (⇑iso ⁻¹' s)

Tactic:
intro y hy

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm
B : f' = (f'.comp ↑iso).comp ↑iso.symm
y : F
hy : y ∈ s
⊢ iso.symm y ∈ ⇑iso ⁻¹' s

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
⊢ HasFDerivWithinAt f f' s (iso x)

Tactic:
have A : f = (f ∘ iso) ∘ iso.symm := by
  rw [Function.comp_assoc, iso.self_comp_symm]
  rfl

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm
⊢ HasFDerivWithinAt f f' s (iso x)
-- Mathlib/Algebra/Homology/Monoidal.lean
lemma rightUnitor'_inv_comm (i j : I) :
    (rightUnitor' K).inv i ≫ (tensorObj K (tensorUnit C c)).d i j =
      K.d i j ≫ (rightUnitor' K).inv j

Proof state:
case pos
C : Type u_1
inst✝⁹ : Category.{u_2, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i j : I
hij : c.Rel i j
⊢ (ρ_ (K.X i)).inv ≫
      K.X i ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫
        (1 • K.d i j ▷ (tensorUnit C c).X 0 ≫ K.ιMapBifunctor (tensorUnit C c) (curriedTensor C) c j 0 j ⋯) =
    K.d i j ≫ (ρ_ (K.X j)).inv ≫ K.X j ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ K.ιTensorObj (tensorUnit C c) j 0 j ⋯

Tactic:
simp only [one_smul, whisker_exchange_assoc,
  MonoidalCategory.whiskerRight_id, assoc, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem mem_rotate : ∀ {l : List α} {a : α} {n : ℕ}, a ∈ l.rotate n ↔ a ∈ l
  | [], _, n => by simp
  | a :: l, _, 0 => by simp
  | a :: l, _, n + 1 => by simp [rotate_cons_succ, mem_rotate, or_comm]

Proof state:
α : Type u
a : α
l : List α
x✝ : α
⊢ x✝ ∈ (a :: l).rotate 0 ↔ x✝ ∈ a :: l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
x✝ : α
n : ℕ
⊢ x✝ ∈ (a :: l).rotate (n + 1) ↔ x✝ ∈ a :: l

Tactic:
simp [rotate_cons_succ, mem_rotate, or_comm]

Result:
no goals

Proof state:
α : Type u
x✝ : α
n : ℕ
⊢ x✝ ∈ [].rotate n ↔ x✝ ∈ []

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem hasFDerivAt_comp_add_right (a : E) :
    HasFDerivAt (fun x ↦ f (x + a)) f' x ↔ HasFDerivAt f f' (x + a)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x a : E
⊢ HasFDerivAt (fun x => f (x + a)) f' x ↔ HasFDerivAt f f' (x + a)

Tactic:
simp [← hasFDerivWithinAt_univ, hasFDerivWithinAt_comp_add_right]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_insert [DecidableEq α] {a : α} {s : Set α} [Fintype (insert a s : Set α)]
    [Fintype s] : (insert a s).toFinset = insert a s.toFinset

Proof state:
α : Type u_1
inst✝² : DecidableEq α
a : α
s : Set α
inst✝¹ : Fintype ↑(insert a s)
inst✝ : Fintype ↑s
⊢ (insert a s).toFinset = insert a s.toFinset

Tactic:
ext

Result:
case h
α : Type u_1
inst✝² : DecidableEq α
a : α
s : Set α
inst✝¹ : Fintype ↑(insert a s)
inst✝ : Fintype ↑s
a✝ : α
⊢ a✝ ∈ (insert a s).toFinset ↔ a✝ ∈ insert a s.toFinset

Proof state:
case h
α : Type u_1
inst✝² : DecidableEq α
a : α
s : Set α
inst✝¹ : Fintype ↑(insert a s)
inst✝ : Fintype ↑s
a✝ : α
⊢ a✝ ∈ (insert a s).toFinset ↔ a✝ ∈ insert a s.toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem threeAPFree_sphere : ThreeAPFree (sphere n d k : Set (Fin n → ℕ))

Proof state:
n d k : ℕ
⊢ ThreeAPFree ↑(sphere n d k)

Tactic:
set f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toFun := fun f => ((↑) : ℕ → ℝ) ∘ f
    map_zero' := funext fun _ => cast_zero
    map_add' := fun _ _ => funext fun _ => cast_add _ _ }

Result:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f => Nat.cast ∘ f, map_zero' := ⋯, map_add' := ⋯ }
⊢ ThreeAPFree ↑(sphere n d k)

Proof state:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f => Nat.cast ∘ f, map_zero' := ⋯, map_add' := ⋯ }
x : Fin n → ℕ
⊢ x ∈ ↑(sphere n d k) → ‖f x‖ = √↑k

Tactic:
exact norm_of_mem_sphere

Result:
no goals

Proof state:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f => Nat.cast ∘ f, map_zero' := ⋯, map_add' := ⋯ }
x : Fin n → ℕ
⊢ x ∈ ↑(sphere n d k) → x ∈ ⇑f ⁻¹' Metric.sphere 0 √↑k

Tactic:
rw [Set.mem_preimage, mem_sphere_zero_iff_norm]

Result:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f => Nat.cast ∘ f, map_zero' := ⋯, map_add' := ⋯ }
x : Fin n → ℕ
⊢ x ∈ ↑(sphere n d k) → ‖f x‖ = √↑k

Proof state:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f => Nat.cast ∘ f, map_zero' := ⋯, map_add' := ⋯ }
⊢ ThreeAPFree (⇑f '' ↑(sphere n d k))

Tactic:
refine (threeAPFree_sphere 0 (√↑k)).mono (Set.image_subset_iff.2 fun x => ?_)

Result:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f => Nat.cast ∘ f, map_zero' := ⋯, map_add' := ⋯ }
x : Fin n → ℕ
⊢ x ∈ ↑(sphere n d k) → x ∈ ⇑f ⁻¹' Metric.sphere 0 √↑k

Proof state:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f => Nat.cast ∘ f, map_zero' := ⋯, map_add' := ⋯ }
⊢ ThreeAPFree ↑(sphere n d k)

Tactic:
refine ThreeAPFree.of_image (AddMonoidHomClass.isAddFreimanHom f (Set.mapsTo_image _ _))
  cast_injective.comp_left.injOn (Set.subset_univ _) ?_

Result:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f => Nat.cast ∘ f, map_zero' := ⋯, map_add' := ⋯ }
⊢ ThreeAPFree (⇑f '' ↑(sphere n d k))
-- Mathlib/NumberTheory/Divisors.lean
lemma ne_zero_of_mem_divisorsAntidiagonal {p : ℕ × ℕ} (hp : p ∈ n.divisorsAntidiagonal) :
    p.1 ≠ 0 ∧ p.2 ≠ 0

Proof state:
case intro
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 * p.2 = n
hp₂ : n ≠ 0
⊢ p.1 ≠ 0 ∧ p.2 ≠ 0

Tactic:
exact mul_ne_zero_iff.mp (hp₁.symm ▸ hp₂)

Result:
no goals

Proof state:
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ p.1 ≠ 0 ∧ p.2 ≠ 0

Tactic:
obtain ⟨hp₁, hp₂⟩ := Nat.mem_divisorsAntidiagonal.mp hp

Result:
case intro
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 * p.2 = n
hp₂ : n ≠ 0
⊢ p.1 ≠ 0 ∧ p.2 ≠ 0
-- Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean
theorem smul_ne_zero_iff : c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
⊢ c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0

Tactic:
rw [Ne, smul_eq_zero, not_or]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_singleton_group_smul_eq {G} [Group G] [SMul G R] [MulAction G M] [IsScalarTower G R M]
    (g : G) (x : M) : (R ∙ g • x) = R ∙ x

Proof state:
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_9
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
g : G
x : M
⊢ span R {x} ≤ span R {g • x}

Tactic:
convert span_singleton_smul_le R g⁻¹ (g • x)

Result:
case h.e'_3.h.e'_6.h.e'_4
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_9
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
g : G
x : M
⊢ x = g⁻¹ • g • x

Proof state:
case h.e'_3.h.e'_6.h.e'_4
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_9
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
g : G
x : M
⊢ x = g⁻¹ • g • x

Tactic:
exact (inv_smul_smul g x).symm

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_9
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
g : G
x : M
⊢ span R {g • x} = span R {x}

Tactic:
refine le_antisymm (span_singleton_smul_le R g x) ?_

Result:
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_9
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
g : G
x : M
⊢ span R {x} ≤ span R {g • x}
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_const_cpow' {a b : ℂ} (h : b ≠ 0) : ContinuousAt (fun x : ℂ => a ^ x) b

Proof state:
case pos
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt 0 b

Tactic:
exact continuousAt_const

Result:
no goals

Proof state:
case neg
a b : ℂ
h : b ≠ 0
ha : ¬a = 0
⊢ ContinuousAt (fun x => a ^ x) b

Tactic:
exact continuousAt_const_cpow ha

Result:
no goals

Proof state:
case pos
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (fun x => a ^ x) b

Tactic:
rw [ha, continuousAt_congr (zero_cpow_eq_nhds h)]

Result:
case pos
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt 0 b

Proof state:
a b : ℂ
h : b ≠ 0
⊢ ContinuousAt (fun x => a ^ x) b

Tactic:
by_cases ha : a = 0

Result:
case pos
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (fun x => a ^ x) b

case neg
a b : ℂ
h : b ≠ 0
ha : ¬a = 0
⊢ ContinuousAt (fun x => a ^ x) b
-- Mathlib/Data/NNRat/Defs.lean
lemma divNat_mul_divNat (n₁ n₂ : ℕ) {d₁ d₂} (hd₁ : d₁ ≠ 0) (hd₂ : d₂ ≠ 0) :
    divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂)

Proof state:
case a
n₁ n₂ d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
⊢ ↑(divNat n₁ d₁ * divNat n₂ d₂) = ↑(divNat (n₁ * n₂) (d₁ * d₂))

Tactic:
push_cast

Result:
case a
n₁ n₂ d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
⊢ Rat.divInt ↑n₁ ↑d₁ * Rat.divInt ↑n₂ ↑d₂ = Rat.divInt (↑n₁ * ↑n₂) (↑d₁ * ↑d₂)

Proof state:
n₁ n₂ d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
⊢ divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂)

Tactic:
ext

Result:
case a
n₁ n₂ d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
⊢ ↑(divNat n₁ d₁ * divNat n₂ d₂) = ↑(divNat (n₁ * n₂) (d₁ * d₂))

Proof state:
case a
n₁ n₂ d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
⊢ Rat.divInt ↑n₁ ↑d₁ * Rat.divInt ↑n₂ ↑d₂ = Rat.divInt (↑n₁ * ↑n₂) (↑d₁ * ↑d₂)

Tactic:
exact Rat.divInt_mul_divInt _ _ (mod_cast hd₁) (mod_cast hd₂)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem integrableOn_Ioi_norm_cpow_of_lt {a : ℂ} (ha : a.re < -1) {c : ℝ} (hc : 0 < c) :
    IntegrableOn (fun t : ℝ ↦ ‖(t : ℂ) ^ a‖) (Ioi c)

Proof state:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ioi c
⊢ x ^ a.re = ‖↑x ^ a‖

Tactic:
rw [Complex.norm_cpow_eq_rpow_re_of_pos (hc.trans hx)]

Result:
no goals

Proof state:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ IntegrableOn (fun t => ‖↑t ^ a‖) (Ioi c) volume

Tactic:
refine (integrableOn_Ioi_rpow_of_lt ha hc).congr_fun (fun x hx => ?_) measurableSet_Ioi

Result:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ioi c
⊢ x ^ a.re = ‖↑x ^ a‖
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem inv_inj {f : M →* N} (hf : ∀ y : S, IsUnit (f y)) {y z : S}
    (h : (IsUnit.liftRight (f.restrict S) hf y)⁻¹ = (IsUnit.liftRight (f.restrict S) hf z)⁻¹) :
      f y = f z

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (y : ↥S), IsUnit (f ↑y)
y z : ↥S
h : ((IsUnit.liftRight (f.restrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.restrict S) hf) z)⁻¹
⊢ f ↑y = f ↑z

Tactic:
rw [← mul_one (f y), eq_comm, ← mul_inv_left hf y (f z) 1, h]

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (y : ↥S), IsUnit (f ↑y)
y z : ↥S
h : ((IsUnit.liftRight (f.restrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.restrict S) hf) z)⁻¹
⊢ f ↑z * ↑((IsUnit.liftRight (f.restrict S) hf) z)⁻¹ = 1

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (y : ↥S), IsUnit (f ↑y)
y z : ↥S
h : ((IsUnit.liftRight (f.restrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.restrict S) hf) z)⁻¹
⊢ f ↑z * ↑((IsUnit.liftRight (f.restrict S) hf) z)⁻¹ = 1

Tactic:
exact Units.inv_mul (IsUnit.liftRight (f.restrict S) hf z)⁻¹

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_le_zero_iff {x : PGame} : -x ≤ 0 ↔ 0 ≤ x

Proof state:
x : PGame
⊢ -x ≤ 0 ↔ 0 ≤ x

Tactic:
rw [neg_le_iff, neg_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_add (hx : 0 < x) (y z : ℝ) : x ^ (y + z) = x ^ y * x ^ z

Proof state:
x : ℝ
hx : 0 < x
y z : ℝ
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
simp only [rpow_def_of_pos hx, mul_add, exp_add]

Result:
no goals
-- Mathlib/Topology/Algebra/GroupWithZero.lean
theorem HasContinuousInv₀.of_nhds_one (h : Tendsto Inv.inv (𝓝 (1 : G₀)) (𝓝 1)) :
    HasContinuousInv₀ G₀ where
  continuousAt_inv₀ x hx

Proof state:
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ ContinuousAt Inv.inv x

Tactic:
rw [ContinuousAt, ← map_mul_left_nhds_one₀ hx, ← nhds_translation_mul_inv₀ hx',
  tendsto_map'_iff, tendsto_comap_iff]

Result:
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ Tendsto ((fun x_1 => x_1 * x⁻¹⁻¹) ∘ Inv.inv ∘ fun x_1 => x * x_1) (𝓝 1) (𝓝 1)

Proof state:
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
⊢ ContinuousAt Inv.inv x

Tactic:
have hx' := inv_ne_zero hx

Result:
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ ContinuousAt Inv.inv x

Proof state:
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ Tendsto ((fun x_1 => x_1 * x⁻¹⁻¹) ∘ Inv.inv ∘ fun x_1 => x * x_1) (𝓝 1) (𝓝 1)

Tactic:
simpa only [Function.comp_def, mul_inv_rev, mul_inv_cancel_right₀ hx']

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.size_deleteMin_lt {s : Heap α} (eq : s.deleteMin le = some (a, s')) :
    s'.size < s.size

Proof state:
case node.refl
α : Type u_1
le : α → α → Bool
a : α
c sibling✝ : Heap α
⊢ (combine le c).size < (node a c sibling✝).size

Tactic:
simp_arith [size_combine, size]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
a : α
s' s : Heap α
eq : deleteMin le s = some (a, s')
⊢ s'.size < s.size

Tactic:
cases s with cases eq | node a c => simp_arith [size_combine, size]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Logic.lean
theorem congrArg₂ (f : α → β → γ) {x x' : α} {y y' : β}
    (hx : x = x') (hy : y = y') : f x y = f x' y'

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β → γ
x : α
y : β
⊢ f x y = f x y

Tactic:
rfl

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β → γ
x x' : α
y y' : β
hx : x = x'
hy : y = y'
⊢ f x y = f x' y'

Tactic:
subst hx hy

Result:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β → γ
x : α
y : β
⊢ f x y = f x y
-- Mathlib/RingTheory/Valuation/RankOne.lean
theorem unit_ne_one : unit v ≠ 1

Proof state:
R : Type u_1
inst✝² : Ring R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.RankOne
⊢ ¬↑(unit v) = 1

Tactic:
exact ((nontrivial v).choose_spec ).2

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Ring R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.RankOne
⊢ unit v ≠ 1

Tactic:
rw [Ne, ← Units.eq_iff, Units.val_one]

Result:
R : Type u_1
inst✝² : Ring R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.RankOne
⊢ ¬↑(unit v) = 1
-- Mathlib/Data/Finset/Fold.lean
theorem fold_op_rel_iff_or {r : β → β → Prop} (hr : ∀ {x y z}, r x (op y z) ↔ r x y ∨ r x z)
    {c : β} : r c (s.fold op b f) ↔ r c b ∨ ∃ x ∈ s, r c (f x)

Proof state:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ (r c b ∨ r c (f a) ∨ ∃ x ∈ s, r c (f x)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)

Tactic:
apply or_congr Iff.rfl

Result:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ (r c (f a) ∨ ∃ x ∈ s, r c (f x)) ↔ ∃ x ∈ insert a s, r c (f x)

Proof state:
case insert.mp.inl
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
h₁ : r c (f a)
⊢ ∃ x ∈ insert a s, r c (f x)

Tactic:
use a

Result:
case h
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
h₁ : r c (f a)
⊢ a ∈ insert a s ∧ r c (f a)
-- Mathlib/Data/Part.lean
theorem bind_map {γ} (f : α → β) (x) (g : β → Part γ) :
    (map f x).bind g = x.bind fun y => g (f y)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (map f x).bind g = x.bind fun y => g (f y)

Tactic:
rw [← bind_some_eq_map, bind_assoc]

Result:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (x.bind fun x => (some (f x)).bind g) = x.bind fun y => g (f y)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (x.bind fun x => (some (f x)).bind g) = x.bind fun y => g (f y)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
/-- A set is stable under generalization iff it is an intersection of open sets. -/
lemma stableUnderGeneralization_iff_exists_sInter_eq {s : Set X} :
    StableUnderGeneralization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderGeneralization s ↔ ∃ S, (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s

Tactic:
refine ⟨?_, fun ⟨S, hS, e⟩ ↦ e ▸
  stableUnderGeneralization_sInter S (fun x hx ↦ (hS x hx).stableUnderGeneralization)⟩

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderGeneralization s → ∃ S, (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderGeneralization s → ∃ S, (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s

Tactic:
rw [← stableUnderSpecialization_compl_iff, stableUnderSpecialization_iff_exists_sUnion_eq]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ s ∈ S, IsClosed s) ∧ ⋃₀ S = sᶜ) → ∃ S, (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_le_diam (s : Set ℝ) : volume s ≤ EMetric.diam s

Proof state:
s : Set ℝ
⊢ volume s ≤ EMetric.diam s

Tactic:
by_cases hs : Bornology.IsBounded s

Result:
case pos
s : Set ℝ
hs : Bornology.IsBounded s
⊢ volume s ≤ EMetric.diam s

case neg
s : Set ℝ
hs : ¬Bornology.IsBounded s
⊢ volume s ≤ EMetric.diam s

Proof state:
case neg
s : Set ℝ
hs : ¬Bornology.IsBounded s
⊢ volume s ≤ EMetric.diam s

Tactic:
rw [Metric.ediam_of_unbounded hs]

Result:
case neg
s : Set ℝ
hs : ¬Bornology.IsBounded s
⊢ volume s ≤ ⊤

Proof state:
case pos
s : Set ℝ
hs : Bornology.IsBounded s
⊢ volume s ≤ volume (Icc (sInf s) (sSup s))

Tactic:
exact volume.mono hs.subset_Icc_sInf_sSup

Result:
no goals

Proof state:
case pos
s : Set ℝ
hs : Bornology.IsBounded s
⊢ volume s ≤ EMetric.diam s

Tactic:
rw [Real.ediam_eq hs, ← volume_Icc]

Result:
case pos
s : Set ℝ
hs : Bornology.IsBounded s
⊢ volume s ≤ volume (Icc (sInf s) (sSup s))

Proof state:
case neg
s : Set ℝ
hs : ¬Bornology.IsBounded s
⊢ volume s ≤ ⊤

Tactic:
exact le_top

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem exists_eq_right_right : (∃ (a : α), p a ∧ q a ∧ a = a') ↔ p a' ∧ q a'

Proof state:
α : Sort u_1
p q : α → Prop
a' : α
⊢ (∃ a, p a ∧ q a ∧ a = a') ↔ p a' ∧ q a'

Tactic:
simp [← and_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
lemma setLIntegral_le_meas {s t : Set α} (hs : MeasurableSet s)
    {f : α → ℝ≥0∞} (hf : ∀ a ∈ s, a ∈ t → f a ≤ 1)
    (hf' : ∀ a ∈ s, a ∉ t → f a = 0) : ∫⁻ a in s, f a ∂μ ≤ μ t

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
⊢ ∫⁻ (a : α), s.indicator f a ∂μ ≤ μ t

Tactic:
refine lintegral_le_meas (fun a ↦ ?_) (by aesop)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
⊢ s.indicator f a ≤ 1

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ μ t

Tactic:
rw [← lintegral_indicator hs]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
⊢ ∫⁻ (a : α), s.indicator f a ∂μ ≤ μ t

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
⊢ ∀ a ∈ tᶜ, s.indicator f a = 0

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
⊢ s.indicator f a ≤ 1

Tactic:
by_cases has : a ∈ s <;> [by_cases hat : a ∈ t; skip] <;> simp [*]

Result:
no goals