harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem nth_of_bisim [Inhabited (M F)] (bisim : IsBisimulation R) (s₁ s₂) (ps : Path F) :
    (R s₁ s₂) →
      IsPath ps s₁ ∨ IsPath ps s₂ →
        iselect ps s₁ = iselect ps s₂ ∧
          ∃ (a : _) (f f' : F.B a → M F),
            isubtree ps s₁ = M.mk ⟨a, f⟩ ∧
              isubtree ps s₂ = M.mk ⟨a, f'⟩ ∧ ∀ i : F.B a, f i ~ f' i

Proof state:
case f.f.cons.mk.f
F : PFunctor.{u}
R : F.M → F.M → Prop
inst✝ : Inhabited F.M
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
h₁ : R (f i) (f' i)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
⊢ (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)).head = (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)).head ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)

Tactic:
induction' h' : f' i using PFunctor.M.casesOn' with a₁ f₁

Result:
case f.f.cons.mk.f.f
F : PFunctor.{u}
R : F.M → F.M → Prop
inst✝ : Inhabited F.M
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
h₁ : R (f i) (f' i)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
a₁ : F.A
f₁ : F.B a₁ → F.M
h' : f' i = M.mk ⟨a₁, f₁⟩
⊢ (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)).head = (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)).head ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
-- Mathlib/GroupTheory/GroupAction/Pointwise.lean
theorem preimage_smul_setₛₗ_of_units (hc : IsUnit c) (hc' : IsUnit (σ c)) :
    h ⁻¹' (σ c • t) = c • h ⁻¹' t

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : IsUnit c
hc' : IsUnit (σ c)
⊢ ⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t

Tactic:
apply preimage_smul_setₛₗ'

Result:
case hc
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : IsUnit c
hc' : IsUnit (σ c)
⊢ Function.Surjective fun m => c • m

case hc'
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : IsUnit c
hc' : IsUnit (σ c)
⊢ Function.Injective fun n => σ c • n

Proof state:
case hc'
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : IsUnit c
hc' : IsUnit (σ c)
⊢ Function.Injective fun n => σ c • n

Tactic:
exact (MulAction.smul_bijective_of_is_unit hc').injective

Result:
no goals

Proof state:
case hc
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
t : Set N
hc : IsUnit c
hc' : IsUnit (σ c)
⊢ Function.Surjective fun m => c • m

Tactic:
exact (MulAction.smul_bijective_of_is_unit hc).surjective

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_closure₁ : hausdorffEdist (closure s) t = hausdorffEdist s t

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEdist (closure s) t = hausdorffEdist s t

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEdist (closure s) t ≤ hausdorffEdist s t

case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEdist s t ≤ hausdorffEdist (closure s) t

Proof state:
case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEdist (closure s) t ≤ hausdorffEdist s t

Tactic:
calc
  _ ≤ hausdorffEdist (closure s) s + hausdorffEdist s t := hausdorffEdist_triangle
  _ = hausdorffEdist s t := by simp [hausdorffEdist_comm]

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEdist (closure s) s + hausdorffEdist s t = hausdorffEdist s t

Tactic:
simp [hausdorffEdist_comm]

Result:
no goals

Proof state:
case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEdist s t ≤ hausdorffEdist (closure s) t

Tactic:
calc
  _ ≤ hausdorffEdist s (closure s) + hausdorffEdist (closure s) t := hausdorffEdist_triangle
  _ = hausdorffEdist (closure s) t := by simp

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEdist s (closure s) + hausdorffEdist (closure s) t = hausdorffEdist (closure s) t

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
lemma starComp_apply (hR : 0 < ringChar R) {φ : AddChar R ℂ} (a : R) :
    (starRingEnd ℂ) (φ a) = φ⁻¹ a

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ (starRingEnd ℂ) (φ a) = φ⁻¹ a

Tactic:
rw [← starComp_eq_inv hR]

Result:
R : Type u_1
inst✝ : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ (starRingEnd ℂ) (φ a) = ((↑(starRingEnd ℂ)).compAddChar φ) a

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ (starRingEnd ℂ) (φ a) = ((↑(starRingEnd ℂ)).compAddChar φ) a

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem IsMittagLeffler.toPreimages (h : F.IsMittagLeffler) : (F.toPreimages s).IsMittagLeffler :=
  (isMittagLeffler_iff_subset_range_comp _).2 fun j => by
    obtain ⟨j₁, g₁, f₁, -⟩ := IsCofilteredOrEmpty.cone_objs i j
    obtain ⟨j₂, f₂, h₂⟩ := F.isMittagLeffler_iff_eventualRange.1 h j₁
    refine ⟨j₂, f₂ ≫ f₁, fun j₃ f₃ => ?_⟩
    rintro _ ⟨⟨x, hx⟩, rfl⟩
    have : F.map f₂ x ∈ F.eventualRange j₁

Proof state:
case intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
⊢ ∃ i_1 f, ∀ ⦃k : J⦄ (g : k ⟶ i_1), range ((F.toPreimages s).map f) ⊆ range ((F.toPreimages s).map (g ≫ f))

Tactic:
obtain ⟨j₂, f₂, h₂⟩ := F.isMittagLeffler_iff_eventualRange.1 h j₁

Result:
case intro.intro.intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range (F.map f₂)
⊢ ∃ i_1 f, ∀ ⦃k : J⦄ (g : k ⟶ i_1), range ((F.toPreimages s).map f) ⊆ range ((F.toPreimages s).map (g ≫ f))
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.symmetry' (P Q : C) :
    biprod.lift biprod.snd biprod.fst ≫ biprod.lift biprod.snd biprod.fst = 𝟙 (P ⊞ Q)

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
P Q : C
⊢ lift snd fst ≫ lift snd fst = 𝟙 (P ⊞ Q)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma vanishingIdeal_isClosed_isIrreducible :
    vanishingIdeal (R := R) '' {s | IsClosed s ∧ IsIrreducible s} = {P | P.IsPrime}

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s} = {P | P.IsPrime}

Tactic:
refine (subset_antisymm ?_ ?_).trans vanishingIdeal_isIrreducible

Result:
case refine_1
R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s} ⊆ vanishingIdeal '' {s | IsIrreducible s}

case refine_2
R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' {s | IsIrreducible s} ⊆ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s}

Proof state:
case refine_2
R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' {s | IsIrreducible s} ⊆ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s}

Tactic:
rintro _ ⟨s, hs, rfl⟩

Result:
case refine_2.intro.intro
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : s ∈ {s | IsIrreducible s}
⊢ vanishingIdeal s ∈ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s}

Proof state:
case refine_2.intro.intro
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : s ∈ {s | IsIrreducible s}
⊢ vanishingIdeal s ∈ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s}

Tactic:
exact ⟨closure s, ⟨isClosed_closure, hs.closure⟩, vanishingIdeal_closure s⟩

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s} ⊆ vanishingIdeal '' {s | IsIrreducible s}

Tactic:
exact Set.image_subset _ fun _ ↦ And.right

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
lemma range_eq_top_of_ne_zero :
    LinearMap.range f = ⊤

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
v : V₁
hv : f v ≠ 0
x : K
x✝ : x ∈ ⊤
⊢ f (x • (f v)⁻¹ • v) = x

Tactic:
simp [inv_mul_cancel₀ hv]

Result:
no goals

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
⊢ ∃ v, f v ≠ 0

Tactic:
contrapose! hf

Result:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
f : Dual K V₁
hf : ∀ (v : V₁), f v = 0
⊢ f = 0

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
f : Dual K V₁
hf : ∀ (v : V₁), f v = 0
⊢ f = 0

Tactic:
ext v

Result:
case h
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
f : Dual K V₁
hf : ∀ (v : V₁), f v = 0
v : V₁
⊢ f v = 0 v

Proof state:
case intro
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
v : V₁
hv : f v ≠ 0
⊢ ⊤ ≤ LinearMap.range f

Tactic:
exact fun x _ ↦ ⟨x • (f v)⁻¹ • v, by simp [inv_mul_cancel₀ hv]⟩

Result:
no goals

Proof state:
case intro
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
v : V₁
hv : f v ≠ 0
⊢ LinearMap.range f = ⊤

Tactic:
rw [eq_top_iff]

Result:
case intro
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
v : V₁
hv : f v ≠ 0
⊢ ⊤ ≤ LinearMap.range f

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
⊢ LinearMap.range f = ⊤

Tactic:
obtain ⟨v, hv⟩ : ∃ v, f v ≠ 0 := by contrapose! hf; ext v; simpa using hf v

Result:
case intro
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
v : V₁
hv : f v ≠ 0
⊢ LinearMap.range f = ⊤

Proof state:
case h
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
f : Dual K V₁
hf : ∀ (v : V₁), f v = 0
v : V₁
⊢ f v = 0 v

Tactic:
simpa using hf v

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem exists_mem_ne_zero_of_rank_pos {s : Submodule R M} (h : 0 < Module.rank R s) :
    ∃ b : M, b ∈ s ∧ b ≠ 0 :=
  exists_mem_ne_zero_of_ne_bot fun eq => by rw [eq, rank_bot] at h; exact lt_irrefl _ h

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Submodule R M
h : 0 < Module.rank R ↥s
eq : s = ⊥
⊢ False

Tactic:
rw [eq, rank_bot] at h

Result:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Submodule R M
h : 0 < 0
eq : s = ⊥
⊢ False

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Submodule R M
h : 0 < 0
eq : s = ⊥
⊢ False

Tactic:
exact lt_irrefl _ h

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem smul (c : ℝ) (hf : Martingale f ℱ μ) : Martingale (c • f) ℱ μ

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
c : ℝ
hf : Martingale f ℱ μ
⊢ Martingale (c • f) ℱ μ

Tactic:
refine ⟨hf.adapted.smul c, fun i j hij => ?_⟩

Result:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
c : ℝ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[(c • f) j|↑ℱ i] =ᶠ[ae μ] (c • f) i

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
c : ℝ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[(c • f) j|↑ℱ i] =ᶠ[ae μ] (c • f) i

Tactic:
refine (condExp_smul ..).trans ((hf.2 i j hij).mono fun x hx => ?_)

Result:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
c : ℝ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
x : Ω
hx : (μ[f j|↑ℱ i]) x = f i x
⊢ (c • μ[f j|↑ℱ i]) x = (c • f) i x

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ι → Ω → E
ℱ : Filtration ι m0
c : ℝ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
x : Ω
hx : (μ[f j|↑ℱ i]) x = f i x
⊢ (c • μ[f j|↑ℱ i]) x = (c • f) i x

Tactic:
simp only [Pi.smul_apply, hx]

Result:
no goals
-- Mathlib/Topology/Connected/TotallyDisconnected.lean
theorem totallyDisconnectedSpace_iff_connectedComponent_singleton :
    TotallyDisconnectedSpace α ↔ ∀ x : α, connectedComponent x = {x}

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
⊢ (connectedComponent x).Subsingleton ↔ connectedComponent x = {x}

Tactic:
rw [subsingleton_iff_singleton]

Result:
α : Type u
inst✝ : TopologicalSpace α
x : α
⊢ x ∈ connectedComponent x

Proof state:
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), (connectedComponent x).Subsingleton) ↔ ∀ (x : α), connectedComponent x = {x}

Tactic:
refine forall_congr' fun x => ?_

Result:
α : Type u
inst✝ : TopologicalSpace α
x : α
⊢ (connectedComponent x).Subsingleton ↔ connectedComponent x = {x}

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
⊢ x ∈ connectedComponent x

Tactic:
exact mem_connectedComponent

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
⊢ TotallyDisconnectedSpace α ↔ ∀ (x : α), connectedComponent x = {x}

Tactic:
rw [totallyDisconnectedSpace_iff_connectedComponent_subsingleton]

Result:
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), (connectedComponent x).Subsingleton) ↔ ∀ (x : α), connectedComponent x = {x}
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_eq_X_mul_T_sub_pol_U (n : ℤ) : T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ : U R (n + 1) = X * U R n + T R (n + 1)
h₂ : U R (n + 1 + 1) = X * U R (n + 1) + T R (n + 1 + 1)
h₃ : U R (n + 2) = 2 * X * U R (n + 1) - U R n
⊢ T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n

Tactic:
linear_combination (norm := ring_nf) h₃ - h₂ + (X : R[X]) * h₁

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ : U R (n + 1) = X * U R n + T R (n + 1)
h₂ : U R (n + 1 + 1) = X * U R (n + 1) + T R (n + 1 + 1)
⊢ T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n

Tactic:
have h₃ := U_add_two R n

Result:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ : U R (n + 1) = X * U R n + T R (n + 1)
h₂ : U R (n + 1 + 1) = X * U R (n + 1) + T R (n + 1 + 1)
h₃ : U R (n + 2) = 2 * X * U R (n + 1) - U R n
⊢ T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ : U R (n + 1) = X * U R n + T R (n + 1)
⊢ T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n

Tactic:
have h₂ := U_eq_X_mul_U_add_T R (n + 1)

Result:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ : U R (n + 1) = X * U R n + T R (n + 1)
h₂ : U R (n + 1 + 1) = X * U R (n + 1) + T R (n + 1 + 1)
⊢ T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n

Tactic:
have h₁ := U_eq_X_mul_U_add_T R n

Result:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ : U R (n + 1) = X * U R n + T R (n + 1)
⊢ T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_pos' (hμ : μ ≠ 0) (h_int_X : Integrable (fun ω => exp (t * X ω)) μ) :
    0 < mgf X μ t

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω => rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
x : Ω
⊢ (x ∈ Function.support fun x => rexp (t * X x)) ↔ x ∈ Set.univ

Tactic:
simp only [Function.mem_support, Set.mem_univ, iff_true]

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω => rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
x : Ω
⊢ rexp (t * X x) ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_filterMap (xs : List α) (f : α → Option β) (p : β → Bool) :
    (xs.filterMap f).find? p = (xs.find? (fun a => (f a).any p)).bind f

Proof state:
case cons.h_2
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : find? p (filterMap f xs) = (find? (fun a => Option.any p (f a)) xs).bind f
x✝ : Option β
b✝ : β
heq✝ : f x = some b✝
⊢ find? p (b✝ :: filterMap f xs) = (find? (fun a => Option.any p (f a)) (x :: xs)).bind f

Tactic:
simp only [find?_cons]

Result:
case cons.h_2
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : find? p (filterMap f xs) = (find? (fun a => Option.any p (f a)) xs).bind f
x✝ : Option β
b✝ : β
heq✝ : f x = some b✝
⊢ (match p b✝ with
    | true => some b✝
    | false => find? p (filterMap f xs)) =
    (match Option.any p (f x) with
        | true => some x
        | false => find? (fun a => Option.any p (f a)) xs).bind
      f

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : find? p (filterMap f xs) = (find? (fun a => Option.any p (f a)) xs).bind f
⊢ find? p (filterMap f (x :: xs)) = (find? (fun a => Option.any p (f a)) (x :: xs)).bind f

Tactic:
simp only [filterMap_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : find? p (filterMap f xs) = (find? (fun a => Option.any p (f a)) xs).bind f
⊢ find? p
      (match f x with
      | none => filterMap f xs
      | some b => b :: filterMap f xs) =
    (find? (fun a => Option.any p (f a)) (x :: xs)).bind f

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
⊢ find? p (filterMap f []) = (find? (fun a => Option.any p (f a)) []).bind f

Tactic:
simp

Result:
no goals

Proof state:
case cons.h_2
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : find? p (filterMap f xs) = (find? (fun a => Option.any p (f a)) xs).bind f
x✝ : Option β
b✝ : β
heq✝ : f x = some b✝
⊢ (match p b✝ with
    | true => some b✝
    | false => find? p (filterMap f xs)) =
    (match Option.any p (f x) with
        | true => some x
        | false => find? (fun a => Option.any p (f a)) xs).bind
      f

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma dvd_mul_of_div_dvd (h : b ∣ a) (hdiv : a / b ∣ c) : a ∣ b * c

Proof state:
case intro
a b : ℤ
h : b ∣ a
e : ℤ
⊢ a ∣ b * (a / b * e)

Tactic:
rw [← Int.mul_assoc, Int.mul_comm _ (a / b), Int.ediv_mul_cancel h]

Result:
case intro
a b : ℤ
h : b ∣ a
e : ℤ
⊢ a ∣ a * e

Proof state:
a b c : ℤ
h : b ∣ a
hdiv : a / b ∣ c
⊢ a ∣ b * c

Tactic:
obtain ⟨e, rfl⟩ := hdiv

Result:
case intro
a b : ℤ
h : b ∣ a
e : ℤ
⊢ a ∣ b * (a / b * e)

Proof state:
case intro
a b : ℤ
h : b ∣ a
e : ℤ
⊢ a ∣ a * e

Tactic:
exact Int.dvd_mul_right a e

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- `m` is `s`-factored if and only if all prime divisors of `m` are in `s`. -/
lemma mem_factoredNumbers' {s : Finset ℕ} {m : ℕ} :
    m ∈ factoredNumbers s ↔ ∀ p, p.Prime → p ∣ m → p ∈ s

Proof state:
case intro.intro
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
⊢ (m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s) ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s

Tactic:
refine ⟨fun ⟨H₀, H₁⟩ ↦ fun p hp₁ hp₂ ↦ H₁ p (le_of_dvd (Nat.pos_of_ne_zero H₀) hp₂) hp₁ hp₂,
       fun H ↦ ⟨fun h ↦ lt_irrefl p ?_, fun p _ ↦ H p⟩⟩

Result:
case intro.intro
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
H : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
h : m = 0
⊢ p < p

Proof state:
case intro.intro
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
H : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
h : m = 0
⊢ p < p

Tactic:
calc
  p ≤ s.sup id := Finset.le_sup (f := @id ℕ) <| H p hp₂ <| h.symm ▸ dvd_zero p
  _ < 1 + s.sup id := lt_one_add _
  _ ≤ p := hp₁

Result:
no goals

Proof state:
s : Finset ℕ
m : ℕ
⊢ m ∈ factoredNumbers s ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s

Tactic:
obtain ⟨p, hp₁, hp₂⟩ := exists_infinite_primes (1 + Finset.sup s id)

Result:
case intro.intro
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
⊢ m ∈ factoredNumbers s ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s

Proof state:
case intro.intro
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
⊢ m ∈ factoredNumbers s ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s

Tactic:
rw [mem_factoredNumbers_iff_forall_le]

Result:
case intro.intro
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
⊢ (m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s) ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s