harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_cast {x : BitVec w} (h : w = w') : ~~~(x.cast h) = (~~~x).cast h

Proof state:
w w' : Nat
x : BitVec w
h : w = w'
⊢ ~~~BitVec.cast h x = BitVec.cast h (~~~x)

Tactic:
ext

Result:
case pred
w w' : Nat
x : BitVec w
h : w = w'
i✝ : Nat
a✝ : i✝ < w'
⊢ (~~~BitVec.cast h x).getLsbD i✝ = (BitVec.cast h (~~~x)).getLsbD i✝

Proof state:
case pred
w w' : Nat
x : BitVec w
h : w = w'
i✝ : Nat
a✝ : i✝ < w'
⊢ (~~~BitVec.cast h x).getLsbD i✝ = (BitVec.cast h (~~~x)).getLsbD i✝

Tactic:
simp_all [lt_of_getLsbD]

Result:
no goals
-- Mathlib/Data/Fintype/EquivFin.lean
theorem sigma_of_right {β : α → Type*} {a : α} [Infinite (β a)] :
    Infinite ((a : α) × β a) :=
  Infinite.of_injective (f := fun x ↦ ⟨a,x⟩) fun _ _ ↦ by simp

Proof state:
α : Type u_1
β : α → Type u_4
a : α
inst✝ : Infinite (β a)
x✝¹ x✝ : β a
⊢ (fun x => ⟨a, x⟩) x✝¹ = (fun x => ⟨a, x⟩) x✝ → x✝¹ = x✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem or_assoc (x y z : Nat) : (x ||| y) ||| z = x ||| (y ||| z)

Proof state:
case pred
x y z : Nat
⊢ ∀ (i : Nat), (x ||| y ||| z).testBit i = (x ||| (y ||| z)).testBit i

Tactic:
simp [Bool.or_assoc]

Result:
no goals

Proof state:
x y z : Nat
⊢ x ||| y ||| z = x ||| (y ||| z)

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x y z : Nat
⊢ ∀ (i : Nat), (x ||| y ||| z).testBit i = (x ||| (y ||| z)).testBit i
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extChartAt_image_nhd_mem_nhds_of_boundaryless [I.Boundaryless]
    {x : M} (hx : s ∈ 𝓝 x) : extChartAt I x '' s ∈ 𝓝 (extChartAt I x x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
hx : s ∈ 𝓝 x
⊢ ↑(extChartAt I x) '' s ∈ 𝓝 (↑(extChartAt I x) x)

Tactic:
rw [extChartAt]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
hx : s ∈ 𝓝 x
⊢ ↑((chartAt H x).extend I) '' s ∈ 𝓝 (↑((chartAt H x).extend I) x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
hx : s ∈ 𝓝 x
⊢ ↑((chartAt H x).extend I) '' s ∈ 𝓝 (↑((chartAt H x).extend I) x)

Tactic:
exact extend_image_nhd_mem_nhds_of_boundaryless _ (mem_chart_source H x) hx

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem pow_lt_ascFactorial' (n k : ℕ) : (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2)

Proof state:
n k : ℕ
⊢ (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2)

Tactic:
rw [Nat.pow_succ, ascFactorial, Nat.mul_comm]

Result:
n k : ℕ
⊢ (n + 1) * (n + 1) ^ (k + 1) < (n + 1 + (k + 1)) * (n + 1).ascFactorial (k + 1)

Proof state:
n k : ℕ
⊢ (n + 1) * (n + 1) ^ (k + 1) < (n + 1 + (k + 1)) * (n + 1).ascFactorial (k + 1)

Tactic:
exact Nat.mul_lt_mul_of_lt_of_le' (Nat.lt_add_of_pos_right k.succ_pos)
  (pow_succ_le_ascFactorial n.succ _) (Nat.pow_pos n.succ_pos)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem eq_zero_of_gcd_eq_zero_right {m n : Nat} (H : gcd m n = 0) : n = 0

Proof state:
m n : Nat
H : m.gcd n = 0
⊢ n = 0

Tactic:
rw [gcd_comm] at H

Result:
m n : Nat
H : n.gcd m = 0
⊢ n = 0

Proof state:
m n : Nat
H : n.gcd m = 0
⊢ n = 0

Tactic:
exact eq_zero_of_gcd_eq_zero_left H

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem zeroLocus_singleton_mul (f g : R) :
    zeroLocus ({f * g} : Set R) = zeroLocus {f} ∪ zeroLocus {g} :=
  Set.ext fun x => by simpa using x.2.mul_mem_iff_mem_or_mem

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R
x : PrimeSpectrum R
⊢ x ∈ zeroLocus {f * g} ↔ x ∈ zeroLocus {f} ∪ zeroLocus {g}

Tactic:
simpa using x.2.mul_mem_iff_mem_or_mem

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_le_count_push (a b : α) (l : Vector α n) : count a l ≤ count a (l.push b)

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
l : Array α
⊢ count a { toArray := l, size_toArray := ⋯ } ≤ count a ({ toArray := l, size_toArray := ⋯ }.push b)

Tactic:
simp [Array.count_push]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
n : Nat
a b : α
l : Vector α n
⊢ count a l ≤ count a (l.push b)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
l : Array α
⊢ count a { toArray := l, size_toArray := ⋯ } ≤ count a ({ toArray := l, size_toArray := ⋯ }.push b)
-- Mathlib/MeasureTheory/Covering/DensityTheorem.lean
theorem ae_tendsto_measure_inter_div (S : Set α) (K : ℝ) : ∀ᵐ x ∂μ.restrict S,
    ∀ {ι : Type*} {l : Filter ι} (w : ι → α) (δ : ι → ℝ) (_ : Tendsto δ l (𝓝[>] 0))
      (_ : ∀ᶠ j in l, x ∈ closedBall (w j) (K * δ j)),
      Tendsto (fun j => μ (S ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)

Proof state:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
S : Set α
K : ℝ
⊢ ∀ᵐ (x : α) ∂μ.restrict S,
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[>] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (fun j => μ (S ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)

Tactic:
filter_upwards [(vitaliFamily μ K).ae_tendsto_measure_inter_div S] with x hx ι l w δ δlim
  xmem using hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Transitive.lean
theorem isPretransitive_iff_base (a : X) :
    IsPretransitive G X ↔ ∀ x : X, ∃ g : G, g • a = x where
  mp hG x := exists_smul_eq _ a x
  mpr hG := .mk fun x y ↦ by
    obtain ⟨g, hx⟩ := hG x
    obtain ⟨h, hy⟩ := hG y
    exact ⟨h * g⁻¹, by rw [← hx, smul_smul, inv_mul_cancel_right, hy]⟩

Proof state:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨g, hx⟩ := hG x

Result:
case intro
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
⊢ ∃ g, g • x = y

Proof state:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • x = y

Tactic:
rw [← hx, smul_smul, inv_mul_cancel_right, hy]

Result:
no goals

Proof state:
case intro
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨h, hy⟩ := hG y

Result:
case intro.intro
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ ∃ g, g • x = y

Proof state:
case intro.intro
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ ∃ g, g • x = y

Tactic:
exact ⟨h * g⁻¹, by rw [← hx, smul_smul, inv_mul_cancel_right, hy]⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁} :
    get (m.insert k v) a h₁ =
      if h₂ : k == a then v else get m a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂))

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β
h₁ : a ∈ m.insert k v
⊢ get (m.insert k v) a h₁ = if h₂ : (k == a) = true then v else get m a ⋯

Tactic:
simp_to_raw using Raw₀.Const.get_insert ⟨m, _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem add_le_zero_iff_le_neg {a b : Int} : a + b ≤ 0 ↔ a ≤ - b

Proof state:
a b : Int
⊢ a + b ≤ 0 ↔ a ≤ -b

Tactic:
rw [add_le_iff_le_sub, Int.zero_sub]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_div_eq_div (m n : ℕ) : ⌊(m : α) / n⌋₊ = m / n

Proof state:
case h.e'_3.h.e'_5
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
m n : ℕ
⊢ m = ⌊↑m⌋₊

Tactic:
rw [m.floor_natCast]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
m n : ℕ
⊢ ⌊↑m / ↑n⌋₊ = m / n

Tactic:
convert floor_div_nat (m : α) n

Result:
case h.e'_3.h.e'_5
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
m n : ℕ
⊢ m = ⌊↑m⌋₊
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem conjugate_nonneg' {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ c * a * star c

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
⊢ 0 ≤ c * a * star c

Tactic:
simpa only [star_star] using conjugate_nonneg ha (star c)

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
lemma ceil_lt_iff : ⌈a⌉ < z ↔ a ≤ z - 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌈a⌉ < z ↔ a ≤ ↑z - 1

Tactic:
rw [← le_sub_one_iff, ceil_le]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ a ≤ ↑(z - 1) ↔ a ≤ ↑z - 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ a ≤ ↑(z - 1) ↔ a ≤ ↑z - 1

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Data/PNat/Find.lean
theorem le_find_iff (n : ℕ+) : n ≤ PNat.find h ↔ ∀ m < n, ¬p m

Proof state:
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ+
⊢ n ≤ PNat.find h ↔ ∀ m < n, ¬p m

Tactic:
simp only [← not_lt, find_lt_iff, not_exists, not_and]

Result:
no goals
-- Mathlib/Data/Ordering/Lemmas.lean
theorem cmpUsing_eq_gt [IsStrictOrder α lt] (a b : α) : cmpUsing lt a b = Ordering.gt ↔ lt b a

Proof state:
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ lt b a → ¬lt a b

Tactic:
exact fun hba hab ↦ (irrefl a) (_root_.trans hab hba)

Result:
no goals

Proof state:
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ cmpUsing lt a b = Ordering.gt ↔ lt b a

Tactic:
simp only [cmpUsing, Ordering.ite_eq_gt_distrib, if_false_right, and_true, if_false_left,
  and_iff_right_iff_imp, reduceCtorEq]

Result:
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ lt b a → ¬lt a b
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma one_sub_prime_cpow_ne_zero {p : ℕ} (hp : p.Prime) {s : ℂ} (hs : 1 < s.re) :
    1 - (p : ℂ) ^ (-s) ≠ 0

Proof state:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
⊢ False

Tactic:
have := norm_prime_cpow_le_one_half ⟨p, hp⟩ hs

Result:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : ‖↑↑⟨p, hp⟩ ^ (-s)‖ ≤ 1 / 2
⊢ False

Proof state:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
⊢ 1 - ↑p ^ (-s) ≠ 0

Tactic:
refine sub_ne_zero_of_ne fun H ↦ ?_

Result:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
⊢ False

Proof state:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : ‖↑↑⟨p, hp⟩ ^ (-s)‖ ≤ 1 / 2
⊢ False

Tactic:
simp only at this

Result:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : ‖↑p ^ (-s)‖ ≤ 1 / 2
⊢ False

Proof state:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : ‖↑p ^ (-s)‖ ≤ 1 / 2
⊢ False

Tactic:
rw [← H, norm_one] at this

Result:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : 1 ≤ 1 / 2
⊢ False

Proof state:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : 1 ≤ 1 / 2
⊢ False

Tactic:
norm_num at this

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem map_comp (f : X ⟶ Y) (g : Y ⟶ Z) [Mono f] [Mono g] (x : Subobject X) :
    (map (f ≫ g)).obj x = (map g).obj ((map f).obj x)

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
t : MonoOver X
⊢ (map (f ≫ g)).obj (Quotient.mk'' t) = (map g).obj ((map f).obj (Quotient.mk'' t))

Tactic:
exact Quotient.sound ⟨(MonoOver.mapComp _ _).app t⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
x : Subobject X
⊢ (map (f ≫ g)).obj x = (map g).obj ((map f).obj x)

Tactic:
induction' x using Quotient.inductionOn' with t

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
t : MonoOver X
⊢ (map (f ≫ g)).obj (Quotient.mk'' t) = (map g).obj ((map f).obj (Quotient.mk'' t))
-- Mathlib/Data/Option/NAry.lean
theorem map₂_map_left (f : γ → β → δ) (g : α → γ) :
    map₂ f (a.map g) b = map₂ (fun a b => f (g a) b) a b

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
f : γ → β → δ
g : α → γ
⊢ map₂ f (Option.map g a) b = map₂ (fun a b => f (g a) b) a b

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem domRestrict (H : B.IsSymm) (p : Submodule R M) : (B.domRestrict₁₂ p p).IsSymm :=
  fun _ _ ↦ by
  simp_rw [domRestrict₁₂_apply]
  exact H _ _

Proof state:
R : Type u_1
M : Type u_5
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
p : Submodule R M
x✝¹ x✝ : ↥p
⊢ I (((B.domRestrict₁₂ p p) x✝¹) x✝) = ((B.domRestrict₁₂ p p) x✝) x✝¹

Tactic:
simp_rw [domRestrict₁₂_apply]

Result:
R : Type u_1
M : Type u_5
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
p : Submodule R M
x✝¹ x✝ : ↥p
⊢ I ((B ↑x✝¹) ↑x✝) = (B ↑x✝) ↑x✝¹

Proof state:
R : Type u_1
M : Type u_5
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
p : Submodule R M
x✝¹ x✝ : ↥p
⊢ I ((B ↑x✝¹) ↑x✝) = (B ↑x✝) ↑x✝¹

Tactic:
exact H _ _

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Category.lean
/-- The monoid of natural transformations of the identity is commutative. -/
lemma id_comm (α β : (𝟭 C) ⟶ (𝟭 C)) : α ≫ β = β ≫ α

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α β : 𝟭 C ⟶ 𝟭 C
⊢ α ≫ β = β ≫ α

Tactic:
ext X

Result:
case w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α β : 𝟭 C ⟶ 𝟭 C
X : C
⊢ (α ≫ β).app X = (β ≫ α).app X

Proof state:
case w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α β : 𝟭 C ⟶ 𝟭 C
X : C
⊢ (α ≫ β).app X = (β ≫ α).app X

Tactic:
exact (α.naturality (β.app X)).symm

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_pos {p : ℝ} : 0 < ENNReal.ofReal p ↔ 0 < p

Proof state:
p : ℝ
⊢ 0 < ENNReal.ofReal p ↔ 0 < p

Tactic:
simp [ENNReal.ofReal]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem mul_eq_one_iff_inv_eq {a : α} : ↑u * a = 1 ↔ ↑u⁻¹ = a

Proof state:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
⊢ ↑u * a = 1 ↔ ↑u⁻¹ = a

Tactic:
rw [← inv_mul_eq_one, inv_inv]

Result:
no goals
-- Mathlib/Order/Heyting/Hom.lean
theorem map_symmDiff (a b : α) : f (a ∆ b) = f a ∆ f b

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a b : α
⊢ f (a ∆ b) = f a ∆ f b

Tactic:
simp_rw [symmDiff, map_sup, map_sdiff]

Result:
no goals
-- Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean
theorem prod_self_subset {U} (hU : U ∈ 𝓝 (1 : G × G)) :
    ∃ V : OpenSubgroup G, (V : Set G) ×ˢ (V : Set G) ⊆ U :=
  let ⟨V, W, h⟩ := prod_subset hU
  ⟨V ⊓ W, by refine Set.Subset.trans (Set.prod_mono ?_ ?_) ‹_› <;> simp⟩

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : NonarchimedeanGroup G
U : Set (G × G)
hU : U ∈ 𝓝 1
V W : OpenSubgroup G
h : ↑V ×ˢ ↑W ⊆ U
⊢ ↑(V ⊓ W) ×ˢ ↑(V ⊓ W) ⊆ U

Tactic:
refine Set.Subset.trans (Set.prod_mono ?_ ?_) ‹_› <;> simp

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedDeriv_succ : iteratedDeriv (n + 1) f = deriv (iteratedDeriv n f)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv (n + 1) f = deriv (iteratedDeriv n f)

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDeriv (n + 1) f x = deriv (iteratedDeriv n f) x

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDerivWithin (n + 1) f univ x = derivWithin (iteratedDerivWithin n f univ) univ x

Tactic:
exact iteratedDerivWithin_succ

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDeriv (n + 1) f x = deriv (iteratedDeriv n f) x

Tactic:
rw [← iteratedDerivWithin_univ, ← iteratedDerivWithin_univ, ← derivWithin_univ]

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDerivWithin (n + 1) f univ x = derivWithin (iteratedDerivWithin n f univ) univ x
-- Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean
theorem comp {g : β → γ} {f : α → β} (hg : QuasiMeasurePreserving g μb μc)
    (hf : QuasiMeasurePreserving f μa μb) : QuasiMeasurePreserving (g ∘ f) μa μc :=
  ⟨hg.measurable.comp hf.measurable, by
    rw [← map_map hg.1 hf.1]
    exact (hf.2.map hg.1).trans hg.2⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : QuasiMeasurePreserving g μb μc
hf : QuasiMeasurePreserving f μa μb
⊢ map (g ∘ f) μa ≪ μc

Tactic:
rw [← map_map hg.1 hf.1]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : QuasiMeasurePreserving g μb μc
hf : QuasiMeasurePreserving f μa μb
⊢ map g (map f μa) ≪ μc

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : QuasiMeasurePreserving g μb μc
hf : QuasiMeasurePreserving f μa μb
⊢ map g (map f μa) ≪ μc

Tactic:
exact (hf.2.map hg.1).trans hg.2

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem prev_cons_cons_of_ne' (y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz : x = z) :
    prev (y :: z :: l) x h = y

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
h : x ∈ [y, z]
⊢ [y, z].prev x h = y

Tactic:
simp [prev, hy, hz]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ (y :: z :: head✝ :: tail✝).prev x h = y

Tactic:
rw [prev, dif_neg hy, if_pos hz]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x = z
⊢ (y :: z :: l).prev x h = y

Tactic:
cases l

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
h : x ∈ [y, z]
⊢ [y, z].prev x h = y

case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ (y :: z :: head✝ :: tail✝).prev x h = y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem setIfInBounds_setIfInBounds (a b : α) (v : Vector α n) (i : Nat) :
    (v.setIfInBounds i a).setIfInBounds i b = v.setIfInBounds i b

Proof state:
α : Type u_1
n : Nat
a b : α
v : Vector α n
i : Nat
⊢ (v.setIfInBounds i a).setIfInBounds i b = v.setIfInBounds i b

Tactic:
rcases v with ⟨v, rfl⟩

Result:
case mk
α : Type u_1
a b : α
i : Nat
v : Array α
⊢ ({ toArray := v, size_toArray := ⋯ }.setIfInBounds i a).setIfInBounds i b =
    { toArray := v, size_toArray := ⋯ }.setIfInBounds i b

Proof state:
case mk
α : Type u_1
a b : α
i : Nat
v : Array α
⊢ ({ toArray := v, size_toArray := ⋯ }.setIfInBounds i a).setIfInBounds i b =
    { toArray := v, size_toArray := ⋯ }.setIfInBounds i b

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
    pmap f l H = l.attach.map fun x => f x.1 (H _ x.2)

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ l → p a
⊢ pmap f l H = map (fun x => f x.val ⋯) l.attach

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ pmap f { toList := toList✝ } H = map (fun x => f x.val ⋯) { toList := toList✝ }.attach

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ pmap f { toList := toList✝ } H = map (fun x => f x.val ⋯) { toList := toList✝ }.attach

Tactic:
simp [List.pmap_eq_map_attach]

Result:
no goals