harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/ModelTheory/Substructures.lean
theorem subtype_substructureEquivMap (f : M ↪[L] N) (s : L.Substructure M) :
    (subtype _).comp (f.substructureEquivMap s).toEmbedding = f.comp (subtype _)

Proof state:
case h
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
x✝ : ↥s
⊢ ((Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding) x✝ = (f.comp s.subtype) x✝

Tactic:
rfl

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
⊢ (Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding = f.comp s.subtype

Tactic:
ext

Result:
case h
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
x✝ : ↥s
⊢ ((Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding) x✝ = (f.comp s.subtype) x✝
-- Mathlib/Tactic/Abel.lean
theorem term_add_const {α} [AddCommMonoid α] (n x a k a') (h : a + k = a') :
    @term α _ n x a + k = term n x a'

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
n : ℕ
x a k a' : α
h : a + k = a'
⊢ term n x a + k = term n x a'

Tactic:
simp [h.symm, term, add_assoc]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem subset_closedBall_norm_mul (a : A) : σ a ⊆ Metric.closedBall (0 : 𝕜) (‖a‖ * ‖(1 : A)‖) :=
  fun k hk => by simp [norm_le_norm_mul_of_mem hk]

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ σ a
⊢ k ∈ Metric.closedBall 0 (‖a‖ * ‖1‖)

Tactic:
simp [norm_le_norm_mul_of_mem hk]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem cycleRange_of_lt {n : ℕ} [NeZero n] {i j : Fin n} (h : j < i) : cycleRange i j = j + 1

Proof state:
n : ℕ
inst✝ : NeZero n
i j : Fin n
h : j < i
⊢ i.cycleRange j = j + 1

Tactic:
rw [cycleRange_of_le h.le, if_neg h.ne]

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
lemma wInner_sub_right (w : ι → ℝ) (f g₁ g₂ : ∀ i, E i) :
    ⟪f, g₁ - g₂⟫_[𝕜, w] = ⟪f, g₁⟫_[𝕜, w] - ⟪f, g₂⟫_[𝕜, w]

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f g₁ g₂ : (i : ι) → E i
⊢ wInner w f (g₁ - g₂) = wInner w f g₁ - wInner w f g₂

Tactic:
simp_rw [sub_eq_add_neg, wInner_add_right, wInner_neg_right]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive] lemma mabs_le_mabs_of_one_le (ha : 1 ≤ a) (hab : a ≤ b) : |a|ₘ ≤ |b|ₘ

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a b : α
inst✝ : MulLeftMono α
ha : 1 ≤ a
hab : a ≤ b
⊢ mabs a ≤ mabs b

Tactic:
rwa [mabs_of_one_le ha, mabs_of_one_le (ha.trans hab)]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
@[simp] lemma isNilpotent_C_iff :
    IsNilpotent (C r) ↔ IsNilpotent r :=
  exists_congr fun k ↦ by simpa only [← C_pow] using C_eq_zero

Proof state:
R : Type u_1
r : R
inst✝ : Semiring R
k : ℕ
⊢ C r ^ k = 0 ↔ r ^ k = 0

Tactic:
simpa only [← C_pow] using C_eq_zero

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem himp_idem : b ⇨ b ⇨ a = b ⇨ a

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ b ⇨ b ⇨ a = b ⇨ a

Tactic:
rw [himp_himp, inf_idem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_modify (h : m.1.WF) {k k' : α} {f : β k → β k} :
    (m.modify k f).contains k' = m.contains k'

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k k' : α
f : β k → β k
⊢ (m.modify k f).contains k' = m.contains k'

Tactic:
simp_to_model [modify] using List.containsKey_modifyKey

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem prod_ofNatList (l : List ℕ) (h) : ((ofNatList l h).prod : ℕ) = l.prod

Proof state:
l : List ℕ
h : ∀ p ∈ l, Nat.Prime p
⊢ ↑(ofNatList l h).prod = l.prod

Tactic:
have := prod_ofNatMultiset (l : Multiset ℕ) h

Result:
l : List ℕ
h : ∀ p ∈ l, Nat.Prime p
this : ↑(ofNatMultiset (↑l) h).prod = (↑l).prod
⊢ ↑(ofNatList l h).prod = l.prod

Proof state:
l : List ℕ
h : ∀ p ∈ l, Nat.Prime p
this : ↑(ofNatMultiset (↑l) h).prod = (↑l).prod
⊢ ↑(ofNatList l h).prod = l.prod

Tactic:
rw [Multiset.prod_coe] at this

Result:
l : List ℕ
h : ∀ p ∈ l, Nat.Prime p
this : ↑(ofNatMultiset (↑l) h).prod = l.prod
⊢ ↑(ofNatList l h).prod = l.prod

Proof state:
l : List ℕ
h : ∀ p ∈ l, Nat.Prime p
this : ↑(ofNatMultiset (↑l) h).prod = l.prod
⊢ ↑(ofNatList l h).prod = l.prod

Tactic:
exact this

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_eq_zero : ⌈a⌉₊ = 0 ↔ a ≤ 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ ⌈a⌉₊ = 0 ↔ a ≤ 0

Tactic:
rw [← Nat.le_zero, ceil_le, Nat.cast_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Basic.lean
theorem comp_left_eq_zero [IsIso f] : f ≫ g = 0 ↔ g = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : IsIso f
⊢ f ≫ g = 0 ↔ g = 0

Tactic:
rw [← IsIso.eq_inv_comp, Limits.comp_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem eq_add_of_sub_eq {a b c : Nat} (hle : b ≤ a) (h : a - b = c) : a = c + b

Proof state:
a b c : Nat
hle : b ≤ a
h : a - b = c
⊢ a = c + b

Tactic:
rw [h.symm, Nat.sub_add_cancel hle]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin)

Proof state:
n : Nat
x y : BitVec n
⊢ x * y = { toFin := x.toFin * y.toFin }

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_mul_div_comm : a / b * (c / d) = a * c / (b * d)

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b * (c / d) = a * c / (b * d)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_mul [Fintype n] [NonUnitalSemiring α] [StarRing α] (M : Matrix m n α)
    (N : Matrix n l α) : (M * N)ᴴ = Nᴴ * Mᴴ :=
  Matrix.ext <| by simp [mul_apply]

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : Fintype n
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
M : Matrix m n α
N : Matrix n l α
⊢ ∀ (i : l) (j : m), (M * N)ᴴ i j = (Nᴴ * Mᴴ) i j

Tactic:
simp [mul_apply]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformRing.lean
theorem inseparableSetoid_ring (α) [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] :
    inseparableSetoid α = Submodule.quotientRel (Ideal.closure ⊥) :=
  Setoid.ext fun x y =>
    addGroup_inseparable_iff.trans <| .trans (by rfl) (Submodule.quotientRel_def _).symm

Proof state:
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
x y : α
⊢ x - y ∈ closure 0 ↔ x - y ∈ ⊥.closure

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Dialectica/Monoidal.lean
theorem braiding_naturality_left {X Y : Dial C} (f : X ⟶ Y) (Z : Dial C) :
    tensorHom f (𝟙 Z) ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ tensorHom (𝟙 Z) f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
Z : Dial C
⊢ tensorHom f (𝟙 Z) ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ tensorHom (𝟙 Z) f

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem Tape.map_fst {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') :
    ∀ T : Tape Γ, (T.map f).1 = f T.1

Proof state:
case mk
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ (map f { head := head✝, left := left✝, right := right✝ }).head =
    f.f { head := head✝, left := left✝, right := right✝ }.head

Tactic:
rfl

Result:
no goals

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
⊢ ∀ (T : Tape Γ), (map f T).head = f.f T.head

Tactic:
rintro ⟨⟩

Result:
case mk
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ (map f { head := head✝, left := left✝, right := right✝ }).head =
    f.f { head := head✝, left := left✝, right := right✝ }.head
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem IntegrableOn.inter_of_restrict (h : IntegrableOn f s (μ.restrict t)) :
    IntegrableOn f (s ∩ t) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s t : Set α
μ : Measure α
h : IntegrableOn f s (μ.restrict t)
⊢ IntegrableOn f (s ∩ t) μ

Tactic:
have := h.mono_set (inter_subset_left (t := t))

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s t : Set α
μ : Measure α
h : IntegrableOn f s (μ.restrict t)
this : IntegrableOn f (s ∩ t) (μ.restrict t)
⊢ IntegrableOn f (s ∩ t) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s t : Set α
μ : Measure α
h : IntegrableOn f s (μ.restrict t)
this : IntegrableOn f (s ∩ t) (μ.restrict t)
⊢ IntegrableOn f (s ∩ t) μ

Tactic:
rwa [IntegrableOn, μ.restrict_restrict_of_subset inter_subset_right] at this

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNormEssSup_const_smul (c : 𝕜) (f : α → F) :
    eLpNormEssSup (c • f) μ = ‖c‖ₑ * eLpNormEssSup f μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
c : 𝕜
f : α → F
⊢ eLpNormEssSup (c • f) μ = ‖c‖ₑ * eLpNormEssSup f μ

Tactic:
simp_rw [eLpNormEssSup_eq_essSup_enorm, Pi.smul_apply, enorm_smul,
  ENNReal.essSup_const_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem finrank_eq_zero_of_basis_imp_false (h : ∀ s : Finset M, Basis.{v} (s : Set M) R M → False) :
    finrank R M = 0 :=
  finrank_eq_zero_of_basis_imp_not_finite fun s b hs =>
    h hs.toFinset
      (by
        convert b
        simp)

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Finset M), Basis (↑↑s) R M → False
s : Set M
b : Basis (↑s) R M
hs : s.Finite
⊢ Basis (↑↑hs.toFinset) R M

Tactic:
convert b

Result:
case h.e'_1.h.e'_2
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Finset M), Basis (↑↑s) R M → False
s : Set M
b : Basis (↑s) R M
hs : s.Finite
⊢ ↑hs.toFinset = s

Proof state:
case h.e'_1.h.e'_2
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Finset M), Basis (↑↑s) R M → False
s : Set M
b : Basis (↑s) R M
hs : s.Finite
⊢ ↑hs.toFinset = s

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem continuous_zpow : ∀ z : ℤ, Continuous fun a : G => a ^ z
  | Int.ofNat n => by simpa using continuous_pow n
  | Int.negSucc n => by simpa using (continuous_pow (n + 1)).inv

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
n : ℕ
⊢ Continuous fun a => a ^ Int.ofNat n

Tactic:
simpa using continuous_pow n

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
n : ℕ
⊢ Continuous fun a => a ^ Int.negSucc n

Tactic:
simpa using (continuous_pow (n + 1)).inv

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem invApp_app (U : Opens X) :
    H.invApp _ U ≫ f.c.app (op (opensFunctor f |>.obj U)) = X.presheaf.map
      (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective])) :=
  PresheafedSpace.IsOpenImmersion.invApp_app f.1 U

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑X.toTopCat
⊢ op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))

Tactic:
simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective]

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma Odd.toUnitHom_eval_neg_one (hψ : ψ.Odd) : ψ.toUnitHom (-1) = -1

Proof state:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Odd
⊢ (toUnitHom ψ) (-1) = -1

Tactic:
rw [← Units.eq_iff, MulChar.coe_toUnitHom]

Result:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Odd
⊢ ψ ↑(-1) = ↑(-1)

Proof state:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Odd
⊢ ψ ↑(-1) = ↑(-1)

Tactic:
exact hψ

Result:
no goals
-- Mathlib/Algebra/ZeroOne/Lemmas.lean
@[to_additive ite_nonneg]
lemma one_le_ite [LE α] (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ ite p a b

Proof state:
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 ≤ if p then a else b

Tactic:
split <;> assumption

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convergence.lean
lemma LSeriesSummable.abscissaOfAbsConv_le {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) :
    abscissaOfAbsConv f ≤ s.re :=
  sInf_le <| by simpa using h.of_re_le_re (by simp)

Proof state:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ s.re ≤ (↑s.re).re

Tactic:
simp

Result:
no goals

Proof state:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ ↑s.re ∈ Real.toEReal '' {x | LSeriesSummable f ↑x}

Tactic:
simpa using h.of_re_le_re (by simp)

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma lintegral_rnDeriv [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) :
    ∫⁻ x, μ.rnDeriv ν x ∂ν = μ Set.univ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x ∂ν = μ Set.univ

Tactic:
rw [← setLIntegral_univ, setLIntegral_rnDeriv' hμν MeasurableSet.univ]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem mapIso_trans (F : C ⥤ D) {X Y Z : C} (i : X ≅ Y) (j : Y ≅ Z) :
    F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j

Tactic:
ext

Result:
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ (F.mapIso (i ≪≫ j)).hom = (F.mapIso i ≪≫ F.mapIso j).hom

Proof state:
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ (F.mapIso (i ≪≫ j)).hom = (F.mapIso i ≪≫ F.mapIso j).hom

Tactic:
apply Functor.map_comp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_insertEntryIfNew [BEq α] [PartialEquivBEq α] [Inhabited α]
    {l : List ((a : α) × β a)} {k a : α} {v : β k} : getKey! a (insertEntryIfNew k v l) =
      if k == a ∧ containsKey k l = false then k else getKey! a l

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : PartialEquivBEq α
inst✝ : Inhabited α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ getKey! a (insertEntryIfNew k v l) = if (k == a) = true ∧ containsKey k l = false then k else getKey! a l

Tactic:
simp [getKey!_eq_getKey?, getKey?_insertEntryIfNew, apply_ite Option.get!]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_comp_smul {S : Type*} [SMul S R] [ContinuousConstSMul S R] [SMulZeroClass S A]
    [IsScalarTower S R A] [IsScalarTower S R (R → R)] (s : S) (f : R → R) (a : A)
    (hf : ContinuousOn f ((s • ·) '' (spectrum R a))

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝⁵ : UniqueHom R A
S : Type u_3
inst✝⁴ : SMul S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : autoParam (ContinuousOn f ((fun x => s • x) '' spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => f (s • x)) a = cfc f (s • a)

Tactic:
rw [cfc_comp' .., cfc_smul_id ..]

Result:
no goals
-- Mathlib/GroupTheory/Exponent.lean
theorem ExponentExists.isOfFinOrder (h : ExponentExists G) {g : G} : IsOfFinOrder g :=
  isOfFinOrder_iff_pow_eq_one.mpr <| by peel 2 h; exact this g

Proof state:
G : Type u
inst✝ : Monoid G
h : ExponentExists G
g : G
⊢ ∃ n, 0 < n ∧ g ^ n = 1

Tactic:
peel 2 h

Result:
case h.h
G : Type u
inst✝ : Monoid G
h : ExponentExists G
g : G
n✝ : ℕ
p✝ : 0 < n✝
this : ∀ (g : G), g ^ n✝ = 1
⊢ g ^ n✝ = 1

Proof state:
case h.h
G : Type u
inst✝ : Monoid G
h : ExponentExists G
g : G
n✝ : ℕ
p✝ : 0 < n✝
this : ∀ (g : G), g ^ n✝ = 1
⊢ g ^ n✝ = 1

Tactic:
exact this g

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive] lemma IsMulFreimanHom.mul (h₁ : IsMulFreimanHom n A B₁ f₁)
    (h₂ : IsMulFreimanHom n A B₂ f₂) : IsMulFreimanHom n A (B₁ * B₂) (f₁ * f₂) where
  mapsTo := h₁.mapsTo.mul h₂.mapsTo
  map_prod_eq_map_prod s t hsA htA hs ht h

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B₁ B₂ : Set β
f₁ f₂ : α → β
n : ℕ
h₁ : IsMulFreimanHom n A B₁ f₁
h₂ : IsMulFreimanHom n A B₂ f₂
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
⊢ (map (f₁ * f₂) s).prod = (map (f₁ * f₂) t).prod

Tactic:
rw [Pi.mul_def, prod_map_mul, prod_map_mul, h₁.map_prod_eq_map_prod hsA htA hs ht h,
  h₂.map_prod_eq_map_prod hsA htA hs ht h]

Result:
no goals
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli'_eq_bernoulli (n : ℕ) : bernoulli' n = (-1) ^ n * bernoulli n

Proof state:
n : ℕ
⊢ bernoulli' n = (-1) ^ n * bernoulli n

Tactic:
simp [bernoulli, ← mul_assoc, ← sq, ← pow_mul, mul_comm n 2]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[simp]
lemma negPart_smul {r : ℝ≥0} {a : A} : (r • a)⁻ = r • a⁻

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ≥0
a : A
⊢ (r • a)⁻ = r • a⁻

Tactic:
simpa using posPart_smul (r := r) (a := -a)

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem zsmul_add_modEq (z : ℤ) : z • p + a ≡ a [PMOD p] :=
  ⟨-z, by simp [← sub_sub]⟩

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a : α
z : ℤ
⊢ a - (z • p + a) = -z • p

Tactic:
simp [← sub_sub]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b)

Proof state:
a b : Nat
⊢ ((a == b) = true) = (a = b)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem rootSet_neg (p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] :
    (-p).rootSet S = p.rootSet S

Proof state:
T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ (-p).rootSet S = p.rootSet S

Tactic:
rw [rootSet, aroots_neg, rootSet]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_erase [LawfulBEq α] (h : m.WF) {k a : α} [Inhabited (β a)] :
    (m.erase k).get! a = if k == a then default else m.get! a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
k a : α
inst✝ : Inhabited (β a)
⊢ (m.erase k).get! a = if (k == a) = true then default else m.get! a

Tactic:
simp_to_raw using Raw₀.get!_erase

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem deriv_sub_const_fun (c : F) : deriv (f · - c) = deriv f

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
⊢ (deriv fun x => f x - c) = deriv f

Tactic:
ext

Result:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
x✝ : 𝕜
⊢ deriv (fun x => f x - c) x✝ = deriv f x✝

Proof state:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
x✝ : 𝕜
⊢ deriv (fun x => f x - c) x✝ = deriv f x✝

Tactic:
apply deriv_sub_const

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_iff_getElem? {a} {l : Array α} : a ∈ l ↔ ∃ i : Nat, l[i]? = some a

Proof state:
α : Type u_1
a : α
l : Array α
⊢ a ∈ l ↔ ∃ i, l[i]? = some a

Tactic:
simp [getElem?_eq_some_iff, mem_iff_getElem]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem mem_sup (x : M) : x ∈ N ⊔ N' ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x : M
⊢ x ∈ N ⊔ N' ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x

Tactic:
rw [← mem_toSubmodule, sup_toSubmodule, Submodule.mem_sup]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x : M
⊢ (∃ y ∈ ↑N, ∃ z ∈ ↑N', y + z = x) ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x : M
⊢ (∃ y ∈ ↑N, ∃ z ∈ ↑N', y + z = x) ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x

Tactic:
exact Iff.rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_of_containsKey_insertList [BEq α] [PartialEquivBEq α]
    {l toInsert : List ((a : α) × β a)} {k : α} (h₁ : containsKey k (insertList l toInsert))
    (h₂ : (toInsert.map Sigma.fst).contains k = false) : containsKey k l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l toInsert : List ((a : α) × β a)
k : α
h₁ : containsKey k (insertList l toInsert) = true
h₂ : (List.map Sigma.fst toInsert).contains k = false
⊢ containsKey k l = true

Tactic:
rw [containsKey_insertList, h₂] at h₁

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l toInsert : List ((a : α) × β a)
k : α
h₁ : (containsKey k l || false) = true
h₂ : (List.map Sigma.fst toInsert).contains k = false
⊢ containsKey k l = true

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l toInsert : List ((a : α) × β a)
k : α
h₁ : (containsKey k l || false) = true
h₂ : (List.map Sigma.fst toInsert).contains k = false
⊢ containsKey k l = true

Tactic:
simp at h₁

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l toInsert : List ((a : α) × β a)
k : α
h₂ : (List.map Sigma.fst toInsert).contains k = false
h₁ : containsKey k l = true
⊢ containsKey k l = true

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l toInsert : List ((a : α) × β a)
k : α
h₂ : (List.map Sigma.fst toInsert).contains k = false
h₁ : containsKey k l = true
⊢ containsKey k l = true

Tactic:
exact h₁

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_lt_of_one_lt_left [ExistsAddOfLE α] [MulPosStrictMono α]
    [AddRightStrictMono α] [AddRightReflectLT α]
    (hb : b < 0) (h : 1 < a) : a * b < b

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
hb : b < 0
h : 1 < a
⊢ a * b < b

Tactic:
simpa only [one_mul] using mul_lt_mul_of_neg_right h hb

Result:
no goals