harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem univ_pi_Ioi_ae_eq_Ici {f : ∀ i, α i} :
    (pi univ fun i => Ioi (f i)) =ᵐ[Measure.pi μ] Ici f

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f : (i : ι) → α i
⊢ (univ.pi fun i => Ioi (f i)) =ᶠ[ae (Measure.pi μ)] Ici f

Tactic:
rw [← pi_univ_Ici]

Result:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f : (i : ι) → α i
⊢ (univ.pi fun i => Ioi (f i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Ici (f i)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f : (i : ι) → α i
⊢ (univ.pi fun i => Ioi (f i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Ici (f i)

Tactic:
exact pi_Ioi_ae_eq_pi_Ici

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean
@[to_additive]
lemma prod_Ico_mul_right (h : a ≤ b) : (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a b : α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x

Tactic:
rw [mul_comm, right_mul_prod_Ico h]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_left_eq_arccos_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    ∡ p₃ p₁ p₂ = Real.arccos (dist p₁ p₂ / dist p₁ p₃)

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
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃))

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
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
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃))

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
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sign = 1

Tactic:
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

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
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃))

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm,
  angle_eq_arccos_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h),
  dist_comm p₁ p₃]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma sum_prodMkRight {ι : Type*} [Countable ι] {κ : ι → Kernel α β} :
    Kernel.sum (fun i ↦ Kernel.prodMkRight γ (κ i)) = Kernel.prodMkRight γ (Kernel.sum κ)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
⊢ (Kernel.sum fun i => prodMkRight γ (κ i)) = prodMkRight γ (Kernel.sum κ)

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
a✝¹ : α × γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.sum fun i => prodMkRight γ (κ i)) a✝¹) s✝ = ((prodMkRight γ (Kernel.sum κ)) a✝¹) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
a✝¹ : α × γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.sum fun i => prodMkRight γ (κ i)) a✝¹) s✝ = ((prodMkRight γ (Kernel.sum κ)) a✝¹) s✝

Tactic:
simp_rw [sum_apply, prodMkRight_apply, sum_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
@[reassoc (attr := simp)]
lemma μ_inv_natural_right (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :
    (μ L W ε X Y₁).inv ≫ (L').obj X ◁ (L').map g =
      (L').map (X ◁ g) ≫ (μ L W ε X Y₂).inv

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ (μ L W ε X Y₁).inv ≫ L'.obj X ◁ L'.map g = L'.map (X ◁ g) ≫ (μ L W ε X Y₂).inv

Tactic:
simp [Iso.eq_comp_inv]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem Biprod.ofComponents_eq (f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂) :
    Biprod.ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd)
        (biprod.inr ≫ f ≫ biprod.fst) (biprod.inr ≫ f ≫ biprod.snd) =
      f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
      (biprod.inr ≫ f ≫ biprod.snd) =
    f

Tactic:
ext <;>
  simp only [Category.comp_id, biprod.inr_fst, biprod.inr_snd, biprod.inl_snd, add_zero, zero_add,
    Biprod.inl_ofComponents, Biprod.inr_ofComponents, eq_self_iff_true, Category.assoc,
    comp_zero, biprod.inl_fst, Preadditive.add_comp]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arctan_zero : arctan 0 = 0

Proof state:
⊢ arctan 0 = 0

Tactic:
simp [arctan_eq_arcsin]

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
lemma biUnion_congr (hs : s₁ = s₂) (ht : ∀ a ∈ s₁, t₁ a = t₂ a) : s₁.biUnion t₁ = s₂.biUnion t₂ :=
  ext fun x ↦ by
    -- Porting note: this entire proof was `simp [or_and_right, exists_or]`
    simp_rw [mem_biUnion]
    apply exists_congr
    simp +contextual only [hs, and_congr_right_iff, ht, implies_true]

Proof state:
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
hs : s₁ = s₂
ht : ∀ a ∈ s₁, t₁ a = t₂ a
x : β
⊢ (∃ a ∈ s₁, x ∈ t₁ a) ↔ ∃ a ∈ s₂, x ∈ t₂ a

Tactic:
apply exists_congr

Result:
case h
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
hs : s₁ = s₂
ht : ∀ a ∈ s₁, t₁ a = t₂ a
x : β
⊢ ∀ (a : α), a ∈ s₁ ∧ x ∈ t₁ a ↔ a ∈ s₂ ∧ x ∈ t₂ a

Proof state:
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
hs : s₁ = s₂
ht : ∀ a ∈ s₁, t₁ a = t₂ a
x : β
⊢ x ∈ s₁.biUnion t₁ ↔ x ∈ s₂.biUnion t₂

Tactic:
simp_rw [mem_biUnion]

Result:
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
hs : s₁ = s₂
ht : ∀ a ∈ s₁, t₁ a = t₂ a
x : β
⊢ (∃ a ∈ s₁, x ∈ t₁ a) ↔ ∃ a ∈ s₂, x ∈ t₂ a

Proof state:
case h
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
hs : s₁ = s₂
ht : ∀ a ∈ s₁, t₁ a = t₂ a
x : β
⊢ ∀ (a : α), a ∈ s₁ ∧ x ∈ t₁ a ↔ a ∈ s₂ ∧ x ∈ t₂ a

Tactic:
simp +contextual only [hs, and_congr_right_iff, ht, implies_true]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Simplex.lean
@[simp] lemma equilateral_reindex_iff {s : Simplex R P m} (e : Fin (m + 1) ≃ Fin (n + 1)) :
    (s.reindex e).Equilateral ↔ s.Equilateral

Proof state:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).Equilateral ↔ s.Equilateral

Tactic:
refine ⟨fun ⟨r, hr⟩ ↦ ⟨r, fun i j hij ↦ ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r, fun i j hij ↦ ?_⟩⟩

Result:
case refine_1
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
x✝ : (s.reindex e).Equilateral
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist ((s.reindex e).points i) ((s.reindex e).points j) = r
i j : Fin (m + 1)
hij : i ≠ j
⊢ dist (s.points i) (s.points j) = r

case refine_2
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
x✝ : s.Equilateral
r : ℝ
hr : ∀ (i j : Fin (m + 1)), i ≠ j → dist (s.points i) (s.points j) = r
i j : Fin (n + 1)
hij : i ≠ j
⊢ dist ((s.reindex e).points i) ((s.reindex e).points j) = r

Proof state:
case refine_2
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
x✝ : s.Equilateral
r : ℝ
hr : ∀ (i j : Fin (m + 1)), i ≠ j → dist (s.points i) (s.points j) = r
i j : Fin (n + 1)
hij : i ≠ j
⊢ dist ((s.reindex e).points i) ((s.reindex e).points j) = r

Tactic:
convert hr (e.symm i) (e.symm j) (e.symm.injective.ne hij) using 2

Result:
no goals

Proof state:
case refine_1
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
x✝ : (s.reindex e).Equilateral
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist ((s.reindex e).points i) ((s.reindex e).points j) = r
i j : Fin (m + 1)
hij : i ≠ j
⊢ dist (s.points i) (s.points j) = r

Tactic:
convert hr (e i) (e j) (e.injective.ne hij) using 2 <;> simp

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem iSup_induction {ι : Sort*} (S : ι → Submonoid M) {C : M → Prop} {x : M} (hx : x ∈ ⨆ i, S i)
    (mem : ∀ (i), ∀ x ∈ S i, C x) (one : C 1) (mul : ∀ x y, C x → C y → C (x * y)) : C x

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : M → Prop
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x

Tactic:
refine closure_induction (fun x hx => ?_) one (fun _ _ _ _ ↦ mul _ _) hx

Result:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : M), C x → C y → C (x * y)
x : M
hx : x ∈ ⋃ i, ↑(S i)
⊢ C x

Proof state:
case intro
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : M), C x → C y → C (x * y)
x : M
hx : x ∈ ⋃ i, ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x

Tactic:
exact mem _ _ hi

Result:
no goals

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : M), C x → C y → C (x * y)
x : M
hx : x ∈ ⋃ i, ↑(S i)
⊢ C x

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx

Result:
case intro
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : M), C x → C y → C (x * y)
x : M
hx : x ∈ ⋃ i, ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : M → Prop
x : M
hx : x ∈ ⨆ i, S i
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x

Tactic:
rw [iSup_eq_closure] at hx

Result:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : M → Prop
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/List.lean
theorem foldlM_toList [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : α → β → m α) :
    o.toList.foldlM f a = o.elim (pure a) (fun b => f a b)

Proof state:
m : Type u_1 → Type u_2
β : Type u_3
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
o : Option β
a : α
f : α → β → m α
⊢ List.foldlM f a o.toList = o.elim (pure a) fun b => f a b

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Basic.lean
/-- The cardinality of morphisms `A ⟶ X` is smaller than the cardinality of
the fiber of the target if the source is connected. -/
lemma card_hom_le_card_fiber_of_connected (A X : C) [IsConnected A] :
    Nat.card (A ⟶ X) ≤ Nat.card (F.obj X)

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
⊢ Nat.card (A ⟶ X) ≤ Nat.card (F.obj X).carrier

Tactic:
apply Nat.card_le_card_of_injective

Result:
case hf
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
⊢ Function.Injective ?f

case f
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
⊢ (A ⟶ X) → (F.obj X).carrier

Proof state:
case hf
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
⊢ Function.Injective ?f

case f
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
⊢ (A ⟶ X) → (F.obj X).carrier

Tactic:
exact evaluation_injective_of_isConnected F A X (Classical.arbitrary _)

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem pi_def (i : Set α) (s : ∀ a, Set (π a)) : pi i s = ⋂ a ∈ i, eval a ⁻¹' s a

Proof state:
case h
α : Type u_1
π : α → Type u_12
i : Set α
s : (a : α) → Set (π a)
x✝ : (i : α) → π i
⊢ x✝ ∈ i.pi s ↔ x✝ ∈ ⋂ a ∈ i, eval a ⁻¹' s a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
π : α → Type u_12
i : Set α
s : (a : α) → Set (π a)
⊢ i.pi s = ⋂ a ∈ i, eval a ⁻¹' s a

Tactic:
ext

Result:
case h
α : Type u_1
π : α → Type u_12
i : Set α
s : (a : α) → Set (π a)
x✝ : (i : α) → π i
⊢ x✝ ∈ i.pi s ↔ x✝ ∈ ⋂ a ∈ i, eval a ⁻¹' s a
-- Mathlib/Order/Interval/Set/SuccOrder.lean
lemma Ici.coe_pred_of_not_isMin
    [PredOrder J] {j : J} {i : Set.Ici j} (hi : ¬ IsMin i) :
    (Order.pred i).1 = Order.pred i.1

Proof state:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ Order.pred ↑i ∈ Ici j

Tactic:
apply Order.le_pred_of_lt

Result:
case a
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ j < ↑i

Proof state:
case a
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ j < ↑i

Tactic:
exact lt_of_le_of_ne (α := Set.Ici j) bot_le (Ne.symm (by simpa using hi))

Result:
no goals

Proof state:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ ↑(Order.pred i) = Order.pred ↑i

Tactic:
rw [coe_pred_of_mem]

Result:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ Order.pred ↑i ∈ Ici j

Proof state:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ i ≠ ⊥

Tactic:
simpa using hi

Result:
no goals
-- Mathlib/FieldTheory/Extension.lean
theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits {F K : Type*} (L : Type*)
    [Field F] [Field K] [Field L] [Algebra F L] [Algebra F K]
    (hA : ∀ x : K, (minpoly F x).Splits (algebraMap F L))
    [Algebra.IsAlgebraic F K] (x : K) :
    (Set.range fun (ψ : K →ₐ[F] L) => ψ x) = (minpoly F x).rootSet L

Proof state:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)
inst✝ : Algebra.IsAlgebraic F K
x : K
⊢ (Set.range fun ψ => ψ x) = (minpoly F x).rootSet L

Tactic:
ext a

Result:
case h
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)
inst✝ : Algebra.IsAlgebraic F K
x : K
a : L
⊢ (a ∈ Set.range fun ψ => ψ x) ↔ a ∈ (minpoly F x).rootSet L

Proof state:
case h
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)
inst✝ : Algebra.IsAlgebraic F K
x : K
a : L
⊢ (a ∈ Set.range fun ψ => ψ x) ↔ (aeval a) (minpoly F x) = 0

Tactic:
refine ⟨fun ⟨ψ, hψ⟩ ↦ ?_, fun ha ↦ IntermediateField.exists_algHom_of_splits_of_aeval
  (fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, hA x⟩) ha⟩

Result:
case h
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)
inst✝ : Algebra.IsAlgebraic F K
x : K
a : L
x✝ : a ∈ Set.range fun ψ => ψ x
ψ : K →ₐ[F] L
hψ : (fun ψ => ψ x) ψ = a
⊢ (aeval a) (minpoly F x) = 0

Proof state:
case h
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)
inst✝ : Algebra.IsAlgebraic F K
x : K
a : L
x✝ : a ∈ Set.range fun ψ => ψ x
ψ : K →ₐ[F] L
hψ : (fun ψ => ψ x) ψ = a
⊢ (aeval a) (minpoly F x) = 0

Tactic:
rw [← hψ, Polynomial.aeval_algHom_apply ψ x, minpoly.aeval, map_zero]

Result:
no goals

Proof state:
case h
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)
inst✝ : Algebra.IsAlgebraic F K
x : K
a : L
⊢ (a ∈ Set.range fun ψ => ψ x) ↔ a ∈ (minpoly F x).rootSet L

Tactic:
rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x))]

Result:
case h
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)
inst✝ : Algebra.IsAlgebraic F K
x : K
a : L
⊢ (a ∈ Set.range fun ψ => ψ x) ↔ (aeval a) (minpoly F x) = 0
-- Mathlib/Data/Set/NAry.lean
theorem image2_inter_union_subset {f : α → α → β} {s t : Set α} (hf : ∀ a b, f a b = f b a) :
    image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t

Proof state:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t

Tactic:
rw [inter_comm]

Result:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (t ∩ s) (s ∪ t) ⊆ image2 f s t

Proof state:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (t ∩ s) (s ∪ t) ⊆ image2 f s t

Tactic:
exact image2_inter_union_subset_union.trans (union_subset (image2_comm hf).subset Subset.rfl)

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem xPrevIso_comp_dTo {i j : ι} (r : c.Rel i j) : (C.xPrevIso r).inv ≫ C.dTo j = C.d i j

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : c.Rel i j
⊢ (C.xPrevIso r).inv ≫ C.dTo j = C.d i j

Tactic:
simp [C.dTo_eq r]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem coe_filterMap : (s.filterMap f f_inj : Set β) = {b | ∃ a ∈ s, f a = some b} :=
  Set.ext (by simp only [mem_coe, mem_filterMap, Option.mem_def, Set.mem_setOf_eq, implies_true])

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
s : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
⊢ ∀ (x : β), x ∈ ↑(filterMap f s f_inj) ↔ x ∈ {b | ∃ a ∈ s, f a = some b}

Tactic:
simp only [mem_coe, mem_filterMap, Option.mem_def, Set.mem_setOf_eq, implies_true]

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem lintegral_pdf_mul {X : Ω → E} [HasPDF X ℙ μ] {f : E → ℝ≥0∞}
    (hf : AEMeasurable f μ) : ∫⁻ x, pdf X ℙ μ x * f x ∂μ = ∫⁻ x, f (X x) ∂ℙ

Proof state:
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (x : E), pdf X ℙ μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ

Tactic:
rw [pdf_def,
  ← lintegral_map' (hf.mono_ac HasPDF.absolutelyContinuous) (HasPDF.aemeasurable X ℙ μ),
  lintegral_rnDeriv_mul HasPDF.absolutelyContinuous hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue!_alterKey [EquivBEq α] {k k' : α} [Inhabited β] {f : Option β → Option β}
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
    getValue! k' (alterKey k f l) =
      if k == k' then
        (f (getValue? k l)).get!
      else
        getValue! k' l

Proof state:
α : Type u
inst✝² : BEq α
β : Type v
inst✝¹ : EquivBEq α
k k' : α
inst✝ : Inhabited β
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getValue! k' (alterKey k f l) = if (k == k') = true then (f (getValue? k l)).get! else getValue! k' l

Tactic:
simp only [hl, getValue!_eq_getValue?, getValue?_alterKey, beq_iff_eq, Function.comp_apply,
  apply_ite Option.get!]

Result:
no goals
-- Mathlib/Topology/Homotopy/Basic.lean
theorem extend_apply_of_le_zero (F : Homotopy f₀ f₁) {t : ℝ} (ht : t ≤ 0) (x : X) :
    F.extend t x = f₀ x

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : t ≤ 0
x : X
⊢ (F.extend t) x = F (0, x)

Tactic:
exact ContinuousMap.congr_fun (Set.IccExtend_of_le_left (zero_le_one' ℝ) F.curry ht) x

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : t ≤ 0
x : X
⊢ (F.extend t) x = f₀ x

Tactic:
rw [← F.apply_zero]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
t : ℝ
ht : t ≤ 0
x : X
⊢ (F.extend t) x = F (0, x)