harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Localization/Bousfield.lean
lemma W_adj_unit_app (X : D) : W (· ∈ Set.range F.obj) (adj.unit.app X)

Proof state:
case h.e'_3.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
Y : C
e_1✝ : ((G ⋙ F).obj X ⟶ F.obj Y) = (F.obj (G.obj X) ⟶ F.obj Y)
e_2✝ : ((𝟭 D).obj X ⟶ F.obj Y) = (X ⟶ F.obj Y)
⊢ (fun g => adj.unit.app X ≫ g) =
    (fun f => adj.unit.app X ≫ F.map f) ∘ ⇑(Functor.FullyFaithful.ofFullyFaithful F).homEquiv.symm

Tactic:
aesop

Result:
no goals

Proof state:
case intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
Y : C
⊢ Function.Bijective fun g => adj.unit.app X ≫ g

Tactic:
convert ((Functor.FullyFaithful.ofFullyFaithful F).homEquiv.symm.trans
  (adj.homEquiv X Y)).bijective using 1

Result:
case h.e'_3.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
Y : C
e_1✝ : ((G ⋙ F).obj X ⟶ F.obj Y) = (F.obj (G.obj X) ⟶ F.obj Y)
e_2✝ : ((𝟭 D).obj X ⟶ F.obj Y) = (X ⟶ F.obj Y)
⊢ (fun g => adj.unit.app X ≫ g) = ⇑((Functor.FullyFaithful.ofFullyFaithful F).homEquiv.symm.trans (adj.homEquiv X Y))

Proof state:
case h.e'_3.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
Y : C
e_1✝ : ((G ⋙ F).obj X ⟶ F.obj Y) = (F.obj (G.obj X) ⟶ F.obj Y)
e_2✝ : ((𝟭 D).obj X ⟶ F.obj Y) = (X ⟶ F.obj Y)
⊢ (fun g => adj.unit.app X ≫ g) = ⇑((Functor.FullyFaithful.ofFullyFaithful F).homEquiv.symm.trans (adj.homEquiv X Y))

Tactic:
dsimp [Adjunction.homEquiv]

Result:
case h.e'_3.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
Y : C
e_1✝ : ((G ⋙ F).obj X ⟶ F.obj Y) = (F.obj (G.obj X) ⟶ F.obj Y)
e_2✝ : ((𝟭 D).obj X ⟶ F.obj Y) = (X ⟶ F.obj Y)
⊢ (fun g => adj.unit.app X ≫ g) =
    (fun f => adj.unit.app X ≫ F.map f) ∘ ⇑(Functor.FullyFaithful.ofFullyFaithful F).homEquiv.symm

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
⊢ W (fun x => x ∈ Set.range F.obj) (adj.unit.app X)

Tactic:
rintro _ ⟨Y, rfl⟩

Result:
case intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
Y : C
⊢ Function.Bijective fun g => adj.unit.app X ≫ g
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_eq_guard_findIdx_lt {xs : Array α} {p : α → Bool} :
    xs.findIdx? p = Option.guard (fun i => i < xs.size) (xs.findIdx p)

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ findIdx? p xs = Option.guard (fun i => i < xs.size) (findIdx p xs)

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx? p { toList := xs } = Option.guard (fun i => i < { toList := xs }.size) (findIdx p { toList := xs })

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx? p { toList := xs } = Option.guard (fun i => i < { toList := xs }.size) (findIdx p { toList := xs })

Tactic:
simp [List.findIdx?_eq_guard_findIdx_lt]

Result:
no goals
-- Mathlib/GroupTheory/Submonoid/Inverses.lean
theorem leftInv_leftInv_le : S.leftInv.leftInv ≤ S

Proof state:
case intro.mk.intro
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x ∈ S

Tactic:
convert z.prop

Result:
case h.e'_5
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x = ↑z

Proof state:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
⊢ S.leftInv.leftInv ≤ S

Tactic:
rintro x ⟨⟨y, z, h₁⟩, h₂ : x * y = 1⟩

Result:
case intro.mk.intro
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x ∈ S

Proof state:
case h.e'_5
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x = ↑z

Tactic:
rw [← mul_one x, ← h₁, ← mul_assoc, h₂, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findSome?_isSome_iff {f : α → Option β} {l : List α} :
    (l.findSome? f).isSome ↔ ∃ x, x ∈ l ∧ (f x).isSome

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih : (findSome? f xs).isSome = true ↔ ∃ x, x ∈ xs ∧ (f x).isSome = true
⊢ (match f x with
        | some b => some b
        | none => findSome? f xs).isSome =
      true ↔
    ∃ x_1, x_1 ∈ x :: xs ∧ (f x_1).isSome = true

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih : (findSome? f xs).isSome = true ↔ ∃ x, x ∈ xs ∧ (f x).isSome = true
⊢ (findSome? f (x :: xs)).isSome = true ↔ ∃ x_1, x_1 ∈ x :: xs ∧ (f x_1).isSome = true

Tactic:
simp only [findSome?_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih : (findSome? f xs).isSome = true ↔ ∃ x, x ∈ xs ∧ (f x).isSome = true
⊢ (match f x with
        | some b => some b
        | none => findSome? f xs).isSome =
      true ↔
    ∃ x_1, x_1 ∈ x :: xs ∧ (f x_1).isSome = true

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ (findSome? f l).isSome = true ↔ ∃ x, x ∈ l ∧ (f x).isSome = true

Tactic:
induction l with
| nil => simp
| cons x xs ih =>
  simp only [findSome?_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → Option β
⊢ (findSome? f []).isSome = true ↔ ∃ x, x ∈ [] ∧ (f x).isSome = true

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Maps/Proper/Basic.lean
theorem Continuous.isProperMap [CompactSpace X] [T2Space Y] (hf : Continuous f) : IsProperMap f :=
  isProperMap_iff_isClosedMap_and_tendsto_cofinite.2 ⟨hf, hf.isClosedMap, by simp⟩

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
hf : Continuous f
⊢ Tendsto f (cocompact X) cofinite

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_le_inv₀ (ha : 0 < a) : 1 ≤ a⁻¹ ↔ a ≤ 1

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha : 0 < a
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
simpa using one_le_inv_mul₀ ha (b := 1)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_eq_false_of_containsKey [BEq α] {l : List ((a : α) × β a)} {a : α}
    (h : containsKey a l = true) : l.isEmpty = false

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
a : α
h : containsKey a l = true
⊢ l.isEmpty = false

Tactic:
cases l <;> simp_all

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem map_eq_bot_iff_le_ker {I : Ideal R} (f : F) : I.map f = ⊥ ↔ I ≤ RingHom.ker f

Proof state:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
I : Ideal R
f : F
⊢ map f I = ⊥ ↔ I ≤ RingHom.ker f

Tactic:
rw [RingHom.ker, eq_bot_iff, map_le_iff_le_comap]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem PInfty_comp_QInfty : (PInfty : K[X] ⟶ _) ≫ QInfty = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty ≫ QInfty = 0

Tactic:
ext n

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (PInfty ≫ QInfty).f n = HomologicalComplex.Hom.f 0 n

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (PInfty ≫ QInfty).f n = HomologicalComplex.Hom.f 0 n

Tactic:
apply PInfty_f_comp_QInfty_f

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mdifferentiableAt_prod_iff (f : M → M' × N') :
    MDifferentiableAt I (I'.prod J') f x ↔
      MDifferentiableAt I I' (Prod.fst ∘ f) x ∧ MDifferentiableAt I J' (Prod.snd ∘ f) x

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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
x : M
f : M → M' × N'
⊢ MDifferentiableWithinAt I (I'.prod J') f univ x ↔
    MDifferentiableWithinAt I I' (Prod.fst ∘ f) univ x ∧ MDifferentiableWithinAt I J' (Prod.snd ∘ f) univ x

Tactic:
exact mdifferentiableWithinAt_prod_iff f

Result:
no goals

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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
x : M
f : M → M' × N'
⊢ MDifferentiableAt I (I'.prod J') f x ↔
    MDifferentiableAt I I' (Prod.fst ∘ f) x ∧ MDifferentiableAt I J' (Prod.snd ∘ f) x

Tactic:
simp_rw [← mdifferentiableWithinAt_univ]

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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
x : M
f : M → M' × N'
⊢ MDifferentiableWithinAt I (I'.prod J') f univ x ↔
    MDifferentiableWithinAt I I' (Prod.fst ∘ f) univ x ∧ MDifferentiableWithinAt I J' (Prod.snd ∘ f) univ x
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_zero' : IsBigOWith 0 l (fun _x => (0 : E')) g :=
  IsBigOWith.of_bound <| univ_mem' fun x => by simp

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
x : α
⊢ x ∈ {x | (fun x => ‖0‖ ≤ 0 * ‖g x‖) x}

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_mul_const_Ioo (a b : α) {c : α} (h : 0 < c) :
    (fun x => x * c) ⁻¹' Ioo a b = Ioo (a / c) (b / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : 0 < c
⊢ (fun x => x * c) ⁻¹' Ioo a b = Ioo (a / c) (b / c)

Tactic:
simp [← Ioi_inter_Iio, h]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
lemma val_awayMap (a) : (awayMap 𝒜 hg hx a).val = Localization.awayLift (algebraMap A _) _
    (isUnit_of_dvd_unit (map_dvd _ ⟨_, hx⟩) (IsLocalization.Away.algebraMap_isUnit x)) a.val

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : Away 𝒜 f
⊢ val ((awayMap 𝒜 hg hx) a) = (Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯) (val a)

Tactic:
rw [val_awayMap_eq_aux]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : Away 𝒜 f
⊢ (HomogeneousLocalization.awayMapAux 𝒜 ⋯) a =
    (Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯) (val a)

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : Away 𝒜 f
⊢ (HomogeneousLocalization.awayMapAux 𝒜 ⋯) a =
    (Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯) (val a)

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem prodPrimeFactors [CommMonoidWithZero R] (f : ℕ → R) :
    IsMultiplicative (prodPrimeFactors f)

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hxy : x.Coprime y
hxy₀ : x * y ≠ 0
⊢ (ArithmeticFunction.prodPrimeFactors f) (x * y) =
    (ArithmeticFunction.prodPrimeFactors f) x * (ArithmeticFunction.prodPrimeFactors f) y

Tactic:
rw [prodPrimeFactors_apply hxy₀, prodPrimeFactors_apply hx, prodPrimeFactors_apply hy,
  Nat.primeFactors_mul hx hy, ← Finset.prod_union hxy.disjoint_primeFactors]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
⊢ ∀ {m n : ℕ},
    ¬m = 0 →
      ¬n = 0 →
        m.Coprime n →
          (ArithmeticFunction.prodPrimeFactors f) (m * n) =
            (ArithmeticFunction.prodPrimeFactors f) m * (ArithmeticFunction.prodPrimeFactors f) n

Tactic:
intro x y hx hy hxy

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hxy : x.Coprime y
⊢ (ArithmeticFunction.prodPrimeFactors f) (x * y) =
    (ArithmeticFunction.prodPrimeFactors f) x * (ArithmeticFunction.prodPrimeFactors f) y

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
⊢ (ArithmeticFunction.prodPrimeFactors f).IsMultiplicative

Tactic:
rw [iff_ne_zero]

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
⊢ (ArithmeticFunction.prodPrimeFactors f) 1 = 1 ∧
    ∀ {m n : ℕ},
      m ≠ 0 →
        n ≠ 0 →
          m.Coprime n →
            (ArithmeticFunction.prodPrimeFactors f) (m * n) =
              (ArithmeticFunction.prodPrimeFactors f) m * (ArithmeticFunction.prodPrimeFactors f) n

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
⊢ (ArithmeticFunction.prodPrimeFactors f) 1 = 1 ∧
    ∀ {m n : ℕ},
      m ≠ 0 →
        n ≠ 0 →
          m.Coprime n →
            (ArithmeticFunction.prodPrimeFactors f) (m * n) =
              (ArithmeticFunction.prodPrimeFactors f) m * (ArithmeticFunction.prodPrimeFactors f) n

Tactic:
simp only [ne_eq, one_ne_zero, not_false_eq_true, prodPrimeFactors_apply, primeFactors_one,
  prod_empty, true_and]

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
⊢ ∀ {m n : ℕ},
    ¬m = 0 →
      ¬n = 0 →
        m.Coprime n →
          (ArithmeticFunction.prodPrimeFactors f) (m * n) =
            (ArithmeticFunction.prodPrimeFactors f) m * (ArithmeticFunction.prodPrimeFactors f) n

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hxy : x.Coprime y
⊢ (ArithmeticFunction.prodPrimeFactors f) (x * y) =
    (ArithmeticFunction.prodPrimeFactors f) x * (ArithmeticFunction.prodPrimeFactors f) y

Tactic:
have hxy₀ : x * y ≠ 0 := mul_ne_zero hx hy

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hxy : x.Coprime y
hxy₀ : x * y ≠ 0
⊢ (ArithmeticFunction.prodPrimeFactors f) (x * y) =
    (ArithmeticFunction.prodPrimeFactors f) x * (ArithmeticFunction.prodPrimeFactors f) y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_mkVector_of_length_pos (h : 0 < n) :
    find? p (mkVector n a) = if p a then some a else none

Proof state:
n : Nat
α✝ : Type
p : α✝ → Bool
a : α✝
h : 0 < n
⊢ find? p (mkVector n a) = if p a = true then some a else none

Tactic:
simp [find?_mkVector, Nat.ne_of_gt h]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/EpiMono.lean
theorem reflectsMonomorphisms.of_iso {F G : C ⥤ D} [ReflectsMonomorphisms F] (α : F ≅ G) :
    ReflectsMonomorphisms G :=
  { reflects := fun {X} {Y} f h => by
      apply F.mono_of_mono_map
      suffices F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv from this ▸ mono_comp _ _
      rw [← Category.assoc, Iso.eq_comp_inv, Iso.app_hom, Iso.app_hom, NatTrans.naturality] }

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.ReflectsMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
⊢ Mono f

Tactic:
apply F.mono_of_mono_map

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.ReflectsMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
⊢ Mono (F.map f)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.ReflectsMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
⊢ Mono (F.map f)

Tactic:
suffices F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv from this ▸ mono_comp _ _

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.ReflectsMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
⊢ F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.ReflectsMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
⊢ F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv

Tactic:
rw [← Category.assoc, Iso.eq_comp_inv, Iso.app_hom, Iso.app_hom, NatTrans.naturality]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
lemma abs_sin_half (x : ℝ) : |sin (x / 2)| = sqrt ((1 - cos x) / 2)

Proof state:
x : ℝ
⊢ |sin (x / 2)| = √((1 - cos x) / 2)

Tactic:
rw [← sqrt_sq_eq_abs, sin_sq_eq_half_sub, two_mul, add_halves, sub_div]

Result:
no goals
-- Mathlib/Topology/Algebra/ClopenNhdofOne.lean
theorem exist_openNormalSubgroup_sub_clopen_nhd_of_one {G : Type*} [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) (einW : 1 ∈ W) :
    ∃ H : OpenNormalSubgroup G, (H : Set G) ⊆ W

Proof state:
case intro
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
H : OpenSubgroup G
hH : ↑H ⊆ W
this : (↑H).FiniteIndex
⊢ ∃ H, ↑H ⊆ W

Tactic:
use { toSubgroup := Subgroup.normalCore H
      isOpen' := Subgroup.isOpen_of_isClosed_of_finiteIndex _ (H.normalCore_isClosed H.isClosed) }

Result:
case h
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
H : OpenSubgroup G
hH : ↑H ⊆ W
this : (↑H).FiniteIndex
⊢ ↑{ toSubgroup := (↑H).normalCore, isOpen' := ⋯, isNormal' := ⋯ } ⊆ W

Proof state:
case intro
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
H : OpenSubgroup G
hH : ↑H ⊆ W
⊢ ∃ H, ↑H ⊆ W

Tactic:
have : Subgroup.FiniteIndex H.toSubgroup := H.finiteIndex_of_finite_quotient

Result:
case intro
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
H : OpenSubgroup G
hH : ↑H ⊆ W
this : (↑H).FiniteIndex
⊢ ∃ H, ↑H ⊆ W

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
⊢ ∃ H, ↑H ⊆ W

Tactic:
rcases exist_openSubgroup_sub_clopen_nhd_of_one WClopen einW with ⟨H, hH⟩

Result:
case intro
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
H : OpenSubgroup G
hH : ↑H ⊆ W
⊢ ∃ H, ↑H ⊆ W

Proof state:
case h
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
H : OpenSubgroup G
hH : ↑H ⊆ W
this : (↑H).FiniteIndex
⊢ ↑{ toSubgroup := (↑H).normalCore, isOpen' := ⋯, isNormal' := ⋯ } ⊆ W

Tactic:
exact fun _ b ↦ hH (H.normalCore_le b)

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem optionCasesOn_right {o : α → Option β} {f : α → σ} {g : α → β →. σ} (ho : Computable o)
    (hf : Computable f) (hg : Partrec₂ g) :
    @Partrec _ σ _ _ fun a => Option.casesOn (o a) (Part.some (f a)) (g a) :=
  have :
    Partrec fun a : α =>
      Nat.casesOn (encode (o a)) (Part.some (f a)) (fun n => Part.bind (decode (α := β) n) (g a)) :=
    nat_casesOn_right (h := fun a n ↦ Part.bind (ofOption (decode n)) fun b ↦ g a b)
      (encode_iff.2 ho) hf.partrec <|
        ((@Computable.decode β _).comp snd).ofOption.bind (hg.comp (fst.comp fst) snd).to₂
  this.of_eq fun a => by rcases o a with - | b <;> simp [encodek]

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a => Nat.casesOn (encode (o a)) (Part.some (f a)) fun n => (↑(decode n)).bind (g a)
a : α
⊢ (Nat.casesOn (encode (o a)) (Part.some (f a)) fun n => (↑(decode n)).bind (g a)) =
    Option.casesOn (o a) (Part.some (f a)) (g a)

Tactic:
rcases o a with - | b <;> simp [encodek]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.slt_eq_ult (x y : BitVec w) :
    x.slt y = ((!x.getLsbD (w - 1) == y.getLsbD (w - 1)) ^^ x.ult y)

Proof state:
w : Nat
x y : BitVec w
⊢ x.slt y = (!x.getLsbD (w - 1) == y.getLsbD (w - 1) ^^ x.ult y)

Tactic:
simp [_root_.BitVec.slt_eq_ult, BitVec.msb_eq_getLsbD_last, Bool.bne_to_beq]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_nonpos_iff_neg_imp_nonneg : a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
rw [← neg_nonneg, ← neg_smul, smul_nonneg_iff_pos_imp_nonneg]

Result:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
simp only [neg_pos, neg_nonneg]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem coe_iInf {ι : Sort*} {S : ι → NonUnitalStarSubalgebra R A} :
    (↑(⨅ i, S i) : Set A) = ⋂ i, S i

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
ι : Sort u_1
S : ι → NonUnitalStarSubalgebra R A
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp [iInf]

Result:
no goals