harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem norm_image_sub_le_of_norm_deriv_le_segment_01 {C : ℝ}
    (hf : DifferentiableOn ℝ f (Icc (0 : ℝ) 1))
    (bound : ∀ x ∈ Ico (0 : ℝ) 1, ‖derivWithin f (Icc (0 : ℝ) 1) x‖ ≤ C) : ‖f 1 - f 0‖ ≤ C

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
C : ℝ
hf : DifferentiableOn ℝ f (Icc 0 1)
bound : ∀ x ∈ Ico 0 1, ‖derivWithin f (Icc 0 1) x‖ ≤ C
⊢ ‖f 1 - f 0‖ ≤ C

Tactic:
simpa only [sub_zero, mul_one] using
  norm_image_sub_le_of_norm_deriv_le_segment hf bound 1 (right_mem_Icc.2 zero_le_one)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean
theorem tendsto_lintegral_thickenedIndicator_of_isClosed {Ω : Type*} [MeasurableSpace Ω]
    [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ : Measure Ω) [IsFiniteMeasure μ] {F : Set Ω}
    (F_closed : IsClosed F) {δs : ℕ → ℝ} (δs_pos : ∀ n, 0 < δs n)
    (δs_lim : Tendsto δs atTop (𝓝 0)) :
    Tendsto (fun n ↦ lintegral μ fun ω ↦ (thickenedIndicator (δs_pos n) F ω : ℝ≥0∞)) atTop
      (𝓝 (μ F))

Proof state:
Ω : Type u_2
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
⊢ Tendsto (fun n ω => (thickenedIndicator ⋯ F) ω) atTop (𝓝 (F.indicator fun x => 1))

Tactic:
have key := thickenedIndicator_tendsto_indicator_closure δs_pos δs_lim F

Result:
Ω : Type u_2
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
key : Tendsto (fun n => ⇑(thickenedIndicator ⋯ F)) atTop (𝓝 ((closure F).indicator fun x => 1))
⊢ Tendsto (fun n ω => (thickenedIndicator ⋯ F) ω) atTop (𝓝 (F.indicator fun x => 1))

Proof state:
Ω : Type u_2
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
⊢ Tendsto (fun n => ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) atTop (𝓝 (μ F))

Tactic:
apply measure_of_cont_bdd_of_tendsto_indicator μ F_closed.measurableSet
  (fun n ↦ thickenedIndicator (δs_pos n) F) fun n ω ↦ thickenedIndicator_le_one (δs_pos n) F ω

Result:
Ω : Type u_2
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
⊢ Tendsto (fun n ω => (thickenedIndicator ⋯ F) ω) atTop (𝓝 (F.indicator fun x => 1))

Proof state:
Ω : Type u_2
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
key : Tendsto (fun n => ⇑(thickenedIndicator ⋯ F)) atTop (𝓝 ((closure F).indicator fun x => 1))
⊢ Tendsto (fun n ω => (thickenedIndicator ⋯ F) ω) atTop (𝓝 (F.indicator fun x => 1))

Tactic:
rwa [F_closed.closure_eq] at key

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_shrink_loop (a : Array α) (n : Nat) : (shrink.loop n a).size = a.size - n

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ (a : Array α), (shrink.loop n a).size = a.size - n
a : Array α
⊢ a.size - 1 - n = a.size - (n + 1)

Tactic:
omega

Result:
no goals

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ (a : Array α), (shrink.loop n a).size = a.size - n
a : Array α
⊢ (shrink.loop (n + 1) a).size = a.size - (n + 1)

Tactic:
simp [shrink.loop, ih]

Result:
case succ
α : Type u_1
n : Nat
ih : ∀ (a : Array α), (shrink.loop n a).size = a.size - n
a : Array α
⊢ a.size - 1 - n = a.size - (n + 1)

Proof state:
case zero
α : Type u_1
a : Array α
⊢ (shrink.loop 0 a).size = a.size - 0

Tactic:
simp [shrink.loop]

Result:
no goals

Proof state:
α : Type u_1
a : Array α
n : Nat
⊢ (shrink.loop n a).size = a.size - n

Tactic:
induction n generalizing a with
| zero => simp [shrink.loop]
| succ n ih =>
  simp [shrink.loop, ih]
  omega

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Linear.lean
theorem ContinuousLinearMap.hasStrictFDerivAt {x : E} : HasStrictFDerivAt e e x :=
  .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left fun x => by
    simp only [e.map_sub, sub_self, Pi.zero_apply]

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
e : E →L[𝕜] F
x✝ : E
x : E × E
⊢ 0 x = e x.1 - e x.2 - e (x.1 - x.2)

Tactic:
simp only [e.map_sub, sub_self, Pi.zero_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem decide_implies (u v : Prop)
    [duv : Decidable (u → v)] [du : Decidable u] {dv : u → Decidable v}
  : decide (u → v) = dite u (fun h => @decide v (dv h)) (fun _ => true) :=
  if h : u then by
    simp [h]
  else by
    simp [h]

Proof state:
u v : Prop
duv : Decidable (u → v)
du : Decidable u
dv : u → Decidable v
h : ¬u
⊢ decide (u → v) = if h : u then decide v else true

Tactic:
simp [h]

Result:
no goals

Proof state:
u v : Prop
duv : Decidable (u → v)
du : Decidable u
dv : u → Decidable v
h : u
⊢ decide (u → v) = if h : u then decide v else true

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem map_injective {f : G →g G'} (hinj : Function.Injective f) (u v : V) :
    Function.Injective (Path.map f hinj : G.Path u v → G'.Path (f u) (f v))

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v : V
⊢ Injective (Path.map f hinj)

Tactic:
rintro ⟨p, hp⟩ ⟨p', hp'⟩ h

Result:
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v : V
p : G.Walk u v
hp : p.IsPath
p' : G.Walk u v
hp' : p'.IsPath
h : Path.map f hinj ⟨p, hp⟩ = Path.map f hinj ⟨p', hp'⟩
⊢ ⟨p, hp⟩ = ⟨p', hp'⟩

Proof state:
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v : V
p : G.Walk u v
hp : p.IsPath
p' : G.Walk u v
hp' : p'.IsPath
h : Walk.map f p = Walk.map f p'
⊢ ⟨p, hp⟩ = ⟨p', hp'⟩

Tactic:
simp [Walk.map_injective_of_injective hinj u v h]

Result:
no goals

Proof state:
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v : V
p : G.Walk u v
hp : p.IsPath
p' : G.Walk u v
hp' : p'.IsPath
h : Path.map f hinj ⟨p, hp⟩ = Path.map f hinj ⟨p', hp'⟩
⊢ ⟨p, hp⟩ = ⟨p', hp'⟩

Tactic:
simp only [Path.map, Subtype.coe_mk, Subtype.mk.injEq] at h

Result:
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v : V
p : G.Walk u v
hp : p.IsPath
p' : G.Walk u v
hp' : p'.IsPath
h : Walk.map f p = Walk.map f p'
⊢ ⟨p, hp⟩ = ⟨p', hp'⟩
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem coe_linearMapAt (e : Pretrivialization F (π F E)) [e.IsLinear R] (b : B) :
    ⇑(e.linearMapAt R b) = fun y => if b ∈ e.baseSet then (e ⟨b, y⟩).2 else 0

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
⊢ ⇑(if hb : b ∈ e.baseSet then ↑(linearEquivAt R e b hb) else 0) = fun y =>
    if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
⊢ ⇑(Pretrivialization.linearMapAt R e b) = fun y => if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0

Tactic:
rw [Pretrivialization.linearMapAt]

Result:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
⊢ ⇑(if hb : b ∈ e.baseSet then ↑(linearEquivAt R e b hb) else 0) = fun y =>
    if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0
-- Mathlib/Probability/Kernel/Composition/Comp.lean
lemma const_comp (μ : Measure γ) (κ : Kernel α β) :
    const β μ ∘ₖ κ = fun a ↦ (κ a) Set.univ • μ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
⊢ ⇑(const β μ ∘ₖ κ) = fun a => (κ a) Set.univ • μ

Tactic:
ext _ _ hs

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
x✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((const β μ ∘ₖ κ) x✝) s✝ = ((κ x✝) Set.univ • μ) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
x✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((const β μ ∘ₖ κ) x✝) s✝ = ((κ x✝) Set.univ • μ) s✝

Tactic:
simp_rw [comp_apply' _ _ _ hs, const_apply, MeasureTheory.lintegral_const, Measure.smul_apply,
  smul_eq_mul, mul_comm]

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma valMinAbs_natCast_of_half_lt (ha : n / 2 < a) (ha' : a < n) :
    (a : ZMod n).valMinAbs = a - n

Proof state:
case zero
a : ℕ
ha : 0 / 2 < a
ha' : a < 0
⊢ (↑a).valMinAbs = ↑a - ↑0

Tactic:
cases not_lt_bot ha'

Result:
no goals

Proof state:
n a : ℕ
ha : n / 2 < a
ha' : a < n
⊢ (↑a).valMinAbs = ↑a - ↑n

Tactic:
cases n

Result:
case zero
a : ℕ
ha : 0 / 2 < a
ha' : a < 0
⊢ (↑a).valMinAbs = ↑a - ↑0

case succ
a n✝ : ℕ
ha : (n✝ + 1) / 2 < a
ha' : a < n✝ + 1
⊢ (↑a).valMinAbs = ↑a - ↑(n✝ + 1)

Proof state:
case succ
a n✝ : ℕ
ha : (n✝ + 1) / 2 < a
ha' : a < n✝ + 1
⊢ (↑a).valMinAbs = ↑a - ↑(n✝ + 1)

Tactic:
simp [valMinAbs_def_pos, val_natCast, Nat.mod_eq_of_lt ha', ha.not_le]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem le_total (a b : ℤ√d) : a ≤ b ∨ b ≤ a

Proof state:
d : ℕ
a b : ℤ√↑d
t : (b - a).Nonneg ∨ (-(b - a)).Nonneg
⊢ a ≤ b ∨ b ≤ a

Tactic:
rwa [neg_sub] at t

Result:
no goals

Proof state:
d : ℕ
a b : ℤ√↑d
⊢ a ≤ b ∨ b ≤ a

Tactic:
have t := (b - a).nonneg_total

Result:
d : ℕ
a b : ℤ√↑d
t : (b - a).Nonneg ∨ (-(b - a)).Nonneg
⊢ a ≤ b ∨ b ≤ a
-- Mathlib/CategoryTheory/Yoneda.lean
lemma isIso_iff_isIso_yoneda_map {X Y : C} (f : X ⟶ Y) :
    IsIso f ↔ ∀ c : C, IsIso ((yoneda.map f).app ⟨c⟩)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (∀ (T : C), Function.Bijective fun x => x ≫ f) ↔ ∀ (c : C), IsIso ((yoneda.map f).app (op c))

Tactic:
exact forall_congr' fun _ ↦ (isIso_iff_bijective _).symm

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (c : C), IsIso ((yoneda.map f).app (op c))

Tactic:
rw [isIso_iff_yoneda_map_bijective]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (∀ (T : C), Function.Bijective fun x => x ≫ f) ↔ ∀ (c : C), IsIso ((yoneda.map f).app (op c))
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem rangeS_top_iff_surjective {f : R →+* S} :
    f.rangeS = (⊤ : Subsemiring S) ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_rangeS, coe_top]) Set.range_eq_univ

Proof state:
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
⊢ ↑f.rangeS = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
rw [coe_rangeS, coe_top]

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Ideal.lean
theorem ExponentialIdeal.mk' (h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)) :
    ExponentialIdeal i :=
  ⟨fun hB A => by
    rcases hB with ⟨B', ⟨iB'⟩⟩
    exact Functor.essImage.ofIso ((exp A).mapIso iB') (h B' A)⟩

Proof state:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : ChosenFiniteProducts C
inst✝ : CartesianClosed C
h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)
B✝ : C
hB : i.essImage B✝
A : C
⊢ i.essImage (A ⟹ B✝)

Tactic:
rcases hB with ⟨B', ⟨iB'⟩⟩

Result:
case intro.intro
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : ChosenFiniteProducts C
inst✝ : CartesianClosed C
h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)
B✝ A : C
B' : D
iB' : i.obj B' ≅ B✝
⊢ i.essImage (A ⟹ B✝)

Proof state:
case intro.intro
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : ChosenFiniteProducts C
inst✝ : CartesianClosed C
h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)
B✝ A : C
B' : D
iB' : i.obj B' ≅ B✝
⊢ i.essImage (A ⟹ B✝)

Tactic:
exact Functor.essImage.ofIso ((exp A).mapIso iB') (h B' A)

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
@[simp] lemma sub_apply {f g : E →WOT[𝕜] F} (x : E) : (f - g) x = f x - g x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
f g : E →WOT[𝕜] F
x : E
⊢ (f - g) x = f x - g x

Tactic:
simp only [DFunLike.coe]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
f g : E →WOT[𝕜] F
x : E
⊢ (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm (f - g))).toFun x =
    (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm f)).toFun x -
      (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm g)).toFun x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
f g : E →WOT[𝕜] F
x : E
⊢ (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm (f - g))).toFun x =
    (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm f)).toFun x -
      (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm g)).toFun x

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_add_oangle_rev_neg_right (x y : V) : o.oangle x (-y) + o.oangle y (-x) = 0

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

Tactic:
rw [o.oangle_rev (-x), oangle_neg_left_eq_neg_right, add_neg_cancel]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem sheafedSpace_toSheafedSpace {X Y : SheafedSpace C} (f : X ⟶ Y) [IsOpenImmersion f] :
    toSheafedSpace Y f = X

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ toSheafedSpace Y f = X

Tactic:
cases X

Result:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
Y : SheafedSpace C
toPresheafedSpace✝ : PresheafedSpace C
IsSheaf✝ : toPresheafedSpace✝.presheaf.IsSheaf
f : { toPresheafedSpace := toPresheafedSpace✝, IsSheaf := IsSheaf✝ } ⟶ Y
inst✝ : IsOpenImmersion f
⊢ toSheafedSpace Y f = { toPresheafedSpace := toPresheafedSpace✝, IsSheaf := IsSheaf✝ }

Proof state:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
Y : SheafedSpace C
toPresheafedSpace✝ : PresheafedSpace C
IsSheaf✝ : toPresheafedSpace✝.presheaf.IsSheaf
f : { toPresheafedSpace := toPresheafedSpace✝, IsSheaf := IsSheaf✝ } ⟶ Y
inst✝ : IsOpenImmersion f
⊢ toSheafedSpace Y f = { toPresheafedSpace := toPresheafedSpace✝, IsSheaf := IsSheaf✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem sInf_coe (S : Set (LieSubalgebra R L)) : (↑(sInf S) : Set L) = ⋂ s ∈ S, (s : Set L)

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
⊢ ↑(sInf S) = ⋂ s ∈ S, ↑s

Tactic:
rw [← coe_toSubmodule, sInf_toSubmodule, Submodule.sInf_coe]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
⊢ ⋂ p ∈ {x | ∃ s ∈ S, s.toSubmodule = x}, ↑p = ⋂ s ∈ S, ↑s

Proof state:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
x : L
⊢ x ∈ ⋂ p ∈ {x | ∃ s ∈ S, s.toSubmodule = x}, ↑p ↔ x ∈ ⋂ s ∈ S, ↑s

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
⊢ ⋂ p ∈ {x | ∃ s ∈ S, s.toSubmodule = x}, ↑p = ⋂ s ∈ S, ↑s

Tactic:
ext x

Result:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
x : L
⊢ x ∈ ⋂ p ∈ {x | ∃ s ∈ S, s.toSubmodule = x}, ↑p ↔ x ∈ ⋂ s ∈ S, ↑s
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k : α} {v : β} :
    get! (m.insert k v) k = v

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
k : α
v : β
⊢ get! (m.insert k v) k = v

Tactic:
simp_to_raw using Raw₀.Const.get!_insert_self

Result:
no goals
-- Mathlib/Data/Int/WithZero.lean
theorem toNNReal_eq_one_iff {e : ℝ≥0} (m : ℤₘ₀) (he0 : e ≠ 0) (he1 : e ≠ 1) :
    toNNReal he0 m = 1 ↔ m = 1

Proof state:
case neg
e : ℝ≥0
m : ℤₘ₀
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : unzero hm = 1
⊢ m = 1

Tactic:
rw [← WithZero.coe_unzero hm, h1, coe_one]

Result:
no goals

Proof state:
case pos
e : ℝ≥0
m : ℤₘ₀
he0 : e ≠ 0
he1 : e ≠ 1
hm : m = 0
⊢ (toNNReal he0) m = 1 ↔ m = 1

Tactic:
simp only [hm, map_zero, zero_ne_one]

Result:
no goals

Proof state:
case neg
e : ℝ≥0
m : ℤₘ₀
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : (toNNReal he0) m = 1
⊢ m = 1

Tactic:
rw [toNNReal_neg_apply he0 hm, zpow_eq_one_iff_right₀ (zero_le e) he1, toAdd_eq_zero] at h1

Result:
case neg
e : ℝ≥0
m : ℤₘ₀
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : unzero hm = 1
⊢ m = 1

Proof state:
case neg
e : ℝ≥0
m : ℤₘ₀
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
⊢ (toNNReal he0) m = 1 ↔ m = 1

Tactic:
refine ⟨fun h1 ↦ ?_, fun h1 ↦ h1 ▸ map_one _⟩

Result:
case neg
e : ℝ≥0
m : ℤₘ₀
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : (toNNReal he0) m = 1
⊢ m = 1

Proof state:
e : ℝ≥0
m : ℤₘ₀
he0 : e ≠ 0
he1 : e ≠ 1
⊢ (toNNReal he0) m = 1 ↔ m = 1

Tactic:
by_cases hm : m = 0

Result:
case pos
e : ℝ≥0
m : ℤₘ₀
he0 : e ≠ 0
he1 : e ≠ 1
hm : m = 0
⊢ (toNNReal he0) m = 1 ↔ m = 1

case neg
e : ℝ≥0
m : ℤₘ₀
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
⊢ (toNNReal he0) m = 1 ↔ m = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_filterMap (f : α → Option β) (l : Array α) :
    (l.filterMap f).toList = l.toList.filterMap f

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ (filterMap f l).toList = List.filterMap f l.toList

Tactic:
simp [toList_filterMap']

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_right_comm {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε}
    (h_right_comm : ∀ a b c, f (g a b) c = g' (f' a c) b) :
    image2 f (image2 g s t) u = image2 g' (image2 f' s u) t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 (fun a b => g b a) t s) u = image2 (fun a b => g' b a) t (image2 f' s u)

Tactic:
exact image2_assoc fun _ _ _ => h_right_comm _ _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 g s t) u = image2 g' (image2 f' s u) t

Tactic:
rw [image2_swap g, image2_swap g']

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 (fun a b => g b a) t s) u = image2 (fun a b => g' b a) t (image2 f' s u)
-- Mathlib/GroupTheory/Nilpotent.lean
theorem nilpotencyClass_le_of_surjective {G' : Type*} [Group G'] (f : G →* G')
    (hf : Function.Surjective f) [h : IsNilpotent G] :
    Group.nilpotencyClass (hG := nilpotent_of_surjective _ hf) ≤ Group.nilpotencyClass G

Proof state:
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
⊢ nilpotencyClass G' ≤ nilpotencyClass G

Tactic:
classical apply Nat.find_mono

Result:
case h
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
⊢ ∀ (n : ℕ), upperCentralSeries G n = ⊤ → upperCentralSeries G' n = ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
⊢ nilpotencyClass G' ≤ nilpotencyClass G

Tactic:
apply Nat.find_mono

Result:
case h
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
⊢ ∀ (n : ℕ), upperCentralSeries G n = ⊤ → upperCentralSeries G' n = ⊤

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ⊤ ≤ upperCentralSeries G' n

Tactic:
calc
  ⊤ = f.range := symm (f.range_eq_top_of_surjective hf)
  _ = Subgroup.map f ⊤ := MonoidHom.range_eq_map _
  _ = Subgroup.map f (upperCentralSeries G n) := by rw [hn]
  _ ≤ upperCentralSeries G' n := upperCentralSeries.map hf n

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ Subgroup.map f ⊤ = Subgroup.map f (upperCentralSeries G n)

Tactic:
rw [hn]

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ upperCentralSeries G' n = ⊤

Tactic:
rw [eq_top_iff]

Result:
case h
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ⊤ ≤ upperCentralSeries G' n

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
⊢ ∀ (n : ℕ), upperCentralSeries G n = ⊤ → upperCentralSeries G' n = ⊤

Tactic:
intro n hn

Result:
case h
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ upperCentralSeries G' n = ⊤
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma eval_modulus_sub (x : ZMod n) : χ (n - x) = χ (-x)

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
x : ZMod n
⊢ χ (↑n - x) = χ (-x)

Tactic:
simp

Result:
no goals