harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem intervalIntegrable_iff : IntervalIntegrable f μ a b ↔ IntegrableOn f (Ι a b) μ

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ι a b) μ

Tactic:
rw [uIoc_eq_union, integrableOn_union, IntervalIntegrable]

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem truncate_self {a b : X} (γ : Path a b) (t : ℝ) :
    γ.truncate t t = (Path.refl <| γ.extend t).cast (by rw [min_self]) rfl

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
⊢ γ.truncate t t = (refl (γ.extend t)).cast ⋯ ⋯

Tactic:
ext x

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
⊢ (γ.truncate t t) x = ((refl (γ.extend t)).cast ⋯ ⋯) x

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
⊢ γ.extend (if (if ↑x ≤ t then t else ↑x) ≤ t then if ↑x ≤ t then t else ↑x else t) = γ.extend t

Tactic:
split_ifs with h₁ h₂ <;> congr

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ : Path x y
a b : X
γ : Path a b
t : ℝ
⊢ γ.extend (t ⊓ t) = γ.extend t

Tactic:
rw [min_self]

Result:
no goals

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
⊢ (γ.truncate t t) x = ((refl (γ.extend t)).cast ⋯ ⋯) x

Tactic:
rw [cast_coe]

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
⊢ (γ.truncate t t) x = (refl (γ.extend t)) x

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
⊢ (γ.truncate t t) x = (refl (γ.extend t)) x

Tactic:
simp only [truncate, DFunLike.coe, refl, min_def, max_def]

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
⊢ γ.extend (if (if ↑x ≤ t then t else ↑x) ≤ t then if ↑x ≤ t then t else ↑x else t) = γ.extend t
-- Mathlib/Topology/Order/T5.lean
theorem compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE (hd : Disjoint s (closure t))
    (ha : a ∈ s) : (ordConnectedSection <| ordSeparatingSet s t)ᶜ ∈ 𝓝[≤] a

Proof state:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure t)
ha : a ∈ s
hd' : Disjoint (⇑ofDual ⁻¹' s) (closure (⇑ofDual ⁻¹' t))
ha' : toDual a ∈ ⇑ofDual ⁻¹' s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a

Tactic:
simpa only [dual_ordSeparatingSet, dual_ordConnectedSection] using
  compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE hd' ha'

Result:
no goals

Proof state:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure t)
ha : a ∈ s
hd' : Disjoint (⇑ofDual ⁻¹' s) (closure (⇑ofDual ⁻¹' t))
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a

Tactic:
have ha' : toDual a ∈ ofDual ⁻¹' s := ha

Result:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure t)
ha : a ∈ s
hd' : Disjoint (⇑ofDual ⁻¹' s) (closure (⇑ofDual ⁻¹' t))
ha' : toDual a ∈ ⇑ofDual ⁻¹' s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a

Proof state:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure t)
ha : a ∈ s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a

Tactic:
have hd' : Disjoint (ofDual ⁻¹' s) (closure <| ofDual ⁻¹' t) := hd

Result:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure t)
ha : a ∈ s
hd' : Disjoint (⇑ofDual ⁻¹' s) (closure (⇑ofDual ⁻¹' t))
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_non_aestronglyMeasurable
    (hf : ¬AEStronglyMeasurable f (μ.restrict (Ι a b))) :
    ∫ x in a..b, f x ∂μ = 0

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : ¬AEStronglyMeasurable f (μ.restrict (Ι a b))
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0

Tactic:
rw [intervalIntegral_eq_integral_uIoc, integral_non_aestronglyMeasurable hf, smul_zero]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_ofFinset {p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) :
    @Set.toFinset _ p (Fintype.ofFinset s H) = s :=
  Finset.ext fun x => by rw [@mem_toFinset _ _ (id _), H]

Proof state:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
x : α
⊢ x ∈ p.toFinset ↔ x ∈ s

Tactic:
rw [@mem_toFinset _ _ (id _), H]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem Metric.uniformity_eq_comap_nhds_zero :
    𝓤 α = comap (fun p : α × α => dist p.1 p.2) (𝓝 (0 : ℝ))

Proof state:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (α × α)
⊢ s ∈ 𝓤 α ↔ s ∈ comap (fun p => dist p.1 p.2) (𝓝 0)

Tactic:
simp only [mem_uniformity_dist, (nhds_basis_ball.comap _).mem_iff]

Result:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (α × α)
⊢ (∃ ε > 0, ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ s) ↔ ∃ i, 0 < i ∧ (fun p => dist p.1 p.2) ⁻¹' ball 0 i ⊆ s

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ 𝓤 α = comap (fun p => dist p.1 p.2) (𝓝 0)

Tactic:
ext s

Result:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (α × α)
⊢ s ∈ 𝓤 α ↔ s ∈ comap (fun p => dist p.1 p.2) (𝓝 0)

Proof state:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (α × α)
⊢ (∃ ε > 0, ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ s) ↔ ∃ i, 0 < i ∧ (fun p => dist p.1 p.2) ⁻¹' ball 0 i ⊆ s

Tactic:
simp [subset_def, Real.dist_0_eq_abs]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
@[reassoc]
lemma basicOpenToSpec_SpecMap_awayMap :
    basicOpenToSpec 𝒜 x ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) =
      (Proj 𝒜).homOfLE (basicOpen_mono _ _ _ ⟨_, hx⟩) ≫ basicOpenToSpec 𝒜 f

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ (Proj 𝒜).homOfLE ⋯ ≫ (basicOpen 𝒜 f).toSpecΓ ≫ Spec.map (awayToSection 𝒜 f) = (Proj 𝒜).homOfLE ⋯ ≫ basicOpenToSpec 𝒜 f

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ basicOpenToSpec 𝒜 x ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) = (Proj 𝒜).homOfLE ⋯ ≫ basicOpenToSpec 𝒜 f

Tactic:
rw [basicOpenToSpec, Category.assoc, ← Spec.map_comp, awayMap_awayToSection,
  Spec.map_comp, Scheme.Opens.toSpecΓ_SpecMap_map_assoc]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ (Proj 𝒜).homOfLE ⋯ ≫ (basicOpen 𝒜 f).toSpecΓ ≫ Spec.map (awayToSection 𝒜 f) = (Proj 𝒜).homOfLE ⋯ ≫ basicOpenToSpec 𝒜 f
-- Mathlib/Data/Set/Lattice.lean
theorem image2_sInter_right_subset (t : Set α) (S : Set (Set β)) (f : α → β → γ) :
    image2 f t (⋂₀ S) ⊆ ⋂ s ∈ S, image2 f t s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Set α
S : Set (Set β)
f : α → β → γ
⊢ image2 f t (⋂₀ S) ⊆ ⋂ s ∈ S, image2 f t s

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_sub_nat (a : α) (n : ℕ) : fract (a - n) = fract a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ fract (a - ↑n) = fract a

Tactic:
rw [fract]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ a - ↑n - ↑⌊a - ↑n⌋ = fract a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ a - ↑n - ↑⌊a - ↑n⌋ = fract a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem of_partNum_eq_one {a : K} (nth_partNum_eq : (of v).partNums.get? n = some a) :
    a = 1

Proof state:
case intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_a_eq_a_n : gp.a = a
this : gp.a = 1
⊢ a = 1

Tactic:
rwa [gp_a_eq_a_n] at this

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_a_eq_a_n : gp.a = a
⊢ a = 1

Tactic:
have : gp.a = 1 := (of_partNum_eq_one_and_exists_int_partDen_eq nth_s_eq).left

Result:
case intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_a_eq_a_n : gp.a = a
this : gp.a = 1
⊢ a = 1

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
⊢ a = 1

Tactic:
obtain ⟨gp, nth_s_eq, gp_a_eq_a_n⟩ : ∃ gp, (of v).s.get? n = some gp ∧ gp.a = a :=
  exists_s_a_of_partNum nth_partNum_eq

Result:
case intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_a_eq_a_n : gp.a = a
⊢ a = 1
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem pairwise_univ : (univ : Set α).Pairwise r ↔ Pairwise r

Proof state:
α : Type u_1
r : α → α → Prop
⊢ univ.Pairwise r ↔ Pairwise r

Tactic:
simp only [Set.Pairwise, Pairwise, mem_univ, forall_const]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive sum_le_card_nsmul]
lemma prod_le_pow_card (s : Multiset α) (n : α) (h : ∀ x ∈ s, x ≤ n) : s.prod ≤ n ^ card s

Proof state:
case h
α : Type u_2
inst✝ : OrderedCommMonoid α
n : α
a✝ : List α
h : ∀ x ∈ ⟦a✝⟧, x ≤ n
⊢ prod ⟦a✝⟧ ≤ n ^ card ⟦a✝⟧

Tactic:
simpa using List.prod_le_pow_card _ _ h

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OrderedCommMonoid α
s : Multiset α
n : α
h : ∀ x ∈ s, x ≤ n
⊢ s.prod ≤ n ^ s.card

Tactic:
induction s using Quotient.inductionOn

Result:
case h
α : Type u_2
inst✝ : OrderedCommMonoid α
n : α
a✝ : List α
h : ∀ x ∈ ⟦a✝⟧, x ≤ n
⊢ prod ⟦a✝⟧ ≤ n ^ card ⟦a✝⟧
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.map_id_comp {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct W X]
    [HasBinaryProduct W Y] [HasBinaryProduct W Z] :
    prod.map (𝟙 W) (f ≫ g) = prod.map (𝟙 W) f ≫ prod.map (𝟙 W) g

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasBinaryProduct W X
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct W Z
⊢ map (𝟙 W) (f ≫ g) = map (𝟙 W) f ≫ map (𝟙 W) g

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
theorem le_mul_self : a ≤ b * a

Proof state:
α : Type u
inst✝² : CommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b : α
⊢ a ≤ a * b

Tactic:
exact le_self_mul

Result:
no goals

Proof state:
α : Type u
inst✝² : CommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b : α
⊢ a ≤ b * a

Tactic:
rw [mul_comm]

Result:
α : Type u
inst✝² : CommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b : α
⊢ a ≤ a * b
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem hasFiniteFPowerSeriesOnBall_changeOrigin (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (k : ℕ) (hn : ∀ (m : ℕ), n + k ≤ m → p m = 0) :
    HasFiniteFPowerSeriesOnBall (p.changeOrigin · k) (p.changeOriginSeries k) 0 n ⊤ :=
  (p.changeOriginSeries k).hasFiniteFPowerSeriesOnBall_of_finite
    (fun _ hm => p.changeOriginSeries_finite_of_finite hn k
    (by rw [add_comm n k]; apply add_le_add_left hm))

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n k : ℕ
hn : ∀ (m : ℕ), n + k ≤ m → p m = 0
x✝ : ℕ
hm : n ≤ x✝
⊢ k + n ≤ k + x✝

Tactic:
apply add_le_add_left hm

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n k : ℕ
hn : ∀ (m : ℕ), n + k ≤ m → p m = 0
x✝ : ℕ
hm : n ≤ x✝
⊢ n + k ≤ k + x✝

Tactic:
rw [add_comm n k]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n k : ℕ
hn : ∀ (m : ℕ), n + k ≤ m → p m = 0
x✝ : ℕ
hm : n ≤ x✝
⊢ k + n ≤ k + x✝
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma Monic.supDegree_pow
    (hzero : D 0 = 0) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) (hD : D.Injective)
    [Nontrivial R] (hp : p.Monic D) :
    (p ^ n).supDegree D = n • p.supDegree D

Proof state:
case zero
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
⊢ supDegree D (p ^ 0) = 0 • supDegree D p

Tactic:
rw [pow_zero, zero_nsmul, one_def, supDegree_single 0 1, if_neg one_ne_zero, hzero]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
n : ℕ
ih : supDegree D (p ^ n) = n • supDegree D p
⊢ supDegree D (p ^ (n + 1)) = (n + 1) • supDegree D p

Tactic:
rw [pow_succ', (hp.pow hadd hD).supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero,
ih, succ_nsmul']

Result:
no goals

Proof state:
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
⊢ supDegree D (p ^ n) = n • supDegree D p

Tactic:
induction n with
| zero => rw [pow_zero, zero_nsmul, one_def, supDegree_single 0 1, if_neg one_ne_zero, hzero]
| succ n ih => rw [pow_succ', (hp.pow hadd hD).supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero,
    ih, succ_nsmul']

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem quotEquivQuotMap_symm_apply_mk (f g : R[X]) (I : Ideal R) :
    (AdjoinRoot.quotEquivQuotMap f I).symm (Ideal.Quotient.mk _
      (Polynomial.map (Ideal.Quotient.mk I) g)) =
        Ideal.Quotient.mk (Ideal.map (of f) I) (AdjoinRoot.mk f g)

Proof state:
R : Type u
inst✝ : CommRing R
f g : R[X]
I : Ideal R
⊢ (quotEquivQuotMap f I).symm
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) g)

Tactic:
rw [AdjoinRoot.quotEquivQuotMap_symm_apply,
  AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem isUniformEmbedding_of_spaced_out {α} {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β)
    (hf : Pairwise fun x y => (f x, f y) ∉ s) : @IsUniformEmbedding α β ⊥ ‹_› f

Proof state:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
x✝ : UniformSpace α := ⊥
⊢ IsUniformEmbedding f

Tactic:
have := discreteTopology_bot α

Result:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
x✝ : UniformSpace α := ⊥
this : DiscreteTopology α
⊢ IsUniformEmbedding f

Proof state:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
x✝ : UniformSpace α := ⊥
this : DiscreteTopology α
⊢ IsUniformEmbedding f

Tactic:
exact IsUniformInducing.isUniformEmbedding ⟨comap_uniformity_of_spaced_out hs hf⟩

Result:
no goals

Proof state:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
⊢ IsUniformEmbedding f

Tactic:
let _ : UniformSpace α := ⊥

Result:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
x✝ : UniformSpace α := ⊥
⊢ IsUniformEmbedding f
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerLeft_inv_hom' (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
    X ◁ inv f ≫ X ◁ f = 𝟙 (X ⊗ Z)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ X ◁ inv f ≫ X ◁ f = 𝟙 (X ⊗ Z)

Tactic:
rw [← whiskerLeft_comp, IsIso.inv_hom_id, whiskerLeft_id]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem Orthonormal.isHilbertSum {v : ι → E} (hv : Orthonormal 𝕜 v)
    (hsp : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure) :
    IsHilbertSum 𝕜 (fun _ : ι => 𝕜) fun i => LinearIsometry.toSpanSingleton 𝕜 E (hv.1 i) :=
  IsHilbertSum.mk hv.orthogonalFamily (by
    convert hsp
    simp [← LinearMap.span_singleton_eq_range, ← Submodule.span_iUnion])

Proof state:
case h.e'_4.h.e'_9
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure
⊢ ⨆ i, LinearMap.range (LinearIsometry.toSpanSingleton 𝕜 E ⋯).toLinearMap = span 𝕜 (Set.range v)

Tactic:
simp [← LinearMap.span_singleton_eq_range, ← Submodule.span_iUnion]

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure
⊢ ⊤ ≤ (⨆ i, LinearMap.range (LinearIsometry.toSpanSingleton 𝕜 E ⋯).toLinearMap).topologicalClosure

Tactic:
convert hsp

Result:
case h.e'_4.h.e'_9
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure
⊢ ⨆ i, LinearMap.range (LinearIsometry.toSpanSingleton 𝕜 E ⋯).toLinearMap = span 𝕜 (Set.range v)
-- Mathlib/Data/DFinsupp/Interval.lean
theorem card_pi (f : Π₀ i, Finset (α i)) : #f.pi = f.prod fun i ↦ #(f i)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ ∏ i ∈ f.support, #(f i) = f.prod fun i => ↑(#(f i))

Tactic:
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.natCast_apply, Nat.cast_id]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ #f.pi = f.prod fun i => ↑(#(f i))

Tactic:
rw [pi, card_dfinsupp]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ ∏ i ∈ f.support, #(f i) = f.prod fun i => ↑(#(f i))

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
i : ι
x✝ : i ∈ f.support
⊢ #(f i) = (fun i => ↑(#(f i))) i (f i)

Tactic:
simp only [Pi.natCast_apply, Nat.cast_id]

Result:
no goals
-- Mathlib/Algebra/Homology/ImageToKernel.lean
theorem imageToKernel_comp_right {D : V} (h : C ⟶ D) (w : f ≫ g = 0) :
    imageToKernel f (g ≫ h) (by simp [reassoc_of% w]) =
      imageToKernel f g w ≫ Subobject.ofLE _ _ (kernelSubobject_comp_le g h)

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ imageToKernel f (g ≫ h) ⋯ = imageToKernel f g w ≫ (kernelSubobject g).ofLE (kernelSubobject (g ≫ h)) ⋯

Tactic:
ext

Result:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ imageToKernel f (g ≫ h) ⋯ ≫ (kernelSubobject (g ≫ h)).arrow =
    (imageToKernel f g w ≫ (kernelSubobject g).ofLE (kernelSubobject (g ≫ h)) ⋯) ≫ (kernelSubobject (g ≫ h)).arrow

Proof state:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ imageToKernel f (g ≫ h) ⋯ ≫ (kernelSubobject (g ≫ h)).arrow =
    (imageToKernel f g w ≫ (kernelSubobject g).ofLE (kernelSubobject (g ≫ h)) ⋯) ≫ (kernelSubobject (g ≫ h)).arrow

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ f ≫ g ≫ h = 0

Tactic:
simp [reassoc_of% w]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_cast (h : w = v) (x : BitVec w) : (x.cast h).getLsbD i = x.getLsbD i

Proof state:
w v i : Nat
h : w = v
x : BitVec w
⊢ (BitVec.cast h x).getLsbD i = x.getLsbD i

Tactic:
subst h

Result:
w i : Nat
x : BitVec w
⊢ (BitVec.cast ⋯ x).getLsbD i = x.getLsbD i

Proof state:
w i : Nat
x : BitVec w
⊢ (BitVec.cast ⋯ x).getLsbD i = x.getLsbD i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_insert_of_eq_one_if_not_mem (h : a ∉ s → f a = 1) :
    ∏ᶠ i ∈ insert a s, f i = ∏ᶠ i ∈ s, f i

Proof state:
case inl
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
x : α
hx : x ∈ mulSupport f
h : x ∉ s → f x = 1
⊢ x ∈ s

case inr
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
x : α
hx : x ∈ mulSupport f
hxs : x ∈ s
⊢ x ∈ s

Tactic:
exacts [not_imp_comm.1 h hx, hxs]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
⊢ ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
refine finprod_mem_inter_mulSupport_eq' _ _ _ fun x hx => ⟨?_, Or.inr⟩

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
x : α
hx : x ∈ mulSupport f
⊢ x ∈ insert a s → x ∈ s

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
x : α
hx : x ∈ mulSupport f
⊢ x ∈ insert a s → x ∈ s

Tactic:
rintro (rfl | hxs)

Result:
case inl
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
x : α
hx : x ∈ mulSupport f
h : x ∉ s → f x = 1
⊢ x ∈ s

case inr
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
x : α
hx : x ∈ mulSupport f
hxs : x ∈ s
⊢ x ∈ s
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem preimage_smul_closedBall (c : G) (x : X) (r : ℝ≥0∞) :
    (c • ·) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r

Proof state:
G : Type v
X : Type w
inst✝³ : PseudoEMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ (fun x => c • x) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r

Tactic:
rw [preimage_smul, smul_closedBall]

Result:
no goals