harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Trace/Basic.lean
theorem embeddingsMatrixReindex_eq_vandermonde (pb : PowerBasis A B)
    (e : Fin pb.dim ≃ (B →ₐ[A] C)) :
    embeddingsMatrixReindex A C pb.basis e = (vandermonde fun i => e i pb.gen)ᵀ

Proof state:
case a
A : Type u
B : Type v
C : Type z
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : CommRing C
inst✝ : Algebra A C
pb : PowerBasis A B
e : Fin pb.dim ≃ (B →ₐ[A] C)
i j : Fin pb.dim
⊢ embeddingsMatrixReindex A C (⇑pb.basis) e i j = (vandermonde fun i => (e i) pb.gen)ᵀ i j

Tactic:
simp [embeddingsMatrixReindex, embeddingsMatrix]

Result:
no goals

Proof state:
A : Type u
B : Type v
C : Type z
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : CommRing C
inst✝ : Algebra A C
pb : PowerBasis A B
e : Fin pb.dim ≃ (B →ₐ[A] C)
⊢ embeddingsMatrixReindex A C (⇑pb.basis) e = (vandermonde fun i => (e i) pb.gen)ᵀ

Tactic:
ext i j

Result:
case a
A : Type u
B : Type v
C : Type z
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : CommRing C
inst✝ : Algebra A C
pb : PowerBasis A B
e : Fin pb.dim ≃ (B →ₐ[A] C)
i j : Fin pb.dim
⊢ embeddingsMatrixReindex A C (⇑pb.basis) e i j = (vandermonde fun i => (e i) pb.gen)ᵀ i j
-- Mathlib/Algebra/Module/LinearMap/Rat.lean
theorem AddMonoidHom.toRatLinearMap_injective [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂]
    [Module ℚ M₂] : Function.Injective (@AddMonoidHom.toRatLinearMap M M₂ _ _ _ _)

Proof state:
M : Type u_1
M₂ : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : f.toRatLinearMap = g.toRatLinearMap
⊢ f = g

Tactic:
ext x

Result:
case h
M : Type u_1
M₂ : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : f.toRatLinearMap = g.toRatLinearMap
x : M
⊢ f x = g x

Proof state:
case h
M : Type u_1
M₂ : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : f.toRatLinearMap = g.toRatLinearMap
x : M
⊢ f x = g x

Tactic:
exact LinearMap.congr_fun h x

Result:
no goals

Proof state:
M : Type u_1
M₂ : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
⊢ Injective toRatLinearMap

Tactic:
intro f g h

Result:
M : Type u_1
M₂ : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : f.toRatLinearMap = g.toRatLinearMap
⊢ f = g
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_setWidth (x : BitVec w) : (x.setWidth v).msb = (decide (0 < v) && x.getLsbD (v - 1))

Proof state:
case true
w v : Nat
x : BitVec w
⊢ v - 1 < v ↔ 0 < v

Tactic:
omega

Result:
no goals

Proof state:
w v : Nat
x : BitVec w
⊢ (decide (v - 1 < v) && x.getLsbD (v - 1)) = (decide (0 < v) && x.getLsbD (v - 1))

Tactic:
cases getLsbD x (v - 1) <;> simp

Result:
case true
w v : Nat
x : BitVec w
⊢ v - 1 < v ↔ 0 < v

Proof state:
w v : Nat
x : BitVec w
⊢ (setWidth v x).getLsbD (v - 1) = (decide (0 < v) && x.getLsbD (v - 1))

Tactic:
simp only [getLsbD_setWidth]

Result:
w v : Nat
x : BitVec w
⊢ (decide (v - 1 < v) && x.getLsbD (v - 1)) = (decide (0 < v) && x.getLsbD (v - 1))

Proof state:
w v : Nat
x : BitVec w
⊢ (setWidth v x).msb = (decide (0 < v) && x.getLsbD (v - 1))

Tactic:
rw [msb_eq_getLsbD_last]

Result:
w v : Nat
x : BitVec w
⊢ (setWidth v x).getLsbD (v - 1) = (decide (0 < v) && x.getLsbD (v - 1))
-- Mathlib/Algebra/Order/Module/OrderedSMul.lean
lemma inf_eq_half_smul_add_sub_abs_sub' (x y : β) : x ⊓ y = (2⁻¹ : α) • (x + y - |y - x|)

Proof state:
α : Type u_6
β : Type u_7
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : AddLeftMono β
x y : β
⊢ x ⊓ y = 2⁻¹ • (x + y - |y - x|)

Tactic:
letI := invertibleOfNonzero (two_ne_zero' α)

Result:
α : Type u_6
β : Type u_7
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : AddLeftMono β
x y : β
this : Invertible 2 := invertibleOfNonzero ⋯
⊢ x ⊓ y = 2⁻¹ • (x + y - |y - x|)

Proof state:
α : Type u_6
β : Type u_7
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : AddLeftMono β
x y : β
this : Invertible 2 := invertibleOfNonzero ⋯
⊢ x ⊓ y = 2⁻¹ • (x + y - |y - x|)

Tactic:
exact inf_eq_half_smul_add_sub_abs_sub α x y

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_eq_eraseP [LawfulBEq α] (a : α) : ∀ l : List α,  l.erase a = l.eraseP (a == ·)
  | [] => rfl
  | b :: l => by
    if h : a = b then simp [h] else simp [h, Ne.symm h, erase_eq_eraseP a l]

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
h : a = b
⊢ (b :: l).erase a = eraseP (fun x => a == x) (b :: l)

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
⊢ (b :: l).erase a = eraseP (fun x => a == x) (b :: l)

Tactic:
if h : a = b then simp [h] else simp [h, Ne.symm h, erase_eq_eraseP a l]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
h : ¬a = b
⊢ (b :: l).erase a = eraseP (fun x => a == x) (b :: l)

Tactic:
simp [h, Ne.symm h, erase_eq_eraseP a l]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zero_of_target_iso_zero {X Y : C} (f : X ⟶ Y) (i : Y ≅ 0) : f = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
h : f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv
⊢ f = 0

Tactic:
simpa using h

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
⊢ f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv

Tactic:
simp only [Iso.hom_inv_id, id_comp, comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
⊢ f = 0

Tactic:
have h : f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv := by simp only [Iso.hom_inv_id, id_comp, comp_id]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
h : f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv
⊢ f = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_comm {l : Array α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) :
    (l.eraseP p).eraseP q = (l.eraseP q).eraseP p

Proof state:
case mk
α : Type u_1
p q : α → Bool
l : List α
h : ∀ (a : α), a ∈ { toList := l } → ¬p a = true ∨ ¬q a = true
⊢ ({ toList := l }.eraseP p).eraseP q = ({ toList := l }.eraseP q).eraseP p

Tactic:
simpa using List.eraseP_comm (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
p q : α → Bool
l : List α
h : ∀ (a : α), a ∈ { toList := l } → ¬p a = true ∨ ¬q a = true
⊢ ∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
p q : α → Bool
l : Array α
h : ∀ (a : α), a ∈ l → ¬p a = true ∨ ¬q a = true
⊢ (l.eraseP p).eraseP q = (l.eraseP q).eraseP p

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p q : α → Bool
l : List α
h : ∀ (a : α), a ∈ { toList := l } → ¬p a = true ∨ ¬q a = true
⊢ ({ toList := l }.eraseP p).eraseP q = ({ toList := l }.eraseP q).eraseP p
-- Mathlib/Algebra/Order/Round.lean
theorem round_nat_add (x : α) (y : ℕ) : round ((y : α) + x) = y + round x

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ round (↑y + x) = ↑y + round x

Tactic:
rw [add_comm, round_add_nat, add_comm]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_symm_preimage_inter_range_eventuallyEq {s : Set M} {x : M} (hs : s ⊆ f.source)
    (hx : x ∈ f.source) :
    ((f.extend I).symm ⁻¹' s ∩ range I : Set _) =ᶠ[𝓝 (f.extend I x)] f.extend I '' s

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
x : M
hs : s ⊆ f.source
hx : x ∈ f.source
⊢ ↑(f.extend I).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(f.extend I) x)] ↑(f.extend I) '' s

Tactic:
rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin _ hx,
  map_extend_nhdsWithin_eq_image_of_subset _ hx hs]

Result:
no goals
-- Mathlib/Topology/Compactness/SigmaCompact.lean
theorem mem_iff_find_le {x : X} {n : ℕ} : x ∈ K n ↔ K.find x ≤ n

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
⊢ x ∈ K n ↔ K.find x ≤ n

Tactic:
classical
exact ⟨fun h => Nat.find_min' (K.exists_mem x) h, fun h => K.subset h <| K.mem_find x⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
⊢ x ∈ K n ↔ K.find x ≤ n

Tactic:
exact ⟨fun h => Nat.find_min' (K.exists_mem x) h, fun h => K.subset h <| K.mem_find x⟩

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem sub_div' {a b c : K} (hc : c ≠ 0) : b - a / c = (b * c - a) / c

Proof state:
K : Type u_1
inst✝ : Field K
a b c : K
hc : c ≠ 0
⊢ b - a / c = (b * c - a) / c

Tactic:
simpa using div_sub_div b a one_ne_zero hc

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem adjMatrix_vecMul_apply [NonAssocSemiring α] (v : V) (vec : V → α) :
    (vec ᵥ* G.adjMatrix α) v = ∑ u ∈ G.neighborFinset v, vec u

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (vec ᵥ* adjMatrix α G) v = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
simp only [← dotProduct_adjMatrix, vecMul]

Result:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (vec ⬝ᵥ fun i => adjMatrix α G i v) = vec ⬝ᵥ adjMatrix α G v

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (vec ⬝ᵥ fun i => adjMatrix α G i v) = vec ⬝ᵥ adjMatrix α G v

Tactic:
refine congr rfl ?_

Result:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (fun i => adjMatrix α G i v) = adjMatrix α G v

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (fun i => adjMatrix α G i v) = adjMatrix α G v

Tactic:
ext x

Result:
case h
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
x : V
⊢ adjMatrix α G x v = adjMatrix α G v x

Proof state:
case h
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
x : V
⊢ adjMatrix α G x v = adjMatrix α G v x

Tactic:
rw [← transpose_apply (adjMatrix α G) x v, transpose_adjMatrix]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
lemma shiftFunctorComm_hom_app_f (K : CochainComplex C ℤ) (a b p : ℤ) :
    ((shiftFunctorComm (CochainComplex C ℤ) a b).hom.app K).f p =
      (K.XIsoOfEq (show p + b + a = p + a + b
        by rw [add_assoc, add_comm b, add_assoc])).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).inv.app K).f p ≫
      ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) b a (a + b) ⋯).hom.app K).f p =
    (XIsoOfEq K ⋯).hom

Tactic:
rw [shiftFunctorAdd'_inv_app_f', shiftFunctorAdd'_hom_app_f']

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom = (XIsoOfEq K ⋯).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom = (XIsoOfEq K ⋯).hom

Tactic:
simp only [XIsoOfEq, eqToIso.hom, eqToHom_trans]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ ((shiftFunctorComm (CochainComplex C ℤ) a b).hom.app K).f p = (XIsoOfEq K ⋯).hom

Tactic:
rw [shiftFunctorComm_eq _ _ _ _ rfl]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ (((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).symm ≪≫
                CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) b a (a + b) ⋯).hom.app
          K).f
      p =
    (XIsoOfEq K ⋯).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b p : ℤ
⊢ p + b + a = p + a + b

Tactic:
rw [add_assoc, add_comm b, add_assoc]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ (((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).symm ≪≫
                CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) b a (a + b) ⋯).hom.app
          K).f
      p =
    (XIsoOfEq K ⋯).hom

Tactic:
dsimp

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).inv.app K).f p ≫
      ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) b a (a + b) ⋯).hom.app K).f p =
    (XIsoOfEq K ⋯).hom
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem getLast?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
    (H : ∀ (a : α), a ∈ xs → P a) :
    (xs.pmap f H).getLast? = xs.attach.getLast?.map fun ⟨a, m⟩ => f a (H a m)

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ (pmap f xs H).reverse.head? = Option.map (fun x => f x.val ⋯) xs.attach.reverse.head?

Tactic:
rw [reverse_pmap, reverse_attach, head?_map, pmap_eq_map_attach, head?_map]

Result:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ Option.map (fun x => f x.val ⋯) xs.reverse.attach.head? =
    Option.map (fun x => f x.val ⋯)
      (Option.map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        xs.reverse.attach.head?)

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ (pmap f xs H).getLast? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      xs.attach.getLast?

Tactic:
simp only [getLast?_eq_head?_reverse]

Result:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ (pmap f xs H).reverse.head? = Option.map (fun x => f x.val ⋯) xs.attach.reverse.head?

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ Option.map (fun x => f x.val ⋯) xs.reverse.attach.head? =
    Option.map (fun x => f x.val ⋯)
      (Option.map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        xs.reverse.attach.head?)

Tactic:
simp only [Option.map_map]

Result:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ Option.map (fun x => f x.val ⋯) xs.reverse.attach.head? =
    Option.map ((fun x => f x.val ⋯) ∘ fun x => ⟨x.val, ⋯⟩) xs.reverse.attach.head?

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ Option.map (fun x => f x.val ⋯) xs.reverse.attach.head? =
    Option.map ((fun x => f x.val ⋯) ∘ fun x => ⟨x.val, ⋯⟩) xs.reverse.attach.head?

Tactic:
congr

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_zero_measure {m : MeasurableSpace α} (f : α → G) :
    (∫ x, f x ∂(0 : Measure α)) = 0

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
f : α → G
hG : ¬CompleteSpace G
⊢ ∫ (x : α), f x ∂0 = 0

Tactic:
simp [integral, hG]

Result:
no goals

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
f : α → G
hG : CompleteSpace G
⊢ (if h : True then if hf : Integrable (fun x => f x) 0 then L1.integralCLM (Integrable.toL1 (fun x => f x) hf) else 0
    else 0) =
    0

Tactic:
exact setToFun_measure_zero (dominatedFinMeasAdditive_weightedSMul _) rfl

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
f : α → G
⊢ ∫ (x : α), f x ∂0 = 0

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
f : α → G
hG : CompleteSpace G
⊢ ∫ (x : α), f x ∂0 = 0

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
f : α → G
hG : ¬CompleteSpace G
⊢ ∫ (x : α), f x ∂0 = 0

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
f : α → G
hG : CompleteSpace G
⊢ ∫ (x : α), f x ∂0 = 0

Tactic:
simp only [integral, hG, L1.integral]

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
f : α → G
hG : CompleteSpace G
⊢ (if h : True then if hf : Integrable (fun x => f x) 0 then L1.integralCLM (Integrable.toL1 (fun x => f x) hf) else 0
    else 0) =
    0
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
/-- An induction principle for reasonning about morphisms in SimplexCategoryGenRel, where we compose
with generators on the right. -/
lemma hom_induction' (P : MorphismProperty SimplexCategoryGenRel)
    (id : ∀ {n : ℕ}, P (𝟙 (mk n)))
    (δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n)
      (i : Fin (m + 2)), P u → P (δ i ≫ u))
    (σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n)
      (i : Fin (m + 1)), P u → P (σ i ≫ u )) {a b : SimplexCategoryGenRel} (f : a ⟶ b) :
    P f

Proof state:
case of.inl.δ
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 2)
⊢ P (δ i)

Tactic:
simpa using (δ_comp (𝟙 _) i id)

Result:
no goals

Proof state:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : generators.multiplicativeClosure' ≤ P
⊢ P f

Tactic:
rw [← MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure',
  multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this

Result:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : P = ⊤
⊢ P f
-- Mathlib/Topology/Instances/AddCircle.lean
lemma isLocalHomeomorph_coe [DiscreteTopology (zmultiples p)] [DenselyOrdered 𝕜] :
    IsLocalHomeomorph ((↑) : 𝕜 → AddCircle p)

Proof state:
𝕜 : Type u_1
inst✝⁵ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝⁴ : Archimedean 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
inst✝¹ : DiscreteTopology ↥(zmultiples p)
inst✝ : DenselyOrdered 𝕜
⊢ IsLocalHomeomorph QuotientAddGroup.mk

Tactic:
intro a

Result:
𝕜 : Type u_1
inst✝⁵ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝⁴ : Archimedean 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
inst✝¹ : DiscreteTopology ↥(zmultiples p)
inst✝ : DenselyOrdered 𝕜
a : 𝕜
⊢ ∃ e, a ∈ e.source ∧ QuotientAddGroup.mk = ↑e

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝⁵ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝⁴ : Archimedean 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
inst✝¹ : DiscreteTopology ↥(zmultiples p)
inst✝ : DenselyOrdered 𝕜
a b : 𝕜
hb1 : a - p < b
hb2 : b < a
⊢ ∃ e, a ∈ e.source ∧ QuotientAddGroup.mk = ↑e

Tactic:
exact ⟨partialHomeomorphCoe p b, ⟨hb2, lt_add_of_sub_right_lt hb1⟩, rfl⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝⁴ : Archimedean 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
inst✝¹ : DiscreteTopology ↥(zmultiples p)
inst✝ : DenselyOrdered 𝕜
a : 𝕜
⊢ ∃ e, a ∈ e.source ∧ QuotientAddGroup.mk = ↑e

Tactic:
obtain ⟨b, hb1, hb2⟩ := exists_between (sub_lt_self a hp.out)

Result:
case intro.intro
𝕜 : Type u_1
inst✝⁵ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝⁴ : Archimedean 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
inst✝¹ : DiscreteTopology ↥(zmultiples p)
inst✝ : DenselyOrdered 𝕜
a b : 𝕜
hb1 : a - p < b
hb2 : b < a
⊢ ∃ e, a ∈ e.source ∧ QuotientAddGroup.mk = ↑e
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_eq_foldlM (f : β → α → β) (b) (l : Array α) :
    l.foldl f b start stop = l.foldlM (m := Id) f b start stop

Proof state:
β : Type u_1
α : Type u_2
start stop : Nat
f : β → α → β
b : β
l : Array α
⊢ foldl f b l start stop = foldlM f b l start stop

Tactic:
simp [foldl, Id.run]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Vector α n} (h : ∀ a ∈ l, p a) (i : Nat) :
    (pmap f l h)[i]? = Option.pmap f l[i]? fun x H => h x (mem_of_getElem? H)

Proof state:
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : (a : α) → p a → β
l : Vector α n
h : ∀ (a : α), a ∈ l → p a
i : Nat
⊢ (pmap f l h)[i]? = Option.pmap f l[i]? ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : (a : α) → p a → β
i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ (pmap f { toArray := toArray✝, size_toArray := size_toArray✝ } h)[i]? =
    Option.pmap f { toArray := toArray✝, size_toArray := size_toArray✝ }[i]? ⋯

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : (a : α) → p a → β
i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ (pmap f { toArray := toArray✝, size_toArray := size_toArray✝ } h)[i]? =
    Option.pmap f { toArray := toArray✝, size_toArray := size_toArray✝ }[i]? ⋯

Tactic:
simp

Result:
no goals