harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem fderivWithin_inv' {s : Set R} {x : R} (hx : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun x => x⁻¹) s x = -mulLeftRight 𝕜 R x⁻¹ x⁻¹

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
R : Type u_5
inst✝¹ : NormedDivisionRing R
inst✝ : NormedAlgebra 𝕜 R
s : Set R
x : R
hx : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun x => x⁻¹) s x = -((mulLeftRight 𝕜 R) x⁻¹) x⁻¹

Tactic:
rw [DifferentiableAt.fderivWithin (differentiableAt_inv hx) hxs]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
R : Type u_5
inst✝¹ : NormedDivisionRing R
inst✝ : NormedAlgebra 𝕜 R
s : Set R
x : R
hx : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 Inv.inv x = -((mulLeftRight 𝕜 R) x⁻¹) x⁻¹

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
R : Type u_5
inst✝¹ : NormedDivisionRing R
inst✝ : NormedAlgebra 𝕜 R
s : Set R
x : R
hx : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 Inv.inv x = -((mulLeftRight 𝕜 R) x⁻¹) x⁻¹

Tactic:
exact fderiv_inv' hx

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc]
lemma sndX_inrX (i : ι) (hi : ¬ c.Rel i (c.next i)) :
    sndX φ i ≫ inrX φ i = 𝟙 _

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
⊢ sndX φ i ≫ inrX φ i = 𝟙 (X φ i)

Tactic:
dsimp [sndX, inrX]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
⊢ ((if hi : c.Rel i (c.next i) then (XIsoBiprod φ i (c.next i) hi).hom ≫ biprod.snd else (XIso φ i hi).hom) ≫
      if hi : c.Rel i (c.next i) then biprod.inr ≫ (XIsoBiprod φ i (c.next i) hi).inv else (XIso φ i hi).inv) =
    𝟙 (X φ i)

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
⊢ ((if hi : c.Rel i (c.next i) then (XIsoBiprod φ i (c.next i) hi).hom ≫ biprod.snd else (XIso φ i hi).hom) ≫
      if hi : c.Rel i (c.next i) then biprod.inr ≫ (XIsoBiprod φ i (c.next i) hi).inv else (XIso φ i hi).inv) =
    𝟙 (X φ i)

Tactic:
simp only [dif_neg hi, Iso.hom_inv_id]

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem comp {g : B →+* C} {f : A →+* B} (hg : g.FiniteType) (hf : f.FiniteType) :
    (g.comp f).FiniteType

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.FiniteType
hf : f.FiniteType
⊢ (g.comp f).FiniteType

Tactic:
algebraize_only [f, g, g.comp f]

Result:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.FiniteType
hf : f.FiniteType
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
⊢ (g.comp f).FiniteType

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.FiniteType
hf : f.FiniteType
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
⊢ (g.comp f).FiniteType

Tactic:
exact Algebra.FiniteType.trans hf hg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lcm.lean
theorem lcm_comm (m n : Nat) : lcm m n = lcm n m

Proof state:
m n : Nat
⊢ m.lcm n = n.lcm m

Tactic:
rw [lcm, lcm, Nat.mul_comm n m, gcd_comm n m]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem ofMulEquivOfDom_id :
    f.ofMulEquivOfDom
        (show S.map (MulEquiv.refl M).toMonoidHom = S from
          Submonoid.ext fun x ↦ ⟨fun ⟨_, hy, h⟩ ↦ h ▸ hy, fun h ↦ ⟨x, h, rfl⟩⟩) = f

Proof state:
case h
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x✝ : M
⊢ (f.ofMulEquivOfDom ⋯).toMap x✝ = f.toMap x✝

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
⊢ f.ofMulEquivOfDom ⋯ = f

Tactic:
ext

Result:
case h
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x✝ : M
⊢ (f.ofMulEquivOfDom ⋯).toMap x✝ = f.toMap x✝
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
/-- In a flatten, dropping all the elements up to an index which is the sum of the lengths of the
first `i` sublists, is the same as taking the join after dropping the first `i` sublists. -/
lemma drop_sum_flatten (L : List (List α)) (i : ℕ) :
    L.flatten.drop ((L.map length).take i).sum = (L.drop i).flatten

Proof state:
case nil
α : Type u_2
i : ℕ
⊢ drop (take i (map length [])).sum [].flatten = (drop i []).flatten

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
L : List (List α)
i : ℕ
⊢ drop (take i (map length L)).sum L.flatten = (drop i L).flatten

Tactic:
induction L generalizing i

Result:
case nil
α : Type u_2
i : ℕ
⊢ drop (take i (map length [])).sum [].flatten = (drop i []).flatten

case cons
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (take i (map length tail✝)).sum tail✝.flatten = (drop i tail✝).flatten
i : ℕ
⊢ drop (take i (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (drop i (head✝ :: tail✝)).flatten

Proof state:
case cons
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (take i (map length tail✝)).sum tail✝.flatten = (drop i tail✝).flatten
i : ℕ
⊢ drop (take i (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (drop i (head✝ :: tail✝)).flatten

Tactic:
cases i <;> simp [take_append, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem snd_lt_add_of_mem_zipIdx {x : α × Nat} {l : Vector α n} {k : Nat} (h : x ∈ zipIdx l k) :
    x.2 < k + n

Proof state:
case intro.intro
α : Type u_1
n : Nat
l : Vector α n
k i : Nat
h' : i < n
h : (l.zipIdx k)[i] ∈ l.zipIdx k
⊢ (l.zipIdx k)[i].snd < k + n

Tactic:
simpa using h'

Result:
no goals

Proof state:
α : Type u_1
n : Nat
x : α × Nat
l : Vector α n
k : Nat
h : x ∈ l.zipIdx k
⊢ x.snd < k + n

Tactic:
rcases mem_iff_getElem.1 h with ⟨i, h', rfl⟩

Result:
case intro.intro
α : Type u_1
n : Nat
l : Vector α n
k i : Nat
h' : i < n
h : (l.zipIdx k)[i] ∈ l.zipIdx k
⊢ (l.zipIdx k)[i].snd < k + n
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem coe_lt_degree {p : R[X]} {n : ℕ} : (n : WithBot ℕ) < degree p ↔ n < natDegree p

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p = 0
⊢ ↑n < p.degree ↔ n < p.natDegree

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬p = 0
⊢ ↑n < p.degree ↔ n < p.natDegree

Tactic:
simp [degree_eq_natDegree h, Nat.cast_lt]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ↑n < p.degree ↔ n < p.natDegree

Tactic:
by_cases h : p = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p = 0
⊢ ↑n < p.degree ↔ n < p.natDegree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬p = 0
⊢ ↑n < p.degree ↔ n < p.natDegree
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem conjugateEquiv_symm_id : (conjugateEquiv adj₁ adj₁).symm (𝟙 _) = 𝟙 _

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ : C ⥤ D
R₁ : D ⥤ C
adj₁ : L₁ ⊣ R₁
⊢ (conjugateEquiv adj₁ adj₁).symm (𝟙 R₁) = 𝟙 L₁

Tactic:
rw [Equiv.symm_apply_eq]

Result:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ : C ⥤ D
R₁ : D ⥤ C
adj₁ : L₁ ⊣ R₁
⊢ 𝟙 R₁ = (conjugateEquiv adj₁ adj₁) (𝟙 L₁)

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ : C ⥤ D
R₁ : D ⥤ C
adj₁ : L₁ ⊣ R₁
⊢ 𝟙 R₁ = (conjugateEquiv adj₁ adj₁) (𝟙 L₁)

Tactic:
simp only [conjugateEquiv_id]

Result:
no goals
-- Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean
@[to_additive]
lemma hom_inv_apply {A B : ProfiniteGrp.{u}} (e : A ≅ B) (x : B) : e.hom (e.inv x) = x

Proof state:
A B : ProfiniteGrp.{u}
e : A ≅ B
x : ↑B.toProfinite.toTop
⊢ (Hom.hom e.hom) ((Hom.hom e.inv) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Prod.lean
theorem prod_top : (prod ⊤ ⊤ : Subalgebra R (A × B)) = ⊤

Proof state:
case h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : A × B
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ⊤.prod ⊤ = ⊤

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : A × B
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem invRev_length : (invRev L₁).length = L₁.length

Proof state:
α : Type u
L₁ : List (α × Bool)
⊢ (invRev L₁).length = L₁.length

Tactic:
simp [invRev]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem orderOf {g : Perm α} (ht : IsThreeCycle g) : orderOf g = 3

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ _root_.orderOf g = 3

Tactic:
rw [← lcm_cycleType, ht.cycleType, Multiset.lcm_singleton, normalize_eq]

Result:
no goals
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma singleObjOpcyclesSelfIso_hom_naturality :
    (singleObjOpcyclesSelfIso c j A).hom ≫ opcyclesMap ((single C c j).map f) j  =
      f ≫ (singleObjOpcyclesSelfIso c j B).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (singleObjOpcyclesSelfIso c j A).hom ≫ opcyclesMap ((single C c j).map f) j = f ≫ (singleObjOpcyclesSelfIso c j B).hom

Tactic:
rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
  singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, p_opcyclesMap,
  single_map_f_self, assoc, assoc, singleObjCyclesSelfIso_hom,
  singleObjOpcyclesSelfIso_hom, assoc]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem apriori_dist_iterate_fixedPoint_le (x n) :
    dist (f^[n] x) (fixedPoint f hf) ≤ dist x (f x) * (K : ℝ) ^ n / (1 - K) :=
  calc
    _ ≤ dist (f^[n] x) (f^[n + 1] x) / (1 - K) := hf.aposteriori_dist_iterate_fixedPoint_le x n
    _ ≤ _

Proof state:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist (f^[n] x) (f^[n + 1] x) / (1 - ↑K) ≤ dist x (f x) * ↑K ^ n / (1 - ↑K)

Tactic:
gcongr

Result:
case hc
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ 0 ≤ 1 - ↑K

case hab
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * ↑K ^ n

Proof state:
case hc
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ 0 ≤ 1 - ↑K

case hab
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * ↑K ^ n

Tactic:
exacts [hf.one_sub_K_pos.le, hf.toLipschitzWith.dist_iterate_succ_le_geometric x n]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem mul_one (k : Fin (n + 1)) : k * 1 = k

Proof state:
n : Nat
k : Fin (0 + 1)
⊢ k * 1 = k

Tactic:
exact Subsingleton.elim (α := Fin 1) ..

Result:
no goals

Proof state:
n : Nat
k : Fin (n + 1)
⊢ k * 1 = k

Tactic:
match n with
| 0 => exact Subsingleton.elim (α := Fin 1) ..
| n+1 => simp [Fin.ext_iff, mul_def, Nat.mod_eq_of_lt (is_lt k)]

Result:
no goals

Proof state:
n✝ n : Nat
k : Fin (n + 1 + 1)
⊢ k * 1 = k

Tactic:
simp [Fin.ext_iff, mul_def, Nat.mod_eq_of_lt (is_lt k)]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem splitLower_ne_splitUpper (I : Box ι) (i : ι) (x : ℝ) :
    I.splitLower i x ≠ I.splitUpper i x

Proof state:
case inr
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h✝ : I.lower i < x
⊢ I.splitLower i x ≠ I.splitUpper i x

Tactic:
refine (disjoint_splitLower_splitUpper I i x).ne ?_

Result:
case inr
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h✝ : I.lower i < x
⊢ I.splitLower i x ≠ ⊥

Proof state:
case inl
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ≤ I.lower i
⊢ ⊥ ≠ ↑I

Tactic:
exact WithBot.bot_ne_coe

Result:
no goals

Proof state:
case inl
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ≤ I.lower i
⊢ I.splitLower i x ≠ I.splitUpper i x

Tactic:
rw [splitUpper_eq_self.2 h, splitLower_eq_bot.2 h]

Result:
case inl
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ≤ I.lower i
⊢ ⊥ ≠ ↑I

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitLower i x ≠ I.splitUpper i x

Tactic:
rcases le_or_lt x (I.lower i) with h | _

Result:
case inl
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ≤ I.lower i
⊢ I.splitLower i x ≠ I.splitUpper i x

case inr
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h✝ : I.lower i < x
⊢ I.splitLower i x ≠ I.splitUpper i x

Proof state:
case inr
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h✝ : I.lower i < x
⊢ I.splitLower i x ≠ ⊥

Tactic:
rwa [Ne, splitLower_eq_bot, not_le]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem list_findIdx {f : α → List β} {p : α → β → Bool}
    (hf : Primrec f) (hp : Primrec₂ p) : Primrec fun a => (f a).findIdx (p a) :=
  (list_foldr hf (const 0) <|
        to₂ <| cond (hp.comp fst <| fst.comp snd) (const 0) (succ.comp <| snd.comp snd)).of_eq
    fun a => by dsimp; induction f a <;> simp [List.findIdx_cons, *]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
⊢ List.foldr (fun b s => bif p (a, b, s).1 (a, b, s).2.1 then 0 else (a, b, s).2.2.succ) 0 (f a) =
    List.findIdx (p a) (f a)

Tactic:
dsimp

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
⊢ List.foldr (fun b s => bif p a b then 0 else s + 1) 0 (f a) = List.findIdx (p a) (f a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
⊢ List.foldr (fun b s => bif p a b then 0 else s + 1) 0 (f a) = List.findIdx (p a) (f a)

Tactic:
induction f a <;> simp [List.findIdx_cons, *]

Result:
no goals
-- Mathlib/ModelTheory/Complexity.lean
theorem isPrenex_toPrenexImp {φ ψ : L.BoundedFormula α n} (hφ : IsPrenex φ) (hψ : IsPrenex ψ) :
    IsPrenex (φ.toPrenexImp ψ)

Proof state:
case all
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih1 : ∀ {ψ : L.BoundedFormula α (n✝ + 1)}, ψ.IsPrenex → (φ✝.toPrenexImp ψ).IsPrenex
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ ((∀'φ✝).toPrenexImp ψ).IsPrenex

Tactic:
exact (ih1 hψ.liftAt).ex

Result:
no goals

Proof state:
L : Language
α : Type u'
n : ℕ
φ ψ : L.BoundedFormula α n
hφ : φ.IsPrenex
hψ : ψ.IsPrenex
⊢ (φ.toPrenexImp ψ).IsPrenex

Tactic:
induction hφ with
| of_isQF hφ => rw [hφ.toPrenexImp]; exact isPrenex_toPrenexImpRight hφ hψ
| all _ ih1 => exact (ih1 hψ.liftAt).ex
| ex _ ih2 => exact (ih2 hψ.liftAt).all

Result:
no goals

Proof state:
case ex
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih2 : ∀ {ψ : L.BoundedFormula α (n✝ + 1)}, ψ.IsPrenex → (φ✝.toPrenexImp ψ).IsPrenex
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ ((∃'φ✝).toPrenexImp ψ).IsPrenex

Tactic:
exact (ih2 hψ.liftAt).all

Result:
no goals

Proof state:
case of_isQF
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hφ : φ✝.IsQF
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (φ✝.toPrenexImp ψ).IsPrenex

Tactic:
rw [hφ.toPrenexImp]

Result:
case of_isQF
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hφ : φ✝.IsQF
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (φ✝.toPrenexImpRight ψ).IsPrenex

Proof state:
case of_isQF
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hφ : φ✝.IsQF
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (φ✝.toPrenexImpRight ψ).IsPrenex

Tactic:
exact isPrenex_toPrenexImpRight hφ hψ

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
lemma tensor_ext {f g : M₁ ⊗ M₂ ⟶ M₃} (h : ∀ m n, f.hom (m ⊗ₜ n) = g.hom (m ⊗ₜ n)) :
    f = g :=
  hom_ext <| TensorProduct.ext (by ext; apply h)

Proof state:
R : Type u
inst✝ : CommRing R
M₁ M₂ M₃ : ModuleCat R
f g : M₁ ⊗ M₂ ⟶ M₃
h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)
⊢ (TensorProduct.mk R ↑M₁ ↑M₂).compr₂ (Hom.hom f) = (TensorProduct.mk R ↑M₁ ↑M₂).compr₂ (Hom.hom g)

Tactic:
ext

Result:
case h.h
R : Type u
inst✝ : CommRing R
M₁ M₂ M₃ : ModuleCat R
f g : M₁ ⊗ M₂ ⟶ M₃
h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)
x✝¹ : ↑M₁
x✝ : ↑M₂
⊢ (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ (Hom.hom f)) x✝¹) x✝ =
    (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ (Hom.hom g)) x✝¹) x✝

Proof state:
case h.h
R : Type u
inst✝ : CommRing R
M₁ M₂ M₃ : ModuleCat R
f g : M₁ ⊗ M₂ ⟶ M₃
h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)
x✝¹ : ↑M₁
x✝ : ↑M₂
⊢ (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ (Hom.hom f)) x✝¹) x✝ =
    (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ (Hom.hom g)) x✝¹) x✝

Tactic:
apply h

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem memLp_norm_iff {f : α → E} (hf : AEStronglyMeasurable f μ) :
    MemLp (fun x => ‖f x‖) p μ ↔ MemLp f p μ :=
  ⟨fun h => ⟨hf, by rw [← eLpNorm_norm]; exact h.2⟩, fun h => h.norm⟩

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h : MemLp (fun x => ‖f x‖) p μ
⊢ eLpNorm (fun x => ‖f x‖) p μ < ⊤

Tactic:
exact h.2

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h : MemLp (fun x => ‖f x‖) p μ
⊢ eLpNorm f p μ < ⊤

Tactic:
rw [← eLpNorm_norm]

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
h : MemLp (fun x => ‖f x‖) p μ
⊢ eLpNorm (fun x => ‖f x‖) p μ < ⊤
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_smul_measure {f : α → β} {c : ℝ≥0∞} (h₁ : c ≠ 0) (h₂ : c ≠ ∞) :
    Integrable f (c • μ) ↔ Integrable f μ :=
  ⟨fun h => by
    simpa only [smul_smul, ENNReal.inv_mul_cancel h₁ h₂, one_smul] using
      h.smul_measure (ENNReal.inv_ne_top.2 h₁),
    fun h => h.smul_measure h₂⟩

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ⊤
h : Integrable f (c • μ)
⊢ Integrable f μ

Tactic:
simpa only [smul_smul, ENNReal.inv_mul_cancel h₁ h₂, one_smul] using
  h.smul_measure (ENNReal.inv_ne_top.2 h₁)

Result:
no goals
-- Mathlib/LinearAlgebra/StdBasis.lean
theorem stdBasis_apply' (i i' : ι) : (stdBasis R (fun _x : ι => R) i) 1 i' = ite (i = i') 1 0

Proof state:
R : Type u_1
ι : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq ι
i i' : ι
⊢ (stdBasis R (fun _x => R) i) 1 i' = if i = i' then 1 else 0

Tactic:
simp_rw [stdBasis, single_apply, Pi.single_apply, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCastD_modifyKey [BEq α] [LawfulBEq α] {k k' : α} {fallback : β k'} {f : β k → β k}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
    getValueCastD k' (modifyKey k f l) fallback =
      if heq : k == k' then
        getValueCast? k l |>.map f |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback
      else
        getValueCastD k' l fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
fallback : β k'
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getValueCastD k' (modifyKey k f l) fallback =
    if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (getValueCast? k l))).getD fallback
    else getValueCastD k' l fallback

Tactic:
simp [modifyKey_eq_alterKey, getValueCastD_alterKey, hl]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ioo_sub_one_left_eq_Ioc (a b : α) : Ioo (a - 1) b = Ico a b

Proof state:
α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioo (a - 1) b = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioo_pred_left_eq_Ioc a b

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem cast_card_eq_zero : (q : K) = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
⊢ ↑q = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
    [Inhabited α] (h : m.WF) {l : List α} {k k' : α} (k_beq : k == k') :
    ¬ k ∈ m → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
      getKey! (insertManyIfNewUnit m l) k' = k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
l : List α
k k' : α
k_beq : (k == k') = true
⊢ ¬k ∈ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKey! k' = k

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
l : List α
k k' : α
k_beq : (k == k') = true
⊢ m.contains k = false →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKey! k' = k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
l : List α
k k' : α
k_beq : (k == k') = true
⊢ m.contains k = false →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKey! k' = k

Tactic:
simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem swap' {f} (hf : Nat.Primrec (unpaired f)) : Nat.Primrec (unpaired (swap f)) :=
  (hf.comp .swap).of_eq fun n => by simp

Proof state:
f : ℕ → ℕ → ℕ
hf : Nat.Primrec (unpaired f)
n : ℕ
⊢ unpaired f (unpaired (swap Nat.pair) n) = unpaired (swap f) n

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
@[reassoc (attr := simp)]
lemma hom_inv_id_eval (e : X ≅ Y) (j : J) :
    e.hom j ≫ e.inv j = 𝟙 _

Proof state:
C : Type u_1
J : Type u_4
inst✝ : Category.{u_5, u_1} C
X Y : GradedObject J C
e : X ≅ Y
j : J
⊢ e.hom j ≫ e.inv j = 𝟙 (X j)

Tactic:
rw [← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id,
  GradedObject.categoryOfGradedObjects_id]

Result:
no goals