harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Extension.lean
@[simp]
lemma Hom.id_comp (f : Hom P P') : (Hom.id P').comp f = f

Proof state:
case toRingHom.a
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Extension R S
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
x✝ : P.Ring
⊢ ((Hom.id P').comp f).toRingHom x✝ = f.toRingHom x✝

Tactic:
simp [Hom.id, aeval_X_left]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Extension R S
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
⊢ (Hom.id P').comp f = f

Tactic:
ext

Result:
case toRingHom.a
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Extension R S
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
x✝ : P.Ring
⊢ ((Hom.id P').comp f).toRingHom x✝ = f.toRingHom x✝
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem comp (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) :
    MeasurableEmbedding (g ∘ f) :=
  ⟨hg.injective.comp hf.injective, hg.measurable.comp hf.measurable, fun s hs => by
    rwa [image_comp, hg.measurableSet_image, hf.measurableSet_image]⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (g ∘ f '' s)

Tactic:
rwa [image_comp, hg.measurableSet_image, hf.measurableSet_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_modify (m : Raw₀ α (fun _ => β)) (h : m.1.WF) {k : α} {f : β → β} :
    (Const.modify m k f).1.isEmpty = m.1.isEmpty

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

Tactic:
simp_to_model [Const.modify] using List.Const.isEmpty_modifyKey

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
@[simp]
lemma prodEquiv_symm_apply_fst (x : ToType X₁ × ToType X₂) :
    (Limits.prod.fst : X₁ ⨯ X₂ ⟶ X₁) ((prodEquiv X₁ X₂).symm x) = x.1

Proof state:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
y : ToType (X₁ ⨯ X₂)
⊢ (ConcreteCategory.hom prod.fst) ((prodEquiv X₁ X₂).symm ((prodEquiv X₁ X₂) y)) = ((prodEquiv X₁ X₂) y).1

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
x : ToType X₁ × ToType X₂
⊢ (ConcreteCategory.hom prod.fst) ((prodEquiv X₁ X₂).symm x) = x.1

Tactic:
obtain ⟨y, rfl⟩ := (prodEquiv X₁ X₂).surjective x

Result:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
y : ToType (X₁ ⨯ X₂)
⊢ (ConcreteCategory.hom prod.fst) ((prodEquiv X₁ X₂).symm ((prodEquiv X₁ X₂) y)) = ((prodEquiv X₁ X₂) y).1
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factors_of_factors_right {X Y Z : C} {P : Subobject Z} (f : X ⟶ Y) {g : Y ⟶ Z}
    (h : P.Factors g) : P.Factors (f ≫ g)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
P : MonoOver Z
g : Y ⟶ P.obj.left
⊢ (f ≫ g) ≫ P.arrow = f ≫ g ≫ P.arrow

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : P.Factors g
⊢ P.Factors (f ≫ g)

Tactic:
induction' P using Quotient.ind' with P

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : MonoOver Z
h : Factors (Quotient.mk'' P) g
⊢ Factors (Quotient.mk'' P) (f ≫ g)

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : MonoOver Z
h : Factors (Quotient.mk'' P) g
⊢ Factors (Quotient.mk'' P) (f ≫ g)

Tactic:
obtain ⟨g, rfl⟩ := h

Result:
case h.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
P : MonoOver Z
g : Y ⟶ P.obj.left
⊢ Factors (Quotient.mk'' P) (f ≫ g ≫ P.arrow)

Proof state:
case h.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
P : MonoOver Z
g : Y ⟶ P.obj.left
⊢ Factors (Quotient.mk'' P) (f ≫ g ≫ P.arrow)

Tactic:
exact ⟨f ≫ g, by simp⟩

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsOpen.div_left (ht : IsOpen t) : IsOpen (s / t)

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
ht : IsOpen t
⊢ IsOpen (s / t)

Tactic:
rw [← iUnion_div_left_image]

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
ht : IsOpen t
⊢ IsOpen (⋃ a ∈ s, (fun x => a / x) '' t)

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
ht : IsOpen t
⊢ IsOpen (⋃ a ∈ s, (fun x => a / x) '' t)

Tactic:
exact isOpen_biUnion fun a _ => isOpenMap_div_left a t ht

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem ext_of_eq_adjoin {S : Subalgebra R A} {s : Set A} (hS : S = adjoin R s) ⦃φ₁ φ₂ : S →ₐ[R] B⦄
    (h : ∀ x hx, φ₁ ⟨x, hS.ge (subset_adjoin hx)⟩ = φ₂ ⟨x, hS.ge (subset_adjoin hx)⟩) :
    φ₁ = φ₂

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
S : Subalgebra R A
s : Set A
hS : S = adjoin R s
φ₁ φ₂ : ↥S →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
⊢ φ₁ = φ₂

Tactic:
subst hS

Result:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
⊢ φ₁ = φ₂

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
⊢ φ₁ = φ₂

Tactic:
exact adjoin_ext h

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma mono_f (s : S.Splitting) : Mono S.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
this : IsSplitMono S.f
⊢ Mono S.f

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
⊢ Mono S.f

Tactic:
have := s.isSplitMono_f

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
this : IsSplitMono S.f
⊢ Mono S.f
-- Mathlib/NumberTheory/Dioph.lean
theorem reindex_dioph (f : α → β) : Dioph S → Dioph {v | v ∘ f ∈ S}
  | ⟨γ, p, pe⟩ => ⟨γ, p.map (inl ∘ f ⊗ inr), fun v =>
      (pe _).trans <|
        exists_congr fun t =>
          suffices v ∘ f ⊗ t = (v ⊗ t) ∘ (inl ∘ f ⊗ inr) by simp [this]
          funext fun s => by rcases s with a | b <;> rfl⟩

Proof state:
α β : Type u
S : Set (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : β → ℕ
t : γ → ℕ
this : v ∘ f ⊗ t = (v ⊗ t) ∘ (inl ∘ f ⊗ inr)
⊢ p (v ∘ f ⊗ t) = 0 ↔ (Poly.map (inl ∘ f ⊗ inr) p) (v ⊗ t) = 0

Tactic:
simp [this]

Result:
no goals

Proof state:
α β : Type u
S : Set (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : β → ℕ
t : γ → ℕ
s : α ⊕ γ
⊢ (v ∘ f ⊗ t) s = ((v ⊗ t) ∘ (inl ∘ f ⊗ inr)) s

Tactic:
rcases s with a | b <;> rfl

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
theorem monotone_dual_iff : Monotone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Monotone f

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ Monotone (⇑toDual ∘ f ∘ ⇑ofDual) ↔ Monotone f

Tactic:
rw [monotone_toDual_comp_iff, antitone_comp_ofDual_iff]

Result:
no goals
-- Mathlib/Algebra/Ring/Equiv.lean
theorem symm_toNonUnitalRingHom_comp_toNonUnitalRingHom (e : R ≃+* S) :
    e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id _

Proof state:
case a
R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
x✝ : R
⊢ (e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom) x✝ = (NonUnitalRingHom.id R) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
⊢ e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id R

Tactic:
ext

Result:
case a
R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
x✝ : R
⊢ (e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom) x✝ = (NonUnitalRingHom.id R) x✝
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem CG.range {N : Type*} [L.Structure N] (h : CG L M) (f : M →[L] N) : f.range.CG

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : CG L M
f : M →[L] N
⊢ (map f ⊤).CG

Tactic:
exact (cg_def.1 h).map f

Result:
no goals

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : CG L M
f : M →[L] N
⊢ f.range.CG

Tactic:
rw [Hom.range_eq_map]

Result:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : CG L M
f : M →[L] N
⊢ (map f ⊤).CG
-- Mathlib/NumberTheory/NumberField/Units/Basic.lean
theorem sum_mult_mul_log [NumberField K] (x : (𝓞 K)ˣ) :
    ∑ w : InfinitePlace K, w.mult * Real.log (w x) = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ ∑ w : InfinitePlace K, ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0

Tactic:
simpa [Units.norm, Real.log_prod, Real.log_pow] using
  congr_arg Real.log (prod_eq_abs_norm (x : K))

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem eq_ones_iff_le_length {c : Composition n} : c = ones n ↔ n ≤ c.length

Proof state:
n : ℕ
c : Composition n
⊢ c = ones n ↔ n ≤ c.length

Tactic:
simp [eq_ones_iff_length, le_antisymm_iff, c.length_le]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem clusterPt_iff_lift'_closure {F : Filter X} :
    ClusterPt x F ↔ pure x ≤ (F.lift' closure)

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
F : Filter X
⊢ ClusterPt x F ↔ pure x ≤ F.lift' closure

Tactic:
simp_rw [clusterPt_iff_forall_mem_closure,
  (hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure, id, singleton_subset_iff, true_and,
  exists_const]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem eventually_eventually_nhdsWithin {a : α} {s : Set α} {p : α → Prop} :
    (∀ᶠ y in 𝓝[s] a, ∀ᶠ x in 𝓝[s] y, p x) ↔ ∀ᶠ x in 𝓝[s] a, p x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x
⊢ ∀ᶠ (x : α) in 𝓝[s] a, p x

Tactic:
simp only [eventually_nhdsWithin_iff] at h ⊢

Result:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (x : α) in 𝓝 a, x ∈ s → ∀ᶠ (x : α) in 𝓝 x, x ∈ s → p x
⊢ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → p x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (x : α) in 𝓝 a, x ∈ s → ∀ᶠ (x : α) in 𝓝 x, x ∈ s → p x
⊢ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → p x

Tactic:
exact h.mono fun x hx hxs => (hx hxs).self_of_nhds hxs

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
⊢ (∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x

Tactic:
refine ⟨fun h => ?_, fun h => (eventually_nhds_nhdsWithin.2 h).filter_mono inf_le_left⟩

Result:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x
⊢ ∀ᶠ (x : α) in 𝓝[s] a, p x
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mulPosReflectLT_iff_contravariant_pos :
    MulPosReflectLT α ↔ ContravariantClass α>0 α (fun x y => y * x) (· < ·) :=
  ⟨@MulPosReflectLT.to_contravariantClass_pos_mul_lt _ _ _ _, fun h =>
    { elim a b c h

Proof state:
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y => y * ↑x) fun x1 x2 => x1 < x2
a : α≥0
b c : α
h : b * ↑a < c * ↑a
⊢ b < c

Tactic:
obtain ha | ha := a.prop.eq_or_lt

Result:
case inl
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y => y * ↑x) fun x1 x2 => x1 < x2
a : α≥0
b c : α
h : b * ↑a < c * ↑a
ha : 0 = ↑a
⊢ b < c

case inr
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y => y * ↑x) fun x1 x2 => x1 < x2
a : α≥0
b c : α
h : b * ↑a < c * ↑a
ha : 0 < ↑a
⊢ b < c

Proof state:
case inl
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y => y * ↑x) fun x1 x2 => x1 < x2
a : α≥0
b c : α
h : b * ↑a < c * ↑a
ha : 0 = ↑a
⊢ b < c

Tactic:
simp [← ha] at h

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem range_eq_iUnion {ι} (f : ι → α) : range f = ⋃ i, {f i} :=
  Set.ext fun a => by simp [@eq_comm α a]

Proof state:
α : Type u_1
ι : Sort u_12
f : ι → α
a : α
⊢ a ∈ range f ↔ a ∈ ⋃ i, {f i}

Tactic:
simp [@eq_comm α a]

Result:
no goals
-- Mathlib/Data/Erased.lean
theorem out_inj {α} (a b : Erased α) (h : a.out = b.out) : a = b

Proof state:
α : Sort u_1
a b : Erased α
h : a.out = b.out
⊢ a = b

Tactic:
simpa using congr_arg mk h

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
lemma rTensor.inverse_apply (y : N ⊗[R] Q) :
    (rTensor.inverse Q hfg hg) ((rTensor Q g) y) =
      Submodule.Quotient.mk (p := LinearMap.range (rTensor Q f)) y

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
y : N ⊗[R] Q
⊢ (inverse Q hfg hg) ((rTensor Q g) y) = Submodule.Quotient.mk y

Tactic:
rw [rTensor.inverse, rTensor.inverse_of_rightInverse_apply]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/FixedPoints.lean
theorem fixedBy_mul (m₁ m₂ : M) : fixedBy α m₁ ∩ fixedBy α m₂ ⊆ fixedBy α (m₁ * m₂)

Proof state:
α : Type u_1
M : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
m₁ m₂ : M
a : α
h₁ : a ∈ fixedBy α m₁
h₂ : a ∈ fixedBy α m₂
⊢ a ∈ fixedBy α (m₁ * m₂)

Tactic:
rw [mem_fixedBy, mul_smul, h₂, h₁]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
m₁ m₂ : M
⊢ fixedBy α m₁ ∩ fixedBy α m₂ ⊆ fixedBy α (m₁ * m₂)

Tactic:
intro a ⟨h₁, h₂⟩

Result:
α : Type u_1
M : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
m₁ m₂ : M
a : α
h₁ : a ∈ fixedBy α m₁
h₂ : a ∈ fixedBy α m₂
⊢ a ∈ fixedBy α (m₁ * m₂)
-- Mathlib/Topology/Order/Monotone.lean
theorem MonotoneOn.map_sSup_of_continuousWithinAt {f : α → β} {s : Set α}
    (Cf : ContinuousWithinAt f s (sSup s))
    (Mf : MonotoneOn f s) (fbot : f ⊥ = ⊥) : f (sSup s) = sSup (f '' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
⊢ f (sSup s) = sSup (f '' s)

Tactic:
rcases s.eq_empty_or_nonempty with h | h

Result:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
h : s = ∅
⊢ f (sSup s) = sSup (f '' s)

case inr
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
h : s.Nonempty
⊢ f (sSup s) = sSup (f '' s)

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
h : s.Nonempty
⊢ f (sSup s) = sSup (f '' s)

Tactic:
exact Mf.map_csSup_of_continuousWithinAt Cf h

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
h : s = ∅
⊢ f (sSup s) = sSup (f '' s)

Tactic:
simp [h, fbot]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
@[to_additive]
lemma toWord_mul_sublist (x y : FreeGroup α) : (x * y).toWord <+ x.toWord ++ y.toWord

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
this : x * y = mk (x.toWord ++ y.toWord)
⊢ Red (x.toWord ++ y.toWord) (mk (x.toWord ++ y.toWord)).toWord

Tactic:
exact FreeGroup.reduce.red

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ Red (x.toWord ++ y.toWord) (x * y).toWord

Tactic:
have : x * y = FreeGroup.mk (x.toWord ++ y.toWord) := by
  rw [← FreeGroup.mul_mk, FreeGroup.mk_toWord, FreeGroup.mk_toWord]

Result:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
this : x * y = mk (x.toWord ++ y.toWord)
⊢ Red (x.toWord ++ y.toWord) (x * y).toWord

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ x * y = mk (x.toWord ++ y.toWord)

Tactic:
rw [← FreeGroup.mul_mk, FreeGroup.mk_toWord, FreeGroup.mk_toWord]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ (x * y).toWord <+ x.toWord ++ y.toWord

Tactic:
refine Red.sublist ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ Red (x.toWord ++ y.toWord) (x * y).toWord

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
this : x * y = mk (x.toWord ++ y.toWord)
⊢ Red (x.toWord ++ y.toWord) (x * y).toWord

Tactic:
rw [this]

Result:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
this : x * y = mk (x.toWord ++ y.toWord)
⊢ Red (x.toWord ++ y.toWord) (mk (x.toWord ++ y.toWord)).toWord
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
lemma r_pos : 0 < r z

Proof state:
z : ℍ
⊢ 0 < r z

Tactic:
simp only [r, lt_min_iff, im_pos, Real.sqrt_pos, r1_pos, and_self]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
lemma dist_pi_lt_iff {f g : ∀ b, π b} {r : ℝ} (hr : 0 < r) :
    dist f g < r ↔ ∀ b, dist (f b) (g b) < r

Proof state:
case intro
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < ↑r
⊢ dist f g < ↑r ↔ ∀ (b : β), dist (f b) (g b) < ↑r

Tactic:
exact nndist_pi_lt_iff hr

Result:
no goals

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ
hr : 0 < r
⊢ dist f g < r ↔ ∀ (b : β), dist (f b) (g b) < r

Tactic:
lift r to ℝ≥0 using hr.le

Result:
case intro
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < ↑r
⊢ dist f g < ↑r ↔ ∀ (b : β), dist (f b) (g b) < ↑r
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.mul [Add α] [Mul β] [HasDistribNeg β] (hf : Antiperiodic f c)
    (hg : Antiperiodic g c) : Periodic (f * g) c

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
c : α
inst✝² : Add α
inst✝¹ : Mul β
inst✝ : HasDistribNeg β
hf : Antiperiodic f c
hg : Antiperiodic g c
⊢ Periodic (f * g) c

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_add (m₁ m₂ : M) (s : S) : mk' f (m₁ + m₂) s = mk' f m₁ s + mk' f m₂ s

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s : ↥S
⊢ mk' f (m₁ + m₂) s = mk' f m₁ s + mk' f m₂ s

Tactic:
rw [mk'_add_mk', ← smul_add, mk'_cancel_left]

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem tendsto (x : E) (hf : IsBoundedLinearMap 𝕜 f) : Tendsto f (𝓝 x) (𝓝 (f x)) :=
  let ⟨hf, M, _, hM⟩ := hf
  tendsto_iff_norm_sub_tendsto_zero.2 <|
    squeeze_zero (fun _ => norm_nonneg _)
      (fun e =>
        calc
          ‖f e - f x‖ = ‖hf.mk' f (e - x)‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
hf✝ : IsBoundedLinearMap 𝕜 f
hf : IsLinearMap 𝕜 f
M : ℝ
left✝ : 0 < M
hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
this : Tendsto (fun e => M * ‖e - x‖) (𝓝 x) (𝓝 (M * 0))
⊢ Tendsto (fun e => M * ‖e - x‖) (𝓝 x) (𝓝 0)

Tactic:
simpa

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
hf✝ : IsBoundedLinearMap 𝕜 f
hf : IsLinearMap 𝕜 f
M : ℝ
left✝ : 0 < M
hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
e : E
⊢ ‖f e - f x‖ = ‖(IsLinearMap.mk' f hf) (e - x)‖

Tactic:
rw [(hf.mk' _).map_sub e x]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
hf✝ : IsBoundedLinearMap 𝕜 f
hf : IsLinearMap 𝕜 f
M : ℝ
left✝ : 0 < M
hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
e : E
⊢ ‖f e - f x‖ = ‖(IsLinearMap.mk' f hf) e - (IsLinearMap.mk' f hf) x‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
hf✝ : IsBoundedLinearMap 𝕜 f
hf : IsLinearMap 𝕜 f
M : ℝ
left✝ : 0 < M
hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
e : E
⊢ ‖f e - f x‖ = ‖(IsLinearMap.mk' f hf) e - (IsLinearMap.mk' f hf) x‖

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
theorem incMatrix_apply_eq_one_iff : G.incMatrix R a e = 1 ↔ e ∈ G.incidenceSet a

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ incMatrix R G a e = 1 ↔ e ∈ G.incidenceSet a

Tactic:
convert one_ne_zero.ite_eq_left_iff

Result:
case convert_3
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ NeZero 1

Proof state:
case convert_3
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : MulZeroOneClass R
a : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ NeZero 1

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem Finsupp.sum_mul (b : S) (s : α →₀ R) {f : α → R → S} :
    s.sum f * b = s.sum fun a c => f a c * b

Proof state:
α : Type u_1
R : Type u_14
S : Type u_15
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
b : S
s : α →₀ R
f : α → R → S
⊢ s.sum f * b = s.sum fun a c => f a c * b

Tactic:
simp only [Finsupp.sum, Finset.sum_mul]

Result:
no goals