harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
theorem toQuaternion_star (c : CliffordAlgebra (Q c₁ c₂)) :
    toQuaternion (star c) = star (toQuaternion c)

Proof state:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
c : CliffordAlgebra (Q c₁ c₂)
⊢ toQuaternion (star c) = star (toQuaternion c)

Tactic:
simp only [CliffordAlgebra.star_def']

Result:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
c : CliffordAlgebra (Q c₁ c₂)
⊢ toQuaternion (involute (reverse c)) = star (toQuaternion c)

Proof state:
case add
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
x₁ x₂ : CliffordAlgebra (Q c₁ c₂)
hx₁ : toQuaternion (involute (reverse x₁)) = star (toQuaternion x₁)
hx₂ : toQuaternion (involute (reverse x₂)) = star (toQuaternion x₂)
⊢ toQuaternion (involute (reverse (x₁ + x₂))) = star (toQuaternion (x₁ + x₂))

Tactic:
simp [hx₁, hx₂]

Result:
no goals

Proof state:
case mul
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
x₁ x₂ : CliffordAlgebra (Q c₁ c₂)
hx₁ : toQuaternion (involute (reverse x₁)) = star (toQuaternion x₁)
hx₂ : toQuaternion (involute (reverse x₂)) = star (toQuaternion x₂)
⊢ toQuaternion (involute (reverse (x₁ * x₂))) = star (toQuaternion (x₁ * x₂))

Tactic:
simp [hx₁, hx₂]

Result:
no goals

Proof state:
case algebraMap
R : Type u_1
inst✝ : CommRing R
c₁ c₂ r : R
⊢ toQuaternion (involute (reverse ((algebraMap R (CliffordAlgebra (Q c₁ c₂))) r))) =
    star (toQuaternion ((algebraMap R (CliffordAlgebra (Q c₁ c₂))) r))

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
c : CliffordAlgebra (Q c₁ c₂)
⊢ toQuaternion (involute (reverse c)) = star (toQuaternion c)

Tactic:
induction c using CliffordAlgebra.induction with
| algebraMap r => simp
| ι x => simp
| mul x₁ x₂ hx₁ hx₂ => simp [hx₁, hx₂]
| add x₁ x₂ hx₁ hx₂ => simp [hx₁, hx₂]

Result:
no goals

Proof state:
case ι
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
x : R × R
⊢ toQuaternion (involute (reverse ((ι (Q c₁ c₂)) x))) = star (toQuaternion ((ι (Q c₁ c₂)) x))

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem reflection_orthogonal_apply (v : E) : reflection Kᗮ v = -reflection K v

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
⊢ 2 • (v - ↑((orthogonalProjection K) v)) - v = v - 2 • ↑((orthogonalProjection K) v)

Tactic:
abel

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
⊢ (reflection Kᗮ) v = -(reflection K) v

Tactic:
simp [reflection_apply]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
⊢ 2 • (v - ↑((orthogonalProjection K) v)) - v = v - 2 • ↑((orthogonalProjection K) v)
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombinationOn_range (s : Set α) :
    LinearMap.range (linearCombinationOn α M R v s) = ⊤

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ span R (v '' s) ≤ map (linearCombination R v) (supported R R s)

Tactic:
exact (span_image_eq_map_linearCombination _ _).le

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ LinearMap.range (linearCombinationOn α M R v s) = ⊤

Tactic:
rw [linearCombinationOn, LinearMap.range_eq_map, LinearMap.map_codRestrict,
  ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top, LinearMap.range_comp,
  range_subtype]

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ span R (v '' s) ≤ map (linearCombination R v) (supported R R s)
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsVanKampenColimit.precompose_isIso {F G : J ⥤ C} (α : F ⟶ G) [IsIso α]
    {c : Cocone G} (hc : IsVanKampenColimit c) :
    IsVanKampenColimit ((Cocones.precompose α).obj c)

Proof state:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
F G : J ⥤ C
α : F ⟶ G
inst✝ : IsIso α
c : Cocone G
hc : IsVanKampenColimit c
⊢ IsVanKampenColimit ((Cocones.precompose α).obj c)

Tactic:
intros F' c' α' f e hα

Result:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
F G : J ⥤ C
α : F ⟶ G
inst✝ : IsIso α
c : Cocone G
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocones.precompose α).obj c).pt
e : α' ≫ ((Cocones.precompose α).obj c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α'
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocones.precompose α).obj c).ι.app j)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
theorem go_val_eq_bitblast (aig : AIG BVBit) (expr : BVExpr w) :
    (go aig expr).val = bitblast aig expr

Proof state:
w : Nat
aig : AIG BVBit
expr : BVExpr w
⊢ (go aig expr).val = bitblast aig expr

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem eq_of_perm_of_sorted [IsAntisymm α r] {l₁ l₂ : List α} (hp : l₁ ~ l₂) (hs₁ : Sorted r l₁)
    (hs₂ : Sorted r l₂) : l₁ = l₂

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ l₂ : List α
hp : l₁ ~ l₂
hs₁ : Sorted r l₁
hs₂ : Sorted r l₂
⊢ l₁ = l₂

Tactic:
induction' hs₁ with a l₁ h₁ hs₁ IH generalizing l₂

Result:
case nil
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ l₂ : List α
hp : [] ~ l₂
hs₂ : Sorted r l₂
⊢ [] = l₂

case cons
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁✝ : List α
a : α
l₁ : List α
h₁ : ∀ a' ∈ l₁, r a a'
hs₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
l₂ : List α
hp : a :: l₁ ~ l₂
hs₂ : Sorted r l₂
⊢ a :: l₁ = l₂

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁✝ : List α
a : α
l₁ : List α
h₁ : ∀ a' ∈ l₁, r a a'
hs₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
u₂ v₂ : List α
hp : a :: l₁ ~ u₂ ++ a :: v₂
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
hp' : l₁ ~ u₂ ++ v₂
⊢ u₂ ++ v₂ <+ u₂ ++ a :: v₂

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem natDegree_pow_X_add_C [Nontrivial R] (n : ℕ) (r : R) : ((X + C r) ^ n).natDegree = n

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ ((X + C r) ^ n).natDegree = n

Tactic:
rw [(monic_X_add_C r).natDegree_pow, natDegree_X_add_C, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_reverse {x : BitVec w} :
    (x.reverse).msb = x.getLsbD 0 :=
  by rw [BitVec.msb, getMsbD_reverse]

Proof state:
w : Nat
x : BitVec w
⊢ x.reverse.msb = x.getLsbD 0

Tactic:
rw [BitVec.msb, getMsbD_reverse]

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem _root_.Squarefree.natFactorization_le_one {n : ℕ} (p : ℕ) (hn : Squarefree n) :
    n.factorization p ≤ 1

Proof state:
case pos
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1 ∨ IsUnit p
⊢ n.factorization p ≤ 1

Tactic:
rw [← multiplicity_eq_factorization hp hn']

Result:
case pos
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1 ∨ IsUnit p
⊢ multiplicity p n ≤ 1

Proof state:
case inr
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
⊢ n.factorization p ≤ 1

Tactic:
by_cases hp : p.Prime

Result:
case pos
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
⊢ n.factorization p ≤ 1

case neg
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ n.factorization p ≤ 1

Proof state:
case neg
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

Result:
no goals

Proof state:
n p : ℕ
hn : Squarefree n
⊢ n.factorization p ≤ 1

Tactic:
rcases eq_or_ne n 0 with (rfl | hn')

Result:
case inl
p : ℕ
hn : Squarefree 0
⊢ (factorization 0) p ≤ 1

case inr
n p : ℕ
hn : Squarefree n
hn' : n ≠ 0
⊢ n.factorization p ≤ 1

Proof state:
case inr
n p : ℕ
hn : Squarefree n
hn' : n ≠ 0
⊢ n.factorization p ≤ 1

Tactic:
rw [squarefree_iff_emultiplicity_le_one] at hn

Result:
case inr
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
⊢ n.factorization p ≤ 1

Proof state:
case pos
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1
⊢ multiplicity p n ≤ 1

Tactic:
exact multiplicity_le_of_emultiplicity_le this

Result:
no goals

Proof state:
case pos
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
⊢ n.factorization p ≤ 1

Tactic:
have := hn p

Result:
case pos
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1 ∨ IsUnit p
⊢ n.factorization p ≤ 1

Proof state:
case pos
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1 ∨ IsUnit p
⊢ multiplicity p n ≤ 1

Tactic:
simp only [Nat.isUnit_iff, hp.ne_one, or_false] at this

Result:
case pos
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1
⊢ multiplicity p n ≤ 1

Proof state:
case inl
p : ℕ
hn : Squarefree 0
⊢ (factorization 0) p ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
case neg
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ n.factorization p ≤ 1

Tactic:
rw [factorization_eq_zero_of_non_prime _ hp]

Result:
case neg
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ 0 ≤ 1
-- Mathlib/Topology/Order/LawsonTopology.lean
lemma scottHausdorff_le_isLawson : scottHausdorff α univ ≤ L

Proof state:
α : Type u_1
inst✝¹ : Preorder α
L : TopologicalSpace α
inst✝ : IsLawson α
⊢ scottHausdorff α univ ≤ lawson α

Tactic:
exact scottHausdorff_le_lawson

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
L : TopologicalSpace α
inst✝ : IsLawson α
⊢ scottHausdorff α univ ≤ L

Tactic:
rw [@IsLawson.topology_eq_lawson α _ L _]

Result:
α : Type u_1
inst✝¹ : Preorder α
L : TopologicalSpace α
inst✝ : IsLawson α
⊢ scottHausdorff α univ ≤ lawson α
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
    (h : ∀ x, f x = g x) : f = g

Proof state:
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
extfunApp : Quot eqv → (x : α) → β x := fun f x => f.liftOn (fun f => f x) ⋯
⊢ f = g

Tactic:
show extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)

Result:
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
extfunApp : Quot eqv → (x : α) → β x := fun f x => f.liftOn (fun f => f x) ⋯
⊢ extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)

Proof state:
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
⊢ f = g

Tactic:
let extfunApp (f : Quot eqv) (x : α) : β x :=
  Quot.liftOn f
    (fun (f : ∀ (x : α), β x) => f x)
    (fun _ _ h => h x)

Result:
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
extfunApp : Quot eqv → (x : α) → β x := fun f x => f.liftOn (fun f => f x) ⋯
⊢ f = g

Proof state:
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
extfunApp : Quot eqv → (x : α) → β x := fun f x => f.liftOn (fun f => f x) ⋯
⊢ extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)

Tactic:
exact congrArg extfunApp (Quot.sound h)

Result:
no goals

Proof state:
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
⊢ f = g

Tactic:
let eqv (f g : (x : α) → β x) := ∀ x, f x = g x

Result:
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
⊢ f = g
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_sub_left (x y z : E) : ⟪x - y, z⟫ = ⟪x, z⟫ - ⟪y, z⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : E
⊢ ⟪x - y, z⟫_𝕜 = ⟪x, z⟫_𝕜 - ⟪y, z⟫_𝕜

Tactic:
simp [sub_eq_add_neg, inner_add_left]

Result:
no goals
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff [IsPrime I] (hIJ : I ≤ J) {r : S}
    (hr : r ∈ (J : Set S) \ I) {p : R[X]} (p_ne_zero : p.map (Quotient.mk (I.comap f)) ≠ 0)
    (hpI : p.eval₂ f r ∈ I) : ∃ i, p.coeff i ∈ (J.comap f : Set R) \ I.comap f

Proof state:
case intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)

Tactic:
have rbar_mem_J : Ideal.Quotient.mk I r ∈ J.map (Ideal.Quotient.mk I) := mem_map_of_mem _ hrJ

Result:
case intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Basic.lean
theorem mem_eraseIdx_iff_getElem {x : α} :
    ∀ {l} {k}, x ∈ eraseIdx l k ↔ ∃ i h, i ≠ k ∧ l[i]'h = x
  | [], _ => by
    simp only [eraseIdx, not_mem_nil, false_iff]
    rintro ⟨i, h, -⟩
    exact Nat.not_lt_zero _ h
  | a::l, 0 => by simp [mem_iff_getElem, Nat.succ_lt_succ_iff]
  | a::l, k+1 => by
    rw [← Nat.or_exists_add_one]
    simp [mem_eraseIdx_iff_getElem, @eq_comm _ a, succ_inj', Nat.succ_lt_succ_iff]

Proof state:
α : Type u_1
x : α
x✝ : Nat
⊢ x ∈ [].eraseIdx x✝ ↔ ∃ i h, i ≠ x✝ ∧ [][i] = x

Tactic:
simp only [eraseIdx, not_mem_nil, false_iff]

Result:
α : Type u_1
x : α
x✝ : Nat
⊢ ¬∃ i h, i ≠ x✝ ∧ [][i] = x

Proof state:
α : Type u_1
x : α
x✝ : Nat
⊢ ¬∃ i h, i ≠ x✝ ∧ [][i] = x

Tactic:
rintro ⟨i, h, -⟩

Result:
case intro.intro
α : Type u_1
x : α
x✝ i : Nat
h : i < [].length
⊢ False

Proof state:
case intro.intro
α : Type u_1
x : α
x✝ i : Nat
h : i < [].length
⊢ False

Tactic:
exact Nat.not_lt_zero _ h

Result:
no goals

Proof state:
α : Type u_1
x a : α
l : List α
⊢ x ∈ (a :: l).eraseIdx 0 ↔ ∃ i h, i ≠ 0 ∧ (a :: l)[i] = x

Tactic:
simp [mem_iff_getElem, Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
α : Type u_1
x a : α
l : List α
k : Nat
⊢ x ∈ (a :: l).eraseIdx (k + 1) ↔ (∃ h, 0 ≠ k + 1 ∧ (a :: l)[0] = x) ∨ ∃ n h, n + 1 ≠ k + 1 ∧ (a :: l)[n + 1] = x

Tactic:
simp [mem_eraseIdx_iff_getElem, @eq_comm _ a, succ_inj', Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
α : Type u_1
x a : α
l : List α
k : Nat
⊢ x ∈ (a :: l).eraseIdx (k + 1) ↔ ∃ i h, i ≠ k + 1 ∧ (a :: l)[i] = x

Tactic:
rw [← Nat.or_exists_add_one]

Result:
α : Type u_1
x a : α
l : List α
k : Nat
⊢ x ∈ (a :: l).eraseIdx (k + 1) ↔ (∃ h, 0 ≠ k + 1 ∧ (a :: l)[0] = x) ∨ ∃ n h, n + 1 ≠ k + 1 ∧ (a :: l)[n + 1] = x
-- Mathlib/Data/Matrix/Mul.lean
theorem diagonal_dotProduct (i : m) : diagonal v i ⬝ᵥ w = v i * w i

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
⊢ diagonal v i ⬝ᵥ w = v i * w i

Tactic:
have : ∀ j ≠ i, diagonal v i j * w j = 0 := fun j hij => by
  simp [diagonal_apply_ne' _ hij]

Result:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ diagonal v i ⬝ᵥ w = v i * w i

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i j : m
hij : j ≠ i
⊢ diagonal v i j * w j = 0

Tactic:
simp [diagonal_apply_ne' _ hij]

Result:
no goals

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ diagonal v i ⬝ᵥ w = v i * w i

Tactic:
convert Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem map_le_comap_of_inv_on [RingHomClass G S R] (g : G) (I : Ideal R)
    (hf : Set.LeftInvOn g f I) :
    I.map f ≤ I.comap g

Proof state:
case intro.intro
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
x : R
hx : x ∈ ↑I
⊢ f x ∈ ↑(comap g I)

Tactic:
rw [SetLike.mem_coe, mem_comap, hf hx]

Result:
case intro.intro
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
x : R
hx : x ∈ ↑I
⊢ x ∈ I

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
⊢ ⇑f '' ↑I ⊆ ↑(comap g I)

Tactic:
rintro x ⟨x, hx, rfl⟩

Result:
case intro.intro
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
x : R
hx : x ∈ ↑I
⊢ f x ∈ ↑(comap g I)

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
⊢ map f I ≤ comap g I

Tactic:
refine Ideal.span_le.2 ?_

Result:
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
⊢ ⇑f '' ↑I ⊆ ↑(comap g I)

Proof state:
case intro.intro
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
x : R
hx : x ∈ ↑I
⊢ x ∈ I

Tactic:
exact hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attachWith_map {l : Array α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ l.map f → P b} :
    (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
      fun ⟨x, h⟩ => ⟨f x, h⟩

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → β
P : β → Prop
H : ∀ (b : β), b ∈ map f l → P b
⊢ (map f l).attachWith P H =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, h⟩)
      (l.attachWith (P ∘ f) ⋯)

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
P : β → Prop
toList✝ : List α
H : ∀ (b : β), b ∈ map f { toList := toList✝ } → P b
⊢ (map f { toList := toList✝ }).attachWith P H =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, h⟩)
      ({ toList := toList✝ }.attachWith (P ∘ f) ⋯)

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
P : β → Prop
toList✝ : List α
H : ∀ (b : β), b ∈ map f { toList := toList✝ } → P b
⊢ (map f { toList := toList✝ }).attachWith P H =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, h⟩)
      ({ toList := toList✝ }.attachWith (P ∘ f) ⋯)

Tactic:
simp [List.attachWith_map]

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem tendsto_Lp_finite_of_tendstoInMeasure [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ ∞)
    (hf : ∀ n, AEStronglyMeasurable (f n) μ) (hg : MemLp g p μ) (hui : UnifIntegrable f p μ)
    (hfg : TendstoInMeasure μ f atTop g) : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : TendstoInMeasure μ f atTop g
⊢ Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
refine tendsto_of_subseq_tendsto fun ns hns => ?_

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
⊢ ∃ ms, Tendsto (fun n => eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
ms : ℕ → ℕ
left✝ : StrictMono ms
hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns (ms i)) x) atTop (𝓝 (g x))
⊢ ∃ ms, Tendsto (fun n => eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Tactic:
exact ⟨ms,
  tendsto_Lp_finite_of_tendsto_ae hp hp' (fun _ => hf _) hg (fun ε hε =>
    let ⟨δ, hδ, hδ'⟩ := hui hε
    ⟨δ, hδ, fun i s hs hμs => hδ' _ s hs hμs⟩)
    hms'⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
⊢ ∃ ms, Tendsto (fun n => eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Tactic:
obtain ⟨ms, _, hms'⟩ := TendstoInMeasure.exists_seq_tendsto_ae fun ε hε => (hfg ε hε).comp hns

Result:
case intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
ms : ℕ → ℕ
left✝ : StrictMono ms
hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns (ms i)) x) atTop (𝓝 (g x))
⊢ ∃ ms, Tendsto (fun n => eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)