harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/Single.lean
@[simp]
lemma mkHomFromSingle_f {K : HomologicalComplex V c} {j : ι} {A : V} (φ : A ⟶ K.X j)
    (hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0) :
    (mkHomFromSingle φ hφ).f j = (singleObjXSelf c j A).hom ≫ φ

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
⊢ (singleObjXIsoOfEq c j A j ⋯).hom ≫ φ = (singleObjXSelf c j A).hom ≫ φ

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
⊢ (if hi : j = j then (singleObjXIsoOfEq c j A j hi).hom ≫ φ ≫ 𝟙 (K.X j) else 0) = (singleObjXSelf c j A).hom ≫ φ

Tactic:
rw [dif_pos rfl, comp_id]

Result:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
⊢ (singleObjXIsoOfEq c j A j ⋯).hom ≫ φ = (singleObjXSelf c j A).hom ≫ φ

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
⊢ (mkHomFromSingle φ hφ).f j = (singleObjXSelf c j A).hom ≫ φ

Tactic:
dsimp [mkHomFromSingle]

Result:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
⊢ (if hi : j = j then (singleObjXIsoOfEq c j A j hi).hom ≫ φ ≫ 𝟙 (K.X j) else 0) = (singleObjXSelf c j A).hom ≫ φ
-- Mathlib/FieldTheory/Relrank.lean
theorem lift_rank_comap (f : L →+* E) :
    lift.{v} (Module.rank (A.comap f) L) = lift.{w} (relrank A f.fieldRange)

Proof state:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A : Subfield E
f : L →+* E
⊢ lift.{v, w} (Module.rank (↥(comap f A)) L) = lift.{w, v} (A.relrank f.fieldRange)

Tactic:
simpa only [relrank_top_right, ← RingHom.fieldRange_eq_map] using lift_relrank_comap A f ⊤

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_mul_left_Ioc {a : α} (h : 0 < a) (b c : α) :
    (a * ·) '' Ioc b c = Ioc (a * b) (a * c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
h : 0 < a
b c : α
⊢ (fun x => a * x) '' Ioc b c = Ioc (a * b) (a * c)

Tactic:
convert image_mul_right_Ioc b c h using 1 <;> simp only [mul_comm _ a]

Result:
no goals
-- Mathlib/RingTheory/Generators.lean
@[simp]
lemma Hom.toAlgHom_id : Hom.toAlgHom (.id P) = AlgHom.id _ _

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
⊢ (Hom.id P).toAlgHom = AlgHom.id R P.Ring

Tactic:
ext1

Result:
case hf
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
i✝ : P.vars
⊢ (Hom.id P).toAlgHom (X i✝) = (AlgHom.id R P.Ring) (X i✝)

Proof state:
case hf
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
i✝ : P.vars
⊢ (Hom.id P).toAlgHom (X i✝) = (AlgHom.id R P.Ring) (X i✝)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Defs.lean
theorem isReduced_of_injective [MonoidWithZero R] [MonoidWithZero S] {F : Type*}
    [FunLike F R S] [MonoidWithZeroHomClass F R S]
    (f : F) (hf : Function.Injective f) [IsReduced S] :
    IsReduced R

Proof state:
case eq_zero
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Injective ⇑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ x = 0

Tactic:
apply hf

Result:
case eq_zero.a
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Injective ⇑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ f x = f 0

Proof state:
case eq_zero.a
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Injective ⇑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ f x = 0

Tactic:
exact (hx.map f).eq_zero

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Injective ⇑f
inst✝ : IsReduced S
⊢ IsReduced R

Tactic:
constructor

Result:
case eq_zero
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Injective ⇑f
inst✝ : IsReduced S
⊢ ∀ (x : R), IsNilpotent x → x = 0

Proof state:
case eq_zero
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Injective ⇑f
inst✝ : IsReduced S
⊢ ∀ (x : R), IsNilpotent x → x = 0

Tactic:
intro x hx

Result:
case eq_zero
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Injective ⇑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ x = 0

Proof state:
case eq_zero.a
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Injective ⇑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ f x = f 0

Tactic:
rw [map_zero]

Result:
case eq_zero.a
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Injective ⇑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ f x = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h) :
    (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
  getElem_ofFn_go _ _ _ (by simp) (by simp) nofun

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < (ofFn f).size
⊢ 0 = (mkEmpty n).size

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < (ofFn f).size
⊢ 0 ≤ n

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma image_coe_Ioi (x : ℝ) : Real.toEReal '' Ioi x = Ioo ↑x ⊤

Proof state:
x : ℝ
⊢ Real.toEReal '' Ioi x = Ioo ↑x ⊤

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Result:
x : ℝ
⊢ WithBot.some '' (WithTop.some '' Ioi x) = Ioo ↑x ⊤

Proof state:
x : ℝ
⊢ WithBot.some '' (WithTop.some '' Ioi x) = Ioo ↑x ⊤

Tactic:
rw [WithTop.image_coe_Ioi, WithBot.image_coe_Ioo]

Result:
x : ℝ
⊢ Ioo ↑↑x ↑⊤ = Ioo ↑x ⊤

Proof state:
x : ℝ
⊢ Ioo ↑↑x ↑⊤ = Ioo ↑x ⊤

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem tsum_mul_tsum_eq_tsum_sum_range (hf : Summable f) (hg : Summable g)
    (hfg : Summable fun x : ℕ × ℕ ↦ f x.1 * g x.2) :
    ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ k ∈ range (n + 1), f k * g (n - k)

Proof state:
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.1 * g x.2
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2

Tactic:
exact tsum_mul_tsum_eq_tsum_sum_antidiagonal hf hg hfg

Result:
no goals

Proof state:
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.1 * g x.2
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l ↦ f k * g l]

Result:
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.1 * g x.2
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem reverse_mkVector (n) (a : α) : reverse (mkVector n a) = mkVector n a

Proof state:
α : Type u_1
n : Nat
a : α
⊢ (mkVector n a).reverse.toArray = (mkVector n a).toArray

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
⊢ (mkVector n a).reverse = mkVector n a

Tactic:
rw [← toArray_inj]

Result:
α : Type u_1
n : Nat
a : α
⊢ (mkVector n a).reverse.toArray = (mkVector n a).toArray
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma inv_hom_apply {R S : CommRingCat} (e : R ≅ S) (r : R) : e.inv (e.hom r) = r

Proof state:
R S : CommRingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
simp

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem compl_sSup (S : Set (LowerSet α)) : (sSup S).compl = ⨆ s ∈ S, LowerSet.compl s :=
  UpperSet.ext <| by simp only [coe_compl, coe_sSup, compl_iUnion₂, UpperSet.coe_iSup₂]

Proof state:
α : Type u_1
inst✝ : LE α
S : Set (LowerSet α)
⊢ ↑(sSup S).compl = ↑(⨆ s ∈ S, s.compl)

Tactic:
simp only [coe_compl, coe_sSup, compl_iUnion₂, UpperSet.coe_iSup₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zip_unzip : ∀ l : List (α × β), zip (unzip l).1 (unzip l).2 = l
  | [] => rfl
  | (a, b) :: l => by simp only [unzip_cons, zip_cons_cons, zip_unzip l]

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
l : List (α × β)
⊢ ((a, b) :: l).unzip.fst.zip ((a, b) :: l).unzip.snd = (a, b) :: l

Tactic:
simp only [unzip_cons, zip_cons_cons, zip_unzip l]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β}
    (h : m.WF) {hc : k ∈ Const.modify m k f} :
    haveI h' : k ∈ m := mem_modify h |>.mp hc
    Const.get (Const.modify m k f) k hc = f (Const.get m k h')

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : β → β
h : m.WF
hc : k ∈ modify m k f
⊢ get (modify m k f) k hc = f (get m k ⋯)

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : β → β
h : m.WF
hc✝ : k ∈ modify m k f
hc : (modify m k f).contains k = true
⊢ get (modify m k f) k hc✝ = f (get m k ⋯)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : β → β
h : m.WF
hc✝ : k ∈ modify m k f
hc : (modify m k f).contains k = true
⊢ get (modify m k f) k hc✝ = f (get m k ⋯)

Tactic:
revert hc

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : β → β
h : m.WF
hc : k ∈ modify m k f
⊢ (modify m k f).contains k = true → get (modify m k f) k hc = f (get m k ⋯)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : β → β
h : m.WF
hc : k ∈ modify m k f
⊢ (modify m k f).contains k = true → get (modify m k f) k hc = f (get m k ⋯)

Tactic:
simp_to_raw using Raw₀.Const.get_modify_self

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Finite.lean
lemma _root_.AlgebraicGeometry.IsClosedImmersion.eq_isFinite_inf_mono :
    @IsClosedImmersion = (@IsFinite ⊓ monomorphisms Scheme : MorphismProperty _)

Proof state:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsClosedImmersion x✝ ↔ (@IsFinite ⊓ monomorphisms Scheme) x✝

Tactic:
exact IsClosedImmersion.iff_isFinite_and_mono _

Result:
no goals

Proof state:
⊢ @IsClosedImmersion = @IsFinite ⊓ monomorphisms Scheme

Tactic:
ext

Result:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsClosedImmersion x✝ ↔ (@IsFinite ⊓ monomorphisms Scheme) x✝
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pi_div_thirty_two : sin (π / 32) = √(2 - √(2 + √(2 + √2))) / 2

Proof state:
⊢ sin (π / 32) = sin (π / 2 ^ 5)

Tactic:
congr

Result:
case e_x.e_a

⊢ 32 = 2 ^ 5

Proof state:
⊢ sin (π / 2 ^ 5) = √(2 - √(2 + √(2 + √2))) / 2

Tactic:
simp

Result:
no goals

Proof state:
case e_x.e_a

⊢ 32 = 2 ^ 5

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ sin (π / 32) = √(2 - √(2 + √(2 + √2))) / 2

Tactic:
trans sin (π / 2 ^ 5)

Result:
⊢ sin (π / 32) = sin (π / 2 ^ 5)


⊢ sin (π / 2 ^ 5) = √(2 - √(2 + √(2 + √2))) / 2
-- Mathlib/Data/W/Cardinal.lean
theorem cardinalMk_le_of_le {κ : Cardinal.{u}} (hκ : (sum fun a : α => κ ^ #(β a)) ≤ κ) :
    #(WType β) ≤ κ := cardinalMk_le_of_le' <| by simp_rw [lift_id]; exact hκ

Proof state:
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ : (sum fun a => κ ^ #(β a)) ≤ κ
⊢ (sum fun a => κ ^ #(β a)) ≤ κ

Tactic:
exact hκ

Result:
no goals

Proof state:
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ : (sum fun a => κ ^ #(β a)) ≤ κ
⊢ (sum fun a => κ ^ lift.{u, u} #(β a)) ≤ κ

Tactic:
simp_rw [lift_id]

Result:
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ : (sum fun a => κ ^ #(β a)) ≤ κ
⊢ (sum fun a => κ ^ #(β a)) ≤ κ
-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
theorem contMDiff_of_subsingleton [Subsingleton M'] : ContMDiff I I' n f

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝ : Subsingleton M'
⊢ ContMDiff I I' n f

Tactic:
intro x

Result:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝ : Subsingleton M'
x : M
⊢ ContMDiffAt I I' n f x

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝ : Subsingleton M'
x : M
⊢ ContMDiffAt I I' n f x

Tactic:
rw [Subsingleton.elim f fun _ => (f x)]

Result:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝ : Subsingleton M'
x : M
⊢ ContMDiffAt I I' n (fun x_1 => f x) x

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝ : Subsingleton M'
x : M
⊢ ContMDiffAt I I' n (fun x_1 => f x) x

Tactic:
exact contMDiffAt_const

Result:
no goals
-- Mathlib/Analysis/Fourier/ZMod.lean
lemma invDFT_apply (Ψ : ZMod N → E) (k : ZMod N) :
    𝓕⁻ Ψ k = (N : ℂ)⁻¹ • ∑ j : ZMod N, stdAddChar (j * k) • Ψ j

Proof state:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Ψ : ZMod N → E
k : ZMod N
⊢ 𝓕.symm Ψ k = (↑N)⁻¹ • ∑ j : ZMod N, stdAddChar (j * k) • Ψ j

Tactic:
simp only [dft, LinearEquiv.coe_symm_mk, auxDFT, mul_neg, neg_neg]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem IsAcc.mono {o : Ordinal} {S T : Set Ordinal} (h : S ⊆ T) (ho : o.IsAcc S) :
    o.IsAcc T

Proof state:
o : Ordinal.{u_1}
S T : Set Ordinal.{u_1}
h : S ⊆ T
ho : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
⊢ o ≠ 0 ∧ ∀ p < o, (T ∩ Ioo p o).Nonempty

Tactic:
exact ⟨ho.1, fun p plto ↦ (ho.2 p plto).casesOn fun s hs ↦ ⟨s, h hs.1, hs.2⟩⟩

Result:
no goals

Proof state:
o : Ordinal.{u_1}
S T : Set Ordinal.{u_1}
h : S ⊆ T
ho : o.IsAcc S
⊢ o.IsAcc T

Tactic:
rw [isAcc_iff] at *

Result:
o : Ordinal.{u_1}
S T : Set Ordinal.{u_1}
h : S ⊆ T
ho : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
⊢ o ≠ 0 ∧ ∀ p < o, (T ∩ Ioo p o).Nonempty
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem X_ne_zero [Nontrivial R] (s : σ) :
    X (R := R) s ≠ 0

Proof state:
case h
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ coeff (Finsupp.single s 1) (X s) ≠ 0

Tactic:
simp only [coeff_X, ne_eq, one_ne_zero, not_false_eq_true]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ ∃ d, coeff d (X s) ≠ 0

Tactic:
use Finsupp.single s 1

Result:
case h
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ coeff (Finsupp.single s 1) (X s) ≠ 0

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ X s ≠ 0

Tactic:
rw [ne_zero_iff]

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ ∃ d, coeff d (X s) ≠ 0
-- Mathlib/Topology/OmegaCompletePartialOrder.lean
theorem continuous_of_scottContinuous {α β} [OmegaCompletePartialOrder α]
    [OmegaCompletePartialOrder β] (f : Scott α → Scott β)
    (hf : ωScottContinuous f) : Continuous f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ωScottContinuous f
⊢ ∀ (s : Set (Scott β)), IsOpen s → IsOpen (f ⁻¹' s)

Tactic:
intro s hs

Result:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ωScottContinuous f
s : Set (Scott β)
hs : IsOpen s
⊢ IsOpen (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ωScottContinuous f
s : Set (Scott β)
hs : IsOpen s
⊢ ωScottContinuous fun x => x ∈ f ⁻¹' s

Tactic:
simp_rw [mem_preimage, mem_def, ← Function.comp_def]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ωScottContinuous f
s : Set (Scott β)
hs : IsOpen s
⊢ ωScottContinuous (s ∘ f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ωScottContinuous f
s : Set (Scott β)
hs : IsOpen s
⊢ ωScottContinuous (s ∘ f)

Tactic:
apply ωScottContinuous.comp hs hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ωScottContinuous f
s : Set (Scott β)
hs : IsOpen s
⊢ IsOpen (f ⁻¹' s)

Tactic:
dsimp only [IsOpen, TopologicalSpace.IsOpen, Scott.IsOpen]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ωScottContinuous f
s : Set (Scott β)
hs : IsOpen s
⊢ ωScottContinuous fun x => x ∈ f ⁻¹' s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ωScottContinuous f
⊢ Continuous f

Tactic:
rw [continuous_def]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ωScottContinuous f
⊢ ∀ (s : Set (Scott β)), IsOpen s → IsOpen (f ⁻¹' s)
-- Mathlib/Algebra/Ring/Hom/Defs.lean
theorem codomain_trivial_iff_range_trivial : (0 : β) = 1 ↔ ∀ x, f x = 0 :=
  f.codomain_trivial_iff_map_one_eq_zero.trans
    ⟨fun h x => by rw [← mul_one x, map_mul, h, mul_zero], fun h => h 1⟩

Proof state:
α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
h : f 1 = 0
x : α
⊢ f x = 0

Tactic:
rw [← mul_one x, map_mul, h, mul_zero]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
lemma pmap_map {P : α → Prop} {Q : β → Prop} (f : ∀ a, P a → β) (g : β → γ)
    (z : Sym2 α) (h : ∀ a ∈ z, P a) (h' : ∀ b ∈ z.pmap f h, Q b) :
    (z.pmap f h).map g = z.pmap (fun a ha => g (f a (h a ha))) (fun _ ha ↦ ha)

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : β → γ
x y : α
h : ∀ a ∈ s(x, y), P a
h' : ∀ b ∈ pmap f s(x, y) h, Q b
⊢ map g (pmap f s(x, y) h) = pmap (fun a ha => g (f a ⋯)) s(x, y) ⋯

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : β → γ
z : Sym2 α
h : ∀ a ∈ z, P a
h' : ∀ b ∈ pmap f z h, Q b
⊢ map g (pmap f z h) = pmap (fun a ha => g (f a ⋯)) z ⋯

Tactic:
induction' z with x y

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : β → γ
x y : α
h : ∀ a ∈ s(x, y), P a
h' : ∀ b ∈ pmap f s(x, y) h, Q b
⊢ map g (pmap f s(x, y) h) = pmap (fun a ha => g (f a ⋯)) s(x, y) ⋯