harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/Subsemiring/MulOpposite.lean
theorem op_closure (s : Set R) : (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Proof state:
case e_a.h
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set R
a : Subsemiring Rᵐᵒᵖ
⊢ a ∈ {a | s ⊆ MulOpposite.op ⁻¹' ↑a} ↔ a ∈ {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Tactic:
exact MulOpposite.unop_surjective.forall

Result:
no goals

Proof state:
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set R
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Tactic:
congr with a

Result:
case e_a.h
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set R
a : Subsemiring Rᵐᵒᵖ
⊢ a ∈ {a | s ⊆ MulOpposite.op ⁻¹' ↑a} ↔ a ∈ {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Proof state:
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set R
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
simp_rw [closure, op_sInf, Set.preimage_setOf_eq, coe_unop]

Result:
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set R
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem isCycleOn_swap [DecidableEq α] (hab : a ≠ b) : (swap a b).IsCycleOn {a, b} :=
  ⟨bijOn_swap (by simp) (by simp), fun x hx y hy => by
    rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hx hy
    obtain rfl | rfl := hx <;> obtain rfl | rfl := hy
    · exact ⟨0, by rw [zpow_zero, coe_one, id]⟩
    · exact ⟨1, by rw [zpow_one, swap_apply_left]⟩
    · exact ⟨1, by rw [zpow_one, swap_apply_right]⟩
    · exact ⟨0, by rw [zpow_zero, coe_one, id]⟩⟩

Proof state:
α : Type u_2
b : α
inst✝ : DecidableEq α
y : α
hab : y ≠ b
⊢ (swap y b ^ 0) y = y

Tactic:
rw [zpow_zero, coe_one, id]

Result:
no goals

Proof state:
case inl.inl
α : Type u_2
b : α
inst✝ : DecidableEq α
y : α
hab : y ≠ b
⊢ (swap y b).SameCycle y y

Tactic:
exact ⟨0, by rw [zpow_zero, coe_one, id]⟩

Result:
no goals

Proof state:
α : Type u_2
a b : α
inst✝ : DecidableEq α
hab : a ≠ b
x : α
hx : x ∈ {a, b}
y : α
hy : y ∈ {a, b}
⊢ (swap a b).SameCycle x y

Tactic:
rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hx hy

Result:
α : Type u_2
a b : α
inst✝ : DecidableEq α
hab : a ≠ b
x : α
hx : x = a ∨ x = b
y : α
hy : y = a ∨ y = b
⊢ (swap a b).SameCycle x y

Proof state:
case inr.inr
α : Type u_2
a : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ (swap a y).SameCycle y y

Tactic:
exact ⟨0, by rw [zpow_zero, coe_one, id]⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DecidableEq α
x y : α
hab : x ≠ y
⊢ (swap x y ^ 1) x = y

Tactic:
rw [zpow_one, swap_apply_left]

Result:
no goals

Proof state:
α : Type u_2
a b : α
inst✝ : DecidableEq α
hab : a ≠ b
⊢ b ∈ {a, b}

Tactic:
simp

Result:
no goals

Proof state:
case inl.inr
α : Type u_2
inst✝ : DecidableEq α
x y : α
hab : x ≠ y
⊢ (swap x y).SameCycle x y

Tactic:
exact ⟨1, by rw [zpow_one, swap_apply_left]⟩

Result:
no goals

Proof state:
α : Type u_2
a b : α
inst✝ : DecidableEq α
hab : a ≠ b
x : α
hx : x = a ∨ x = b
y : α
hy : y = a ∨ y = b
⊢ (swap a b).SameCycle x y

Tactic:
obtain rfl | rfl := hx <;> obtain rfl | rfl := hy

Result:
case inl.inl
α : Type u_2
b : α
inst✝ : DecidableEq α
y : α
hab : y ≠ b
⊢ (swap y b).SameCycle y y

case inl.inr
α : Type u_2
inst✝ : DecidableEq α
x y : α
hab : x ≠ y
⊢ (swap x y).SameCycle x y

case inr.inl
α : Type u_2
inst✝ : DecidableEq α
x y : α
hab : y ≠ x
⊢ (swap y x).SameCycle x y

case inr.inr
α : Type u_2
a : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ (swap a y).SameCycle y y

Proof state:
case inr.inl
α : Type u_2
inst✝ : DecidableEq α
x y : α
hab : y ≠ x
⊢ (swap y x).SameCycle x y

Tactic:
exact ⟨1, by rw [zpow_one, swap_apply_right]⟩

Result:
no goals

Proof state:
α : Type u_2
a b : α
inst✝ : DecidableEq α
hab : a ≠ b
⊢ a ∈ {a, b}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
a : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ (swap a y ^ 0) y = y

Tactic:
rw [zpow_zero, coe_one, id]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DecidableEq α
x y : α
hab : y ≠ x
⊢ (swap y x ^ 1) x = y

Tactic:
rw [zpow_one, swap_apply_right]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProd_restrict_left {s : Set β} (hs : MeasurableSet s) :
    Kernel.restrict κ hs ⊗ₖ η = Kernel.restrict (κ ⊗ₖ η) (hs.prod MeasurableSet.univ)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
hs : MeasurableSet s
⊢ κ.restrict hs ⊗ₖ η = (κ ⊗ₖ η).restrict ⋯

Tactic:
rw [← compProd_restrict]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
hs : MeasurableSet s
⊢ κ.restrict hs ⊗ₖ η = κ.restrict ?hs ⊗ₖ η.restrict ?ht

case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s

case ht
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet Set.univ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
hs : MeasurableSet s
⊢ κ.restrict hs ⊗ₖ η = κ.restrict ?hs ⊗ₖ η.restrict ?ht

Tactic:
congr

Result:
case e_η
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
hs : MeasurableSet s
⊢ η = η.restrict ?ht

Proof state:
case e_η
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
hs : MeasurableSet s
⊢ η = η.restrict ?ht

Tactic:
exact Kernel.restrict_univ.symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_replicate : (replicate n a)[m]? = if m < n then some a else none

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
h : ¬m < n
⊢ (replicate n a).length ≤ m

Tactic:
simpa using h

Result:
no goals

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ (replicate n a)[m]? = if m < n then some a else none

Tactic:
by_cases h : m < n

Result:
case pos
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
h : m < n
⊢ (replicate n a)[m]? = if m < n then some a else none

case neg
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
h : ¬m < n
⊢ (replicate n a)[m]? = if m < n then some a else none

Proof state:
case pos
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
h : m < n
⊢ (replicate n a)[m]? = if m < n then some a else none

Tactic:
rw [getElem?_eq_getElem (by simpa), getElem_replicate, if_pos h]

Result:
no goals

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
h : m < n
⊢ m < (replicate n a).length

Tactic:
simpa

Result:
no goals

Proof state:
case neg
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
h : ¬m < n
⊢ (replicate n a)[m]? = if m < n then some a else none

Tactic:
rw [getElem?_eq_none (by simpa using h), if_neg h]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
theorem inner_pos_of_dist_lt_radius {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s)
    (hp₂ : dist p₂ s.center < s.radius) : 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Proof state:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)

Tactic:
rw [h, mem_sphere] at hp₁

Result:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : dist p₂ s.center = s.radius
hp₂ : dist p₂ s.center < s.radius
h : p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)

Proof state:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : ¬p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)

Tactic:
exact (inner_pos_or_eq_of_dist_le_radius hp₁ hp₂.le).resolve_right h

Result:
no goals

Proof state:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : dist p₂ s.center = s.radius
hp₂ : dist p₂ s.center < s.radius
h : p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)

Tactic:
exact False.elim (hp₂.ne hp₁)

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)

Tactic:
by_cases h : p₁ = p₂

Result:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)

case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : ¬p₁ = p₂
⊢ 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousOn_iSup {f : ι → α → δ} (h : ∀ i, LowerSemicontinuousOn (f i) s) :
    LowerSemicontinuousOn (fun x' => ⨆ i, f i x') s :=
  lowerSemicontinuousOn_ciSup (by simp) h

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
ι : Sort u_3
δ : Type u_4
inst✝ : CompleteLinearOrder δ
f : ι → α → δ
h : ∀ (i : ι), LowerSemicontinuousOn (f i) s
⊢ ∀ x ∈ s, BddAbove (range fun i => f i x)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_iUnion {ι : Sort*} [Countable ι] (s : ι → Set X) :
    dimH (⋃ i, s i) = ⨆ i, dimH (s i)

Proof state:
X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ⨆ i, dimH (s i) < ↑d
this : ∀ (i : ι), μH[↑d] (s i) = 0
⊢ μH[↑d] (⋃ i, s i) ≠ ⊤

Tactic:
rw [measure_iUnion_null this]

Result:
X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ⨆ i, dimH (s i) < ↑d
this : ∀ (i : ι), μH[↑d] (s i) = 0
⊢ 0 ≠ ⊤

Proof state:
X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : μH[↑d] (⋃ i, s i) = ⊤
⊢ ↑d ≤ ⨆ i, dimH (s i)

Tactic:
contrapose! hd

Result:
X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ⨆ i, dimH (s i) < ↑d
⊢ μH[↑d] (⋃ i, s i) ≠ ⊤

Proof state:
X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ⨆ i, dimH (s i) < ↑d
this : ∀ (i : ι), μH[↑d] (s i) = 0
⊢ 0 ≠ ⊤

Tactic:
exact ENNReal.zero_ne_top

Result:
no goals

Proof state:
X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH (⋃ i, s i) = ⨆ i, dimH (s i)

Tactic:
refine le_antisymm (dimH_le fun d hd => ?_) (iSup_le fun i => dimH_mono <| subset_iUnion _ _)

Result:
X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : μH[↑d] (⋃ i, s i) = ⊤
⊢ ↑d ≤ ⨆ i, dimH (s i)

Proof state:
X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
⊢ dimH (⋃ i, s i) = ⨆ i, dimH (s i)

Tactic:
borelize X

Result:
X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH (⋃ i, s i) = ⨆ i, dimH (s i)

Proof state:
X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ⨆ i, dimH (s i) < ↑d
⊢ μH[↑d] (⋃ i, s i) ≠ ⊤

Tactic:
have : ∀ i, μH[d] (s i) = 0 := fun i =>
  hausdorffMeasure_of_dimH_lt ((le_iSup (fun i => dimH (s i)) i).trans_lt hd)

Result:
X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ⨆ i, dimH (s i) < ↑d
this : ∀ (i : ι), μH[↑d] (s i) = 0
⊢ μH[↑d] (⋃ i, s i) ≠ ⊤
-- Mathlib/Data/Complex/Exponential.lean
theorem add_one_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : x + 1 ≤ exp x

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ x + 1 ≤ rexp x

Tactic:
rcases eq_or_lt_of_le hx with (rfl | h)

Result:
case inl
hx : 0 ≤ 0
⊢ 0 + 1 ≤ rexp 0

case inr
x : ℝ
hx : 0 ≤ x
h : 0 < x
⊢ x + 1 ≤ rexp x

Proof state:
case inr
x : ℝ
hx : 0 ≤ x
h : 0 < x
⊢ x + 1 ≤ rexp x

Tactic:
exact (add_one_lt_exp_of_pos h).le

Result:
no goals

Proof state:
case inr
x : ℝ
hx : 0 ≤ x
h : 0 < x
⊢ x + 1 ≤ rexp x

Tactic:
exact (add_one_lt_exp_of_pos h).le

Result:
no goals

Proof state:
case inl
hx : 0 ≤ 0
⊢ 0 + 1 ≤ rexp 0

Tactic:
simp

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ x + 1 ≤ rexp x

Tactic:
rcases eq_or_lt_of_le hx with (rfl | h)

Result:
case inl
hx : 0 ≤ 0
⊢ 0 + 1 ≤ rexp 0

case inr
x : ℝ
hx : 0 ≤ x
h : 0 < x
⊢ x + 1 ≤ rexp x

Proof state:
case inl
hx : 0 ≤ 0
⊢ 0 + 1 ≤ rexp 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Divisibility/Lemmas.lean
lemma pow_dvd_pow_of_add_pow_eq_zero (hp : n + m ≤ p + 1) (h_comm : Commute x y)
    (h : (x + y) ^ n = 0) : x ^ m ∣ y ^ p

Proof state:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ x ^ m ∣ (-y) ^ p * (-1) ^ p

Tactic:
apply dvd_mul_of_dvd_left

Result:
case h
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ x ^ m ∣ (-y) ^ p

Proof state:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ x ^ m ∣ y ^ p

Tactic:
rw [← neg_neg y, neg_pow']

Result:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ x ^ m ∣ (-y) ^ p * (-1) ^ p

Proof state:
case h
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ (x - -y) ^ n = 0

Tactic:
simpa

Result:
no goals

Proof state:
case h
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ x ^ m ∣ (-y) ^ p

Tactic:
apply h_comm.neg_right.pow_dvd_pow_of_sub_pow_eq_zero hp

Result:
case h
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ (x - -y) ^ n = 0
-- Mathlib/Computability/Partrec.lean
theorem vector_mOfFn :
    ∀ {n} {f : Fin n → α →. σ},
      (∀ i, Partrec (f i)) → Partrec fun a : α => Vector.mOfFn fun i => f i a
  | 0, _, _ => const _
  | n + 1, f, hf => by
    simp only [Vector.mOfFn, Nat.add_eq, Nat.add_zero, pure_eq_some, bind_eq_bind]
    exact
      (hf 0).bind
        (Partrec.bind ((vector_mOfFn fun i => hf i.succ).comp fst)
          (Primrec.vector_cons.to_comp.comp (snd.comp fst) snd))

Proof state:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
⊢ Partrec fun a => Vector.mOfFn fun i => f i a

Tactic:
simp only [Vector.mOfFn, Nat.add_eq, Nat.add_zero, pure_eq_some, bind_eq_bind]

Result:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
⊢ Partrec fun a => (f 0 a).bind fun a_1 => (Vector.mOfFn fun i => f i.succ a).bind fun v => Part.some (a_1 ::ᵥ v)

Proof state:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
⊢ Partrec fun a => (f 0 a).bind fun a_1 => (Vector.mOfFn fun i => f i.succ a).bind fun v => Part.some (a_1 ::ᵥ v)

Tactic:
exact
  (hf 0).bind
    (Partrec.bind ((vector_mOfFn fun i => hf i.succ).comp fst)
      (Primrec.vector_cons.to_comp.comp (snd.comp fst) snd))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_intMin_le (x : BitVec w) :
    (intMin w).toInt ≤ x.toInt

Proof state:
w : Nat
x : BitVec (w + 1)
this : 0 < 2 ^ w
⊢ ↑(2 ^ w) < ↑(2 ^ (w + 1))

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ (intMin w).toInt ≤ x.toInt

Tactic:
cases w

Result:
case zero
x : BitVec 0
⊢ (intMin 0).toInt ≤ x.toInt

case succ
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ (intMin (n✝ + 1)).toInt ≤ x.toInt

Proof state:
case zero
x : BitVec 0
⊢ (intMin 0).toInt ≤ x.toInt

case succ
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ (intMin (n✝ + 1)).toInt ≤ x.toInt

Tactic:
case zero => simp [@of_length_zero x]

Result:
case succ
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ (intMin (n✝ + 1)).toInt ≤ x.toInt

Proof state:
w : Nat
x : BitVec (w + 1)
this : 0 < 2 ^ w
⊢ ↑(2 ^ w) = ↑(2 ^ (w + 1)) / 2

Tactic:
omega

Result:
no goals

Proof state:
case succ
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ (intMin (n✝ + 1)).toInt ≤ x.toInt

Tactic:
case succ w =>
  simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod]
  have : 0 < 2 ^ w := Nat.two_pow_pos w
  rw [Int.emod_eq_of_lt (by omega) (by omega)]
  rw [BitVec.toInt_eq_toNat_bmod]
  rw [show (2 ^ w : Nat) = ((2 ^ (w + 1) : Nat) : Int) / 2 by omega]
  apply Int.le_bmod (by omega)

Result:
no goals

Proof state:
w : Nat
x : BitVec (w + 1)
this : 0 < 2 ^ w
⊢ 0 ≤ ↑(2 ^ w)

Tactic:
omega

Result:
no goals

Proof state:
x : BitVec 0
⊢ (intMin 0).toInt ≤ x.toInt

Tactic:
simp [@of_length_zero x]

Result:
no goals

Proof state:
w : Nat
x : BitVec (w + 1)
⊢ (intMin (w + 1)).toInt ≤ x.toInt

Tactic:
simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod]

Result:
w : Nat
x : BitVec (w + 1)
⊢ -(↑(2 ^ w) % ↑(2 ^ (w + 1))) ≤ x.toInt

Proof state:
w : Nat
x : BitVec (w + 1)
⊢ -(↑(2 ^ w) % ↑(2 ^ (w + 1))) ≤ x.toInt

Tactic:
have : 0 < 2 ^ w := Nat.two_pow_pos w

Result:
w : Nat
x : BitVec (w + 1)
this : 0 < 2 ^ w
⊢ -(↑(2 ^ w) % ↑(2 ^ (w + 1))) ≤ x.toInt

Proof state:
w : Nat
x : BitVec (w + 1)
this : 0 < 2 ^ w
⊢ 0 < 2 ^ (w + 1)

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec (w + 1)
this : 0 < 2 ^ w
⊢ -↑(2 ^ w) ≤ (↑x.toNat).bmod (2 ^ (w + 1))

Tactic:
rw [show (2 ^ w : Nat) = ((2 ^ (w + 1) : Nat) : Int) / 2 by omega]

Result:
w : Nat
x : BitVec (w + 1)
this : 0 < 2 ^ w
⊢ -(↑(2 ^ (w + 1)) / 2) ≤ (↑x.toNat).bmod (2 ^ (w + 1))

Proof state:
w : Nat
x : BitVec (w + 1)
this : 0 < 2 ^ w
⊢ -(↑(2 ^ w) % ↑(2 ^ (w + 1))) ≤ x.toInt

Tactic:
rw [Int.emod_eq_of_lt (by omega) (by omega)]

Result:
w : Nat
x : BitVec (w + 1)
this : 0 < 2 ^ w
⊢ -↑(2 ^ w) ≤ x.toInt

Proof state:
w : Nat
x : BitVec (w + 1)
this : 0 < 2 ^ w
⊢ -(↑(2 ^ (w + 1)) / 2) ≤ (↑x.toNat).bmod (2 ^ (w + 1))

Tactic:
apply Int.le_bmod (by omega)

Result:
no goals

Proof state:
w : Nat
x : BitVec (w + 1)
this : 0 < 2 ^ w
⊢ -↑(2 ^ w) ≤ x.toInt

Tactic:
rw [BitVec.toInt_eq_toNat_bmod]

Result:
w : Nat
x : BitVec (w + 1)
this : 0 < 2 ^ w
⊢ -↑(2 ^ w) ≤ (↑x.toNat).bmod (2 ^ (w + 1))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Perm.lean
theorem Perm.refl (l : Array α) : l ~ l

Proof state:
α : Type u_1
l : Array α
⊢ l ~ l

Tactic:
cases l

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ } ~ { toList := toList✝ }

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ } ~ { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Condexp.lean
theorem _root_.MeasureTheory.Integrable.norm_integral_condExpKernel [NormedSpace ℝ F]
    (hf_int : Integrable f μ) :
    Integrable (fun ω => ‖∫ y, f y ∂condExpKernel μ m ω‖) μ

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ‖∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω‖) μ

Tactic:
convert Integrable.norm_integral_condDistrib
  (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
  (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ)) using 1

Result:
no goals

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ‖∫ (y : Ω), f y ∂(condExpKernel μ m) ω‖) μ

Tactic:
rw [condExpKernel_eq]

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ‖∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω‖) μ

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
⊢ Integrable (fun ω => ‖∫ (y : Ω), f y ∂(condExpKernel μ m) ω‖) μ

Tactic:
nontriviality Ω

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ‖∫ (y : Ω), f y ∂(condExpKernel μ m) ω‖) μ
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem ker_quotLeftToQuotSup : RingHom.ker (quotLeftToQuotSup I J) =
    J.map (Ideal.Quotient.mk I)

Proof state:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.ker (quotLeftToQuotSup I J) = map (Ideal.Quotient.mk I) J

Tactic:
simp only [mk_ker, sup_idem, sup_comm, quotLeftToQuotSup, Quotient.factor, ker_quotient_lift,
  map_eq_iff_sup_ker_eq_of_surjective (Ideal.Quotient.mk I) Quotient.mk_surjective, ← sup_assoc]

Result:
no goals
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem Fix.dest_mk (x : F (Fix F)) : Fix.dest (Fix.mk x) = x

Proof state:
F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = x

Tactic:
conv =>
  rhs
  rw [← id_map x]

Result:
F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x

Proof state:
case e_a.h
F : Type u → Type u
q : QPF F
x✝ : F (Fix F)
x : Fix F
⊢ (mk ∘ dest) x = id x

Tactic:
apply Fix.mk_dest

Result:
no goals

Proof state:
F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ rec (Functor.map mk) (mk x) = x

Tactic:
rw [Fix.rec_eq, ← Fix.dest, ← comp_map]

Result:
F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = x

Proof state:
F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x

Tactic:
congr with x

Result:
case e_a.h
F : Type u → Type u
q : QPF F
x✝ : F (Fix F)
x : Fix F
⊢ (mk ∘ dest) x = id x

Proof state:
F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ (mk x).dest = x

Tactic:
unfold Fix.dest

Result:
F : Type u → Type u
q : QPF F
x : F (Fix F)
⊢ rec (Functor.map mk) (mk x) = x