harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/CharP/Algebra.lean
/-- If a ring homomorphism `R →+* A` is injective then `A` has the same exponential characteristic
as `R`. -/
lemma expChar_of_injective_ringHom {R A : Type*}
    [Semiring R] [Semiring A] {f : R →+* A} (h : Function.Injective f)
    (q : ℕ) [hR : ExpChar R q] : ExpChar A q

Proof state:
case zero
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring A
f : R →+* A
h : Function.Injective ⇑f
inst✝ : CharZero R
⊢ ExpChar A 1

Tactic:
haveI := charZero_of_injective_ringHom h

Result:
case zero
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring A
f : R →+* A
h : Function.Injective ⇑f
inst✝ : CharZero R
this : CharZero A
⊢ ExpChar A 1

Proof state:
case prime
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring A
f : R →+* A
h : Function.Injective ⇑f
q : ℕ
hprime : Nat.Prime q
hchar✝ : CharP R q
this : CharP A q
⊢ ExpChar A q

Tactic:
exact .prime hprime

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring A
f : R →+* A
h : Function.Injective ⇑f
q : ℕ
hR : ExpChar R q
⊢ ExpChar A q

Tactic:
rcases hR with _ | hprime

Result:
case zero
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring A
f : R →+* A
h : Function.Injective ⇑f
inst✝ : CharZero R
⊢ ExpChar A 1

case prime
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring A
f : R →+* A
h : Function.Injective ⇑f
q : ℕ
hprime : Nat.Prime q
hchar✝ : CharP R q
⊢ ExpChar A q

Proof state:
case prime
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring A
f : R →+* A
h : Function.Injective ⇑f
q : ℕ
hprime : Nat.Prime q
hchar✝ : CharP R q
⊢ ExpChar A q

Tactic:
haveI := charP_of_injective_ringHom h q

Result:
case prime
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring A
f : R →+* A
h : Function.Injective ⇑f
q : ℕ
hprime : Nat.Prime q
hchar✝ : CharP R q
this : CharP A q
⊢ ExpChar A q

Proof state:
case zero
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring A
f : R →+* A
h : Function.Injective ⇑f
inst✝ : CharZero R
this : CharZero A
⊢ ExpChar A 1

Tactic:
exact .zero

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem of_comp_surjective (hf : Surjective f) (hf' : Continuous f)
    (hfg : IsClosedMap (g ∘ f)) : IsClosedMap g

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Surjective f
hf' : Continuous f
hfg : IsClosedMap (g ∘ f)
K : Set Y
hK : IsClosed K
⊢ IsClosed (g '' K)

Tactic:
rw [← image_preimage_eq K hf, ← image_comp]

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Surjective f
hf' : Continuous f
hfg : IsClosedMap (g ∘ f)
K : Set Y
hK : IsClosed K
⊢ IsClosed (g ∘ f '' (f ⁻¹' K))

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Surjective f
hf' : Continuous f
hfg : IsClosedMap (g ∘ f)
⊢ IsClosedMap g

Tactic:
intro K hK

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Surjective f
hf' : Continuous f
hfg : IsClosedMap (g ∘ f)
K : Set Y
hK : IsClosed K
⊢ IsClosed (g '' K)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Surjective f
hf' : Continuous f
hfg : IsClosedMap (g ∘ f)
K : Set Y
hK : IsClosed K
⊢ IsClosed (g ∘ f '' (f ⁻¹' K))

Tactic:
exact hfg _ (hK.preimage hf')

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem inner_orthogonalProjection_eq_of_mem_left [HasOrthogonalProjection K] (u : K) (v : E) :
    ⟪u, orthogonalProjection K v⟫ = ⟪(u : E), v⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
u : ↥K
v : E
⊢ ⟪u, (orthogonalProjection K) v⟫_𝕜 = ⟪↑u, v⟫_𝕜

Tactic:
rw [← inner_conj_symm, ← inner_conj_symm (u : E), inner_orthogonalProjection_eq_of_mem_right]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
theorem _root_.Filter.EventuallyEq.lieBracket_vectorField
    (hV : V₁ =ᶠ[𝓝 x] V) (hW : W₁ =ᶠ[𝓝 x] W) : lieBracket 𝕜 V₁ W₁ =ᶠ[𝓝 x] lieBracket 𝕜 V W

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
⊢ lieBracket 𝕜 V₁ W₁ =ᶠ[𝓝 x] lieBracket 𝕜 V W

Tactic:
filter_upwards [hV.eventuallyEq_nhds, hW.eventuallyEq_nhds] with y hVy hWy

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
y : E
hVy : V₁ =ᶠ[𝓝 y] V
hWy : W₁ =ᶠ[𝓝 y] W
⊢ lieBracket 𝕜 V₁ W₁ y = lieBracket 𝕜 V W y

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
y : E
hVy : V₁ =ᶠ[𝓝 y] V
hWy : W₁ =ᶠ[𝓝 y] W
⊢ lieBracket 𝕜 V₁ W₁ y = lieBracket 𝕜 V W y

Tactic:
exact hVy.lieBracket_vectorField_eq hWy

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Strict.lean
theorem eqToHom_whiskerRight {a b c : B} {f g : a ⟶ b} (η : f = g) (h : b ⟶ c) :
    eqToHom η ▷ h = eqToHom (congr_arg₂ (· ≫ ·) η rfl)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
η : f = g
h : b ⟶ c
⊢ eqToHom η ▷ h = eqToHom ⋯

Tactic:
cases η

Result:
case refl
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
h : b ⟶ c
⊢ eqToHom ⋯ ▷ h = eqToHom ⋯

Proof state:
case refl
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
h : b ⟶ c
⊢ eqToHom ⋯ ▷ h = eqToHom ⋯

Tactic:
simp only [id_whiskerRight, eqToHom_refl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem containsThenInsertIfNew_snd (h : m.WF) {k : α} {v : β k} :
    (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝¹ : BEq α
inst✝ : Hashable α
h : m.WF
k : α
v : β k
⊢ (m.containsThenInsertIfNew k v).snd = m.insertIfNew k v

Tactic:
simp_to_raw using congrArg Subtype.val (Raw₀.containsThenInsertIfNew_snd _)

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma homologyι_comp_fromOpcycles :
    S.homologyι ≫ S.fromOpcycles = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ (S.rightHomologyIso.inv ≫ S.rightHomologyι) ≫ S.fromOpcycles = 0

Tactic:
simp only [assoc, rightHomologyι_comp_fromOpcycles, comp_zero]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.homologyι ≫ S.fromOpcycles = 0

Tactic:
dsimp only [homologyι]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ (S.rightHomologyIso.inv ≫ S.rightHomologyι) ≫ S.fromOpcycles = 0
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem formPerm_eq_self_of_not_mem (s : Cycle α) (h : Nodup s) (x : α) (hx : x ∉ s) :
    formPerm s h x = x

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∉ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α)) a✝) h) x = x

Tactic:
simpa using List.formPerm_eq_self_of_not_mem _ _ hx

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
h : s.Nodup
x : α
hx : x ∉ s
⊢ (s.formPerm h) x = x

Tactic:
induction s using Quot.inductionOn

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∉ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α)) a✝) h) x = x
-- Mathlib/CategoryTheory/Shift/Localization.lean
lemma shift {X Y : C} {f : X ⟶ Y} (hf : W f) (a : A) : W (f⟦a⟧')

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
hf : W f
a : A
⊢ W ((shiftFunctor C a).map f)

Tactic:
simpa only [IsCompatibleWithShift.iff W f a] using hf

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem convs'_of_int (a : ℤ) : (of (a : K)).convs' n = a

Proof state:
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
a : ℤ
n✝ : ℕ
a✝ : (of ↑a).convs' n✝ = ↑a
⊢ convs'Aux (of ↑a).s (n✝ + 1) = 0

Tactic:
exact convs'Aux_succ_none ((of_s_of_int K a).symm ▸ Stream'.Seq.get?_nil 0) _

Result:
no goals

Proof state:
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
a : ℤ
n✝ : ℕ
a✝ : (of ↑a).convs' n✝ = ↑a
⊢ (of ↑a).convs' (n✝ + 1) = ↑a

Tactic:
rw [convs', of_h_eq_floor, floor_intCast, add_right_eq_self]

Result:
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
a : ℤ
n✝ : ℕ
a✝ : (of ↑a).convs' n✝ = ↑a
⊢ convs'Aux (of ↑a).s (n✝ + 1) = 0

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
a : ℤ
⊢ (of ↑a).convs' n = ↑a

Tactic:
induction n with
| zero => simp only [zeroth_conv'_eq_h, of_h_eq_floor, floor_intCast]
| succ =>
  rw [convs', of_h_eq_floor, floor_intCast, add_right_eq_self]
  exact convs'Aux_succ_none ((of_s_of_int K a).symm ▸ Stream'.Seq.get?_nil 0) _

Result:
no goals

Proof state:
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
a : ℤ
⊢ (of ↑a).convs' 0 = ↑a

Tactic:
simp only [zeroth_conv'_eq_h, of_h_eq_floor, floor_intCast]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
lemma exp_cgf_of_neZero [hμ : NeZero μ] (hX : Integrable (fun ω ↦ exp (t * X ω)) μ) :
    exp (cgf X μ t) = mgf X μ t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
hX : Integrable (fun ω => rexp (t * X ω)) μ
⊢ rexp (cgf X μ t) = mgf X μ t

Tactic:
rw [cgf, exp_log (mgf_pos' hμ.out hX)]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_eq_self_iff {v : E} : (orthogonalProjection K v : E) = v ↔ v ∈ K

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
⊢ ↑((orthogonalProjection K) v) = v ↔ v ∈ K

Tactic:
refine ⟨fun h => ?_, fun h => eq_orthogonalProjection_of_mem_of_inner_eq_zero h ?_⟩

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
h : ↑((orthogonalProjection K) v) = v
⊢ v ∈ K

case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
h : v ∈ K
⊢ ∀ w ∈ K, ⟪v - v, w⟫_𝕜 = 0

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
h : ↑((orthogonalProjection K) v) = v
⊢ ↑((orthogonalProjection K) v) ∈ K

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
h : ↑((orthogonalProjection K) v) = v
⊢ v ∈ K

Tactic:
rw [← h]

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
h : ↑((orthogonalProjection K) v) = v
⊢ ↑((orthogonalProjection K) v) ∈ K

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
h : v ∈ K
⊢ ∀ w ∈ K, ⟪v - v, w⟫_𝕜 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_iff_isBoundedUnder_le_div (h : ∀ᶠ x in l, g'' x ≠ 0) :
    f =O[l] g'' ↔ IsBoundedUnder (· ≤ ·) l fun x => ‖f x‖ / ‖g'' x‖

Proof state:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
l : Filter α
h : ∀ᶠ (x : α) in l, g'' x ≠ 0
⊢ (∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g'' x‖) ↔ ∃ b, ∀ᶠ (a : α) in l, ‖f a‖ / ‖g'' a‖ ≤ b

Tactic:
exact
  exists_congr fun c =>
    eventually_congr <| h.mono fun x hx => (div_le_iff₀ <| norm_pos_iff.2 hx).symm

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
l : Filter α
h : ∀ᶠ (x : α) in l, g'' x ≠ 0
⊢ f =O[l] g'' ↔ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x‖ / ‖g'' x‖

Tactic:
simp only [isBigO_iff, IsBoundedUnder, IsBounded, eventually_map]

Result:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
l : Filter α
h : ∀ᶠ (x : α) in l, g'' x ≠ 0
⊢ (∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g'' x‖) ↔ ∃ b, ∀ᶠ (a : α) in l, ‖f a‖ / ‖g'' a‖ ≤ b
-- Mathlib/GroupTheory/QuotientGroup/Basic.lean
theorem rangeKerLift_surjective : Surjective (rangeKerLift φ)

Proof state:
case h
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ (rangeKerLift φ) ↑g = ⟨φ g, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mk.intro
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ ∃ a, (rangeKerLift φ) a = ⟨φ g, ⋯⟩

Tactic:
use mk g

Result:
case h
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ (rangeKerLift φ) ↑g = ⟨φ g, ⋯⟩

Proof state:
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Surjective ⇑(rangeKerLift φ)

Tactic:
rintro ⟨_, g, rfl⟩

Result:
case mk.intro
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ ∃ a, (rangeKerLift φ) a = ⟨φ g, ⋯⟩
-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
theorem esymm_to_weight [DecidableEq σ] (k : ℕ) : k * esymm σ R k =
    (-1) ^ k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ↑k * esymm σ R k =
    (-1) ^ k *
      ∑ t ∈ filter (fun t => #t.1 = k) (MvPolynomial.NewtonIdentities.pairs σ k),
        MvPolynomial.NewtonIdentities.weight σ R k t

Tactic:
rw [esymm, sum_filter_pairs_eq_sum_powersetCard_sum σ R k (fun t ↦ weight σ R k t),
  sum_congr rfl (esymm_summand_to_weight σ R k), mul_comm (k : MvPolynomial σ R) ((-1) ^ k),
  ← mul_sum, ← mul_assoc, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k, rfl⟩, one_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem X_mul_monomial (n : ℕ) (r : R) : X * monomial n r = monomial (n + 1) r

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ X * (monomial n) r = (monomial (n + 1)) r

Tactic:
rw [X_mul, monomial_mul_X]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_append_left [LawfulBEq α] {l₁ : List α} (l₂) (h : a ∈ l₁) :
    (l₁ ++ l₂).erase a = l₁.erase a ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l₁ l₂ : List α
h : a ∈ l₁
⊢ (l₁ ++ l₂).erase a = l₁.erase a ++ l₂

Tactic:
simp [erase_eq_eraseP]

Result:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l₁ l₂ : List α
h : a ∈ l₁
⊢ eraseP (fun x => a == x) (l₁ ++ l₂) = eraseP (fun x => a == x) l₁ ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l₁ l₂ : List α
h : a ∈ l₁
⊢ eraseP (fun x => a == x) (l₁ ++ l₂) = eraseP (fun x => a == x) l₁ ++ l₂

Tactic:
exact eraseP_append_left (beq_self_eq_true a) l₂ h

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
lemma _root_.MeasurableEmbedding.gaussianReal_comap_apply (hv : v ≠ 0)
    {f : ℝ → ℝ} (hf : MeasurableEmbedding f)
    {f' : ℝ → ℝ} (h_deriv : ∀ x, HasDerivAt f (f' x) x) {s : Set ℝ} (hs : MeasurableSet s) :
    (gaussianReal μ v).comap f s
      = ENNReal.ofReal (∫ x in s, |f' x| * gaussianPDFReal μ v (f x))

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ → ℝ
hf : MeasurableEmbedding f
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt f (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.comap f (ℙ.withDensity fun x => ENNReal.ofReal (gaussianPDFReal μ v x))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))

Tactic:
exact hf.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul' hs h_deriv
  (ae_of_all _ (gaussianPDFReal_nonneg _ _)) (integrable_gaussianPDFReal _ _)

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ → ℝ
hf : MeasurableEmbedding f
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt f (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.comap f (gaussianReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))

Tactic:
rw [gaussianReal_of_var_ne_zero _ hv, gaussianPDF_def]

Result:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ → ℝ
hf : MeasurableEmbedding f
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt f (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.comap f (ℙ.withDensity fun x => ENNReal.ofReal (gaussianPDFReal μ v x))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem Measurable.iSup_Prop {α} {mα : MeasurableSpace α} [ConditionallyCompleteLattice α]
    (p : Prop) {f : δ → α} (hf : Measurable f) : Measurable fun b => ⨆ _ : p, f b

Proof state:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable fun b => if h : p then f b else sSup ∅

Tactic:
split_ifs with h

Result:
case pos
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : p
⊢ Measurable fun b => f b

case neg
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ Measurable fun b => sSup ∅

Proof state:
case neg
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ Measurable fun b => sSup ∅

Tactic:
exact measurable_const

Result:
no goals

Proof state:
case pos
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : p
⊢ Measurable fun b => f b

Tactic:
exact hf

Result:
no goals

Proof state:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable fun b => ⨆ (_ : p), f b

Tactic:
simp_rw [ciSup_eq_ite]

Result:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable fun b => if h : p then f b else sSup ∅
-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π {j} {k} :
    (limitCurrySwapCompLimIsoLimitCurryCompLim G).inv ≫ limit.π _ k ≫ limit.π _ j =
      (limit.π _ j ≫ limit.π _ k : limit (_ ⋙ lim) ⟶ _)

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_5, u_1} J
inst✝⁴ : Category.{u_6, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitCurrySwapCompLimIsoLimitCurryCompLim G).inv ≫
      limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k

Tactic:
simp [limitCurrySwapCompLimIsoLimitCurryCompLim]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_self {n} {i : Fin (n + 1)} : X.δ (Fin.castSucc i) ≫ X.σ i = 𝟙 _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.castSucc ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
dsimp [δ, σ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.δ i.castSucc) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X ^⦋n⦌)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.δ i.castSucc) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X ^⦋n⦌)

Tactic:
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_self, X.map_id]

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.affinity (hs : StarConvex 𝕜 x s) (z : E) (c : 𝕜) :
    StarConvex 𝕜 (z + c • x) ((fun x => z + c • x) '' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedCommSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
c : 𝕜
⊢ StarConvex 𝕜 (z + c • x) ((fun x => z + c • x) '' s)

Tactic:
have h := (hs.smul c).add_left z

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedCommSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
c : 𝕜
h : StarConvex 𝕜 (z + c • x) ((fun x => z + x) '' (c • s))
⊢ StarConvex 𝕜 (z + c • x) ((fun x => z + c • x) '' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedCommSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
c : 𝕜
h : StarConvex 𝕜 (z + c • x) ((fun x => z + x) '' (c • s))
⊢ StarConvex 𝕜 (z + c • x) ((fun x => z + c • x) '' s)

Tactic:
rwa [← image_smul, image_image] at h

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem star_dotProduct : star v ⬝ᵥ w = star (star w ⬝ᵥ v)

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ star v ⬝ᵥ w = star (star w ⬝ᵥ v)

Tactic:
simp [dotProduct]

Result:
no goals
-- Mathlib/Data/Real/Pi/Irrational.lean
/--
Auxiliary for the proof that `π` is irrational.
The recursive formula for `I (n + 2) θ * θ ^ 2` in terms of `I n θ` and `I (n + 1) θ`.
-/
private lemma recursion (n : ℕ) :
    I (n + 2) θ * θ ^ 2 =
      2 * (n + 2) * (2 * n + 3) * I (n + 1) θ - 4 * (n + 2) * (n + 1) * I n θ

Proof state:
θ : ℝ
n : ℕ
⊢ I (n + 2) θ * θ ^ 2 = 2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ

Tactic:
rw [recursion' (n + 1)]

Result:
θ : ℝ
n : ℕ
⊢ -(2 * 2 * ((↑(n + 1) + 1) * (0 ^ (n + 1) * cos θ))) + 2 * (↑(n + 1) + 1) * (2 * ↑(n + 1) + 1) * I (n + 1) θ -
      4 * (↑(n + 1) + 1) * ↑(n + 1) * I (n + 1 - 1) θ =
    2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ

Proof state:
θ : ℝ
n : ℕ
⊢ 2 * (↑n + 1 + 1) * (2 * (↑n + 1) + 1) * I (n + 1) θ - 4 * (↑n + 1 + 1) * (↑n + 1) * I n θ =
    2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ

Tactic:
ring!

Result:
no goals

Proof state:
θ : ℝ
n : ℕ
⊢ -(2 * 2 * ((↑(n + 1) + 1) * (0 ^ (n + 1) * cos θ))) + 2 * (↑(n + 1) + 1) * (2 * ↑(n + 1) + 1) * I (n + 1) θ -
      4 * (↑(n + 1) + 1) * ↑(n + 1) * I (n + 1 - 1) θ =
    2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ

Tactic:
simp

Result:
θ : ℝ
n : ℕ
⊢ 2 * (↑n + 1 + 1) * (2 * (↑n + 1) + 1) * I (n + 1) θ - 4 * (↑n + 1 + 1) * (↑n + 1) * I n θ =
    2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ
-- Mathlib/Order/Defs/PartialOrder.lean
lemma le_of_eq (hab : a = b) : a ≤ b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a = b
⊢ a ≤ b

Tactic:
rw [hab]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_two_mul : cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2

Proof state:
x : ℝ
⊢ cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2

Tactic:
rw [← ofReal_inj]

Result:
x : ℝ
⊢ ↑(cosh (2 * x)) = ↑(cosh x ^ 2 + sinh x ^ 2)

Proof state:
x : ℝ
⊢ ↑(cosh (2 * x)) = ↑(cosh x ^ 2 + sinh x ^ 2)

Tactic:
simp [cosh_two_mul]

Result:
no goals