harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
lemma integrable_pow_mul_norm_one_add_mul_inv (n : ℕ) {z : ℂ} (hz : ‖z‖ < 1) :
    IntervalIntegrable (fun t : ℝ ↦ t ^ n * ‖(1 + t * z)⁻¹‖) MeasureTheory.volume 0 1

Proof state:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ IntervalIntegrable (fun t => t ^ n * ‖(1 + ↑t * z)⁻¹‖) MeasureTheory.volume 0 1

Tactic:
have := continuousOn_one_add_mul_inv <| mem_slitPlane_of_norm_lt_one hz

Result:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
this : ContinuousOn (fun t => (1 + t • z)⁻¹) (Set.Icc 0 1)
⊢ IntervalIntegrable (fun t => t ^ n * ‖(1 + ↑t * z)⁻¹‖) MeasureTheory.volume 0 1

Proof state:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
this : ContinuousOn (fun t => (1 + t • z)⁻¹) (Set.uIcc 0 1)
⊢ IntervalIntegrable (fun t => t ^ n * ‖(1 + ↑t * z)⁻¹‖) MeasureTheory.volume 0 1

Tactic:
exact ContinuousOn.intervalIntegrable (by fun_prop)

Result:
no goals

Proof state:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
this : ContinuousOn (fun t => (1 + t • z)⁻¹) (Set.Icc 0 1)
⊢ IntervalIntegrable (fun t => t ^ n * ‖(1 + ↑t * z)⁻¹‖) MeasureTheory.volume 0 1

Tactic:
rw [← Set.uIcc_of_le zero_le_one] at this

Result:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
this : ContinuousOn (fun t => (1 + t • z)⁻¹) (Set.uIcc 0 1)
⊢ IntervalIntegrable (fun t => t ^ n * ‖(1 + ↑t * z)⁻¹‖) MeasureTheory.volume 0 1

Proof state:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
this : ContinuousOn (fun t => (1 + t • z)⁻¹) (Set.uIcc 0 1)
⊢ ContinuousOn (fun t => t ^ n * ‖(1 + ↑t * z)⁻¹‖) (Set.uIcc 0 1)

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Algebra/Field/Periodic.lean
theorem Antiperiodic.const_inv_smul₀ [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α]
    (h : Antiperiodic f c) {a : γ} (ha : a ≠ 0) : Antiperiodic (fun x => f (a⁻¹ • x)) (a • c)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : AddCommMonoid α
inst✝² : Neg β
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Antiperiodic f c
a : γ
ha : a ≠ 0
⊢ Antiperiodic (fun x => f (a⁻¹ • x)) (a • c)

Tactic:
simpa only [inv_inv] using h.const_smul₀ (inv_ne_zero ha)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem hom_trans (C : G.ComponentCompl L) (h : K ⊆ L) (h' : M ⊆ K) :
    C.hom (h'.trans h) = (C.hom h).hom h'

Proof state:
V : Type u
G : SimpleGraph V
K L M : Set V
C : G.ComponentCompl L
h : K ⊆ L
h' : M ⊆ K
⊢ hom ⋯ C = hom h' (hom h C)

Tactic:
change C.map _ = (C.map _).map _

Result:
V : Type u
G : SimpleGraph V
K L M : Set V
C : G.ComponentCompl L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (induceHom Hom.id ⋯) C =
    ConnectedComponent.map (induceHom Hom.id ⋯) (ConnectedComponent.map (induceHom Hom.id ⋯) C)

Proof state:
V : Type u
G : SimpleGraph V
K L M : Set V
C : G.ComponentCompl L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (induceHom Hom.id ⋯) C =
    ConnectedComponent.map (induceHom Hom.id ⋯) (ConnectedComponent.map (induceHom Hom.id ⋯) C)

Tactic:
rw [ConnectedComponent.map_comp, induceHom_comp]

Result:
V : Type u
G : SimpleGraph V
K L M : Set V
C : G.ComponentCompl L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (induceHom Hom.id ⋯) C = ConnectedComponent.map (induceHom (Hom.id.comp Hom.id) ⋯) C

Proof state:
V : Type u
G : SimpleGraph V
K L M : Set V
C : G.ComponentCompl L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (induceHom Hom.id ⋯) C = ConnectedComponent.map (induceHom (Hom.id.comp Hom.id) ⋯) C

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isOpenMap_inl : IsOpenMap (@inl X Y) := fun u hu => by
  simpa [isOpen_sum_iff, preimage_image_eq u Sum.inl_injective]

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
u : Set X
hu : IsOpen u
⊢ IsOpen (inl '' u)

Tactic:
simpa [isOpen_sum_iff, preimage_image_eq u Sum.inl_injective]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_liftCover [Countable ι] (t : ι → Set α) (htm : ∀ i, MeasurableSet (t i))
    (f : ∀ i, t i → β) (hfm : ∀ i, Measurable (f i))
    (hf : ∀ (i j) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩)
    (htU : ⋃ i, t i = univ) :
    Measurable (liftCover t f hf htU) := fun s hs => by
  rw [preimage_liftCover]
  exact .iUnion fun i => .subtype_image (htm i) <| hfm i hs

Proof state:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → ↑(t i) → β
hfm : ∀ (i : ι), Measurable (f i)
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
htU : ⋃ i, t i = univ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (liftCover t f hf htU ⁻¹' s)

Tactic:
rw [preimage_liftCover]

Result:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → ↑(t i) → β
hfm : ∀ (i : ι), Measurable (f i)
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
htU : ⋃ i, t i = univ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (⋃ i, Subtype.val '' (f i ⁻¹' s))

Proof state:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → ↑(t i) → β
hfm : ∀ (i : ι), Measurable (f i)
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
htU : ⋃ i, t i = univ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (⋃ i, Subtype.val '' (f i ⁻¹' s))

Tactic:
exact .iUnion fun i => .subtype_image (htm i) <| hfm i hs

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
@[simp] lemma mem_Ico : x ∈ Ico a b ↔ a ≤ x ∧ x < b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ico a b ↔ a ≤ x ∧ x < b

Tactic:
rw [Ico, ← Finset.mem_def, Finset.mem_Ico]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Action/Basic.lean
theorem _root_.ErgodicSMul.of_aestabilizer [Group G] [MulAction G α] [SMulInvariantMeasure G α μ]
    (h : ∀ s, MeasurableSet s → aestabilizer G μ s = ⊤ → EventuallyConst s (ae μ)) :
    ErgodicSMul G α μ :=
  ⟨fun hm hs ↦ h _ hm <| (Subgroup.eq_top_iff' _).2 fun g ↦ by
    simpa only [preimage_smul_inv] using hs g⁻¹⟩

Proof state:
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : SMulInvariantMeasure G α μ
h : ∀ (s : Set α), MeasurableSet s → aestabilizer G μ s = ⊤ → EventuallyConst s (ae μ)
s✝ : Set α
hm : MeasurableSet s✝
hs : ∀ (g : G), (fun x => g • x) ⁻¹' s✝ =ᶠ[ae μ] s✝
g : G
⊢ g ∈ aestabilizer G μ s✝

Tactic:
simpa only [preimage_smul_inv] using hs g⁻¹

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem sumCongr_trans {X'' Y'' : Type*} [TopologicalSpace X''] [TopologicalSpace Y'']
    (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') (h₃ : X' ≃ₜ X'') (h₄ : Y' ≃ₜ Y'') :
    (sumCongr h₁ h₂).trans (sumCongr h₃ h₄) = sumCongr (h₁.trans h₃) (h₂.trans h₄)

Proof state:
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
X'' : Type u_7
Y'' : Type u_8
inst✝¹ : TopologicalSpace X''
inst✝ : TopologicalSpace Y''
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
h₃ : X' ≃ₜ X''
h₄ : Y' ≃ₜ Y''
⊢ (h₁.sumCongr h₂).trans (h₃.sumCongr h₄) = (h₁.trans h₃).sumCongr (h₂.trans h₄)

Tactic:
ext i

Result:
case H
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
X'' : Type u_7
Y'' : Type u_8
inst✝¹ : TopologicalSpace X''
inst✝ : TopologicalSpace Y''
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
h₃ : X' ≃ₜ X''
h₄ : Y' ≃ₜ Y''
i : X ⊕ Y
⊢ ((h₁.sumCongr h₂).trans (h₃.sumCongr h₄)) i = ((h₁.trans h₃).sumCongr (h₂.trans h₄)) i

Proof state:
case H
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
X'' : Type u_7
Y'' : Type u_8
inst✝¹ : TopologicalSpace X''
inst✝ : TopologicalSpace Y''
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
h₃ : X' ≃ₜ X''
h₄ : Y' ≃ₜ Y''
i : X ⊕ Y
⊢ ((h₁.sumCongr h₂).trans (h₃.sumCongr h₄)) i = ((h₁.trans h₃).sumCongr (h₂.trans h₄)) i

Tactic:
cases i <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem spanExt_hom_app_left : (spanExt iX iY iZ wf wg).hom.app WalkingSpan.left = iY.hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).hom.app WalkingSpan.left = iY.hom

Tactic:
dsimp [spanExt]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem nnnorm_eq [NumberField K] (x : K) :
    ‖canonicalEmbedding K x‖₊ = Finset.univ.sup (fun φ : K →+* ℂ => ‖φ x‖₊)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ‖(canonicalEmbedding K) x‖₊ = Finset.univ.sup fun φ => ‖φ x‖₊

Tactic:
simp_rw [Pi.nnnorm_def, apply_at]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem edist_le_of_edist_le_geometric_of_tendsto₀ {a : α} (ha : Tendsto f atTop (𝓝 a)) :
    edist (f 0) a ≤ C / (1 - r)

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ edist (f 0) a ≤ C / (1 - r)

Tactic:
simpa only [_root_.pow_zero, mul_one] using edist_le_of_edist_le_geometric_of_tendsto r C hu ha 0

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
@[simp]
lemma inverseImage_iff (P : MorphismProperty D) (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) :
    P.inverseImage F f ↔ P (F.map f)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ P.inverseImage F f ↔ P (F.map f)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_union [Fintype (s ∪ t : Set _)] : (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

Proof state:
case h
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∪ t)
a✝ : α
⊢ a✝ ∈ (s ∪ t).toFinset ↔ a✝ ∈ s.toFinset ∪ t.toFinset

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∪ t)
⊢ (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

Tactic:
ext

Result:
case h
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∪ t)
a✝ : α
⊢ a✝ ∈ (s ∪ t).toFinset ↔ a✝ ∈ s.toFinset ∪ t.toFinset
-- Mathlib/LinearAlgebra/Semisimple.lean
theorem IsSemisimple.of_mem_adjoin_singleton {a : End K M}
    (ha : a ∈ Algebra.adjoin K {f}) : a.IsSemisimple

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
a : End K M
ha : a ∈ Algebra.adjoin K {f}
⊢ a.IsSemisimple

Tactic:
rw [Algebra.adjoin_singleton_eq_range_aeval] at ha

Result:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
a : End K M
ha : a ∈ (aeval f).range
⊢ a.IsSemisimple

Proof state:
case intro
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
⊢ ((aeval f).toRingHom p).IsSemisimple

Tactic:
exact .aeval hf _

Result:
no goals

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
a : End K M
ha : a ∈ (aeval f).range
⊢ a.IsSemisimple

Tactic:
obtain ⟨p, rfl⟩ := ha

Result:
case intro
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
⊢ ((aeval f).toRingHom p).IsSemisimple
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem inner_left_of_mem_orthogonal {u v : E} (hu : u ∈ K) (hv : v ∈ Kᗮ) : ⟪v, u⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
⊢ inner u v = 0

Tactic:
exact inner_right_of_mem_orthogonal hu hv

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
⊢ inner v u = 0

Tactic:
rw [inner_eq_zero_symm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
⊢ inner u v = 0
-- Mathlib/Analysis/Calculus/MeanValue.lean
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is strictly positive,
then `f` is a strictly monotone function on `D`. -/
lemma strictMonoOn_of_hasDerivWithinAt_pos {D : Set ℝ} (hD : Convex ℝ D) {f f' : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x)
    (hf'₀ : ∀ x ∈ interior D, 0 < f' x) : StrictMonoOn f D :=
  strictMonoOn_of_deriv_pos hD hf fun x hx ↦ by
    rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx

Proof state:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 < f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 < deriv f x

Tactic:
rw [deriv_eqOn isOpen_interior hf' hx]

Result:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 < f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 < f' x

Proof state:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 < f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 < f' x

Tactic:
exact hf'₀ _ hx

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem coe_vanishingIdeal (t : Set (ProjectiveSpectrum 𝒜)) :
    (vanishingIdeal t : Set A) =
      { f | ∀ x : ProjectiveSpectrum 𝒜, x ∈ t → f ∈ x.asHomogeneousIdeal }

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
x : ProjectiveSpectrum 𝒜
⊢ f ∈ (⨅ (_ : x ∈ t), x.asHomogeneousIdeal).toIdeal ↔ x ∈ t → f ∈ x.asHomogeneousIdeal

Tactic:
rw [HomogeneousIdeal.toIdeal_iInf, Submodule.mem_iInf, HomogeneousIdeal.mem_iff]

Result:
no goals

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ ↑(vanishingIdeal t) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}

Tactic:
rw [vanishingIdeal, SetLike.mem_coe, ← HomogeneousIdeal.mem_iff, HomogeneousIdeal.toIdeal_iInf,
  Submodule.mem_iInf]

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ (∀ (i : ProjectiveSpectrum 𝒜), f ∈ (⨅ (_ : i ∈ t), i.asHomogeneousIdeal).toIdeal) ↔
    f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ (∀ (i : ProjectiveSpectrum 𝒜), f ∈ (⨅ (_ : i ∈ t), i.asHomogeneousIdeal).toIdeal) ↔
    f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}

Tactic:
refine forall_congr' fun x => ?_

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
x : ProjectiveSpectrum 𝒜
⊢ f ∈ (⨅ (_ : x ∈ t), x.asHomogeneousIdeal).toIdeal ↔ x ∈ t → f ∈ x.asHomogeneousIdeal

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ ↑(vanishingIdeal t) = {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}

Tactic:
ext f

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ ↑(vanishingIdeal t) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_ratCast_smul [DivisionRing R] [AddCommGroup α] [StarAddMonoid α] [Module R α]
    (c : ℚ) (M : Matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
  Matrix.ext <| by simp

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℚ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (↑c • M)ᴴ i j = (↑c • Mᴴ) i j

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Commute.lean
theorem div_left (hac : Commute a c) (hbc : Commute b c) : Commute (a / b) c

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a / b) c

Tactic:
rw [div_eq_mul_inv]

Result:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a * b⁻¹) c

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a * b⁻¹) c

Tactic:
exact hac.mul_left hbc.inv_left₀

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem bot_ne_top : (⊥ : AffineSubspace k P) ≠ ⊤

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
contra : ⊥ = ⊤
⊢ False

Tactic:
rw [AffineSubspace.ext_iff, bot_coe, top_coe] at contra

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
contra : ∅ = univ
⊢ False

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
contra : ∅ = univ
⊢ False

Tactic:
exact Set.empty_ne_univ contra

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
⊢ ⊥ ≠ ⊤

Tactic:
intro contra

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
contra : ⊥ = ⊤
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_eq_right_iff {p : Prop} [Decidable p] {x y : α} : (if p then x else y) = y ↔ p → x = y

Proof state:
α : Sort u_1
p : Prop
inst✝ : Decidable p
x y : α
⊢ (if p then x else y) = y ↔ p → x = y

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/List/Basic.lean
lemma mem_pair {a b c : α} : a ∈ [b, c] ↔ a = b ∨ a = c

Proof state:
α : Type u
a b c : α
⊢ a ∈ [b, c] ↔ a = b ∨ a = c

Tactic:
rw [mem_cons, mem_singleton]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_mul (n m : ℕ) :
    descPochhammer R n * (descPochhammer R m).comp (X - (n : R[X])) = descPochhammer R (n + m)

Proof state:
case zero
R : Type u
inst✝ : Ring R
n : ℕ
⊢ descPochhammer R n * (descPochhammer R 0).comp (X - ↑n) = descPochhammer R (n + 0)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
n m : ℕ
⊢ descPochhammer R n * (descPochhammer R m).comp (X - ↑n) = descPochhammer R (n + m)

Tactic:
induction' m with m ih

Result:
case zero
R : Type u
inst✝ : Ring R
n : ℕ
⊢ descPochhammer R n * (descPochhammer R 0).comp (X - ↑n) = descPochhammer R (n + 0)

case succ
R : Type u
inst✝ : Ring R
n m : ℕ
ih : descPochhammer R n * (descPochhammer R m).comp (X - ↑n) = descPochhammer R (n + m)
⊢ descPochhammer R n * (descPochhammer R (m + 1)).comp (X - ↑n) = descPochhammer R (n + (m + 1))

Proof state:
case succ
R : Type u
inst✝ : Ring R
n m : ℕ
ih : descPochhammer R n * (descPochhammer R m).comp (X - ↑n) = descPochhammer R (n + m)
⊢ descPochhammer R n * (descPochhammer R (m + 1)).comp (X - ↑n) = descPochhammer R (n + (m + 1))

Tactic:
rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
  ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Cover/Open.lean
theorem OpenCover.iSup_opensRange {X : Scheme.{u}} (𝒰 : X.OpenCover) :
    ⨆ i, (𝒰.map i).opensRange = ⊤ :=
  Opens.ext <| by rw [Opens.coe_iSup]; exact 𝒰.iUnion_range

Proof state:
X : Scheme
𝒰 : X.OpenCover
⊢ ↑(⨆ i, Hom.opensRange (𝒰.map i)) = ↑⊤

Tactic:
rw [Opens.coe_iSup]

Result:
X : Scheme
𝒰 : X.OpenCover
⊢ ⋃ i, ↑(Hom.opensRange (𝒰.map i)) = ↑⊤

Proof state:
X : Scheme
𝒰 : X.OpenCover
⊢ ⋃ i, ↑(Hom.opensRange (𝒰.map i)) = ↑⊤

Tactic:
exact 𝒰.iUnion_range

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpInd_disjoint_union (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ∞)
    (hμt : μ t ≠ ∞) (hst : Disjoint s t) : (condExpInd G hm μ (s ∪ t) : G →L[ℝ] α →₁[μ] G) =
    condExpInd G hm μ s + condExpInd G hm μ t

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
⊢ (condExpInd G hm μ (s ∪ t)) x = (condExpInd G hm μ s + condExpInd G hm μ t) x

Tactic:
push_cast

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
⊢ (condExpInd G hm μ (s ∪ t)) x = (⇑(condExpInd G hm μ s) + ⇑(condExpInd G hm μ t)) x

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
⊢ condExpInd G hm μ (s ∪ t) = condExpInd G hm μ s + condExpInd G hm μ t

Tactic:
ext1 x

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
⊢ (condExpInd G hm μ (s ∪ t)) x = (condExpInd G hm μ s + condExpInd G hm μ t) x

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
⊢ (condExpInd G hm μ (s ∪ t)) x = (⇑(condExpInd G hm μ s) + ⇑(condExpInd G hm μ t)) x

Tactic:
exact condExpInd_disjoint_union_apply hs ht hμs hμt hst x

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
@[reassoc (attr := simp)]
lemma πObj_ιIteration_app_right :
    πObj I κ f ≫ ((ιIteration I κ).app f).right =
      ((iteration I κ).obj (Arrow.mk f)).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
⊢ πObj I κ f ≫ ((ιIteration I κ).app (Arrow.mk f)).right = ((iteration I κ).obj (Arrow.mk f)).hom

Tactic:
simp [πObj]

Result:
no goals