harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
lemma _root_.LinearMap.restrictScalars_toMatrix (f : M →ₗ[A] M) :
    (f.restrictScalars R).toMatrix (bA.smulTower' bM) (bA.smulTower' bM) =
      ((f.toMatrix bM bM).map (leftMulMatrix bA)).comp _ _ _ _ _

Proof state:
case a
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq m
A : Type u_4
M : Type u_5
n : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : CommSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
bA : Basis m R A
bM : Basis n A M
f : M →ₗ[A] M
i✝ j✝ : n × m
⊢ (toMatrix (bA.smulTower' bM) (bA.smulTower' bM)) (↑R f) i✝ j✝ =
    (Matrix.comp n n m m R) (((toMatrix bM bM) f).map ⇑(leftMulMatrix bA)) i✝ j✝

Tactic:
simp [toMatrix, Basis.repr, Algebra.leftMulMatrix_apply,
Basis.smulTower'_repr, Basis.smulTower'_apply, mul_comm]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq m
A : Type u_4
M : Type u_5
n : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : CommSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
bA : Basis m R A
bM : Basis n A M
f : M →ₗ[A] M
⊢ (toMatrix (bA.smulTower' bM) (bA.smulTower' bM)) (↑R f) =
    (Matrix.comp n n m m R) (((toMatrix bM bM) f).map ⇑(leftMulMatrix bA))

Tactic:
ext

Result:
case a
R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq m
A : Type u_4
M : Type u_5
n : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : CommSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
bA : Basis m R A
bM : Basis n A M
f : M →ₗ[A] M
i✝ j✝ : n × m
⊢ (toMatrix (bA.smulTower' bM) (bA.smulTower' bM)) (↑R f) i✝ j✝ =
    (Matrix.comp n n m m R) (((toMatrix bM bM) f).map ⇑(leftMulMatrix bA)) i✝ j✝
-- Mathlib/ModelTheory/Encoding.lean
/-- Decodes a list of symbols as a list of formulas. -/
@[simp]
lemma sigmaImp_apply {n} {φ ψ : L.BoundedFormula α n} :
    sigmaImp ⟨n, φ⟩ ⟨n, ψ⟩ = ⟨n, φ.imp ψ⟩

Proof state:
L : Language
α : Type u'
n : ℕ
φ ψ : L.BoundedFormula α n
⊢ sigmaImp ⟨n, φ⟩ ⟨n, ψ⟩ = ⟨n, φ ⟹ ψ⟩

Tactic:
simp only [sigmaImp, ↓reduceDIte, eq_mp_eq_cast, cast_eq]

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Basic.lean
theorem finite_sUnion_mem_iff {s : Set (Set α)} (hs : s.Finite) : ⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f :=
  Finite.induction_on _ hs (by simp) fun _ _ his => by
    simp [union_mem_iff, his, or_and_right, exists_or]

Proof state:
α : Type u
f : Ultrafilter α
s : Set (Set α)
hs : s.Finite
⊢ ⋃₀ ∅ ∈ f ↔ ∃ t ∈ ∅, t ∈ f

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
f : Ultrafilter α
s : Set (Set α)
hs : s.Finite
a✝ : Set α
s✝ : Set (Set α)
x✝¹ : a✝ ∉ s✝
x✝ : s✝.Finite
his : ⋃₀ s✝ ∈ f ↔ ∃ t ∈ s✝, t ∈ f
⊢ ⋃₀ insert a✝ s✝ ∈ f ↔ ∃ t ∈ insert a✝ s✝, t ∈ f

Tactic:
simp [union_mem_iff, his, or_and_right, exists_or]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.size_merge_node (le) (a₁ : α) (c₁ s₁ : Heap α) (a₂ : α) (c₂ s₂ : Heap α) :
    (merge le (.node a₁ c₁ s₁) (.node a₂ c₂ s₂)).size = c₁.size + c₂.size + 2

Proof state:
α : Type u_1
le : α → α → Bool
a₁ : α
c₁ s₁ : Heap α
a₂ : α
c₂ s₂ : Heap α
⊢ (merge le (node a₁ c₁ s₁) (node a₂ c₂ s₂)).size = c₁.size + c₂.size + 2

Tactic:
unfold merge

Result:
α : Type u_1
le : α → α → Bool
a₁ : α
c₁ s₁ : Heap α
a₂ : α
c₂ s₂ : Heap α
⊢ (match node a₁ c₁ s₁, node a₂ c₂ s₂ with
      | nil, nil => nil
      | nil, node a₂ c₂ sibling => node a₂ c₂ nil
      | node a₁ c₁ sibling, nil => node a₁ c₁ nil
      | node a₁ c₁ sibling, node a₂ c₂ sibling_1 =>
        if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil).size =
    c₁.size + c₂.size + 2

Proof state:
α : Type u_1
le : α → α → Bool
a₁ : α
c₁ s₁ : Heap α
a₂ : α
c₂ s₂ : Heap α
⊢ (match node a₁ c₁ s₁, node a₂ c₂ s₂ with
      | nil, nil => nil
      | nil, node a₂ c₂ sibling => node a₂ c₂ nil
      | node a₁ c₁ sibling, nil => node a₁ c₁ nil
      | node a₁ c₁ sibling, node a₂ c₂ sibling_1 =>
        if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil).size =
    c₁.size + c₂.size + 2

Tactic:
dsimp

Result:
α : Type u_1
le : α → α → Bool
a₁ : α
c₁ s₁ : Heap α
a₂ : α
c₂ s₂ : Heap α
⊢ (if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil).size = c₁.size + c₂.size + 2

Proof state:
α : Type u_1
le : α → α → Bool
a₁ : α
c₁ s₁ : Heap α
a₂ : α
c₂ s₂ : Heap α
⊢ (if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil).size = c₁.size + c₂.size + 2

Tactic:
split <;> simp_arith [size]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem mem_graph_snd_inj' (f : E →ₗ.[R] F) {x y : E × F} (hx : x ∈ f.graph) (hy : y ∈ f.graph)
    (hxy : x.1 = y.1) : x.2 = y.2

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x y : E × F
hx : x ∈ f.graph
hy : y ∈ f.graph
hxy : x.1 = y.1
⊢ x.2 = y.2

Tactic:
cases x

Result:
case mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
y : E × F
hy : y ∈ f.graph
fst✝ : E
snd✝ : F
hx : (fst✝, snd✝) ∈ f.graph
hxy : (fst✝, snd✝).1 = y.1
⊢ (fst✝, snd✝).2 = y.2

Proof state:
case mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
y : E × F
hy : y ∈ f.graph
fst✝ : E
snd✝ : F
hx : (fst✝, snd✝) ∈ f.graph
hxy : (fst✝, snd✝).1 = y.1
⊢ (fst✝, snd✝).2 = y.2

Tactic:
cases y

Result:
case mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
fst✝¹ : E
snd✝¹ : F
hx : (fst✝¹, snd✝¹) ∈ f.graph
fst✝ : E
snd✝ : F
hy : (fst✝, snd✝) ∈ f.graph
hxy : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
⊢ (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2

Proof state:
case mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
fst✝¹ : E
snd✝¹ : F
hx : (fst✝¹, snd✝¹) ∈ f.graph
fst✝ : E
snd✝ : F
hy : (fst✝, snd✝) ∈ f.graph
hxy : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
⊢ (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2

Tactic:
exact f.mem_graph_snd_inj hx hy hxy

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
theorem map_subset_iff_subset_preimage {f : α ↪ β} {s : Finset α} {t : Finset β} :
    s.map f ⊆ t ↔ s ⊆ t.preimage f f.injective.injOn

Proof state:
α : Type u
β : Type v
f : α ↪ β
s : Finset α
t : Finset β
⊢ map f s ⊆ t ↔ s ⊆ t.preimage ⇑f ⋯

Tactic:
rw [map_eq_image, image_subset_iff_subset_preimage]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α ↪ β
s : Finset α
t : Finset β
⊢ map f s ⊆ t ↔ s ⊆ t.preimage ⇑f ⋯

Tactic:
classical rw [map_eq_image, image_subset_iff_subset_preimage]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/InjSurj.lean
theorem Function.Injective.isRightCancelMulZero
    [IsRightCancelMulZero M₀'] : IsRightCancelMulZero M₀ where
  mul_right_cancel_of_ne_zero Hne He

Proof state:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
this : f (a✝ * b✝) = f (c✝ * b✝)
⊢ a✝ = c✝

Tactic:
rw [mul, mul] at this

Result:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
this : f a✝ * f b✝ = f c✝ * f b✝
⊢ a✝ = c✝

Proof state:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
this : f a✝ * f b✝ = f c✝ * f b✝
⊢ a✝ = c✝

Tactic:
exact hf (mul_right_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)

Result:
no goals

Proof state:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
⊢ a✝ = c✝

Tactic:
have := congr_arg f He

Result:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
this : f (a✝ * b✝) = f (c✝ * b✝)
⊢ a✝ = c✝

Proof state:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
this : f a✝ * f b✝ = f c✝ * f b✝
Hfa : f b✝ = 0
⊢ f b✝ = f 0

Tactic:
rw [Hfa, zero]

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem symm_symm (γ : Path x y) : γ.symm.symm = γ

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ γ.symm.symm t = γ t

Tactic:
show γ (σ (σ t)) = γ t

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ γ (σ (σ t)) = γ t

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ γ (σ (σ t)) = γ t

Tactic:
rw [unitInterval.symm_symm]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.symm.symm = γ

Tactic:
ext t

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ γ.symm.symm t = γ t
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma sub_pow_expChar_pow_of_commute (h : Commute x y) :
    (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n

Proof state:
R : Type u_1
inst✝ : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n

Tactic:
simp [eq_sub_iff_add_eq, ← add_pow_expChar_pow_of_commute _ _ (h.sub_left rfl)]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_eq_one_of_finrank_eq_zero {𝕜 : Type*} [Field 𝕜] {M : Type*} [AddCommGroup M]
    [Module 𝕜 M] (h : Module.finrank 𝕜 M = 0) (f : M →ₗ[𝕜] M) :
    LinearMap.det (f : M →ₗ[𝕜] M) = 1

Proof state:
𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : Module.finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
⊢ ∀ (s : Finset M) (b : Basis { x // x ∈ s } 𝕜 M), (fun t => t = 1) ((toMatrix b b) f).det

Tactic:
intro s b

Result:
𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : Module.finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis { x // x ∈ s } 𝕜 M
⊢ ((toMatrix b b) f).det = 1

Proof state:
𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : Module.finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis { x // x ∈ s } 𝕜 M
⊢ ((toMatrix b b) f).det = 1

Tactic:
have : IsEmpty s := by
  rw [← Fintype.card_eq_zero_iff]
  exact (Module.finrank_eq_card_basis b).symm.trans h

Result:
𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : Module.finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis { x // x ∈ s } 𝕜 M
this : IsEmpty { x // x ∈ s }
⊢ ((toMatrix b b) f).det = 1

Proof state:
𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : Module.finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis { x // x ∈ s } 𝕜 M
this : IsEmpty { x // x ∈ s }
⊢ ((toMatrix b b) f).det = 1

Tactic:
exact Matrix.det_isEmpty

Result:
no goals

Proof state:
𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : Module.finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis { x // x ∈ s } 𝕜 M
⊢ IsEmpty { x // x ∈ s }

Tactic:
rw [← Fintype.card_eq_zero_iff]

Result:
𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : Module.finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis { x // x ∈ s } 𝕜 M
⊢ Fintype.card { x // x ∈ s } = 0

Proof state:
𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : Module.finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
⊢ LinearMap.det f = 1

Tactic:
classical
  refine @LinearMap.det_cases M _ 𝕜 _ _ _ (fun t => t = 1) f ?_ rfl
  intro s b
  have : IsEmpty s := by
    rw [← Fintype.card_eq_zero_iff]
    exact (Module.finrank_eq_card_basis b).symm.trans h
  exact Matrix.det_isEmpty

Result:
no goals

Proof state:
𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : Module.finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis { x // x ∈ s } 𝕜 M
⊢ Fintype.card { x // x ∈ s } = 0

Tactic:
exact (Module.finrank_eq_card_basis b).symm.trans h

Result:
no goals

Proof state:
𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : Module.finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
⊢ LinearMap.det f = 1

Tactic:
refine @LinearMap.det_cases M _ 𝕜 _ _ _ (fun t => t = 1) f ?_ rfl

Result:
𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : Module.finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
⊢ ∀ (s : Finset M) (b : Basis { x // x ∈ s } 𝕜 M), (fun t => t = 1) ((toMatrix b b) f).det
-- Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
lemma quasiIso_of_epi_of_isIso_of_mono (φ : S₁ ⟶ S₂) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] :
    QuasiIso φ

Proof state:
C : Type u_2
inst✝⁶ : Category.{u_1, u_2} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ QuasiIso φ

Tactic:
rw [((LeftHomologyMapData.ofEpiOfIsIsoOfMono φ) S₁.leftHomologyData).quasiIso_iff]

Result:
C : Type u_2
inst✝⁶ : Category.{u_1, u_2} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (LeftHomologyMapData.ofEpiOfIsIsoOfMono φ S₁.leftHomologyData).φH

Proof state:
C : Type u_2
inst✝⁶ : Category.{u_1, u_2} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (𝟙 S₁.leftHomologyData.H)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_2
inst✝⁶ : Category.{u_1, u_2} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (LeftHomologyMapData.ofEpiOfIsIsoOfMono φ S₁.leftHomologyData).φH

Tactic:
dsimp

Result:
C : Type u_2
inst✝⁶ : Category.{u_1, u_2} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (𝟙 S₁.leftHomologyData.H)
-- Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.lean
@[to_additive] lemma exists_one_lt_mul_of_lt' [MulLeftReflectLT α] (h : a < b) :
    ∃ c, 1 < c ∧ a * c = b

Proof state:
case intro
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a : α
inst✝ : MulLeftReflectLT α
c : α
h : a < a * c
⊢ ∃ c_1, 1 < c_1 ∧ a * c_1 = a * c

Tactic:
exact ⟨c, one_lt_of_lt_mul_right h, rfl⟩

Result:
no goals

Proof state:
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a b : α
inst✝ : MulLeftReflectLT α
h : a < b
⊢ ∃ c, 1 < c ∧ a * c = b

Tactic:
obtain ⟨c, rfl⟩ := exists_mul_of_le h.le

Result:
case intro
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a : α
inst✝ : MulLeftReflectLT α
c : α
h : a < a * c
⊢ ∃ c_1, 1 < c_1 ∧ a * c_1 = a * c
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofLE_mk_le_mk_of_comm {B A₁ A₂ : C} {f₁ : A₁ ⟶ B} {f₂ : A₂ ⟶ B} [Mono f₁] [Mono f₂]
    (g : A₁ ⟶ A₂) (w : g ≫ f₂ = f₁) :
    ofLE _ _ (mk_le_mk_of_comm g w) = (underlyingIso _).hom ≫ g ≫ (underlyingIso _).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f₁ : A₁ ⟶ B
f₂ : A₂ ⟶ B
inst✝¹ : Mono f₁
inst✝ : Mono f₂
g : A₁ ⟶ A₂
w : g ≫ f₂ = f₁
⊢ (mk f₁).ofLE (mk f₂) ⋯ = (underlyingIso f₁).hom ≫ g ≫ (underlyingIso f₂).inv

Tactic:
ext

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f₁ : A₁ ⟶ B
f₂ : A₂ ⟶ B
inst✝¹ : Mono f₁
inst✝ : Mono f₂
g : A₁ ⟶ A₂
w : g ≫ f₂ = f₁
⊢ (mk f₁).ofLE (mk f₂) ⋯ ≫ (mk f₂).arrow = ((underlyingIso f₁).hom ≫ g ≫ (underlyingIso f₂).inv) ≫ (mk f₂).arrow

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f₁ : A₁ ⟶ B
f₂ : A₂ ⟶ B
inst✝¹ : Mono f₁
inst✝ : Mono f₂
g : A₁ ⟶ A₂
w : g ≫ f₂ = f₁
⊢ (mk f₁).ofLE (mk f₂) ⋯ ≫ (mk f₂).arrow = ((underlyingIso f₁).hom ≫ g ≫ (underlyingIso f₂).inv) ≫ (mk f₂).arrow

Tactic:
simp [w]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorPower/Basic.lean
theorem algebraMap₀_mul_algebraMap₀ (r s : R) :
    cast R M (add_zero _) (algebraMap₀ r ₜ* algebraMap₀ s) = algebraMap₀ (r * s)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul (algebraMap₀ r) (algebraMap₀ s)) = r • algebraMap₀ s

Tactic:
exact algebraMap₀_mul r (@algebraMap₀ R M _ _ _ s)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul (algebraMap₀ r) (algebraMap₀ s)) = algebraMap₀ (r * s)

Tactic:
rw [← smul_eq_mul, LinearEquiv.map_smul]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul (algebraMap₀ r) (algebraMap₀ s)) = r • algebraMap₀ s
-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem HasStrictFDerivAt.hasStrictDerivAt_norm_smul_pos
    (ht : 0 < t) (h : HasStrictFDerivAt (‖·‖) f x) :
    HasStrictFDerivAt (‖·‖) f (t • x)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : 0 < t
h : HasStrictFDerivAt (fun x => ‖x‖) f x
⊢ HasStrictFDerivAt (fun x => ‖x‖) f (t • x)

Tactic:
simpa [ht] using h.hasStrictFDerivAt_norm_smul ht.ne'

Result:
no goals
-- Mathlib/Analysis/Calculus/FirstDerivativeTest.lean
/-- The First-Derivative Test from calculus, maxima version,
expressed in terms of left and right filters. -/
lemma isLocalMax_of_deriv' {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b)
    (hd₀ : ∀ᶠ x in 𝓝[<] b, DifferentiableAt ℝ f x) (hd₁ : ∀ᶠ x in 𝓝[>] b, DifferentiableAt ℝ f x)
    (h₀ : ∀ᶠ x in 𝓝[<] b, 0 ≤ deriv f x) (h₁ : ∀ᶠ x in 𝓝[>] b, deriv f x ≤ 0) :
    IsLocalMax f b

Proof state:
case intro.intro
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, 0 ≤ deriv f x
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≤ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ 0 ≤ deriv f x
c : ℝ
hc : b < c ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo b c → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0
⊢ IsLocalMax f b

Tactic:
exact isLocalMax_of_deriv_Ioo ha.1 hc.1 h
  (fun _ hx => (ha.2 hx).1.differentiableWithinAt)
  (fun _ hx => (hc.2 hx).1.differentiableWithinAt)
  (fun _ hx => (ha.2 hx).2) (fun x hx => (hc.2 hx).2)

Result:
no goals

Proof state:
case intro
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, 0 ≤ deriv f x
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≤ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ 0 ≤ deriv f x
⊢ IsLocalMax f b

Tactic:
obtain ⟨c, hc⟩ := (nhdsGT_basis b).eventually_iff.mp <| hd₁.and h₁

Result:
case intro.intro
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, 0 ≤ deriv f x
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≤ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ 0 ≤ deriv f x
c : ℝ
hc : b < c ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo b c → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0
⊢ IsLocalMax f b

Proof state:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, 0 ≤ deriv f x
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≤ 0
⊢ IsLocalMax f b

Tactic:
obtain ⟨a, ha⟩ := (nhdsLT_basis b).eventually_iff.mp <| hd₀.and h₀

Result:
case intro
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, 0 ≤ deriv f x
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≤ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ 0 ≤ deriv f x
⊢ IsLocalMax f b
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem HasProd.abs (hfx : HasProd f x) : HasProd (|f ·|) |x|

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : LinearOrderedCommRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : ι → α
x : α
hfx : HasProd f x
⊢ HasProd (fun x => |f x|) |x|

Tactic:
simpa only [HasProd, ← abs_prod] using hfx.abs

Result:
no goals
-- Mathlib/Data/Multiset/Lattice.lean
theorem sup_add (s₁ s₂ : Multiset α) : (s₁ + s₂).sup = s₁.sup ⊔ s₂.sup :=
  Eq.trans (by simp [sup]) (fold_add _ _ _ _ _)

Proof state:
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s₁ s₂ : Multiset α
⊢ (s₁ + s₂).sup = fold (fun x1 x2 => x1 ⊔ x2) (⊥ ⊔ ⊥) (s₁ + s₂)

Tactic:
simp [sup]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem spectralRadius_lt_of_forall_lt_of_nonempty [ProperSpace 𝕜] {a : A} (ha : (σ a).Nonempty)
    {r : ℝ≥0} (hr : ∀ k ∈ σ a, ‖k‖₊ < r) : spectralRadius 𝕜 a < r :=
  sSup_image.symm.trans_lt <| ((spectrum.isCompact a).sSup_lt_iff_of_continuous ha
    continuous_enorm.continuousOn (r : ℝ≥0∞)).mpr (by simpa using hr)

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
a : A
ha : (σ a).Nonempty
r : ℝ≥0
hr : ∀ k ∈ σ a, ‖k‖₊ < r
⊢ ∀ x ∈ σ a, ‖x‖ₑ < ↑r

Tactic:
simpa using hr

Result:
no goals