harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem aestronglyMeasurable_condExpL1 {f : α → F'} :
    AEStronglyMeasurable[m] (condExpL1 hm μ f) μ

Proof state:
case pos
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hf : Integrable f μ
⊢ AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ

Tactic:
rw [condExpL1_eq hf]

Result:
case pos
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hf : Integrable f μ
⊢ AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (Integrable.toL1 f hf))) μ

Proof state:
case neg
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hf : ¬Integrable f μ
⊢ AEStronglyMeasurable (↑↑0) μ

Tactic:
exact stronglyMeasurable_zero.aestronglyMeasurable.congr (coeFn_zero ..).symm

Result:
no goals

Proof state:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
⊢ AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hf : Integrable f μ
⊢ AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ

case neg
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hf : ¬Integrable f μ
⊢ AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ

Proof state:
case neg
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hf : ¬Integrable f μ
⊢ AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ

Tactic:
rw [condExpL1_undef hf]

Result:
case neg
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hf : ¬Integrable f μ
⊢ AEStronglyMeasurable (↑↑0) μ

Proof state:
case pos
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hf : Integrable f μ
⊢ AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (Integrable.toL1 f hf))) μ

Tactic:
exact aestronglyMeasurable_condExpL1CLM _

Result:
no goals
-- Mathlib/Algebra/ZeroOne/Lemmas.lean
@[to_additive dite_nonneg]
lemma one_le_dite [LE α] (ha : ∀ h, 1 ≤ a h) (hb : ∀ h, 1 ≤ b h) : 1 ≤ dite p a b

Proof state:
case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), 1 ≤ a h
hb : ∀ (h : ¬p), 1 ≤ b h
h✝ : p
⊢ 1 ≤ a h✝

case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), 1 ≤ a h
hb : ∀ (h : ¬p), 1 ≤ b h
h✝ : ¬p
⊢ 1 ≤ b h✝

Tactic:
exacts [ha ‹_›, hb ‹_›]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), 1 ≤ a h
hb : ∀ (h : ¬p), 1 ≤ b h
⊢ 1 ≤ dite p a b

Tactic:
split

Result:
case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), 1 ≤ a h
hb : ∀ (h : ¬p), 1 ≤ b h
h✝ : p
⊢ 1 ≤ a h✝

case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LE α
ha : ∀ (h : p), 1 ≤ a h
hb : ∀ (h : ¬p), 1 ≤ b h
h✝ : ¬p
⊢ 1 ≤ b h✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem attach_reverse (xs : List α) :
    xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩

Proof state:
case h
α : Type u_1
xs : List α
⊢ ∀ (a : α), a ∈ xs.reverse → ∀ (h₁ : a ∈ xs.reverse) (h₂ : a ∈ xs), ⟨a, h₁⟩ = ⟨a, ⋯⟩

Tactic:
intros

Result:
case h
α : Type u_1
xs : List α
a✝¹ : α
a✝ h₁✝ : a✝¹ ∈ xs.reverse
h₂✝ : a✝¹ ∈ xs
⊢ ⟨a✝¹, h₁✝⟩ = ⟨a✝¹, ⋯⟩

Proof state:
α : Type u_1
xs : List α
⊢ pmap Subtype.mk xs.reverse ⋯ = pmap (fun a h => ⟨a, ⋯⟩) xs.reverse ⋯

Tactic:
apply pmap_congr_left

Result:
case h
α : Type u_1
xs : List α
⊢ ∀ (a : α), a ∈ xs.reverse → ∀ (h₁ : a ∈ xs.reverse) (h₂ : a ∈ xs), ⟨a, h₁⟩ = ⟨a, ⋯⟩

Proof state:
α : Type ?u.78578
xs : List α
x✝ : { x // x ∈ xs }
x : α
h : x ∈ xs
⊢ x ∈ xs.reverse

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
xs : List α
⊢ xs.reverse.attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.attach.reverse

Tactic:
simp only [attach, attachWith, reverse_pmap, map_pmap]

Result:
α : Type u_1
xs : List α
⊢ pmap Subtype.mk xs.reverse ⋯ = pmap (fun a h => ⟨a, ⋯⟩) xs.reverse ⋯

Proof state:
case h
α : Type u_1
xs : List α
a✝¹ : α
a✝ h₁✝ : a✝¹ ∈ xs.reverse
h₂✝ : a✝¹ ∈ xs
⊢ ⟨a✝¹, h₁✝⟩ = ⟨a✝¹, ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
theorem Sigma.ι_reindex_inv (b : β) :
    Sigma.ι f (ε b) ≫ (Sigma.reindex ε f).inv = Sigma.ι (f ∘ ε) b

Proof state:
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ⇑ε)
b : β
⊢ ι f (ε b) ≫ (reindex ε f).inv = ι (f ∘ ⇑ε) b

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/Data/Analysis/Topology.lean
theorem is_basis [T : TopologicalSpace α] (F : Realizer α) :
    TopologicalSpace.IsTopologicalBasis (Set.range F.F.f)

Proof state:
α : Type u_1
T : TopologicalSpace α
F : Realizer α
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)

Tactic:
have := toTopsp_isTopologicalBasis F.F

Result:
α : Type u_1
T : TopologicalSpace α
F : Realizer α
this : TopologicalSpace.IsTopologicalBasis (range F.F.f)
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)

Proof state:
α : Type u_1
T : TopologicalSpace α
F : Realizer α
this : TopologicalSpace.IsTopologicalBasis (range F.F.f)
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)

Tactic:
rwa [F.eq] at this

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem invOf_fromBlocks₂₂_eq (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α)
    (D : Matrix n n α) [Invertible D] [Invertible (A - B * ⅟ D * C)]
    [Invertible (fromBlocks A B C D)] :
    ⅟ (fromBlocks A B C D) =
      fromBlocks (⅟ (A - B * ⅟ D * C)) (-(⅟ (A - B * ⅟ D * C) * B * ⅟ D))
        (-(⅟ D * C * ⅟ (A - B * ⅟ D * C))) (⅟ D + ⅟ D * C * ⅟ (A - B * ⅟ D * C) * B * ⅟ D)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible D
inst✝¹ : Invertible (A - B * ⅟D * C)
inst✝ : Invertible (fromBlocks A B C D)
this : Invertible (fromBlocks A B C D) := A.fromBlocks₂₂Invertible B C D
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
      (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D)

Tactic:
convert (rfl : ⅟ (fromBlocks A B C D) = _)

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible D
inst✝¹ : Invertible (A - B * ⅟D * C)
inst✝ : Invertible (fromBlocks A B C D)
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
      (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D)

Tactic:
letI := fromBlocks₂₂Invertible A B C D

Result:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible D
inst✝¹ : Invertible (A - B * ⅟D * C)
inst✝ : Invertible (fromBlocks A B C D)
this : Invertible (fromBlocks A B C D) := A.fromBlocks₂₂Invertible B C D
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
      (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D)
-- Mathlib/Topology/Maps/Basic.lean
theorem of_comp_iff (f : X → Y) (hg : IsOpenEmbedding g) :
    IsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding f

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
hg : IsOpenEmbedding g
⊢ IsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding f

Tactic:
simp only [isOpenEmbedding_iff_continuous_injective_isOpenMap, ← hg.isOpenMap_iff, ←
  hg.1.continuous_iff, hg.injective.of_comp_iff]

Result:
no goals
-- Mathlib/Topology/Homotopy/HSpaces.lean
theorem qRight_zero_left (θ : I) : qRight (0, θ) = 0 :=
  Set.projIcc_of_le_left _ <| by simp only [coe_zero, mul_zero, zero_div, le_refl]

Proof state:
θ : ↑I
⊢ 2 * ↑(0, θ).1 / (1 + ↑(0, θ).2) ≤ 0

Tactic:
simp only [coe_zero, mul_zero, zero_div, le_refl]

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem to_part {n f} (pf : @Partrec' n f) : _root_.Partrec f

Proof state:
case rfind
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
hf : _root_.Partrec ↑f✝
this✝ : _root_.Partrec fun a => ↑f✝ (a.2 ::ᵥ a.1)
this : Partrec₂ fun a => ↑fun b => decide ((fun a => id a = 0) (f✝ ((a, b).2 ::ᵥ (a, b).1)))
⊢ _root_.Partrec fun v => Nat.rfind fun n => Part.some (decide (f✝ (n ::ᵥ v) = 0))

Tactic:
exact _root_.Partrec.rfind this

Result:
no goals

Proof state:
case prim
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
hf : Primrec' f✝
⊢ _root_.Partrec ↑f✝

Tactic:
exact hf.to_prim.to_comp

Result:
no goals

Proof state:
n : ℕ
f : List.Vector ℕ n →. ℕ
pf : Partrec' f
⊢ _root_.Partrec f

Tactic:
induction pf with
| prim hf => exact hf.to_prim.to_comp
| comp _ _ _ hf hg => exact (Partrec.vector_mOfFn hg).bind (hf.comp snd)
| rfind _ hf =>
  have := hf.comp (vector_cons.comp snd fst)
  have :=
    ((Primrec.eq.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp
      this).to₂.partrec₂
  exact _root_.Partrec.rfind this

Result:
no goals

Proof state:
case rfind
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
hf : _root_.Partrec ↑f✝
⊢ _root_.Partrec fun v => Nat.rfind fun n => Part.some (decide (f✝ (n ::ᵥ v) = 0))

Tactic:
have := hf.comp (vector_cons.comp snd fst)

Result:
case rfind
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
hf : _root_.Partrec ↑f✝
this : _root_.Partrec fun a => ↑f✝ (a.2 ::ᵥ a.1)
⊢ _root_.Partrec fun v => Nat.rfind fun n => Part.some (decide (f✝ (n ::ᵥ v) = 0))

Proof state:
case comp
n : ℕ
f : List.Vector ℕ n →. ℕ
m✝ n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
g✝ : Fin n✝ → List.Vector ℕ m✝ →. ℕ
a✝¹ : Partrec' f✝
a✝ : ∀ (i : Fin n✝), Partrec' (g✝ i)
hf : _root_.Partrec f✝
hg : ∀ (i : Fin n✝), _root_.Partrec (g✝ i)
⊢ _root_.Partrec fun v => (mOfFn fun i => g✝ i v) >>= f✝

Tactic:
exact (Partrec.vector_mOfFn hg).bind (hf.comp snd)

Result:
no goals

Proof state:
case rfind
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
hf : _root_.Partrec ↑f✝
this : _root_.Partrec fun a => ↑f✝ (a.2 ::ᵥ a.1)
⊢ _root_.Partrec fun v => Nat.rfind fun n => Part.some (decide (f✝ (n ::ᵥ v) = 0))

Tactic:
have :=
  ((Primrec.eq.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp
    this).to₂.partrec₂

Result:
case rfind
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
hf : _root_.Partrec ↑f✝
this✝ : _root_.Partrec fun a => ↑f✝ (a.2 ::ᵥ a.1)
this : Partrec₂ fun a => ↑fun b => decide ((fun a => id a = 0) (f✝ ((a, b).2 ::ᵥ (a, b).1)))
⊢ _root_.Partrec fun v => Nat.rfind fun n => Part.some (decide (f✝ (n ::ᵥ v) = 0))
-- Mathlib/Order/Disjointed.lean
lemma disjointed_of_isMin (f : ι → α) {i : ι} (hn : IsMin i) :
    disjointed f i = f i

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hn : IsMin i
⊢ Iio i = ∅

Tactic:
rwa [← Finset.coe_eq_empty, coe_Iio, Set.Iio_eq_empty_iff]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hn : IsMin i
⊢ disjointed f i = f i

Tactic:
have : Iio i = ∅ := by rwa [← Finset.coe_eq_empty, coe_Iio, Set.Iio_eq_empty_iff]

Result:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hn : IsMin i
this : Iio i = ∅
⊢ disjointed f i = f i

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hn : IsMin i
this : Iio i = ∅
⊢ disjointed f i = f i

Tactic:
simp only [disjointed_apply, this, sup_empty, sdiff_bot]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem basis_singleton_iff {R M : Type*} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M]
    [NoZeroSMulDivisors R M] (ι : Type*) [Unique ι] :
    Nonempty (Basis ι R M) ↔ ∃ x ≠ 0, ∀ y : M, ∃ r : R, r • x = y

Proof state:
case mpr.intro.intro.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ (fun c => c • x)
      (((fun y => single default ⋯.choose) ({ toFun := fun f => f default • x, map_add' := ⋯, map_smul' := ⋯ }.toFun f))
        default) =
    (fun c => c • x) (f default)

Tactic:
simp only [Finsupp.single_eq_same]

Result:
case mpr.intro.intro.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ⋯.choose • x = f default • x

Proof state:
case mpr.intro.intro.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ((fun y => single default ⋯.choose) ({ toFun := fun f => f default • x, map_add' := ⋯, map_smul' := ⋯ }.toFun f))
      default =
    f default

Tactic:
refine smul_left_injective _ nz ?_

Result:
case mpr.intro.intro.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ (fun c => c • x)
      (((fun y => single default ⋯.choose) ({ toFun := fun f => f default • x, map_add' := ⋯, map_smul' := ⋯ }.toFun f))
        default) =
    (fun c => c • x) (f default)

Proof state:
case mp.intro
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
b : Basis ι R M
⊢ ∀ (y : M), ∃ r, r • b default = y

Tactic:
simpa [span_singleton_eq_top_iff, Set.range_unique] using b.span_eq

Result:
no goals

Proof state:
case mpr.intro.intro.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ ⋯.choose • x = y

Tactic:
exact (w y).choose_spec

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem conjugateEquiv_adjunction_id_symm {L R : C ⥤ C} (adj : L ⊣ R) (α : R ⟶ 𝟭 C) (c : C) :
    ((conjugateEquiv adj Adjunction.id).symm α).app c = adj.unit.app c ≫ α.app (L.obj c)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
L R : C ⥤ C
adj : L ⊣ R
α : R ⟶ 𝟭 C
c : C
⊢ ((conjugateEquiv adj Adjunction.id).symm α).app c = adj.unit.app c ≫ α.app (L.obj c)

Tactic:
simp [conjugateEquiv, mateEquiv, Adjunction.id]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Defs.lean
theorem three_add_one_eq_four [AddMonoidWithOne R] : 3 + 1 = (4 : R)

Proof state:
case h
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 + 1 + 1 = 4

Tactic:
decide

Result:
no goals

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 3 + 1 = 4

Tactic:
rw [← two_add_one_eq_three, ← one_add_one_eq_two, ← Nat.cast_one,
  ← Nat.cast_add, ← Nat.cast_add, ← Nat.cast_add]

Result:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1 + 1 + 1) = 4

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1 + 1 + 1) = 4

Tactic:
apply congrArg

Result:
case h
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 + 1 + 1 = 4
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
lemma isUnit_charpolyRev_of_isNilpotent (hM : IsNilpotent M) :
    IsUnit M.charpolyRev

Proof state:
case h.e'_4
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 = 1 - (X • M.map ⇑C) ^ k

Tactic:
rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_zero]

Result:
no goals

Proof state:
case intro
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : 1 - X • M.map ⇑C ∣ 1
⊢ IsUnit M.charpolyRev

Tactic:
apply isUnit_of_dvd_one

Result:
case intro.h
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : 1 - X • M.map ⇑C ∣ 1
⊢ M.charpolyRev ∣ 1

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
⊢ IsUnit M.charpolyRev

Tactic:
obtain ⟨k, hk⟩ := hM

Result:
case intro
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ IsUnit M.charpolyRev

Proof state:
case intro.h
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : 1 - X • M.map ⇑C ∣ 1
⊢ M.charpolyRev ∣ 1

Tactic:
rw [← det_one (R := R[X]) (n := n)]

Result:
case intro.h
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : 1 - X • M.map ⇑C ∣ 1
⊢ M.charpolyRev ∣ det 1

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 - X • M.map ⇑C ∣ 1

Tactic:
convert one_sub_dvd_one_sub_pow ((X : R[X]) • M.map C) k

Result:
case h.e'_4
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 = 1 - (X • M.map ⇑C) ^ k

Proof state:
case intro
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ IsUnit M.charpolyRev

Tactic:
replace hk : 1 - (X : R[X]) • M.map C ∣ 1 := by
  convert one_sub_dvd_one_sub_pow ((X : R[X]) • M.map C) k
  rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_zero]

Result:
case intro
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : 1 - X • M.map ⇑C ∣ 1
⊢ IsUnit M.charpolyRev

Proof state:
case intro.h
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : 1 - X • M.map ⇑C ∣ 1
⊢ M.charpolyRev ∣ det 1

Tactic:
exact map_dvd detMonoidHom hk

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem norm_pow_mul_le_seminorm (f : 𝓢(E, F)) (k : ℕ) (x₀ : E) :
    ‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
k : ℕ
x₀ : E
this : ‖x₀‖ ^ k * ‖iteratedFDeriv ℝ 0 (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f
⊢ ‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f

Tactic:
rwa [norm_iteratedFDeriv_zero] at this

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
k : ℕ
x₀ : E
⊢ ‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f

Tactic:
have := SchwartzMap.le_seminorm 𝕜 k 0 f x₀

Result:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
k : ℕ
x₀ : E
this : ‖x₀‖ ^ k * ‖iteratedFDeriv ℝ 0 (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f
⊢ ‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f
-- Mathlib/RingTheory/TensorProduct/Basic.lean
lemma liftBaseChange_comp {P} [AddCommMonoid P] [Module A P] [Module R P] [IsScalarTower R A P]
    (l : M →ₗ[R] N) (l' : N →ₗ[A] P) :
      l' ∘ₗ l.liftBaseChange A = (l'.restrictScalars R ∘ₗ l).liftBaseChange A

Proof state:
case a.h.h
R : Type u_3
M : Type u_4
N : Type u_5
A : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module A N
inst✝⁴ : IsScalarTower R A N
P : Type u_1
inst✝³ : AddCommMonoid P
inst✝² : Module A P
inst✝¹ : Module R P
inst✝ : IsScalarTower R A P
l : M →ₗ[R] N
l' : N →ₗ[A] P
x✝ : M
⊢ ((AlgebraTensorModule.curry (l' ∘ₗ liftBaseChange A l)) 1) x✝ =
    ((AlgebraTensorModule.curry (liftBaseChange A (↑R l' ∘ₗ l))) 1) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
A : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module A N
inst✝⁴ : IsScalarTower R A N
P : Type u_1
inst✝³ : AddCommMonoid P
inst✝² : Module A P
inst✝¹ : Module R P
inst✝ : IsScalarTower R A P
l : M →ₗ[R] N
l' : N →ₗ[A] P
⊢ l' ∘ₗ liftBaseChange A l = liftBaseChange A (↑R l' ∘ₗ l)

Tactic:
ext

Result:
case a.h.h
R : Type u_3
M : Type u_4
N : Type u_5
A : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module A N
inst✝⁴ : IsScalarTower R A N
P : Type u_1
inst✝³ : AddCommMonoid P
inst✝² : Module A P
inst✝¹ : Module R P
inst✝ : IsScalarTower R A P
l : M →ₗ[R] N
l' : N →ₗ[A] P
x✝ : M
⊢ ((AlgebraTensorModule.curry (l' ∘ₗ liftBaseChange A l)) 1) x✝ =
    ((AlgebraTensorModule.curry (liftBaseChange A (↑R l' ∘ₗ l))) 1) x✝