harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupExtension/Defs.lean
theorem rightHom_comp_inl : S.rightHom.comp S.inl = 1

Proof state:
case h
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
n : N
⊢ (S.rightHom.comp S.inl) n = 1 n

Tactic:
rw [MonoidHom.one_apply, MonoidHom.comp_apply]

Result:
case h
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
n : N
⊢ S.rightHom (S.inl n) = 1

Proof state:
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
⊢ S.rightHom.comp S.inl = 1

Tactic:
ext n

Result:
case h
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
n : N
⊢ (S.rightHom.comp S.inl) n = 1 n

Proof state:
case h
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
n : N
⊢ S.rightHom (S.inl n) = 1

Tactic:
exact S.rightHom_inl n

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
theorem algHom_ext_iff {φ₁ φ₂ : k[G] →ₐ[k] A} :
    (∀ x, φ₁ (Finsupp.single x 1) = φ₂ (Finsupp.single x 1)) ↔ φ₁ = φ₂ :=
  ⟨fun h => algHom_ext h, by rintro rfl _; rfl⟩

Proof state:
k : Type u₁
G : Type u₂
inst✝³ : CommSemiring k
inst✝² : AddMonoid G
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra k A
φ₁ φ₂ : k[G] →ₐ[k] A
⊢ φ₁ = φ₂ → ∀ (x : G), φ₁ (Finsupp.single x 1) = φ₂ (Finsupp.single x 1)

Tactic:
rintro rfl _

Result:
k : Type u₁
G : Type u₂
inst✝³ : CommSemiring k
inst✝² : AddMonoid G
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra k A
φ₁ : k[G] →ₐ[k] A
x✝ : G
⊢ φ₁ (Finsupp.single x✝ 1) = φ₁ (Finsupp.single x✝ 1)

Proof state:
k : Type u₁
G : Type u₂
inst✝³ : CommSemiring k
inst✝² : AddMonoid G
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra k A
φ₁ : k[G] →ₐ[k] A
x✝ : G
⊢ φ₁ (Finsupp.single x✝ 1) = φ₁ (Finsupp.single x✝ 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
/-- Composing a formal multilinear series with an ordered partition extended by adding a left point
to an already existing atom of index `i` corresponds to updating the `i`th block,
using `p (c.partSize i + 1)` instead of `p (c.partSize i)` there.
This is one of the terms that appears when differentiating in the Faa di Bruno
formula, going from step `m` to step `m + 1`. -/
private lemma faaDiBruno_aux2 {m : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
    (p : FormalMultilinearSeries 𝕜 E F) (c : OrderedFinpartition m) (i : Fin c.length) :
    (q.compAlongOrderedFinpartition p (c.extend (some i))).curryLeft =
    ((c.compAlongOrderedFinpartitionL 𝕜 E F G (q c.length)).toContinuousLinearMap
      (fun i ↦ p (c.partSize i)) i).comp (p (c.partSize i + 1)).curryLeft

Proof state:
case h.H.h.e_6.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
i : Fin c.length
e : E
v : Fin m → E
⊢ (fun m_1 =>
      (p (update c.partSize i (c.partSize i + 1) m_1))
        (cons e v ∘
          if h : m_1 = i then (fun i_1 => cases 0 (succ ∘ c.emb i) i_1) ∘ Fin.cast ⋯
          else succ ∘ c.emb m_1 ∘ Fin.cast ⋯)) =
    fun m_1 => (update (fun i => p (c.partSize i)) i ((p (c.partSize i + 1)).curryLeft e) m_1) (v ∘ c.emb m_1)

Tactic:
ext j

Result:
case h.H.h.e_6.h.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
i : Fin c.length
e : E
v : Fin m → E
j : Fin c.length
⊢ (p (update c.partSize i (c.partSize i + 1) j))
      (cons e v ∘
        if h : j = i then (fun i_1 => cases 0 (succ ∘ c.emb i) i_1) ∘ Fin.cast ⋯ else succ ∘ c.emb j ∘ Fin.cast ⋯) =
    (update (fun i => p (c.partSize i)) i ((p (c.partSize i + 1)).curryLeft e) j) (v ∘ c.emb j)
-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
theorem isEquipartition [DecidableEq V] : h.finpartition.IsEquipartition

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
⊢ fp.IsEquipartition

Tactic:
by_contra hn

Result:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
hn : ¬fp.IsEquipartition
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
⊢ False

Tactic:
apply absurd h

Result:
case intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
⊢ ¬G.IsTuranMaximal r

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
hn : small = large
⊢ False

Tactic:
rw [hn] at ineq

Result:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #large + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
hn : small = large
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem le_rpow_inv_iff {x y : ℝ≥0} {z : ℝ} (hz : 0 < z) : x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Proof state:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
rw [← rpow_le_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz.ne']

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_eq_sInf_lsub (o : Ordinal.{u}) : cof o =
    sInf { a : Cardinal | ∃ (ι : Type u) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = a }

Proof state:
case refine_1.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
a : o.toType
⊢ ∃ b ∈ ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding ⁻¹' range f, ¬b < a

Tactic:
have := typein_lt_self a

Result:
case refine_1.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
a : o.toType
this : (typein fun x1 x2 => x1 < x2).toRelEmbedding a < o
⊢ ∃ b ∈ ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding ⁻¹' range f, ¬b < a

Proof state:
case refine_2.intro.intro
o : Ordinal.{u}
S : Set o.toType
hS : Unbounded (fun x1 x2 => x1 < x2) S
hS' : #↑S = (type fun x1 x2 => x1 < x2).cof
f : ↑S → Ordinal.{u} := fun s => (typein LT.lt).toRelEmbedding ↑s
⊢ o.cof ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}

Tactic:
refine ⟨S, f, le_antisymm (lsub_le fun i => typein_lt_self (o := o) i)
  (le_of_forall_lt fun a ha => ?_), by rwa [type_toType o] at hS'⟩

Result:
case refine_2.intro.intro
o : Ordinal.{u}
S : Set o.toType
hS : Unbounded (fun x1 x2 => x1 < x2) S
hS' : #↑S = (type fun x1 x2 => x1 < x2).cof
f : ↑S → Ordinal.{u} := fun s => (typein LT.lt).toRelEmbedding ↑s
a : Ordinal.{u}
ha : a < o
⊢ a < lsub f
-- Mathlib/Geometry/Manifold/WhitneyEmbedding.lean
theorem comp_embeddingPiTangent_mfderiv (x : M) (hx : x ∈ s) :
    ((ContinuousLinearMap.fst ℝ E ℝ).comp
            (@ContinuousLinearMap.proj ℝ _ ι (fun _ => E × ℝ) _ _ (fun _ => inferInstance)
              (f.ind x hx))).comp
        (mfderiv I 𝓘(ℝ, ι → E × ℝ) f.embeddingPiTangent x) =
      mfderiv I I (chartAt H (f.c (f.ind x hx))) x

Proof state:
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ ((ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))).comp
      (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) =
    mfderiv I I (↑(chartAt H (f.c (f.ind x hx)))) x

Tactic:
set L :=
  (ContinuousLinearMap.fst ℝ E ℝ).comp
    (@ContinuousLinearMap.proj ℝ _ ι (fun _ => E × ℝ) _ _ (fun _ => inferInstance) (f.ind x hx))

Result:
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
L : (ι → E × ℝ) →L[ℝ] E := (ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))
⊢ L.comp (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) = mfderiv I I (↑(chartAt H (f.c (f.ind x hx)))) x
-- Mathlib/Analysis/Convex/GaugeRescale.lean
theorem mapsTo_gaugeRescale_interior (h₀ : t ∈ 𝓝 0) (hc : Convex ℝ t) :
    MapsTo (gaugeRescale s t) (interior s) (interior t) := fun x hx ↦ by
  rw [← gauge_lt_one_iff_mem_interior] <;> try assumption
  exact (gauge_gaugeRescale_le _ _ _).trans_lt (interior_subset_gauge_lt_one _ hx)

Proof state:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s t : Set E
h₀ : t ∈ 𝓝 0
hc : Convex ℝ t
x : E
hx : x ∈ interior s
⊢ gauge t (gaugeRescale s t x) < 1

Tactic:
exact (gauge_gaugeRescale_le _ _ _).trans_lt (interior_subset_gauge_lt_one _ hx)

Result:
no goals

Proof state:
case hs₀
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s t : Set E
h₀ : t ∈ 𝓝 0
hc : Convex ℝ t
x : E
hx : x ∈ interior s
⊢ t ∈ 𝓝 0

Tactic:
assumption

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s t : Set E
h₀ : t ∈ 𝓝 0
hc : Convex ℝ t
x : E
hx : x ∈ interior s
⊢ gaugeRescale s t x ∈ interior t

Tactic:
rw [← gauge_lt_one_iff_mem_interior] <;> try assumption

Result:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s t : Set E
h₀ : t ∈ 𝓝 0
hc : Convex ℝ t
x : E
hx : x ∈ interior s
⊢ gauge t (gaugeRescale s t x) < 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem mul_distrib_left (xs ys zs : IntList) : (xs + ys) * zs = xs * zs + ys * zs

Proof state:
case cons.cons.nil
x : Int
xs : List Int
ih₁ : ∀ (ys zs : IntList), (xs + ys) * zs = xs * zs + ys * zs
head✝ : Int
tail✝ : List Int
⊢ (x :: xs + head✝ :: tail✝) * [] = (x :: xs) * [] + (head✝ :: tail✝) * []

Tactic:
simp

Result:
no goals

Proof state:
case nil
ys zs : IntList
⊢ ([] + ys) * zs = [] * zs + ys * zs

Tactic:
cases ys with
| nil => simp
| cons _ _ =>
  cases zs with
  | nil => simp
  | cons _ _ => simp_all [Int.add_mul]

Result:
no goals

Proof state:
case cons.cons
x : Int
xs : List Int
ih₁ : ∀ (ys zs : IntList), (xs + ys) * zs = xs * zs + ys * zs
zs : IntList
head✝ : Int
tail✝ : List Int
⊢ (x :: xs + head✝ :: tail✝) * zs = (x :: xs) * zs + (head✝ :: tail✝) * zs

Tactic:
cases zs with
| nil => simp
| cons _ _ => simp_all [Int.add_mul]

Result:
no goals

Proof state:
case nil.cons.cons
head✝¹ : Int
tail✝¹ : List Int
head✝ : Int
tail✝ : List Int
⊢ ([] + head✝¹ :: tail✝¹) * (head✝ :: tail✝) = [] * (head✝ :: tail✝) + (head✝¹ :: tail✝¹) * (head✝ :: tail✝)

Tactic:
simp_all [Int.add_mul]

Result:
no goals

Proof state:
case cons.cons.cons
x : Int
xs : List Int
ih₁ : ∀ (ys zs : IntList), (xs + ys) * zs = xs * zs + ys * zs
head✝¹ : Int
tail✝¹ : List Int
head✝ : Int
tail✝ : List Int
⊢ (x :: xs + head✝¹ :: tail✝¹) * (head✝ :: tail✝) = (x :: xs) * (head✝ :: tail✝) + (head✝¹ :: tail✝¹) * (head✝ :: tail✝)

Tactic:
simp_all [Int.add_mul]

Result:
no goals

Proof state:
case nil.cons.nil
head✝ : Int
tail✝ : List Int
⊢ ([] + head✝ :: tail✝) * [] = [] * [] + (head✝ :: tail✝) * []

Tactic:
simp

Result:
no goals

Proof state:
case cons.nil
x : Int
xs : List Int
ih₁ : ∀ (ys zs : IntList), (xs + ys) * zs = xs * zs + ys * zs
zs : IntList
⊢ (x :: xs + []) * zs = (x :: xs) * zs + [] * zs

Tactic:
simp_all

Result:
no goals

Proof state:
case nil.cons
zs : IntList
head✝ : Int
tail✝ : List Int
⊢ ([] + head✝ :: tail✝) * zs = [] * zs + (head✝ :: tail✝) * zs

Tactic:
cases zs with
| nil => simp
| cons _ _ => simp_all [Int.add_mul]

Result:
no goals

Proof state:
case nil.nil
zs : IntList
⊢ ([] + []) * zs = [] * zs + [] * zs

Tactic:
simp

Result:
no goals

Proof state:
case cons
x : Int
xs : List Int
ih₁ : ∀ (ys zs : IntList), (xs + ys) * zs = xs * zs + ys * zs
ys zs : IntList
⊢ (x :: xs + ys) * zs = (x :: xs) * zs + ys * zs

Tactic:
cases ys with
| nil => simp_all
| cons _ _ =>
  cases zs with
  | nil => simp
  | cons _ _ => simp_all [Int.add_mul]

Result:
no goals

Proof state:
xs ys zs : IntList
⊢ (xs + ys) * zs = xs * zs + ys * zs

Tactic:
induction xs generalizing ys zs with
| nil =>
  cases ys with
  | nil => simp
  | cons _ _ =>
    cases zs with
    | nil => simp
    | cons _ _ => simp_all [Int.add_mul]
| cons x xs ih₁ =>
  cases ys with
  | nil => simp_all
  | cons _ _ =>
    cases zs with
    | nil => simp
    | cons _ _ => simp_all [Int.add_mul]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean
lemma quasiIso_extendMap_iff [∀ j, K.HasHomology j] [∀ j, L.HasHomology j] :
    QuasiIso (extendMap φ e) ↔ QuasiIso φ

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
inst✝¹ : ∀ (j : ι), K.HasHomology j
inst✝ : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (extendMap φ e) (e.f i)
j' : ι'
hj' : ¬∃ j, e.f j = j'
⊢ QuasiIsoAt (extendMap φ e) j'

Tactic:
rw [quasiIsoAt_iff_exactAt]

Result:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
inst✝¹ : ∀ (j : ι), K.HasHomology j
inst✝ : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (extendMap φ e) (e.f i)
j' : ι'
hj' : ¬∃ j, e.f j = j'
⊢ (L.extend e).ExactAt j'

case neg.hK
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
inst✝¹ : ∀ (j : ι), K.HasHomology j
inst✝ : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (extendMap φ e) (e.f i)
j' : ι'
hj' : ¬∃ j, e.f j = j'
⊢ (K.extend e).ExactAt j'
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem exists_ae_eq_range_subset (H : AEMeasurable f μ) {t : Set β} (ht : ∀ᵐ x ∂μ, f x ∈ t)
    (h₀ : t.Nonempty) : ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᵐ[μ] g

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x => h₀.some) (mk f H)
⊢ {x | f x = mk f H x ∧ f x ∈ t} ∈ ae μ

Tactic:
exact H.ae_eq_mk.and ht

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem hasProd_one_iff_of_one_le (hf : ∀ i, 1 ≤ f i) : HasProd f 1 ↔ f = 1

Proof state:
case refine_1.h
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : ∀ (i : ι), 1 ≤ f i
hf' : HasProd f 1
i : ι
⊢ f i = 1 i

Tactic:
exact (hf i).antisymm' (le_hasProd hf' _ fun j _ ↦ hf j)

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : ∀ (i : ι), 1 ≤ f i
⊢ HasProd f 1 ↔ f = 1

Tactic:
refine ⟨fun hf' ↦ ?_, ?_⟩

Result:
case refine_1
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : ∀ (i : ι), 1 ≤ f i
hf' : HasProd f 1
⊢ f = 1

case refine_2
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : ∀ (i : ι), 1 ≤ f i
⊢ f = 1 → HasProd f 1

Proof state:
case refine_1
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : ∀ (i : ι), 1 ≤ f i
hf' : HasProd f 1
⊢ f = 1

Tactic:
ext i

Result:
case refine_1.h
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : ∀ (i : ι), 1 ≤ f i
hf' : HasProd f 1
i : ι
⊢ f i = 1 i

Proof state:
case refine_2
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : ∀ (i : ι), 1 ≤ f i
⊢ f = 1 → HasProd f 1

Tactic:
rintro rfl

Result:
case refine_2
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
hf : ∀ (i : ι), 1 ≤ 1 i
⊢ HasProd 1 1

Proof state:
case refine_2
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
hf : ∀ (i : ι), 1 ≤ 1 i
⊢ HasProd 1 1

Tactic:
exact hasProd_one

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem ker_zero : ker (0 : M →ₛₗ[τ₁₂] M₂) = ⊤ :=
  eq_top_iff'.2 fun x => by simp

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x : M
⊢ x ∈ ker 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Perfection.lean
theorem valAux_eq {f : PreTilt O p} {n : ℕ} (hfn : coeff _ _ n f ≠ 0) :
    valAux K v O p f = ModP.preVal K v O p (coeff _ _ n f) ^ p ^ n

Proof state:
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff (ModP O p) p n) f ≠ 0
k : ℕ
ih :
  (coeff (ModP O p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (ModP O p) p (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (ModP O p) p (Nat.find h + k + 1)) f
h1 : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
⊢ (coeff (ModP O p) p (Nat.find h + k)) f ≠ 0

Tactic:
exact coeff_nat_find_add_ne_zero k

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Types.lean
theorem Presheaf.isSheaf_yoneda' {α : Type u} :
    Presheaf.IsSheaf typesGrothendieckTopology (yoneda.obj α)

Proof state:
α : Type u
⊢ IsSheaf typesGrothendieckTopology (yoneda.obj α)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Result:
α : Type u
⊢ Presieve.IsSheaf typesGrothendieckTopology (yoneda.obj α)

Proof state:
α : Type u
⊢ Presieve.IsSheaf typesGrothendieckTopology (yoneda.obj α)

Tactic:
exact Presieve.isSheaf_yoneda'

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem adjoint_inner_left (A : E →ₗ[𝕜] F) (x : E) (y : F) : ⟪adjoint A y, x⟫ = ⟪y, A x⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this✝ : CompleteSpace E
this : CompleteSpace F
⊢ ⟪↑(ContinuousLinearMap.adjoint (toContinuousLinearMap ↑(toContinuousLinearMap A))) y, x⟫_𝕜 =
    ⟪y, ↑(toContinuousLinearMap A) x⟫_𝕜

Tactic:
exact ContinuousLinearMap.adjoint_inner_left _ x y

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this✝ : CompleteSpace E
this : CompleteSpace F
⊢ ⟪(adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜

Tactic:
rw [← coe_toContinuousLinearMap A, adjoint_eq_toCLM_adjoint]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this✝ : CompleteSpace E
this : CompleteSpace F
⊢ ⟪↑(ContinuousLinearMap.adjoint (toContinuousLinearMap ↑(toContinuousLinearMap A))) y, x⟫_𝕜 =
    ⟪y, ↑(toContinuousLinearMap A) x⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this : CompleteSpace E
⊢ ⟪(adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜

Tactic:
haveI := FiniteDimensional.complete 𝕜 F

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this✝ : CompleteSpace E
this : CompleteSpace F
⊢ ⟪(adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
⊢ ⟪(adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜

Tactic:
haveI := FiniteDimensional.complete 𝕜 E

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this : CompleteSpace E
⊢ ⟪(adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜
-- Mathlib/RingTheory/Radical.lean
theorem divRadical_ne_zero {a : E} (ha : a ≠ 0) : divRadical a ≠ 0

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
ha : a ≠ 0
⊢ divRadical a ≠ 0

Tactic:
rw [← radical_mul_divRadical a] at ha

Result:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
ha : radical a * divRadical a ≠ 0
⊢ divRadical a ≠ 0

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
ha : radical a * divRadical a ≠ 0
⊢ divRadical a ≠ 0

Tactic:
exact right_ne_zero_of_mul ha

Result:
no goals