harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsLittleO.tendsto_zero_of_tendsto {α E 𝕜 : Type*} [NormedAddCommGroup E] [NormedField 𝕜]
    {u : α → E} {v : α → 𝕜} {l : Filter α} {y : 𝕜} (huv : u =o[l] v) (hv : Tendsto v l (𝓝 y)) :
    Tendsto u l (𝓝 0)

Proof state:
α : Type u_17
E : Type u_18
𝕜 : Type u_19
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedField 𝕜
u : α → E
v : α → 𝕜
l : Filter α
y : 𝕜
huv : u =o[l] v
hv : Tendsto v l (𝓝 y)
⊢ Tendsto u l (𝓝 0)

Tactic:
suffices h : u =o[l] fun _x => (1 : 𝕜) by
  rwa [isLittleO_one_iff] at h

Result:
α : Type u_17
E : Type u_18
𝕜 : Type u_19
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedField 𝕜
u : α → E
v : α → 𝕜
l : Filter α
y : 𝕜
huv : u =o[l] v
hv : Tendsto v l (𝓝 y)
⊢ u =o[l] fun _x => 1

Proof state:
α : Type u_17
E : Type u_18
𝕜 : Type u_19
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedField 𝕜
u : α → E
v : α → 𝕜
l : Filter α
y : 𝕜
huv : u =o[l] v
hv : Tendsto v l (𝓝 y)
⊢ u =o[l] fun _x => 1

Tactic:
exact huv.trans_isBigO (hv.isBigO_one 𝕜)

Result:
no goals

Proof state:
α : Type u_17
E : Type u_18
𝕜 : Type u_19
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedField 𝕜
u : α → E
v : α → 𝕜
l : Filter α
y : 𝕜
huv : u =o[l] v
hv : Tendsto v l (𝓝 y)
h : u =o[l] fun _x => 1
⊢ Tendsto u l (𝓝 0)

Tactic:
rwa [isLittleO_one_iff] at h

Result:
no goals
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
/-- The multiplicative indicators of closed δ-thickenings of a set tend pointwise to the
multiplicative indicator of the set, as δ tends to zero. -/
@[to_additive "The indicators of closed δ-thickenings of a set tend pointwise to the indicator
of the set, as δ tends to zero."]
lemma tendsto_mulIndicator_cthickening_mulIndicator_closure (f : α → β) (E : Set α) :
    Tendsto (fun δ ↦ (Metric.cthickening δ E).mulIndicator f) (𝓝 0)
      (𝓝 ((closure E).mulIndicator f))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ ∀ (x : α), Tendsto (fun i => (cthickening i E).mulIndicator f x) (𝓝 0) (𝓝 ((closure E).mulIndicator f x))

Tactic:
intro x

Result:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun i => (cthickening i E).mulIndicator f x) (𝓝 0) (𝓝 ((closure E).mulIndicator f x))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun i => (cthickening i E).mulIndicator f x) (𝓝 0) (𝓝 ((closure E).mulIndicator f x))

Tactic:
rw [tendsto_congr' (mulIndicator_cthickening_eventually_eq_mulIndicator_closure f E x)]

Result:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun x_1 => (closure E).mulIndicator f x) (𝓝 0) (𝓝 ((closure E).mulIndicator f x))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ Tendsto (fun δ => (cthickening δ E).mulIndicator f) (𝓝 0) (𝓝 ((closure E).mulIndicator f))

Tactic:
rw [tendsto_pi_nhds]

Result:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ ∀ (x : α), Tendsto (fun i => (cthickening i E).mulIndicator f x) (𝓝 0) (𝓝 ((closure E).mulIndicator f x))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun x_1 => (closure E).mulIndicator f x) (𝓝 0) (𝓝 ((closure E).mulIndicator f x))

Tactic:
apply tendsto_const_nhds

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem imageMonoFactorisation_e' {X Y : C} (f : X ⟶ Y) :
    (imageMonoFactorisation f).e = cokernel.π _ ≫ Abelian.coimageImageComparison f

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ kernel.lift (cokernel.π f) f ⋯ ≫ equalizer.ι (cokernel.π f) 0 =
    (cokernel.π (kernel.ι f) ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0

Tactic:
simp only [Abelian.coimageImageComparison, imageMonoFactorisation_e, Category.assoc,
  cokernel.π_desc_assoc]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ (imageMonoFactorisation f).e = cokernel.π (kernel.ι f) ≫ coimageImageComparison f

Tactic:
dsimp

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ kernel.lift (cokernel.π f) f ⋯ = cokernel.π (kernel.ι f) ≫ coimageImageComparison f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ kernel.lift (cokernel.π f) f ⋯ = cokernel.π (kernel.ι f) ≫ coimageImageComparison f

Tactic:
ext

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ kernel.lift (cokernel.π f) f ⋯ ≫ equalizer.ι (cokernel.π f) 0 =
    (cokernel.π (kernel.ι f) ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem balLeft_toList {l : RBNode α} {v r} :
    (l.balLeft v r).toList = l.toList ++ v :: r.toList

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balLeft v r).toList = l.toList ++ v :: r.toList

Tactic:
unfold balLeft

Result:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (match l with
      | node red a x b => node red (node black a x b) v r
      | l =>
        match r with
        | node black a y b => l.balance2 v (node red a y b)
        | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
        | r => node red l v r).toList =
    l.toList ++ v :: r.toList

Proof state:
case h_1
α : Type u_1
v : α
r l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
⊢ (node red (node black a✝ x✝ b✝) v r).toList = (node red a✝ x✝ b✝).toList ++ v :: r.toList

Tactic:
try simp

Result:
no goals

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (match l with
      | node red a x b => node red (node black a x b) v r
      | l =>
        match r with
        | node black a y b => l.balance2 v (node red a y b)
        | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
        | r => node red l v r).toList =
    l.toList ++ v :: r.toList

Tactic:
split <;> (try simp)

Result:
case h_2
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
⊢ (match r with
      | node black a y b => l.balance2 v (node red a y b)
      | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
      | r => node red l v r).toList =
    l.toList ++ v :: r.toList

Proof state:
case h_1
α : Type u_1
v : α
r l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
⊢ (node red (node black a✝ x✝ b✝) v r).toList = (node red a✝ x✝ b✝).toList ++ v :: r.toList

Tactic:
simp

Result:
no goals

Proof state:
case h_2
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
⊢ (match r with
      | node black a y b => l.balance2 v (node red a y b)
      | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
      | r => node red l v r).toList =
    l.toList ++ v :: r.toList

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean
@[fun_prop]
lemma analyticAt_log (hx : 0 < x) : AnalyticAt ℝ Real.log x

Proof state:
x : ℝ
hx : 0 < x
⊢ Real.log = fun x => (log ↑x).re

Tactic:
ext x

Result:
case h
x✝ : ℝ
hx : 0 < x✝
x : ℝ
⊢ Real.log x = (log ↑x).re

Proof state:
x : ℝ
hx : 0 < x
this : Real.log = fun x => (log ↑x).re
⊢ ↑x ∈ slitPlane

Tactic:
simp [hx]

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
this : Real.log = fun x => (log ↑x).re
⊢ AnalyticAt ℝ Real.log x

Tactic:
rw [this]

Result:
x : ℝ
hx : 0 < x
this : Real.log = fun x => (log ↑x).re
⊢ AnalyticAt ℝ (fun x => (log ↑x).re) x

Proof state:
x : ℝ
hx : 0 < x
⊢ AnalyticAt ℝ Real.log x

Tactic:
have : Real.log = fun x : ℝ ↦ (Complex.log x).re := by ext x; exact (Complex.log_ofReal_re x).symm

Result:
x : ℝ
hx : 0 < x
this : Real.log = fun x => (log ↑x).re
⊢ AnalyticAt ℝ Real.log x

Proof state:
case h
x✝ : ℝ
hx : 0 < x✝
x : ℝ
⊢ Real.log x = (log ↑x).re

Tactic:
exact (Complex.log_ofReal_re x).symm

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
this : Real.log = fun x => (log ↑x).re
⊢ AnalyticAt ℝ (fun x => (log ↑x).re) x

Tactic:
refine AnalyticAt.re_ofReal <| analyticAt_clog ?_

Result:
x : ℝ
hx : 0 < x
this : Real.log = fun x => (log ↑x).re
⊢ ↑x ∈ slitPlane
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem changeForm_self_apply (x : CliffordAlgebra Q) : changeForm (Q' := Q)
    changeForm.zero_proof x = x

Proof state:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm ⋯) x✝ = x✝
⊢ (changeForm ⋯) ((ι Q) m✝ * x✝) = (ι Q) m✝ * x✝

Tactic:
rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
sub_zero]

Result:
no goals

Proof state:
case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm ⋯) x✝ = x✝
hy : (changeForm ⋯) y✝ = y✝
⊢ (changeForm ⋯) (x✝ + y✝) = x✝ + y✝

Tactic:
rw [map_add, hx, hy]

Result:
no goals

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ (changeForm ⋯) x = x

Tactic:
induction x using CliffordAlgebra.left_induction with
| algebraMap => simp_rw [changeForm_algebraMap]
| add _ _ hx hy => rw [map_add, hx, hy]
| ι_mul _ _ hx => rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
    sub_zero]

Result:
no goals

Proof state:
case algebraMap
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r✝ : R
⊢ (changeForm ⋯) ((algebraMap R (CliffordAlgebra Q)) r✝) = (algebraMap R (CliffordAlgebra Q)) r✝

Tactic:
simp_rw [changeForm_algebraMap]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Frobenius.lean
theorem map_frobeniusPoly.key₂ {n i j : ℕ} (hi : i ≤ n) (hj : j < p ^ (n - i)) :
    j - v p (j + 1) + n = i + j + (n - i - v p (j + 1))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
⊢ m ≤ n - i ∧ m ≤ j

Tactic:
have hle : p ^ m ≤ j + 1 := h ▸ Nat.le_of_dvd j.succ_pos (pow_multiplicity_dvd _ _)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
hle : p ^ m ≤ j + 1
⊢ m ≤ n - i ∧ m ≤ j

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
⊢ j - v p (j + 1) + n = i + j + (n - i - v p (j + 1))

Tactic:
generalize h : v p (j + 1) = m

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
⊢ j - m + n = i + j + (n - i - m)

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j - m + n = i + j + (n - i - m)

Tactic:
rw [tsub_add_eq_add_tsub h₂, add_comm i j, add_tsub_assoc_of_le (h₁.trans (Nat.sub_le n i)),
  add_assoc, tsub_right_comm, add_comm i,
  tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi).mp h₁))]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
hle : p ^ m ≤ j + 1
⊢ m ≤ n - i ∧ m ≤ j

Tactic:
exact ⟨(Nat.pow_le_pow_iff_right hp.1.one_lt).1 (hle.trans hj),
   Nat.le_of_lt_succ ((m.lt_pow_self hp.1.one_lt).trans_le hle)⟩

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
⊢ j - m + n = i + j + (n - i - m)

Tactic:
rsuffices ⟨h₁, h₂⟩ : m ≤ n - i ∧ m ≤ j

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j - m + n = i + j + (n - i - m)

p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
⊢ m ≤ n - i ∧ m ≤ j
-- Mathlib/Order/Atoms.lean
theorem ComplementedLattice.isStronglyCoatomic' [h : IsCoatomic α] : IsStronglyAtomic α

Proof state:
α : Type u_2
inst✝³ : Lattice α
inst✝² : BoundedOrder α
inst✝¹ : IsModularLattice α
inst✝ : ComplementedLattice α
h : IsCoatomic α
⊢ IsStronglyAtomic α

Tactic:
rw [← isAtomic_iff_isCoatomic] at h

Result:
α : Type u_2
inst✝³ : Lattice α
inst✝² : BoundedOrder α
inst✝¹ : IsModularLattice α
inst✝ : ComplementedLattice α
h : IsAtomic α
⊢ IsStronglyAtomic α

Proof state:
α : Type u_2
inst✝³ : Lattice α
inst✝² : BoundedOrder α
inst✝¹ : IsModularLattice α
inst✝ : ComplementedLattice α
h : IsAtomic α
⊢ IsStronglyAtomic α

Tactic:
exact isStronglyAtomic

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem le_inf {A : C} (h f g : Subobject A) : h ≤ f → h ≤ g → h ≤ (inf.obj f).obj g :=
  Quotient.inductionOn₃' h f g
    (by
      rintro f g h ⟨k⟩ ⟨l⟩
      exact ⟨MonoOver.leInf _ _ _ k l⟩)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
h f g : Subobject A
⊢ ∀ (a₁ a₂ a₃ : MonoOver A),
    Quotient.mk'' a₁ ≤ Quotient.mk'' a₂ →
      Quotient.mk'' a₁ ≤ Quotient.mk'' a₃ → Quotient.mk'' a₁ ≤ (inf.obj (Quotient.mk'' a₂)).obj (Quotient.mk'' a₃)

Tactic:
rintro f g h ⟨k⟩ ⟨l⟩

Result:
case intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
h✝ f✝ g✝ : Subobject A
f g h : MonoOver A
k : f ⟶ g
l : f ⟶ h
⊢ Quotient.mk'' f ≤ (inf.obj (Quotient.mk'' g)).obj (Quotient.mk'' h)

Proof state:
case intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
h✝ f✝ g✝ : Subobject A
f g h : MonoOver A
k : f ⟶ g
l : f ⟶ h
⊢ Quotient.mk'' f ≤ (inf.obj (Quotient.mk'' g)).obj (Quotient.mk'' h)

Tactic:
exact ⟨MonoOver.leInf _ _ _ k l⟩

Result:
no goals
-- Mathlib/Data/DFinsupp/Multiset.lean
theorem toMultiset_sup : toMultiset (f ⊔ g) = toMultiset f∪ toMultiset g :=
  Multiset.toDFinsupp_injective <| by simp

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ Multiset.toDFinsupp (toMultiset (f ⊔ g)) = Multiset.toDFinsupp (toMultiset f ∪ toMultiset g)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/DirectSum/Decomposition.lean
theorem sum_support_decompose [∀ (i) (x : ℳ i), Decidable (x ≠ 0)] (r : M) :
    (∑ i ∈ (decompose ℳ r).support, (decompose ℳ r i : M)) = r

Proof state:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) r), ↑(((decompose ℳ) r) i) =
    ∑ i ∈ DFinsupp.support ((decompose ℳ) r), (decompose ℳ).symm ((of (fun i => ↥(ℳ i)) i) (((decompose ℳ) r) i))

Tactic:
simp_rw [decompose_symm_of]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) r), ↑(((decompose ℳ) r) i) =
    (decompose ℳ).symm (∑ i ∈ DFinsupp.support ((decompose ℳ) r), (of (fun i => ↥(ℳ i)) i) (((decompose ℳ) r) i))

Tactic:
rw [decompose_symm_sum]

Result:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) r), ↑(((decompose ℳ) r) i) =
    ∑ i ∈ DFinsupp.support ((decompose ℳ) r), (decompose ℳ).symm ((of (fun i => ↥(ℳ i)) i) (((decompose ℳ) r) i))

Proof state:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) r), ↑(((decompose ℳ) r) i) = r

Tactic:
conv_rhs =>
  rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (decompose ℳ r)]

Result:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) r), ↑(((decompose ℳ) r) i) =
    (decompose ℳ).symm (∑ i ∈ DFinsupp.support ((decompose ℳ) r), (of (fun i => ↥(ℳ i)) i) (((decompose ℳ) r) i))
-- Mathlib/Data/Seq/Seq.lean
theorem map_join' (f : α → β) (S) : Seq.map f (Seq.join S) = Seq.join (Seq.map (map f) S)

Proof state:
α : Type u
β : Type v
f : α → β
S✝ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join
S : Seq (Seq1 α)
⊢ match (Seq.map f S.join).destruct, (Seq.map (map f) S).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ s_1 S, s = s_1.append (Seq.map f S.join) ∧ s' = s_1.append (Seq.map (map f) S).join
  | x, x_1 => False

Tactic:
cases S <;> simp

Result:
case cons
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join
x✝ : Seq1 α
s✝ : Seq (Seq1 α)
⊢ match (Seq.map f (Seq.cons x✝ s✝).join).destruct, (Seq.cons (map f x✝) (Seq.map (map f) s✝)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ s_1 S, s = s_1.append (Seq.map f S.join) ∧ s' = s_1.append (Seq.map (map f) S).join
  | x, x_1 => False
-- Mathlib/Data/List/Permutation.lean
theorem nodup_permutations'Aux_iff {s : List α} {x : α} : Nodup (permutations'Aux x s) ↔ x ∉ s

Proof state:
case h.e'_3.h.e'_3
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H✝ : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
hl : (insertIdx k x s).length = (insertIdx (k + 1) x s).length
m : ℕ
hn✝ : k.succ + m + 1 < (insertIdx k x s).length
hn : (k + m).succ < s.length
hn' : k.succ + m + 1 < (insertIdx (k + 1) x s).length
H : k < k.succ + m + 1
H' : k.succ < k.succ + m + 1
⊢ ⟨k + 1 + m, ?intro.mk.a.inr.inr.inr.intro.hk'⟩ = ⟨k + m.succ, ⋯⟩

Tactic:
simp [Nat.add_left_comm, Nat.add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_mkArray_nil {c} :
    toListModel (mkArray c (AssocList.nil : AssocList α β)) = []

Proof state:
α : Type u
β : α → Type v
c d : Nat
⊢ flatMap AssocList.toList (replicate d AssocList.nil) = []

Tactic:
induction d <;> simp_all [List.replicate]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
c : Nat
⊢ toListModel (mkArray c AssocList.nil) = []

Tactic:
suffices ∀ d, (List.replicate d AssocList.nil).flatMap AssocList.toList = [] from this _

Result:
α : Type u
β : α → Type v
c : Nat
⊢ ∀ (d : Nat), flatMap AssocList.toList (replicate d AssocList.nil) = []

Proof state:
α : Type u
β : α → Type v
c : Nat
⊢ ∀ (d : Nat), flatMap AssocList.toList (replicate d AssocList.nil) = []

Tactic:
intro d

Result:
α : Type u
β : α → Type v
c d : Nat
⊢ flatMap AssocList.toList (replicate d AssocList.nil) = []
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : ‖x‖ / Real.Angle.tan (o.oangle y (y - x)) = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖x‖ / (o.oangle y (y - x)).tan = ‖y‖

Tactic:
have hs : (o.oangle y (y - x)).sign = 1 := by
  rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ ‖x‖ / (o.oangle y (y - x)).tan = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ ‖x‖ / (o.oangle y (y - x)).tan = ‖y‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  InnerProductGeometry.norm_div_tan_angle_sub_of_inner_eq_zero
    (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inr (o.left_ne_zero_of_oangle_eq_pi_div_two h))]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).sign = 1

Tactic:
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatten_flatten {L : Vector (Vector (Vector α n) m) k} :
    flatten (flatten L) = (flatten (map flatten L)).cast (by simp [Nat.mul_assoc])

Proof state:
case of
α : Type u_1
n m k : Nat
xss : Array (Array (Array α))
h₁ : xss.size = k
h₂ : ∀ (xs : Array (Array α)), xs ∈ xss → xs.size = m
h₃ : ∀ (xs : Array (Array α)), xs ∈ xss → ∀ (x : Array α), x ∈ xs → x.size = n
⊢ {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ =>
                  {
                    toArray :=
                      Array.map
                        (fun x =>
                          match x with
                          | ⟨x, m'⟩ => { toArray := x, size_toArray := ⋯ })
                        xs.attach,
                    size_toArray := ⋯ })
              xss.attach,
          size_toArray := ⋯ }.flatten.flatten =
    Vector.cast ⋯
      (map flatten
          {
            toArray :=
              Array.map
                (fun x =>
                  match x with
                  | ⟨xs, m_1⟩ =>
                    {
                      toArray :=
                        Array.map
                          (fun x =>
                            match x with
                            | ⟨x, m'⟩ => { toArray := x, size_toArray := ⋯ })
                          xs.attach,
                      size_toArray := ⋯ })
                xss.attach,
            size_toArray := ⋯ }).flatten

Tactic:
simp [Array.map_attach, Array.flatten_flatten, Array.map_pmap]

Result:
no goals

Proof state:
α : Type ?u.306895
n m k : Nat
L : Vector (Vector (Vector α n) m) k
⊢ k * (m * n) = k * m * n

Tactic:
simp [Nat.mul_assoc]

Result:
no goals

Proof state:
α : Type u_1
n m k : Nat
L : Vector (Vector (Vector α n) m) k
⊢ L.flatten.flatten = Vector.cast ⋯ (map flatten L).flatten

Tactic:
induction L using vector₃_induction with
| of xss h₁ h₂ h₃ =>
  simp [Array.map_attach, Array.flatten_flatten, Array.map_pmap]

Result:
no goals