harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem tprod_tprod (l : List δ) (μ : ∀ i, Measure (π i)) [∀ i, SigmaFinite (μ i)]
    (s : ∀ i, Set (π i)) :
    Measure.tprod l μ (Set.tprod l s) = (l.map fun i => (μ i) (s i)).prod

Proof state:
case cons
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (π i)
a : δ
l : List δ
ih : (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i => (μ i) (s i)) l).prod
⊢ (Measure.tprod (a :: l) μ) (Set.tprod (a :: l) s) = (List.map (fun i => (μ i) (s i)) (a :: l)).prod

Tactic:
rw [tprod_cons, Set.tprod]

Result:
case cons
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (π i)
a : δ
l : List δ
ih : (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i => (μ i) (s i)) l).prod
⊢ ((μ a).prod (Measure.tprod l μ)) (s a ×ˢ Set.tprod l s) = (List.map (fun i => (μ i) (s i)) (a :: l)).prod

Proof state:
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
l : List δ
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (π i)
⊢ (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i => (μ i) (s i)) l).prod

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  rw [tprod_cons, Set.tprod]
  erw [prod_prod] rw [map_cons, prod_cons, ih]

Result:
no goals

Proof state:
case nil
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (π i)
⊢ (Measure.tprod [] μ) (Set.tprod [] s) = (List.map (fun i => (μ i) (s i)) []).prod

Tactic:
simp

Result:
no goals

Proof state:
case cons
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (π i)
a : δ
l : List δ
ih : (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i => (μ i) (s i)) l).prod
⊢ (μ a) (s a) * (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i => (μ i) (s i)) (a :: l)).prod

Tactic:
rw [map_cons, prod_cons, ih]

Result:
no goals

Proof state:
case cons
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (π i)
a : δ
l : List δ
ih : (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i => (μ i) (s i)) l).prod
⊢ ((μ a).prod (Measure.tprod l μ)) (s a ×ˢ Set.tprod l s) = (List.map (fun i => (μ i) (s i)) (a :: l)).prod

Tactic:
erw [prod_prod]

Result:
case cons
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (π i)
a : δ
l : List δ
ih : (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i => (μ i) (s i)) l).prod
⊢ (μ a) (s a) * (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i => (μ i) (s i)) (a :: l)).prod
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem comap_normalizer_eq_of_injective_of_le_range {N : Type*} [Group N] (H : Subgroup G)
    {f : N →* G} (hf : Function.Injective f) (h : H.normalizer ≤ f.range) :
    comap f H.normalizer = (comap f H).normalizer

Proof state:
case a.a
G : Type u_1
inst✝¹ : Group G
N : Type u_6
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ⇑f
h : H.normalizer ≤ f.range
⊢ H.normalizer ≤ map f (comap f H).normalizer

Tactic:
refine le_trans (le_of_eq ?_) (map_mono (le_normalizer_comap _))

Result:
case a.a
G : Type u_1
inst✝¹ : Group G
N : Type u_6
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ⇑f
h : H.normalizer ≤ f.range
⊢ H.normalizer = map f (comap f H.normalizer)

Proof state:
case a.a
G : Type u_1
inst✝¹ : Group G
N : Type u_6
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ⇑f
h : H.normalizer ≤ f.range
⊢ map f (comap f H).normalizer ≤ H.normalizer

Tactic:
refine le_trans (le_normalizer_map f) (le_of_eq ?_)

Result:
case a.a
G : Type u_1
inst✝¹ : Group G
N : Type u_6
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ⇑f
h : H.normalizer ≤ f.range
⊢ (map f (comap f H)).normalizer = H.normalizer

Proof state:
case a.a
G : Type u_1
inst✝¹ : Group G
N : Type u_6
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ⇑f
h : H.normalizer ≤ f.range
⊢ H.normalizer = map f (comap f H.normalizer)

Tactic:
rw [map_comap_eq_self h]

Result:
no goals

Proof state:
case a
G : Type u_1
inst✝¹ : Group G
N : Type u_6
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ⇑f
h : H.normalizer ≤ f.range
⊢ H.normalizer = map f (comap f H).normalizer

Tactic:
apply le_antisymm

Result:
case a.a
G : Type u_1
inst✝¹ : Group G
N : Type u_6
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ⇑f
h : H.normalizer ≤ f.range
⊢ H.normalizer ≤ map f (comap f H).normalizer

case a.a
G : Type u_1
inst✝¹ : Group G
N : Type u_6
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ⇑f
h : H.normalizer ≤ f.range
⊢ map f (comap f H).normalizer ≤ H.normalizer

Proof state:
case a.a
G : Type u_1
inst✝¹ : Group G
N : Type u_6
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ⇑f
h : H.normalizer ≤ f.range
⊢ (map f (comap f H)).normalizer = H.normalizer

Tactic:
rw [map_comap_eq_self (le_trans le_normalizer h)]

Result:
no goals

Proof state:
case a
G : Type u_1
inst✝¹ : Group G
N : Type u_6
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ⇑f
h : H.normalizer ≤ f.range
⊢ map f (comap f H.normalizer) = map f (comap f H).normalizer

Tactic:
rw [map_comap_eq_self h]

Result:
case a
G : Type u_1
inst✝¹ : Group G
N : Type u_6
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ⇑f
h : H.normalizer ≤ f.range
⊢ H.normalizer = map f (comap f H).normalizer

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_6
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ⇑f
h : H.normalizer ≤ f.range
⊢ comap f H.normalizer = (comap f H).normalizer

Tactic:
apply Subgroup.map_injective hf

Result:
case a
G : Type u_1
inst✝¹ : Group G
N : Type u_6
inst✝ : Group N
H : Subgroup G
f : N →* G
hf : Injective ⇑f
h : H.normalizer ≤ f.range
⊢ map f (comap f H.normalizer) = map f (comap f H).normalizer
-- Mathlib/Data/Nat/Totient.lean
theorem totient_even {n : ℕ} (hn : 2 < n) : Even n.totient

Proof state:
n : ℕ
hn : 2 < n
this : Fact (1 < n)
⊢ Even (φ n)

Tactic:
haveI : NeZero n := NeZero.of_gt hn

Result:
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ Even (φ n)

Proof state:
n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ Even (φ n)

Tactic:
rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]

Result:
n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ orderOf (-1) ∣ Fintype.card (ZMod n)ˣ

Proof state:
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ 2 = orderOf (-1)

Tactic:
rw [← orderOf_units, Units.coe_neg_one, orderOf_neg_one, ringChar.eq (ZMod n) n, if_neg hn.ne']

Result:
no goals

Proof state:
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ Even (φ n)

Tactic:
suffices 2 = orderOf (-1 : (ZMod n)ˣ) by
  rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
  exact orderOf_dvd_card

Result:
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ 2 = orderOf (-1)

Proof state:
n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ orderOf (-1) ∣ Fintype.card (ZMod n)ˣ

Tactic:
exact orderOf_dvd_card

Result:
no goals

Proof state:
n : ℕ
hn : 2 < n
⊢ Even (φ n)

Tactic:
haveI : Fact (1 < n) := ⟨one_lt_two.trans hn⟩

Result:
n : ℕ
hn : 2 < n
this : Fact (1 < n)
⊢ Even (φ n)
-- Mathlib/Order/Cover.lean
theorem mk_wcovBy_mk_iff_left : (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
⊢ (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂

Tactic:
refine ⟨WCovBy.fst, (And.imp mk_le_mk_iff_left.2) fun h c h₁ h₂ => ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < c
h₂ : c < (a₂, b)
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < c
h₂ : c < (a₂, b)
⊢ False

Tactic:
have : c.2 = b := h₂.le.2.antisymm h₁.le.2

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < c
h₂ : c < (a₂, b)
this : c.2 = b
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < c
h₂ : c < (a₂, b)
this : c.2 = b
⊢ False

Tactic:
rw [← @Prod.mk.eta _ _ c, this, mk_lt_mk_iff_left] at h₁ h₂

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : a₁ < c.1
h₂ : c.1 < a₂
this : c.2 = b
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : a₁ < c.1
h₂ : c.1 < a₂
this : c.2 = b
⊢ False

Tactic:
exact h h₁ h₂

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem sModNatTR_eq_sModNat (q : ℕ) (i : ℕ) : sModNatTR q i = sModNat q i

Proof state:
q i : ℕ
⊢ sModNatTR q i = sModNat q i

Tactic:
rw [sModNatTR, helper, sModNat_aux_eq]

Result:
no goals

Proof state:
case succ
q✝ i q k : ℕ
ih : ∀ (b : ℕ), sModNatTR.go q k b = sModNat_aux b q k
b : ℕ
⊢ sModNatTR.go q (k + 1) b = sModNat_aux b q (k + 1)

Tactic:
rw [sModNatTR.go, ih, sModNat_aux]

Result:
case succ
q✝ i q k : ℕ
ih : ∀ (b : ℕ), sModNatTR.go q k b = sModNat_aux b q k
b : ℕ
⊢ sModNat_aux ((b ^ 2 + (q - 2)) % q) q k = (sModNat_aux b q k ^ 2 + (q - 2)) % q

Proof state:
case zero
q✝ i q b : ℕ
⊢ sModNatTR.go q 0 b = sModNat_aux b q 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ.zero
q✝ i q b : ℕ
⊢ sModNat_aux ((b ^ 2 + (q - 2)) % q) q 0 = (sModNat_aux b q 0 ^ 2 + (q - 2)) % q

Tactic:
rfl

Result:
no goals

Proof state:
case succ.succ
q✝ i q b k : ℕ
ih : sModNat_aux ((b ^ 2 + (q - 2)) % q) q k = (sModNat_aux b q k ^ 2 + (q - 2)) % q
⊢ sModNat_aux ((b ^ 2 + (q - 2)) % q) q (k + 1) = (sModNat_aux b q (k + 1) ^ 2 + (q - 2)) % q

Tactic:
rw [sModNat_aux, ih, sModNat_aux]

Result:
no goals

Proof state:
q✝ i b q k : ℕ
⊢ sModNatTR.go q k b = sModNat_aux b q k

Tactic:
induction k generalizing b with
| zero => rfl
| succ k ih =>
  rw [sModNatTR.go, ih, sModNat_aux]
  clear ih
  induction k with
  | zero => rfl
  | succ k ih =>
    rw [sModNat_aux, ih, sModNat_aux]

Result:
no goals

Proof state:
case succ
q✝ i q k : ℕ
ih : ∀ (b : ℕ), sModNatTR.go q k b = sModNat_aux b q k
b : ℕ
⊢ sModNat_aux ((b ^ 2 + (q - 2)) % q) q k = (sModNat_aux b q k ^ 2 + (q - 2)) % q

Tactic:
clear ih

Result:
case succ
q✝ i q k b : ℕ
⊢ sModNat_aux ((b ^ 2 + (q - 2)) % q) q k = (sModNat_aux b q k ^ 2 + (q - 2)) % q

Proof state:
case succ
q✝ i q k b : ℕ
⊢ sModNat_aux ((b ^ 2 + (q - 2)) % q) q k = (sModNat_aux b q k ^ 2 + (q - 2)) % q

Tactic:
induction k with
| zero => rfl
| succ k ih =>
  rw [sModNat_aux, ih, sModNat_aux]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem inter_mem_inter [Inter α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma ∩ mb ∈ a ∩ b

Proof state:
α : Type u_1
inst✝ : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1 ∈ a, ∃ a ∈ b, a_1 ∩ a = ma ∩ mb

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ∩ mb ∈ a ∩ b

Tactic:
simp [inter_def]

Result:
α : Type u_1
inst✝ : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1 ∈ a, ∃ a ∈ b, a_1 ∩ a = ma ∩ mb
-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidt_def'' (f : ι → E) (n : ι) :
    f n = gramSchmidt 𝕜 f n + ∑ i ∈ Iio n,
      (⟪gramSchmidt 𝕜 f i, f n⟫ / (‖gramSchmidt 𝕜 f i‖ : 𝕜) ^ 2) • gramSchmidt 𝕜 f i

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
⊢ f n =
    gramSchmidt 𝕜 f n + ∑ i ∈ Iio n, (inner (gramSchmidt 𝕜 f i) (f n) / ↑‖gramSchmidt 𝕜 f i‖ ^ 2) • gramSchmidt 𝕜 f i

Tactic:
convert gramSchmidt_def' 𝕜 f n

Result:
case h.e'_3.h.e'_6.a
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n x✝ : ι
a✝ : x✝ ∈ Iio n
⊢ (inner (gramSchmidt 𝕜 f x✝) (f n) / ↑‖gramSchmidt 𝕜 f x✝‖ ^ 2) • gramSchmidt 𝕜 f x✝ =
    ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f x✝})) (f n))

Proof state:
case h.e'_3.h.e'_6.a
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n x✝ : ι
a✝ : x✝ ∈ Iio n
⊢ (inner (gramSchmidt 𝕜 f x✝) (f n) / ↑‖gramSchmidt 𝕜 f x✝‖ ^ 2) • gramSchmidt 𝕜 f x✝ =
    ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f x✝})) (f n))

Tactic:
rw [orthogonalProjection_singleton, RCLike.ofReal_pow]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem algebraMap_apply (k : 𝕜) (a : α) : algebraMap 𝕜 (α →ᵇ γ) k a = k • (1 : γ)

Proof state:
α : Type u
γ : Type w
𝕜 : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : TopologicalSpace α
inst✝¹ : NormedRing γ
inst✝ : NormedAlgebra 𝕜 γ
k : 𝕜
a : α
⊢ ((algebraMap 𝕜 (α →ᵇ γ)) k) a = k • 1

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, coe_smul, coe_one, Pi.one_apply]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
/-- Expresses the integral over `Ioi 0` of `t ^ (a - 1) * exp (-(r * t))`, for positive real `r`,
in terms of the Gamma function. -/
lemma integral_rpow_mul_exp_neg_mul_Ioi {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    ∫ t : ℝ in Ioi 0, t ^ (a - 1) * exp (-(r * t)) = (1 / r) ^ a * Gamma a

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ↑(∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t))) = (↑1 / ↑r) ^ ↑a * Complex.Gamma ↑a

Tactic:
convert integral_cpow_mul_exp_neg_mul_Ioi (by rwa [ofReal_re] : 0 < (a : ℂ).re) hr

Result:
case h.e'_2
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ↑(∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t))) = ∫ (t : ℝ) in Ioi 0, ↑t ^ (↑a - 1) * cexp (-(↑r * ↑t))

Proof state:
case h.e'_2
a r : ℝ
ha : 0 < a
hr : 0 < r
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑(t ^ (a - 1) * rexp (-(r * t))) = ↑t ^ (↑a - 1) * cexp (-(↑r * ↑t))

Tactic:
norm_cast

Result:
case h.e'_2
a r : ℝ
ha : 0 < a
hr : 0 < r
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑(t ^ (a - 1) * rexp (-(r * t))) = ↑t ^ ↑(a - 1) * ↑(rexp (-(r * t)))

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ 0 ≤ 1 / r

Tactic:
positivity

Result:
no goals

Proof state:
case h.e'_2
a r : ℝ
ha : 0 < a
hr : 0 < r
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑(t ^ (a - 1) * rexp (-(r * t))) = ↑t ^ ↑(a - 1) * ↑(rexp (-(r * t)))

Tactic:
simp_rw [← ofReal_cpow ht.le, RCLike.ofReal_mul, coe_algebraMap]

Result:
no goals

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ 0 < (↑a).re

Tactic:
rwa [ofReal_re]

Result:
no goals

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t)) = (1 / r) ^ a * Gamma a

Tactic:
rw [← ofReal_inj, ofReal_mul, ← Gamma_ofReal, ofReal_cpow (by positivity), ofReal_div]

Result:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ↑(∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t))) = (↑1 / ↑r) ^ ↑a * Complex.Gamma ↑a

Proof state:
case h.e'_2
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ↑(∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t))) = ∫ (t : ℝ) in Ioi 0, ↑t ^ (↑a - 1) * cexp (-(↑r * ↑t))

Tactic:
refine integral_ofReal.symm.trans <| setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)

Result:
case h.e'_2
a r : ℝ
ha : 0 < a
hr : 0 < r
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑(t ^ (a - 1) * rexp (-(r * t))) = ↑t ^ (↑a - 1) * cexp (-(↑r * ↑t))
-- Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
@[simp]
lemma μIso_hom_freeMk_tmul_freeMk {X Y : Type u} (x : X) (y : Y) :
    (μIso R X Y).hom (freeMk x ⊗ₜ freeMk y) = freeMk ⟨x, y⟩

Proof state:
R : Type u
inst✝ : CommRing R
X Y : Type u
x : X
y : Y
⊢ (ConcreteCategory.hom (μIso R X Y).hom) (freeMk x ⊗ₜ[R] freeMk y) = freeMk (x, y)

Tactic:
dsimp [μIso, freeMk]

Result:
R : Type u
inst✝ : CommRing R
X Y : Type u
x : X
y : Y
⊢ ↑(finsuppTensorFinsupp' R X Y) (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single y 1) = Finsupp.single (x, y) 1

Proof state:
R : Type u
inst✝ : CommRing R
X Y : Type u
x : X
y : Y
⊢ Finsupp.single (x, y) (1 * 1) = Finsupp.single (x, y) 1

Tactic:
rw [mul_one]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
X Y : Type u
x : X
y : Y
⊢ ↑(finsuppTensorFinsupp' R X Y) (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single y 1) = Finsupp.single (x, y) 1

Tactic:
erw [finsuppTensorFinsupp'_single_tmul_single]

Result:
R : Type u
inst✝ : CommRing R
X Y : Type u
x : X
y : Y
⊢ Finsupp.single (x, y) (1 * 1) = Finsupp.single (x, y) 1
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem toFinsupp_toFreeAbelianGroup (f : X →₀ ℤ) :
    FreeAbelianGroup.toFinsupp (Finsupp.toFreeAbelianGroup f) = f

Proof state:
X : Type u_1
f : X →₀ ℤ
⊢ toFinsupp (toFreeAbelianGroup f) = f

Tactic:
rw [← AddMonoidHom.comp_apply, toFinsupp_comp_toFreeAbelianGroup, AddMonoidHom.id_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem set_eq_of_length_le {l : List α} {n : Nat} (h : l.length ≤ n) {a : α} :
    l.set n a = l

Proof state:
case cons
α : Type u_1
a✝ a : α
l : List α
ih : ∀ {n : Nat}, l.length ≤ n → l.set n a✝ = l
n : Nat
h : (a :: l).length ≤ n
⊢ (a :: l).set n a✝ = a :: l

Tactic:
induction n

Result:
case cons.zero
α : Type u_1
a✝ a : α
l : List α
ih : ∀ {n : Nat}, l.length ≤ n → l.set n a✝ = l
h : (a :: l).length ≤ 0
⊢ (a :: l).set 0 a✝ = a :: l

case cons.succ
α : Type u_1
a✝¹ a : α
l : List α
ih : ∀ {n : Nat}, l.length ≤ n → l.set n a✝¹ = l
n✝ : Nat
a✝ : (a :: l).length ≤ n✝ → (a :: l).set n✝ a✝¹ = a :: l
h : (a :: l).length ≤ n✝ + 1
⊢ (a :: l).set (n✝ + 1) a✝¹ = a :: l

Proof state:
case nil
α : Type u_1
a : α
n : Nat
h : [].length ≤ n
⊢ [].set n a = []

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
a✝¹ a : α
l : List α
ih : ∀ {n : Nat}, l.length ≤ n → l.set n a✝¹ = l
n✝ : Nat
a✝ : (a :: l).length ≤ n✝ → (a :: l).set n✝ a✝¹ = a :: l
h : (a :: l).length ≤ n✝ + 1
⊢ (a :: l).set (n✝ + 1) a✝¹ = a :: l

Tactic:
simp only [set_cons_succ, cons.injEq, true_and]

Result:
case cons.succ
α : Type u_1
a✝¹ a : α
l : List α
ih : ∀ {n : Nat}, l.length ≤ n → l.set n a✝¹ = l
n✝ : Nat
a✝ : (a :: l).length ≤ n✝ → (a :: l).set n✝ a✝¹ = a :: l
h : (a :: l).length ≤ n✝ + 1
⊢ l.set n✝ a✝¹ = l

Proof state:
case cons.zero
α : Type u_1
a✝ a : α
l : List α
ih : ∀ {n : Nat}, l.length ≤ n → l.set n a✝ = l
h : (a :: l).length ≤ 0
⊢ (a :: l).set 0 a✝ = a :: l

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
a✝¹ a : α
l : List α
ih : ∀ {n : Nat}, l.length ≤ n → l.set n a✝¹ = l
n✝ : Nat
a✝ : (a :: l).length ≤ n✝ → (a :: l).set n✝ a✝¹ = a :: l
h : (a :: l).length ≤ n✝ + 1
⊢ l.length ≤ n✝

Tactic:
exact Nat.succ_le_succ_iff.mp h

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
a✝¹ a : α
l : List α
ih : ∀ {n : Nat}, l.length ≤ n → l.set n a✝¹ = l
n✝ : Nat
a✝ : (a :: l).length ≤ n✝ → (a :: l).set n✝ a✝¹ = a :: l
h : (a :: l).length ≤ n✝ + 1
⊢ l.set n✝ a✝¹ = l

Tactic:
rw [ih]

Result:
case cons.succ
α : Type u_1
a✝¹ a : α
l : List α
ih : ∀ {n : Nat}, l.length ≤ n → l.set n a✝¹ = l
n✝ : Nat
a✝ : (a :: l).length ≤ n✝ → (a :: l).set n✝ a✝¹ = a :: l
h : (a :: l).length ≤ n✝ + 1
⊢ l.length ≤ n✝
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.pairwise_of_forall_ne {l : List α} {r : α → α → Prop} (hl : l.Nodup)
    (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b) : l.Pairwise r

Proof state:
case a
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ≠ b

Tactic:
exact heq

Result:
no goals

Proof state:
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
⊢ Pairwise r l

Tactic:
rw [pairwise_iff_forall_sublist]

Result:
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
⊢ ∀ {a b : α}, [a, b] <+ l → r a b

Proof state:
case a.a
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ [a, b]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
⊢ ∀ {a b : α}, [a, b] <+ l → r a b

Tactic:
intro a b hab

Result:
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a b : α
hab : [a, b] <+ l
⊢ r a b

Proof state:
case a
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ l

Tactic:
(apply hab.subset; simp)

Result:
no goals

Proof state:
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a b : α
hab : [a, b] <+ l
⊢ r a b

Tactic:
if heq : a = b then
  cases heq; have := nodup_iff_sublist.mp hl _ hab; contradiction
else
  apply h <;> try (apply hab.subset; simp)
  exact heq

Result:
no goals

Proof state:
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a b : α
hab : [a, b] <+ l
heq : a = b
⊢ r a b

Tactic:
cases heq

Result:
case refl
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a : α
hab : [a, a] <+ l
⊢ r a a

Proof state:
case a
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ l

Tactic:
apply hab.subset

Result:
case a.a
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ [a, b]

Proof state:
case refl
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a : α
hab : [a, a] <+ l
⊢ r a a

Tactic:
have := nodup_iff_sublist.mp hl _ hab

Result:
case refl
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a : α
hab : [a, a] <+ l
this : False
⊢ r a a

Proof state:
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ r a b

Tactic:
apply h <;> try (apply hab.subset; simp)

Result:
case a
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ≠ b

Proof state:
case refl
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b
a : α
hab : [a, a] <+ l
this : False
⊢ r a a

Tactic:
contradiction

Result:
no goals
-- Mathlib/Algebra/IsPrimePow.lean
theorem not_isPrimePow_zero [NoZeroDivisors R] : ¬IsPrimePow (0 : R)

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : NoZeroDivisors R
⊢ ∀ (x : R) (x_1 : ℕ), 0 < x_1 → x ^ x_1 = 0 → ¬Prime x

Tactic:
intro x n _hn hx

Result:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : NoZeroDivisors R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime x

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : NoZeroDivisors R
⊢ ¬IsPrimePow 0

Tactic:
simp only [isPrimePow_def, not_exists, not_and', and_imp]

Result:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : NoZeroDivisors R
⊢ ∀ (x : R) (x_1 : ℕ), 0 < x_1 → x ^ x_1 = 0 → ¬Prime x

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : NoZeroDivisors R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : NoZeroDivisors R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime x

Tactic:
rw [pow_eq_zero hx]

Result:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : NoZeroDivisors R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime 0