harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Ext.lean
theorem CancelMonoid.toLeftCancelMonoid_injective {M : Type u} :
    Function.Injective (@CancelMonoid.toLeftCancelMonoid M)

Proof state:
case mk.mk
M : Type u
toLeftCancelMonoid✝¹ : LeftCancelMonoid M
mul_right_cancel✝¹ : ∀ (a b c : M), a * b = c * b → a = c
toLeftCancelMonoid✝ : LeftCancelMonoid M
mul_right_cancel✝ : ∀ (a b c : M), a * b = c * b → a = c
h : toLeftCancelMonoid = toLeftCancelMonoid
⊢ mk mul_right_cancel✝¹ = mk mul_right_cancel✝

Tactic:
congr

Result:
no goals

Proof state:
M : Type u
⊢ Injective (@toLeftCancelMonoid M)

Tactic:
rintro ⟨⟩ ⟨⟩ h

Result:
case mk.mk
M : Type u
toLeftCancelMonoid✝¹ : LeftCancelMonoid M
mul_right_cancel✝¹ : ∀ (a b c : M), a * b = c * b → a = c
toLeftCancelMonoid✝ : LeftCancelMonoid M
mul_right_cancel✝ : ∀ (a b c : M), a * b = c * b → a = c
h : toLeftCancelMonoid = toLeftCancelMonoid
⊢ mk mul_right_cancel✝¹ = mk mul_right_cancel✝
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.insert_indep_iff (hI : M.Indep I) :
    M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

Proof state:
case inr
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

Tactic:
rw [hI.insert_indep_iff_of_not_mem h, or_iff_left h]

Result:
no goals

Proof state:
case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

Tactic:
simp_rw [insert_eq_of_mem h, iff_true_intro hI, true_iff, iff_true_intro h, or_true]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

Tactic:
obtain (h | h) := em (e ∈ I)

Result:
case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

case inr
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
-- Mathlib/Algebra/BigOperators/WithTop.lean
/-- A sum is finite iff all terms are finite. -/
lemma sum_ne_top : ∑ i ∈ s, f i ≠ ⊤ ↔ ∀ i ∈ s, f i ≠ ⊤

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : AddCommMonoid α
s : Finset ι
f : ι → WithTop α
⊢ ∑ i ∈ s, f i ≠ ⊤ ↔ ∀ i ∈ s, f i ≠ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
@[simp] lemma mem_sigma : ∀ {p : Σa, σ a}, p ∈ @Multiset.sigma α σ s t ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
  | ⟨a, b⟩ => by simp [Multiset.sigma, and_assoc, and_left_comm]

Proof state:
α : Type u_1
σ : α → Type u_4
s : Multiset α
t : (a : α) → Multiset (σ a)
a : α
b : σ a
⊢ ⟨a, b⟩ ∈ s.sigma t ↔ ⟨a, b⟩.fst ∈ s ∧ ⟨a, b⟩.snd ∈ t ⟨a, b⟩.fst

Tactic:
simp [Multiset.sigma, and_assoc, and_left_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Opposite.lean
theorem imageUnopOp_inv_comp_op_factorThruImage :
    (imageUnopOp g).inv ≫ (factorThruImage g.unop).op = image.ι g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ (imageUnopOp g).inv ≫ (factorThruImage g.unop).op = image.ι g

Tactic:
rw [Iso.inv_comp_eq, imageUnopOp_hom_comp_image_ι]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Slope.lean
theorem isSeparable_range_derivWithin [SeparableSpace 𝕜] (f : 𝕜 → F) (s : Set 𝕜) :
    IsSeparable (range (derivWithin f s))

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure t
this : s ⊆ closure (s ∩ t)
⊢ IsSeparable (closure ↑(Submodule.span 𝕜 (f '' t)))

Tactic:
exact (Countable.image t_count f).isSeparable.span.closure

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure t
this : s ⊆ closure (s ∩ t)
⊢ IsSeparable (range (derivWithin f s))

Tactic:
apply IsSeparable.mono _ (range_derivWithin_subset_closure_span_image f this)

Result:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure t
this : s ⊆ closure (s ∩ t)
⊢ IsSeparable (closure ↑(Submodule.span 𝕜 (f '' t)))

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure t
⊢ s ⊆ closure (s ∩ t)

Tactic:
rwa [inter_eq_self_of_subset_right ts]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s : Set 𝕜
⊢ IsSeparable (range (derivWithin f s))

Tactic:
obtain ⟨t, ts, t_count, ht⟩ : ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ closure t :=
  (IsSeparable.of_separableSpace s).exists_countable_dense_subset

Result:
case intro.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure t
⊢ IsSeparable (range (derivWithin f s))

Proof state:
case intro.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure t
⊢ IsSeparable (range (derivWithin f s))

Tactic:
have : s ⊆ closure (s ∩ t) := by rwa [inter_eq_self_of_subset_right ts]

Result:
case intro.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure t
this : s ⊆ closure (s ∩ t)
⊢ IsSeparable (range (derivWithin f s))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem insertEntry_append_of_not_contains_right [BEq α] {l l' : List ((a : α) × β a)}
    {k : α} {v : β k} (h' : containsKey k l' = false) :
    insertEntry k v (l ++ l') = insertEntry k v l ++ l'

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h' : containsKey k l' = false
h : containsKey k l = true
⊢ insertEntry k v (l ++ l') = insertEntry k v l ++ l'

Tactic:
simp [insertEntry, containsKey_append, h, h', replaceEntry_append_of_containsKey_left h]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h' : containsKey k l' = false
⊢ insertEntry k v (l ++ l') = insertEntry k v l ++ l'

Tactic:
cases h : containsKey k l

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h' : containsKey k l' = false
h : containsKey k l = false
⊢ insertEntry k v (l ++ l') = insertEntry k v l ++ l'

case true
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h' : containsKey k l' = false
h : containsKey k l = true
⊢ insertEntry k v (l ++ l') = insertEntry k v l ++ l'

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h' : containsKey k l' = false
h : containsKey k l = false
⊢ insertEntry k v (l ++ l') = insertEntry k v l ++ l'

Tactic:
simp [insertEntry, containsKey_append, h, h']

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
lemma exists_iff_castSucc {P : Fin (n + 1) → Prop} :
    (∃ i, P i) ↔ P (last n) ∨ ∃ i : Fin n, P i.castSucc where
  mp

Proof state:
n : ℕ
P : Fin (n + 1) → Prop
⊢ (P (last n) ∨ ∃ i, P i.castSucc) → ∃ i, P i

Tactic:
rintro (h | ⟨i, hi⟩) <;> exact ⟨_, ‹_›⟩

Result:
no goals

Proof state:
case intro
n : ℕ
P : Fin (n + 1) → Prop
i : Fin (n + 1)
hi : P i
⊢ P (last n) ∨ ∃ i, P i.castSucc

Tactic:
induction' i using lastCases

Result:
case intro.last
n : ℕ
P : Fin (n + 1) → Prop
hi : P (last n)
⊢ P (last n) ∨ ∃ i, P i.castSucc

case intro.cast
n : ℕ
P : Fin (n + 1) → Prop
i✝ : Fin n
hi : P i✝.castSucc
⊢ P (last n) ∨ ∃ i, P i.castSucc

Proof state:
case intro.last
n : ℕ
P : Fin (n + 1) → Prop
hi : P (last n)
⊢ P (last n) ∨ ∃ i, P i.castSucc

Tactic:
exact .inl hi

Result:
no goals

Proof state:
case intro.cast
n : ℕ
P : Fin (n + 1) → Prop
i✝ : Fin n
hi : P i✝.castSucc
⊢ P (last n) ∨ ∃ i, P i.castSucc

Tactic:
exact .inr ⟨_, hi⟩

Result:
no goals

Proof state:
n : ℕ
P : Fin (n + 1) → Prop
⊢ (∃ i, P i) → P (last n) ∨ ∃ i, P i.castSucc

Tactic:
rintro ⟨i, hi⟩

Result:
case intro
n : ℕ
P : Fin (n + 1) → Prop
i : Fin (n + 1)
hi : P i
⊢ P (last n) ∨ ∃ i, P i.castSucc
-- Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
theorem directSumRight_tmul_lof (x : M₁') (i : ι₂) (y : M₂ i) :
    directSumRight R M₁' M₂ (x ⊗ₜ[R] DirectSum.lof R _ _ i y) =
    DirectSum.lof R _ _ i (x ⊗ₜ[R] y)

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
ι₂ : Type v₂
inst✝⁴ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝³ : AddCommMonoid M₁'
inst✝² : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝¹ : Module R M₁'
inst✝ : (i₂ : ι₂) → Module R (M₂ i₂)
x : M₁'
i : ι₂
y : M₂ i
⊢ (directSumRight R M₁' M₂) (x ⊗ₜ[R] (lof R ι₂ M₂ i) y) = (lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)

Tactic:
dsimp only [directSumRight, LinearEquiv.trans_apply, TensorProduct.comm_tmul]

Result:
R : Type u
inst✝⁵ : CommSemiring R
ι₂ : Type v₂
inst✝⁴ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝³ : AddCommMonoid M₁'
inst✝² : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝¹ : Module R M₁'
inst✝ : (i₂ : ι₂) → Module R (M₂ i₂)
x : M₁'
i : ι₂
y : M₂ i
⊢ (DFinsupp.mapRange.linearEquiv fun x => TensorProduct.comm R (M₂ x) M₁')
      ((directSumLeft R M₂ M₁') ((lof R ι₂ M₂ i) y ⊗ₜ[R] x)) =
    (lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
ι₂ : Type v₂
inst✝⁴ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝³ : AddCommMonoid M₁'
inst✝² : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝¹ : Module R M₁'
inst✝ : (i₂ : ι₂) → Module R (M₂ i₂)
x : M₁'
i : ι₂
y : M₂ i
⊢ (DFinsupp.mapRange.linearEquiv fun x => TensorProduct.comm R (M₂ x) M₁')
      ((directSumLeft R M₂ M₁') ((lof R ι₂ M₂ i) y ⊗ₜ[R] x)) =
    (lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)

Tactic:
rw [directSumLeft_tmul_lof]

Result:
R : Type u
inst✝⁵ : CommSemiring R
ι₂ : Type v₂
inst✝⁴ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝³ : AddCommMonoid M₁'
inst✝² : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝¹ : Module R M₁'
inst✝ : (i₂ : ι₂) → Module R (M₂ i₂)
x : M₁'
i : ι₂
y : M₂ i
⊢ (DFinsupp.mapRange.linearEquiv fun x => TensorProduct.comm R (M₂ x) M₁')
      ((lof R ι₂ (fun i => M₂ i ⊗[R] M₁') i) (y ⊗ₜ[R] x)) =
    (lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
ι₂ : Type v₂
inst✝⁴ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝³ : AddCommMonoid M₁'
inst✝² : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝¹ : Module R M₁'
inst✝ : (i₂ : ι₂) → Module R (M₂ i₂)
x : M₁'
i : ι₂
y : M₂ i
⊢ (DFinsupp.mapRange.linearEquiv fun x => TensorProduct.comm R (M₂ x) M₁')
      ((lof R ι₂ (fun i => M₂ i ⊗[R] M₁') i) (y ⊗ₜ[R] x)) =
    (lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)

Tactic:
exact DFinsupp.mapRange_single (hf := fun _ => rfl)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem setIntegral_prod (f : α × β → E) {s : Set α} {t : Set β}
    (hf : IntegrableOn f (s ×ˢ t) (μ.prod ν)) :
    ∫ z in s ×ˢ t, f z ∂μ.prod ν = ∫ x in s, ∫ y in t, f (x, y) ∂ν ∂μ

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α × β → E
s : Set α
t : Set β
hf : Integrable f ((μ.restrict s).prod (ν.restrict t))
⊢ ∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t) = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ

Tactic:
exact integral_prod f hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α × β → E
s : Set α
t : Set β
hf : IntegrableOn f (s ×ˢ t) (μ.prod ν)
⊢ ∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ

Tactic:
simp only [← Measure.prod_restrict s t, IntegrableOn] at hf ⊢

Result:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α × β → E
s : Set α
t : Set β
hf : Integrable f ((μ.restrict s).prod (ν.restrict t))
⊢ ∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t) = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_eq_nil_iff (l : Array α) : l.toList = [] ↔ l = #[]

Proof state:
α : Type u_1
l : Array α
⊢ l.toList = [] ↔ l = #[]

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/Ascoli.lean
/-- Let `X` be a topological space, `𝔖` a family of compact subsets of `X`, `α` a uniform space,
and `F : ι → (X → α)` a family which is equicontinuous on each `K ∈ 𝔖`. Then, the topologies
of uniform convergence on `𝔖` and pointwise convergence on `⋃₀ 𝔖` induce the same topology on  `ι`.

In particular, pointwise convergence and compact convergence coincide on an equicontinuous
subset of `X → α`.

This is a consequence of `EquicontinuousOn.comap_uniformOnFun_eq` stated in terms of `IsInducing`
for convenience. -/
lemma EquicontinuousOn.inducing_uniformOnFun_iff_pi' [TopologicalSpace ι]
    {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K)
    (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) :
    IsInducing (UniformOnFun.ofFun 𝔖 ∘ F) ↔
    IsInducing ((⋃₀ 𝔖).restrict ∘ F)

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ inst✝ = UniformSpace.toTopologicalSpace ↔ inst✝ = UniformSpace.toTopologicalSpace

Tactic:
rw [← EquicontinuousOn.comap_uniformOnFun_eq 𝔖_compact F_eqcont]

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsInducing ((⋃₀ 𝔖).restrict ∘ F)

Tactic:
rw [isInducing_iff, isInducing_iff]

Result:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ inst✝ = TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (UniformOnFun.topologicalSpace X α 𝔖) ↔
    inst✝ = TopologicalSpace.induced ((⋃₀ 𝔖).restrict ∘ F) Pi.topologicalSpace

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ inst✝ = TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (UniformOnFun.topologicalSpace X α 𝔖) ↔
    inst✝ = TopologicalSpace.induced ((⋃₀ 𝔖).restrict ∘ F) Pi.topologicalSpace

Tactic:
change (_ = ((UniformOnFun.uniformSpace X α 𝔖).comap F).toTopologicalSpace) ↔
  (_ = ((Pi.uniformSpace _).comap ((⋃₀ 𝔖).restrict ∘ F)).toTopologicalSpace)

Result:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ inst✝ = UniformSpace.toTopologicalSpace ↔ inst✝ = UniformSpace.toTopologicalSpace
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
theorem Integrable.condKernel_ae {f : α × Ω → F} (hf_int : Integrable f ρ) :
    ∀ᵐ a ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a)

Proof state:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
hf_ae : AEStronglyMeasurable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)

Tactic:
rw [← hf_ae.ae_integrable_condKernel_iff] at hf_int

Result:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int :
  (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧
    Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst
hf_ae : AEStronglyMeasurable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)

Proof state:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)

Tactic:
have hf_ae : AEStronglyMeasurable f ρ := hf_int.1

Result:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
hf_ae : AEStronglyMeasurable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)

Proof state:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int :
  (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧
    Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst
hf_ae : AEStronglyMeasurable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)

Tactic:
exact hf_int.1

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem isRoot_of_eval₂_map_eq_zero (hf : Function.Injective f) {r : R} :
    eval₂ f (f r) p = 0 → p.IsRoot r

Proof state:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
r : R
⊢ eval₂ f (f r) p = 0 → p.IsRoot r

Tactic:
intro h

Result:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
r : R
h : eval₂ f (f r) p = 0
⊢ p.IsRoot r

Proof state:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
r : R
h : eval₂ f (f r) p = 0
⊢ p.IsRoot r

Tactic:
apply hf

Result:
case a
R : Type u
S : Type v
inst✝¹ : CommSemiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
r : R
h : eval₂ f (f r) p = 0
⊢ f (eval r p) = f 0

Proof state:
case a
R : Type u
S : Type v
inst✝¹ : CommSemiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
r : R
h : eval₂ f (f r) p = 0
⊢ f (eval r p) = f 0

Tactic:
rw [← eval₂_hom, h, f.map_zero]

Result:
no goals
-- Mathlib/RingTheory/ClassGroup.lean
theorem mem_principal_ideals_iff {I : (FractionalIdeal R⁰ K)ˣ} :
    I ∈ (toPrincipalIdeal R K).range ↔ ∃ x : K, spanSingleton R⁰ x = I

Proof state:
case mpr.intro
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
hx : spanSingleton R⁰ 0 = ↑I
⊢ False

Tactic:
simp [I.ne_zero.symm] at hx

Result:
no goals

Proof state:
case mpr.intro
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ x ≠ 0

Tactic:
rintro rfl

Result:
case mpr.intro
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
hx : spanSingleton R⁰ 0 = ↑I
⊢ False

Proof state:
case mp.intro
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : Kˣ
hx : spanSingleton R⁰ ↑x = ↑I
⊢ ∃ x, spanSingleton R⁰ x = ↑I

Tactic:
exact ⟨x, hx⟩

Result:
no goals

Proof state:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
⊢ I ∈ (toPrincipalIdeal R K).range ↔ ∃ x, spanSingleton R⁰ x = ↑I

Tactic:
simp only [MonoidHom.mem_range, toPrincipalIdeal_eq_iff]

Result:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ ↑x = ↑I) ↔ ∃ x, spanSingleton R⁰ x = ↑I

Proof state:
case mpr.intro
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I

Tactic:
refine ⟨Units.mk0 x ?_, hx⟩

Result:
case mpr.intro
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ x ≠ 0

Proof state:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ ↑x = ↑I) ↔ ∃ x, spanSingleton R⁰ x = ↑I

Tactic:
constructor <;> rintro ⟨x, hx⟩

Result:
case mp.intro
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : Kˣ
hx : spanSingleton R⁰ ↑x = ↑I
⊢ ∃ x, spanSingleton R⁰ x = ↑I

case mpr.intro
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I