harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepSet.indep_generateFrom_le [LinearOrder ι] {s : ι → Set Ω}
    (hsm : ∀ n, MeasurableSet (s n)) (hs : iIndepSet s κ μ) (i : ι) {k : ι} (hk : i < k) :
    Indep (generateFrom {s k}) (generateFrom { t | ∃ j ≤ i, s j = t }) κ μ

Proof state:
case h.e'_4
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : LinearOrder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i k : ι
hk : i < k
⊢ generateFrom {s k} = generateFrom {t | ∃ n ∈ {k}, s n = t}

Tactic:
simp only [Set.mem_singleton_iff, exists_prop, exists_eq_left, Set.setOf_eq_eq_singleton']

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : LinearOrder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i k : ι
hk : i < k
⊢ Indep (generateFrom {s k}) (generateFrom {t | ∃ j ≤ i, s j = t}) κ μ

Tactic:
convert iIndepSet.indep_generateFrom_of_disjoint hsm hs {k} { j | j ≤ i }
    (Set.disjoint_singleton_left.mpr hk.not_le) using 1

Result:
case h.e'_4
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : LinearOrder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i k : ι
hk : i < k
⊢ generateFrom {s k} = generateFrom {t | ∃ n ∈ {k}, s n = t}
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorRightHomEquiv_whiskerLeft_comp_evaluation {X Y : C} [HasRightDual X] [HasRightDual Y]
    (f : X ⟶ Y) : (tensorRightHomEquiv _ _ _ _) ((Yᘁ : C) ◁ f ≫ ε_ _ _) = fᘁ ≫ (λ_ _).inv

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ (tensorRightHomEquiv Yᘁ X Xᘁ (𝟙_ C)) (Yᘁ ◁ f ≫ ε_ Y Yᘁ) = fᘁ ≫ (λ_ Xᘁ).inv

Tactic:
dsimp [tensorRightHomEquiv, rightAdjointMate]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ (α_ Yᘁ X Xᘁ).inv ≫ (Yᘁ ◁ f ≫ ε_ Y Yᘁ) ▷ Xᘁ =
    ((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫ (λ_ Xᘁ).inv

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ (α_ Yᘁ X Xᘁ).inv ≫ (Yᘁ ◁ f ≫ ε_ Y Yᘁ) ▷ Xᘁ =
    ((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫ (λ_ Xᘁ).inv

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem concat_perm (l : List α) (a : α) : concat l a ~ a :: l

Proof state:
α : Type u_1
l : List α
a : α
⊢ l.concat a ~ a :: l

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem isTransitive_iff_sUnion_subset : x.IsTransitive ↔ (⋃₀ x : ZFSet) ⊆ x

Proof state:
x : ZFSet.{u}
⊢ x.IsTransitive ↔ ⋃₀ x ⊆ x

Tactic:
constructor <;>
intro h y hy

Result:
case mp
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
⊢ y ∈ x

case mpr
x : ZFSet.{u}
h : ⋃₀ x ⊆ x
y : ZFSet.{u}
hy : y ∈ x
⊢ y ⊆ x

Proof state:
case mp
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
⊢ y ∈ x

Tactic:
obtain ⟨z, hz, hz'⟩ := mem_sUnion.1 hy

Result:
case mp.intro.intro
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ x
hz' : y ∈ z
⊢ y ∈ x

Proof state:
case mp.intro.intro
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ x
hz' : y ∈ z
⊢ y ∈ x

Tactic:
exact h.mem_trans hz' hz

Result:
no goals

Proof state:
case mpr
x : ZFSet.{u}
h : ⋃₀ x ⊆ x
y : ZFSet.{u}
hy : y ∈ x
⊢ y ⊆ x

Tactic:
exact fun z hz ↦ h <| mem_sUnion_of_mem hz hy

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_map_polynomial (q : R[X]) (f : R → R) (a : A) (ha : p a

Proof state:
case h_C
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
r : R
⊢ cfc (fun x => Polynomial.eval (f x) (Polynomial.C r)) a = (aeval (cfc f a)) (Polynomial.C r)

Tactic:
simp [cfc_const r a]

Result:
no goals

Proof state:
case h_monomial
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
n : ℕ
r : R
a✝ : cfc (fun x => Polynomial.eval (f x) (Polynomial.C r * X ^ n)) a = (aeval (cfc f a)) (Polynomial.C r * X ^ n)
⊢ cfc (fun x => Polynomial.eval (f x) (Polynomial.C r * X ^ (n + 1))) a =
    (aeval (cfc f a)) (Polynomial.C r * X ^ (n + 1))

Tactic:
simp only [eval_mul, eval_C, eval_pow, eval_X, map_mul, aeval_C, map_pow, aeval_X]

Result:
case h_monomial
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
n : ℕ
r : R
a✝ : cfc (fun x => Polynomial.eval (f x) (Polynomial.C r * X ^ n)) a = (aeval (cfc f a)) (Polynomial.C r * X ^ n)
⊢ cfc (fun x => r * f x ^ (n + 1)) a = (algebraMap R A) r * cfc f a ^ (n + 1)

Proof state:
case h_monomial
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
n : ℕ
r : R
a✝ : cfc (fun x => Polynomial.eval (f x) (Polynomial.C r * X ^ n)) a = (aeval (cfc f a)) (Polynomial.C r * X ^ n)
⊢ cfc (fun x => r * f x ^ (n + 1)) a = (algebraMap R A) r * cfc f a ^ (n + 1)

Tactic:
rw [cfc_const_mul .., cfc_pow _ (n + 1) _, ← smul_eq_mul, algebraMap_smul]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem Commute.tsum_right (a) (h : ∀ i, Commute a (f i)) : Commute a (∑' i, f i)

Proof state:
case pos
ι : Type u_1
α : Type u_3
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
inst✝ : T2Space α
a : α
h : ∀ (i : ι), Commute a (f i)
hf : Summable f
⊢ Commute a (∑' (i : ι), f i)

Tactic:
exact (hf.tsum_mul_left a).symm.trans ((congr_arg _ <| funext h).trans (hf.tsum_mul_right a))

Result:
no goals

Proof state:
case neg
ι : Type u_1
α : Type u_3
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
inst✝ : T2Space α
a : α
h : ∀ (i : ι), Commute a (f i)
hf : ¬Summable f
⊢ Commute a (∑' (i : ι), f i)

Tactic:
exact (tsum_eq_zero_of_not_summable hf).symm ▸ Commute.zero_right _

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
inst✝ : T2Space α
a : α
h : ∀ (i : ι), Commute a (f i)
⊢ Commute a (∑' (i : ι), f i)

Tactic:
by_cases hf : Summable f

Result:
case pos
ι : Type u_1
α : Type u_3
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
inst✝ : T2Space α
a : α
h : ∀ (i : ι), Commute a (f i)
hf : Summable f
⊢ Commute a (∑' (i : ι), f i)

case neg
ι : Type u_1
α : Type u_3
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
inst✝ : T2Space α
a : α
h : ∀ (i : ι), Commute a (f i)
hf : ¬Summable f
⊢ Commute a (∑' (i : ι), f i)
-- Mathlib/Data/Finsupp/BigOperators.lean
theorem List.mem_foldr_sup_support_iff [Zero M] {l : List (ι →₀ M)} {x : ι} :
    x ∈ l.foldr (Finsupp.support · ⊔ ·) ∅ ↔ ∃ f ∈ l, x ∈ f.support

Proof state:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
l : List (ι →₀ M)
x : ι
⊢ x ∈ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ l ↔ ∃ f ∈ l, x ∈ f.support

Tactic:
simp only [Finset.sup_eq_union, List.foldr_map, Finsupp.mem_support_iff, exists_prop]

Result:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
l : List (ι →₀ M)
x : ι
⊢ x ∈ foldr (fun x1 x2 => x1.support ∪ x2) ∅ l ↔ ∃ f ∈ l, f x ≠ 0

Proof state:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
l : List (ι →₀ M)
x : ι
⊢ x ∈ foldr (fun x1 x2 => x1.support ∪ x2) ∅ l ↔ ∃ f ∈ l, f x ≠ 0

Tactic:
induction' l with hd tl IH

Result:
case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
⊢ x ∈ foldr (fun x1 x2 => x1.support ∪ x2) ∅ [] ↔ ∃ f ∈ [], f x ≠ 0

case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
hd : ι →₀ M
tl : List (ι →₀ M)
IH : x ∈ foldr (fun x1 x2 => x1.support ∪ x2) ∅ tl ↔ ∃ f ∈ tl, f x ≠ 0
⊢ x ∈ foldr (fun x1 x2 => x1.support ∪ x2) ∅ (hd :: tl) ↔ ∃ f ∈ hd :: tl, f x ≠ 0

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
hd : ι →₀ M
tl : List (ι →₀ M)
IH : x ∈ foldr (fun x1 x2 => x1.support ∪ x2) ∅ tl ↔ ∃ f ∈ tl, f x ≠ 0
⊢ x ∈ foldr (fun x1 x2 => x1.support ∪ x2) ∅ (hd :: tl) ↔ ∃ f ∈ hd :: tl, f x ≠ 0

Tactic:
simp only [foldr, Function.comp_apply, Finset.mem_union, Finsupp.mem_support_iff, ne_eq, IH,
  find?, mem_cons, exists_eq_or_imp]

Result:
no goals

Proof state:
case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
⊢ x ∈ foldr (fun x1 x2 => x1.support ∪ x2) ∅ [] ↔ ∃ f ∈ [], f x ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/EulerProduct/ExpLog.lean
/-- If `f : α → ℂ` is summable, then so is `n ↦ log (1 - f n)`. -/
lemma Summable.clog_one_sub {α  : Type*} {f : α → ℂ} (hsum : Summable f) :
    Summable fun n ↦ log (1 - f n)

Proof state:
α : Type u_1
f : α → ℂ
hsum : Summable f
this : 1 - 0 ∈ slitPlane
⊢ DifferentiableAt ℂ (fun z => log (1 - z)) 0

Tactic:
fun_prop (disch := assumption)

Result:
no goals

Proof state:
α : Type u_1
f : α → ℂ
hsum : Summable f
⊢ Summable fun n => log (1 - f n)

Tactic:
have hg : DifferentiableAt ℂ (fun z ↦ log (1 - z)) 0 := by
  have : 1 - 0 ∈ slitPlane := (sub_zero (1 : ℂ)).symm ▸ one_mem_slitPlane
  fun_prop (disch := assumption)

Result:
α : Type u_1
f : α → ℂ
hsum : Summable f
hg : DifferentiableAt ℂ (fun z => log (1 - z)) 0
⊢ Summable fun n => log (1 - f n)

Proof state:
α : Type u_1
f : α → ℂ
hsum : Summable f
hg : DifferentiableAt ℂ (fun z => log (1 - z)) 0
⊢ Summable fun n => log (1 - f n)

Tactic:
have : (fun z ↦ log (1 - z)) =O[𝓝 0] id := by
  simpa only [sub_zero, log_one] using hg.isBigO_sub

Result:
α : Type u_1
f : α → ℂ
hsum : Summable f
hg : DifferentiableAt ℂ (fun z => log (1 - z)) 0
this : (fun z => log (1 - z)) =O[𝓝 0] id
⊢ Summable fun n => log (1 - f n)

Proof state:
α : Type u_1
f : α → ℂ
hsum : Summable f
hg : DifferentiableAt ℂ (fun z => log (1 - z)) 0
⊢ (fun z => log (1 - z)) =O[𝓝 0] id

Tactic:
simpa only [sub_zero, log_one] using hg.isBigO_sub

Result:
no goals

Proof state:
α : Type u_1
f : α → ℂ
hsum : Summable f
⊢ DifferentiableAt ℂ (fun z => log (1 - z)) 0

Tactic:
have : 1 - 0 ∈ slitPlane := (sub_zero (1 : ℂ)).symm ▸ one_mem_slitPlane

Result:
α : Type u_1
f : α → ℂ
hsum : Summable f
this : 1 - 0 ∈ slitPlane
⊢ DifferentiableAt ℂ (fun z => log (1 - z)) 0

Proof state:
case funProp.discharger
α : Type u_1
f : α → ℂ
hsum : Summable f
this : 1 - 0 ∈ slitPlane
⊢ 1 - 0 ∈ slitPlane

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
f : α → ℂ
hsum : Summable f
hg : DifferentiableAt ℂ (fun z => log (1 - z)) 0
this : (fun z => log (1 - z)) =O[𝓝 0] id
⊢ Summable fun n => log (1 - f n)

Tactic:
exact this.comp_summable hsum

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem ofDual_max' {s : Finset αᵒᵈ} (hs : s.Nonempty) :
    ofDual (max' s hs) = min' (s.image ofDual) (hs.image _)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ ↑(ofDual (s.max' hs)) = ↑((image (⇑ofDual) s).min' ⋯)

Tactic:
simp only [max'_eq_sup', id_eq, ofDual_sup', Function.comp_apply, coe_inf', min'_eq_inf',
  inf_image]

Result:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ s.inf (WithTop.some ∘ fun x => ofDual x) = s.inf ((WithTop.some ∘ fun x => x) ∘ ⇑ofDual)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ s.inf (WithTop.some ∘ fun x => ofDual x) = s.inf ((WithTop.some ∘ fun x => x) ∘ ⇑ofDual)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ ofDual (s.max' hs) = (image (⇑ofDual) s).min' ⋯

Tactic:
rw [← WithTop.coe_eq_coe]

Result:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ ↑(ofDual (s.max' hs)) = ↑((image (⇑ofDual) s).min' ⋯)
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_X_sub_pow (n k : ℕ) (c : R) :
    derivative^[k] ((X - C c) ^ n) = n.descFactorial k • (X - C c) ^ (n - k)

Proof state:
R : Type u
inst✝ : CommRing R
n k : ℕ
c : R
⊢ (⇑derivative)^[k] ((X - C c) ^ n) = n.descFactorial k • (X - C c) ^ (n - k)

Tactic:
rw [sub_eq_add_neg, ← C_neg, iterate_derivative_X_add_pow]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/TensorProduct.lean
@[local simp]
lemma mulActionBaseChange_smul_zero (a : A) :
    a • (0 : S ⊗[R] Ω[A⁄R]) = 0

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
⊢ a • 0 = 0

Tactic:
rw [← zero_tmul _ (0 : Ω[A⁄R]), mulActionBaseChange_smul_tmul, smul_zero]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_piCongrLeft (f : δ' ≃ δ) : Measurable (piCongrLeft π f)

Proof state:
δ : Type u_4
δ' : Type u_5
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
f : δ' ≃ δ
i : δ
⊢ Measurable fun x => (piCongrLeft π f) x i

Tactic:
simp_rw [piCongrLeft_apply_eq_cast]

Result:
δ : Type u_4
δ' : Type u_5
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
f : δ' ≃ δ
i : δ
⊢ Measurable fun x => cast ⋯ (x (f.symm i))

Proof state:
δ : Type u_4
δ' : Type u_5
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
f : δ' ≃ δ
i : δ
⊢ Measurable fun x => cast ⋯ (x (f.symm i))

Tactic:
exact Measurable.eq_mp π (f.apply_symm_apply i) <| measurable_pi_apply <| f.symm i

Result:
no goals

Proof state:
δ : Type u_4
δ' : Type u_5
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
f : δ' ≃ δ
⊢ Measurable ⇑(piCongrLeft π f)

Tactic:
rw [measurable_pi_iff]

Result:
δ : Type u_4
δ' : Type u_5
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
f : δ' ≃ δ
⊢ ∀ (a : δ), Measurable fun x => (piCongrLeft π f) x a

Proof state:
δ : Type u_4
δ' : Type u_5
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
f : δ' ≃ δ
⊢ ∀ (a : δ), Measurable fun x => (piCongrLeft π f) x a

Tactic:
intro i

Result:
δ : Type u_4
δ' : Type u_5
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
f : δ' ≃ δ
i : δ
⊢ Measurable fun x => (piCongrLeft π f) x i
-- Mathlib/Algebra/Regular/Basic.lean
/-- Any power of a right-regular element is right-regular. -/
lemma IsRightRegular.pow (n : ℕ) (rra : IsRightRegular a) : IsRightRegular (a ^ n)

Proof state:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ IsRightRegular (a ^ n)

Tactic:
rw [IsRightRegular, ← mul_right_iterate]

Result:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective (fun x => x * a)^[n]

Proof state:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective (fun x => x * a)^[n]

Tactic:
exact rra.iterate n

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedDeriv_zero : iteratedDeriv 0 f = f

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ iteratedDeriv 0 f x = f x

Tactic:
simp [iteratedDeriv]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ iteratedDeriv 0 f = f

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ iteratedDeriv 0 f x = f x
-- Mathlib/Algebra/Polynomial/Module/Basic.lean
theorem smul_apply (f : R[X]) (g : PolynomialModule R M) (n : ℕ) :
    (f • g) n = ∑ x ∈ Finset.antidiagonal n, f.coeff x.1 • g x.2

Proof state:
case h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (∑ x ∈ Finset.range n.succ, if f_n = x then f_a • g (n - x) else 0) =
    ∑ x ∈ Finset.range n.succ, (if f_n = x then f_a else 0) • g (n - x)

Tactic:
congr

Result:
case h_monomial.e_f
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (fun x => if f_n = x then f_a • g (n - x) else 0) = fun x => (if f_n = x then f_a else 0) • g (n - x)
-- Mathlib/Analysis/Calculus/Deriv/Polynomial.lean
theorem hasStrictDerivAt_aeval (x : 𝕜) :
    HasStrictDerivAt (fun x => aeval x q) (aeval x (derivative q)) x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R 𝕜
q : R[X]
x : 𝕜
⊢ HasStrictDerivAt (fun x => (aeval x) q) ((aeval x) (derivative q)) x

Tactic:
simpa only [aeval_def, eval₂_eq_eval_map, derivative_map] using
  (q.map (algebraMap R 𝕜)).hasStrictDerivAt x

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addZ_self (P : Fin 3 → R) : W'.addZ P P = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * P z ^ 2 - P y ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * P z ^ 2 -
                  W'.a₁ * P x * P y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * P z ^ 2 -
          W'.a₃ * P y * P z ^ 2 * P z -
        W'.a₄ * P x * P z * P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * P z =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.addZ P P = 0

Tactic:
rw [addZ]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * P z ^ 2 - P y ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * P z ^ 2 -
                  W'.a₁ * P x * P y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * P z ^ 2 -
          W'.a₃ * P y * P z ^ 2 * P z -
        W'.a₄ * P x * P z * P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * P z =
    0
-- Mathlib/CategoryTheory/Generator/Basic.lean
lemma IsCoseparating.of_equivalence
    {𝒢 : Set C} (h : IsCoseparating 𝒢) {D : Type*} [Category D] (α : C ≌ D) :
    IsCoseparating (α.functor.obj '' 𝒢) := fun X Y f g H =>
  α.inverse.map_injective (h _ _ (fun Z hZ h => by
    obtain ⟨h', rfl⟩ := (α.symm.toAdjunction.homEquiv _ _).symm.surjective h
    simp only [Adjunction.homEquiv_symm_apply, ← Category.assoc, ← Functor.map_comp,
      Equivalence.symm_functor, H (α.functor.obj Z) (Set.mem_image_of_mem _ hZ) h']))

Proof state:
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h : IsCoseparating 𝒢
D : Type u_1
inst✝ : Category.{u_2, u_1} D
α : C ≌ D
X Y : D
f g : X ⟶ Y
H : ∀ G ∈ α.functor.obj '' 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
Z : C
hZ : Z ∈ 𝒢
h' : Y ⟶ α.symm.inverse.obj Z
⊢ α.inverse.map f ≫ (α.symm.toAdjunction.homEquiv Y Z).symm h' =
    α.inverse.map g ≫ (α.symm.toAdjunction.homEquiv Y Z).symm h'

Tactic:
simp only [Adjunction.homEquiv_symm_apply, ← Category.assoc, ← Functor.map_comp,
  Equivalence.symm_functor, H (α.functor.obj Z) (Set.mem_image_of_mem _ hZ) h']

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h✝ : IsCoseparating 𝒢
D : Type u_1
inst✝ : Category.{u_2, u_1} D
α : C ≌ D
X Y : D
f g : X ⟶ Y
H : ∀ G ∈ α.functor.obj '' 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
Z : C
hZ : Z ∈ 𝒢
h : α.inverse.obj Y ⟶ Z
⊢ α.inverse.map f ≫ h = α.inverse.map g ≫ h

Tactic:
obtain ⟨h', rfl⟩ := (α.symm.toAdjunction.homEquiv _ _).symm.surjective h

Result:
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h : IsCoseparating 𝒢
D : Type u_1
inst✝ : Category.{u_2, u_1} D
α : C ≌ D
X Y : D
f g : X ⟶ Y
H : ∀ G ∈ α.functor.obj '' 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
Z : C
hZ : Z ∈ 𝒢
h' : Y ⟶ α.symm.inverse.obj Z
⊢ α.inverse.map f ≫ (α.symm.toAdjunction.homEquiv Y Z).symm h' =
    α.inverse.map g ≫ (α.symm.toAdjunction.homEquiv Y Z).symm h'
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem card_le_card_biUnion {s : Finset ι} {f : ι → Finset α} (hs : (s : Set ι).PairwiseDisjoint f)
    (hf : ∀ i ∈ s, (f i).Nonempty) : #s ≤ #(s.biUnion f)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
hf : ∀ i ∈ s, (f i).Nonempty
⊢ #s ≤ #(s.biUnion f)

Tactic:
rw [card_biUnion hs, card_eq_sum_ones]

Result:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
hf : ∀ i ∈ s, (f i).Nonempty
⊢ ∑ x ∈ s, 1 ≤ ∑ u ∈ s, #(f u)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
hf : ∀ i ∈ s, (f i).Nonempty
⊢ ∑ x ∈ s, 1 ≤ ∑ u ∈ s, #(f u)

Tactic:
exact sum_le_sum fun i hi ↦ (hf i hi).card_pos

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Dual.lean
theorem separatingLeft_dualProd :
    (dualProd R M).SeparatingLeft ↔ Function.Injective (Module.Dual.eval R M)

Proof state:
case refine_2.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
x : Module.Dual R M × M
x✝ : Module.Dual R M
⊢ (h_d x).2 x✝ = ((id.prodMap (Module.Dual.eval R M)) x).2 x✝

Tactic:
dsimp [e, h_d, Module.Dual.eval, LinearEquiv.prodComm]

Result:
case refine_2.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
x : Module.Dual R M × M
x✝ : Module.Dual R M
⊢ x✝ x.2 + x.1 0 = x✝ x.2