harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem mapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → m β} {g : α → m β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.mapM f = l.unattach.mapM g

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → m β
g : α → m β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ mapM' f l = mapM' g l.unattach

Tactic:
induction l with
| nil => simp
| cons a l ih => simp [ih, hf]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → m β
g : α → m β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ mapM f l = mapM g (map (fun x => x.val) l)

Tactic:
simp [← List.mapM'_eq_mapM]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → m β
g : α → m β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ mapM' f l = mapM' g l.unattach

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → m β
g : α → m β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : mapM' f l = mapM' g l.unattach
⊢ mapM' f (a :: l) = mapM' g (a :: l).unattach

Tactic:
simp [ih, hf]

Result:
no goals

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → m β
g : α → m β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ mapM' f [] = mapM' g [].unattach

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → m β
g : α → m β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ mapM f l = mapM g l.unattach

Tactic:
unfold unattach

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → m β
g : α → m β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ mapM f l = mapM g (map (fun x => x.val) l)
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem minkowskiBound_lt_top : minkowskiBound K I < ⊤

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ 2 ^ finrank ℝ (mixedSpace K) < ⊤

Tactic:
exact ENNReal.pow_lt_top (lt_top_iff_ne_top.mpr ENNReal.ofNat_ne_top) _

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ minkowskiBound K I < ⊤

Tactic:
refine ENNReal.mul_lt_top ?_ ?_

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) < ⊤

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ 2 ^ finrank ℝ (mixedSpace K) < ⊤

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) < ⊤

Tactic:
exact (fundamentalDomain_isBounded _).measure_lt_top

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Exact.lean
theorem preservesMonomorphisms_of_map_exact : L.PreservesMonomorphisms where
  preserves f hf

Proof state:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Mono f
⊢ (ShortComplex.mk 0 (L.map f) ⋯).Exact

Tactic:
refine ShortComplex.exact_of_iso ?_ (hL _ (((tfae_mono f 0).out 0 2).mp hf))

Result:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Mono f
⊢ (ShortComplex.mk 0 f ⋯).map L ≅ ShortComplex.mk 0 (L.map f) ⋯

Proof state:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Mono (L.map f)

Tactic:
apply ((Abelian.tfae_mono (L.map f) (L.obj 0)).out 2 0).mp

Result:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Mono f
⊢ (ShortComplex.mk 0 (L.map f) ⋯).Exact

Proof state:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Mono f
⊢ (ShortComplex.mk 0 f ⋯).map L ≅ ShortComplex.mk 0 (L.map f) ⋯

Tactic:
exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
theorem Integrable.uniformIntegrable_condExp {ι : Type*} [IsFiniteMeasure μ] {g : α → ℝ}
    (hint : Integrable g μ) {ℱ : ι → MeasurableSpace α} (hℱ : ∀ i, ℱ i ≤ m0) :
    UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ

Proof state:
case neg.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
this : ∀ (n : ι), μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ
n : ι
⊢ eLpNorm ({x | C ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator (μ[g|ℱ n])) 1 μ ≤ eLpNorm ({x | C ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator g) 1 μ

Tactic:
have hmeasℱ : MeasurableSet[ℱ n] {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} :=
  @measurableSet_le _ _ _ _ _ (ℱ n) _ _ _ _ _ measurable_const
    (@Measurable.nnnorm _ _ _ _ _ (ℱ n) _ stronglyMeasurable_condExp.measurable)

Result:
case neg.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = ⟨δ, ⋯⟩⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
this : ∀ (n : ι), μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ
n : ι
hmeasℱ : MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
⊢ eLpNorm ({x | C ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator (μ[g|ℱ n])) 1 μ ≤ eLpNorm ({x | C ≤ ‖(μ[g|ℱ n]) x‖₊}.indicator g) 1 μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
⊢ UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ

Tactic:
have hmeas : ∀ n, ∀ C, MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} := fun n C =>
  measurableSet_le measurable_const (stronglyMeasurable_condExp.mono (hℱ n)).measurable.nnnorm

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
⊢ UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.drop m).take n

Proof state:
α : Type u_1
l : List α
m n : Nat
⊢ take (m + n) l = take m l ++ take n (drop m l)

Tactic:
suffices take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l) by
  rw [take_append_drop] at this
  assumption

Result:
α : Type u_1
l : List α
m n : Nat
⊢ take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l)

Proof state:
α : Type u_1
l : List α
m n : Nat
this : take (m + n) l = take m l ++ take n (drop m l)
⊢ take (m + n) l = take m l ++ take n (drop m l)

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
l : List α
m n : Nat
⊢ (take m l).length ≤ m + n

Tactic:
apply Nat.le_trans (m := m)

Result:
case a
α : Type u_1
l : List α
m n : Nat
⊢ (take m l).length ≤ m

case a
α : Type u_1
l : List α
m n : Nat
⊢ m ≤ m + n

Proof state:
α : Type u_1
l : List α
m n : Nat
⊢ take (m + n - (take m l).length) (drop m l) = take n (drop m l)

Tactic:
simp only [take_eq_take, length_take, length_drop]

Result:
α : Type u_1
l : List α
m n : Nat
⊢ min (m + n - min m l.length) (l.length - m) = min n (l.length - m)

Proof state:
case a
α : Type u_1
l : List α
m n : Nat
⊢ m ≤ m + n

Tactic:
apply Nat.le_add_right

Result:
no goals

Proof state:
case a
α : Type u_1
l : List α
m n : Nat
⊢ (take m l).length ≤ m

Tactic:
apply length_take_le

Result:
no goals

Proof state:
α : Type u_1
l : List α
m n : Nat
⊢ min (m + n - min m l.length) (l.length - m) = min n (l.length - m)

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
m n : Nat
this : take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l)
⊢ take (m + n) l = take m l ++ take n (drop m l)

Tactic:
rw [take_append_drop] at this

Result:
α : Type u_1
l : List α
m n : Nat
this : take (m + n) l = take m l ++ take n (drop m l)
⊢ take (m + n) l = take m l ++ take n (drop m l)

Proof state:
α : Type u_1
l : List α
m n : Nat
⊢ take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l)

Tactic:
rw [take_append_eq_append_take, take_of_length_le, append_right_inj]

Result:
α : Type u_1
l : List α
m n : Nat
⊢ take (m + n - (take m l).length) (drop m l) = take n (drop m l)

α : Type u_1
l : List α
m n : Nat
⊢ (take m l).length ≤ m + n
-- Mathlib/RingTheory/Polynomial/HilbertPoly.lean
theorem natDegree_hilbertPoly_of_ne_zero
    {p : F[X]} {d : ℕ} (hh : hilbertPoly p d ≠ 0) :
    (hilbertPoly p d).natDegree = d - p.rootMultiplicity 1 - 1

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : hilbertPoly 0 d ≠ 0
h : p = 0
⊢ False

Tactic:
exact hh (hilbertPoly_zero_left d)

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
⊢ p ≠ 0

Tactic:
intro h

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
h : p = 0
⊢ False

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
have hp : p ≠ 0 := by
  intro h
  rw [h] at hh
  exact hh (hilbertPoly_zero_left d)

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
⊢ rootMultiplicity 1 p < d

Tactic:
by_contra h

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
h : ¬rootMultiplicity 1 p < d
⊢ False

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
h : ¬rootMultiplicity 1 p < d
⊢ False

Tactic:
exact hh (hilbertPoly_eq_zero_of_le_rootMultiplicity_one <| not_lt.1 h)

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
have hpd : p.rootMultiplicity 1 < d := by
  by_contra h
  exact hh (hilbertPoly_eq_zero_of_le_rootMultiplicity_one <| not_lt.1 h)

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
exact natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt hp hpd

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
h : p = 0
⊢ False

Tactic:
rw [h] at hh

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : hilbertPoly 0 d ≠ 0
h : p = 0
⊢ False
-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
/-- Any property of scheme morphisms induced by a property of ring homomorphisms is stable
under composition with open immersions. -/
lemma respects_isOpenImmersion (hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource Q) :
    P.Respects @IsOpenImmersion where
  postcomp {X Y Z} i hi f hf

Proof state:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme} (i : Y ⟶ Z), IsOpenImmersion i → ∀ (f : X ⟶ Y), P f → IsAffine Z → P (f ≫ i)
hZ : ¬IsAffine Z
U : ↑Z.affineOpens
⊢ P ((f ≫ i) ∣_ ↑U)

Tactic:
rw [morphismRestrict_comp]

Result:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme} (i : Y ⟶ Z), IsOpenImmersion i → ∀ (f : X ⟶ Y), P f → IsAffine Z → P (f ≫ i)
hZ : ¬IsAffine Z
U : ↑Z.affineOpens
⊢ P (f ∣_ i ⁻¹ᵁ ↑U ≫ i ∣_ ↑U)

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
⊢ Set.range ⇑(ConcreteCategory.hom i.base) = Set.range ⇑(ConcreteCategory.hom (Scheme.Hom.opensRange i).ι.base)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
@[simp]
lemma map_ofHom (f : X ⟶ Y) (L : C ⥤ D) (hL : W.IsInvertedBy L) [W.ContainsIdentities] :
    (ofHom W f).map L hL = L.map f

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
f : X ⟶ Y
L : C ⥤ D
hL : W.IsInvertedBy L
inst✝ : W.ContainsIdentities
⊢ (ofHom W f).map L hL = L.map f

Tactic:
simp [map]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean
lemma quasiIsoAt_extendMap_iff :
    QuasiIsoAt (extendMap φ e) j' ↔ QuasiIsoAt φ j

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{u_4, u_3} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.extend e).HasHomology j'
inst✝ : (L.extend e).HasHomology j'
⊢ IsIso (homologyMap (extendMap φ e) j') ↔ IsIso (homologyMap φ j)

Tactic:
exact (MorphismProperty.isomorphisms C).arrow_mk_iso_iff
  (Arrow.isoMk (K.extendHomologyIso e hj') (L.extendHomologyIso e hj'))

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{u_4, u_3} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.extend e).HasHomology j'
inst✝ : (L.extend e).HasHomology j'
⊢ QuasiIsoAt (extendMap φ e) j' ↔ QuasiIsoAt φ j

Tactic:
simp only [quasiIsoAt_iff_isIso_homologyMap]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{u_4, u_3} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.extend e).HasHomology j'
inst✝ : (L.extend e).HasHomology j'
⊢ IsIso (homologyMap (extendMap φ e) j') ↔ IsIso (homologyMap φ j)
-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem jacobson_bot : jacobson (⊥ : Ideal R) = Ring.jacobson R

Proof state:
R : Type u
inst✝ : Ring R
⊢ ⊥.jacobson = Ring.jacobson R

Tactic:
simp_rw [jacobson, Ring.jacobson, Module.jacobson, bot_le, true_and, isMaximal_def]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem analyticAt_exp_of_mem_ball (x : 𝔸) (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    AnalyticAt 𝕂 (exp 𝕂) x

Proof state:
case neg
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
h : ¬(expSeries 𝕂 𝔸).radius = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x

Tactic:
have h := pos_iff_ne_zero.mpr h

Result:
case neg
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
h✝ : ¬(expSeries 𝕂 𝔸).radius = 0
h : 0 < (expSeries 𝕂 𝔸).radius
⊢ AnalyticAt 𝕂 (exp 𝕂) x

Proof state:
case pos
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 0
h : (expSeries 𝕂 𝔸).radius = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x

Tactic:
exact (ENNReal.not_lt_zero hx).elim

Result:
no goals

Proof state:
case neg
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
h✝ : ¬(expSeries 𝕂 𝔸).radius = 0
h : 0 < (expSeries 𝕂 𝔸).radius
⊢ AnalyticAt 𝕂 (exp 𝕂) x

Tactic:
exact (hasFPowerSeriesOnBall_exp_of_radius_pos h).analyticAt_of_mem hx

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ AnalyticAt 𝕂 (exp 𝕂) x

Tactic:
by_cases h : (expSeries 𝕂 𝔸).radius = 0

Result:
case pos
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
h : (expSeries 𝕂 𝔸).radius = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x

case neg
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
h : ¬(expSeries 𝕂 𝔸).radius = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x

Proof state:
case pos
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
h : (expSeries 𝕂 𝔸).radius = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x

Tactic:
rw [h] at hx

Result:
case pos
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 0
h : (expSeries 𝕂 𝔸).radius = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem Parallel.trans {s₁ s₂ s₃ : AffineSubspace k P} (h₁₂ : s₁ ∥ s₂) (h₂₃ : s₂ ∥ s₃) :
    s₁ ∥ s₃

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
s₁ s₂ s₃ : AffineSubspace k P
h₁₂ : s₁ ∥ s₂
h₂₃ : s₂ ∥ s₃
⊢ s₁ ∥ s₃

Tactic:
rcases h₁₂ with ⟨v₁₂, rfl⟩

Result:
case intro
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
s₁ s₃ : AffineSubspace k P
v₁₂ : V
h₂₃ : map (↑(constVAdd k P v₁₂)) s₁ ∥ s₃
⊢ s₁ ∥ s₃

Proof state:
case intro.intro
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
s₁ : AffineSubspace k P
v₁₂ v₂₃ : V
⊢ map (↑(constVAdd k P v₂₃)) (map (↑(constVAdd k P v₁₂)) s₁) = map (↑(constVAdd k P (v₂₃ + v₁₂))) s₁

Tactic:
rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add]

Result:
no goals

Proof state:
case intro
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
s₁ s₃ : AffineSubspace k P
v₁₂ : V
h₂₃ : map (↑(constVAdd k P v₁₂)) s₁ ∥ s₃
⊢ s₁ ∥ s₃

Tactic:
rcases h₂₃ with ⟨v₂₃, rfl⟩

Result:
case intro.intro
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
s₁ : AffineSubspace k P
v₁₂ v₂₃ : V
⊢ s₁ ∥ map (↑(constVAdd k P v₂₃)) (map (↑(constVAdd k P v₁₂)) s₁)

Proof state:
case intro.intro
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
s₁ : AffineSubspace k P
v₁₂ v₂₃ : V
⊢ s₁ ∥ map (↑(constVAdd k P v₂₃)) (map (↑(constVAdd k P v₁₂)) s₁)

Tactic:
refine ⟨v₂₃ + v₁₂, ?_⟩

Result:
case intro.intro
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
s₁ : AffineSubspace k P
v₁₂ v₂₃ : V
⊢ map (↑(constVAdd k P v₂₃)) (map (↑(constVAdd k P v₁₂)) s₁) = map (↑(constVAdd k P (v₂₃ + v₁₂))) s₁
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem eLpNorm'_sum_norm_sub_le_tsum_of_cauchy_eLpNorm' {f : ℕ → α → E}
    (hf : ∀ n, AEStronglyMeasurable (f n) μ) {p : ℝ} (hp1 : 1 ≤ p) {B : ℕ → ℝ≥0∞}
    (h_cau : ∀ N n m : ℕ, N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N) (n : ℕ) :
    eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' i, B i

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ), (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) = ∑ i ∈ Finset.range (n + 1), f_norm_diff i
⊢ eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i

Tactic:
rw [hgf_norm_diff]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ), (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) = ∑ i ∈ Finset.range (n + 1), f_norm_diff i
⊢ eLpNorm' (∑ i ∈ Finset.range (n + 1), f_norm_diff i) p μ ≤ ∑' (i : ℕ), B i