harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
lemma Measurable.iff (hp : Measurable p) (hq : Measurable q) : Measurable fun a ↦ p a ↔ q a :=
  measurableSet_setOf.1 <| by simp_rw [iff_iff_implies_and_implies]; exact hq.setOf.bihimp hp.setOf

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ MeasurableSet {a | (p a → q a) ∧ (q a → p a)}

Tactic:
exact hq.setOf.bihimp hp.setOf

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ MeasurableSet {a | p a ↔ q a}

Tactic:
simp_rw [iff_iff_implies_and_implies]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ MeasurableSet {a | (p a → q a) ∧ (q a → p a)}
-- Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean
theorem Real.hasSum_arctan {x : ℝ} (hx : ‖x‖ < 1) :
    HasSum (fun n : ℕ => (-1) ^ n * x ^ (2 * n + 1) / ↑(2 * n + 1)) (arctan x) :=
  mod_cast Complex.hasSum_arctan (z := x) (by simpa)

Proof state:
x : ℝ
hx : ‖x‖ < 1
⊢ ‖↑x‖ < 1

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldlM_push' [Monad m] [LawfulMonad m] (l : Array α) (a : α) (f : β → α → m β) (b)
    (w : stop = l.size + 1) :
    (l.push a).foldlM f b 0 stop = l.foldlM f b >>= fun b => f b a

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
a : α
f : β → α → m β
b : β
⊢ foldlM f b (l.push a) 0 (l.size + 1) = do
    let b ← foldlM f b l
    f b a

Tactic:
simp [← append_singleton]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
stop : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
a : α
f : β → α → m β
b : β
w : stop = l.size + 1
⊢ foldlM f b (l.push a) 0 stop = do
    let b ← foldlM f b l
    f b a

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
a : α
f : β → α → m β
b : β
⊢ foldlM f b (l.push a) 0 (l.size + 1) = do
    let b ← foldlM f b l
    f b a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_map_hom (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : Array α)
    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
    (l.map g).foldr f' (g a) = g (l.foldr f a)

Proof state:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ List.foldr f' (g a) (List.map g toList✝) = g (List.foldr f a toList✝)

Tactic:
rw [List.foldr_map_hom _ _ _ _ _ h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
l : Array α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
⊢ foldr f' (g a) (map g l) = g (foldr f a l)

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ foldr f' (g a) (map g { toList := toList✝ }) = g (foldr f a { toList := toList✝ })

Proof state:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ foldr f' (g a) (map g { toList := toList✝ }) = g (foldr f a { toList := toList✝ })

Tactic:
simp

Result:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ List.foldr f' (g a) (List.map g toList✝) = g (List.foldr f a toList✝)
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem disjoint_closedBall_of_lt_infEdist {r : ℝ≥0∞} (h : r < infEdist x s) :
    Disjoint (closedBall x r) s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEdist x s
y : α
hy : y ∈ closedBall x r
h'y : y ∈ s
⊢ infEdist x s < infEdist x s

Tactic:
calc
  infEdist x s ≤ edist x y := infEdist_le_edist_of_mem h'y
  _ ≤ r := by rwa [mem_closedBall, edist_comm] at hy
  _ < infEdist x s := h

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEdist x s
y : α
hy : y ∈ closedBall x r
h'y : y ∈ s
⊢ False

Tactic:
apply lt_irrefl (infEdist x s)

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEdist x s
y : α
hy : y ∈ closedBall x r
h'y : y ∈ s
⊢ infEdist x s < infEdist x s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEdist x s
⊢ Disjoint (closedBall x r) s

Tactic:
rw [disjoint_left]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEdist x s
⊢ ∀ ⦃a : α⦄, a ∈ closedBall x r → a ∉ s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEdist x s
⊢ ∀ ⦃a : α⦄, a ∈ closedBall x r → a ∉ s

Tactic:
intro y hy h'y

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEdist x s
y : α
hy : y ∈ closedBall x r
h'y : y ∈ s
⊢ False

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEdist x s
y : α
hy : y ∈ closedBall x r
h'y : y ∈ s
⊢ edist x y ≤ r

Tactic:
rwa [mem_closedBall, edist_comm] at hy

Result:
no goals
-- Mathlib/ModelTheory/DirectLimit.lean
theorem lift_quotient_mk'_sigma_mk' {i} (x : G i) : lift L ι G f g Hg ⟦.mk f i x⟧ = (g i) x

Proof state:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
i : ι
x : G i
⊢ (lift L ι G f g Hg).toFun ⟦Structure.Sigma.mk f i x⟧ = (g i) x

Tactic:
simp only [lift, Quotient.lift_mk]

Result:
no goals

Proof state:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
i : ι
x : G i
⊢ (lift L ι G f g Hg) ⟦Structure.Sigma.mk f i x⟧ = (g i) x

Tactic:
change (lift L ι G f g Hg).toFun ⟦.mk f i x⟧ = _

Result:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
i : ι
x : G i
⊢ (lift L ι G f g Hg).toFun ⟦Structure.Sigma.mk f i x⟧ = (g i) x
-- Mathlib/LinearAlgebra/Basis/Bilinear.lean
theorem sum_repr_mul_repr_mulₛₗ {B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (x y) :
    ((b₁.repr x).sum fun i xi => (b₂.repr y).sum fun j yj => ρ₁₂ xi • σ₁₂ yj • B (b₁ i) (b₂ j)) =
      B x y

Proof state:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ ((b₁.repr x).sum fun i xi => (b₂.repr y).sum fun j yj => ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) = (B x) y

Tactic:
conv_rhs => rw [← b₁.linearCombination_repr x, ← b₂.linearCombination_repr y]

Result:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ ((b₁.repr x).sum fun i xi => (b₂.repr y).sum fun j yj => ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) =
    (B ((Finsupp.linearCombination R ⇑b₁) (b₁.repr x))) ((Finsupp.linearCombination S ⇑b₂) (b₂.repr y))

Proof state:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ ((b₁.repr x).sum fun i xi => (b₂.repr y).sum fun j yj => ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) =
    (B ((Finsupp.linearCombination R ⇑b₁) (b₁.repr x))) ((Finsupp.linearCombination S ⇑b₂) (b₂.repr y))

Tactic:
simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂, map_sum, LinearMap.map_smulₛₗ₂,
  LinearMap.map_smulₛₗ]

Result:
no goals
-- Mathlib/Order/SuccPred/Tree.lean
@[simp]
lemma isAtom_findAtom_iff {r : α} :
    IsAtom (findAtom r) ↔ r ≠ ⊥ where
  mpr := isAtom_findAtom
  mp h nh

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
nh : r = ⊥
h : IsAtom ⊥
⊢ False

Tactic:
exact h.1 rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : IsAtom (findAtom r)
nh : r = ⊥
⊢ False

Tactic:
simp only [nh, findAtom_bot] at h

Result:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
nh : r = ⊥
h : IsAtom ⊥
⊢ False
-- Mathlib/Data/DFinsupp/Defs.lean
theorem update_eq_sub_add_single {β : ι → Type*} [∀ i, AddGroup (β i)] (f : Π₀ i, β i) (i : ι)
    (b : β i) : f.update i b = f - single i (f i) + single i b

Proof state:
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update i b = f - single i (f i) + single i b

Tactic:
rw [update_eq_erase_add_single f i b, erase_eq_sub_single f i]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Basic.lean
theorem inter_assoc (s₁ s₂ s₃ : Finset α) : s₁ ∩ s₂ ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) :=
  ext fun _ => by simp only [mem_inter, and_assoc]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finset α
x✝ : α
⊢ x✝ ∈ s₁ ∩ s₂ ∩ s₃ ↔ x✝ ∈ s₁ ∩ (s₂ ∩ s₃)

Tactic:
simp only [mem_inter, and_assoc]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem Tendsto.isCompact_insert_range_of_cocompact {f : X → Y} {y}
    (hf : Tendsto f (cocompact X) (𝓝 y)) (hfc : Continuous f) : IsCompact (insert y (range f))

Proof state:
case h.inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hfc : Continuous f
l : Filter Y
hne : l.NeBot
s t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hf : Tendsto f (cocompact X) (𝓝 y)
hle : l ≤ 𝓟 (insert y (range f))
hsy : s ∈ 𝓝 y
⊢ y ∈ f '' K

case h.inr.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
x : X
hyt : f x ∈ t
⊢ f x ∈ f '' K

Tactic:
exacts [(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim,
  mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]

Result:
no goals

Proof state:
case neg.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
rcases mem_cocompact.1 (hf hsy) with ⟨K, hKc, hKs⟩

Result:
case neg.intro.intro.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Proof state:
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
hy : ClusterPt y l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
exact ⟨y, Or.inl rfl, hy⟩

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropAt_of_mem_maximalAtlas [HasGroupoid M G] (hG : G.LocalInvariantProp G Q)
    (hQ : ∀ y, Q id univ y) (he : e ∈ maximalAtlas M G) (hx : x ∈ e.source) : LiftPropAt Q e x

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
x : M
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.source
⊢ Q (↑(PartialHomeomorph.refl H) ∘ ↑e ∘ ↑e.symm) (↑e.symm ⁻¹' univ) (↑e x)

Tactic:
exact hG.congr' (e.eventually_right_inverse' hx) (hQ _)

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
x : M
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.source
⊢ LiftPropAt Q (↑e) x

Tactic:
simp_rw [LiftPropAt, hG.liftPropWithinAt_indep_chart he hx G.id_mem_maximalAtlas (mem_univ _),
  (e.continuousAt hx).continuousWithinAt, true_and]

Result:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
x : M
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.source
⊢ Q (↑(PartialHomeomorph.refl H) ∘ ↑e ∘ ↑e.symm) (↑e.symm ⁻¹' univ) (↑e x)
-- Mathlib/Data/Sum/Interval.lean
lemma Ioo_inr_inr :
    Ioo (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Ioo b₁ b₂).map (Embedding.inr.trans toLex.toEmbedding)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Ioo (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioo b₁ b₂))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Ioo (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Ioo b₁ b₂)

Tactic:
rw [← Finset.map_map]

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Ioo (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioo b₁ b₂))
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_nonpos (ha : a ≤ 0) : ⌊a⌋ ≤ 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : a ≤ 0
⊢ ↑⌊a⌋ ≤ 0

Tactic:
exact (floor_le a).trans ha

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : a ≤ 0
⊢ ⌊a⌋ ≤ 0

Tactic:
rw [← @cast_le α, Int.cast_zero]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : a ≤ 0
⊢ ↑⌊a⌋ ≤ 0
-- Mathlib/Topology/Basic.lean
theorem mem_closure_of_mem_closure_union (h : x ∈ closure (s₁ ∪ s₂))
    (h₁ : s₁ᶜ ∈ 𝓝 x) : x ∈ closure s₂

Proof state:
X : Type u
x : X
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥

Tactic:
rwa [← sup_principal, inf_sup_left, inf_principal_eq_bot.mpr h₁, bot_sup_eq] at h

Result:
no goals

Proof state:
X : Type u
x : X
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h : x ∈ closure (s₁ ∪ s₂)
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ x ∈ closure s₂

Tactic:
rw [mem_closure_iff_nhds_ne_bot] at *

Result:
X : Type u
x : X
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma supSum_union_add_supSum_infs (𝒜 ℬ : Finset (Finset α)) :
    supSum (𝒜 ∪ ℬ) + supSum (𝒜 ⊼ ℬ) = supSum 𝒜 + supSum ℬ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ,
    ↑(#((𝒜 ∪ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
        ↑(#((𝒜 ⊼ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
      ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
        ↑(#(ℬ.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s))

Tactic:
simp_rw [div_add_div_same, ← Nat.cast_add, card_truncatedSup_union_add_card_truncatedSup_infs]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ, True

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ, True

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ supSum (𝒜 ∪ ℬ) + supSum (𝒜 ⊼ ℬ) = supSum 𝒜 + supSum ℬ

Tactic:
unfold supSum

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ s : Finset α, ↑(#((𝒜 ∪ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
      ∑ s : Finset α, ↑(#((𝒜 ⊼ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
    ∑ s : Finset α, ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
      ∑ s : Finset α, ↑(#(ℬ.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s))

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ s : Finset α, ↑(#((𝒜 ∪ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
      ∑ s : Finset α, ↑(#((𝒜 ⊼ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
    ∑ s : Finset α, ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
      ∑ s : Finset α, ↑(#(ℬ.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s))

Tactic:
rw [← sum_add_distrib, ← sum_add_distrib, sum_congr rfl fun s _ ↦ _]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ,
    ↑(#((𝒜 ∪ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
        ↑(#((𝒜 ⊼ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
      ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
        ↑(#(ℬ.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s))
-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma one_fromCols_isTotallyUnimodular_iff [DecidableEq m] (A : Matrix m n R) :
    (fromCols (1 : Matrix m m R) A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m n R
⊢ (fromCols 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
rw [←transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
  one_fromRows_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Ioi_bot : Real.toEReal ⁻¹' Ioi ⊥ = univ

Proof state:
⊢ WithBot.some ∘ WithTop.some ⁻¹' Ioi ⊥ = univ

Tactic:
refine preimage_comp.trans ?_

Result:
⊢ WithTop.some ⁻¹' (WithBot.some ⁻¹' Ioi ⊥) = univ

Proof state:
⊢ Real.toEReal ⁻¹' Ioi ⊥ = univ

Tactic:
change (WithBot.some ∘ WithTop.some) ⁻¹' (Ioi ⊥) = _

Result:
⊢ WithBot.some ∘ WithTop.some ⁻¹' Ioi ⊥ = univ

Proof state:
⊢ WithTop.some ⁻¹' (WithBot.some ⁻¹' Ioi ⊥) = univ

Tactic:
simp only [WithBot.preimage_coe_Ioi_bot, preimage_univ]

Result:
no goals
-- Mathlib/Order/Hom/Lattice.lean
theorem map_symmDiff' (a b : α) : f (a ∆ b) = f a ∆ f b

Proof state:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a ∆ b) = f a ∆ f b

Tactic:
rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma id_X (p q : ℤ) (hpq : p + 1 = q) :
    (fst φ).1.v p q hpq ≫ (inl φ).v q p (by omega) +
      (snd φ).v p p (add_zero p) ≫ (inr φ).f p = 𝟙 ((mappingCone φ).X p)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ q + -1 = p

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ (↑(fst φ)).v p q hpq ≫ (inl φ).v q p ⋯ + (snd φ).v p p ⋯ ≫ (inr φ).f p = 𝟙 ((mappingCone φ).X p)

Tactic:
simpa only [Cochain.add_v, Cochain.comp_zero_cochain_v, Cochain.ofHom_v, id_f,
  Cochain.comp_v _ _ (add_neg_cancel 1) p q p hpq (by omega)]
  using Cochain.congr_v (id φ) p p (add_zero p)

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.85814, u_1} C
inst✝³ : Category.{?u.85818, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ q + -1 = p

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubVSubWeights_apply_left [DecidableEq ι] {i j : ι} (h : i ≠ j) :
    weightedVSubVSubWeights k i j i = 1

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
⊢ weightedVSubVSubWeights k i j i = 1

Tactic:
simp [weightedVSubVSubWeights, h]

Result:
no goals