harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma nnrpow_add {a : A} {x y : ℝ≥0} (hx : 0 < x) (hy : 0 < y) :
    a ^ (x + y) = a ^ x * a ^ y

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
⊢ cfcₙ (fun x_1 => x_1.nnrpow (x + y)) a = cfcₙ (fun x_1 => x_1.nnrpow x) a * cfcₙ (fun x => x.nnrpow y) a

Tactic:
rw [← cfcₙ_mul _ _ a]

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
⊢ cfcₙ (fun x_1 => x_1.nnrpow (x + y)) a = cfcₙ (fun x_1 => x_1.nnrpow x * x_1.nnrpow y) a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
⊢ a ^ (x + y) = a ^ x * a ^ y

Tactic:
simp only [nnrpow_def]

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
⊢ cfcₙ (fun x_1 => x_1.nnrpow (x + y)) a = cfcₙ (fun x_1 => x_1.nnrpow x) a * cfcₙ (fun x => x.nnrpow y) a

Proof state:
case h.e'_17.h
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
z : ℝ≥0
⊢ z.nnrpow (x + y) = z.nnrpow x * z.nnrpow y

Tactic:
exact mod_cast z.rpow_add' <| ne_of_gt (add_pos hx hy)

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
⊢ cfcₙ (fun x_1 => x_1.nnrpow (x + y)) a = cfcₙ (fun x_1 => x_1.nnrpow x * x_1.nnrpow y) a

Tactic:
congr! 2 with z

Result:
case h.e'_17.h
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
z : ℝ≥0
⊢ z.nnrpow (x + y) = z.nnrpow x * z.nnrpow y
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.toMatrix₂_compl₂ (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (f : M₂' →ₗ[R] M₂) :
    LinearMap.toMatrix₂ b₁ b₂' (B.compl₂ f) =
      LinearMap.toMatrix₂ b₁ b₂ B * toMatrix b₂' b₂ f

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₂' : Type u_9
n : Type u_11
m : Type u_12
m' : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₂'
inst✝² : Module R M₂'
b₂' : Basis m' R M₂'
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₂' →ₗ[R] M₂
⊢ (toMatrix₂ b₁ b₂') (B.compl₂ f) = (toMatrix₂ b₁ b₂) B * (toMatrix b₂' b₂) f

Tactic:
rw [← LinearMap.comp_id B, ← LinearMap.compl₁₂, LinearMap.toMatrix₂_compl₁₂ b₁ b₂]

Result:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₂' : Type u_9
n : Type u_11
m : Type u_12
m' : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₂'
inst✝² : Module R M₂'
b₂' : Basis m' R M₂'
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₂' →ₗ[R] M₂
⊢ ((toMatrix b₁ b₁) id)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix b₂' b₂) f = (toMatrix₂ b₁ b₂) (B ∘ₗ id) * (toMatrix b₂' b₂) f

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₂' : Type u_9
n : Type u_11
m : Type u_12
m' : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₂'
inst✝² : Module R M₂'
b₂' : Basis m' R M₂'
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₂' →ₗ[R] M₂
⊢ ((toMatrix b₁ b₁) id)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix b₂' b₂) f = (toMatrix₂ b₁ b₂) (B ∘ₗ id) * (toMatrix b₂' b₂) f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Ioc {a b : α} : ((↑) : ℤ → α) ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋ ⌊b⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ Int.cast ⁻¹' Ioc a b = Ioc ⌊a⌋ ⌊b⌋

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ioc a b ↔ x✝ ∈ Ioc ⌊a⌋ ⌊b⌋

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ioc a b ↔ x✝ ∈ Ioc ⌊a⌋ ⌊b⌋

Tactic:
simp [floor_lt, le_floor]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
lemma listTake_succ_alternatingWord (i j : B) (p : ℕ) (k : ℕ) (h : k + 1 < 2 * p) :
    List.take (k + 1) (alternatingWord i j (2 * p)) =
    i :: (List.take k (alternatingWord j i (2 * p)))

Proof state:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k

Tactic:
by_cases h_even : Even k

Result:
case pos
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : Even k
⊢ (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k

case neg
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : ¬Even k
⊢ (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k

Proof state:
case pos
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : Even k
⊢ (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k

Tactic:
simp [h_even, Nat.not_even_iff_odd.mpr (Even.add_one h_even), alternatingWord_succ', h_even]

Result:
no goals

Proof state:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < 2 * p

Tactic:
omega

Result:
no goals

Proof state:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : ¬Even k
⊢ Even (k + 1)

Tactic:
rw [Nat.not_even_iff_odd] at h_even

Result:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : Odd k
⊢ Even (k + 1)

Proof state:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ take (k + 1) (alternatingWord i j (2 * p)) = i :: take k (alternatingWord j i (2 * p))

Tactic:
rw [listTake_alternatingWord j i p k (by omega), listTake_alternatingWord i j p (k+1) h]

Result:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k

Proof state:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : Odd k
⊢ Even (k + 1)

Tactic:
exact Odd.add_one h_even

Result:
no goals

Proof state:
case neg
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : ¬Even k
⊢ (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k

Tactic:
simp [h_even, (by rw [Nat.not_even_iff_odd] at h_even; exact Odd.add_one h_even : Even (k + 1)),
  alternatingWord_succ', h_even]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_replicate (w : replicate n a ≠ []) : (replicate n a).head w = a

Proof state:
case zero
α✝ : Type u_1
a : α✝
w : replicate 0 a ≠ []
⊢ (replicate 0 a).head w = a

Tactic:
simp at w

Result:
no goals

Proof state:
case succ
α✝ : Type u_1
a : α✝
n✝ : Nat
w : replicate (n✝ + 1) a ≠ []
⊢ (replicate (n✝ + 1) a).head w = a

Tactic:
simp_all [replicate_succ]

Result:
no goals

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
w : replicate n a ≠ []
⊢ (replicate n a).head w = a

Tactic:
cases n

Result:
case zero
α✝ : Type u_1
a : α✝
w : replicate 0 a ≠ []
⊢ (replicate 0 a).head w = a

case succ
α✝ : Type u_1
a : α✝
n✝ : Nat
w : replicate (n✝ + 1) a ≠ []
⊢ (replicate (n✝ + 1) a).head w = a
-- Mathlib/SetTheory/Cardinal/Continuum.lean
theorem lift_lt_continuum {c : Cardinal.{u}} : lift.{v} c < 𝔠 ↔ c < 𝔠

Proof state:
c : Cardinal.{u}
⊢ lift.{v, u} c < 𝔠 ↔ c < 𝔠

Tactic:
rw [← lift_continuum.{v, u}, lift_lt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulVecOperator.lean
theorem lt_size (entry : Entrypoint α) (input : β entry.aig len) :
    entry.ref.gate < (f entry.aig input).aig.decls.size

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size

Tactic:
have h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size := by
  apply le_size

Result:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size

Tactic:
apply le_size

Result:
no goals

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size

Tactic:
have h1 := entry.ref.hgate

Result:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
entry : Entrypoint α
input : β entry.aig len
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem app_inv_app' (U : Opens Y) (hU : (U : Set Y) ⊆ Set.range f.base) :
    f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U) =
      Y.presheaf.map
        (eqToHom
            (le_antisymm (Set.image_preimage_subset f.base U.1) <|
              (Set.image_preimage_eq_inter_range (f := f.base) (t := U.1)).symm ▸
                Set.subset_inter_iff.mpr ⟨fun _ h => h, hU⟩)).op

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯) =
    f.c.app (op U) ≫ ((TopCat.Presheaf.pushforward C f.base).obj X.presheaf).map (eqToHom ⋯).op

Tactic:
congr

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U) = Y.presheaf.map (eqToHom ⋯).op

Tactic:
erw [← Category.assoc]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ (f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj ((Opens.map f.base).obj U)))) =
    Y.presheaf.map (eqToHom ⋯).op

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ (f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj ((Opens.map f.base).obj U)))) =
    Y.presheaf.map (eqToHom ⋯).op

Tactic:
rw [IsIso.comp_inv_eq, f.c.naturality]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯) =
    f.c.app (op U) ≫ ((TopCat.Presheaf.pushforward C f.base).obj X.presheaf).map (eqToHom ⋯).op
-- Mathlib/LinearAlgebra/Multilinear/Basis.lean
theorem Basis.ext_multilinear_fin {f g : MultilinearMap R M M₂} {ι₁ : Fin n → Type*}
    (e : ∀ i, Basis (ι₁ i) R (M i))
    (h : ∀ v : ∀ i, ι₁ i, (f fun i => e i (v i)) = g fun i => e i (v i)) : f = g

Proof state:
case succ.a
R : Type u_1
M₂ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (f fun i => (e i) (v i)) = g fun i => (e i) (v i)) → f = g
M : Fin (m + 1) → Type u_3
inst✝¹ : (i : Fin (m + 1)) → AddCommMonoid (M i)
inst✝ : (i : Fin (m + 1)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (m + 1) → Type u_6
e : (i : Fin (m + 1)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (m + 1)) → ι₁ i), (f fun i => (e i) (v i)) = g fun i => (e i) (v i)
⊢ ∀ (i : ι₁ 0), f.curryLeft ((e 0) i) = g.curryLeft ((e 0) i)

Tactic:
intro i

Result:
case succ.a
R : Type u_1
M₂ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (f fun i => (e i) (v i)) = g fun i => (e i) (v i)) → f = g
M : Fin (m + 1) → Type u_3
inst✝¹ : (i : Fin (m + 1)) → AddCommMonoid (M i)
inst✝ : (i : Fin (m + 1)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (m + 1) → Type u_6
e : (i : Fin (m + 1)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (m + 1)) → ι₁ i), (f fun i => (e i) (v i)) = g fun i => (e i) (v i)
i : ι₁ 0
⊢ f.curryLeft ((e 0) i) = g.curryLeft ((e 0) i)

Proof state:
case h.e'_3.h.e_6.h.h
R : Type u_1
M₂ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (f fun i => (e i) (v i)) = g fun i => (e i) (v i)) → f = g
M : Fin (m + 1) → Type u_3
inst✝¹ : (i : Fin (m + 1)) → AddCommMonoid (M i)
inst✝ : (i : Fin (m + 1)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (m + 1) → Type u_6
e : (i : Fin (m + 1)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (m + 1)) → ι₁ i), (f fun i => (e i) (v i)) = g fun i => (e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ i.succ
x✝ : Fin (m + 1)
x : Fin m
⊢ Fin.cons ((e 0) i) (fun i => (e i.succ) (j i)) x.succ = (e x.succ) (Fin.cons i j x.succ)

Tactic:
rw [Fin.cons_succ, Fin.cons_succ]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- Sending `Fin n` into `Fin (n + 1)` with a gap at `p`
then back to `Fin n` by subtracting one from anything above `p` is the identity. -/
@[simp]
lemma predAbove_succAbove (p : Fin n) (i : Fin n) : p.predAbove ((castSucc p).succAbove i) = i

Proof state:
case inr
n : ℕ
p i : Fin n
h : i < p
⊢ p.predAbove (p.castSucc.succAbove i) = i

Tactic:
rw [succAbove_castSucc_of_lt _ _ h, predAbove_castSucc_of_le _ _ <| Fin.le_of_lt h]

Result:
no goals

Proof state:
n : ℕ
p i : Fin n
⊢ p.predAbove (p.castSucc.succAbove i) = i

Tactic:
obtain h | h := p.le_or_lt i

Result:
case inl
n : ℕ
p i : Fin n
h : p ≤ i
⊢ p.predAbove (p.castSucc.succAbove i) = i

case inr
n : ℕ
p i : Fin n
h : i < p
⊢ p.predAbove (p.castSucc.succAbove i) = i

Proof state:
case inl
n : ℕ
p i : Fin n
h : p ≤ i
⊢ p.predAbove (p.castSucc.succAbove i) = i

Tactic:
rw [succAbove_castSucc_of_le _ _ h, predAbove_succ_of_le _ _ h]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem List.aemeasurable_prod' (l : List (α → M)) (hl : ∀ f ∈ l, AEMeasurable f μ) :
    AEMeasurable l.prod μ

Proof state:
case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.prod μ
hl : AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ
⊢ AEMeasurable (f * l.prod) μ

Tactic:
exact hl.1.mul (ihl hl.2)

Result:
no goals

Proof state:
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : List (α → M)
hl : ∀ f ∈ l, AEMeasurable f μ
⊢ AEMeasurable l.prod μ

Tactic:
induction' l with f l ihl

Result:
case nil
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
hl : ∀ f ∈ [], AEMeasurable f μ
⊢ AEMeasurable [].prod μ

case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.prod μ
hl : ∀ f_1 ∈ f :: l, AEMeasurable f_1 μ
⊢ AEMeasurable (f :: l).prod μ

Proof state:
case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.prod μ
hl : ∀ f_1 ∈ f :: l, AEMeasurable f_1 μ
⊢ AEMeasurable (f :: l).prod μ

Tactic:
rw [List.forall_mem_cons] at hl

Result:
case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.prod μ
hl : AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ
⊢ AEMeasurable (f :: l).prod μ

Proof state:
case nil
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
hl : ∀ f ∈ [], AEMeasurable f μ
⊢ AEMeasurable [].prod μ

Tactic:
exact aemeasurable_one

Result:
no goals

Proof state:
case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.prod μ
hl : AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ
⊢ AEMeasurable (f :: l).prod μ

Tactic:
rw [List.prod_cons]

Result:
case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.prod μ
hl : AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ
⊢ AEMeasurable (f * l.prod) μ
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.finsupp_sum_mem_span_eval {a : I} {as : List I}
    (ha : List.Chain' (· > ·) (a :: as)) {c : Products I →₀ ℤ}
    (hc : (c.support : Set (Products I)) ⊆ {m | m.val ≤ as}) :
    (Finsupp.sum c fun a_1 b ↦ e (π C (· ∈ s)) a * b • Products.eval (π C (· ∈ s)) a_1) ∈
      Submodule.span ℤ (Products.eval (π C (· ∈ s)) '' {m | m.val ≤ a :: as})

Proof state:
case a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
⊢ m ∈ ↑c.support

Tactic:
simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm

Result:
no goals

Proof state:
case h.h.a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
hmas : ↑m ≤ as
⊢ e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m ∈
    Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as}

Tactic:
refine ⟨⟨a :: m.val, ha.cons_of_le m.prop hmas⟩, ⟨List.cons_le_cons a hmas, ?_⟩⟩

Result:
case h.h.a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
hmas : ↑m ≤ as
⊢ Products.eval (π C fun x => x ∈ s) ⟨a :: ↑m, ⋯⟩ = e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    (LinearMap.mulLeft ℤ (e (π C fun x => x ∈ s) a)) (c • x) = c • (LinearMap.mulLeft ℤ (e (π C fun x => x ∈ s) a)) x
⊢ e (π C fun x => x ∈ s) a * c m • Products.eval (π C fun x => x ∈ s) m ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
dsimp at hsm

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
⊢ e (π C fun x => x ∈ s) a * c m • Products.eval (π C fun x => x ∈ s) m ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})