harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Module/StrongTopology.lean
theorem isUniformInducing_postcomp
    {G : Type*} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G]
    {𝕜₃ : Type*} [NormedField 𝕜₃] [Module 𝕜₃ G]
    {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] [UniformSpace F] [UniformAddGroup F]
    (g : F →SL[τ] G) (hg : IsUniformInducing g) (𝔖 : Set (Set E)) :
    IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (β := UniformConvergenceCLM ρ G 𝔖)
      g.comp

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₂ F
G : Type u_5
inst✝⁷ : AddCommGroup G
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformAddGroup G
𝕜₃ : Type u_6
inst✝⁴ : NormedField 𝕜₃
inst✝³ : Module 𝕜₃ G
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝² : RingHomCompTriple σ τ ρ
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
g : F →SL[τ] G
hg : IsUniformInducing ⇑g
𝔖 : Set (Set E)
⊢ IsUniformInducing g.comp

Tactic:
rw [← (isUniformInducing_coeFn _ _ _).of_comp_iff]

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₂ F
G : Type u_5
inst✝⁷ : AddCommGroup G
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformAddGroup G
𝕜₃ : Type u_6
inst✝⁴ : NormedField 𝕜₃
inst✝³ : Module 𝕜₃ G
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝² : RingHomCompTriple σ τ ρ
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
g : F →SL[τ] G
hg : IsUniformInducing ⇑g
𝔖 : Set (Set E)
⊢ IsUniformInducing ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ g.comp)

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₂ F
G : Type u_5
inst✝⁷ : AddCommGroup G
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformAddGroup G
𝕜₃ : Type u_6
inst✝⁴ : NormedField 𝕜₃
inst✝³ : Module 𝕜₃ G
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝² : RingHomCompTriple σ τ ρ
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
g : F →SL[τ] G
hg : IsUniformInducing ⇑g
𝔖 : Set (Set E)
⊢ IsUniformInducing ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ g.comp)

Tactic:
exact (UniformOnFun.postcomp_isUniformInducing hg).comp (isUniformInducing_coeFn _ _ _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem anyTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) (j : Nat) (h : j ≤ n) :
    anyTR.loop n f j h = anyTR.loop m (fun i h => f i (by omega)) j (by omega)

Proof state:
n : Nat
f : (i : Nat) → i < n → Bool
j : Nat
h : j ≤ n
⊢ anyTR.loop n f j h = anyTR.loop n (fun i h => f i ⋯) j ⋯

Tactic:
rfl

Result:
no goals

Proof state:
n m : Nat
w : n = m
f : (i : Nat) → i < n → Bool
j : Nat
h : j ≤ n
⊢ j ≤ m

Tactic:
omega

Result:
no goals

Proof state:
n m : Nat
w : n = m
f : (i : Nat) → i < n → Bool
j : Nat
h : j ≤ n
⊢ anyTR.loop n f j h = anyTR.loop m (fun i h => f i ⋯) j ⋯

Tactic:
subst m

Result:
n : Nat
f : (i : Nat) → i < n → Bool
j : Nat
h : j ≤ n
⊢ anyTR.loop n f j h = anyTR.loop n (fun i h => f i ⋯) j ⋯

Proof state:
n m : Nat
w : n = m
f : (i : Nat) → i < n → Bool
j : Nat
h✝ : j ≤ n
i : Nat
h : i < m
⊢ i < n

Tactic:
omega

Result:
no goals
-- Mathlib/Tactic/Abel.lean
theorem term_add_termg {α} [AddCommGroup α] (n₁ x a₁ n₂ a₂ n' a')
    (h₁ : n₁ + n₂ = n') (h₂ : a₁ + a₂ = a') :
    @termg α _ n₁ x a₁ + @termg α _ n₂ x a₂ = termg n' x a'

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ termg n₁ x a₁ + termg n₂ x a₂ = termg n' x a'

Tactic:
simp only [termg, h₁.symm, add_zsmul, h₂.symm]

Result:
α : Type u_1
inst✝ : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ n₁ • x + a₁ + (n₂ • x + a₂) = n₁ • x + n₂ • x + (a₁ + a₂)

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ n₁ • x + a₁ + (n₂ • x + a₂) = n₁ • x + n₂ • x + (a₁ + a₂)

Tactic:
exact add_add_add_comm (n₁ • x) a₁ (n₂ • x) a₂

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem nthRootsFinset_zero : nthRootsFinset 0 R = ∅

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ nthRootsFinset 0 R = ∅

Tactic:
classical simp [nthRootsFinset_def]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ nthRootsFinset 0 R = ∅

Tactic:
simp [nthRootsFinset_def]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_closure_zero : gauge (closure (0 : Set E)) = 0 := funext fun x ↦ by
  simp only [← singleton_zero, gauge_def', mem_closure_zero_iff_norm, norm_smul, mul_eq_zero,
    norm_eq_zero, inv_eq_zero]
  rcases (norm_nonneg x).eq_or_gt with hx | hx
  · convert csInf_Ioi (a := (0 : ℝ))
    exact Set.ext fun r ↦ and_iff_left (.inr hx)
  · convert Real.sInf_empty
    exact eq_empty_of_forall_not_mem fun r ⟨hr₀, hr⟩ ↦ hx.ne' <| hr.resolve_left hr₀.out.ne'

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ gauge (closure 0) x = 0 x

Tactic:
simp only [← singleton_zero, gauge_def', mem_closure_zero_iff_norm, norm_smul, mul_eq_zero,
  norm_eq_zero, inv_eq_zero]

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x

Proof state:
case h.e'_2.h.e'_3
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : 0 < ‖x‖
⊢ {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = ∅

Tactic:
exact eq_empty_of_forall_not_mem fun r ⟨hr₀, hr⟩ ↦ hx.ne' <| hr.resolve_left hr₀.out.ne'

Result:
no goals

Proof state:
case h.e'_2.h.e'_3
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 0
⊢ {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = Ioi 0

Tactic:
exact Set.ext fun r ↦ and_iff_left (.inr hx)

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x

Tactic:
rcases (norm_nonneg x).eq_or_gt with hx | hx

Result:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 0
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x

case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : 0 < ‖x‖
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x

Proof state:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 0
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x

Tactic:
convert csInf_Ioi (a := (0 : ℝ))

Result:
case h.e'_2.h.e'_3
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 0
⊢ {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = Ioi 0

Proof state:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : 0 < ‖x‖
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x

Tactic:
convert Real.sInf_empty

Result:
case h.e'_2.h.e'_3
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : 0 < ‖x‖
⊢ {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = ∅
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem IsPrefix.findIdx?_eq_some {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
    List.findIdx? p l₁ = some i → List.findIdx? p l₂ = some i

Proof state:
α : Type u_1
i : Nat
l₁ l₂ : List α
p : α → Bool
h : ∃ t, l₁ ++ t = l₂
⊢ findIdx? p l₁ = some i → findIdx? p l₂ = some i

Tactic:
obtain ⟨t, rfl⟩ := h

Result:
case intro
α : Type u_1
i : Nat
l₁ : List α
p : α → Bool
t : List α
⊢ findIdx? p l₁ = some i → findIdx? p (l₁ ++ t) = some i

Proof state:
case intro
α : Type u_1
i : Nat
l₁ : List α
p : α → Bool
t : List α
⊢ findIdx? p l₁ = some i → findIdx? p (l₁ ++ t) = some i

Tactic:
intro h

Result:
case intro
α : Type u_1
i : Nat
l₁ : List α
p : α → Bool
t : List α
h : findIdx? p l₁ = some i
⊢ findIdx? p (l₁ ++ t) = some i

Proof state:
α : Type u_1
i : Nat
l₁ l₂ : List α
p : α → Bool
h : l₁ <+: l₂
⊢ findIdx? p l₁ = some i → findIdx? p l₂ = some i

Tactic:
rw [IsPrefix] at h

Result:
α : Type u_1
i : Nat
l₁ l₂ : List α
p : α → Bool
h : ∃ t, l₁ ++ t = l₂
⊢ findIdx? p l₁ = some i → findIdx? p l₂ = some i

Proof state:
case intro
α : Type u_1
i : Nat
l₁ : List α
p : α → Bool
t : List α
h : findIdx? p l₁ = some i
⊢ findIdx? p (l₁ ++ t) = some i

Tactic:
simp [findIdx?_append, h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff {θ : ℝ} {k : ℤ} :
    (θ : Angle).toReal = θ - 2 * k * π ↔ θ ∈ Set.Ioc ((2 * k - 1 : ℝ) * π) ((2 * k + 1) * π)

Proof state:
θ : ℝ
k : ℤ
h : -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π
⊢ (2 * ↑k - 1) * π < θ

Tactic:
linarith

Result:
no goals

Proof state:
θ : ℝ
k : ℤ
⊢ -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π ↔ (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π

Tactic:
exact ⟨fun h => ⟨by linarith, by linarith⟩, fun h => ⟨by linarith, by linarith⟩⟩

Result:
no goals

Proof state:
θ : ℝ
k : ℤ
h : (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π
⊢ θ - 2 * ↑k * π ≤ π

Tactic:
linarith

Result:
no goals

Proof state:
θ : ℝ
k : ℤ
h : -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π
⊢ θ ≤ (2 * ↑k + 1) * π

Tactic:
linarith

Result:
no goals

Proof state:
θ : ℝ
k : ℤ
⊢ (↑θ).toReal = θ - 2 * ↑k * π ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * π) ((2 * ↑k + 1) * π)

Tactic:
rw [← sub_zero (θ : Angle), ← zsmul_zero k, ← coe_two_pi, ← coe_zsmul, ← coe_sub, zsmul_eq_mul, ←
  mul_assoc, mul_comm (k : ℝ), toReal_coe_eq_self_iff, Set.mem_Ioc]

Result:
θ : ℝ
k : ℤ
⊢ -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π ↔ (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π

Proof state:
θ : ℝ
k : ℤ
h : (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π
⊢ -π < θ - 2 * ↑k * π

Tactic:
linarith

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsCondKernelCDF.setLIntegral [IsFiniteKernel κ]
    {f : α × β → StieltjesFunction} (hf : IsCondKernelCDF f κ ν)
    (a : α) {s : Set β} (hs : MeasurableSet s) (x : ℝ) :
    ∫⁻ b in s, ENNReal.ofReal (f (a, b) x) ∂(ν a) = κ a (s ×ˢ Iic x)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
inst✝ : IsFiniteKernel κ
f : α × β → StieltjesFunction
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
x : ℝ
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = (κ a) (s ×ˢ Iic x)

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal (hf.integrable a x).restrict
  (ae_of_all _ (fun _ ↦ hf.nonneg _ _)), hf.setIntegral a hs x, ENNReal.ofReal_toReal]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
inst✝ : IsFiniteKernel κ
f : α × β → StieltjesFunction
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
x : ℝ
⊢ (κ a) (s ×ˢ Iic x) ≠ ⊤

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
inst✝ : IsFiniteKernel κ
f : α × β → StieltjesFunction
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
x : ℝ
⊢ (κ a) (s ×ˢ Iic x) ≠ ⊤

Tactic:
exact measure_ne_top _ _

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem integral_smul_const [CompleteSpace E] (f : ℂ → ℂ) (a : E) (c : ℂ) (R : ℝ) :
    (∮ z in C(c, R), f z • a) = (∮ z in C(c, R), f z) • a

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → ℂ
a : E
c : ℂ
R : ℝ
⊢ (∮ (z : ℂ) in C(c, R), f z • a) = (∮ (z : ℂ) in C(c, R), f z) • a

Tactic:
simp only [circleIntegral, intervalIntegral.integral_smul_const, ← smul_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem BinaryFan.isLimit_iff_isIso_fst {X Y : C} (h : IsTerminal Y) (c : BinaryFan X Y) :
    Nonempty (IsLimit c) ↔ IsIso c.fst

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso c.fst
⊢ Nonempty (IsLimit c)

Tactic:
exact
  ⟨BinaryFan.IsLimit.mk _ (fun f _ => f ≫ inv c.fst) (fun _ _ => by simp)
      (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ => by simp [← e]⟩

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ IsIso c.fst → Nonempty (IsLimit c)

Tactic:
intro

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso c.fst
⊢ Nonempty (IsLimit c)

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) → IsIso c.fst

Tactic:
rintro ⟨H⟩

Result:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
⊢ IsIso c.fst

Proof state:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
⊢ IsIso c.fst

Tactic:
obtain ⟨l, hl, -⟩ := BinaryFan.IsLimit.lift' H (𝟙 X) (h.from X)

Result:
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ c.fst = 𝟙 X
⊢ IsIso c.fst

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso c.fst
T✝ : C
x✝¹ : T✝ ⟶ X
x✝ : T✝ ⟶ Y
⊢ (fun {T} f x => f ≫ inv c.fst) x✝¹ x✝ ≫ c.fst = x✝¹

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso c.fst
T✝ : C
x✝³ : T✝ ⟶ X
x✝² : T✝ ⟶ Y
x✝¹ : T✝ ⟶ c.pt
e : x✝¹ ≫ c.fst = x✝³
x✝ : x✝¹ ≫ c.snd = x✝²
⊢ x✝¹ = (fun {T} f x => f ≫ inv c.fst) x✝³ x✝²

Tactic:
simp [← e]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ c.fst = 𝟙 X
⊢ (c.fst ≫ l) ≫ c.fst = 𝟙 (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }) ≫ c.fst

Tactic:
simpa [hl, -Category.comp_id] using Category.comp_id _

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) ↔ IsIso c.fst

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) → IsIso c.fst

case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ IsIso c.fst → Nonempty (IsLimit c)

Proof state:
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ c.fst = 𝟙 X
⊢ IsIso c.fst

Tactic:
exact
  ⟨⟨l,
      BinaryFan.IsLimit.hom_ext H (by simpa [hl, -Category.comp_id] using Category.comp_id _)
        (h.hom_ext _ _),
      hl⟩⟩

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
theorem mlieBracketWithin_inter (ht : t ∈ 𝓝 x) :
    mlieBracketWithin I V W (s ∩ t) x = mlieBracketWithin I V W s x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
ht : t ∈ 𝓝 x
⊢ mlieBracketWithin I V W (s ∩ t) x = mlieBracketWithin I V W s x

Tactic:
apply mlieBracketWithin_congr_set

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
ht : t ∈ 𝓝 x
⊢ s ∩ t =ᶠ[𝓝 x] s

Proof state:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
ht : t ∈ 𝓝 x
y : M
hy : y ∈ t
⊢ (s ∩ t) y = s y

Tactic:
change (y ∈ s ∩ t) = (y ∈ s)

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
ht : t ∈ 𝓝 x
y : M
hy : y ∈ t
⊢ (y ∈ s ∩ t) = (y ∈ s)

Proof state:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
ht : t ∈ 𝓝 x
⊢ s ∩ t =ᶠ[𝓝 x] s

Tactic:
filter_upwards [ht] with y hy

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
ht : t ∈ 𝓝 x
y : M
hy : y ∈ t
⊢ (s ∩ t) y = s y

Proof state:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
ht : t ∈ 𝓝 x
y : M
hy : y ∈ t
⊢ (y ∈ s ∩ t) = (y ∈ s)

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_of_back? {xs : Vector α n} {a : α} (h : xs.back? = some a) : a ∈ xs

Proof state:
case mk
α : Type u_1
n : Nat
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : { toArray := toArray✝, size_toArray := size_toArray✝ }.back? = some a
⊢ a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simpa using Array.mem_of_back? (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : { toArray := toArray✝, size_toArray := size_toArray✝ }.back? = some a
⊢ toArray✝.back? = some a

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
a : α
h : xs.back? = some a
⊢ a ∈ xs

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : Nat
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : { toArray := toArray✝, size_toArray := size_toArray✝ }.back? = some a
⊢ a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_empty {a fallback : α} {c} :
    (empty c : Raw α β).getKeyD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
a fallback : α
c : Nat
⊢ (empty c).getKeyD a fallback = fallback

Tactic:
simp_to_raw using Raw₀.getKeyD_empty

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Impl.lean
theorem mergeSort_eq_mergeSortTR₂ : @mergeSort = @mergeSortTR₂

Proof state:
⊢ @mergeSort = @mergeSortTR₂

Tactic:
funext

Result:
case h.h.h
x✝² : Type u_1
x✝¹ : List x✝²
x✝ : autoParam (x✝² → x✝² → Bool) _auto✝
⊢ x✝¹.mergeSort x✝ = mergeSortTR₂ x✝¹ x✝

Proof state:
case h.h.h
x✝² : Type u_1
x✝¹ : List x✝²
x✝ : autoParam (x✝² → x✝² → Bool) _auto✝
⊢ x✝¹.mergeSort x✝ = mergeSortTR₂ x✝¹ x✝

Tactic:
rw [mergeSortTR₂, mergeSortTR₂_run_eq_mergeSort]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_lt_zpow_of_neg₀ (ha₀ : 0 < a) (ha₁ : a < 1) (hn : n < 0) : 1 < a ^ n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
hn : n < 0
⊢ 1 < a ^ n

Tactic:
simpa using zpow_right_strictAnti₀ ha₀ ha₁ hn

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem _root_.AddAction.IsBlock.of_addSubgroup_of_conjugate
    {G : Type*} [AddGroup G] {X : Type*} [AddAction G X] {B : Set X}
    {H : AddSubgroup G} (hB : AddAction.IsBlock H B) (g : G) :
    AddAction.IsBlock (H.map (AddAut.conj g).toMul.toAddMonoidHom) (g +ᵥ B)

Proof state:
case intro.intro
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
⊢ ↑h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B

Tactic:
rw [← hh, vadd_vadd, vadd_vadd]

Result:
case intro.intro
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
⊢ (g + h + -g + g) +ᵥ B = (g + h) +ᵥ B
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullbackWithin_smul_apply :
    mpullbackWithin I I' f (c • V) s x = c • mpullbackWithin I I' f V s x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
V : (x : M') → TangentSpace I' x
c : 𝕜
⊢ mpullbackWithin I I' f (c • V) s x = c • mpullbackWithin I I' f V s x

Tactic:
simp [mpullbackWithin_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_conj_of_mul_eq_one [DecidableEq m] [DecidableEq n] {M : Matrix m n A}
    {M' : Matrix n m A} {N : Matrix n n A} (hMM' : M * M' = 1) (hM'M : M' * M = 1) :
    det (M * N * M') = det N

Proof state:
A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ (M * N * M').det = N.det

Tactic:
rw [← det_comm' hM'M hMM', ← Matrix.mul_assoc, hM'M, Matrix.one_mul]

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem inv_gold : φ⁻¹ = -ψ

Proof state:
⊢ 0 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ φ⁻¹ = -ψ

Tactic:
have : 1 + √5 ≠ 0 := ne_of_gt (add_pos (by norm_num) <| Real.sqrt_pos.mpr (by norm_num))

Result:
this : 1 + √5 ≠ 0
⊢ φ⁻¹ = -ψ

Proof state:
this : 1 + √5 ≠ 0
⊢ φ⁻¹ = -ψ

Tactic:
field_simp [sub_mul, mul_add]

Result:
this : 1 + √5 ≠ 0
⊢ 2 * 2 = 5 - 1

Proof state:
⊢ 0 < 5

Tactic:
norm_num

Result:
no goals

Proof state:
this : 1 + √5 ≠ 0
⊢ 2 * 2 = 5 - 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem unassigned_of_has_neither (assignment : Assignment) (lacks_pos : ¬(hasPosAssignment assignment))
  (lacks_neg : ¬(hasNegAssignment assignment)) :
  assignment = unassigned

Proof state:
assignment : Assignment
lacks_neg : ¬assignment.hasNegAssignment = true
lacks_pos :
  (match assignment with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
⊢ assignment = unassigned

Tactic:
split at lacks_pos <;> simp_all +decide

Result:
no goals

Proof state:
assignment : Assignment
lacks_pos : ¬assignment.hasPosAssignment = true
lacks_neg : ¬assignment.hasNegAssignment = true
⊢ assignment = unassigned

Tactic:
simp only [hasPosAssignment, Bool.not_eq_true] at lacks_pos

Result:
assignment : Assignment
lacks_neg : ¬assignment.hasNegAssignment = true
lacks_pos :
  (match assignment with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
⊢ assignment = unassigned