harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
theorem inverse_continuousOn (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c)
    (hc : Subsingleton E ∨ c < N⁻¹) : ContinuousOn (hf.toPartialEquiv hc).symm (f '' 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
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ ContinuousOn (↑(hf.toPartialEquiv hc).symm) (f '' s)

Tactic:
apply continuousOn_iff_continuous_restrict.2

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
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ Continuous ((f '' s).restrict ↑(hf.toPartialEquiv hc).symm)

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
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ Continuous ((f '' s).restrict ↑(hf.toPartialEquiv hc).symm)

Tactic:
refine ((hf.antilipschitz hc).to_rightInvOn' ?_ (hf.toPartialEquiv hc).right_inv').continuous

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
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ MapsTo (hf.toPartialEquiv hc).invFun (hf.toPartialEquiv hc).target 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
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ MapsTo (hf.toPartialEquiv hc).invFun (hf.toPartialEquiv hc).target s

Tactic:
exact fun x hx => (hf.toPartialEquiv hc).map_target hx

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem of_comp_finite {f : A →+* B} {g : B →+* C} (h : (g.comp f).Finite) : g.Finite

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).Finite
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝ : Module.Finite A C
⊢ g.Finite

Tactic:
exact Module.Finite.of_restrictScalars_finite A B C

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).Finite
⊢ g.Finite

Tactic:
algebraize [f, g, g.comp f]

Result:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).Finite
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝ : Module.Finite A C
⊢ g.Finite
-- Mathlib/Topology/Order.lean
theorem isClosed_induced_iff' {f : α → β} {s : Set α} :
    IsClosed[t.induced f] s ↔ ∀ a, f a ∈ closure (f '' s) → a ∈ s

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set α
this : TopologicalSpace α := induced f t
⊢ IsClosed s ↔ ∀ (a : α), f a ∈ closure (f '' s) → a ∈ s

Tactic:
simp only [← closure_subset_iff_isClosed, subset_def, closure_induced]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set α
⊢ IsClosed s ↔ ∀ (a : α), f a ∈ closure (f '' s) → a ∈ s

Tactic:
letI := t.induced f

Result:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set α
this : TopologicalSpace α := induced f t
⊢ IsClosed s ↔ ∀ (a : α), f a ∈ closure (f '' s) → a ∈ s
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem norm_normedMk_le (S : AddSubgroup M) : ‖S.normedMk‖ ≤ 1 :=
  NormedAddGroupHom.opNorm_le_bound _ zero_le_one fun m => by simp [quotient_norm_mk_le']

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ‖S.normedMk m‖ ≤ 1 * ‖m‖

Tactic:
simp [quotient_norm_mk_le']

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_norm {f : α → F} :
    eLpNorm' (fun a => ‖f a‖) q μ = eLpNorm' f q μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
⊢ eLpNorm' (fun a => ‖f a‖) q μ = eLpNorm' f q μ

Tactic:
simp [eLpNorm'_eq_lintegral_enorm]

Result:
no goals
-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem eval_section_surjective_of_surjective (i : J) :
    (fun s : F.sections => s.val i).Surjective := fun x => by
  let s : Set (F.obj i) := {x}
  haveI := F.toPreimages_nonempty_of_surjective s Fsur (singleton_nonempty x)
  obtain ⟨sec, h⟩ := nonempty_sections_of_finite_cofiltered_system (F.toPreimages s)
  refine ⟨⟨fun j => (sec j).val, fun jk => by simpa [Subtype.ext_iff] using h jk⟩, ?_⟩
  · have := (sec i).prop
    simp only [mem_iInter, mem_preimage, mem_singleton_iff] at this
    have := this (𝟙 i)
    rwa [map_id_apply] at this

Proof state:
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
j✝ j'✝ : J
jk : j✝ ⟶ j'✝
⊢ F.map jk ((fun j => ↑(sec j)) j✝) = (fun j => ↑(sec j)) j'✝

Tactic:
simpa [Subtype.ext_iff] using h jk

Result:
no goals
-- Mathlib/Data/Nat/Choose/Bounds.lean
theorem choose_le_two_pow (n k : ℕ) (p : 0 < n) : n.choose k < 2 ^ n

Proof state:
n k : ℕ
p : 0 < n
⊢ n.choose k < 2 ^ n

Tactic:
refine lt_of_le_of_lt ?_ (Nat.two_pow_pred_lt_two_pow p)

Result:
n k : ℕ
p : 0 < n
⊢ n.choose k ≤ 2 ^ (n - 1)

Proof state:
n k : ℕ
p : 0 < n
⊢ n.choose k ≤ 2 ^ (n - 1)

Tactic:
rw [← Nat.sub_add_cancel p]

Result:
n k : ℕ
p : 0 < n
⊢ (n - succ 0 + succ 0).choose k ≤ 2 ^ (n - succ 0 + succ 0 - 1)

Proof state:
n k : ℕ
p : 0 < n
⊢ (n - succ 0 + succ 0).choose k ≤ 2 ^ (n - succ 0 + succ 0 - 1)

Tactic:
exact choose_succ_le_two_pow (n - 1) k

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem topologicalGroup_iInf {ts' : ι → TopologicalSpace G}
    (h' : ∀ i, @IsTopologicalGroup G (ts' i) _) : @IsTopologicalGroup G (⨅ i, ts' i) _

Proof state:
G : Type w
ι : Sort u_1
inst✝ : Group G
ts' : ι → TopologicalSpace G
h' : ∀ (i : ι), IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
exact topologicalGroup_sInf (Set.forall_mem_range.mpr h')

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma one_le_inv_iff_le_one {a : Aˣ} (ha : 0 ≤ (a : A)) :
    1 ≤ (↑a⁻¹ : A) ↔ a ≤ 1

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : 0 ≤ ↑a
⊢ 1 ≤ ↑a⁻¹ ↔ a ≤ 1

Tactic:
simpa using CStarAlgebra.le_inv_iff (a := 1) (by simp) ha

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : 0 ≤ ↑a
⊢ 0 ≤ ↑1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem Basis.ofZLatticeBasis_comap (e : F ≃L[K] E) {ι : Type*} (b : Basis ι ℤ L) :
    (b.ofZLatticeComap K L e.toLinearEquiv).ofZLatticeBasis K (ZLattice.comap K L e.toLinearMap) =
    (b.ofZLatticeBasis K L).map e.symm.toLinearEquiv

Proof state:
case a
K : Type u_1
inst✝¹² : NormedLinearOrderedField K
inst✝¹¹ : HasSolidNorm K
inst✝¹⁰ : FloorRing K
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace K E
inst✝⁷ : FiniteDimensional K E
inst✝⁶ : ProperSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace K F
inst✝³ : FiniteDimensional K F
inst✝² : ProperSpace F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
e : F ≃L[K] E
ι : Type u_4
b : Basis ι ℤ ↥L
i✝ : ι
⊢ (ofZLatticeBasis K (ZLattice.comap K L ↑e.toLinearEquiv) (ofZLatticeComap K L e.toLinearEquiv b)) i✝ =
    ((ofZLatticeBasis K L b).map e.symm.toLinearEquiv) i✝

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝¹² : NormedLinearOrderedField K
inst✝¹¹ : HasSolidNorm K
inst✝¹⁰ : FloorRing K
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace K E
inst✝⁷ : FiniteDimensional K E
inst✝⁶ : ProperSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace K F
inst✝³ : FiniteDimensional K F
inst✝² : ProperSpace F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
e : F ≃L[K] E
ι : Type u_4
b : Basis ι ℤ ↥L
⊢ ofZLatticeBasis K (ZLattice.comap K L ↑e.toLinearEquiv) (ofZLatticeComap K L e.toLinearEquiv b) =
    (ofZLatticeBasis K L b).map e.symm.toLinearEquiv

Tactic:
ext

Result:
case a
K : Type u_1
inst✝¹² : NormedLinearOrderedField K
inst✝¹¹ : HasSolidNorm K
inst✝¹⁰ : FloorRing K
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace K E
inst✝⁷ : FiniteDimensional K E
inst✝⁶ : ProperSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace K F
inst✝³ : FiniteDimensional K F
inst✝² : ProperSpace F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
e : F ≃L[K] E
ι : Type u_4
b : Basis ι ℤ ↥L
i✝ : ι
⊢ (ofZLatticeBasis K (ZLattice.comap K L ↑e.toLinearEquiv) (ofZLatticeComap K L e.toLinearEquiv b)) i✝ =
    ((ofZLatticeBasis K L b).map e.symm.toLinearEquiv) i✝
-- Mathlib/Analysis/Convex/Strong.lean
nonrec lemma StrongConcaveOn.strictConcaveOn (hf : StrongConcaveOn s m f) (hm : 0 < m) :
    StrictConcaveOn ℝ s f := hf.strictConcaveOn fun r hr ↦ by positivity

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
f : E → ℝ
m : ℝ
hf : StrongConcaveOn s m f
hm : 0 < m
r : ℝ
hr : r ≠ 0
⊢ 0 < m / 2 * r ^ 2

Tactic:
positivity

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem neg_nim (o : Ordinal) : -nim o = nim o

Proof state:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, -nim k = nim k
⊢ (-mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)) =
    mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)

Tactic:
dsimp

Result:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, -nim k = nim k
⊢ (mk o.toType o.toType (fun x => -nim ↑(o.enumIsoToType.symm x)) fun x => -nim ↑(o.enumIsoToType.symm x)) =
    mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)

Proof state:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, -nim k = nim k
⊢ (mk o.toType o.toType (fun x => -nim ↑(o.enumIsoToType.symm x)) fun x => -nim ↑(o.enumIsoToType.symm x)) =
    mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)

Tactic:
congr <;> funext i <;> exact IH _ (Ordinal.typein_lt_self i)

Result:
no goals

Proof state:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, -nim k = nim k
⊢ -nim o = nim o

Tactic:
rw [nim]

Result:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, -nim k = nim k
⊢ (-mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)) =
    mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)

Proof state:
o : Ordinal.{u_1}
⊢ -nim o = nim o

Tactic:
induction' o using Ordinal.induction with o IH

Result:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, -nim k = nim k
⊢ -nim o = nim o
-- Mathlib/MeasureTheory/Group/Integral.lean
theorem integral_eq_zero_of_mul_right_eq_neg [IsMulRightInvariant μ] (hf' : ∀ x, f (x * g) = -f x) :
    ∫ x, f x ∂μ = 0

Proof state:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
hf' : ∀ (x : G), f (x * g) = -f x
⊢ ∫ (x : G), f x ∂μ = 0

Tactic:
simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_right_eq_self]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_singleton {b n : ℕ} : ofDigits b [n] = n

Proof state:
b n : ℕ
⊢ ofDigits b [n] = n

Tactic:
simp [ofDigits]

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
lemma tendsto_klFun_atTop : Tendsto klFun atTop atTop

Proof state:
this : klFun = fun x => x * (log x - 1) + 1
⊢ Tendsto (fun x => x * (log x - 1) + 1) atTop atTop

Tactic:
refine Tendsto.atTop_add ?_ tendsto_const_nhds

Result:
this : klFun = fun x => x * (log x - 1) + 1
⊢ Tendsto (fun x => x * (log x - 1)) atTop atTop

Proof state:
⊢ klFun = fun x => x * (log x - 1) + 1

Tactic:
unfold klFun

Result:
⊢ (fun x => x * log x + 1 - x) = fun x => x * (log x - 1) + 1

Proof state:
⊢ Tendsto klFun atTop atTop

Tactic:
have : klFun = (fun x ↦ x * (log x - 1) + 1) := by unfold klFun; ext; ring

Result:
this : klFun = fun x => x * (log x - 1) + 1
⊢ Tendsto klFun atTop atTop

Proof state:
case h
x✝ : ℝ
⊢ x✝ * log x✝ + 1 - x✝ = x✝ * (log x✝ - 1) + 1

Tactic:
ring

Result:
no goals

Proof state:
⊢ (fun x => x * log x + 1 - x) = fun x => x * (log x - 1) + 1

Tactic:
ext

Result:
case h
x✝ : ℝ
⊢ x✝ * log x✝ + 1 - x✝ = x✝ * (log x✝ - 1) + 1

Proof state:
this : klFun = fun x => x * (log x - 1) + 1
⊢ Tendsto klFun atTop atTop

Tactic:
rw [this]

Result:
this : klFun = fun x => x * (log x - 1) + 1
⊢ Tendsto (fun x => x * (log x - 1) + 1) atTop atTop

Proof state:
this : klFun = fun x => x * (log x - 1) + 1
⊢ Tendsto (fun x => log x - 1) atTop atTop

Tactic:
exact tendsto_log_atTop.atTop_add tendsto_const_nhds

Result:
no goals

Proof state:
this : klFun = fun x => x * (log x - 1) + 1
⊢ Tendsto (fun x => x * (log x - 1)) atTop atTop

Tactic:
refine tendsto_id.atTop_mul_atTop₀ ?_

Result:
this : klFun = fun x => x * (log x - 1) + 1
⊢ Tendsto (fun x => log x - 1) atTop atTop
-- Mathlib/GroupTheory/Complement.lean
theorem toRightFun_mul_inv_mem (hT : IsComplement H T) (g : G) :
    (toRightFun hT g : G) * g⁻¹ ∈ H :=
  (congr_arg (· ∈ H) (by rw [mul_inv_rev, inv_inv])).mp (H.inv_mem (mul_inv_toRightFun_mem hT g))

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hT : IsComplement (↑H) T
g : G
⊢ (g * (↑(hT.toRightFun g))⁻¹)⁻¹ = ↑(hT.toRightFun g) * g⁻¹

Tactic:
rw [mul_inv_rev, inv_inv]

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
lemma slope_lt_of_hasDerivWithinAt_Ioi (hfc : StrictConcaveOn ℝ S f)
    (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Ioi x) x) :
    slope f x y < f'

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ slope f x y < f'

Tactic:
simpa only [Pi.neg_def, slope_neg, neg_neg] using
  neg_lt_neg (hfc.neg.lt_slope_of_hasDerivWithinAt_Ioi hx hy hxy hf'.neg)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
    (range n).find? p = some i ↔ p i ∧ i ∈ range n ∧ ∀ j, j < i → !p j

Proof state:
n i : Nat
p : Nat → Bool
⊢ find? p (range n) = some i ↔ p i = true ∧ i ∈ range n ∧ ∀ (j : Nat), j < i → (!p j) = true

Tactic:
simp [range_eq_range']

Result:
no goals
-- Mathlib/Data/PEquiv.lean
theorem self_trans_symm (f : α ≃. β) : f.trans f.symm = ofSet { a | (f a).isSome }

Proof state:
case h.a.mpr
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, f a = some a_1} → ∃ a, f x✝ = some a ∧ f a✝ = some a

Tactic:
simp +contextual

Result:
no goals

Proof state:
case h.a.mp
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ (∃ a, f x✝ = some a ∧ f a✝ = some a) → a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, f a = some a_1}

Tactic:
rintro ⟨b, hb₁, hb₂⟩

Result:
case h.a.mp.intro.intro
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
b : β
hb₁ : f x✝ = some b
hb₂ : f a✝ = some b
⊢ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, f a = some a_1}

Proof state:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ a✝ ∈ (f x✝).bind ⇑f.symm ↔ a✝ ∈ (ofSet {a | (f a).isSome = true}) x✝

Tactic:
simp only [eq_some_iff f, Option.isSome_iff_exists, Option.mem_def, bind_eq_some',
  ofSet_eq_some_iff]

Result:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ (∃ a, f x✝ = some a ∧ f a✝ = some a) ↔ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, f a = some a_1}

Proof state:
α : Type u
β : Type v
f : α ≃. β
⊢ f.trans f.symm = ofSet {a | (f a).isSome = true}

Tactic:
ext

Result:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ a✝ ∈ (f.trans f.symm) x✝ ↔ a✝ ∈ (ofSet {a | (f a).isSome = true}) x✝

Proof state:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ (∃ a, f x✝ = some a ∧ f a✝ = some a) ↔ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, f a = some a_1}

Tactic:
constructor

Result:
case h.a.mp
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ (∃ a, f x✝ = some a ∧ f a✝ = some a) → a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, f a = some a_1}

case h.a.mpr
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, f a = some a_1} → ∃ a, f x✝ = some a ∧ f a✝ = some a

Proof state:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ a✝ ∈ (f.trans f.symm) x✝ ↔ a✝ ∈ (ofSet {a | (f a).isSome = true}) x✝

Tactic:
dsimp [PEquiv.trans]

Result:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ a✝ ∈ (f x✝).bind ⇑f.symm ↔ a✝ ∈ (ofSet {a | (f a).isSome = true}) x✝

Proof state:
case h.a.mp.intro.intro
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
b : β
hb₁ : f x✝ = some b
hb₂ : f a✝ = some b
⊢ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, f a = some a_1}

Tactic:
exact ⟨PEquiv.inj _ hb₂ hb₁, b, hb₂⟩

Result:
no goals
-- Mathlib/GroupTheory/PGroup.lean
theorem to_le {H K : Subgroup G} (hK : IsPGroup p K) (hHK : H ≤ K) : IsPGroup p H :=
  hK.of_injective (Subgroup.inclusion hHK) fun a b h =>
    Subtype.ext (by
      change ((Subgroup.inclusion hHK) a : G) = (Subgroup.inclusion hHK) b
      apply Subtype.ext_iff.mp h)

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : IsPGroup p ↥K
hHK : H ≤ K
a b : ↥H
h : (Subgroup.inclusion hHK) a = (Subgroup.inclusion hHK) b
⊢ ↑a = ↑b

Tactic:
change ((Subgroup.inclusion hHK) a : G) = (Subgroup.inclusion hHK) b

Result:
p : ℕ
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : IsPGroup p ↥K
hHK : H ≤ K
a b : ↥H
h : (Subgroup.inclusion hHK) a = (Subgroup.inclusion hHK) b
⊢ ↑((Subgroup.inclusion hHK) a) = ↑((Subgroup.inclusion hHK) b)

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : IsPGroup p ↥K
hHK : H ≤ K
a b : ↥H
h : (Subgroup.inclusion hHK) a = (Subgroup.inclusion hHK) b
⊢ ↑((Subgroup.inclusion hHK) a) = ↑((Subgroup.inclusion hHK) b)

Tactic:
apply Subtype.ext_iff.mp h

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_of_injOn (e : ι → κ) (he : Set.InjOn e s) (hest : Set.MapsTo e s t)
    (h' : ∀ i ∈ t, i ∉ e '' s → g i = 1) (h : ∀ i ∈ s, f i = g (e i))  :
    ∏ i ∈ s, f i = ∏ j ∈ t, g j

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝ : CommMonoid α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
e : ι → κ
he : Set.InjOn e ↑s
hest : Set.MapsTo e ↑s ↑t
h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ ∀ x ∈ t, x ∉ image e s → g x = 1

Tactic:
simpa using h'

Result:
no goals

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝ : CommMonoid α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
e : ι → κ
he : Set.InjOn e ↑s
hest : Set.MapsTo e ↑s ↑t
h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ ∏ i ∈ s, f i = ∏ j ∈ t, g j

Tactic:
exact (prod_nbij e (fun a ↦ mem_image_of_mem e) he (by simp [Set.surjOn_image]) h).trans <|
  prod_subset (image_subset_iff.2 hest) <| by simpa using h'

Result:
no goals

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝ : CommMonoid α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
e : ι → κ
he : Set.InjOn e ↑s
hest : Set.MapsTo e ↑s ↑t
h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ ∏ i ∈ s, f i = ∏ j ∈ t, g j

Tactic:
classical
exact (prod_nbij e (fun a ↦ mem_image_of_mem e) he (by simp [Set.surjOn_image]) h).trans <|
  prod_subset (image_subset_iff.2 hest) <| by simpa using h'

Result:
no goals

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝ : CommMonoid α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
e : ι → κ
he : Set.InjOn e ↑s
hest : Set.MapsTo e ↑s ↑t
h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ Set.SurjOn e ↑s ↑(image e s)

Tactic:
simp [Set.surjOn_image]

Result:
no goals
-- Mathlib/Data/Multiset/Dedup.lean
theorem dedup_map_dedup_eq [DecidableEq β] (f : α → β) (s : Multiset α) :
    dedup (map f (dedup s)) = dedup (map f s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
⊢ (map f s.dedup).dedup = (map f s).dedup

Tactic:
simp [dedup_ext]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean
theorem IsLocallyFull.ext [G.IsLocallyFull K]
    (ℱ : Sheaf K (Type _)) {X Y : C} (i : G.obj X ⟶ G.obj Y)
    {s t : ℱ.val.obj (op (G.obj X))}
    (h : ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y), G.map f = G.map j ≫ i →
      ℱ.1.map (G.map j).op s = ℱ.1.map (G.map j).op t) : s = t

Proof state:
case intro.intro.intro.intro.intro
C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFull K
ℱ : Sheaf K (Type u_2)
X Y : C
i : G.obj X ⟶ G.obj Y
s t : ℱ.val.obj (op (G.obj X))
h : ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y), G.map f = G.map j ≫ i → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t
Z : D
W : C
iWX : W ⟶ X
iZW : Z ⟶ G.obj W
iWY : W ⟶ Y
e : G.map iWY = G.map iWX ≫ i
⊢ ℱ.val.map (iZW ≫ G.map iWX).op s = ℱ.val.map (iZW ≫ G.map iWX).op t

Tactic:
simp [h iWX iWY e]

Result:
no goals

Proof state:
C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFull K
ℱ : Sheaf K (Type u_2)
X Y : C
i : G.obj X ⟶ G.obj Y
s t : ℱ.val.obj (op (G.obj X))
h : ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y), G.map f = G.map j ≫ i → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t
⊢ ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj X⦄,
    (Sieve.functorPushforward G (G.imageSieve i)).arrows f → ℱ.val.map f.op s = ℱ.val.map f.op t

Tactic:
rintro Z _ ⟨W, iWX, iZW, ⟨iWY, e⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro
C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFull K
ℱ : Sheaf K (Type u_2)
X Y : C
i : G.obj X ⟶ G.obj Y
s t : ℱ.val.obj (op (G.obj X))
h : ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y), G.map f = G.map j ≫ i → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t
Z : D
W : C
iWX : W ⟶ X
iZW : Z ⟶ G.obj W
iWY : W ⟶ Y
e : G.map iWY = G.map iWX ≫ i
⊢ ℱ.val.map (iZW ≫ G.map iWX).op s = ℱ.val.map (iZW ≫ G.map iWX).op t

Proof state:
C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFull K
ℱ : Sheaf K (Type u_2)
X Y : C
i : G.obj X ⟶ G.obj Y
s t : ℱ.val.obj (op (G.obj X))
h : ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y), G.map f = G.map j ≫ i → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t
⊢ s = t

Tactic:
apply (((isSheaf_iff_isSheaf_of_type _ _).1 ℱ.cond) _
  (G.functorPushforward_imageSieve_mem K i)).isSeparatedFor.ext

Result:
C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFull K
ℱ : Sheaf K (Type u_2)
X Y : C
i : G.obj X ⟶ G.obj Y
s t : ℱ.val.obj (op (G.obj X))
h : ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y), G.map f = G.map j ≫ i → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t
⊢ ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj X⦄,
    (Sieve.functorPushforward G (G.imageSieve i)).arrows f → ℱ.val.map f.op s = ℱ.val.map f.op t