harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Int/ModEq.lean
theorem cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [ZMOD m]) :
    a ≡ b [ZMOD m / gcd m c]

Proof state:
case refine_2
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ (m / ↑(m.gcd c)).gcd (c / ↑d) = 1

Tactic:
rw [gcd_div gcd_dvd_left gcd_dvd_right, natAbs_ofNat,
  Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]

Result:
no goals

Proof state:
case refine_1
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑d ∣ c / ↑d * (b - a)

Tactic:
rw [mul_comm, ← Int.mul_ediv_assoc (b - a) gcd_dvd_right, Int.sub_mul]

Result:
case refine_1
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑d ∣ (b * c - a * c) / ↑(m.gcd c)

Proof state:
case refine_1
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑d ∣ (b * c - a * c) / ↑(m.gcd c)

Tactic:
exact Int.ediv_dvd_ediv gcd_dvd_left h

Result:
no goals

Proof state:
m a b c : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
⊢ a ≡ b [ZMOD m / ↑(m.gcd c)]

Tactic:
letI d := gcd m c

Result:
m a b c : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := m.gcd c
⊢ a ≡ b [ZMOD m / ↑(m.gcd c)]

Proof state:
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑(m.gcd c) ∣ b - a

Tactic:
refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_

Result:
case refine_1
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑d ∣ c / ↑d * (b - a)

case refine_2
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ (m / ↑(m.gcd c)).gcd (c / ↑d) = 1

Proof state:
m a b c : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := m.gcd c
⊢ a ≡ b [ZMOD m / ↑(m.gcd c)]

Tactic:
rw [modEq_iff_dvd] at h ⊢

Result:
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑(m.gcd c) ∣ b - a
-- Mathlib/Data/Real/ConjExponents.lean
lemma isConjExponent_iff_eq_conjExponent (hp : 1 < p) : p.IsConjExponent q ↔ q = p / (p - 1) :=
  ⟨IsConjExponent.conj_eq, fun h ↦ ⟨hp, by field_simp [h]⟩⟩

Proof state:
p q : ℝ
hp : 1 < p
h : q = p / (p - 1)
⊢ p⁻¹ + q⁻¹ = 1

Tactic:
field_simp [h]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem Unit_of_divided_by_X_pow_order_nonzero {f : k⟦X⟧} (hf : f ≠ 0) :
    ↑(Unit_of_divided_by_X_pow_order f) = divided_by_X_pow_order hf

Proof state:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ ↑f.Unit_of_divided_by_X_pow_order = divided_by_X_pow_order hf

Tactic:
simp only [Unit_of_divided_by_X_pow_order, dif_neg hf, Units.val_mk]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem lt_sup_iff : a < b ⊔ c ↔ a < b ∨ a < c

Proof state:
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ a < b ⊔ c ↔ a < b ∨ a < c

Tactic:
exact ⟨fun h =>
  (le_total c b).imp
    (fun bc => by rwa [sup_eq_left.2 bc] at h)
    (fun bc => by rwa [sup_eq_right.2 bc] at h),
  fun h => h.elim lt_sup_of_lt_left lt_sup_of_lt_right⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : LinearOrder α
a b c : α
h : a < b ⊔ c
bc : c ≤ b
⊢ a < b

Tactic:
rwa [sup_eq_left.2 bc] at h

Result:
no goals

Proof state:
α : Type u
inst✝ : LinearOrder α
a b c : α
h : a < b ⊔ c
bc : b ≤ c
⊢ a < c

Tactic:
rwa [sup_eq_right.2 bc] at h

Result:
no goals
-- Mathlib/Logic/Function/FiberPartition.lean
lemma map_eq_image (f : Y → Z) (a : Fiber f) (x : a.1) : f x = a.image

Proof state:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : ↑↑a
⊢ f ↑x = image f a

Tactic:
have := a.2.choose_spec

Result:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : ↑↑a
this : (fun x => f ⁻¹' {↑x}) (Exists.choose ⋯) = ↑a
⊢ f ↑x = image f a

Proof state:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : ↑↑a
this : (fun x => f ⁻¹' {↑x}) (Exists.choose ⋯) = ↑a
⊢ ↑x ∈ f ⁻¹' {image f a}

Tactic:
convert x.prop

Result:
no goals

Proof state:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : ↑↑a
this : (fun x => f ⁻¹' {↑x}) (Exists.choose ⋯) = ↑a
⊢ f ↑x = image f a

Tactic:
rw [← Set.mem_singleton_iff, ← Set.mem_preimage]

Result:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : ↑↑a
this : (fun x => f ⁻¹' {↑x}) (Exists.choose ⋯) = ↑a
⊢ ↑x ∈ f ⁻¹' {image f a}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mod_eq_sub (x w : Nat) : x % w = x - w * (x / w)

Proof state:
x w : Nat
⊢ x % w = x % w + w * (x / w) - w * (x / w)

Tactic:
simp

Result:
no goals

Proof state:
x w : Nat
⊢ x % w = x - w * (x / w)

Tactic:
conv => rhs; congr; rw [← mod_add_div x w]

Result:
x w : Nat
⊢ x % w = x % w + w * (x / w) - w * (x / w)
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
/-- The fractional ideals of a Noetherian ring are finitely generated. -/
lemma fg_of_isNoetherianRing [hR : IsNoetherianRing R] (hS : S ≤ R⁰) (I : FractionalIdeal S P) :
    FG I.coeToSubmodule

Proof state:
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
S : Submonoid R
P : Type u_4
inst✝³ : Nontrivial P
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hR : IsNoetherianRing R
hS : S ≤ R⁰
I : FractionalIdeal S P
this : ⊤.FG
⊢ ⊤.FG

Tactic:
exact fg_of_linearEquiv (I.equivNum <| coe_ne_zero ⟨(I.den : R), hS (SetLike.coe_mem I.den)⟩) this

Result:
no goals

Proof state:
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
S : Submonoid R
P : Type u_4
inst✝³ : Nontrivial P
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hR : IsNoetherianRing R
hS : S ≤ R⁰
I : FractionalIdeal S P
this : FG I.num
⊢ (↑I).FG

Tactic:
rw [← fg_top] at this ⊢

Result:
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
S : Submonoid R
P : Type u_4
inst✝³ : Nontrivial P
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hR : IsNoetherianRing R
hS : S ≤ R⁰
I : FractionalIdeal S P
this : ⊤.FG
⊢ ⊤.FG

Proof state:
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
S : Submonoid R
P : Type u_4
inst✝³ : Nontrivial P
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hR : IsNoetherianRing R
hS : S ≤ R⁰
I : FractionalIdeal S P
⊢ (↑I).FG

Tactic:
have := hR.noetherian I.num

Result:
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
S : Submonoid R
P : Type u_4
inst✝³ : Nontrivial P
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hR : IsNoetherianRing R
hS : S ≤ R⁰
I : FractionalIdeal S P
this : FG I.num
⊢ (↑I).FG
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem perm_append_right_iff {l₁ l₂ : List α} (l) : l₁ ++ l ~ l₂ ++ l ↔ l₁ ~ l₂

Proof state:
α : Type u_1
l₁ l₂ l : List α
p : l₁ ++ l ~ l₂ ++ l
⊢ l₁ ~ l₂

Tactic:
exact (perm_append_left_iff _).1 <| perm_append_comm.trans <| p.trans perm_append_comm

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ l : List α
⊢ l₁ ++ l ~ l₂ ++ l ↔ l₁ ~ l₂

Tactic:
refine ⟨fun p => ?_, .append_right _⟩

Result:
α : Type u_1
l₁ l₂ l : List α
p : l₁ ++ l ~ l₂ ++ l
⊢ l₁ ~ l₂
-- Mathlib/Data/Set/Prod.lean
theorem offDiag_empty : (∅ : Set α).offDiag = ∅

Proof state:
α : Type u_1
⊢ ∅.offDiag = ∅

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_le_iff {a b : Ordinal} : a.toPGame ≤ b.toPGame ↔ a ≤ b :=
  ⟨by contrapose; rw [not_le, PGame.not_le]; exact toPGame_lf, toPGame_le⟩

Proof state:
a b : Ordinal.{u_1}
⊢ ¬a ≤ b → ¬a.toPGame ≤ b.toPGame

Tactic:
rw [not_le, PGame.not_le]

Result:
a b : Ordinal.{u_1}
⊢ b < a → b.toPGame ⧏ a.toPGame

Proof state:
a b : Ordinal.{u_1}
⊢ b < a → b.toPGame ⧏ a.toPGame

Tactic:
exact toPGame_lf

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
⊢ a.toPGame ≤ b.toPGame → a ≤ b

Tactic:
contrapose

Result:
a b : Ordinal.{u_1}
⊢ ¬a ≤ b → ¬a.toPGame ≤ b.toPGame
-- Mathlib/Topology/Algebra/TopologicallyNilpotent.lean
theorem map {F : Type*} [FunLike F R S] [MonoidWithZeroHomClass F R S]
    {φ : F} (hφ : Continuous φ) {a : R} (ha : IsTopologicallyNilpotent a) :
    IsTopologicallyNilpotent (φ a)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : TopologicalSpace R
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : TopologicalSpace S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
φ : F
hφ : Continuous ⇑φ
a : R
ha : Tendsto (fun x => a ^ x) atTop (𝓝 0)
⊢ Tendsto (fun x => φ (a ^ x)) atTop (𝓝 0)

Tactic:
exact (map_zero φ ▸ hφ.tendsto 0).comp ha

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : TopologicalSpace R
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : TopologicalSpace S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
φ : F
hφ : Continuous ⇑φ
a : R
ha : Tendsto (fun x => a ^ x) atTop (𝓝 0)
⊢ Tendsto (fun x => φ a ^ x) atTop (𝓝 0)

Tactic:
simp_rw [← map_pow]

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : TopologicalSpace R
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : TopologicalSpace S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
φ : F
hφ : Continuous ⇑φ
a : R
ha : Tendsto (fun x => a ^ x) atTop (𝓝 0)
⊢ Tendsto (fun x => φ (a ^ x)) atTop (𝓝 0)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : TopologicalSpace R
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : TopologicalSpace S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
φ : F
hφ : Continuous ⇑φ
a : R
ha : IsTopologicallyNilpotent a
⊢ IsTopologicallyNilpotent (φ a)

Tactic:
unfold IsTopologicallyNilpotent at ha ⊢

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : TopologicalSpace R
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : TopologicalSpace S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
φ : F
hφ : Continuous ⇑φ
a : R
ha : Tendsto (fun x => a ^ x) atTop (𝓝 0)
⊢ Tendsto (fun x => φ a ^ x) atTop (𝓝 0)
-- Mathlib/.lake/packages/batteries/Batteries/Logic.lean
theorem eq_rec_constant {α : Sort _} {a a' : α} {β : Sort _} (y : β) (h : a = a') :
    (@Eq.rec α a (fun _ _ => β) y a' h) = y

Proof state:
case refl
α : Sort u_1
a : α
β : Sort u_2
y : β
⊢ ⋯ ▸ y = y

Tactic:
rfl

Result:
no goals

Proof state:
α : Sort u_1
a a' : α
β : Sort u_2
y : β
h : a = a'
⊢ h ▸ y = y

Tactic:
cases h

Result:
case refl
α : Sort u_1
a : α
β : Sort u_2
y : β
⊢ ⋯ ▸ y = y
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem cos_oangle_sub_left_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.cos (o.oangle (x - y) x) = ‖x‖ / ‖x - y‖

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

Tactic:
exact (-o).cos_oangle_sub_right_of_oangle_eq_pi_div_two h

Result:
no goals

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

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle x (x - y)).cos = ‖x‖ / ‖x - y‖
-- Mathlib/MeasureTheory/Function/Floor.lean
theorem Nat.measurable_floor : Measurable (Nat.floor : R → ℕ) :=
  measurable_to_countable fun n => by
    rcases eq_or_ne ⌊n⌋₊ 0 with h | h <;> simp [h, Nat.preimage_floor_of_ne_zero, -floor_eq_zero]

Proof state:
R : Type u_2
inst✝⁵ : LinearOrderedSemiring R
inst✝⁴ : FloorSemiring R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
n : R
⊢ MeasurableSet (floor ⁻¹' {⌊n⌋₊})

Tactic:
rcases eq_or_ne ⌊n⌋₊ 0 with h | h <;> simp [h, Nat.preimage_floor_of_ne_zero, -floor_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem lt_length_right_of_zipWith {f : α → β → γ} {i : Nat} {l : List α} {l' : List β}
    (h : i < (zipWith f l l').length) : i < l'.length

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
l : List α
l' : List β
h : i < (zipWith f l l').length
⊢ i < l'.length

Tactic:
rw [length_zipWith] at h

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
l : List α
l' : List β
h : i < min l.length l'.length
⊢ i < l'.length

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
l : List α
l' : List β
h : i < min l.length l'.length
⊢ i < l'.length

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Fin/VecNotation.lean
theorem empty_vecAlt0 (α) {h} : vecAlt0 h (![] : Fin 0 → α) = ![]

Proof state:
α : Type u_1
h : 0 = 0 + 0
⊢ vecAlt0 h ![] = ![]

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem isLUB_le_iff (h : IsLUB s a) : a ≤ b ↔ b ∈ upperBounds s

Proof state:
α : Type u
inst✝ : Preorder α
s : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ Ici a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
inst✝ : Preorder α
s : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ upperBounds s

Tactic:
rw [h.upperBounds_eq]

Result:
α : Type u
inst✝ : Preorder α
s : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ Ici a
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive (attr := simp)] lemma leOnePart_div_oneLePart (a : α) : a⁻ᵐ / a⁺ᵐ = a⁻¹

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a : α
⊢ a⁻ᵐ / a⁺ᵐ = a⁻¹

Tactic:
rw [← inv_div, oneLePart_div_leOnePart]

Result:
no goals
-- Mathlib/Order/Disjointed.lean
protected lemma Monotone.disjointed_succ {f : ι → α} (hf : Monotone f) {i : ι} (hn : ¬IsMax i) :
    disjointed f (succ i) = f (succ i) \ f i

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
hn : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ f i

Tactic:
rwa [disjointed_succ, hf.partialSups_eq]

Result:
no goals
-- Mathlib/Probability/Distributions/Gamma.lean
lemma gammaCDFReal_eq_integral {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) :
    gammaCDFReal a r x = ∫ x in Iic x, gammaPDFReal a r x

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
⊢ ↑(gammaCDFReal a r) x = ∫ (x : ℝ) in Iic x, gammaPDFReal a r x

Tactic:
have : IsProbabilityMeasure (gammaMeasure a r) := isProbabilityMeasureGamma ha hr

Result:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ ↑(gammaCDFReal a r) x = ∫ (x : ℝ) in Iic x, gammaPDFReal a r x

Proof state:
case refine_1
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ 0 ≤ᶠ[ae (ℙ.restrict (Iic x))] gammaPDFReal a r

Tactic:
exact ae_of_all _ fun b ↦ by simp only [Pi.zero_apply, gammaPDFReal_nonneg ha hr]

Result:
no goals

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
b : ℝ
⊢ 0 b ≤ gammaPDFReal a r b

Tactic:
simp only [Pi.zero_apply, gammaPDFReal_nonneg ha hr]

Result:
no goals

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ (∫⁻ (a_1 : ℝ) in Iic x, gammaPDF a r a_1).toReal = ∫ (x : ℝ) in Iic x, gammaPDFReal a r x

Tactic:
refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm

Result:
case refine_1
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ 0 ≤ᶠ[ae (ℙ.restrict (Iic x))] gammaPDFReal a r

case refine_2
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ AEStronglyMeasurable (gammaPDFReal a r) (ℙ.restrict (Iic x))

Proof state:
case refine_2
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ AEStronglyMeasurable (gammaPDFReal a r) (ℙ.restrict (Iic x))

Tactic:
exact (measurable_gammaPDFReal a r).aestronglyMeasurable.restrict

Result:
no goals

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ ↑(gammaCDFReal a r) x = ∫ (x : ℝ) in Iic x, gammaPDFReal a r x

Tactic:
rw [gammaCDFReal, cdf_eq_toReal, gammaMeasure, withDensity_apply _ measurableSet_Iic]

Result:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ (∫⁻ (a_1 : ℝ) in Iic x, gammaPDF a r a_1).toReal = ∫ (x : ℝ) in Iic x, gammaPDFReal a r x
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem cyclotomic.roots_to_finset_eq_primitiveRoots [NeZero (n : R)] :
    (⟨(cyclotomic n R).roots, roots_cyclotomic_nodup⟩ : Finset _) = primitiveRoots n R

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
a : R
⊢ a ∈ { val := (cyclotomic n R).roots, nodup := ⋯ } ↔ IsPrimitiveRoot a n

Tactic:
convert isRoot_cyclotomic_iff (n := n) (μ := a) using 0

Result:
case a
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
a : R
⊢ (a ∈ { val := (cyclotomic n R).roots, nodup := ⋯ } ↔ IsPrimitiveRoot a n) ↔
    ((cyclotomic n R).IsRoot a ↔ IsPrimitiveRoot a n)

Proof state:
case a
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
a : R
⊢ (a ∈ { val := (cyclotomic n R).roots, nodup := ⋯ } ↔ IsPrimitiveRoot a n) ↔
    ((cyclotomic n R).IsRoot a ↔ IsPrimitiveRoot a n)

Tactic:
simp [cyclotomic_ne_zero n R]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
a : R
⊢ a ∈ { val := (cyclotomic n R).roots, nodup := ⋯ } ↔ a ∈ primitiveRoots n R

Tactic:
simp only [mem_primitiveRoots, NeZero.pos_of_neZero_natCast R]

Result:
case h
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
a : R
⊢ a ∈ { val := (cyclotomic n R).roots, nodup := ⋯ } ↔ IsPrimitiveRoot a n

Proof state:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
⊢ { val := (cyclotomic n R).roots, nodup := ⋯ } = primitiveRoots n R

Tactic:
ext a

Result:
case h
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
a : R
⊢ a ∈ { val := (cyclotomic n R).roots, nodup := ⋯ } ↔ a ∈ primitiveRoots n R
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma XIsoOfEq_inv_comp_d (K : HomologicalComplex V c) {p₂ p₁ : ι} (h : p₂ = p₁) (p₃ : ι) :
    (K.XIsoOfEq h).inv ≫ K.d p₂ p₃ = K.d p₁ p₃

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
⊢ (K.XIsoOfEq ⋯).inv ≫ K.d p₂ p₃ = K.d p₂ p₃

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₁ : ι
h : p₂ = p₁
p₃ : ι
⊢ (K.XIsoOfEq h).inv ≫ K.d p₂ p₃ = K.d p₁ p₃

Tactic:
subst h

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
⊢ (K.XIsoOfEq ⋯).inv ≫ K.d p₂ p₃ = K.d p₂ p₃
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem add_equiv_add {f1 f2 g1 g2 : CauSeq β abv} (hf : f1 ≈ f2) (hg : g1 ≈ g2) :
    f1 + g1 ≈ f2 + g2

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ f1 + g1 ≈ f2 + g2

Tactic:
simpa only [← add_sub_add_comm] using add_limZero hf hg

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem support_single_of_ne (h : r ≠ 0) : support (single a r) = {a}

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ ((single a) r).support = {a}

Tactic:
classical exact Pi.support_single_of_ne h

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ ((single a) r).support = {a}

Tactic:
exact Pi.support_single_of_ne h

Result:
no goals
-- Mathlib/Algebra/Algebra/Basic.lean
theorem mul_sub_algebraMap_commutes [Ring A] [Algebra R A] (x : A) (r : R) :
    x * (x - algebraMap R A r) = (x - algebraMap R A r) * x

Proof state:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * (x - (algebraMap R A) r) = (x - (algebraMap R A) r) * x

Tactic:
rw [mul_sub, ← commutes, sub_mul]

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem same_add_div (h : b ≠ 0) : (b + a) / b = 1 + a / b

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
a b : K
h : b ≠ 0
⊢ (b + a) / b = 1 + a / b

Tactic:
rw [← div_self h, add_div]

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonUnitalNonAssocRing_injective :
    Function.Injective (@toNonUnitalNonAssocRing R)

Proof state:
R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocRing R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Result:
case mk.mk
R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
⊢ mk mul_comm✝¹ = mk mul_comm✝

Proof state:
case mk.mk
R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
⊢ mk mul_comm✝¹ = mk mul_comm✝

Tactic:
congr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α] [Inhabited α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
    (not_contains : (toInsert.map Prod.fst).contains k = false) :
    getKey! k (insertListConst l toInsert) = getKey! k l

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ getKey! k (insertListConst l toInsert) = getKey! k l

Tactic:
rw [getKey!_eq_getKey?, getKey?_insertListConst_of_contains_eq_false not_contains,
  getKey!_eq_getKey?]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem comp {g : α → α} (hco : Commute f g) (hf : IsPeriodicPt f n x) (hg : IsPeriodicPt g n x) :
    IsPeriodicPt (f ∘ g) n x

Proof state:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f^[n] ∘ g^[n]) x

Tactic:
exact IsFixedPt.comp hf hg

Result:
no goals

Proof state:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt (f ∘ g) n x

Tactic:
rw [IsPeriodicPt, hco.comp_iterate]

Result:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f^[n] ∘ g^[n]) x
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem IsOrtho.comap_iff (f : E ≃ₗᵢ[𝕜] F) {U V : Submodule 𝕜 F} : U.comap f ⟂ V.comap f ↔ U ⟂ V :=
  ⟨fun h => by
    have hf : ∀ p : Submodule 𝕜 F, (p.comap f).map f.toLinearIsometry = p :=
      map_comap_eq_of_surjective f.surjective
    simpa only [hf] using h.map f.toLinearIsometry, IsOrtho.comap f.toLinearIsometry⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : Submodule.comap f U ⟂ Submodule.comap f V
⊢ U ⟂ V

Tactic:
have hf : ∀ p : Submodule 𝕜 F, (p.comap f).map f.toLinearIsometry = p :=
  map_comap_eq_of_surjective f.surjective

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : Submodule.comap f U ⟂ Submodule.comap f V
hf : ∀ (p : Submodule 𝕜 F), Submodule.map f.toLinearIsometry (Submodule.comap f p) = p
⊢ U ⟂ V

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : Submodule.comap f U ⟂ Submodule.comap f V
hf : ∀ (p : Submodule 𝕜 F), Submodule.map f.toLinearIsometry (Submodule.comap f p) = p
⊢ U ⟂ V

Tactic:
simpa only [hf] using h.map f.toLinearIsometry

Result:
no goals