harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Multiset/Bind.lean
theorem product_add (s : Multiset α) : ∀ t u : Multiset β, s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u :=
  Multiset.induction_on s (fun _ _ => rfl) fun a s IH t u => by
    rw [cons_product, IH]
    simp [add_comm, add_left_comm, add_assoc]

Proof state:
α : Type u_1
β : Type v
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ map (Prod.mk a) (t + u) + (s ×ˢ t + s ×ˢ u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u

Tactic:
simp [add_comm, add_left_comm, add_assoc]

Result:
no goals

Proof state:
α : Type u_1
β : Type v
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ (a ::ₘ s) ×ˢ (t + u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u

Tactic:
rw [cons_product, IH]

Result:
α : Type u_1
β : Type v
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ map (Prod.mk a) (t + u) + (s ×ˢ t + s ×ˢ u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem order_eq_find [DecidablePred fun n => p n ≠ 0] (hp : ∃ n, p n ≠ 0) :
    p.order = Nat.find hp

Proof state:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousAdd E
inst✝⁶ : ContinuousConstSMul 𝕜 E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst✝ : DecidablePred fun n => p n ≠ 0
hp : ∃ n, p n ≠ 0
⊢ p.order = Nat.find hp

Tactic:
convert Nat.sInf_def hp

Result:
no goals
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem mem_neLocus {f g : Π₀ a, N a} {a : α} : a ∈ f.neLocus g ↔ f a ≠ g a

Proof state:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
a : α
⊢ a ∈ f.neLocus g ↔ f a ≠ g a

Tactic:
simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff,
  and_iff_right_iff_imp] using Ne.ne_or_ne _

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasStrictDerivAt.const_smul (c : R) (hf : HasStrictDerivAt f f' x) :
    HasStrictDerivAt (fun y => c • f y) (c • f') x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
R : Type u_2
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun y => c • f y) (c • f') x

Tactic:
simpa using (hf.const_smul c).hasStrictDerivAt

Result:
no goals
-- Mathlib/Data/Part.lean
theorem union_get_eq [Union α] (a b : Part α) (hab : Dom (a ∪ b)) :
    (a ∪ b).get hab = a.get (left_dom_of_union_dom hab) ∪ b.get (right_dom_of_union_dom hab)

Proof state:
α : Type u_1
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ (a ∪ b).get hab = a.get ⋯ ∪ b.get ⋯

Tactic:
simp [union_def]

Result:
α : Type u_1
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ (a.bind fun y => map (fun x => y ∪ x) b).get ⋯ = a.get ⋯ ∪ b.get ⋯

Proof state:
α : Type u_1
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ (a.bind fun y => map (fun x => y ∪ x) b).get ⋯ = a.get ⋯ ∪ b.get ⋯

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_subtype_of_mem (f : α → β) {p : α → Prop} [DecidablePred p] (h : ∀ x ∈ s, p x) :
    ∏ x ∈ s.subtype p, f x = ∏ x ∈ s, f x

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
f : α → β
p : α → Prop
inst✝ : DecidablePred p
h : ∀ x ∈ s, p x
⊢ ∀ x ∈ s, p x

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
f : α → β
p : α → Prop
inst✝ : DecidablePred p
h : ∀ x ∈ s, p x
⊢ ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s, f x

Tactic:
rw [prod_subtype_eq_prod_filter, filter_true_of_mem]

Result:
α : Type u_3
β : Type u_4
s : Finset α
inst✝¹ : CommMonoid β
f : α → β
p : α → Prop
inst✝ : DecidablePred p
h : ∀ x ∈ s, p x
⊢ ∀ x ∈ s, p x
-- Mathlib/Data/Sym/Sym2.lean
theorem fromRel_top : fromRel (fun (_ _ : α) z => z : Symmetric ⊤) = Set.univ

Proof state:
α : Type u_1
⊢ ∀ (e : Sym2 α), e ∈ fromRel ⋯

Tactic:
apply Sym2.ind

Result:
case h
α : Type u_1
⊢ ∀ (x y : α), s(x, y) ∈ fromRel ⋯

Proof state:
case h
α : Type u_1
⊢ ∀ (x y : α), s(x, y) ∈ fromRel ⋯

Tactic:
simp [-Set.top_eq_univ, Prop.top_eq_true]

Result:
no goals

Proof state:
α : Type u_1
⊢ fromRel ⋯ = Set.univ

Tactic:
apply Set.eq_univ_of_forall fun e => _

Result:
α : Type u_1
⊢ ∀ (e : Sym2 α), e ∈ fromRel ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem reverse_reverse (as : Array α) : as.reverse.reverse = as

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.reverse.reverse = { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
as : Array α
⊢ as.reverse.reverse = as

Tactic:
cases as

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.reverse.reverse = { toList := toList✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toFin_concat (x : BitVec w) (b : Bool) :
    (concat x b).toFin = Fin.mk (x.toNat * 2 + b.toNat) (by
      have := Bool.toNat_lt b
      simp [← Nat.two_pow_pred_add_two_pow_pred, Bool.toNat_lt b]
      omega
    )

Proof state:
w : Nat
x : BitVec w
b : Bool
⊢ x.toNat * 2 + b.toNat < 2 ^ (w + 1)

Tactic:
have := Bool.toNat_lt b

Result:
w : Nat
x : BitVec w
b : Bool
this : b.toNat < 2
⊢ x.toNat * 2 + b.toNat < 2 ^ (w + 1)

Proof state:
w : Nat
x : BitVec w
b : Bool
this : b.toNat < 2
⊢ x.toNat * 2 + b.toNat < 2 ^ (w + 1)

Tactic:
simp [← Nat.two_pow_pred_add_two_pow_pred, Bool.toNat_lt b]

Result:
w : Nat
x : BitVec w
b : Bool
this : b.toNat < 2
⊢ x.toNat * 2 + b.toNat < 2 ^ w + 2 ^ w

Proof state:
w : Nat
x : BitVec w
b : Bool
this : b.toNat < 2
⊢ x.toNat * 2 + b.toNat < 2 ^ w + 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
b : Bool
⊢ (x.concat b).toFin = ⟨x.toNat * 2 + b.toNat, ⋯⟩

Tactic:
simp [← Fin.val_inj]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem reindex_apply (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') (i' : ι') :
    (b.reindex e) i' = b (e.symm i')

Proof state:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ b.repr.symm ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e).symm (EuclideanSpace.single i' 1)) = b (e.symm i')

Tactic:
rw [← b.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm,
  EuclideanSpace.piLpCongrLeft_single]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ (b.reindex e) i' = b (e.symm i')

Tactic:
classical
  dsimp [reindex]
  rw [coe_ofRepr]
  dsimp
  rw [← b.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm,
    EuclideanSpace.piLpCongrLeft_single]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ (b.reindex e) i' = b (e.symm i')

Tactic:
dsimp [reindex]

Result:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ { repr := b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) } i' = b (e.symm i')

Proof state:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ (fun i => (b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e)).symm (EuclideanSpace.single i 1)) i' =
    b (e.symm i')

Tactic:
dsimp

Result:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ b.repr.symm ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e).symm (EuclideanSpace.single i' 1)) = b (e.symm i')

Proof state:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ { repr := b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) } i' = b (e.symm i')

Tactic:
rw [coe_ofRepr]

Result:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ (fun i => (b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e)).symm (EuclideanSpace.single i 1)) i' =
    b (e.symm i')
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
@[simp]
lemma map_tmul (f : Hom P P') (x y) :
    CotangentSpace.map f (x ⊗ₜ .D _ _ y) = (algebraMap _ _ x) ⊗ₜ .D _ _ (f.toAlgHom y)

Proof state:
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : S
y : P.Ring
⊢ (CotangentSpace.map f) (x ⊗ₜ[P.Ring] (D R P.Ring) y) = (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)

Tactic:
simp only [CotangentSpace.map, AlgHom.toRingHom_eq_coe, LinearMap.liftBaseChange_tmul,
  LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, map_D, mk_apply]

Result:
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : S
y : P.Ring
⊢ x • 1 ⊗ₜ[P'.Ring] (D R' P'.Ring) ((algebraMap P.Ring P'.Ring) y) =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)

Proof state:
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : S
y : P.Ring
⊢ x • 1 ⊗ₜ[P'.Ring] (D R' P'.Ring) ((algebraMap P.Ring P'.Ring) y) =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)

Tactic:
rw [smul_tmul', ← Algebra.algebraMap_eq_smul_one]

Result:
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : S
y : P.Ring
⊢ (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) ((algebraMap P.Ring P'.Ring) y) =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)

Proof state:
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : S
y : P.Ring
⊢ (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) ((algebraMap P.Ring P'.Ring) y) =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Localization/Algebra.lean
lemma IsLocalization.ker_map (hT : Submonoid.map g M = T) :
    RingHom.ker (IsLocalization.map Q g (hT.symm ▸ M.le_comap_map) : S →+* Q) =
      (RingHom.ker g).map (algebraMap R S)

Proof state:
case h.intro.intro
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
x : R
s : ↥M
⊢ mk' S x s ∈ RingHom.ker (map Q g ⋯) ↔ mk' S x s ∈ Ideal.map (algebraMap R S) (RingHom.ker g)

Tactic:
simp [RingHom.mem_ker, IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff,
  IsLocalization.mk'_mem_map_algebraMap_iff, ← hT]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
⊢ RingHom.ker (map Q g ⋯) = Ideal.map (algebraMap R S) (RingHom.ker g)

Tactic:
ext x

Result:
case h
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
x : S
⊢ x ∈ RingHom.ker (map Q g ⋯) ↔ x ∈ Ideal.map (algebraMap R S) (RingHom.ker g)

Proof state:
case h
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
x : S
⊢ x ∈ RingHom.ker (map Q g ⋯) ↔ x ∈ Ideal.map (algebraMap R S) (RingHom.ker g)

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective M x

Result:
case h.intro.intro
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
x : R
s : ↥M
⊢ mk' S x s ∈ RingHom.ker (map Q g ⋯) ↔ mk' S x s ∈ Ideal.map (algebraMap R S) (RingHom.ker g)
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_Ico_id_eq_factorial : ∀ n : ℕ, (∏ x ∈ Ico 1 (n + 1), x) = n !
  | 0 => rfl
  | n + 1 => by
    rw [prod_Ico_succ_top <| Nat.succ_le_succ <| Nat.zero_le n, Nat.factorial_succ,
      prod_Ico_id_eq_factorial n, Nat.succ_eq_add_one, mul_comm]

Proof state:
n : ℕ
⊢ ∏ x ∈ Ico 1 (n + 1 + 1), x = (n + 1)!

Tactic:
rw [prod_Ico_succ_top <| Nat.succ_le_succ <| Nat.zero_le n, Nat.factorial_succ,
  prod_Ico_id_eq_factorial n, Nat.succ_eq_add_one, mul_comm]

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Lemmas.lean
lemma isNilpotent.restrict
    {f : M →ₗ[R] M} {p : Submodule R M} (hf : MapsTo f p p) (hnil : IsNilpotent f) :
    IsNilpotent (f.restrict hf)

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
hnil : IsNilpotent f
⊢ IsNilpotent (f.restrict hf)

Tactic:
obtain ⟨n, hn⟩ := hnil

Result:
case intro
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
n : ℕ
hn : f ^ n = 0
⊢ IsNilpotent (f.restrict hf)

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
n : ℕ
hn : f ^ n = 0
m : ↥p
⊢ ⟨0, ⋯⟩ = 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
n : ℕ
hn : f ^ n = 0
m : ↥p
⊢ (f.restrict hf ^ n) m = 0 m

Tactic:
simp only [LinearMap.pow_restrict n, hn,
LinearMap.restrict_apply, LinearMap.zero_apply]

Result:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
n : ℕ
hn : f ^ n = 0
m : ↥p
⊢ ⟨0, ⋯⟩ = 0

Proof state:
case intro
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
n : ℕ
hn : f ^ n = 0
⊢ IsNilpotent (f.restrict hf)

Tactic:
exact ⟨n, LinearMap.ext fun m ↦ by simp only [LinearMap.pow_restrict n, hn,
  LinearMap.restrict_apply, LinearMap.zero_apply]; rfl⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Vandermonde.lean
theorem eq_zero_of_forall_index_sum_mul_pow_eq_zero {R : Type*} [CommRing R] [IsDomain R] {n : ℕ}
    {f v : Fin n → R} (hf : Function.Injective f) (hfv : ∀ j, (∑ i, v i * f j ^ (i : ℕ)) = 0) :
    v = 0

Proof state:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), ∑ i : Fin n, v i * f j ^ ↑i = 0
⊢ v = 0

Tactic:
apply eq_zero_of_forall_index_sum_pow_mul_eq_zero hf

Result:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), ∑ i : Fin n, v i * f j ^ ↑i = 0
⊢ ∀ (j : Fin n), ∑ i : Fin n, f j ^ ↑i * v i = 0

Proof state:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), ∑ i : Fin n, v i * f j ^ ↑i = 0
⊢ ∀ (j : Fin n), ∑ i : Fin n, f j ^ ↑i * v i = 0

Tactic:
simp_rw [mul_comm]

Result:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), ∑ i : Fin n, v i * f j ^ ↑i = 0
⊢ ∀ (j : Fin n), ∑ x : Fin n, v x * f j ^ ↑x = 0

Proof state:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), ∑ i : Fin n, v i * f j ^ ↑i = 0
⊢ ∀ (j : Fin n), ∑ x : Fin n, v x * f j ^ ↑x = 0

Tactic:
exact hfv

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem inter_eq_singleton_orthogonalProjectionFn {s : AffineSubspace ℝ P} [Nonempty s]
    [HasOrthogonalProjection s.direction] (p : P) :
    (s : Set P) ∩ mk' p s.directionᗮ = {orthogonalProjectionFn s p} :=
  Classical.choose_spec <|
    inter_eq_singleton_of_nonempty_of_isCompl (nonempty_subtype.mp ‹_›)
      (mk'_nonempty p s.directionᗮ)
      (by
        rw [direction_mk' p s.directionᗮ]
        exact Submodule.isCompl_orthogonal_of_completeSpace)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ IsCompl s.direction s.directionᗮ

Tactic:
exact Submodule.isCompl_orthogonal_of_completeSpace

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ IsCompl s.direction (mk' p s.directionᗮ).direction

Tactic:
rw [direction_mk' p s.directionᗮ]

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ IsCompl s.direction s.directionᗮ
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem prod_apply_inl_fst (i) : (b.prod b' (Sum.inl i)).1 = b i :=
  b.repr.injective <| by
    ext j
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply, LinearEquiv.prod_symm,
      LinearEquiv.prod_apply, b.repr.apply_symm_apply, LinearEquiv.symm_symm, repr_self,
      Equiv.toFun_as_coe, Finsupp.fst_sumFinsuppLEquivProdFinsupp]
    apply Finsupp.single_apply_left Sum.inl_injective

Proof state:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i j : ι
⊢ (b.repr ((b.prod b') (Sum.inl i)).1) j = (b.repr (b i)) j

Tactic:
simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply, LinearEquiv.prod_symm,
  LinearEquiv.prod_apply, b.repr.apply_symm_apply, LinearEquiv.symm_symm, repr_self,
  Equiv.toFun_as_coe, Finsupp.fst_sumFinsuppLEquivProdFinsupp]

Result:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i j : ι
⊢ (single (Sum.inl i) 1) (Sum.inl j) = (single i 1) j

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι
⊢ b.repr ((b.prod b') (Sum.inl i)).1 = b.repr (b i)

Tactic:
ext j

Result:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i j : ι
⊢ (b.repr ((b.prod b') (Sum.inl i)).1) j = (b.repr (b i)) j

Proof state:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i j : ι
⊢ (single (Sum.inl i) 1) (Sum.inl j) = (single i 1) j

Tactic:
apply Finsupp.single_apply_left Sum.inl_injective

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_forIn' {α : Type uu}
    (as : List α) (init : β) (f : γ → (a : α) → a ∈ as → β → m (ForInStep β)) (hmono : monotone f) :
    monotone (fun x => forIn' as init (f x))

Proof state:
case hmono
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
β : Type u
γ : Type w
inst✝ : PartialOrder γ
α : Type uu
as : List α
init : β
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
⊢ monotone f

Tactic:
apply hmono

Result:
no goals

Proof state:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
β : Type u
γ : Type w
inst✝ : PartialOrder γ
α : Type uu
as : List α
init : β
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
⊢ monotone fun x => forIn' as init (f x)

Tactic:
apply monotone_forIn'_loop

Result:
case hmono
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
β : Type u
γ : Type w
inst✝ : PartialOrder γ
α : Type uu
as : List α
init : β
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
⊢ monotone f
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_nat_eq_sum_factorization (n : ℕ) :
    logb b n = n.factorization.sum fun p t => t * logb b p

Proof state:
b : ℝ
n : ℕ
⊢ logb b ↑n = n.factorization.sum fun p t => ↑t * logb b ↑p

Tactic:
simp only [logb, mul_div_assoc', log_nat_eq_sum_factorization n, Finsupp.sum, Finset.sum_div]

Result:
no goals