harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_eq_iff {l : Array α} : mapIdx f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map (f i)

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : Array α✝
l : Array α
⊢ mapIdx f l = l' ↔ ∀ (i : Nat), l'[i]? = Option.map (f i) l[i]?

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : Array α✝
l : List α
⊢ mapIdx f { toList := l } = l' ↔ ∀ (i : Nat), l'[i]? = Option.map (f i) { toList := l }[i]?

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l' : Array α✝
l : List α
⊢ mapIdx f { toList := l } = l' ↔ ∀ (i : Nat), l'[i]? = Option.map (f i) { toList := l }[i]?

Tactic:
rcases l' with ⟨l'⟩

Result:
case mk.mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
l' : List α✝
⊢ mapIdx f { toList := l } = { toList := l' } ↔ ∀ (i : Nat), { toList := l' }[i]? = Option.map (f i) { toList := l }[i]?

Proof state:
case mk.mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
l' : List α✝
⊢ mapIdx f { toList := l } = { toList := l' } ↔ ∀ (i : Nat), { toList := l' }[i]? = Option.map (f i) { toList := l }[i]?

Tactic:
simp [List.mapIdx_eq_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem find?_range_eq_none {n : Nat} {p : Nat → Bool} :
    (range n).find? p = none ↔ ∀ i, i < n → !p i

Proof state:
n : Nat
p : Nat → Bool
⊢ find? p (range n) = none ↔ ∀ (i : Nat), i < n → (!p i) = true

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_mkVector_of_lt {n : Nat} {m : Nat} (h : m < n) : (mkVector n a)[m]? = some a

Proof state:
α✝ : Type u_1
a : α✝
n m : Nat
h : m < n
⊢ (mkVector n a)[m]? = some a

Tactic:
simp [getElem?_mkVector, h]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem mul_self_mul_inv (a : G₀) : a * a * a⁻¹ = a

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a * a⁻¹ = a

Tactic:
by_cases h : a = 0

Result:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ a * a * a⁻¹ = a

case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a * a⁻¹ = a

Proof state:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ a * a * a⁻¹ = a

Tactic:
rw [h, inv_zero, mul_zero]

Result:
no goals

Proof state:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a * a⁻¹ = a

Tactic:
rw [mul_assoc, mul_inv_cancel₀ h, mul_one]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_le_ceil (a : α) : ⌊a⌋₊ ≤ ⌈a⌉₊

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Tactic:
exact cast_le.1 ((floor_le ha).trans <| le_ceil _)

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Tactic:
obtain ha | ha := le_total a 0

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

case inr
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Tactic:
rw [floor_of_nonpos ha]

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : a ≤ 0
⊢ 0 ≤ ⌈a⌉₊

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : a ≤ 0
⊢ 0 ≤ ⌈a⌉₊

Tactic:
exact Nat.zero_le _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] {a fallback : α} :
    a ∈ m → m.getKey? a = some (m.getKeyD a fallback)

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
a fallback : α
⊢ a ∈ m → m.getKey? a = some (m.getKeyD a fallback)

Tactic:
simpa [mem_iff_contains] using getKey?_eq_some_getKeyD_of_contains

Result:
no goals
-- Mathlib/RingTheory/Ideal/Defs.lean
theorem unit_mul_mem_iff_mem {x y : α} (hy : IsUnit y) : y * x ∈ I ↔ x ∈ I

Proof state:
α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
⊢ y * x ∈ I ↔ x ∈ I

Tactic:
refine ⟨fun h => ?_, fun h => I.mul_mem_left y h⟩

Result:
α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
⊢ x ∈ I

Proof state:
case intro
α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : y' * (y * x) ∈ I
⊢ x ∈ I

Tactic:
rwa [← mul_assoc, hy', one_mul] at this

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
⊢ x ∈ I

Tactic:
obtain ⟨y', hy'⟩ := hy.exists_left_inv

Result:
case intro
α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
⊢ x ∈ I

Proof state:
case intro
α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
⊢ x ∈ I

Tactic:
have := I.mul_mem_left y' h

Result:
case intro
α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : y' * (y * x) ∈ I
⊢ x ∈ I
-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
@[simp]
lemma netEntropyEntourage_empty {T : X → X} {U : Set (X × X)} : netEntropyEntourage T ∅ U = ⊥

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
⊢ ∃ a, ∀ b ≥ a, ⊥ / ↑b = ⊥

Tactic:
exact ⟨1, fun n n_pos ↦ bot_div_of_pos_ne_top (Nat.cast_pos'.2 n_pos) (natCast_ne_top n)⟩

Result:
no goals

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
h : ∀ᶠ (n : ℕ) in atTop, (↑(netMaxcard T ∅ U n)).log / ↑n = ⊥
⊢ netEntropyEntourage T ∅ U = ⊥

Tactic:
rw [netEntropyEntourage, limsup_congr h]

Result:
X : Type u_1
T : X → X
U : Set (X × X)
h : ∀ᶠ (n : ℕ) in atTop, (↑(netMaxcard T ∅ U n)).log / ↑n = ⊥
⊢ limsup (fun a => ⊥) atTop = ⊥

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑(netMaxcard T ∅ U n)).log / ↑n = ⊥

Tactic:
simp only [netMaxcard_empty, ENat.toENNReal_zero, log_zero, eventually_atTop]

Result:
X : Type u_1
T : X → X
U : Set (X × X)
⊢ ∃ a, ∀ b ≥ a, ⊥ / ↑b = ⊥

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
h : ∀ᶠ (n : ℕ) in atTop, (↑(netMaxcard T ∅ U n)).log / ↑n = ⊥
⊢ limsup (fun a => ⊥) atTop = ⊥

Tactic:
exact limsup_const ⊥

Result:
no goals

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
⊢ netEntropyEntourage T ∅ U = ⊥

Tactic:
suffices h : ∀ᶠ n : ℕ in atTop, log (netMaxcard T ∅ U n) / n = ⊥ by
  rw [netEntropyEntourage, limsup_congr h]
  exact limsup_const ⊥

Result:
X : Type u_1
T : X → X
U : Set (X × X)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑(netMaxcard T ∅ U n)).log / ↑n = ⊥
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_eq_sdiff_iff_inf_eq_inf : y \ x = y \ z ↔ y ⊓ x = y ⊓ z :=
  ⟨fun h => eq_of_inf_eq_sup_eq (a := y \ x) (by rw [inf_inf_sdiff, h, inf_inf_sdiff])
    (by rw [sup_inf_sdiff, h, sup_inf_sdiff]),
    fun h => by rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]⟩

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
⊢ y ⊓ x ⊓ y \ x = y ⊓ z ⊓ y \ x

Tactic:
rw [inf_inf_sdiff, h, inf_inf_sdiff]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y ⊓ x = y ⊓ z
⊢ y \ x = y \ z

Tactic:
rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
⊢ y ⊓ x ⊔ y \ x = y ⊓ z ⊔ y \ x

Tactic:
rw [sup_inf_sdiff, h, sup_inf_sdiff]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Bilinear.lean
theorem map₂_bot_left (f : M →ₗ[R] N →ₗ[R] P) (q : Submodule R N) : map₂ f ⊥ q = ⊥ :=
  eq_bot_iff.2 <|
    map₂_le.2 fun m hm n _ => by
      rw [Submodule.mem_bot] at hm ⊢
      rw [hm, LinearMap.map_zero₂]

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
q : Submodule R N
m : M
hm : m ∈ ⊥
n : N
x✝ : n ∈ q
⊢ (f m) n ∈ ⊥

Tactic:
rw [Submodule.mem_bot] at hm ⊢

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
q : Submodule R N
m : M
hm : m = 0
n : N
x✝ : n ∈ q
⊢ (f m) n = 0

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
q : Submodule R N
m : M
hm : m = 0
n : N
x✝ : n ∈ q
⊢ (f m) n = 0

Tactic:
rw [hm, LinearMap.map_zero₂]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
lemma stableUnderComposition (hP : RingHom.StableUnderComposition Q) :
    P.IsStableUnderComposition where
  comp_mem {X Y Z} f g hf hg

Proof state:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
this : ∀ {X Y : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Y → P (f ≫ g)
hY : ¬IsAffine Y
i : (Scheme.Cover.pullbackCover Y.affineCover f).J
⊢ P ((Scheme.Cover.pullbackCover Y.affineCover f).map i ≫ f ≫ g)

Tactic:
rw [← Scheme.Cover.pullbackHom_map_assoc]

Result:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
this : ∀ {X Y : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Y → P (f ≫ g)
hY : ¬IsAffine Y
i : (Scheme.Cover.pullbackCover Y.affineCover f).J
⊢ P (Scheme.Cover.pullbackHom Y.affineCover f i ≫ Y.affineCover.map i ≫ g)
-- Mathlib/Data/List/OfFn.lean
lemma ofFn_cons {n} (a : α) (f : Fin n → α) : ofFn (Fin.cons a f) = a :: ofFn f

Proof state:
α : Type u
n : ℕ
a : α
f : Fin n → α
⊢ (Fin.cons a f 0 :: ofFn fun i => Fin.cons a f i.succ) = a :: ofFn f

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
n : ℕ
a : α
f : Fin n → α
⊢ ofFn (Fin.cons a f) = a :: ofFn f

Tactic:
rw [ofFn_succ]

Result:
α : Type u
n : ℕ
a : α
f : Fin n → α
⊢ (Fin.cons a f 0 :: ofFn fun i => Fin.cons a f i.succ) = a :: ofFn f
-- Mathlib/Analysis/MellinTransform.lean
theorem isBigO_rpow_top_log_smul [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} (hab : b < a)
    (hf : f =O[atTop] (· ^ (-a))) :
    (fun t : ℝ => log t • f t) =O[atTop] (· ^ (-b))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : b < a
hf : f =O[atTop] fun x => x ^ (-a)
t : ℝ
ht : 0 < t
⊢ t ^ (a - b) • t ^ (-a) = t ^ (-b)

Tactic:
rw [smul_eq_mul, ← rpow_add ht, ← sub_eq_add_neg, sub_eq_add_neg a, add_sub_cancel_left]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : b < a
hf : f =O[atTop] fun x => x ^ (-a)
⊢ (fun t => log t • f t) =O[atTop] fun x => x ^ (-b)

Tactic:
refine
  ((isLittleO_log_rpow_atTop (sub_pos.mpr hab)).isBigO.smul hf).congr'
    (Eventually.of_forall fun t => by rfl)
    ((eventually_gt_atTop 0).mp (Eventually.of_forall fun t ht => ?_))

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : b < a
hf : f =O[atTop] fun x => x ^ (-a)
t : ℝ
ht : 0 < t
⊢ (fun x => x ^ (a - b) • x ^ (-a)) t = (fun x => x ^ (-b)) t

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : b < a
hf : f =O[atTop] fun x => x ^ (-a)
t : ℝ
⊢ (fun x => log x • f x) t = (fun t => log t • f t) t

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : b < a
hf : f =O[atTop] fun x => x ^ (-a)
t : ℝ
ht : 0 < t
⊢ (fun x => x ^ (a - b) • x ^ (-a)) t = (fun x => x ^ (-b)) t

Tactic:
simp only

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : b < a
hf : f =O[atTop] fun x => x ^ (-a)
t : ℝ
ht : 0 < t
⊢ t ^ (a - b) • t ^ (-a) = t ^ (-b)
-- Mathlib/Logic/Equiv/Fin.lean
theorem finSuccEquiv'_at (i : Fin (n + 1)) : (finSuccEquiv' i) i = none

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ (finSuccEquiv' i) i = none

Tactic:
simp [finSuccEquiv']

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
lemma contMDiff_of_discreteTopology [DiscreteTopology M] :
    ContMDiff I I' n f

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝ : DiscreteTopology M
x : M
⊢ ContMDiffAt I I' n f x

Tactic:
apply contMDiff_const (c := f x).contMDiffAt.congr_of_eventuallyEq

Result:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝ : DiscreteTopology M
x : M
⊢ f =ᶠ[𝓝 x] fun x_1 => f x

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝ : DiscreteTopology M
x : M
⊢ f =ᶠ[𝓝 x] fun x_1 => f x

Tactic:
simp [EventuallyEq]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝ : DiscreteTopology M
⊢ ContMDiff I I' n f

Tactic:
intro x

Result:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝ : DiscreteTopology M
x : M
⊢ ContMDiffAt I I' n f x
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem mem_vars_rename (f : σ → τ) (φ : MvPolynomial σ R) {j : τ} (h : j ∈ (rename f φ).vars) :
    ∃ i : σ, i ∈ φ.vars ∧ f i = j

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
j : τ
h : j ∈ ((rename f) φ).vars
⊢ ∃ i ∈ φ.vars, f i = j

Tactic:
simpa only [exists_prop, Finset.mem_image] using vars_rename f φ h

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
j : τ
h : j ∈ ((rename f) φ).vars
⊢ ∃ i ∈ φ.vars, f i = j

Tactic:
classical
simpa only [exists_prop, Finset.mem_image] using vars_rename f φ h

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/Basic.lean
theorem liftp_iff' {α : Type u} (p : α → Prop) (a : P.A) (f : P.B a → α) :
    @Liftp.{u} P.Obj _ α p ⟨a, f⟩ ↔ ∀ i, p (f i)

Proof state:
case mpr.h.h.right
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
assumption

Result:
no goals

Proof state:
case mpr
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)

Tactic:
repeat' first |constructor|assumption

Result:
no goals

Proof state:
case mpr.h.h.right
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
first |constructor|assumption

Result:
no goals

Proof state:
case mpr.h.h.left
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩

Tactic:
constructor

Result:
no goals

Proof state:
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ Liftp p ⟨a, f⟩ ↔ ∀ (i : P.B a), p (f i)

Tactic:
simp only [liftp_iff, Sigma.mk.inj_iff]

Result:
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)) ↔ ∀ (i : P.B a), p (f i)

Proof state:
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)) ↔ ∀ (i : P.B a), p (f i)

Tactic:
constructor <;> intro h

Result:
case mp
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)
⊢ ∀ (i : P.B a), p (f i)

case mpr
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)

Proof state:
case mp.intro.intro.intro
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
a' : P.A
f' : P.B a' → α
heq : ⟨a, f⟩ = ⟨a', f'⟩
h' : ∀ (i : P.B a'), p (f' i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
cases heq

Result:
case mp.intro.intro.intro.refl
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h' : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B a), p (f i)

Proof state:
case mp
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
rcases h with ⟨a', f', heq, h'⟩

Result:
case mp.intro.intro.intro
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
a' : P.A
f' : P.B a' → α
heq : ⟨a, f⟩ = ⟨a', f'⟩
h' : ∀ (i : P.B a'), p (f' i)
⊢ ∀ (i : P.B a), p (f i)

Proof state:
case mp.intro.intro.intro.refl
P : PFunctor.{u}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h' : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
assumption

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma absolutelyContinuous_tilted (hf : Integrable (fun x ↦ exp (f x)) μ) : μ ≪ μ.tilted f

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
h : μ = 0
x✝¹ : Set α
x✝ : 0 x✝¹ = 0
⊢ 0 x✝¹ = 0

Tactic:
simp

Result:
no goals

Proof state:
case inr.refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
h0 : NeZero μ
⊢ AEMeasurable (fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ

Tactic:
exact (hf.1.aemeasurable.div_const _).ennreal_ofReal

Result:
no goals

Proof state:
case inr.refine_2.h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
h0 : NeZero μ
⊢ ∀ (a : α), 0 < rexp (f a) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)

Result:
no goals

Proof state:
case inr.refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
h0 : NeZero μ
⊢ ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ≠ 0

Tactic:
filter_upwards

Result:
case inr.refine_2.h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
h0 : NeZero μ
⊢ ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ≠ 0

Proof state:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
h : μ = 0
⊢ 0 ≪ 0

Tactic:
exact fun _ _ ↦ by simp

Result:
no goals

Proof state:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
h : μ = 0
⊢ μ ≪ μ.tilted f

Tactic:
simp only [h, tilted_zero_measure]

Result:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
h : μ = 0
⊢ 0 ≪ 0

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
h0 : NeZero μ
⊢ μ ≪ μ.tilted f

Tactic:
refine withDensity_absolutelyContinuous' ?_ ?_

Result:
case inr.refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
h0 : NeZero μ
⊢ AEMeasurable (fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ

case inr.refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
h0 : NeZero μ
⊢ ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ≠ 0

Proof state:
case inr.refine_2.h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
h0 : NeZero μ
⊢ ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ≠ 0

Tactic:
simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]

Result:
case inr.refine_2.h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
h0 : NeZero μ
⊢ ∀ (a : α), 0 < rexp (f a) / ∫ (x : α), rexp (f x) ∂μ