harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Sheaves/SheafCondition/Sites.lean
theorem extend_hom_app (h : Opens.IsBasis (Set.range B))
    (α : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.1) (i : ι) :
    (restrictHomEquivHom F F' h α).app (op (B i)) = α.app (op i)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.val
i : ι
⊢ ((restrictHomEquivHom F F' h) α).app (op (B i)) = α.app (op i)

Tactic:
nth_rw 2 [← (restrictHomEquivHom F F' h).left_inv α]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.val
i : ι
⊢ ((restrictHomEquivHom F F' h) α).app (op (B i)) =
    ((restrictHomEquivHom F F' h).invFun ((restrictHomEquivHom F F' h).toFun α)).app (op i)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.val
i : ι
⊢ ((restrictHomEquivHom F F' h) α).app (op (B i)) =
    ((restrictHomEquivHom F F' h).invFun ((restrictHomEquivHom F F' h).toFun α)).app (op i)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem whiskerLeft_inv_hom (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
    f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)

Tactic:
rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]

Result:
no goals
-- Mathlib/Analysis/Calculus/SmoothSeries.lean
theorem hasFDerivAt_tsum_of_isPreconnected (hu : Summable u) (hs : IsOpen s)
    (h's : IsPreconnected s) (hf : ∀ n x, x ∈ s → HasFDerivAt (f n) (f' n x) x)
    (hf' : ∀ n x, x ∈ s → ‖f' n x‖ ≤ u n) (hx₀ : x₀ ∈ s) (hf0 : Summable fun n => f n x₀)
    (hx : x ∈ s) : HasFDerivAt (fun y => ∑' n, f n y) (∑' n, f' n x) x

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun n => f n x₀
hx : x ∈ s
A : ∀ x ∈ s, Tendsto (fun t => ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))
t : Finset α
y : E
hy : y ∈ s
⊢ HasFDerivAt (fun x => ∑ n ∈ t, f n x) (∑ n ∈ t, f' n y) y

Tactic:
exact HasFDerivAt.sum fun n _ => hf n y hy

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
lemma factor_surjective (H : p ≤ p') : Function.Surjective (factor H)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
⊢ Function.Surjective ⇑(factor H)

Tactic:
intro x

Result:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M ⧸ p'
⊢ ∃ a, (factor H) a = x

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M ⧸ p'
⊢ ∃ a, (factor H) a = x

Tactic:
use Quotient.mk x.out

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M ⧸ p'
⊢ (factor H) (Quotient.mk (Quotient.out x)) = x

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M ⧸ p'
⊢ (factor H) (Quotient.mk (Quotient.out x)) = x

Tactic:
exact Quotient.out_eq x

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- `pred` commutes with `succAbove`. -/
lemma pred_succAbove_pred {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ 0) (hb : b ≠ 0)
    (hk := succAbove_ne_zero ha hb) :
    (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk

Proof state:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (a.succAbove b ≠ 0) ⋯
⊢ (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk

Tactic:
simp_rw [← succ_inj (b := pred (succAbove a b) hk), ← succ_succAbove_succ, succ_pred]

Result:
no goals
-- Mathlib/Logic/ExistsUnique.lean
theorem ExistsUnique.intro₂ {p : α → Sort*} [∀ x, Subsingleton (p x)]
    {q : ∀ (x : α) (_ : p x), Prop} (w : α) (hp : p w) (hq : q w hp)
    (H : ∀ (y) (hy : p y), q y hy → y = w) : ∃! x, ∃! hx : p x, q x hx

Proof state:
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x, ∃ hx, q x hx

Tactic:
exact ExistsUnique.intro w ⟨hp, hq⟩ fun y ⟨hyp, hyq⟩ ↦ H y hyp hyq

Result:
no goals

Proof state:
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x, ∃! hx, q x hx

Tactic:
simp only [existsUnique_iff_exists]

Result:
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x, ∃ hx, q x hx
-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem mapPiLocalization_comp (g : S →+* P) :
    mapPiLocalization (g.comp f) = (mapPiLocalization g).comp (mapPiLocalization f)

Proof state:
case a.h
R : Type u_1
S : Type u_2
P : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring P
f : R →+* S
g : S →+* P
x✝¹ : PiLocalization R
x✝ : PrimeSpectrum P
⊢ (mapPiLocalization (g.comp f)) x✝¹ x✝ = ((mapPiLocalization g).comp (mapPiLocalization f)) x✝¹ x✝

Tactic:
exact congr($(Localization.localRingHom_comp _ _ _ _ rfl _ rfl) _)

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
P : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring P
f : R →+* S
g : S →+* P
⊢ mapPiLocalization (g.comp f) = (mapPiLocalization g).comp (mapPiLocalization f)

Tactic:
ext

Result:
case a.h
R : Type u_1
S : Type u_2
P : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring P
f : R →+* S
g : S →+* P
x✝¹ : PiLocalization R
x✝ : PrimeSpectrum P
⊢ (mapPiLocalization (g.comp f)) x✝¹ x✝ = ((mapPiLocalization g).comp (mapPiLocalization f)) x✝¹ x✝
-- Mathlib/Data/Part.lean
theorem map_id' {f : α → α} (H : ∀ x : α, f x = x) (o) : map f o = o

Proof state:
α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map id o = o

Tactic:
exact id_map o

Result:
no goals

Proof state:
α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map f o = o

Tactic:
rw [show f = id from funext H]

Result:
α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map id o = o
-- Mathlib/Data/Multiset/Filter.lean
theorem filter_cons_of_pos {a : α} (s) : p a → filter p (a ::ₘ s) = a ::ₘ filter p s :=
  Quot.inductionOn s fun _ h => congr_arg ofList <| List.filter_cons_of_pos <| by simpa using h

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
x✝ : List α
h : p a
⊢ decide (p a) = true

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Instances.lean
theorem coe_eq_one {x : Ioc (0 : α) 1} : (x : α) = 1 ↔ x = 1

Proof state:
α : Type u_1
inst✝ : StrictOrderedSemiring α
x : ↑(Ioc 0 1)
⊢ ↑x = 1 ↔ x = 1

Tactic:
symm

Result:
α : Type u_1
inst✝ : StrictOrderedSemiring α
x : ↑(Ioc 0 1)
⊢ x = 1 ↔ ↑x = 1

Proof state:
α : Type u_1
inst✝ : StrictOrderedSemiring α
x : ↑(Ioc 0 1)
⊢ x = 1 ↔ ↑x = 1

Tactic:
exact Subtype.ext_iff

Result:
no goals
-- Mathlib/Data/Finset/Sigma.lean
theorem sigma_eq_empty : s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅

Tactic:
simp only [← not_nonempty_iff_eq_empty, sigma_nonempty, not_exists, not_and]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Pointwise.lean
theorem pointwise_smul_subset_iff {a : M} {S T : Ideal R} : a • S ≤ T ↔ S ≤ a⁻¹ • T

Proof state:
M : Type u_1
R : Type u_2
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S T : Ideal R
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T

Tactic:
rw [← pointwise_smul_le_pointwise_smul_iff (a := a⁻¹), inv_smul_smul]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_sub (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ)
    (hg : Integrable g μ) : setToFun μ T hT (f - g) = setToFun μ T hT f - setToFun μ T hT g

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
⊢ setToFun μ T hT (f - g) = setToFun μ T hT f - setToFun μ T hT g

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, setToFun_add hT hf hg.neg, setToFun_neg hT g]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Inv.lean
theorem derivWithin_inv (x_ne_zero : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    derivWithin (fun x => x⁻¹) s x = -(x ^ 2)⁻¹

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv Inv.inv x = -(x ^ 2)⁻¹

Tactic:
exact deriv_inv

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x => x⁻¹) s x = -(x ^ 2)⁻¹

Tactic:
rw [DifferentiableAt.derivWithin (differentiableAt_inv x_ne_zero) hxs]

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv Inv.inv x = -(x ^ 2)⁻¹
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem affineSpan_insert_affineSpan (p : P) (ps : Set P) :
    affineSpan k (insert p (affineSpan k ps : Set P)) = affineSpan k (insert p ps)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
ps : Set P
⊢ affineSpan k (insert p ↑(affineSpan k ps)) = affineSpan k (insert p ps)

Tactic:
rw [Set.insert_eq, Set.insert_eq, span_union, span_union, affineSpan_coe]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem preimage_mul_preimage_subset {s t : Set β} : m ⁻¹' s * m ⁻¹' t ⊆ m ⁻¹' (s * t)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
⊢ ⇑m ⁻¹' s * ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s * t)

Tactic:
rintro _ ⟨_, _, _, _, rfl⟩

Result:
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
w✝¹ : α
left✝¹ : w✝¹ ∈ ⇑m ⁻¹' s
w✝ : α
left✝ : w✝ ∈ ⇑m ⁻¹' t
⊢ (fun x1 x2 => x1 * x2) w✝¹ w✝ ∈ ⇑m ⁻¹' (s * t)

Proof state:
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
w✝¹ : α
left✝¹ : w✝¹ ∈ ⇑m ⁻¹' s
w✝ : α
left✝ : w✝ ∈ ⇑m ⁻¹' t
⊢ (fun x1 x2 => x1 * x2) w✝¹ w✝ ∈ ⇑m ⁻¹' (s * t)

Tactic:
exact ⟨_, ‹_›, _, ‹_›, (map_mul m ..).symm⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem localizationToStalk_mk' (x : PrimeSpectrum.Top R) (f : R) (s : x.asIdeal.primeCompl) :
    localizationToStalk R x (IsLocalization.mk' (Localization.AtPrime x.asIdeal) f s) =
      (structureSheaf R).presheaf.germ (PrimeSpectrum.basicOpen (s : R)) x s.2
        (const R f s (PrimeSpectrum.basicOpen s) fun _ => id) :=
  (IsLocalization.lift_mk'_spec (S := Localization.AtPrime x.asIdeal) _ _ _ _).2 <| by
    rw [← germ_toOpen R (PrimeSpectrum.basicOpen s) x s.2,
      ← germ_toOpen R (PrimeSpectrum.basicOpen s) x s.2, ← RingHom.map_mul, toOpen_eq_const,
      toOpen_eq_const, const_mul_cancel']

Proof state:
R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
f : R
s : ↥x.asIdeal.primeCompl
⊢ (ConcreteCategory.hom (toStalk R x)) f =
    (ConcreteCategory.hom (toStalk R x)) ↑s *
      (ConcreteCategory.hom ((structureSheaf R).presheaf.germ (PrimeSpectrum.basicOpen ↑s) x ⋯))
        (const R f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)

Tactic:
rw [← germ_toOpen R (PrimeSpectrum.basicOpen s) x s.2,
  ← germ_toOpen R (PrimeSpectrum.basicOpen s) x s.2, ← RingHom.map_mul, toOpen_eq_const,
  toOpen_eq_const, const_mul_cancel']

Result:
no goals
-- Mathlib/Data/Prod/Lex.lean
theorem monotone_fst [Preorder α] [LE β] (t c : α ×ₗ β) (h : t ≤ c) :
    (ofLex t).1 ≤ (ofLex c).1

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LE β
t c : Lex (α × β)
h : t ≤ c
h' : t.1 < c.1
⊢ (ofLex t).1 ≤ (ofLex c).1

Tactic:
exact h'.le

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LE β
t c : Lex (α × β)
h : t ≤ c
h' : t.1 = c.1 ∧ t.2 ≤ c.2
⊢ (ofLex t).1 ≤ (ofLex c).1

Tactic:
exact h'.1.le

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LE β
t c : Lex (α × β)
h : t ≤ c
⊢ (ofLex t).1 ≤ (ofLex c).1

Tactic:
cases toLex_le_toLex.mp h with
| inl h' => exact h'.le
| inr h' => exact h'.1.le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)} {k : α}
    (h' : (l.map Prod.fst).contains k = false) :
    get? (insertMany m l).1 k = get? m k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
k : α
h' : (List.map Prod.fst l).contains k = false
⊢ get? (insertMany m l).val k = get? m k

Tactic:
simp_to_model [Const.insertMany] using List.getValue?_insertListConst_of_contains_eq_false

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem eq_of_mem_map_const {b₁ b₂ : β} {l : List α} (h : b₁ ∈ map (const α b₂) l) :
    b₁ = b₂

Proof state:
α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) l
⊢ b₁ = b₂

Tactic:
rw [map_const] at h

Result:
α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ replicate l.length b₂
⊢ b₁ = b₂

Proof state:
α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ replicate l.length b₂
⊢ b₁ = b₂

Tactic:
exact eq_of_mem_replicate h

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem subtype_comp_inclusion {H K : S} (hH : H ≤ K) :
    (SubgroupClass.subtype K).comp (inclusion hH) = SubgroupClass.subtype H

Proof state:
G : Type u_1
inst✝² : Group G
S : Type u_4
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
H K : S
hH : H ≤ K
⊢ (↑K).comp (inclusion hH) = ↑H

Tactic:
ext

Result:
case h
G : Type u_1
inst✝² : Group G
S : Type u_4
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
H K : S
hH : H ≤ K
x✝ : ↥H
⊢ ((↑K).comp (inclusion hH)) x✝ = ↑H x✝

Proof state:
case h
G : Type u_1
inst✝² : Group G
S : Type u_4
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
H K : S
hH : H ≤ K
x✝ : ↥H
⊢ ((↑K).comp (inclusion hH)) x✝ = ↑H x✝

Tactic:
simp only [MonoidHom.comp_apply, coe_subtype, coe_inclusion]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem comapDomain_add [∀ i, AddZeroClass (β i)] (h : κ → ι) (hh : Function.Injective h)
    (f g : Π₀ i, β i) : comapDomain h hh (f + g) = comapDomain h hh f + comapDomain h hh g

Proof state:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
hh : Function.Injective h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain h hh (f + g)) i✝ = (comapDomain h hh f + comapDomain h hh g) i✝

Tactic:
rw [add_apply, comapDomain_apply, comapDomain_apply, comapDomain_apply, add_apply]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
hh : Function.Injective h
f g : Π₀ (i : ι), β i
⊢ comapDomain h hh (f + g) = comapDomain h hh f + comapDomain h hh g

Tactic:
ext

Result:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
hh : Function.Injective h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain h hh (f + g)) i✝ = (comapDomain h hh f + comapDomain h hh g) i✝
-- Mathlib/Data/Matrix/Mul.lean
theorem mulVec_smul [Fintype n] [Monoid R] [NonUnitalNonAssocSemiring S] [DistribMulAction R S]
    [SMulCommClass R S S] (M : Matrix m n S) (b : R) (v : n → S) :
    M *ᵥ (b • v) = b • M *ᵥ v

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst✝⁴ : Fintype n
inst✝³ : Monoid R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : DistribMulAction R S
inst✝ : SMulCommClass R S S
M : Matrix m n S
b : R
v : n → S
⊢ M *ᵥ b • v = b • M *ᵥ v

Tactic:
ext i

Result:
case h
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst✝⁴ : Fintype n
inst✝³ : Monoid R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : DistribMulAction R S
inst✝ : SMulCommClass R S S
M : Matrix m n S
b : R
v : n → S
i : m
⊢ (M *ᵥ b • v) i = (b • M *ᵥ v) i

Proof state:
case h
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst✝⁴ : Fintype n
inst✝³ : Monoid R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : DistribMulAction R S
inst✝ : SMulCommClass R S S
M : Matrix m n S
b : R
v : n → S
i : m
⊢ (M *ᵥ b • v) i = (b • M *ᵥ v) i

Tactic:
simp only [mulVec, dotProduct, Finset.smul_sum, Pi.smul_apply, mul_smul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem conjugateEquiv_comm {α : L₂ ⟶ L₁} {β : L₁ ⟶ L₂} (βα : β ≫ α = 𝟙 _) :
    conjugateEquiv adj₁ adj₂ α ≫ conjugateEquiv adj₂ adj₁ β = 𝟙 _

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
β : L₁ ⟶ L₂
βα : β ≫ α = 𝟙 L₁
⊢ (conjugateEquiv adj₁ adj₂) α ≫ (conjugateEquiv adj₂ adj₁) β = 𝟙 R₁

Tactic:
rw [conjugateEquiv_comp, βα, conjugateEquiv_id]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_inf_self_right (a b : α) : b \ (a ⊓ b) = b \ a

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b \ (a ⊓ b) = b \ a

Tactic:
rw [sdiff_inf, sdiff_self, sup_bot_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem rightAdjointUniq_trans_app {F : C ⥤ D} {G G' G'' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
    (adj3 : F ⊣ G'') (x : D) :
    (rightAdjointUniq adj1 adj2).hom.app x ≫ (rightAdjointUniq adj2 adj3).hom.app x =
      (rightAdjointUniq adj1 adj3).hom.app x

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
    (adj1.rightAdjointUniq adj3).hom.app x

Tactic:
rw [← rightAdjointUniq_trans adj1 adj2 adj3]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
    ((adj1.rightAdjointUniq adj2).hom ≫ (adj2.rightAdjointUniq adj3).hom).app x

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
    ((adj1.rightAdjointUniq adj2).hom ≫ (adj2.rightAdjointUniq adj3).hom).app x

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/Lookmap.lean
theorem lookmap_cons_some {a b : α} (l : List α) (h : f a = some b) :
    (a :: l).lookmap f = b :: l

Proof state:
α : Type u_1
f : α → Option α
a b : α
l : List α
h : f a = some b
⊢ (match f a with
    | some b => b :: l
    | none => lookmap.go f l (#[].push a)) =
    b :: l

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Type u_1
f : α → Option α
a b : α
l : List α
h : f a = some b
⊢ lookmap f (a :: l) = b :: l

Tactic:
simp only [lookmap, lookmap.go, Array.toListAppend_eq, Array.toList_toArray, nil_append]

Result:
α : Type u_1
f : α → Option α
a b : α
l : List α
h : f a = some b
⊢ (match f a with
    | some b => b :: l
    | none => lookmap.go f l (#[].push a)) =
    b :: l
-- Mathlib/LinearAlgebra/Ray.lean
theorem units_smul_eq_self_iff {u : Rˣ} {v : Module.Ray R M} : u • v = v ↔ 0 < u.1

Proof state:
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
u : Rˣ
v : Module.Ray R M
⊢ u • v = v ↔ 0 < ↑u

Tactic:
induction v using Module.Ray.ind with | h v hv =>
simp only [smul_rayOfNeZero, ray_eq_iff, Units.smul_def, sameRay_smul_left_iff_of_ne hv u.ne_zero]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
u : Rˣ
v : M
hv : v ≠ 0
⊢ u • rayOfNeZero R v hv = rayOfNeZero R v hv ↔ 0 < ↑u

Tactic:
simp only [smul_rayOfNeZero, ray_eq_iff, Units.smul_def, sameRay_smul_left_iff_of_ne hv u.ne_zero]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_lt_nmul_of_pos_right (h₁ : a < b) (h₂ : 0 < c) : a ⨳ c < b ⨳ c :=
  lt_nmul_iff.2 ⟨a, h₁, 0, h₂, by simp⟩

Proof state:
a b c : Ordinal.{u}
h₁ : a < b
h₂ : 0 < c
⊢ a ⨳ c ♯ a ⨳ 0 ≤ a ⨳ c ♯ b ⨳ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
lemma IsSelfAdjoint.coe_mem_spectrum_complex {A : Type*} [TopologicalSpace A] [Ring A]
    [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ (IsStarNormal : A → Prop)]
    {a : A} {x : ℝ} (ha : IsSelfAdjoint a

Proof state:
A : Type u_3
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
a : A
x : ℝ
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ ↑x ∈ spectrum ℂ a ↔ x ∈ spectrum ℝ a

Tactic:
simp [← ha.spectrumRestricts.algebraMap_image]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean
theorem isUnit_of_isUnit_ι {m : M} (h : IsUnit (ι Q m)) : IsUnit (Q m)

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
m : M
h : IsUnit ((ι Q) m)
⊢ IsUnit (Q m)

Tactic:
cases h.nonempty_invertible

Result:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
m : M
h : IsUnit ((ι Q) m)
val✝ : Invertible ((ι Q) m)
⊢ IsUnit (Q m)

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
m : M
h : IsUnit ((ι Q) m)
val✝ : Invertible ((ι Q) m)
this : Invertible (Q m) := invertibleOfInvertibleι Q m
⊢ IsUnit (Q m)

Tactic:
exact isUnit_of_invertible (Q m)

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
m : M
h : IsUnit ((ι Q) m)
val✝ : Invertible ((ι Q) m)
⊢ IsUnit (Q m)

Tactic:
letI := invertibleOfInvertibleι Q m

Result:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
m : M
h : IsUnit ((ι Q) m)
val✝ : Invertible ((ι Q) m)
this : Invertible (Q m) := invertibleOfInvertibleι Q m
⊢ IsUnit (Q m)