harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Group/CompactOpen.lean
@[to_additive]
lemma range_toContinuousMap :
    Set.range (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) =
      {f : C(A, B) | f 1 = 1 ∧ ∀ x y, f (x * y) = f x * f y}

Proof state:
case intro
A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
f : C(A, B)
h1 : f 1 = 1
hmul : ∀ (x y : A), f (x * y) = f x * f y
⊢ f ∈ Set.range toContinuousMap

Tactic:
exact ⟨{ f with map_one' := h1, map_mul' := hmul }, rfl⟩

Result:
no goals

Proof state:
A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ {f | f 1 = 1 ∧ ∀ (x y : A), f (x * y) = f x * f y} ⊆ Set.range toContinuousMap

Tactic:
rintro f ⟨h1, hmul⟩

Result:
case intro
A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
f : C(A, B)
h1 : f 1 = 1
hmul : ∀ (x y : A), f (x * y) = f x * f y
⊢ f ∈ Set.range toContinuousMap

Proof state:
A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ Set.range toContinuousMap = {f | f 1 = 1 ∧ ∀ (x y : A), f (x * y) = f x * f y}

Tactic:
refine Set.Subset.antisymm (Set.range_subset_iff.2 fun f ↦ ⟨map_one f, map_mul f⟩) ?_

Result:
A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ {f | f 1 = 1 ∧ ∀ (x y : A), f (x * y) = f x * f y} ⊆ Set.range toContinuousMap
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem mem_ker {r} : r ∈ ker f ↔ f r = 0

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rcf : RingHomClass F R S
f : F
r : R
⊢ r ∈ ker f ↔ f r = 0

Tactic:
rw [ker, Ideal.mem_comap, Submodule.mem_bot]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
theorem IicSnd_apply (r : ℝ) {s : Set α} (hs : MeasurableSet s) :
    ρ.IicSnd r s = ρ (s ×ˢ Iic r)

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℝ
s : Set α
hs : MeasurableSet s
⊢ (ρ.IicSnd r) s = ρ (s ×ˢ Iic r)

Tactic:
rw [IicSnd, fst_apply hs, restrict_apply' (MeasurableSet.univ.prod measurableSet_Iic),
  univ_prod, Set.prod_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem Sheaf.Hom.mono_iff_presheaf_mono {F G : Sheaf J D} (f : F ⟶ G) : Mono f ↔ Mono f.1 :=
  ⟨fun m => by infer_instance, fun m => by exact Sheaf.Hom.mono_of_presheaf_mono J D f⟩

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
F G : Sheaf J D
f : F ⟶ G
m : Mono f.val
⊢ Mono f

Tactic:
exact Sheaf.Hom.mono_of_presheaf_mono J D f

Result:
no goals

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
F G : Sheaf J D
f : F ⟶ G
m : Mono f
⊢ Mono f.val

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Compare.lean
theorem compare_eq_eq {a b : Nat} : compare a b = .eq ↔ a = b

Proof state:
case isFalse.isFalse
a b : Nat
h✝¹ : ¬a < b
h✝ : ¬b < a
⊢ a = b

Tactic:
next hlt hgt => exact Nat.le_antisymm (Nat.not_lt.1 hgt) (Nat.not_lt.1 hlt)

Result:
no goals

Proof state:
a b : Nat
⊢ compare a b = Ordering.eq ↔ a = b

Tactic:
rw [compare_def_lt]

Result:
a b : Nat
⊢ (if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq) = Ordering.eq ↔ a = b

Proof state:
case isFalse
a b : Nat
h✝ : ¬a < b
⊢ (if b < a then Ordering.gt else Ordering.eq) = Ordering.eq ↔ a = b

Tactic:
split

Result:
case isFalse.isTrue
a b : Nat
h✝¹ : ¬a < b
h✝ : b < a
⊢ Ordering.gt = Ordering.eq ↔ a = b

case isFalse.isFalse
a b : Nat
h✝¹ : ¬a < b
h✝ : ¬b < a
⊢ Ordering.eq = Ordering.eq ↔ a = b

Proof state:
a b : Nat
⊢ (if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq) = Ordering.eq ↔ a = b

Tactic:
repeat' split

Result:
case isTrue
a b : Nat
h✝ : a < b
⊢ Ordering.lt = Ordering.eq ↔ a = b

case isFalse.isTrue
a b : Nat
h✝¹ : ¬a < b
h✝ : b < a
⊢ Ordering.gt = Ordering.eq ↔ a = b

case isFalse.isFalse
a b : Nat
h✝¹ : ¬a < b
h✝ : ¬b < a
⊢ Ordering.eq = Ordering.eq ↔ a = b

Proof state:
a b : Nat
hlt : ¬a < b
hgt : ¬b < a
⊢ a = b

Tactic:
exact Nat.le_antisymm (Nat.not_lt.1 hgt) (Nat.not_lt.1 hlt)

Result:
no goals

Proof state:
a b : Nat
⊢ (if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq) = Ordering.eq ↔ a = b

Tactic:
(repeat' split) <;> simp [Nat.ne_of_lt, Nat.ne_of_gt, *]

Result:
case isFalse.isFalse
a b : Nat
h✝¹ : ¬a < b
h✝ : ¬b < a
⊢ a = b
-- Mathlib/Algebra/Regular/SMul.lean
theorem pow_iff {n : ℕ} (n0 : 0 < n) : IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a

Proof state:
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n.pred • a) → IsSMulRegular M a

Tactic:
exact of_smul _

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a

Tactic:
refine ⟨?_, pow n⟩

Result:
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) → IsSMulRegular M a

Proof state:
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) → IsSMulRegular M a

Tactic:
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ, ← smul_eq_mul]

Result:
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n.pred • a) → IsSMulRegular M a
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem isLittleO_exp_comp_exp_comp {f g : α → ℝ} :
    ((fun x => exp (f x)) =o[l] fun x => exp (g x)) ↔ Tendsto (fun x => g x - f x) l atTop

Proof state:
α : Type u_1
l : Filter α
f g : α → ℝ
⊢ ((fun x => rexp (f x)) =o[l] fun x => rexp (g x)) ↔ Tendsto (fun x => g x - f x) l atTop

Tactic:
simp only [isLittleO_iff_tendsto, exp_ne_zero, ← exp_sub, ← tendsto_neg_atTop_iff, false_imp_iff,
  imp_true_iff, tendsto_exp_comp_nhds_zero, neg_sub]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem oreDiv_mul_char (r₁ r₂ : R) (s₁ s₂ : S) (r' : R) (s' : S) (huv : s' * r₁ = r' * s₂) :
    r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : ↑s' * r₁ = r' * ↑s₂
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)

Tactic:
exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : ↑s' * r₁ = r' * ↑s₂
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)

Tactic:
with_unfolding_all exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem lookup_replicate_self_of_pos {a : α} (h : 0 < n) :
    (replicate n (a, b)).lookup a = some b

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
α✝ : Type u_1
b : α✝
a : α
h : 0 < n
⊢ lookup a (replicate n (a, b)) = some b

Tactic:
simp [lookup_replicate_self, Nat.ne_of_gt h]

Result:
no goals
-- Mathlib/FieldTheory/Galois/Basic.lean
lemma fixingSubgroup_anti : Antitone (IntermediateField.fixingSubgroup (F := F) (E := E))

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K K' : IntermediateField F E
h : K ≤ K'
⊢ K ≤ fixedField K'.fixingSubgroup

Tactic:
exact le_trans h ((le_iff_le _ _).mpr (le_refl K'.fixingSubgroup))

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K K' : IntermediateField F E
h : K ≤ K'
⊢ K'.fixingSubgroup ≤ K.fixingSubgroup

Tactic:
rw [← le_iff_le]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K K' : IntermediateField F E
h : K ≤ K'
⊢ K ≤ fixedField K'.fixingSubgroup

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ Antitone fixingSubgroup

Tactic:
intro K K' h

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K K' : IntermediateField F E
h : K ≤ K'
⊢ K'.fixingSubgroup ≤ K.fixingSubgroup
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_attach_biUnion [DecidableEq M] {α : Type*} (s : Finset α) (f : s → Finset M) :
    span R (s.attach.biUnion f : Set M) = ⨆ x, span R (f x)

Proof state:
R : Type u_1
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq M
α : Type u_9
s : Finset α
f : { x // x ∈ s } → Finset M
⊢ span R ↑(s.attach.biUnion f) = ⨆ x, span R ↑(f x)

Tactic:
simp [span_iUnion]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem add_right_eq_self {x y : BitVec w} : x + y = x ↔ y = 0#w

Proof state:
w : Nat
x y : BitVec w
⊢ y + x = x ↔ y = 0#w

Tactic:
exact BitVec.add_left_eq_self

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x + y = x ↔ y = 0#w

Tactic:
rw [BitVec.add_comm]

Result:
w : Nat
x y : BitVec w
⊢ y + x = x ↔ y = 0#w
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma rpow_natCast (a : A) (n : ℕ) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
n : ℕ
ha : autoParam (0 ≤ a) _auto✝
⊢ cfc (fun x => x ^ ↑n) a = cfc (fun x => x ^ n) a

Tactic:
congr

Result:
case e_f
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
n : ℕ
ha : autoParam (0 ≤ a) _auto✝
⊢ (fun x => x ^ ↑n) = fun x => x ^ n

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
n : ℕ
ha : autoParam (0 ≤ a) _auto✝
⊢ a ^ ↑n = a ^ n

Tactic:
rw [← cfc_pow_id (R := ℝ≥0) a n, rpow_def]

Result:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
n : ℕ
ha : autoParam (0 ≤ a) _auto✝
⊢ cfc (fun x => x ^ ↑n) a = cfc (fun x => x ^ n) a

Proof state:
case e_f
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
n : ℕ
ha : autoParam (0 ≤ a) _auto✝
⊢ (fun x => x ^ ↑n) = fun x => x ^ n

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem eq_empty (v : Vector α 0) : v = #v[]

Proof state:
α : Type u_1
v : Vector α 0
⊢ v.toArray = { toArray := #[], size_toArray := ⋯ }.toArray

Tactic:
apply Array.eq_empty_of_size_eq_zero v.2

Result:
no goals

Proof state:
α : Type u_1
v : Vector α 0
⊢ v = { toArray := #[], size_toArray := ⋯ }

Tactic:
apply Vector.toArray_inj.1

Result:
α : Type u_1
v : Vector α 0
⊢ v.toArray = { toArray := #[], size_toArray := ⋯ }.toArray
-- Mathlib/GroupTheory/QuotientGroup/Basic.lean
theorem equivQuotientZPowOfEquiv_refl :
    MulEquiv.refl (A ⧸ (zpowGroupHom n : A →* A).range) =
      equivQuotientZPowOfEquiv (MulEquiv.refl A) n

Proof state:
A : Type u
inst✝ : CommGroup A
n : ℤ
⊢ MulEquiv.refl (A ⧸ (zpowGroupHom n).range) = equivQuotientZPowOfEquiv (MulEquiv.refl A) n

Tactic:
ext x

Result:
case h
A : Type u
inst✝ : CommGroup A
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ (MulEquiv.refl (A ⧸ (zpowGroupHom n).range)) x = (equivQuotientZPowOfEquiv (MulEquiv.refl A) n) x

Proof state:
case h
A : Type u
inst✝ : CommGroup A
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ (MulEquiv.refl (A ⧸ (zpowGroupHom n).range)) (Quotient.mk'' (Quotient.out x)) =
    (equivQuotientZPowOfEquiv (MulEquiv.refl A) n) (Quotient.mk'' (Quotient.out x))

Tactic:
rfl

Result:
no goals

Proof state:
case h
A : Type u
inst✝ : CommGroup A
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ (MulEquiv.refl (A ⧸ (zpowGroupHom n).range)) x = (equivQuotientZPowOfEquiv (MulEquiv.refl A) n) x

Tactic:
rw [← Quotient.out_eq' x]

Result:
case h
A : Type u
inst✝ : CommGroup A
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ (MulEquiv.refl (A ⧸ (zpowGroupHom n).range)) (Quotient.mk'' (Quotient.out x)) =
    (equivQuotientZPowOfEquiv (MulEquiv.refl A) n) (Quotient.mk'' (Quotient.out x))
-- Mathlib/Data/Bool/Basic.lean
theorem le_iff_imp : ∀ {x y : Bool}, x ≤ y ↔ x → y

Proof state:
⊢ ∀ {x y : Bool}, x ≤ y ↔ x = true → y = true

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Nat/Count.lean
theorem count_succ (n : ℕ) : count p (n + 1) = count p n + if p n then 1 else 0

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n + if p n then 1 else 0

Tactic:
split_ifs with h <;> simp [count, List.range_succ, h]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem coeff_coe_powerSeries (x : R⟦X⟧) (n : ℕ) :
    HahnSeries.coeff (x : R⸨X⸩) n = PowerSeries.coeff R n x

Proof state:
R : Type u_1
inst✝ : Semiring R
x : R⟦X⟧
n : ℕ
⊢ ((ofPowerSeries ℤ R) x).coeff ↑n = (PowerSeries.coeff R n) x

Tactic:
rw [ofPowerSeries_apply_coeff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
    [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k fallback : α} :
    ¬ k ∈ m → l.contains k = false →
      getKeyD (insertManyIfNewUnit m l) k fallback = fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k fallback : α
⊢ m.contains k = false → l.contains k = false → (insertManyIfNewUnit m l).getKeyD k fallback = fallback

Tactic:
simp_to_raw using
  Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k fallback : α
⊢ ¬k ∈ m → l.contains k = false → (insertManyIfNewUnit m l).getKeyD k fallback = fallback

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k fallback : α
⊢ m.contains k = false → l.contains k = false → (insertManyIfNewUnit m l).getKeyD k fallback = fallback
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem SatisfiesM_anyM [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) (start stop)
    (hstart : start ≤ min stop as.size) (tru : Prop) (fal : Nat → Prop) (h0 : fal start)
    (hp : ∀ i : Fin as.size, i.1 < stop → fal i.1 →
      SatisfiesM (bif · then tru else fal (i + 1)) (p as[i])) :
    SatisfiesM
      (fun res => bif res then tru else fal (min stop as.size))
      (anyM p as start stop)

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop✝ : Nat
hstart : start ≤ min stop✝ as.size
tru : Prop
fal : Nat → Prop
h0✝ : fal start
hp✝ : ∀ (i : Fin as.size), ↑i < stop✝ → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
stop j : Nat
hj' : j ≤ stop
hstop : stop ≤ as.size
h0 : fal j
hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])
hj : j < stop
⊢ SatisfiesM (fun res => bif res then tru else fal stop)
    (let_fun this := ⋯;
    do
    let __do_lift ← p as[j]
    if __do_lift = true then pure true else anyM.loop p as stop hstop (j + 1))

Tactic:
exact (hp ⟨j, Nat.lt_of_lt_of_le hj hstop⟩ hj h0).bind fun
  | true, h => .pure h
  | false, h => go hj hstop h hp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
theorem cospherical_singleton (p : P) : Cospherical ({p} : Set P)

Proof state:
P : Type u_2
inst✝ : MetricSpace P
p : P
⊢ Cospherical {p}

Tactic:
use p

Result:
case h
P : Type u_2
inst✝ : MetricSpace P
p : P
⊢ ∃ radius, ∀ p_1 ∈ {p}, dist p_1 p = radius

Proof state:
case h
P : Type u_2
inst✝ : MetricSpace P
p : P
⊢ ∃ radius, ∀ p_1 ∈ {p}, dist p_1 p = radius

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem filter_zero : (0 : α →₀ M).filter p = 0

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p 0 = 0

Tactic:
rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p 0 = 0

Tactic:
classical rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
lemma «exists» {p : Sym α n → Prop} :
    (∃ s : Sym α n, p s) ↔ ∃ (s : Multiset α) (hs : Multiset.card s = n), p (Sym.mk s hs)

Proof state:
α : Type u_1
n : ℕ
p : Sym α n → Prop
⊢ (∃ s, p s) ↔ ∃ s, ∃ (hs : s.card = n), p (mk s hs)

Tactic:
simp [Sym]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_eq_sum_mapIdx_aux (b : ℕ) (l : List ℕ) :
    (l.zipWith ((fun a i : ℕ => a * b ^ (i + 1))) (List.range l.length)).sum =
      b * (l.zipWith (fun a i => a * b ^ i) (List.range l.length)).sum

Proof state:
b : ℕ
l : List ℕ
⊢ (List.zipWith (fun a i => a * b ^ (i + 1)) l (List.range l.length)).sum =
    b * (List.zipWith (fun a i => a * b ^ i) l (List.range l.length)).sum

Tactic:
suffices
  l.zipWith (fun a i : ℕ => a * b ^ (i + 1)) (List.range l.length) =
    l.zipWith (fun a i=> b * (a * b ^ i)) (List.range l.length)
  by simp [this]

Result:
b : ℕ
l : List ℕ
⊢ List.zipWith (fun a i => a * b ^ (i + 1)) l (List.range l.length) =
    List.zipWith (fun a i => b * (a * b ^ i)) l (List.range l.length)

Proof state:
case e_f.h.h
b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ x✝¹ * b ^ (x✝ + 1) = b * (x✝¹ * b ^ x✝)

Tactic:
simp [pow_succ]

Result:
case e_f.h.h
b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ x✝¹ * (b ^ x✝ * b) = b * (x✝¹ * b ^ x✝)

Proof state:
case e_f.h.h
b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ x✝¹ * (b ^ x✝ * b) = b * (x✝¹ * b ^ x✝)

Tactic:
ring

Result:
no goals

Proof state:
b : ℕ
l : List ℕ
this :
  List.zipWith (fun a i => a * b ^ (i + 1)) l (List.range l.length) =
    List.zipWith (fun a i => b * (a * b ^ i)) l (List.range l.length)
⊢ (List.zipWith (fun a i => a * b ^ (i + 1)) l (List.range l.length)).sum =
    b * (List.zipWith (fun a i => a * b ^ i) l (List.range l.length)).sum

Tactic:
simp [this]

Result:
no goals

Proof state:
case e_f
b : ℕ
l : List ℕ
⊢ (fun a i => a * b ^ (i + 1)) = fun a i => b * (a * b ^ i)

Tactic:
ext

Result:
case e_f.h.h
b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ x✝¹ * b ^ (x✝ + 1) = b * (x✝¹ * b ^ x✝)

Proof state:
b : ℕ
l : List ℕ
⊢ List.zipWith (fun a i => a * b ^ (i + 1)) l (List.range l.length) =
    List.zipWith (fun a i => b * (a * b ^ i)) l (List.range l.length)

Tactic:
congr

Result:
case e_f
b : ℕ
l : List ℕ
⊢ (fun a i => a * b ^ (i + 1)) = fun a i => b * (a * b ^ i)
-- Mathlib/NumberTheory/Harmonic/GammaDeriv.lean
private lemma HasDerivAt.complex_of_real {f : ℂ → ℂ} {g : ℝ → ℝ} {g' s : ℝ}
    (hf : DifferentiableAt ℂ f s) (hg : HasDerivAt g g' s) (hfg : ∀ s : ℝ, f ↑s = ↑(g s)) :
    HasDerivAt f ↑g' s

Proof state:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f ↑s
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f ↑s = ↑(g s)
⊢ deriv (fun x => ↑(g x)) s = ↑g'

Tactic:
exact hg.ofReal_comp.deriv

Result:
no goals

Proof state:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f ↑s
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f ↑s = ↑(g s)
⊢ deriv f ↑s = ↑g'

Tactic:
rw [← (funext hfg ▸ hf.hasDerivAt.comp_ofReal.deriv :)]

Result:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f ↑s
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f ↑s = ↑(g s)
⊢ deriv (fun x => ↑(g x)) s = ↑g'

Proof state:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f ↑s
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f ↑s = ↑(g s)
⊢ HasDerivAt f ↑g' ↑s

Tactic:
refine HasDerivAt.congr_deriv hf.hasDerivAt ?_

Result:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f ↑s
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f ↑s = ↑(g s)
⊢ deriv f ↑s = ↑g'
-- Mathlib/Order/WellFoundedSet.lean
theorem wellFoundedOn_insert : WellFoundedOn (insert a s) r ↔ WellFoundedOn s r

Proof state:
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
a : α
⊢ (insert a s).WellFoundedOn r ↔ s.WellFoundedOn r

Tactic:
simp only [← singleton_union, wellFoundedOn_union, wellFoundedOn_singleton, true_and]

Result:
no goals
-- Mathlib/Logic/Embedding/Basic.lean
theorem equiv_symm_toEmbedding_trans_toEmbedding {α β : Sort*} (e : α ≃ β) :
    e.symm.toEmbedding.trans e.toEmbedding = Embedding.refl _

Proof state:
case h
α : Sort u_1
β : Sort u_2
e : α ≃ β
x✝ : β
⊢ (e.symm.toEmbedding.trans e.toEmbedding) x✝ = (Embedding.refl β) x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_2
e : α ≃ β
⊢ e.symm.toEmbedding.trans e.toEmbedding = Embedding.refl β

Tactic:
ext

Result:
case h
α : Sort u_1
β : Sort u_2
e : α ≃ β
x✝ : β
⊢ (e.symm.toEmbedding.trans e.toEmbedding) x✝ = (Embedding.refl β) x✝
-- Mathlib/Topology/UniformSpace/Cauchy.lean
lemma cauchy_prod_iff [UniformSpace β] {F : Filter (α × β)} :
    Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F)

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
F : Filter (α × β)
⊢ Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F)

Tactic:
simp_rw [instUniformSpaceProd, ← cauchy_comap_uniformSpace, ← cauchy_inf_uniformSpace]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem to_iso [h' : Epi f.base] : IsIso f

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
⊢ IsIso f

Tactic:
suffices IsIso (LocallyRingedSpace.forgetToSheafedSpace.map f) from
  isIso_of_reflects_iso _ LocallyRingedSpace.forgetToSheafedSpace

Result:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
⊢ IsIso (forgetToSheafedSpace.map f)

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
⊢ IsIso (forgetToSheafedSpace.map f)

Tactic:
exact SheafedSpace.IsOpenImmersion.to_iso f.1

Result:
no goals