harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Image.lean
theorem range_ite_subset' {p : Prop} [Decidable p] {f g : α → β} :
    range (if p then f else g) ⊆ range f ∪ range g

Proof state:
case neg
α : Type u_1
β : Type u_2
p : Prop
inst✝ : Decidable p
f g : α → β
h : ¬p
⊢ range g ⊆ range f ∪ range g

Tactic:
exact subset_union_right

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
p : Prop
inst✝ : Decidable p
f g : α → β
h : ¬p
⊢ range (if p then f else g) ⊆ range f ∪ range g

Tactic:
rw [if_neg h]

Result:
case neg
α : Type u_1
β : Type u_2
p : Prop
inst✝ : Decidable p
f g : α → β
h : ¬p
⊢ range g ⊆ range f ∪ range g

Proof state:
α : Type u_1
β : Type u_2
p : Prop
inst✝ : Decidable p
f g : α → β
⊢ range (if p then f else g) ⊆ range f ∪ range g

Tactic:
by_cases h : p

Result:
case pos
α : Type u_1
β : Type u_2
p : Prop
inst✝ : Decidable p
f g : α → β
h : p
⊢ range (if p then f else g) ⊆ range f ∪ range g

case neg
α : Type u_1
β : Type u_2
p : Prop
inst✝ : Decidable p
f g : α → β
h : ¬p
⊢ range (if p then f else g) ⊆ range f ∪ range g

Proof state:
case pos
α : Type u_1
β : Type u_2
p : Prop
inst✝ : Decidable p
f g : α → β
h : p
⊢ range (if p then f else g) ⊆ range f ∪ range g

Tactic:
rw [if_pos h]

Result:
case pos
α : Type u_1
β : Type u_2
p : Prop
inst✝ : Decidable p
f g : α → β
h : p
⊢ range f ⊆ range f ∪ range g

Proof state:
case pos
α : Type u_1
β : Type u_2
p : Prop
inst✝ : Decidable p
f g : α → β
h : p
⊢ range f ⊆ range f ∪ range g

Tactic:
exact subset_union_left

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
lemma nndist_pi_le_iff {f g : ∀ b, π b} {r : ℝ≥0} :
    nndist f g ≤ r ↔ ∀ b, nndist (f b) (g b) ≤ r

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
⊢ nndist f g ≤ r ↔ ∀ (b : β), nndist (f b) (g b) ≤ r

Tactic:
simp [nndist_pi_def]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem map_mem_closure₂ {f : X → Y → Z} {x : X} {y : Y} {s : Set X} {t : Set Y} {u : Set Z}
    (hf : Continuous (uncurry f)) (hx : x ∈ closure s) (hy : y ∈ closure t)
    (h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u) : f x y ∈ closure u :=
  have H₁ : (x, y) ∈ closure (s ×ˢ t)

Proof state:
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y → Z
x : X
y : Y
s : Set X
t : Set Y
u : Set Z
hf : Continuous (uncurry f)
hx : x ∈ closure s
hy : y ∈ closure t
h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u
⊢ (x, y) ∈ closure (s ×ˢ t)

Tactic:
simpa only [closure_prod_eq] using mk_mem_prod hx hy

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma one_lt_two_pow' (n : ℕ) : 1 < 2 ^ (n + 1) := one_lt_pow n.succ_ne_zero (by decide)

Proof state:
n : ℕ
⊢ 1 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem neighborFinset_eq_filter {v : V} [DecidableRel G.Adj] :
    G.neighborFinset v = ({w | G.Adj v w} : Finset _)

Proof state:
case h
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
v : V
inst✝ : DecidableRel G.Adj
a✝ : V
⊢ a✝ ∈ G.neighborFinset v ↔ a✝ ∈ filter (fun w => G.Adj v w) univ

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
v : V
inst✝ : DecidableRel G.Adj
⊢ G.neighborFinset v = filter (fun w => G.Adj v w) univ

Tactic:
ext

Result:
case h
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
v : V
inst✝ : DecidableRel G.Adj
a✝ : V
⊢ a✝ ∈ G.neighborFinset v ↔ a✝ ∈ filter (fun w => G.Adj v w) univ
-- Mathlib/CategoryTheory/Generator/Preadditive.lean
theorem isCoseparator_iff_faithful_preadditiveYonedaObj (G : C) :
    IsCoseparator G ↔ (preadditiveYonedaObj G).Faithful

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsCoseparator G ↔ (preadditiveYonedaObj G).Faithful

Tactic:
rw [isCoseparator_iff_faithful_preadditiveYoneda, preadditiveYoneda_obj]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ (preadditiveYonedaObj G ⋙ forget₂ (ModuleCat (End G)) AddCommGrp).Faithful ↔ (preadditiveYonedaObj G).Faithful

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ (preadditiveYonedaObj G ⋙ forget₂ (ModuleCat (End G)) AddCommGrp).Faithful ↔ (preadditiveYonedaObj G).Faithful

Tactic:
exact ⟨fun h => Functor.Faithful.of_comp _ (forget₂ _ AddCommGrp.{v}),
  fun h => Functor.Faithful.comp _ _⟩

Result:
no goals
-- Mathlib/Data/PFunctor/Multivariate/W.lean
theorem wDest'_wMk' {α : TypeVec n} (x : P (α.append1 (P.W α))) : P.wDest' (P.wMk' x) = x

Proof state:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α ::: P.W α
⊢ P.wDest' (P.wMk' ⟨a, f⟩) = ⟨a, f⟩

Tactic:
rw [wMk', wDest'_wMk, split_dropFun_lastFun]

Result:
no goals

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : ↑P (α ::: P.W α)
⊢ P.wDest' (P.wMk' x) = x

Tactic:
obtain ⟨a, f⟩ := x

Result:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α ::: P.W α
⊢ P.wDest' (P.wMk' ⟨a, f⟩) = ⟨a, f⟩
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_range_div' (n : ℕ) (f : ℕ → G) :
    ((range n).map fun k ↦ f k / f (k + 1)).prod = f 0 / f n

Proof state:
case succ
G : Type u_7
inst✝ : Group G
f : ℕ → G
n : ℕ
h : (map (fun k => f k / f (k + 1)) (range n)).prod = f 0 / f n
⊢ (map (fun k => f k / f (k + 1)) (range (n + 1))).prod = f 0 / f (n + 1)

Tactic:
rw [range_succ, map_append, map_singleton, prod_append, prod_singleton, h, div_mul_div_cancel]

Result:
no goals

Proof state:
case zero
G : Type u_7
inst✝ : Group G
f : ℕ → G
⊢ (map (fun k => f k / f (k + 1)) (range 0)).prod = f 0 / f 0

Tactic:
exact (div_self' (f 0)).symm

Result:
no goals

Proof state:
G : Type u_7
inst✝ : Group G
n : ℕ
f : ℕ → G
⊢ (map (fun k => f k / f (k + 1)) (range n)).prod = f 0 / f n

Tactic:
induction n with
| zero => exact (div_self' (f 0)).symm
| succ n h =>
  rw [range_succ, map_append, map_singleton, prod_append, prod_singleton, h, div_mul_div_cancel]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/OfSequence.lean
@[simp]
lemma ofOpSequence_map_homOfLE_succ (n : ℕ) :
    (ofOpSequence f).map (homOfLE (Nat.le_add_right n 1)).op = f n

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ℕ → C
f : (n : ℕ) → X (n + 1) ⟶ X n
n : ℕ
⊢ (ofOpSequence f).map (homOfLE ⋯).op = f n

Tactic:
simp [ofOpSequence]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi : cos π = -1

Proof state:
⊢ 2 * 0 ^ 2 - 1 = -1

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ cos π = -1

Tactic:
rw [← mul_div_cancel_left₀ π (two_ne_zero' ℝ), mul_div_assoc, cos_two_mul, cos_pi_div_two]

Result:
⊢ 2 * 0 ^ 2 - 1 = -1
-- Mathlib/Topology/ContinuousOn.lean
lemma Filter.EventuallyEq.mem_interior {x : α} {s t : Set α} (hst : s =ᶠ[𝓝 x] t)
    (h : x ∈ interior s) : x ∈ interior t

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hst : 𝓝[s] x = 𝓝[t] x
h : x ∈ interior s
⊢ x ∈ interior t

Tactic:
simpa [mem_interior_iff_mem_nhds, ← nhdsWithin_eq_nhds, hst] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hst : s =ᶠ[𝓝 x] t
h : x ∈ interior s
⊢ x ∈ interior t

Tactic:
rw [← nhdsWithin_eq_iff_eventuallyEq] at hst

Result:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hst : 𝓝[s] x = 𝓝[t] x
h : x ∈ interior s
⊢ x ∈ interior t
-- Mathlib/Topology/ContinuousOn.lean
/-- Writing a punctured neighborhood filter as a sup of left and right filters. -/
lemma punctured_nhds_eq_nhdsWithin_sup_nhdsWithin [LinearOrder α] {x : α} :
    𝓝[≠] x = 𝓝[<] x ⊔ 𝓝[>] x

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
x : α
⊢ 𝓝[≠] x = 𝓝[<] x ⊔ 𝓝[>] x

Tactic:
rw [← Iio_union_Ioi, nhdsWithin_union]

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Real.lean
lemma Icc_isInteriorPoint_interior {p : Set.Icc x y} (hp : x < p.val ∧ p.val < y) :
    (𝓡∂ 1).IsInteriorPoint p

Proof state:
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : x < ↑p ∧ ↑p < y
⊢ (𝓡∂ 1).IsInteriorPoint p

Tactic:
rw [ModelWithCorners.IsInteriorPoint, extChartAt, Icc_chartedSpaceChartAt_of_le_top hp.2,
  interior_range_modelWithCornersEuclideanHalfSpace]

Result:
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : x < ↑p ∧ ↑p < y
⊢ ↑((IccLeftChart x y).extend (𝓡∂ 1)) p ∈ {y | 0 < y 0}

Proof state:
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : x < ↑p ∧ ↑p < y
⊢ ↑((IccLeftChart x y).extend (𝓡∂ 1)) p ∈ {y | 0 < y 0}

Tactic:
exact IccLeftChart_extend_interior_pos hp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem integral_fn_integral_sub_comp ⦃f g : γ → E⦄ (F : E → E')
    (hf : Integrable f ((η ∘ₖ κ) a)) (hg : Integrable g ((η ∘ₖ κ) a)) :
    ∫ x, F (∫ y, f y - g y ∂η x) ∂κ a = ∫ x, F (∫ y, f y ∂η x - ∫ y, g y ∂η x) ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
⊢ (fun x => F (∫ (y : γ), f y - g y ∂η x)) =ᶠ[ae (κ a)] fun x => F (∫ (y : γ), f y ∂η x - ∫ (y : γ), g y ∂η x)

Tactic:
filter_upwards [hf.ae_of_comp, hg.ae_of_comp] with _ h2f h2g

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
h2g : Integrable g (η a✝)
⊢ F (∫ (y : γ), f y - g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ - ∫ (y : γ), g y ∂η a✝)

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
a✝ : β
h2f : Integrable f (η a✝)
h2g : Integrable g (η a✝)
⊢ F (∫ (y : γ), f y - g y ∂η a✝) = F (∫ (y : γ), f y ∂η a✝ - ∫ (y : γ), g y ∂η a✝)

Tactic:
simp [integral_sub h2f h2g]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
⊢ ∫ (x : β), F (∫ (y : γ), f y - g y ∂η x) ∂κ a = ∫ (x : β), F (∫ (y : γ), f y ∂η x - ∫ (y : γ), g y ∂η x) ∂κ a

Tactic:
refine integral_congr_ae ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝² : NormedSpace ℝ E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : Integrable f ((η ∘ₖ κ) a)
hg : Integrable g ((η ∘ₖ κ) a)
⊢ (fun x => F (∫ (y : γ), f y - g y ∂η x)) =ᶠ[ae (κ a)] fun x => F (∫ (y : γ), f y ∂η x - ∫ (y : γ), g y ∂η x)
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_le_prod_of_mem {l : List (Perm α)} (h : f ∈ l) (hl : l.Pairwise Disjoint) :
    f.support ≤ l.prod.support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
x : α
hx : x ∈ f.support
⊢ x ∈ l.prod.support

Tactic:
rwa [mem_support, ← eq_on_support_mem_disjoint h hl _ hx, ← mem_support]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
⊢ f.support ≤ l.prod.support

Tactic:
intro x hx

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
x : α
hx : x ∈ f.support
⊢ x ∈ l.prod.support
-- Mathlib/Topology/Sequences.lean
theorem SequentialSpace.sup {X} {t₁ t₂ : TopologicalSpace X}
    (h₁ : @SequentialSpace X t₁) (h₂ : @SequentialSpace X t₂) :
    @SequentialSpace X (t₁ ⊔ t₂)

Proof state:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : SequentialSpace X
h₂ : SequentialSpace X
⊢ SequentialSpace X

Tactic:
exact .iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Sphere.lean
theorem concyclic_or_collinear_of_two_zsmul_oangle_eq {p₁ p₂ p₃ p₄ : P}
    (h : (2 : ℤ) • ∡ p₁ p₂ p₄ = (2 : ℤ) • ∡ p₁ p₃ p₄) :
    Concyclic ({p₁, p₂, p₃, p₄} : Set P) ∨ Collinear ℝ ({p₁, p₂, p₃, p₄} : Set P)

Proof state:
case inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
⊢ Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}

Tactic:
exact Or.inr hc

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
⊢ Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}

Tactic:
rcases cospherical_or_collinear_of_two_zsmul_oangle_eq h with (hc | hc)

Result:
case inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Cospherical {p₁, p₂, p₃, p₄}
⊢ Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}

case inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
⊢ Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}

Proof state:
case inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Cospherical {p₁, p₂, p₃, p₄}
⊢ Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}

Tactic:
exact Or.inl ⟨hc, coplanar_of_fact_finrank_eq_two _⟩

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma mul_div_cancel_left (h : IsUnit a) (b : α) : a * b / a = b

Proof state:
α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a * b / a = b

Tactic:
rw [mul_comm, h.mul_div_cancel_right]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
lemma iInf_unique [Unique ι] (f : ι → α) : ⨅ i, f i = f default

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Unique ι
f : ι → α
⊢ ⨅ i, f i = f default

Tactic:
simp only [congr_arg f (Unique.eq_default _), iInf_const]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma setIntegral_toReal_rnDeriv' [SigmaFinite μ] [HaveLebesgueDecomposition μ ν]
    (hμν : μ ≪ ν) {s : Set α} (hs : MeasurableSet s) :
    ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = (μ s).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (μ s).toReal

Tactic:
rw [setIntegral_toReal_rnDeriv_eq_withDensity' hs, Measure.withDensity_rnDeriv_eq _ _ hμν]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem _root_.Real.toNNReal_inv {x : ℝ} : Real.toNNReal x⁻¹ = (Real.toNNReal x)⁻¹

Proof state:
case inl
x : ℝ
hx : 0 ≤ x
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
nth_rw 1 [← Real.coe_toNNReal x hx]

Result:
case inl
x : ℝ
hx : 0 ≤ x
⊢ (↑x.toNNReal)⁻¹.toNNReal = x.toNNReal⁻¹

Proof state:
case inr
x : ℝ
hx : x ≤ 0
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
rw [toNNReal_eq_zero.mpr hx, inv_zero, toNNReal_eq_zero.mpr (inv_nonpos.mpr hx)]

Result:
no goals

Proof state:
case inl
x : ℝ
hx : 0 ≤ x
⊢ (↑x.toNNReal)⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
rw [← NNReal.coe_inv, Real.toNNReal_coe]

Result:
no goals

Proof state:
x : ℝ
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
rcases le_total 0 x with hx | hx

Result:
case inl
x : ℝ
hx : 0 ≤ x
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹

case inr
x : ℝ
hx : x ≤ 0
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹
-- Mathlib/Combinatorics/SimpleGraph/Hasse.lean
theorem hasse_preconnected_of_pred [PredOrder α] [IsPredArchimedean α] : (hasse α).Preconnected :=
  fun a b => by
  rw [reachable_iff_reflTransGen, ← reflTransGen_swap]
  exact
    reflTransGen_of_pred _ (fun c hc => Or.inl <| pred_covBy_of_not_isMin hc.1.not_isMin)
      fun c hc => Or.inr <| pred_covBy_of_not_isMin hc.1.not_isMin

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : α
⊢ (hasse α).Reachable a b

Tactic:
rw [reachable_iff_reflTransGen, ← reflTransGen_swap]

Result:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : α
⊢ ReflTransGen (Function.swap (hasse α).Adj) b a

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : α
⊢ ReflTransGen (Function.swap (hasse α).Adj) b a

Tactic:
exact
  reflTransGen_of_pred _ (fun c hc => Or.inl <| pred_covBy_of_not_isMin hc.1.not_isMin)
    fun c hc => Or.inr <| pred_covBy_of_not_isMin hc.1.not_isMin

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem piecewise_univ (f g : α →ₛ β) : piecewise univ MeasurableSet.univ f g = f :=
  coe_injective <| by simp

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ ⇑(piecewise univ ⋯ f g) = ⇑f

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem invFunOn_pos (h : ∃ a ∈ s, f a = b) : invFunOn f s b ∈ s ∧ f (invFunOn f s b) = b

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ∃ a ∈ s, f a = b
⊢ Classical.choose h ∈ s ∧ f (Classical.choose h) = b

Tactic:
exact Classical.choose_spec h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ∃ a ∈ s, f a = b
⊢ invFunOn f s b ∈ s ∧ f (invFunOn f s b) = b

Tactic:
rw [invFunOn, dif_pos h]

Result:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ∃ a ∈ s, f a = b
⊢ Classical.choose h ∈ s ∧ f (Classical.choose h) = b
-- Mathlib/Data/Matrix/Basis.lean
theorem apply_of_col_ne (i i' : m) {j j' : n} (hj : j ≠ j') (a : α) :
    stdBasisMatrix i j a i' j' = 0

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i i' : m
j j' : n
hj : j ≠ j'
a : α
⊢ stdBasisMatrix i j a i' j' = 0

Tactic:
simp [hj]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Field.lean
theorem one_div_pos_of_nat {n : ℕ} : 0 < 1 / ((n : α) + 1)

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
n : ℕ
⊢ 0 < 1 / (↑n + 1)

Tactic:
rw [one_div]

Result:
α : Type u_1
inst✝ : LinearOrderedSemifield α
n : ℕ
⊢ 0 < (↑n + 1)⁻¹

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
n : ℕ
⊢ 0 < (↑n + 1)⁻¹

Tactic:
exact inv_pos_of_nat

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem mul_eq_zero_of_ne_zero_imp_eq_zero {a b : M₀} (h : a ≠ 0 → b = 0) : a * b = 0

Proof state:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : a = 0
⊢ a * b = 0

Tactic:
rw [ha, zero_mul]

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
⊢ a * b = 0

Tactic:
exact if ha : a = 0 then by rw [ha, zero_mul] else by rw [h ha, mul_zero]

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
⊢ a * b = 0

Tactic:
have : Decidable (a = 0) := Classical.propDecidable (a = 0)

Result:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
⊢ a * b = 0

Proof state:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : ¬a = 0
⊢ a * b = 0

Tactic:
rw [h ha, mul_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean
lemma Hom.toIsometry_injective (V W : QuadraticModuleCat.{v} R) :
    Function.Injective (Hom.toIsometry : Hom V W → _) :=
  fun ⟨f⟩ ⟨g⟩ _ => by congr

Proof state:
R : Type u
inst✝ : CommRing R
V W : QuadraticModuleCat R
x✝² x✝¹ : V.Hom W
f g : V.form →qᵢ W.form
x✝ : { toIsometry' := f }.toIsometry = { toIsometry' := g }.toIsometry
⊢ { toIsometry' := f } = { toIsometry' := g }

Tactic:
congr

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem shiftRight_coe_nat (m n : ℕ) : (m : ℤ) >>> (n : ℤ) = m >>> n

Proof state:
m n : ℕ
⊢ ↑m >>> ↑n = ↑(m >>> n)

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Iio_add_one_eq_Iic (b : α) : Iio (b + 1) = Iic b

Proof state:
α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrderBot α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
b : α
⊢ Iio (b + 1) = Iic b

Tactic:
simpa [succ_eq_add_one] using Iio_succ_eq_Iic b

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem evenOdd_comap_involute (n : ZMod 2) :
    (evenOdd Q n).comap (involute : CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q).toLinearMap =
      evenOdd Q n

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ Submodule.comap involute.toLinearMap (evenOdd Q n) = evenOdd Q n

Tactic:
rw [← submodule_map_involute_eq_comap, evenOdd_map_involute]

Result:
no goals
-- Mathlib/Order/Bounded.lean
theorem unbounded_le_inter_not_le [SemilatticeSup α] (a : α) :
    Unbounded (· ≤ ·) (s ∩ { b | ¬b ≤ a }) ↔ Unbounded (· ≤ ·) s

Proof state:
α : Type u_1
s : Set α
inst✝ : SemilatticeSup α
a : α
⊢ Unbounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | ¬b ≤ a}) ↔ Unbounded (fun x1 x2 => x1 ≤ x2) s

Tactic:
rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]

Result:
α : Type u_1
s : Set α
inst✝ : SemilatticeSup α
a : α
⊢ Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | ¬b ≤ a}) ↔ Bounded (fun x1 x2 => x1 ≤ x2) s

Proof state:
α : Type u_1
s : Set α
inst✝ : SemilatticeSup α
a : α
⊢ Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | ¬b ≤ a}) ↔ Bounded (fun x1 x2 => x1 ≤ x2) s

Tactic:
exact bounded_le_inter_not_le a

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem cosh_log {x : ℝ} (hx : 0 < x) : cosh (log x) = (x + x⁻¹) / 2

Proof state:
x : ℝ
hx : 0 < x
⊢ cosh (log x) = (x + x⁻¹) / 2

Tactic:
rw [cosh_eq, exp_neg, exp_log hx]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem isSymm_compl [Zero α] [One α] (h : A.IsSymm) : A.compl.IsSymm

Proof state:
V : Type u_1
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsSymm
⊢ A.compl.IsSymm

Tactic:
ext

Result:
case a
V : Type u_1
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsSymm
i✝ j✝ : V
⊢ A.complᵀ i✝ j✝ = A.compl i✝ j✝

Proof state:
case a
V : Type u_1
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsSymm
i✝ j✝ : V
⊢ A.complᵀ i✝ j✝ = A.compl i✝ j✝

Tactic:
simp [compl, h.apply, eq_comm]

Result:
no goals