harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/OfAssociative.lean
theorem toLieHom_injective {f g : A →ₐ[R] B} (h : (f : A →ₗ⁅R⁆ B) = (g : A →ₗ⁅R⁆ B)) : f = g

Proof state:
A : Type v
inst✝⁴ : Ring A
R : Type u
inst✝³ : CommRing R
inst✝² : Algebra R A
B : Type w
inst✝¹ : Ring B
inst✝ : Algebra R B
f g : A →ₐ[R] B
h : f.toLieHom = g.toLieHom
⊢ f = g

Tactic:
ext a

Result:
case H
A : Type v
inst✝⁴ : Ring A
R : Type u
inst✝³ : CommRing R
inst✝² : Algebra R A
B : Type w
inst✝¹ : Ring B
inst✝ : Algebra R B
f g : A →ₐ[R] B
h : f.toLieHom = g.toLieHom
a : A
⊢ f a = g a

Proof state:
case H
A : Type v
inst✝⁴ : Ring A
R : Type u
inst✝³ : CommRing R
inst✝² : Algebra R A
B : Type w
inst✝¹ : Ring B
inst✝ : Algebra R B
f g : A →ₐ[R] B
h : f.toLieHom = g.toLieHom
a : A
⊢ f a = g a

Tactic:
exact LieHom.congr_fun h a

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_inl_image {s : Set α} :
    MeasurableSet (Sum.inl '' s : Set (α ⊕ β)) ↔ MeasurableSet s

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
⊢ MeasurableSet (Sum.inl '' s) ↔ MeasurableSet s

Tactic:
simp [measurableSet_sum_iff, Sum.inl_injective.preimage_image]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean
lemma isomorphisms_eq_stalkwise :
    isomorphisms Scheme = (isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓
      stalkwise (fun f ↦ Function.Bijective f)

Proof state:
⊢ isomorphisms Scheme =
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f

Tactic:
rw [isomorphisms_eq_isOpenImmersion_inf_surjective, isOpenImmersion_eq_inf,
  surjective_eq_topologically, inf_right_comm]

Result:
⊢ (((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding) ⊓
        topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective) ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f) =
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f

Proof state:
case e_a

⊢ ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding) ⊓
      topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective) =
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop

Tactic:
ext X Y f

Result:
case e_a.h
X Y : Scheme
f : X ⟶ Y
⊢ ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding) ⊓
        topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective)
      f ↔
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop f

Proof state:
case e_a.h
X Y : Scheme
f : X ⟶ Y
⊢ ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding) ⊓
        topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective)
      f ↔
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop f

Tactic:
exact ⟨fun H ↦ inferInstanceAs (IsIso (TopCat.isoOfHomeo
  (H.1.1.toHomeomorph_of_surjective H.2)).hom), fun (_ : IsIso f.base) ↦
  let e := (TopCat.homeoOfIso <| asIso f.base); ⟨e.isOpenEmbedding, e.surjective⟩⟩

Result:
no goals

Proof state:
⊢ (((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding) ⊓
        topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective) ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f) =
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f

Tactic:
congr 1

Result:
case e_a

⊢ ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding) ⊓
      topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective) =
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop
-- Mathlib/FieldTheory/KummerExtension.lean
lemma IntermediateField.adjoin_root_eq_top_of_isSplittingField :
    K⟮α⟯ = ⊤

Proof state:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ ⊤.toSubalgebra = Algebra.adjoin K {α}

Tactic:
exact (Algebra.adjoin_root_eq_top_of_isSplittingField hζ H hα).symm

Result:
no goals

Proof state:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ K⟮α⟯ = ⊤

Tactic:
refine (IntermediateField.eq_adjoin_of_eq_algebra_adjoin _ _ _ ?_).symm

Result:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ ⊤.toSubalgebra = Algebra.adjoin K {α}
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_imp : (φ.imp ψ).Realize v xs ↔ φ.Realize v xs → ψ.Realize v xs

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs → ψ.Realize v xs

Tactic:
simp only [Realize]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getMsbD_mul (x y : BitVec w) (i : Nat) :
    (x * y).getMsbD i = (mulRec x y w).getMsbD i

Proof state:
w : Nat
x y : BitVec w
i : Nat
⊢ (x * y).getMsbD i = (x.mulRec y w).getMsbD i

Tactic:
simp only [mulRec_eq_mul_signExtend_setWidth]

Result:
w : Nat
x y : BitVec w
i : Nat
⊢ (x * y).getMsbD i = (x * setWidth w (setWidth (w + 1) y)).getMsbD i

Proof state:
w : Nat
x y : BitVec w
i : Nat
⊢ (x * y).getMsbD i = (x * setWidth w (setWidth (w + 1) y)).getMsbD i

Tactic:
rw [setWidth_setWidth_of_le]

Result:
w : Nat
x y : BitVec w
i : Nat
⊢ (x * y).getMsbD i = (x * setWidth w y).getMsbD i

case h
w : Nat
x y : BitVec w
i : Nat
⊢ w ≤ w + 1

Proof state:
w : Nat
x y : BitVec w
i : Nat
⊢ (x * y).getMsbD i = (x * setWidth w y).getMsbD i

Tactic:
simp

Result:
no goals

Proof state:
case h
w : Nat
x y : BitVec w
i : Nat
⊢ w ≤ w + 1

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Sites/CoverLifting.lean
theorem ran_isSheaf_of_isCocontinuous (ℱ : Sheaf J A) :
    Presheaf.IsSheaf K (G.op.ran.obj ℱ.val)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
A : Type w
inst✝² : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : G.IsCocontinuous J K
inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
ℱ : Sheaf J A
X : D
S : K.Cover X
⊢ Nonempty (IsLimit (S.multifork (G.op.ran.obj ℱ.val)))

Tactic:
exact ⟨RanIsSheafOfIsCocontinuous.isLimitMultifork ℱ.2
  (G.op.isPointwiseRightKanExtensionRanCounit ℱ.val) S⟩

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
A : Type w
inst✝² : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : G.IsCocontinuous J K
inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
ℱ : Sheaf J A
⊢ Presheaf.IsSheaf K (G.op.ran.obj ℱ.val)

Tactic:
rw [Presheaf.isSheaf_iff_multifork]

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
A : Type w
inst✝² : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : G.IsCocontinuous J K
inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
ℱ : Sheaf J A
⊢ ∀ (X : D) (S : K.Cover X), Nonempty (IsLimit (S.multifork (G.op.ran.obj ℱ.val)))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
A : Type w
inst✝² : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : G.IsCocontinuous J K
inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
ℱ : Sheaf J A
⊢ ∀ (X : D) (S : K.Cover X), Nonempty (IsLimit (S.multifork (G.op.ran.obj ℱ.val)))

Tactic:
intros X S

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
A : Type w
inst✝² : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : G.IsCocontinuous J K
inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
ℱ : Sheaf J A
X : D
S : K.Cover X
⊢ Nonempty (IsLimit (S.multifork (G.op.ran.obj ℱ.val)))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem Sublist.find?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) : (l₁.find? p).isSome → (l₂.find? p).isSome

Proof state:
case cons₂.h_1
α : Type u_1
p : α → Bool
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (find? p l₁✝).isSome = true → (find? p l₂✝).isSome = true
x✝ : Bool
heq✝ : p a = true
⊢ (some a).isSome = true → (some a).isSome = true

Tactic:
simp

Result:
no goals

Proof state:
case slnil
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ (find? p []).isSome = true → (find? p []).isSome = true

Tactic:
simp

Result:
no goals

Proof state:
case cons₂.h_2
α : Type u_1
p : α → Bool
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (find? p l₁✝).isSome = true → (find? p l₂✝).isSome = true
x✝ : Bool
heq✝ : p a = false
⊢ (find? p l₁✝).isSome = true → (find? p l₂✝).isSome = true

Tactic:
simpa using ih

Result:
no goals

Proof state:
case cons₂
α : Type u_1
p : α → Bool
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (find? p l₁✝).isSome = true → (find? p l₂✝).isSome = true
⊢ (find? p (a :: l₁✝)).isSome = true → (find? p (a :: l₂✝)).isSome = true

Tactic:
simp only [find?]

Result:
case cons₂
α : Type u_1
p : α → Bool
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (find? p l₁✝).isSome = true → (find? p l₂✝).isSome = true
⊢ (match p a with
        | true => some a
        | false => find? p l₁✝).isSome =
      true →
    (match p a with
        | true => some a
        | false => find? p l₂✝).isSome =
      true

Proof state:
case cons₂
α : Type u_1
p : α → Bool
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (find? p l₁✝).isSome = true → (find? p l₂✝).isSome = true
⊢ (match p a with
        | true => some a
        | false => find? p l₁✝).isSome =
      true →
    (match p a with
        | true => some a
        | false => find? p l₂✝).isSome =
      true

Tactic:
split

Result:
case cons₂.h_1
α : Type u_1
p : α → Bool
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (find? p l₁✝).isSome = true → (find? p l₂✝).isSome = true
x✝ : Bool
heq✝ : p a = true
⊢ (some a).isSome = true → (some a).isSome = true

case cons₂.h_2
α : Type u_1
p : α → Bool
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (find? p l₁✝).isSome = true → (find? p l₂✝).isSome = true
x✝ : Bool
heq✝ : p a = false
⊢ (find? p l₁✝).isSome = true → (find? p l₂✝).isSome = true
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem comp_assoc {V₄ : Type*} [SeminormedAddCommGroup V₄] (h : NormedAddGroupHom V₃ V₄)
    (g : NormedAddGroupHom V₂ V₃) (f : NormedAddGroupHom V₁ V₂) :
    (h.comp g).comp f = h.comp (g.comp f)

Proof state:
case H
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V₁
inst✝² : SeminormedAddCommGroup V₂
inst✝¹ : SeminormedAddCommGroup V₃
V₄ : Type u_5
inst✝ : SeminormedAddCommGroup V₄
h : NormedAddGroupHom V₃ V₄
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
x✝ : V₁
⊢ ((h.comp g).comp f) x✝ = (h.comp (g.comp f)) x✝

Tactic:
rfl

Result:
no goals

Proof state:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V₁
inst✝² : SeminormedAddCommGroup V₂
inst✝¹ : SeminormedAddCommGroup V₃
V₄ : Type u_5
inst✝ : SeminormedAddCommGroup V₄
h : NormedAddGroupHom V₃ V₄
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
ext

Result:
case H
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V₁
inst✝² : SeminormedAddCommGroup V₂
inst✝¹ : SeminormedAddCommGroup V₃
V₄ : Type u_5
inst✝ : SeminormedAddCommGroup V₄
h : NormedAddGroupHom V₃ V₄
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
x✝ : V₁
⊢ ((h.comp g).comp f) x✝ = (h.comp (g.comp f)) x✝
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma toAffine_neg {P : Fin 3 → F} (hP : W.Nonsingular P) :
    toAffine W (W.neg P) = -toAffine W P

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
rw [neg_of_Z_eq_zero hP hPz,
  toAffine_smul _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg,
  toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_zero]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
by_cases hPz : P z = 0

Result:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
rw [neg_of_Z_ne_zero hPz, toAffine_smul _ <| Ne.isUnit hPz, toAffine_some <|
    (nonsingular_smul _ <| Ne.isUnit hPz).mp <| neg_of_Z_ne_zero hPz ▸ nonsingular_neg hP,
  toAffine_of_Z_ne_zero hP hPz, Affine.Point.neg_some]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem not_isPredPrelimit [NoMaxOrder α] : ¬ IsPredPrelimit a

Proof state:
α : Type u_1
a : α
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
inst✝ : NoMaxOrder α
⊢ ¬IsPredPrelimit a

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
lemma map_rootsOfUnity {S F} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S]
    {ζ : R} {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n) {f : F} (hf : Function.Injective f) :
    (rootsOfUnity n R).map (Units.map f) = rootsOfUnity n S

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
S : Type u_7
F : Type u_8
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
ζ : R
n : ℕ
inst✝ : NeZero n
hζ✝ : IsPrimitiveRoot ζ n
f : F
hf : Function.Injective ⇑f
this : CommMonoid Sˣ := inferInstance
hζ : IsPrimitiveRoot ⋯.unit n
⊢ Subgroup.map (Units.map ↑f) (rootsOfUnity n R) = rootsOfUnity n S

Tactic:
rw [← hζ.zpowers_eq,
  ← (hζ.map_of_injective (Units.map_injective (f := (f : R →* S)) hf)).zpowers_eq,
  MonoidHom.map_zpowers]

Result:
no goals

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
S : Type u_7
F : Type u_8
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
ζ : R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
f : F
hf : Function.Injective ⇑f
⊢ Subgroup.map (Units.map ↑f) (rootsOfUnity n R) = rootsOfUnity n S

Tactic:
letI : CommMonoid Sˣ := inferInstance

Result:
R : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
S : Type u_7
F : Type u_8
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
ζ : R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
f : F
hf : Function.Injective ⇑f
this : CommMonoid Sˣ := inferInstance
⊢ Subgroup.map (Units.map ↑f) (rootsOfUnity n R) = rootsOfUnity n S

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
S : Type u_7
F : Type u_8
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
ζ : R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
f : F
hf : Function.Injective ⇑f
this : CommMonoid Sˣ := inferInstance
⊢ Subgroup.map (Units.map ↑f) (rootsOfUnity n R) = rootsOfUnity n S

Tactic:
replace hζ := hζ.isUnit_unit <| NeZero.pos n

Result:
R : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
S : Type u_7
F : Type u_8
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
ζ : R
n : ℕ
inst✝ : NeZero n
hζ✝ : IsPrimitiveRoot ζ n
f : F
hf : Function.Injective ⇑f
this : CommMonoid Sˣ := inferInstance
hζ : IsPrimitiveRoot ⋯.unit n
⊢ Subgroup.map (Units.map ↑f) (rootsOfUnity n R) = rootsOfUnity n S
-- Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean
theorem iSup_genEigenspace_eq_top [IsAlgClosed K] [FiniteDimensional K V] (f : End K V) :
    ⨆ (μ : K) (k : ℕ), f.genEigenspace μ k = ⊤

Proof state:
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : IsAlgClosed K
inst✝ : FiniteDimensional K V
f : End K V
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤

Tactic:
apply iSup_maxGenEigenspace_eq_top

Result:
no goals

Proof state:
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : IsAlgClosed K
inst✝ : FiniteDimensional K V
f : End K V
⊢ ⨆ μ, ⨆ k, (f.genEigenspace μ) ↑k = ⊤

Tactic:
simp_rw [iSup_genEigenspace_eq]

Result:
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : IsAlgClosed K
inst✝ : FiniteDimensional K V
f : End K V
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤
-- Mathlib/Analysis/Normed/Group/Ultra.lean
theorem exists_norm_multiset_prod_le (s : Multiset ι) [Nonempty ι] {f : ι → M} :
    ∃ i : ι, (s ≠ 0 → i ∈ s) ∧ ‖(s.map f).prod‖ ≤ ‖f i‖

Proof state:
case cons
M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
inst✝ : Nonempty ι
f : ι → M
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
hM : ∃ i, (t ≠ 0 → i ∈ t) ∧ ‖(Multiset.map f t).prod‖ ≤ ‖f i‖
⊢ ∃ i, (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖

Tactic:
obtain ⟨M, hMs, hM⟩ := hM

Result:
case cons.intro.intro
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
⊢ ∃ i, (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖

Proof state:
M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
s : Multiset ι
inst✝ : Nonempty ι
f : ι → M
⊢ ∃ i, (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖f i‖

Tactic:
inhabit ι

Result:
M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
s : Multiset ι
inst✝ : Nonempty ι
f : ι → M
inhabited_h : Inhabited ι
⊢ ∃ i, (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖f i‖

Proof state:
case pos
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f M‖ ≤ ‖f a‖
⊢ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f a‖

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons]

Result:
case pos
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f M‖ ≤ ‖f a‖
⊢ ‖f a * (Multiset.map f t).prod‖ ≤ ‖f a‖

Proof state:
case empty
M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
inst✝ : Nonempty ι
f : ι → M
inhabited_h : Inhabited ι
⊢ ∃ i, (0 ≠ 0 → i ∈ 0) ∧ ‖(Multiset.map f 0).prod‖ ≤ ‖f i‖

Tactic:
simp

Result:
no goals

Proof state:
case neg
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ¬‖f M‖ ≤ ‖f a‖
⊢ ∃ i, (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖

Tactic:
rw [not_le] at hMa

Result:
case neg
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
⊢ ∃ i, (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem lift_injective_iff :
    Function.Injective (f.lift hg) ↔ ∀ x y, f.toMap x = f.toMap y ↔ g x = g y

Proof state:
case mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : ∀ (x y : M), f.toMap x = f.toMap y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
⊢ z = w

Tactic:
obtain ⟨_, _⟩ := f.surj z

Result:
case mpr.intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : ∀ (x y : M), f.toMap x = f.toMap y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
w✝ : M × ↥S
h✝ : z * f.toMap ↑w✝.2 = f.toMap w✝.1
⊢ z = w
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem reverse_attach (xs : List α) :
    xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩

Proof state:
α : Type u_1
xs : List α
⊢ pmap Subtype.mk xs.reverse ⋯ = pmap (fun a h => ⟨a, ⋯⟩) xs.reverse ⋯

Tactic:
apply pmap_congr_left

Result:
case h
α : Type u_1
xs : List α
⊢ ∀ (a : α), a ∈ xs.reverse → ∀ (h₁ : a ∈ xs) (h₂ : a ∈ xs.reverse), ⟨a, h₁⟩ = ⟨a, ⋯⟩

Proof state:
case h
α : Type u_1
xs : List α
a✝¹ : α
a✝ : a✝¹ ∈ xs.reverse
h₁✝ : a✝¹ ∈ xs
h₂✝ : a✝¹ ∈ xs.reverse
⊢ ⟨a✝¹, h₁✝⟩ = ⟨a✝¹, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
case h
α : Type u_1
xs : List α
⊢ ∀ (a : α), a ∈ xs.reverse → ∀ (h₁ : a ∈ xs) (h₂ : a ∈ xs.reverse), ⟨a, h₁⟩ = ⟨a, ⋯⟩

Tactic:
intros

Result:
case h
α : Type u_1
xs : List α
a✝¹ : α
a✝ : a✝¹ ∈ xs.reverse
h₁✝ : a✝¹ ∈ xs
h₂✝ : a✝¹ ∈ xs.reverse
⊢ ⟨a✝¹, h₁✝⟩ = ⟨a✝¹, ⋯⟩

Proof state:
α : Type u_1
xs : List α
⊢ xs.attach.reverse =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.reverse.attach

Tactic:
simp only [attach, attachWith, reverse_pmap, map_pmap]

Result:
α : Type u_1
xs : List α
⊢ pmap Subtype.mk xs.reverse ⋯ = pmap (fun a h => ⟨a, ⋯⟩) xs.reverse ⋯

Proof state:
α : Type ?u.79234
xs : List α
x✝ : { x // x ∈ xs.reverse }
x : α
h : x ∈ xs.reverse
⊢ x ∈ xs

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem comap_exp_nhdsGT_zero : comap exp (𝓝[>] 0) = atBot

Proof state:
⊢ comap rexp (𝓝[>] 0) = atBot

Tactic:
rw [← map_exp_atBot, comap_map exp_injective]

Result:
no goals
-- Mathlib/Order/Filter/Pointwise.lean
theorem top_mul_of_one_le (hf : 1 ≤ f) : ⊤ * f = ⊤

Proof state:
case intro.intro
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : univ * t ⊆ s
⊢ s = univ

Tactic:
rwa [univ_mul_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
⊢ ⊤ * f = ⊤

Tactic:
refine top_le_iff.1 fun s => ?_

Result:
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
⊢ s ∈ ⊤ * f → s ∈ ⊤

Proof state:
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
⊢ (∃ t₂ ∈ f, univ * t₂ ⊆ s) → s = univ

Tactic:
rintro ⟨t, ht, hs⟩

Result:
case intro.intro
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : univ * t ⊆ s
⊢ s = univ

Proof state:
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
⊢ s ∈ ⊤ * f → s ∈ ⊤

Tactic:
simp only [mem_mul, mem_top, exists_and_left, exists_eq_left]

Result:
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
⊢ (∃ t₂ ∈ f, univ * t₂ ⊆ s) → s = univ