harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/SurjectiveOnStalks.lean
lemma surjectiveOnStalks_of_exists_div (h : ∀ x : S, ∃ r s : R, IsUnit (f s) ∧ f s * x = f r) :
    SurjectiveOnStalks f :=
  surjectiveOnStalks_iff_forall_ideal.mpr fun I hI x ↦
    let ⟨r, s, hr, hr'⟩ := h x
    ⟨r, s, 1, by simpa [← Ideal.eq_top_iff_one], fun h ↦ hI (I.eq_top_of_isUnit_mem h hr), by simpa⟩

Proof state:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
h : ∀ (x : S), ∃ r s, IsUnit (f s) ∧ f s * x = f r
I : Ideal S
hI : I ≠ ⊤
x : S
r s : R
hr : IsUnit (f s)
hr' : f s * x = f r
⊢ 1 * f s * x = 1 * f r

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
h : ∀ (x : S), ∃ r s, IsUnit (f s) ∧ f s * x = f r
I : Ideal S
hI : I ≠ ⊤
x : S
r s : R
hr : IsUnit (f s)
hr' : f s * x = f r
⊢ 1 ∉ I

Tactic:
simpa [← Ideal.eq_top_iff_one]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem isometryEquiv_map_mkMetric (m : ℝ≥0∞ → ℝ≥0∞) (f : X ≃ᵢ Y) :
    map f (mkMetric m) = mkMetric m

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X ≃ᵢ Y
⊢ (map ⇑f) (mkMetric m) = mkMetric m

Tactic:
rw [← isometryEquiv_comap_mkMetric _ f, map_comap_of_surjective f.surjective]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem blimsup_false {f : Filter β} {u : β → α} : (blimsup u f fun _ => False) = ⊥

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ (blimsup u f fun x => False) = ⊥

Tactic:
simp [blimsup_eq]

Result:
no goals
-- Mathlib/Analysis/Normed/Order/Lattice.lean
theorem norm_sup_le_add (x y : α) : ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖

Tactic:
simpa only [sup_idem, sub_zero] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖

Tactic:
have h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖ := norm_sup_sub_sup_le_add_norm x y 0 0

Result:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
-- Mathlib/Data/Set/Card.lean
theorem sep_of_ncard_eq {a : α} {P : α → Prop} (h : { x ∈ s | P x }.ncard = s.ncard) (ha : a ∈ s)
    (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
a : α
P : α → Prop
h : {x | x ∈ s ∧ P x}.ncard = s.ncard
ha : a ∈ s
hs : autoParam s.Finite _auto✝
⊢ {x | x ∈ s ∧ P x} ⊆ s

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem MDifferentiableAt.comp_of_eq {y : M'} (hg : MDifferentiableAt I' I'' g y)
    (hf : MDifferentiableAt I I' f x) (hy : f x = y) : MDifferentiableAt I I'' (g ∘ 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
inst✝¹⁰ : ChartedSpace H 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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
hf : MDifferentiableAt I I' f x
hg : MDifferentiableAt I' I'' g (f x)
⊢ MDifferentiableAt I I'' (g ∘ f) x

Tactic:
exact hg.comp _ hf

Result:
no goals

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
inst✝¹⁰ : ChartedSpace H 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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
y : M'
hg : MDifferentiableAt I' I'' g y
hf : MDifferentiableAt I I' f x
hy : f x = y
⊢ MDifferentiableAt I I'' (g ∘ f) x

Tactic:
subst hy

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
inst✝¹⁰ : ChartedSpace H 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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
hf : MDifferentiableAt I I' f x
hg : MDifferentiableAt I' I'' g (f x)
⊢ MDifferentiableAt I I'' (g ∘ f) x
-- Mathlib/Analysis/Convex/EGauge.lean
lemma egauge_le_one (h : x ∈ s) : egauge 𝕜 s x ≤ 1

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
h : x ∈ 1 • s
⊢ egauge 𝕜 s x ≤ 1

Tactic:
simpa using egauge_le_of_mem_smul h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
h : x ∈ s
⊢ egauge 𝕜 s x ≤ 1

Tactic:
rw [← one_smul 𝕜 s] at h

Result:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
h : x ∈ 1 • s
⊢ egauge 𝕜 s x ≤ 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_neg_add_of_add_le {a b c : Int} (h : a + b ≤ c) : b ≤ -a + c

Proof state:
a b c : Int
h : a + b ≤ c
⊢ b ≤ -a + c

Tactic:
have h := Int.add_le_add_left h (-a)

Result:
a b c : Int
h✝ : a + b ≤ c
h : -a + (a + b) ≤ -a + c
⊢ b ≤ -a + c

Proof state:
a b c : Int
h✝ : a + b ≤ c
h : -a + (a + b) ≤ -a + c
⊢ b ≤ -a + c

Tactic:
rwa [Int.neg_add_cancel_left] at h

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
@[simp] lemma append_eq_cons {a : α} {as : Stream' α} : [a] ++ₛ as = a :: as

Proof state:
α : Type u
a : α
as : Stream' α
⊢ [a] ++ₛ as = a :: as

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem map_monotone (d : ℕ) : Monotone (map d : (Fin n → ℕ) → ℕ) := fun x y h => by
  dsimp; exact sum_le_sum fun i _ => Nat.mul_le_mul_right _ <| h i

Proof state:
n d : ℕ
x y : Fin n → ℕ
h : x ≤ y
⊢ (map d) x ≤ (map d) y

Tactic:
dsimp

Result:
n d : ℕ
x y : Fin n → ℕ
h : x ≤ y
⊢ ∑ i : Fin n, x i * d ^ ↑i ≤ ∑ i : Fin n, y i * d ^ ↑i

Proof state:
n d : ℕ
x y : Fin n → ℕ
h : x ≤ y
⊢ ∑ i : Fin n, x i * d ^ ↑i ≤ ∑ i : Fin n, y i * d ^ ↑i

Tactic:
exact sum_le_sum fun i _ => Nat.mul_le_mul_right _ <| h i

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_reverse {l : List α} (h : l.reverse ≠ []) :
    l.reverse.getLast h = l.head (by simp_all)

Proof state:
α : Type ?u.312901
l : List α
h : l.reverse ≠ []
⊢ l ≠ []

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l : List α
h : l.reverse ≠ []
⊢ l.reverse.getLast h = l.head ⋯

Tactic:
simp [getLast_eq_head_reverse]

Result:
no goals
-- Mathlib/Algebra/Algebra/Bilinear.lean
theorem toSpanSingleton_eq_algebra_linearMap : toSpanSingleton R A 1 = Algebra.linearMap R A

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ toSpanSingleton R A 1 = Algebra.linearMap R A

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (toSpanSingleton R A 1) 1 = (Algebra.linearMap R A) 1

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (toSpanSingleton R A 1) 1 = (Algebra.linearMap R A) 1

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem _root_.IsPrimitiveRoot.pow_add_pow_eq_prod_add_mul (hodd : Odd n)
    (h : IsPrimitiveRoot ζ n) : x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n R, (x + ζ * y)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hodd : Odd n
h : IsPrimitiveRoot ζ n
⊢ x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n R, (x + ζ * y)

Tactic:
simpa [hodd.neg_pow] using h.pow_sub_pow_eq_prod_sub_mul x (-y) hodd.pos

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem false_of_not_eq_self {a : Prop} (h : (Not a) = a) : False

Proof state:
a : Prop
h : (¬a) = a
⊢ False

Tactic:
by_cases a <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} :
    m.1.isEmpty = true → m.getKey! a = default

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
a : α
⊢ (toListModel m.val.buckets).isEmpty = true → List.getKey! a (toListModel m.val.buckets) = default

Tactic:
empty

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
a : α
⊢ m.val.isEmpty = true → m.getKey! a = default

Tactic:
simp_to_model

Result:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
a : α
⊢ (toListModel m.val.buckets).isEmpty = true → List.getKey! a (toListModel m.val.buckets) = default
-- Mathlib/Topology/Algebra/MvPolynomial.lean
theorem MvPolynomial.continuous_eval : Continuous fun x ↦ eval x p

Proof state:
X : Type u_1
σ : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CommSemiring X
inst✝ : IsTopologicalSemiring X
p : MvPolynomial σ X
⊢ Continuous fun x => (eval x) p

Tactic:
continuity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.add_not (a : BitVec w) : a + ~~~a = (-1#w)

Proof state:
case pred
w : Nat
a : BitVec w
i✝ : Nat
a✝ : i✝ < w
⊢ (a + ~~~a).getLsbD i✝ = (-1#w).getLsbD i✝

Tactic:
simp [BitVec.negOne_eq_allOnes]

Result:
no goals

Proof state:
w : Nat
a : BitVec w
⊢ a + ~~~a = -1#w

Tactic:
ext

Result:
case pred
w : Nat
a : BitVec w
i✝ : Nat
a✝ : i✝ < w
⊢ (a + ~~~a).getLsbD i✝ = (-1#w).getLsbD i✝
-- Mathlib/Data/Matroid/Loop.lean
@[simp]
lemma uniqueBaseOn_isLoop_iff {I E : Set α} : (uniqueBaseOn I E).IsLoop e ↔ e ∈ E \ I

Proof state:
α : Type u_1
e : α
I E : Set α
⊢ (uniqueBaseOn I E).IsLoop e ↔ e ∈ E \ I

Tactic:
simp [isLoop_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, if `e₁` and `e₂` are compatible with the
unit of the adjunction `adj`, then `e₂` uniquely determines `e₁`.
-/
lemma compatibilityUnit_unique_left (h : CompatibilityUnit adj e₁ e₂)
    (h' : CompatibilityUnit adj e₁' e₂) : e₁ = e₁'

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ e₁' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁' e₂
⊢ e₁ = e₁'

Tactic:
ext

Result:
case w.w.h
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ e₁' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁' e₂
x✝ : C
⊢ e₁.hom.app x✝ = e₁'.hom.app x✝

Proof state:
case w.w.h
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ e₁' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁' e₂
x✝ : C
⊢ e₁.hom.app x✝ = e₁'.hom.app x✝

Tactic:
rw [compatibilityCounit_left adj e₁ e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h),
  compatibilityCounit_left adj e₁' e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h')]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_ofList_of_contains_eq_false [LawfulBEq α]
    {l : List (α × β)} {k : α}
    (contains_eq_false : (l.map Prod.fst).contains k = false) :
    get? (ofList l) k = none

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k : α
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ get? (ofList l) k = none

Tactic:
simp_to_raw using Raw₀.Const.get?_insertMany_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_inj (hx : 0 ≤ x) (hy : 0 ≤ y) : √x = √y ↔ x = y

Proof state:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x = √y ↔ x = y

Tactic:
simp [le_antisymm_iff, hx, hy]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} :
    m.contains a = false → m.getKey! a = default

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
a : α
⊢ m.contains a = false → m.getKey! a = default

Tactic:
simp_to_model using List.getKey!_eq_default

Result:
no goals
-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_comp_comm' (f : M →ₗ[R] N) (g : N →ₗ[R] M) :
    trace R M (g ∘ₗ f) = trace R N (f ∘ₗ g)

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] M
h : (((llcomp R M N M).compr₂ (trace R M)) g) f = (((llcomp R N M N).flip.compr₂ (trace R N)) g) f
⊢ (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)

Tactic:
simp only [llcomp_apply', compr₂_apply, flip_apply] at h

Result:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] M
h : (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)
⊢ (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] M
⊢ (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)

Tactic:
have h := LinearMap.ext_iff.1 (LinearMap.ext_iff.1 (trace_comp_comm R M N) g) f

Result:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] M
h : (((llcomp R M N M).compr₂ (trace R M)) g) f = (((llcomp R N M N).flip.compr₂ (trace R N)) g) f
⊢ (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] M
h : (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)
⊢ (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)

Tactic:
exact h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem isRight_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
    isRight (x.map f g) = isRight x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
x : α ⊕ γ
⊢ (Sum.map f g x).isRight = x.isRight

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem ringHom_fieldRange_eq_of_comp_eq (h : RingHom.comp f (algebraMap A K) = g) :
    f.fieldRange = Subfield.closure g.range

Proof state:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
⊢ f.fieldRange = Subfield.closure ↑g.range

Tactic:
rw [f.fieldRange_eq_map, ← closure_range_algebraMap A K,
  f.map_field_closure, ← Set.range_comp, ← f.coe_comp, h, g.coe_range]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem mem_fixedPoints_or_exists_zpow_eq (x : α) :
    x ∈ Function.fixedPoints g ∨
      ∃ (c : g.cycleFactorsFinset) (_ : x ∈ c.val.support) (m : ℤ), (g ^ m) (a c) = x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
⊢ x ∉ Function.fixedPoints ⇑g → ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x

Tactic:
intro hx

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : x ∉ Function.fixedPoints ⇑g
⊢ ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ g.SameCycle x x ∧ g.cycleOf x ∈ g.cycleFactorsFinset

Tactic:
simp [SameCycle.rfl, hx, and_self]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
⊢ x ∈ Function.fixedPoints ⇑g ∨ ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x

Tactic:
rw [Classical.or_iff_not_imp_left]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
⊢ x ∉ Function.fixedPoints ⇑g → ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x

Tactic:
refine ⟨⟨g.cycleOf x, hx⟩, ?_, (a.sameCycle hx)⟩

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ x ∈ (↑⟨g.cycleOf x, hx⟩).support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : x ∉ Function.fixedPoints ⇑g
⊢ ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x

Tactic:
rw [Function.mem_fixedPoints_iff, ← ne_eq, ← mem_support,
  ← cycleOf_mem_cycleFactorsFinset_iff] at hx

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ x ∈ (↑⟨g.cycleOf x, hx⟩).support

Tactic:
rw [mem_support_cycleOf_iff, ← cycleOf_mem_cycleFactorsFinset_iff]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ g.SameCycle x x ∧ g.cycleOf x ∈ g.cycleFactorsFinset
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma CFC.eq_zero_of_spectrum_subset_zero (h_spec : spectrum R a ⊆ {0}) (ha : p 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
a : A
h_spec : spectrum R a ⊆ {0}
ha : autoParam (p a) _auto✝
⊢ a = 0

Tactic:
simpa using eq_algebraMap_of_spectrum_subset_singleton a 0 h_spec

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem Filter.Tendsto.mul_atBot {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (𝓝 C))
    (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atBot
⊢ Tendsto (fun x => f x * g x) l atBot

Tactic:
simpa only [mul_comm] using hg.atBot_mul hC hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} {h'}
    (hl : DistinctKeys l) (h : Perm l l') :
    getKey a l h' = getKey a l' ((containsKey_of_perm h).symm.trans h')

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
h' : containsKey a l = true
hl : DistinctKeys l
h : l.Perm l'
⊢ getKey a l h' = getKey a l' ⋯

Tactic:
rw [← Option.some_inj, ← getKey?_eq_some_getKey, ← getKey?_eq_some_getKey,
  getKey?_of_perm hl h]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem mk_eq_one [Monoid M] {a : M} : Associates.mk a = 1 ↔ IsUnit a

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
⊢ Associates.mk a = 1 ↔ IsUnit a

Tactic:
rw [← mk_one, mk_eq_mk_iff_associated, associated_one_iff_isUnit]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem norm_deriv_le_of_lip' {f : 𝕜 → F} {x₀ : 𝕜}
    {C : ℝ} (hC₀ : 0 ≤ C) (hlip : ∀ᶠ x in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) :
    ‖deriv f x₀‖ ≤ C

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x₀ : 𝕜
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : 𝕜) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ‖deriv f x₀‖ ≤ C

Tactic:
simpa [norm_deriv_eq_norm_fderiv] using norm_fderiv_le_of_lip' 𝕜 hC₀ hlip

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
@[to_additive (attr := simp)]
lemma inv_Ioc (a b : α) : (Ioc a b)⁻¹ = Ico b⁻¹ a⁻¹

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ (Ioc a b)⁻¹ = Ico b⁻¹ a⁻¹

Tactic:
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isLittleO_iff_forall_isBigOWith : f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
⊢ f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g

Tactic:
rw [IsLittleO_def]

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem Option.naturality [LawfulApplicative F] {α β} (f : α → F β) (x : Option α) :
    η (Option.traverse f x) = Option.traverse (@η _ ∘ f) x

Proof state:
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
inst✝ : LawfulApplicative F
α : Type u_1
β : Type u
f : α → F β
x : Option α
⊢ (fun {α} => η.app α) (Option.traverse f x) = Option.traverse ((fun {α} => η.app α) ∘ f) x

Tactic:
rcases x with - | x <;> simp! [*, functor_norm, ApplicativeTransformation.preserves_map,
  ApplicativeTransformation.preserves_seq, ApplicativeTransformation.preserves_pure]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem sinh_pos_iff : 0 < sinh x ↔ 0 < x

Proof state:
x : ℝ
⊢ 0 < sinh x ↔ 0 < x

Tactic:
simpa only [sinh_zero] using @sinh_lt_sinh 0 x

Result:
no goals