harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Nilpotent.lean
theorem nilpotent_of_surjective {G' : Type*} [Group G'] [h : IsNilpotent G] (f : G →* G')
    (hf : Function.Surjective f) : IsNilpotent G'

Proof state:
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ Subgroup.map f ⊤ = Subgroup.map f (upperCentralSeries G n)

Tactic:
rw [hn]

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ upperCentralSeries G' n = ⊤

Tactic:
apply eq_top_iff.mpr

Result:
case h
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ⊤ ≤ upperCentralSeries G' n

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ⊤ ≤ upperCentralSeries G' n

Tactic:
calc
  ⊤ = f.range := symm (f.range_eq_top_of_surjective hf)
  _ = Subgroup.map f ⊤ := MonoidHom.range_eq_map _
  _ = Subgroup.map f (upperCentralSeries G n) := by rw [hn]
  _ ≤ upperCentralSeries G' n := upperCentralSeries.map hf n

Result:
no goals

Proof state:
case mk.intro
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ IsNilpotent G'

Tactic:
use n

Result:
case h
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ upperCentralSeries G' n = ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
h : IsNilpotent G
f : G →* G'
hf : Function.Surjective ⇑f
⊢ IsNilpotent G'

Tactic:
rcases h with ⟨n, hn⟩

Result:
case mk.intro
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ IsNilpotent G'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_le_pow_iff_right {a n m : Nat} (h : 1 < a) :
    a ^ n ≤ a ^ m ↔ n ≤ m

Proof state:
a n m : Nat
h : 1 < a
⊢ a ^ n ≤ a ^ m ↔ n ≤ m

Tactic:
constructor

Result:
case mp
a n m : Nat
h : 1 < a
⊢ a ^ n ≤ a ^ m → n ≤ m

case mpr
a n m : Nat
h : 1 < a
⊢ n ≤ m → a ^ n ≤ a ^ m

Proof state:
case mpr
a n m : Nat
h : 1 < a
⊢ n ≤ m → a ^ n ≤ a ^ m

Tactic:
intro w

Result:
case mpr
a n m : Nat
h : 1 < a
w : n ≤ m
⊢ a ^ n ≤ a ^ m

Proof state:
case mpr
a n m : Nat
h : 1 < a
w : n ≤ m
⊢ a ^ n ≤ a ^ m

Tactic:
cases Nat.eq_or_lt_of_le w

Result:
case mpr.inl
a n m : Nat
h : 1 < a
w : n ≤ m
h✝ : n = m
⊢ a ^ n ≤ a ^ m

case mpr.inr
a n m : Nat
h : 1 < a
w : n ≤ m
h✝ : n < m
⊢ a ^ n ≤ a ^ m

Proof state:
case mpr.inr
a n m : Nat
h : 1 < a
w : n ≤ m
h✝ : n < m
⊢ a ^ n ≤ a ^ m

Tactic:
case inr lt => exact Nat.le_of_lt (Nat.pow_lt_pow_of_lt h lt)

Result:
no goals

Proof state:
a n m : Nat
h : 1 < a
w : n ≤ m
eq : n = m
⊢ a ^ n ≤ a ^ m

Tactic:
subst eq

Result:
a n : Nat
h : 1 < a
w : n ≤ n
⊢ a ^ n ≤ a ^ n

Proof state:
a n : Nat
h : 1 < a
w : n ≤ n
⊢ a ^ n ≤ a ^ n

Tactic:
apply Nat.le_refl

Result:
no goals

Proof state:
case mp
a n m : Nat
h : 1 < a
⊢ a ^ n ≤ a ^ m → n ≤ m

Tactic:
apply Decidable.by_contra

Result:
case mp.a
a n m : Nat
h : 1 < a
⊢ ¬(a ^ n ≤ a ^ m → n ≤ m) → False

Proof state:
a n m : Nat
h : 1 < a
w : n ≤ m
lt : n < m
⊢ a ^ n ≤ a ^ m

Tactic:
exact Nat.le_of_lt (Nat.pow_lt_pow_of_lt h lt)

Result:
no goals

Proof state:
case mp.a
a n m : Nat
h : 1 < a
w : a ^ n ≤ a ^ m ∧ m < n
⊢ a ^ n < a ^ n

Tactic:
exact Nat.lt_of_le_of_lt w.1 (Nat.pow_lt_pow_of_lt h w.2)

Result:
no goals

Proof state:
case mp.a
a n m : Nat
h : 1 < a
w : ¬(a ^ n ≤ a ^ m → n ≤ m)
⊢ False

Tactic:
simp [Decidable.not_imp_iff_and_not] at w

Result:
case mp.a
a n m : Nat
h : 1 < a
w : a ^ n ≤ a ^ m ∧ m < n
⊢ False

Proof state:
case mp.a
a n m : Nat
h : 1 < a
⊢ ¬(a ^ n ≤ a ^ m → n ≤ m) → False

Tactic:
intros w

Result:
case mp.a
a n m : Nat
h : 1 < a
w : ¬(a ^ n ≤ a ^ m → n ≤ m)
⊢ False

Proof state:
case mp.a
a n m : Nat
h : 1 < a
w : a ^ n ≤ a ^ m ∧ m < n
⊢ False

Tactic:
apply Nat.lt_irrefl (a ^ n)

Result:
case mp.a
a n m : Nat
h : 1 < a
w : a ^ n ≤ a ^ m ∧ m < n
⊢ a ^ n < a ^ n

Proof state:
case mpr.inl
a n m : Nat
h : 1 < a
w : n ≤ m
h✝ : n = m
⊢ a ^ n ≤ a ^ m

case mpr.inr
a n m : Nat
h : 1 < a
w : n ≤ m
h✝ : n < m
⊢ a ^ n ≤ a ^ m

Tactic:
case inl eq => subst eq; apply Nat.le_refl

Result:
case mpr.inr
a n m : Nat
h : 1 < a
w : n ≤ m
h✝ : n < m
⊢ a ^ n ≤ a ^ m
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem frontier_preimage (e : Trivialization F proj) (s : Set B) :
    e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
s : Set B
⊢ e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)

Tactic:
rw [← (e.isImage_preimage_prod s).frontier.preimage_eq, frontier_prod_univ_eq,
  (e.isImage_preimage_prod _).preimage_eq, e.source_eq, preimage_inter]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
lemma comap_freeLocus_le {A} [CommRing A] [Algebra R A] :
    comap (algebraMap R A) ⁻¹' freeLocus R M ≤ freeLocus A (A ⊗[R] M)

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
hp : p ∈ ⇑(comap (algebraMap R A)) ⁻¹' freeLocus R M
⊢ p ∈ freeLocus A (A ⊗[R] M)

Tactic:
let Rₚ := Localization.AtPrime (comap (algebraMap R A) p).asIdeal

Result:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
hp : p ∈ ⇑(comap (algebraMap R A)) ⁻¹' freeLocus R M
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
⊢ p ∈ freeLocus A (A ⊗[R] M)
-- Mathlib/Probability/CDF.lean
lemma ofReal_cdf [IsProbabilityMeasure μ] (x : ℝ) : ENNReal.ofReal (cdf μ x) = μ (Iic x)

Proof state:
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
⊢ ENNReal.ofReal (↑(cdf μ) x) = μ (Iic x)

Tactic:
have h := lintegral_condCDF ((Measure.dirac Unit.unit).prod μ) x

Result:
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
h :
  ∫⁻ (a : Unit), ENNReal.ofReal (↑(condCDF ((Measure.dirac ()).prod μ) a) x) ∂((Measure.dirac ()).prod μ).fst =
    ((Measure.dirac ()).prod μ) (univ ×ˢ Iic x)
⊢ ENNReal.ofReal (↑(cdf μ) x) = μ (Iic x)

Proof state:
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
h :
  ∫⁻ (a : Unit), ENNReal.ofReal (↑(condCDF ((Measure.dirac ()).prod μ) a) x) ∂((Measure.dirac ()).prod μ).fst =
    ((Measure.dirac ()).prod μ) (univ ×ˢ Iic x)
⊢ ENNReal.ofReal (↑(cdf μ) x) = μ (Iic x)

Tactic:
simpa only [MeasureTheory.Measure.fst_prod, Measure.prod_prod, measure_univ, one_mul,
  lintegral_dirac] using h

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_pos' [LinearOrderedRing α] (hx : 0 < x + 1) (hn : n ≠ 0) :
    0 < ∑ i ∈ range n, x ^ i

Proof state:
case succ.succ.inr
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

Tactic:
exact geom_sum_pos hx' (by simp only [Nat.succ_ne_zero, Ne, not_false_iff])

Result:
no goals

Proof state:
case zero
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : 0 ≠ 0
⊢ 0 < ∑ i ∈ range 0, x ^ i

Tactic:
cases hn rfl

Result:
no goals

Proof state:
case succ.succ
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

Tactic:
obtain hx' | hx' := lt_or_le x 0

Result:
case succ.succ.inl
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : x < 0
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

case succ.succ.inr
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

Proof state:
case succ.succ.inl
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : x < 0
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

Tactic:
exact (geom_sum_pos_and_lt_one hx' hx n.one_lt_succ_succ).1

Result:
no goals

Proof state:
case succ.zero
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : 0 + 1 ≠ 0
⊢ 0 < ∑ i ∈ range (0 + 1), x ^ i

Tactic:
simp only [zero_add, range_one, sum_singleton, pow_zero, zero_lt_one]

Result:
no goals

Proof state:
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ n + 1 + 1 ≠ 0

Tactic:
simp only [Nat.succ_ne_zero, Ne, not_false_iff]

Result:
no goals

Proof state:
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : n ≠ 0
⊢ 0 < ∑ i ∈ range n, x ^ i

Tactic:
obtain _ | _ | n := n

Result:
case zero
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : 0 ≠ 0
⊢ 0 < ∑ i ∈ range 0, x ^ i

case succ.zero
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : 0 + 1 ≠ 0
⊢ 0 < ∑ i ∈ range (0 + 1), x ^ i

case succ.succ
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i
-- Mathlib/RingTheory/Ideal/Quotient/Defs.lean
theorem factor_comp (H1 : S ≤ T) (H2 : T ≤ U) :
    (factor H2).comp (factor H1) = factor (H1.trans H2)

Proof state:
R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
⊢ (factor H2).comp (factor H1) = factor ⋯

Tactic:
ext

Result:
case h.a
R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x✝ : R
⊢ (((factor H2).comp (factor H1)).comp (mk S)) x✝ = ((factor ⋯).comp (mk S)) x✝

Proof state:
case h.a
R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x✝ : R
⊢ (((factor H2).comp (factor H1)).comp (mk S)) x✝ = ((factor ⋯).comp (mk S)) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem restrict_extend {x : FamilyOfElements P R} (t : x.Compatible) :
    x.sieveExtend.restrict (le_generate R) = x

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
⊢ FamilyOfElements.restrict ⋯ x.sieveExtend = x

Tactic:
funext Y f hf

Result:
case h.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
Y : C
f : Y ⟶ X
hf : R f
⊢ FamilyOfElements.restrict ⋯ x.sieveExtend f hf = x f hf

Proof state:
case h.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
Y : C
f : Y ⟶ X
hf : R f
⊢ FamilyOfElements.restrict ⋯ x.sieveExtend f hf = x f hf

Tactic:
exact extend_agrees t hf

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
/--
Checking AB of shape `Discrete ℕ` is enough for countable AB4, provided that the category has
finite biproducts and finite limits.
-/
lemma CountableAB4.of_hasExactColimitsOfShape_nat [HasFiniteLimits C] [HasCountableCoproducts C]
    [HasExactColimitsOfShape (Discrete ℕ) C] : CountableAB4 C

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasFiniteBiproducts C
inst✝² : HasFiniteLimits C
inst✝¹ : HasCountableCoproducts C
inst✝ : HasExactColimitsOfShape (Discrete ℕ) C
⊢ CountableAB4 C

Tactic:
apply (config := { allowSynthFailures := true })
    CountableAB4.of_hasExactColimitsOfShape_nat_and_finite

Result:
case inst
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasFiniteBiproducts C
inst✝² : HasFiniteLimits C
inst✝¹ : HasCountableCoproducts C
inst✝ : HasExactColimitsOfShape (Discrete ℕ) C
⊢ ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C

Proof state:
case inst
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasFiniteBiproducts C
inst✝² : HasFiniteLimits C
inst✝¹ : HasCountableCoproducts C
inst✝ : HasExactColimitsOfShape (Discrete ℕ) C
⊢ ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C

Tactic:
exact fun _ ↦ inferInstance

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem AnalyticAt.hasStrictFDerivAt (h : AnalyticAt 𝕜 f x) :
    HasStrictFDerivAt f (fderiv 𝕜 f x) x

Proof state:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt f p x
⊢ HasStrictFDerivAt f (fderiv 𝕜 f x) x

Tactic:
rw [hp.fderiv_eq]

Result:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt f p x
⊢ HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticAt 𝕜 f x
⊢ HasStrictFDerivAt f (fderiv 𝕜 f x) x

Tactic:
rcases h with ⟨p, hp⟩

Result:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt f p x
⊢ HasStrictFDerivAt f (fderiv 𝕜 f x) x

Proof state:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesAt f p x
⊢ HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x

Tactic:
exact hp.hasStrictFDerivAt

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem set_next_add (s : String) (i : Pos) (c : Char) (b₁ b₂)
    (h : (s.next i).1 + b₁ = s.endPos.1 + b₂) :
    ((s.set i c).next i).1 + b₁ = (s.set i c).endPos.1 + b₂

Proof state:
s : String
i : Pos
c : Char
b₁ b₂ : Nat
h : (s.next i).byteIdx + b₁ = s.endPos.byteIdx + b₂
⊢ ((s.set i c).next i).byteIdx + b₁ = (s.set i c).endPos.byteIdx + b₂

Tactic:
simp [next, get, set, endPos, utf8ByteSize] at h ⊢

Result:
s : String
i : Pos
c : Char
b₁ b₂ : Nat
h : i.byteIdx + (utf8GetAux s.data 0 i).utf8Size + b₁ = utf8ByteSize.go s.data + b₂
⊢ i.byteIdx + (utf8GetAux (utf8SetAux c s.data 0 i) 0 i).utf8Size + b₁ = utf8ByteSize.go (utf8SetAux c s.data 0 i) + b₂
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_submatrix_equiv_self (e : n ≃ m) (A : Matrix m m α) :
    adjugate (A.submatrix e e) = (adjugate A).submatrix e e

Proof state:
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
this : (fun j => Pi.single i 1 (e.symm j)) = Pi.single (e i) 1
⊢ ((A.updateRow (e j) fun j => Pi.single i 1 (e.symm j)).submatrix ⇑e ⇑e).det =
    ((A.updateRow (e j) (Pi.single (e i) 1)).submatrix ⇑e ⇑e).det

Tactic:
erw [this]

Result:
no goals

Proof state:
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
⊢ (A.submatrix ⇑e ⇑e).adjugate = A.adjugate.submatrix ⇑e ⇑e

Tactic:
ext i j

Result:
case a
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ (A.submatrix ⇑e ⇑e).adjugate i j = A.adjugate.submatrix (⇑e) (⇑e) i j

Proof state:
case a
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ (fun j => Pi.single i 1 (e.symm j)) = Pi.single (e i) 1

Tactic:
exact Function.update_comp_equiv _ e.symm _ _

Result:
no goals

Proof state:
case a
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ (A.submatrix ⇑e ⇑e).adjugate i j = A.adjugate.submatrix (⇑e) (⇑e) i j

Tactic:
rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e,
  updateRow_submatrix_equiv]

Result:
case a
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ ((A.updateRow (e j) fun j => Pi.single i 1 (e.symm j)).submatrix ⇑e ⇑e).det =
    ((A.updateRow (e j) (Pi.single (e i) 1)).submatrix ⇑e ⇑e).det

Proof state:
case a
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ ((A.updateRow (e j) fun j => Pi.single i 1 (e.symm j)).submatrix ⇑e ⇑e).det =
    ((A.updateRow (e j) (Pi.single (e i) 1)).submatrix ⇑e ⇑e).det

Tactic:
suffices (fun j => Pi.single i 1 (e.symm j)) = Pi.single (e i) 1 by
  erw [this]

Result:
case a
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ (fun j => Pi.single i 1 (e.symm j)) = Pi.single (e i) 1
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean
theorem integral_cos_mul_cos_pow_even (n : ℕ) (hz : z ≠ 0) :
    (((1 : ℂ) - z ^ 2 / ((n : ℂ) + 1) ^ 2) *
        ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n + 2)) =
      (2 * n + 1 : ℂ) / (2 * n + 2) *
        ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n)

Proof state:
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 ≤ 2 * n + 2

Tactic:
omega

Result:
no goals

Proof state:
case h.e'_2.h.e'_5.h.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / 2 ^ 2 / (↑n + 1) ^ 2

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_3.h.e'_5.h.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 2 = 2 * ↑n + 2

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_3.h.e'_5.h.e'_5
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 1 = ↑(2 * n + 2) - 1

Tactic:
push_cast

Result:
case h.e'_3.h.e'_5.h.e'_5
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 1 = 2 * ↑n + 2 - 1

Proof state:
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ (1 - z ^ 2 / (↑n + 1) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n + 2) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)

Tactic:
convert integral_cos_mul_cos_pow (by omega : 2 ≤ 2 * n + 2) hz using 3

Result:
case h.e'_2.h.e'_5.h.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / ↑(2 * n + 2) ^ 2

case h.e'_3.h.e'_5.h.e'_5
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 1 = ↑(2 * n + 2) - 1

case h.e'_3.h.e'_5.h.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 2 = ↑(2 * n + 2)

Proof state:
case h.e'_2.h.e'_5.h.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / (2 * ↑n + 2 * 1) ^ 2

Tactic:
rw [← mul_add, mul_pow, ← div_div]

Result:
case h.e'_2.h.e'_5.h.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / 2 ^ 2 / (↑n + 1) ^ 2

Proof state:
case h.e'_2.h.e'_5.h.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / (2 * ↑n + 2) ^ 2

Tactic:
nth_rw 2 [← mul_one (2 : ℂ)]

Result:
case h.e'_2.h.e'_5.h.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / (2 * ↑n + 2 * 1) ^ 2

Proof state:
case h.e'_3.h.e'_5.h.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 2 = ↑(2 * n + 2)

Tactic:
push_cast

Result:
case h.e'_3.h.e'_5.h.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 2 = 2 * ↑n + 2

Proof state:
case h.e'_3.h.e'_5.h.e'_5
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 1 = 2 * ↑n + 2 - 1

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_2.h.e'_5.h.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / ↑(2 * n + 2) ^ 2

Tactic:
simp only [Nat.cast_add, Nat.cast_mul, Nat.cast_two]

Result:
case h.e'_2.h.e'_5.h.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / (2 * ↑n + 2) ^ 2
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insertMany_empty_list_of_mem [LawfulBEq α]
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    get? (insertMany (empty : Raw₀ α (fun _ => β)) l) k' = some v

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
⊢ get? (insertMany empty l).val k' = some v

Tactic:
rw [get?_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem mem_image_of_mem_range_restrict {r : β} {s : Set α} {f : α →ₛ β}
    (hr : r ∈ (restrict f s).range) (h0 : r ≠ 0) : r ∈ f '' s :=
  if hs : MeasurableSet s then by simpa [mem_restrict_range hs, h0, -mem_range] using hr
  else by
    rw [restrict_of_not_measurable hs] at hr
    exact (h0 <| eq_zero_of_mem_range_zero hr).elim

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ (f.restrict s).range
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ r ∈ ⇑f '' s

Tactic:
rw [restrict_of_not_measurable hs] at hr

Result:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ SimpleFunc.range 0
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ r ∈ ⇑f '' s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ SimpleFunc.range 0
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ r ∈ ⇑f '' s

Tactic:
exact (h0 <| eq_zero_of_mem_range_zero hr).elim

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ (f.restrict s).range
h0 : r ≠ 0
hs : MeasurableSet s
⊢ r ∈ ⇑f '' s

Tactic:
simpa [mem_restrict_range hs, h0, -mem_range] using hr

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_neg : exp (-x) = (exp x)⁻¹ :=
  ofReal_injective <| by simp [exp_neg]

Proof state:
x : ℝ
⊢ ↑(rexp (-x)) = ↑(rexp x)⁻¹

Tactic:
simp [exp_neg]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem cpow_mul_ofReal_nonneg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) (z : ℂ) :
    (x : ℂ) ^ (↑y * z) = (↑(x ^ y) : ℂ) ^ z

Proof state:
case h₂
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ (log ↑x * ↑y).im ≤ π

Tactic:
rw [← ofReal_log hx, ← ofReal_mul, ofReal_im]

Result:
case h₂
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 ≤ π

Proof state:
case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 < π

Tactic:
exact Real.pi_pos

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ ↑x ^ (↑y * z) = ↑(x ^ y) ^ z

Tactic:
rw [cpow_mul, ofReal_cpow hx]

Result:
case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ -π < (log ↑x * ↑y).im

case h₂
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ (log ↑x * ↑y).im ≤ π

Proof state:
case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ -π < (log ↑x * ↑y).im

Tactic:
rw [← ofReal_log hx, ← ofReal_mul, ofReal_im, neg_lt_zero]

Result:
case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 < π

Proof state:
case h₂
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 ≤ π

Tactic:
exact Real.pi_pos.le

Result:
no goals