harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Opposites.lean
theorem support_opRingEquiv (p : R[X]ᵐᵒᵖ) : (opRingEquiv R p).support = (unop p).support

Proof state:
case h.ofFinsupp
R : Type u_1
inst✝ : Semiring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ((opRingEquiv R) (op { toFinsupp := toFinsupp✝ })).support = (unop (op { toFinsupp := toFinsupp✝ })).support

Tactic:
exact Finsupp.support_mapRange_of_injective (map_zero _) _ op_injective

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ((opRingEquiv R) (op p)).support = (unop (op p)).support

Tactic:
cases p

Result:
case h.ofFinsupp
R : Type u_1
inst✝ : Semiring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ((opRingEquiv R) (op { toFinsupp := toFinsupp✝ })).support = (unop (op { toFinsupp := toFinsupp✝ })).support

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ ((opRingEquiv R) p).support = (unop p).support

Tactic:
induction' p with p

Result:
case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ((opRingEquiv R) (op p)).support = (unop (op p)).support
-- Mathlib/Algebra/BigOperators/Expect.lean
/-- Expectation over a product set equals the expectation of the fiberwise expectations.

For rewriting in the reverse direction, use `Finset.expect_product'`. -/
lemma expect_product (s : Finset ι) (t : Finset κ) (f : ι × κ → M) :
    𝔼 x ∈ s ×ˢ t, f x = 𝔼 i ∈ s, 𝔼 j ∈ t, f (i, j)

Proof state:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
t : Finset κ
f : ι × κ → M
⊢ 𝔼 x ∈ s ×ˢ t, f x = 𝔼 i ∈ s, 𝔼 j ∈ t, f (i, j)

Tactic:
simp only [expect, card_product, sum_product, smul_sum, mul_inv, mul_smul, Nat.cast_mul]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem mul_right' (a : ℤ) {b₁ b₂ : ℕ} (hb₁ : b₁ ≠ 0) (hb₂ : b₂ ≠ 0) :
    J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂)

Proof state:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp => legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp => legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)

Tactic:
case _ => rfl

Result:
no goals

Proof state:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂)

Tactic:
rw [jacobiSym, ((perm_primeFactorsList_mul hb₁ hb₂).pmap _).prod_eq, List.pmap_append,
  List.prod_append]

Result:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp => legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp => legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)

case h
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a

case h
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a

Proof state:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp => legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp => legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)

Tactic:
rfl

Result:
no goals

Proof state:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a

Tactic:
exact fun p hp =>
(List.mem_append.mp hp).elim prime_of_mem_primeFactorsList prime_of_mem_primeFactorsList

Result:
no goals

Proof state:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp => legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp => legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)

case h
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a

case h
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a

Tactic:
case h => exact fun p hp =>
  (List.mem_append.mp hp).elim prime_of_mem_primeFactorsList prime_of_mem_primeFactorsList

Result:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp => legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp => legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)
-- Mathlib/CategoryTheory/DiscreteCategory.lean
theorem functor_map_id (F : Discrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) :
    F.map f = 𝟙 (F.obj j)

Proof state:
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map f = 𝟙 (F.obj j)

Tactic:
rw [h]

Result:
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map (𝟙 j) = 𝟙 (F.obj j)

Proof state:
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
⊢ F.map f = 𝟙 (F.obj j)

Tactic:
have h : f = 𝟙 j := by aesop_cat

Result:
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map f = 𝟙 (F.obj j)

Proof state:
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
⊢ f = 𝟙 j

Tactic:
aesop_cat

Result:
no goals

Proof state:
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map (𝟙 j) = 𝟙 (F.obj j)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_right_comm (a b c : α) : (a \ b) \ c = (a \ c) \ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ (a \ b) \ c = (a \ c) \ b

Tactic:
simp_rw [sdiff_sdiff, sup_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sshiftRight_zero {x : BitVec w} : x.sshiftRight 0 = x

Proof state:
w : Nat
x : BitVec w
⊢ x.sshiftRight 0 = x

Tactic:
ext i h

Result:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (x.sshiftRight 0).getLsbD i = x.getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (x.sshiftRight 0).getLsbD i = x.getLsbD i

Tactic:
simp [getLsbD_sshiftRight, h]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma Odd.sub_odd (hm : Odd m) (hn : Odd n) : Even (m - n) :=
  (le_total n m).elim (fun h ↦ by simp only [even_sub' h, *]) fun h ↦ by
    simp only [Nat.sub_eq_zero_iff_le.2 h, Even.zero]

Proof state:
m n : ℕ
hm : Odd m
hn : Odd n
h : m ≤ n
⊢ Even (m - n)

Tactic:
simp only [Nat.sub_eq_zero_iff_le.2 h, Even.zero]

Result:
no goals

Proof state:
m n : ℕ
hm : Odd m
hn : Odd n
h : n ≤ m
⊢ Even (m - n)

Tactic:
simp only [even_sub' h, *]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem reverse_prod_map_ι :
    ∀ l : List M, reverse (l.map <| ι Q).prod = (l.map <| ι Q).reverse.prod
  | [] => by simp
  | x::xs => by simp [reverse_prod_map_ι xs]

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : M
xs : List M
⊢ reverse (List.map (⇑(ι Q)) (x :: xs)).prod = (List.map (⇑(ι Q)) (x :: xs)).reverse.prod

Tactic:
simp [reverse_prod_map_ι xs]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ reverse (List.map ⇑(ι Q) []).prod = (List.map ⇑(ι Q) []).reverse.prod

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem truncate_const_continuous_family {a b : X} (γ : Path a b)
    (t : ℝ) : Continuous ↿(γ.truncate t)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
key : Continuous fun x => (t, x)
⊢ Continuous ↿(γ.truncate t)

Tactic:
exact γ.truncate_continuous_family.comp key

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
⊢ Continuous fun x => (t, x)

Tactic:
fun_prop

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
⊢ Continuous ↿(γ.truncate t)

Tactic:
have key : Continuous (fun x => (t, x) : ℝ × I → ℝ × ℝ × I) := by fun_prop

Result:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
key : Continuous fun x => (t, x)
⊢ Continuous ↿(γ.truncate t)
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_undef (h : ¬IntervalIntegrable f μ a b) : ∫ x in a..b, f x ∂μ = 0

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : ¬IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0

Tactic:
rw [intervalIntegrable_iff] at h

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : ¬IntegrableOn f (Ι a b) μ
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : ¬IntegrableOn f (Ι a b) μ
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0

Tactic:
rw [intervalIntegral_eq_integral_uIoc, integral_undef h, smul_zero]

Result:
no goals
-- Mathlib/Data/Finite/Prod.lean
theorem Finite.image2 (f : α → β → γ) (hs : s.Finite) (ht : t.Finite) :
    (image2 f s t).Finite

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
⊢ (image2 f s t).Finite

Tactic:
have := hs.to_subtype

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
this : Finite ↑s
⊢ (image2 f s t).Finite

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
this✝ : Finite ↑s
this : Finite ↑t
⊢ (image2 f s t).Finite

Tactic:
apply toFinite

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
this : Finite ↑s
⊢ (image2 f s t).Finite

Tactic:
have := ht.to_subtype

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
this✝ : Finite ↑s
this : Finite ↑t
⊢ (image2 f s t).Finite
-- Mathlib/Algebra/Algebra/Operations.lean
theorem mul_eq_span_mul_set (s t : Submodule R A) : s * t = span R ((s : Set A) * (t : Set A))

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s t : Submodule R A
⊢ map₂ (LinearMap.mul R A) s t = span R (↑s * ↑t)

Tactic:
exact map₂_eq_span_image2 _ s t

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s t : Submodule R A
⊢ s * t = span R (↑s * ↑t)

Tactic:
rw [mul_eq_map₂]

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s t : Submodule R A
⊢ map₂ (LinearMap.mul R A) s t = span R (↑s * ↑t)
-- Mathlib/Analysis/Calculus/Deriv/Shift.lean
/-- Translation in the domain does not change the derivative. -/
lemma deriv_comp_add_const : deriv (fun x ↦ f (x + a)) x = deriv f (x + a)

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
⊢ deriv (fun x => f (x + a)) x = deriv f (x + a)

Tactic:
simpa [add_comm] using deriv_comp_const_add f a x

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem smeval_one : (1 : R[T;T⁻¹]).smeval x = 1

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : MulActionWithZero R S
inst✝ : Monoid S
x : Sˣ
⊢ smeval 1 x = 1

Tactic:
rw [← T_zero, smeval_T_pow 0 x, zpow_zero, Units.val_eq_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.toLin_apply (M : Matrix m n R) (v : M₁) :
    Matrix.toLin v₁ v₂ M v = ∑ j, (M *ᵥ v₁.repr v) j • v₂ j :=
  show v₂.equivFun.symm (Matrix.toLin' M (v₁.repr v)) = _ by
    rw [Matrix.toLin'_apply, v₂.equivFun_symm_apply]

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
v : M₁
⊢ v₂.equivFun.symm ((toLin' M) ⇑(v₁.repr v)) = ∑ j : m, (M *ᵥ ⇑(v₁.repr v)) j • v₂ j

Tactic:
rw [Matrix.toLin'_apply, v₂.equivFun_symm_apply]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem hasBasis_nhds_prod (x y : α) :
    HasBasis (𝓝 (x, y)) (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s ×ˢ ball y s

Proof state:
α : Type ua
inst✝ : UniformSpace α
x y : α
⊢ ∀ {i j : Set (α × α)},
    i ∈ 𝓤 α ∧ SymmetricRel i →
      j ∈ 𝓤 α ∧ SymmetricRel j → ∃ k, (k ∈ 𝓤 α ∧ SymmetricRel k) ∧ ball x k ⊆ ball x i ∧ ball y k ⊆ ball y j

Tactic:
rintro U V ⟨U_in, U_symm⟩ ⟨V_in, V_symm⟩

Result:
case intro.intro
α : Type ua
inst✝ : UniformSpace α
x y : α
U V : Set (α × α)
U_in : U ∈ 𝓤 α
U_symm : SymmetricRel U
V_in : V ∈ 𝓤 α
V_symm : SymmetricRel V
⊢ ∃ k, (k ∈ 𝓤 α ∧ SymmetricRel k) ∧ ball x k ⊆ ball x U ∧ ball y k ⊆ ball y V

Proof state:
case intro.intro
α : Type ua
inst✝ : UniformSpace α
x y : α
U V : Set (α × α)
U_in : U ∈ 𝓤 α
U_symm : SymmetricRel U
V_in : V ∈ 𝓤 α
V_symm : SymmetricRel V
⊢ ∃ k, (k ∈ 𝓤 α ∧ SymmetricRel k) ∧ ball x k ⊆ ball x U ∧ ball y k ⊆ ball y V

Tactic:
exact
  ⟨U ∩ V, ⟨(𝓤 α).inter_sets U_in V_in, U_symm.inter V_symm⟩, ball_inter_left x U V,
    ball_inter_right y U V⟩

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
x y : α
⊢ (𝓝 (x, y)).HasBasis (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s ×ˢ ball y s

Tactic:
rw [nhds_prod_eq]

Result:
α : Type ua
inst✝ : UniformSpace α
x y : α
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s ×ˢ ball y s

Proof state:
α : Type ua
inst✝ : UniformSpace α
x y : α
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s ×ˢ ball y s

Tactic:
apply (hasBasis_nhds x).prod_same_index (hasBasis_nhds y)

Result:
α : Type ua
inst✝ : UniformSpace α
x y : α
⊢ ∀ {i j : Set (α × α)},
    i ∈ 𝓤 α ∧ SymmetricRel i →
      j ∈ 𝓤 α ∧ SymmetricRel j → ∃ k, (k ∈ 𝓤 α ∧ SymmetricRel k) ∧ ball x k ⊆ ball x i ∧ ball y k ⊆ ball y j
-- Mathlib/Order/BooleanAlgebra.lean
theorem eq_of_sdiff_eq_sdiff (hxz : x ≤ z) (hyz : y ≤ z) (h : z \ x = z \ y) : x = y

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

Tactic:
rw [← sdiff_sdiff_eq_self hxz, h, sdiff_sdiff_eq_self hyz]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Basic.lean
lemma lt_iff (I J : TwoSidedIdeal R) : I < J ↔ (I : Set R) ⊂ (J : Set R)

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I < J ↔ ↑I ⊂ ↑J

Tactic:
rw [lt_iff_le_and_ne, Set.ssubset_iff_subset_ne, le_iff]

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ ↑I ⊆ ↑J ∧ I ≠ J ↔ ↑I ⊆ ↑J ∧ ↑I ≠ ↑J

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ ↑I ⊆ ↑J ∧ I ≠ J ↔ ↑I ⊆ ↑J ∧ ↑I ≠ ↑J

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean
lemma unitization_norm_def (x : WithLp 1 (Unitization 𝕜 A)) :
    ‖x‖ = ‖(WithLp.equiv 1 _ x).fst‖ + ‖(WithLp.equiv 1 _ x).snd‖ := calc
  ‖x‖ = (‖(WithLp.equiv 1 _ x).fst‖ ^ (1 : ℝ≥0∞).toReal +
      ‖(WithLp.equiv 1 _ x).snd‖ ^ (1 : ℝ≥0∞).toReal) ^ (1 / (1 : ℝ≥0∞).toReal) :=
    WithLp.prod_norm_eq_add (by simp : 0 < (1 : ℝ≥0∞).toReal) _
  _   = ‖(WithLp.equiv 1 _ x).fst‖ + ‖(WithLp.equiv 1 _ x).snd‖

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NonUnitalNormedRing A
inst✝ : NormedSpace 𝕜 A
x : WithLp 1 (Unitization 𝕜 A)
⊢ 0 < ENNReal.toReal 1

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NonUnitalNormedRing A
inst✝ : NormedSpace 𝕜 A
x : WithLp 1 (Unitization 𝕜 A)
⊢ (‖((WithLp.equiv 1 (Unitization 𝕜 A)) x).fst‖ ^ ENNReal.toReal 1 +
        ‖((WithLp.equiv 1 (Unitization 𝕜 A)) x).snd‖ ^ ENNReal.toReal 1) ^
      (1 / ENNReal.toReal 1) =
    ‖((WithLp.equiv 1 (Unitization 𝕜 A)) x).fst‖ + ‖((WithLp.equiv 1 (Unitization 𝕜 A)) x).snd‖

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_id_eq_sSup [CompleteLattice α] (s : Finset α) : s.sup id = sSup s

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
s : Finset α
⊢ s.sup id = sSup ↑s

Tactic:
simp [sSup_eq_iSup, sup_eq_iSup]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
theorem natAbs_sub_pos_iff {i j : ℤ} : 0 < natAbs (i - j) ↔ i ≠ j

Proof state:
i j : ℤ
⊢ 0 < (i - j).natAbs ↔ i ≠ j

Tactic:
rw [natAbs_pos, ne_eq, sub_eq_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
theorem eLpNorm'_le_eLpNorm'_of_exponent_le {p q : ℝ} (hp0_lt : 0 < p)
    (hpq : p ≤ q) (μ : Measure α) [IsProbabilityMeasure μ] (hf : AEStronglyMeasurable f μ) :
    eLpNorm' f p μ ≤ eLpNorm' f q μ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
μ : Measure α
inst✝ : IsProbabilityMeasure μ
hf : AEStronglyMeasurable f μ
h_le_μ : eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ

Tactic:
rwa [measure_univ, ENNReal.one_rpow, mul_one] at h_le_μ

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
μ : Measure α
inst✝ : IsProbabilityMeasure μ
hf : AEStronglyMeasurable f μ
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ

Tactic:
have h_le_μ := eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ hp0_lt hpq hf

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
μ : Measure α
inst✝ : IsProbabilityMeasure μ
hf : AEStronglyMeasurable f μ
h_le_μ : eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem rightHom_comp_inr : (rightHom : N ⋊[φ] G →* G).comp inr = MonoidHom.id _

Proof state:
case h
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x✝ : G
⊢ (rightHom.comp inr) x✝ = (MonoidHom.id G) x✝

Tactic:
simp [rightHom]

Result:
no goals

Proof state:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
⊢ rightHom.comp inr = MonoidHom.id G

Tactic:
ext

Result:
case h
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x✝ : G
⊢ (rightHom.comp inr) x✝ = (MonoidHom.id G) x✝
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma inv_le_one_iff_one_le {a : Aˣ} (ha : 0 ≤ (a : A)) :
    (↑a⁻¹ : A) ≤ 1 ↔ 1 ≤ a

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : 0 ≤ ↑a
⊢ 0 ≤ ↑1

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : 0 ≤ ↑a
⊢ ↑a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
simpa using CStarAlgebra.inv_le_iff ha (b := 1) (by simp)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mem_zipIdx_iff_getElem? {x : α × Nat} {l : Vector α n} :
    x ∈ l.zipIdx ↔ l[x.2]? = some x.1

Proof state:
α : Type u_1
n : Nat
x : α × Nat
l : Vector α n
⊢ x ∈ l.zipIdx ↔ l[x.snd]? = some x.fst

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
x : α × Nat
l : Array α
⊢ x ∈ { toArray := l, size_toArray := ⋯ }.zipIdx ↔ { toArray := l, size_toArray := ⋯ }[x.snd]? = some x.fst

Proof state:
case mk
α : Type u_1
x : α × Nat
l : Array α
⊢ x ∈ { toArray := l, size_toArray := ⋯ }.zipIdx ↔ { toArray := l, size_toArray := ⋯ }[x.snd]? = some x.fst

Tactic:
simp [Array.mem_zipIdx_iff_getElem?]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem exists_eq_right : (∃ a, p a ∧ a = a') ↔ p a' :=
  (exists_congr <| by exact fun a => And.comm).trans exists_eq_left

Proof state:
α : Sort u_1
p : α → Prop
a' : α
⊢ ∀ (a : α), p a ∧ a = a' ↔ a = a' ∧ p a

Tactic:
exact fun a => And.comm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) :
    m.isEmpty = true ↔ ∀ a, m.contains a = false

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ m.isEmpty = true ↔ ∀ (a : α), m.contains a = false

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

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
theorem geometric_hahn_banach_closed_compact (hs₁ : Convex ℝ s) (hs₂ : IsClosed s)
    (ht₁ : Convex ℝ t) (ht₂ : IsCompact t) (disj : Disjoint s t) :
    ∃ (f : E →L[ℝ] ℝ) (u v : ℝ), (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b :=
  let ⟨f, s, t, hs, st, ht⟩ := geometric_hahn_banach_compact_closed ht₁ ht₂ hs₁ hs₂ disj.symm
  ⟨-f, -t, -s, by simpa using ht, by simpa using st, by simpa using hs⟩

Proof state:
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s✝ t✝ : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
ht₁ : Convex ℝ t✝
ht₂ : IsCompact t✝
disj : Disjoint s✝ t✝
f : E →L[ℝ] ℝ
s t : ℝ
hs : ∀ a ∈ t✝, f a < s
st : s < t
ht : ∀ b ∈ s✝, t < f b
⊢ ∀ b ∈ t✝, -s < (-f) b

Tactic:
simpa using hs

Result:
no goals

Proof state:
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s✝ t✝ : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
ht₁ : Convex ℝ t✝
ht₂ : IsCompact t✝
disj : Disjoint s✝ t✝
f : E →L[ℝ] ℝ
s t : ℝ
hs : ∀ a ∈ t✝, f a < s
st : s < t
ht : ∀ b ∈ s✝, t < f b
⊢ ∀ a ∈ s✝, (-f) a < -t

Tactic:
simpa using ht

Result:
no goals

Proof state:
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s✝ t✝ : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
ht₁ : Convex ℝ t✝
ht₂ : IsCompact t✝
disj : Disjoint s✝ t✝
f : E →L[ℝ] ℝ
s t : ℝ
hs : ∀ a ∈ t✝, f a < s
st : s < t
ht : ∀ b ∈ s✝, t < f b
⊢ -t < -s

Tactic:
simpa using st

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_inf_self_left (a b : α) : a \ (a ⊓ b) = a \ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (a ⊓ b) = a \ b

Tactic:
rw [sdiff_inf, sdiff_self, bot_sup_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_if {f : α → β} [Decidable c] :
     (if c then some a else none).map f = if c then some (f a) else none

Proof state:
α : Type u_1
β : Type u_2
c : Prop
a : α
f : α → β
inst✝ : Decidable c
⊢ Option.map f (if c then some a else none) = if c then some (f a) else none

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rdropWhile_nil : rdropWhile p ([] : List α) = []

Proof state:
α : Type u_1
p : α → Bool
⊢ rdropWhile p [] = []

Tactic:
simp [rdropWhile, dropWhile]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma baseChange_Ψ₂Sq : (W.baseChange B).Ψ₂Sq = (W.baseChange A).Ψ₂Sq.map f

Proof state:
R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W.baseChange B).Ψ₂Sq = Polynomial.map (↑f) (W.baseChange A).Ψ₂Sq

Tactic:
rw [← map_Ψ₂Sq, map_baseChange]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
lemma generateFrom_memPartition_le_range (t : ℕ → Set α) (n : ℕ) :
    generateFrom (memPartition t n) ≤ generateFrom (range t)

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ generateFrom (memPartition t n) ≤ generateFrom (range t)

Tactic:
conv_rhs => rw [← generateFrom_iUnion_memPartition t]

Result:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ generateFrom (memPartition t n) ≤ generateFrom (⋃ n, memPartition t n)

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ generateFrom (memPartition t n) ≤ generateFrom (⋃ n, memPartition t n)

Tactic:
exact generateFrom_mono (subset_iUnion _ _)

Result:
no goals