harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- `t` is in the upper shadow of `𝒜` iff we can remove an element from it so that the resulting
finset is in `𝒜`. -/
lemma mem_upShadow_iff_erase_mem : t ∈ ∂⁺ 𝒜 ↔ ∃ a, a ∈ t ∧ erase t a ∈ 𝒜

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ a ∈ t, t.erase a ∈ 𝒜

Tactic:
simp_rw [mem_upShadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (∃ s ∈ 𝒜, ∃ a ∈ t, t.erase a = s) ↔ ∃ a ∈ t, t.erase a ∈ 𝒜

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (∃ s ∈ 𝒜, ∃ a ∈ t, t.erase a = s) ↔ ∃ a ∈ t, t.erase a ∈ 𝒜

Tactic:
aesop

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem jacobson_le_of_eq_bot {N : Submodule R M} (h : jacobson R (M ⧸ N) = ⊥) :
    jacobson R M ≤ N

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
h : jacobson R (M ⧸ N) = ⊥
⊢ jacobson R M ≤ N

Tactic:
simp_rw [← N.ker_mkQ, ← comap_bot, ← h, le_comap_jacobson]

Result:
no goals
-- Mathlib/Topology/Constructible.lean
@[stacks 005J "Extracted from the proof"]
lemma IsRetrocompact.preimage_of_isOpenEmbedding {s : Set Y} (hf : IsOpenEmbedding f)
    (hs : IsRetrocompact s) : IsRetrocompact (f ⁻¹' s)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hs : IsRetrocompact s
⊢ IsRetrocompact (f ⁻¹' s)

Tactic:
rintro U hUcomp hUopen

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (f ⁻¹' s ∩ U)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (f ⁻¹' s ∩ U)

Tactic:
rw [hf.isCompact_iff, image_preimage_inter]

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (s ∩ f '' U)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (s ∩ f '' U)

Tactic:
exact hs (hUcomp.image hf.continuous) <| hf.isOpenMap _ hUopen

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma comap_sectR (κ : Kernel (α × β) γ) (a : α) {f : δ → β} (hf : Measurable f) :
    comap (sectR κ a) f hf = comap κ (fun d ↦ (a, f d)) (measurable_const.prod_mk hf)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
f : δ → β
hf : Measurable f
⊢ (κ.sectR a).comap f hf = κ.comap (fun d => (a, f d)) ⋯

Tactic:
ext d s

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
f : δ → β
hf : Measurable f
d : δ
s : Set γ
a✝ : MeasurableSet s
⊢ (((κ.sectR a).comap f hf) d) s = ((κ.comap (fun d => (a, f d)) ⋯) d) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
f : δ → β
hf : Measurable f
d : δ
s : Set γ
a✝ : MeasurableSet s
⊢ (((κ.sectR a).comap f hf) d) s = ((κ.comap (fun d => (a, f d)) ⋯) d) s

Tactic:
rw [comap_apply, sectR_apply, comap_apply]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem eq_bot_iff : N = ⊥ ↔ ∀ m : M, m ∈ N → m = 0

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ N = ⊥ ↔ ∀ m ∈ N, m = 0

Tactic:
rw [eq_bot_iff]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ N ≤ ⊥ ↔ ∀ m ∈ N, m = 0

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ N ≤ ⊥ ↔ ∀ m ∈ N, m = 0

Tactic:
exact Iff.rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem isFiniteMeasure_iff_isFiniteMeasureOnCompacts_of_compactSpace [TopologicalSpace α]
    [MeasurableSpace α] {μ : Measure α} [CompactSpace α] :
    IsFiniteMeasure μ ↔ IsFiniteMeasureOnCompacts μ

Proof state:
case mp
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
a✝ : IsFiniteMeasure μ
⊢ IsFiniteMeasureOnCompacts μ

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
⊢ IsFiniteMeasure μ ↔ IsFiniteMeasureOnCompacts μ

Tactic:
constructor <;> intros

Result:
case mp
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
a✝ : IsFiniteMeasure μ
⊢ IsFiniteMeasureOnCompacts μ

case mpr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
a✝ : IsFiniteMeasureOnCompacts μ
⊢ IsFiniteMeasure μ

Proof state:
case mpr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
a✝ : IsFiniteMeasureOnCompacts μ
⊢ IsFiniteMeasure μ

Tactic:
exact CompactSpace.isFiniteMeasure

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
@[reassoc]
lemma Scheme.Opens.toSpecΓ_appTop {X : Scheme.{u}} (U : X.Opens) :
    U.toSpecΓ.appTop = (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv

Proof state:
X : Scheme
U : X.Opens
⊢ Hom.appTop U.toSpecΓ = (ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv

Tactic:
simp [Scheme.Opens.toSpecΓ]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem Function.Injective.map_swap [DecidableEq α] [DecidableEq β] {f : α → β}
    (hf : Function.Injective f) (x y z : α) :
    f (Equiv.swap x y z) = Equiv.swap (f x) (f y) (f z)

Proof state:
case neg
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : ¬f z = f x
h₂ : ¬f z = f y
⊢ f ((Equiv.swap x y) z) = f z

Tactic:
rw [Equiv.swap_apply_of_ne_of_ne (mt (congr_arg f) h₁) (mt (congr_arg f) h₂)]

Result:
no goals

Proof state:
case pos
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : f z = f x
⊢ f ((Equiv.swap x y) z) = f y

Tactic:
rw [hf h₁, Equiv.swap_apply_left]

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ f ((Equiv.swap x y) z) = if f z = f x then f y else if f z = f y then f x else f z

Tactic:
split_ifs with h₁ h₂

Result:
case pos
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : f z = f x
⊢ f ((Equiv.swap x y) z) = f y

case pos
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : ¬f z = f x
h₂ : f z = f y
⊢ f ((Equiv.swap x y) z) = f x

case neg
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : ¬f z = f x
h₂ : ¬f z = f y
⊢ f ((Equiv.swap x y) z) = f z

Proof state:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ f ((Equiv.swap x y) z) = (Equiv.swap (f x) (f y)) (f z)

Tactic:
conv_rhs => rw [Equiv.swap_apply_def]

Result:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ f ((Equiv.swap x y) z) = if f z = f x then f y else if f z = f y then f x else f z

Proof state:
case pos
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : ¬f z = f x
h₂ : f z = f y
⊢ f ((Equiv.swap x y) z) = f x

Tactic:
rw [hf h₂, Equiv.swap_apply_right]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
@[reassoc (attr := simp), elementwise (attr := simp)]
lemma isoOneCocycles_hom_comp_subtype :
    (isoOneCocycles A).hom ≫ ModuleCat.ofHom (oneCocycles A).subtype =
      iCocycles A 1 ≫ (oneCochainsLequiv A).toModuleIso.hom

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
this :
  (shortComplexH1 A).moduleCatCyclesIso.hom ≫
      ModuleCat.ofHom (LinearMap.ker (ModuleCat.Hom.hom (shortComplexH1 A).g)).subtype =
    (shortComplexH1 A).iCycles
⊢ (isoOneCocycles A).hom ≫ ModuleCat.ofHom (oneCocycles A).subtype =
    iCocycles A 1 ≫ (oneCochainsLequiv A).toModuleIso.hom

Tactic:
simp_all [shortComplexH1, isoOneCocycles, oneCocycles]

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (isoOneCocycles A).hom ≫ ModuleCat.ofHom (oneCocycles A).subtype =
    iCocycles A 1 ≫ (oneCochainsLequiv A).toModuleIso.hom

Tactic:
have := (shortComplexH1 A).moduleCatCyclesIso_hom_subtype

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
this :
  (shortComplexH1 A).moduleCatCyclesIso.hom ≫
      ModuleCat.ofHom (LinearMap.ker (ModuleCat.Hom.hom (shortComplexH1 A).g)).subtype =
    (shortComplexH1 A).iCycles
⊢ (isoOneCocycles A).hom ≫ ModuleCat.ofHom (oneCocycles A).subtype =
    iCocycles A 1 ≫ (oneCochainsLequiv A).toModuleIso.hom
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem Antivary.sum_smul_lt_sum_comp_perm_smul_iff (hfg : Antivary f g) :
    ∑ i, f i • g i < ∑ i, f (σ i) • g i ↔ ¬Antivary (f ∘ σ) g

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedSemiring α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i : ι, f i • g i < ∑ i : ι, f (σ i) • g i ↔ ¬Antivary (f ∘ ⇑σ) g

Tactic:
simp [(hfg.antivaryOn _).sum_smul_lt_sum_comp_perm_smul_iff fun _ _ ↦ mem_univ _]

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.centerMass_singleton (hw : w i ≠ 0) : ({i} : Finset ι).centerMass w z = z i

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
w : ι → R
z : ι → E
hw : w i ≠ 0
⊢ (w i)⁻¹ * (w i * 1) = 1

Tactic:
field_simp

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
w : ι → R
z : ι → E
hw : w i ≠ 0
⊢ {i}.centerMass w z = z i

Tactic:
rw [centerMass, sum_singleton, sum_singleton]

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
w : ι → R
z : ι → E
hw : w i ≠ 0
⊢ (w i)⁻¹ • w i • z i = z i

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
w : ι → R
z : ι → E
hw : w i ≠ 0
⊢ (w i)⁻¹ • w i • z i = z i

Tactic:
match_scalars

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
w : ι → R
z : ι → E
hw : w i ≠ 0
⊢ (w i)⁻¹ * (w i * 1) = 1
-- Mathlib/SetTheory/Game/Impartial.lean
theorem exists_left_move_equiv_iff_fuzzy_zero : (∃ i, G.moveLeft i ≈ 0) ↔ G ‖ 0

Proof state:
G : PGame
inst✝ : G.Impartial
hn : G ‖ 0
⊢ ∃ i, G.moveLeft i ≈ 0

Tactic:
rw [fuzzy_zero_iff_gf G, zero_lf_le] at hn

Result:
G : PGame
inst✝ : G.Impartial
hn : ∃ i, 0 ≤ G.moveLeft i
⊢ ∃ i, G.moveLeft i ≈ 0

Proof state:
G : PGame
inst✝ : G.Impartial
hn : ∃ i, 0 ≤ G.moveLeft i
⊢ ∃ i, G.moveLeft i ≈ 0

Tactic:
obtain ⟨i, hi⟩ := hn

Result:
case intro
G : PGame
inst✝ : G.Impartial
i : G.LeftMoves
hi : 0 ≤ G.moveLeft i
⊢ ∃ i, G.moveLeft i ≈ 0

Proof state:
case intro
G : PGame
inst✝ : G.Impartial
i : G.LeftMoves
hi : 0 ≤ G.moveLeft i
⊢ ∃ i, G.moveLeft i ≈ 0

Tactic:
exact ⟨i, (equiv_zero_iff_ge _).2 hi⟩

Result:
no goals

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ (∃ i, G.moveLeft i ≈ 0) ↔ G ‖ 0

Tactic:
refine ⟨fun ⟨i, hi⟩ => (fuzzy_zero_iff_gf G).2 (lf_of_le_moveLeft hi.2), fun hn => ?_⟩

Result:
G : PGame
inst✝ : G.Impartial
hn : G ‖ 0
⊢ ∃ i, G.moveLeft i ≈ 0
-- Mathlib/Algebra/GroupWithZero/Invertible.lean
theorem Invertible.ne_zero [MulZeroOneClass α] (a : α) [Nontrivial α] [Invertible a] : a ≠ 0 :=
  fun ha =>
  zero_ne_one <|
    calc
      0 = ⅟ a * a

Proof state:
α : Type u
inst✝² : MulZeroOneClass α
a : α
inst✝¹ : Nontrivial α
inst✝ : Invertible a
ha : a = 0
⊢ 0 = ⅟a * a

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem conj_I : conj I = -I :=
  Complex.ext_iff.2 <| by simp

Proof state:
⊢ ((starRingEnd ℂ) I).re = (-I).re ∧ ((starRingEnd ℂ) I).im = (-I).im

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem tendsto_iff_forall_lintegral_tendsto {γ : Type*} {F : Filter γ}
    {μs : γ → ProbabilityMeasure Ω} {μ : ProbabilityMeasure Ω} :
    Tendsto μs F (𝓝 μ) ↔
      ∀ f : Ω →ᵇ ℝ≥0,
        Tendsto (fun i ↦ ∫⁻ ω, f ω ∂(μs i : Measure Ω)) F (𝓝 (∫⁻ ω, f ω ∂(μ : Measure Ω)))

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto (toFiniteMeasure ∘ μs) F (𝓝 μ.toFiniteMeasure) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))

Tactic:
exact FiniteMeasure.tendsto_iff_forall_lintegral_tendsto

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))

Tactic:
rw [tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto (toFiniteMeasure ∘ μs) F (𝓝 μ.toFiniteMeasure) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))
-- Mathlib/CategoryTheory/Generator/Basic.lean
lemma isSeparator_of_isColimit_cofan {β : Type w} {f : β → C}
    (hf : IsSeparating (Set.range f)) {c : Cofan f} (hc : IsColimit c) : IsSeparator c.pt

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : IsSeparating (Set.range f)
c : Cofan f
hc : IsColimit c
X Y : C
u v : X ⟶ Y
huv : ∀ (h : c.pt ⟶ X), h ≫ u = h ≫ v
Z : C
hZ : Z ∈ Set.range f
g : Z ⟶ X
⊢ g ≫ u = g ≫ v

Tactic:
obtain ⟨b, rfl⟩ := Set.mem_range.1 hZ

Result:
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : IsSeparating (Set.range f)
c : Cofan f
hc : IsColimit c
X Y : C
u v : X ⟶ Y
huv : ∀ (h : c.pt ⟶ X), h ≫ u = h ≫ v
b : β
hZ : f b ∈ Set.range f
g : f b ⟶ X
⊢ g ≫ u = g ≫ v

Proof state:
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : IsSeparating (Set.range f)
c : Cofan f
hc : IsColimit c
X Y : C
u v : X ⟶ Y
huv : ∀ (h : c.pt ⟶ X), h ≫ u = h ≫ v
b : β
hZ : f b ∈ Set.range f
g : f b ⟶ X
⊢ g ≫ u = g ≫ v

Tactic:
classical simpa using c.ι.app ⟨b⟩ ≫= huv (hc.desc (Cofan.mk _ (Pi.single b g)))

Result:
no goals

Proof state:
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : IsSeparating (Set.range f)
c : Cofan f
hc : IsColimit c
X Y : C
u v : X ⟶ Y
huv : ∀ (h : c.pt ⟶ X), h ≫ u = h ≫ v
b : β
hZ : f b ∈ Set.range f
g : f b ⟶ X
⊢ g ≫ u = g ≫ v

Tactic:
simpa using c.ι.app ⟨b⟩ ≫= huv (hc.desc (Cofan.mk _ (Pi.single b g)))

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : IsSeparating (Set.range f)
c : Cofan f
hc : IsColimit c
⊢ IsSeparator c.pt

Tactic:
refine (isSeparator_def _).2 fun X Y u v huv => hf _ _ fun Z hZ g => ?_

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : IsSeparating (Set.range f)
c : Cofan f
hc : IsColimit c
X Y : C
u v : X ⟶ Y
huv : ∀ (h : c.pt ⟶ X), h ≫ u = h ≫ v
Z : C
hZ : Z ∈ Set.range f
g : Z ⟶ X
⊢ g ≫ u = g ≫ v
-- Mathlib/Algebra/Polynomial/Module/AEval.lean
lemma X_smul_of (m : M) : (X : R[X]) • (of R M a m) = of R M a (a • m)

Proof state:
R : Type u_2
A : Type u_3
M : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
m : M
⊢ X • (of R M a) m = (of R M a) (a • m)

Tactic:
rw [← of_aeval_smul, aeval_X]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma fundCocircuit_isCocircuit (he : e ∈ B) (hB : M.IsBase B) :
    M.IsCocircuit <| M.fundCocircuit e B

Proof state:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∈ M✶.closure (M.E \ B)

Tactic:
rw [hB.compl_isBase_dual.closure_eq, dual_ground]

Result:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∈ M.E

Proof state:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∉ M.E \ B

Tactic:
simp [he]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∈ M.E

Tactic:
exact hB.subset_ground he

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ M.IsCocircuit (M.fundCocircuit e B)

Tactic:
apply hB.compl_isBase_dual.indep.fundCircuit_isCircuit _ (by simp [he])

Result:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∈ M✶.closure (M.E \ B)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem xor_right_comm : ∀ (x y z : Bool), ((x ^^ y) ^^ z) = ((x ^^ z) ^^ y)

Proof state:
⊢ ∀ (x y z : Bool), (x ^^ y ^^ z) = (x ^^ z ^^ y)

Tactic:
decide

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem codisjoint_inf_right : Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
⊢ Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c

Tactic:
simp only [codisjoint_iff, sup_inf_left, inf_eq_top_iff]

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem conjugate' {x : R} (hx : x ∈ skewAdjoint R) (z : R) : star z * x * z ∈ skewAdjoint R

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : x ∈ skewAdjoint R
z : R
⊢ star z * x * z ∈ skewAdjoint R

Tactic:
simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, neg_mul, mul_neg, mul_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Action/Limits.lean
/-- `F : C ⥤ Action V G` preserves colimits of some size
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
lemma preservesColimitsOfSize_of_preserves (F : C ⥤ Action V G)
    (h : PreservesColimitsOfSize.{w₂, w₁} (F ⋙ Action.forget V G)) :
    PreservesColimitsOfSize.{w₂, w₁} F

Proof state:
case preservesColimitsOfShape.h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesColimitsOfShape J (F ⋙ forget V G)

Tactic:
exact PreservesColimitsOfSize.preservesColimitsOfShape

Result:
no goals

Proof state:
case preservesColimitsOfShape
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesColimitsOfShape J F

Tactic:
apply Action.preservesColimitsOfShape_of_preserves

Result:
case preservesColimitsOfShape.h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesColimitsOfShape J (F ⋙ forget V G)

Proof state:
V : Type (u + 1)
inst✝² : LargeCategory V
G : Type u
inst✝¹ : Monoid G
C : Type t₁
inst✝ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
⊢ PreservesColimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} F

Tactic:
constructor

Result:
case preservesColimitsOfShape
V : Type (u + 1)
inst✝² : LargeCategory V
G : Type u
inst✝¹ : Monoid G
C : Type t₁
inst✝ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
⊢ autoParam (∀ {J : Type w₁} [inst : Category.{w₂, w₁} J], PreservesColimitsOfShape J F) _auto✝

Proof state:
case preservesColimitsOfShape
V : Type (u + 1)
inst✝² : LargeCategory V
G : Type u
inst✝¹ : Monoid G
C : Type t₁
inst✝ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
⊢ autoParam (∀ {J : Type w₁} [inst : Category.{w₂, w₁} J], PreservesColimitsOfShape J F) _auto✝

Tactic:
intro J _

Result:
case preservesColimitsOfShape
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesColimitsOfShape J F
-- Mathlib/Probability/Kernel/Basic.lean
theorem lintegral_const {f : β → ℝ≥0∞} {μ : Measure β} {a : α} :
    ∫⁻ x, f x ∂const α μ a = ∫⁻ x, f x ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
μ : Measure β
a : α
⊢ ∫⁻ (x : β), f x ∂(const α μ) a = ∫⁻ (x : β), f x ∂μ

Tactic:
rw [const_apply]

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
lemma addNSMul_eq_right [Archimedean α] (hδ : 0 < δ) :
    ∃ m, ∀ n ≥ m, addNSMul h δ n = b

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
⊢ ∃ m, ∀ n ≥ m, ↑(addNSMul h δ n) = b

Tactic:
obtain ⟨m, hm⟩ := Archimedean.arch (b - a) hδ

Result:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
⊢ ∃ m, ∀ n ≥ m, ↑(addNSMul h δ n) = b

Proof state:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
n : ℕ
hn : n ≥ m
⊢ b ≤ n • δ + a

Tactic:
exact sub_le_iff_le_add.mp (hm.trans <| nsmul_le_nsmul_left hδ.le hn)

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
⊢ ∃ m, ∀ n ≥ m, ↑(addNSMul h δ n) = b

Tactic:
refine ⟨m, fun n hn ↦ ?_⟩

Result:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
n : ℕ
hn : n ≥ m
⊢ ↑(addNSMul h δ n) = b

Proof state:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
n : ℕ
hn : n ≥ m
⊢ ↑(addNSMul h δ n) = b

Tactic:
rw [addNSMul, coe_projIcc, add_comm, min_eq_left_iff.mpr, max_eq_right h]

Result:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
n : ℕ
hn : n ≥ m
⊢ b ≤ n • δ + a