harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem MeasurableSet.of_mem_nhdsGT {s : Set α} (h : ∀ x ∈ s, s ∈ 𝓝[>] x) : MeasurableSet s

Proof state:
case pos.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
x : α
hx : x ∈ s \ {x₀}
⊢ s \ {x₀} ∈ 𝓝[>] x

Tactic:
obtain ⟨u, hu, us⟩ : ∃ (u : α), u ∈ Ioi x ∧ Ioo x u ⊆ s :=
  (mem_nhdsGT_iff_exists_Ioo_subset' (A x hx)).1 (h x hx.1)

Result:
case pos.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
x : α
hx : x ∈ s \ {x₀}
u : α
hu : u ∈ Ioi x
us : Ioo x u ⊆ s
⊢ s \ {x₀} ∈ 𝓝[>] x

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
⊢ s = {x₀} ∪ s \ {x₀}

Tactic:
rw [union_diff_cancel (singleton_subset_iff.2 x₀s)]

Result:
no goals

Proof state:
case pos.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
⊢ MeasurableSet (s \ {x₀})

Tactic:
refine .of_mem_nhdsGT_aux (fun x hx => ?_) fun x hx => ⟨x₀, A x hx⟩

Result:
case pos.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
x : α
hx : x ∈ s \ {x₀}
⊢ s \ {x₀} ∈ 𝓝[>] x

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
⊢ MeasurableSet s

Tactic:
by_cases H : ∃ x ∈ s, IsTop x

Result:
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
H : ∃ x ∈ s, IsTop x
⊢ MeasurableSet s

case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
H : ¬∃ x ∈ s, IsTop x
⊢ MeasurableSet s
-- Mathlib/Order/Interval/Finset/Defs.lean
theorem map_subtype_embedding_Ioc (hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x):
    (Ioc a b).map (Embedding.subtype p) = (Ioc a b : Finset α)

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ioc ↑a ↑b
⊢ p x

Tactic:
rw [mem_Ioc] at hx

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a < x ∧ x ≤ ↑b
⊢ p x

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Ioc a b) = Ioc ↑a ↑b

Tactic:
rw [subtype_Ioc_eq]

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioc ↑a ↑b)) = Ioc ↑a ↑b

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioc ↑a ↑b)) = Ioc ↑a ↑b

Tactic:
refine Finset.subtype_map_of_mem fun x hx => ?_

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ioc ↑a ↑b
⊢ p x

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a < x ∧ x ≤ ↑b
⊢ p x

Tactic:
exact hp hx.1.le hx.2 a.prop b.prop

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_add' : ∀ (x y : R), v x ≤ v (x + y) ∨ v y ≤ v (x + y)

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
⊢ v x ≤ v (x + y) ∨ v y ≤ v (x + y)

Tactic:
rw [← @min_le_iff _ _ (v x) (v y) (v (x+y)), ← ge_iff_le]

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
⊢ v (x + y) ≥ v x ⊓ v y

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
⊢ v (x + y) ≥ v x ⊓ v y

Tactic:
apply map_add

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
⊢ ∀ (x y : R), v x ≤ v (x + y) ∨ v y ≤ v (x + y)

Tactic:
intro x y

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
⊢ v x ≤ v (x + y) ∨ v y ≤ v (x + y)
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem hasFDerivWithinAt_comp_add_right (a : E) :
    HasFDerivWithinAt (fun x ↦ f (x + a)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (x + a)

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
x : E
s : Set E
a : E
⊢ HasFDerivWithinAt (fun x => f (x + a)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (x + a)

Tactic:
simpa only [add_comm a] using hasFDerivWithinAt_comp_add_left a

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem smul_add [Zero R] [DistribSMul R V] (x : HahnSeries Γ R) (y z : HahnModule Γ' R V) :
    x • (y + z) = x • y + x • z

Proof state:
case h.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ∑ x_1 ∈ VAddAntidiagonal ⋯ hwf k, x.coeff x_1.1 • (((of R).symm y).coeff x_1.2 + ((of R).symm z).coeff x_1.2) =
    ((of R).symm (x • y)).coeff k + ((of R).symm (x • z)).coeff k

Tactic:
rw [coeff_smul_right hwf Set.subset_union_right,
  coeff_smul_right hwf Set.subset_union_left]

Result:
case h.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ∑ x_1 ∈ VAddAntidiagonal ⋯ hwf k, x.coeff x_1.1 • (((of R).symm y).coeff x_1.2 + ((of R).symm z).coeff x_1.2) =
    ∑ ij ∈ VAddAntidiagonal ⋯ hwf k, x.coeff ij.1 • ((of R).symm y).coeff ij.2 +
      ∑ ij ∈ VAddAntidiagonal ⋯ hwf k, x.coeff ij.1 • ((of R).symm z).coeff ij.2

Proof state:
case h.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ∑ x_1 ∈ VAddAntidiagonal ⋯ hwf k, x.coeff x_1.1 • (((of R).symm y).coeff x_1.2 + ((of R).symm z).coeff x_1.2) =
    ∑ ij ∈ VAddAntidiagonal ⋯ hwf k, x.coeff ij.1 • ((of R).symm y).coeff ij.2 +
      ∑ ij ∈ VAddAntidiagonal ⋯ hwf k, x.coeff ij.1 • ((of R).symm z).coeff ij.2

Tactic:
simp_all [sum_add_distrib]

Result:
no goals

Proof state:
case h.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k b : Γ'
h : ((of R).symm y).coeff b = 0 ∧ ((of R).symm z).coeff b = 0
⊢ ((of R).symm y).coeff b + ((of R).symm z).coeff b = 0

Tactic:
rw [h.1, h.2, add_zero]

Result:
no goals
-- Mathlib/Algebra/Group/Center.lean
theorem mul_mem_center {z₁ z₂ : M} (hz₁ : z₁ ∈ Set.center M) (hz₂ : z₂ ∈ Set.center M) :
    z₁ * z₂ ∈ Set.center M where
  comm a := calc
    z₁ * z₂ * a = z₂ * z₁ * a

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
a : M
⊢ z₁ * z₂ * a = z₂ * z₁ * a

Tactic:
rw [hz₁.comm]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
a c : M
⊢ a * (z₁ * z₂) * c = a * z₁ * z₂ * c

Tactic:
rw [hz₁.mid_assoc]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
a b : M
⊢ a * b * z₁ * z₂ = a * (b * z₁) * z₂

Tactic:
rw [hz₁.right_assoc]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
b c : M
⊢ z₁ * (z₂ * b) * c = z₁ * z₂ * b * c

Tactic:
rw [hz₂.mid_assoc]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
a b : M
⊢ a * b * (z₁ * z₂) = a * b * z₁ * z₂

Tactic:
rw [hz₂.right_assoc]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
b c : M
⊢ z₁ * (z₂ * (b * c)) = z₁ * (z₂ * b * c)

Tactic:
rw [hz₂.left_assoc]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
b c : M
⊢ z₁ * z₂ * (b * c) = z₁ * (z₂ * (b * c))

Tactic:
rw [hz₂.mid_assoc]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
a b : M
⊢ a * (b * z₁ * z₂) = a * (b * (z₁ * z₂))

Tactic:
rw [hz₁.mid_assoc]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
a : M
⊢ a * z₁ * z₂ = a * (z₁ * z₂)

Tactic:
rw [hz₂.right_assoc a z₁]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
a c : M
⊢ a * (z₁ * (z₂ * c)) = a * (z₁ * z₂ * c)

Tactic:
rw [hz₂.mid_assoc]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
a c : M
⊢ a * z₁ * z₂ * c = a * z₁ * (z₂ * c)

Tactic:
rw [hz₂.mid_assoc]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
a b : M
⊢ a * (b * z₁) * z₂ = a * (b * z₁ * z₂)

Tactic:
rw [hz₂.right_assoc]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
a c : M
⊢ a * z₁ * (z₂ * c) = a * (z₁ * (z₂ * c))

Tactic:
rw [hz₁.mid_assoc]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
a : M
⊢ z₂ * (z₁ * a) = a * z₁ * z₂

Tactic:
rw [hz₁.comm, hz₂.comm]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
a : M
⊢ z₂ * z₁ * a = z₂ * (z₁ * a)

Tactic:
rw [hz₁.mid_assoc z₂]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
b c : M
⊢ z₁ * (z₂ * b * c) = z₁ * (z₂ * b) * c

Tactic:
rw [hz₁.left_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isSeparating_op_iff (𝒢 : Set C) : IsSeparating 𝒢.op ↔ IsCoseparating 𝒢

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢.op, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

Tactic:
refine Quiver.Hom.unop_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.op_inj ?_)

Result:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢.op, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : G ∈ 𝒢
h : unop X ⟶ G
⊢ (f.unop ≫ h).op = (g.unop ≫ h).op

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢.op
X Y : C
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

Tactic:
refine Quiver.Hom.op_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.unop_inj ?_)

Result:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢.op
X Y : C
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : Cᵒᵖ
hG : G ∈ 𝒢.op
h : G ⟶ op Y
⊢ (h ≫ f.op).unop = (h ≫ g.op).unop

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢.op
X Y : C
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : Cᵒᵖ
hG : G ∈ 𝒢.op
h : G ⟶ op Y
⊢ (h ≫ f.op).unop = (h ≫ g.op).unop

Tactic:
simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ (Set.mem_op.1 hG) _

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
⊢ IsSeparating 𝒢.op ↔ IsCoseparating 𝒢

Tactic:
refine ⟨fun h𝒢 X Y f g hfg => ?_, fun h𝒢 X Y f g hfg => ?_⟩

Result:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢.op
X Y : C
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢.op, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢.op, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : G ∈ 𝒢
h : unop X ⟶ G
⊢ (f.unop ≫ h).op = (g.unop ≫ h).op

Tactic:
simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ (Set.op_mem_op.2 hG) _

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_smul_average [IsFiniteMeasure μ] (f : α → E) :
    (μ univ).toReal • ⨍ x, f x ∂μ = ∫ x, f x ∂μ

Proof state:
case inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ = 0
⊢ (μ univ).toReal • ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ

Tactic:
rw [hμ, integral_zero_measure, average_zero_measure, smul_zero]

Result:
no goals

Proof state:
case inr.ha
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ μ univ ≠ 0

Tactic:
rwa [Ne, measure_univ_eq_zero]

Result:
no goals

Proof state:
case inr
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ (μ univ).toReal • ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ

Tactic:
rw [average_eq, smul_inv_smul₀]

Result:
case inr.ha
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ (μ univ).toReal ≠ 0

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
⊢ (μ univ).toReal • ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ

Tactic:
rcases eq_or_ne μ 0 with hμ | hμ

Result:
case inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ = 0
⊢ (μ univ).toReal • ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ

case inr
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ (μ univ).toReal • ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ

Proof state:
case inr.ha
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ (μ univ).toReal ≠ 0

Tactic:
refine (ENNReal.toReal_pos ?_ <| measure_ne_top _ _).ne'

Result:
case inr.ha
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ μ univ ≠ 0
-- Mathlib/Algebra/Algebra/Subalgebra/Tower.lean
@[simp]
lemma range_isScalarTower_toAlgHom [CommSemiring R] [CommSemiring A]
    [Algebra R A] (S : Subalgebra R A) :
    LinearMap.range (IsScalarTower.toAlgHom R S A) = Subalgebra.toSubmodule S

Proof state:
case h
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ (∃ y, (algebraMap (↥S) A) y = x✝) ↔ ∃ y, (toSubmodule S).subtype y = x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ LinearMap.range (toAlgHom R (↥S) A) = toSubmodule S

Tactic:
ext

Result:
case h
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ x✝ ∈ LinearMap.range (toAlgHom R (↥S) A) ↔ x✝ ∈ toSubmodule S

Proof state:
case h
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ x✝ ∈ LinearMap.range (toAlgHom R (↥S) A) ↔ x✝ ∈ toSubmodule S

Tactic:
simp only [← Submodule.range_subtype (Subalgebra.toSubmodule S), LinearMap.mem_range,
  IsScalarTower.coe_toAlgHom', Subalgebra.mem_toSubmodule]

Result:
case h
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ (∃ y, (algebraMap (↥S) A) y = x✝) ↔ ∃ y, (toSubmodule S).subtype y = x✝
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem dfoldlM_loop_lt [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (h : i < n) (x) :
    dfoldlM.loop n α f i (Nat.lt_add_right 1 h) x =
      (f ⟨i, h⟩ x) >>= (dfoldlM.loop n α f (i+1) (Nat.add_lt_add_right h 1))

Proof state:
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin n) → α i.castSucc → m (α i.succ)
h : i < n
x : α ⟨i, ⋯⟩
⊢ dfoldlM.loop n α f i ⋯ x = f ⟨i, h⟩ x >>= dfoldlM.loop n α f (i + 1) ⋯

Tactic:
rw [dfoldlM.loop, dif_pos h]

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem coprime_sq_sub_mul_of_even_odd {m n : ℤ} (h : Int.gcd m n = 1) (hm : m % 2 = 0)
    (hn : n % 2 = 1) : Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1

Proof state:
case intro.intro.intro.inr
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(n.gcd m)
hpn : p ∣ n.natAbs
⊢ False

Tactic:
apply mt (Int.dvd_gcd (Int.natCast_dvd.mpr hpn)) hnp

Result:
case intro.intro.intro.inr
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(n.gcd m)
hpn : p ∣ n.natAbs
⊢ ↑p ∣ m
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_inv_log (hx₀ : 0 < x) (hx₁ : x ≠ 1) : x ^ (log x)⁻¹ = exp 1

Proof state:
x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ x ^ (log x)⁻¹ = rexp 1

Tactic:
rw [rpow_def_of_pos hx₀, mul_inv_cancel₀]

Result:
x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ log x ≠ 0

Proof state:
x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ -1 < 0

Tactic:
norm_num

Result:
no goals

Proof state:
x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ log x ≠ 0

Tactic:
exact log_ne_zero.2 ⟨hx₀.ne', hx₁, (hx₀.trans' <| by norm_num).ne'⟩

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_eq_sum_mapIdx (b : ℕ) (L : List ℕ) :
    ofDigits b L = (L.mapIdx fun i a => a * b ^ i).sum

Proof state:
case cons
b hd : ℕ
tl : List ℕ
hl :
  List.foldr (fun x y => ↑x + b * y) 0 tl =
    (List.zipWith
        (Function.curry fun x =>
          match x with
          | (a, i) => a * b ^ i)
        tl (List.range tl.length)).sum
⊢ List.foldr (fun x y => ↑x + b * y) 0 (hd :: tl) =
    (List.zipWith
        (Function.curry fun x =>
          match x with
          | (a, i) => a * b ^ i)
        (hd :: tl) (List.range (hd :: tl).length)).sum

Tactic:
simpa [List.range_succ_eq_map, List.zipWith_map_right, ofDigits_eq_sum_mapIdx_aux] using
  Or.inl hl

Result:
no goals

Proof state:
case nil
b : ℕ
⊢ List.foldr (fun x y => ↑x + b * y) 0 [] =
    (List.zipWith
        (Function.curry fun x =>
          match x with
          | (a, i) => a * b ^ i)
        [] (List.range [].length)).sum

Tactic:
simp

Result:
no goals

Proof state:
b : ℕ
L : List ℕ
⊢ List.foldr (fun x y => ↑x + b * y) 0 L =
    (List.zipWith
        (Function.curry fun x =>
          match x with
          | (a, i) => a * b ^ i)
        L (List.range L.length)).sum

Tactic:
induction' L with hd tl hl

Result:
case nil
b : ℕ
⊢ List.foldr (fun x y => ↑x + b * y) 0 [] =
    (List.zipWith
        (Function.curry fun x =>
          match x with
          | (a, i) => a * b ^ i)
        [] (List.range [].length)).sum

case cons
b hd : ℕ
tl : List ℕ
hl :
  List.foldr (fun x y => ↑x + b * y) 0 tl =
    (List.zipWith
        (Function.curry fun x =>
          match x with
          | (a, i) => a * b ^ i)
        tl (List.range tl.length)).sum
⊢ List.foldr (fun x y => ↑x + b * y) 0 (hd :: tl) =
    (List.zipWith
        (Function.curry fun x =>
          match x with
          | (a, i) => a * b ^ i)
        (hd :: tl) (List.range (hd :: tl).length)).sum

Proof state:
b : ℕ
L : List ℕ
⊢ ofDigits b L = (List.mapIdx (fun i a => a * b ^ i) L).sum

Tactic:
rw [List.mapIdx_eq_zipIdx_map, List.zipIdx_eq_zip_range', List.map_zip_eq_zipWith,
  ofDigits_eq_foldr, ← List.range_eq_range']

Result:
b : ℕ
L : List ℕ
⊢ List.foldr (fun x y => ↑x + b * y) 0 L =
    (List.zipWith
        (Function.curry fun x =>
          match x with
          | (a, i) => a * b ^ i)
        L (List.range L.length)).sum
-- Mathlib/ModelTheory/Substructures.lean
theorem lift_card_closure_le :
    Cardinal.lift.{u, w} #(closure L s) ≤
      max ℵ₀ (Cardinal.lift.{u, w} #s + Cardinal.lift.{w, u} #(Σi, L.Functions i))

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{u, w} #↥((closure L).toFun s) ≤ ℵ₀ ⊔ (lift.{u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i))

Tactic:
rw [← lift_umax]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max w u, w} #↥((closure L).toFun s) ≤ ℵ₀ ⊔ (lift.{max w u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i))

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ ℵ₀ ⊔ #(↑s ⊕ (i : ℕ) × L.Functions i) ≤ ℵ₀ ⊔ (lift.{max w u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i))

Tactic:
rw [mk_sum, lift_umax.{w, u}]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max w u, w} #↥((closure L).toFun s) ≤ ℵ₀ ⊔ (lift.{max w u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i))

Tactic:
refine lift_card_closure_le_card_term.trans (Term.card_le.trans ?_)

Result:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ ℵ₀ ⊔ #(↑s ⊕ (i : ℕ) × L.Functions i) ≤ ℵ₀ ⊔ (lift.{max w u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i))