harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MonoidAlgebra/Grading.lean
theorem mem_grade_iff (m : M) (a : R[M]) : a ∈ grade R m ↔ a.support ⊆ {m}

Proof state:
M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ a ∈ grade R m ↔ a.support ⊆ {m}

Tactic:
rw [← Finset.coe_subset, Finset.coe_singleton]

Result:
M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ a ∈ grade R m ↔ ↑a.support ⊆ {m}

Proof state:
M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ a ∈ grade R m ↔ ↑a.support ⊆ {m}

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem rev_lt_rev {i j : Fin n} : rev i < rev j ↔ j < i

Proof state:
n : Nat
i j : Fin n
⊢ i.rev < j.rev ↔ j < i

Tactic:
rw [← Fin.not_le, ← Fin.not_le, rev_le_rev]

Result:
no goals
-- Mathlib/Deprecated/Cardinal/Finite.lean
theorem _root_.Cardinal.toPartENat_lt_natCast_iff {n : ℕ} {c : Cardinal} :
    toPartENat c < ↑n ↔ c < ↑n

Proof state:
n : ℕ
c : Cardinal.{u_1}
⊢ toPartENat c < ↑n ↔ c < ↑n

Tactic:
simp only [← not_le, Cardinal.natCast_le_toPartENat_iff]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem cgf_zero_measure : cgf X (0 : Measure Ω) = 0

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
x✝ : ℝ
⊢ cgf X 0 x✝ = 0 x✝

Tactic:
simp [cgf]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
⊢ cgf X 0 = 0

Tactic:
ext

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
x✝ : ℝ
⊢ cgf X 0 x✝ = 0 x✝
-- Mathlib/.lake/packages/batteries/Batteries/Data/ByteArray.lean
theorem size_append (a b : ByteArray) : (a ++ b).size = a.size + b.size

Proof state:
a b : ByteArray
⊢ (a ++ b).size = a.size + b.size

Tactic:
simp only [size, append_eq, data_append]

Result:
a b : ByteArray
⊢ (a.data ++ b.data).size = a.data.size + b.data.size

Proof state:
a b : ByteArray
⊢ (a.data ++ b.data).size = a.data.size + b.data.size

Tactic:
exact Array.size_append ..

Result:
no goals
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem mem_trichotomous (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ∈ y ∨ x = y ∨ y ∈ x

Proof state:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∈ y ∨ y ⊆ x

Tactic:
exact mem_or_subset hx hy

Result:
no goals

Proof state:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∈ y ∨ x = y ∨ y ∈ x

Tactic:
rw [eq_comm, ← subset_iff_eq_or_mem hy hx]

Result:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∈ y ∨ y ⊆ x
-- Mathlib/Logic/Function/Conjugate.lean
theorem comp_right (h : Semiconj f ga gb) (h' : Semiconj f ga' gb') :
    Semiconj f (ga ∘ ga') (gb ∘ gb') := fun x ↦ by
  simp only [comp_apply, h.eq, h'.eq]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
h' : Semiconj f ga' gb'
x : α
⊢ f ((ga ∘ ga') x) = (gb ∘ gb') (f x)

Tactic:
simp only [comp_apply, h.eq, h'.eq]

Result:
no goals
-- Mathlib/Algebra/Order/Kleene.lean
theorem kstar_eq_self : a∗ = a ↔ a * a = a ∧ 1 ≤ a :=
  ⟨fun h ↦ ⟨by rw [← h, kstar_mul_kstar], one_le_kstar.trans_eq h⟩,
    fun h ↦ (kstar_le_of_mul_le_left h.2 h.1.le).antisymm le_kstar⟩

Proof state:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : a∗ = a
⊢ a * a = a

Tactic:
rw [← h, kstar_mul_kstar]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Int.lean
lemma _root_.Nat.cast_natAbs {α : Type*} [AddGroupWithOne α] (n : ℤ) : (n.natAbs : α) = |n|

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑n.natAbs = ↑|n|

Tactic:
rw [← natCast_natAbs, Int.cast_natCast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem then_eq_eq {o₁ o₂ : Ordering} : o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq

Proof state:
o₁ o₂ : Ordering
⊢ o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq

Tactic:
cases o₁ <;> simp [«then»]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@[reassoc]
lemma L₀X₂ToP_comp_φ₁ : S.L₀X₂ToP ≫ S.φ₁ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₀X₂ToP ≫ S.φ₁ = 0

Tactic:
simp only [← cancel_mono S.L₂.f, L₀X₂ToP, assoc, φ₂, φ₁_L₂_f,
  pullback.lift_fst_assoc, w₀₂_τ₂, zero_comp]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem disjoint_left : Disjoint l₁ l₂ ↔ ∀ ⦃a⦄, a ∈ l₁ → a ∉ l₂

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁.Disjoint l₂ ↔ ∀ ⦃a : α✝⦄, a ∈ l₁ → ¬a ∈ l₂

Tactic:
simp [Disjoint]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/MvPolynomial.lean
theorem transcendental_X (i : σ) : Transcendental R (X i : MvPolynomial σ R)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
⊢ Transcendental R (X i)

Tactic:
simpa using transcendental_polynomial_aeval_X R i (Polynomial.transcendental_X R)

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
/-- The defining property of the weak operator topology: a function `f` tends to
`A : E →WOT[𝕜] F` along filter `l` iff `y (f a x)` tends to `y (A x)` along the same filter. -/
lemma tendsto_iff_forall_dual_apply_tendsto {α : Type*} {l : Filter α} {f : α → E →WOT[𝕜] F}
    {A : E →WOT[𝕜] F} :
    Tendsto f l (𝓝 A) ↔ ∀ x (y : F⋆), Tendsto (fun a => y (f a x)) l (𝓝 (y (A x)))

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
α : Type u_4
l : Filter α
f : α → E →WOT[𝕜] F
A : E →WOT[𝕜] F
⊢ Tendsto f l (𝓝 A) ↔ ∀ (x : E) (y : F →L[𝕜] 𝕜), Tendsto (fun a => y ((f a) x)) l (𝓝 (y (A x)))

Tactic:
simp [isInducing_inducingFn.tendsto_nhds_iff, tendsto_pi_nhds]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Module.finrank_pos_iff_exists_ne_zero [NoZeroSMulDivisors R M] :
    0 < finrank R M ↔ ∃ x : M, x ≠ 0

Proof state:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : NoZeroSMulDivisors R M
⊢ 0 < finrank R M ↔ ∃ x, x ≠ 0

Tactic:
rw [← @rank_pos_iff_exists_ne_zero R M, ← finrank_eq_rank]

Result:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : NoZeroSMulDivisors R M
⊢ 0 < finrank R M ↔ 0 < ↑(finrank R M)

Proof state:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : NoZeroSMulDivisors R M
⊢ 0 < finrank R M ↔ 0 < ↑(finrank R M)

Tactic:
norm_cast

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem pow (n : ℕ) (ha : a ≠ 0) : padicValNat p (a ^ n) = n * padicValNat p a

Proof state:
p a : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ha : a ≠ 0
⊢ padicValNat p (a ^ n) = n * padicValNat p a

Tactic:
simpa only [← @Nat.cast_inj ℤ, push_cast] using padicValRat.pow (Nat.cast_ne_zero.mpr ha)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.diag_map {X Y : C} (f : X ⟶ Y) [HasBinaryProduct X X] [HasBinaryProduct Y Y] :
    diag X ≫ prod.map f f = f ≫ diag Y

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasBinaryProduct X X
inst✝ : HasBinaryProduct Y Y
⊢ diag X ≫ map f f = f ≫ diag Y

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) :
    (cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I

Proof state:
n : ℕ
z : ℂ
⊢ (cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I

Tactic:
rw [← exp_mul_I, ← exp_mul_I, ← exp_nat_mul, mul_assoc]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem map_swap_divisorsAntidiagonal :
    (divisorsAntidiagonal n).map (Equiv.prodComm _ _).toEmbedding = divisorsAntidiagonal n

Proof state:
case h
n : ℕ
x✝ : ℕ × ℕ
⊢ x✝ ∈ Prod.swap ⁻¹' ↑n.divisorsAntidiagonal ↔ x✝ ∈ ↑n.divisorsAntidiagonal

Tactic:
exact swap_mem_divisorsAntidiagonal

Result:
no goals

Proof state:
n : ℕ
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal = n.divisorsAntidiagonal

Tactic:
rw [← coe_inj, coe_map, Equiv.coe_toEmbedding, Equiv.coe_prodComm,
  Set.image_swap_eq_preimage_swap]

Result:
n : ℕ
⊢ Prod.swap ⁻¹' ↑n.divisorsAntidiagonal = ↑n.divisorsAntidiagonal

Proof state:
n : ℕ
⊢ Prod.swap ⁻¹' ↑n.divisorsAntidiagonal = ↑n.divisorsAntidiagonal

Tactic:
ext

Result:
case h
n : ℕ
x✝ : ℕ × ℕ
⊢ x✝ ∈ Prod.swap ⁻¹' ↑n.divisorsAntidiagonal ↔ x✝ ∈ ↑n.divisorsAntidiagonal
-- Mathlib/MeasureTheory/Group/Integral.lean
theorem Integrable.comp_div_right {f : G → F} [IsMulRightInvariant μ] (hf : Integrable f μ)
    (g : G) : Integrable (fun t => f (t / g)) μ

Proof state:
G : Type u_4
F : Type u_6
inst✝⁴ : MeasurableSpace G
inst✝³ : NormedAddCommGroup F
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
f : G → F
inst✝ : μ.IsMulRightInvariant
hf : Integrable f μ
g : G
⊢ Integrable (fun t => f (t / g)) μ

Tactic:
simp_rw [div_eq_mul_inv]

Result:
G : Type u_4
F : Type u_6
inst✝⁴ : MeasurableSpace G
inst✝³ : NormedAddCommGroup F
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
f : G → F
inst✝ : μ.IsMulRightInvariant
hf : Integrable f μ
g : G
⊢ Integrable (fun t => f (t * g⁻¹)) μ

Proof state:
G : Type u_4
F : Type u_6
inst✝⁴ : MeasurableSpace G
inst✝³ : NormedAddCommGroup F
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
f : G → F
inst✝ : μ.IsMulRightInvariant
hf : Integrable f μ
g : G
⊢ Integrable (fun t => f (t * g⁻¹)) μ

Tactic:
exact hf.comp_mul_right g⁻¹

Result:
no goals
-- Mathlib/Data/Nat/Fib/Zeckendorf.lean
@[simp] lemma sum_zeckendorf_fib (n : ℕ) : (n.zeckendorf.map fib).sum = n

Proof state:
n : ℕ
⊢ (map fib n.zeckendorf).sum = n

Tactic:
induction n using zeckendorf.induct <;> simp_all [fib_greatestFib_le]

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C :
    interpolate s v r = ∑ i ∈ s, C (nodalWeight s v i) * (nodal s v / (X - C (v i))) * C (r i) :=
  sum_congr rfl fun j hj => by rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hj]

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
j : ι
hj : j ∈ s
⊢ C (r j) * Lagrange.basis s v j = C (nodalWeight s v j) * (nodal s v / (X - C (v j))) * C (r j)

Tactic:
rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hj]

Result:
no goals
-- Mathlib/Data/Multiset/Functor.lean
theorem id_traverse {α : Type*} (x : Multiset α) : traverse (pure : α → Id α) x = x

Proof state:
α : Type u_1
x : Multiset α
a✝ : List α
⊢ traverse pure ⟦a✝⟧ = ⟦a✝⟧

Tactic:
simp [traverse]

Result:
no goals

Proof state:
α : Type u_1
x : Multiset α
⊢ ∀ (a : List α), traverse pure ⟦a⟧ = ⟦a⟧

Tactic:
intro

Result:
α : Type u_1
x : Multiset α
a✝ : List α
⊢ traverse pure ⟦a✝⟧ = ⟦a✝⟧

Proof state:
α : Type u_1
x : Multiset α
⊢ traverse pure x = x

Tactic:
refine Quotient.inductionOn x ?_

Result:
α : Type u_1
x : Multiset α
⊢ ∀ (a : List α), traverse pure ⟦a⟧ = ⟦a⟧
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem mem_ball' : y ∈ ball x ε ↔ dist x y < ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ y ∈ ball x ε ↔ dist x y < ε

Tactic:
rw [dist_comm, mem_ball]

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
lemma imaginaryPart_surjective : Function.Surjective (imaginaryPart (A := A)) :=
  fun x ↦
    ⟨I • (x : A), Subtype.ext <| by simp only [imaginaryPart_I_smul, x.property.coe_realPart]⟩

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : ↥(selfAdjoint A)
⊢ ↑(ℑ (I • ↑x)) = ↑x

Tactic:
simp only [imaginaryPart_I_smul, x.property.coe_realPart]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
lemma inf_sdiff_left_comm (a b c : α) : a ⊓ (b \ c) = b ⊓ (a \ c)

Proof state:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = b ⊓ a \ c

Tactic:
simp_rw [← inf_sdiff_assoc, inf_comm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem leadingCoeff_X : leadingCoeff (X : R[X]) = 1

Proof state:
R : Type u
inst✝ : Semiring R
⊢ X.leadingCoeff = 1

Tactic:
simpa only [pow_one] using @leadingCoeff_X_pow R _ 1

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem topologicalGroup_inf {t₁ t₂ : TopologicalSpace G} (h₁ : @IsTopologicalGroup G t₁ _)
    (h₂ : @IsTopologicalGroup G t₂ _) : @IsTopologicalGroup G (t₁ ⊓ t₂) _

Proof state:
G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
b : Bool
⊢ IsTopologicalGroup G

Tactic:
cases b <;> assumption

Result:
no goals

Proof state:
G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
refine topologicalGroup_iInf fun b => ?_

Result:
G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
b : Bool
⊢ IsTopologicalGroup G
-- Mathlib/Data/Complex/Norm.lean
theorem dist_of_im_eq {z w : ℂ} (h : z.im = w.im) : dist z w = dist z.re w.re

Proof state:
z w : ℂ
h : z.im = w.im
⊢ dist z w = dist z.re w.re

Tactic:
rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs, Real.dist_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exponential.lean
theorem hasStrictDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕂)
    (htx : t • x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasStrictDerivAt (fun u : 𝕂 => exp 𝕂 (u • x)) (exp 𝕂 (t • x) * x) t

Proof state:
𝕂 : Type u_1
𝔸 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : CharZero 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕂
htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ HasStrictDerivAt (fun u => exp 𝕂 (u • x)) (exp 𝕂 (t • x) * x) t

Tactic:
simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 x t htx).hasStrictDerivAt

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem intCast_add (a b : Int) :
    ((a + b : Int) : Rat) = (a : Rat) + (b : Rat)

Proof state:
a b : Int
⊢ ↑(a + b) = ↑a + ↑b

Tactic:
rw [add_def]

Result:
a b : Int
⊢ ↑(a + b) = normalize ((↑a).num * ↑(↑b).den + (↑b).num * ↑(↑a).den) ((↑a).den * (↑b).den) ⋯

Proof state:
a b : Int
⊢ ↑(a + b) = normalize ((↑a).num * ↑(↑b).den + (↑b).num * ↑(↑a).den) ((↑a).den * (↑b).den) ⋯

Tactic:
simp [normalize_eq]

Result:
no goals
-- Mathlib/ModelTheory/LanguageMap.lean
theorem card_constantsOn : (constantsOn α).card = #α

Proof state:
α : Type u'
⊢ (constantsOn α).card = #α

Tactic:
simp [card_eq_card_functions_add_card_relations, sum_nat_eq_add_sum_succ]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_nat_eq_descFactorial (a b : ℕ) :
    (ascPochhammer ℕ b).eval a = (a + b - 1).descFactorial b

Proof state:
a b : ℕ
⊢ eval a (ascPochhammer ℕ b) = (a + b - 1).descFactorial b

Tactic:
rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial']

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem mem_ball_symmetry {V : Set (β × β)} (hV : SymmetricRel V) {x y} :
    x ∈ ball y V ↔ y ∈ ball x V :=
  show (x, y) ∈ Prod.swap ⁻¹' V ↔ (x, y) ∈ V by
    unfold SymmetricRel at hV
    rw [hV]

Proof state:
β : Type ub
V : Set (β × β)
hV : Prod.swap ⁻¹' V = V
x y : β
⊢ (x, y) ∈ Prod.swap ⁻¹' V ↔ (x, y) ∈ V

Tactic:
rw [hV]

Result:
no goals

Proof state:
β : Type ub
V : Set (β × β)
hV : SymmetricRel V
x y : β
⊢ (x, y) ∈ Prod.swap ⁻¹' V ↔ (x, y) ∈ V

Tactic:
unfold SymmetricRel at hV

Result:
β : Type ub
V : Set (β × β)
hV : Prod.swap ⁻¹' V = V
x y : β
⊢ (x, y) ∈ Prod.swap ⁻¹' V ↔ (x, y) ∈ V
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem span_fourier_closure_eq_top : (span ℂ (range <| @fourier T)).topologicalClosure = ⊤

Proof state:
T : ℝ
hT : Fact (0 < T)
⊢ (span ℂ (range fourier)).topologicalClosure = ⊤

Tactic:
rw [← fourierSubalgebra_coe]

Result:
T : ℝ
hT : Fact (0 < T)
⊢ (Subalgebra.toSubmodule fourierSubalgebra.toSubalgebra).topologicalClosure = ⊤
-- Mathlib/RingTheory/OreLocalization/Basic.lean
theorem oreDiv_add_char' {r r' : X} (s s' : S) (rb : R) (sb : R)
    (h : sb * s = rb * s') (h' : sb * s ∈ S) :
    r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ ⟨sb * s, h'⟩

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r r' : X
s s' : ↥S
rb sb : R
h : sb * ↑s = rb * ↑s'
h' : sb * ↑s ∈ S
⊢ r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ ⟨sb * ↑s, h'⟩

Tactic:
with_unfolding_all exact add''_char r s r' s' rb sb h h'

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r r' : X
s s' : ↥S
rb sb : R
h : sb * ↑s = rb * ↑s'
h' : sb * ↑s ∈ S
⊢ r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ ⟨sb * ↑s, h'⟩

Tactic:
exact add''_char r s r' s' rb sb h h'

Result:
no goals
-- Mathlib/Order/Interval/Finset/Box.lean
private lemma Icc_neg_mono : Monotone fun n : ℕ ↦ Icc (-n : α) n

Proof state:
α : Type u_1
inst✝¹ : OrderedRing α
inst✝ : LocallyFiniteOrder α
m n : ℕ
hmn : m ≤ n
⊢ (fun n => Icc (-↑n) ↑n) m ≤ (fun n => Icc (-↑n) ↑n) n

Tactic:
apply Icc_subset_Icc <;> simpa using Nat.mono_cast hmn

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : OrderedRing α
inst✝ : LocallyFiniteOrder α
⊢ Monotone fun n => Icc (-↑n) ↑n

Tactic:
refine fun m n hmn ↦ by apply Icc_subset_Icc <;> simpa using Nat.mono_cast hmn

Result:
no goals
-- Mathlib/Algebra/Ring/Regular.lean
theorem isRightRegular_of_non_zero_divisor [NonUnitalNonAssocRing α] (k : α)
    (h : ∀ x : α, x * k = 0 → x = 0) : IsRightRegular k

Proof state:
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
x y : α
h' : x * k = y * k
⊢ (x - y) * k = 0

Tactic:
rw [sub_mul, sub_eq_zero, h']

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
⊢ IsRightRegular k

Tactic:
refine fun x y (h' : x * k = y * k) => sub_eq_zero.mp (h _ ?_)

Result:
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
x y : α
h' : x * k = y * k
⊢ (x - y) * k = 0
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem pow_mk (n : ℕ) : mk L ^ n = mk (List.flatten <| List.replicate n L) :=
  match n with
  | 0 => rfl
  | n + 1 => by rw [pow_succ', pow_mk, mul_mk, List.replicate_succ, List.flatten_cons]

Proof state:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
⊢ mk L ^ (n + 1) = mk (List.replicate (n + 1) L).flatten

Tactic:
rw [pow_succ', pow_mk, mul_mk, List.replicate_succ, List.flatten_cons]

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem mul_two (n : α) : n * 2 = n + n :=
  (congrArg₂ _ rfl one_add_one_eq_two.symm).trans <| (left_distrib n 1 1).trans (by rw [mul_one])

Proof state:
α : Type u
inst✝ : NonAssocSemiring α
n : α
⊢ n * 1 + n * 1 = n + n

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/Data/Finset/SDiff.lean
lemma cons_sdiff_cons (hab : a ≠ b) (ha hb) : s.cons a ha \ s.cons b hb = {a}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
hb : b ∉ s
⊢ cons a s ha \ cons b s hb = {a}

Tactic:
rw [cons_eq_insert, cons_eq_insert, insert_sdiff_insert' hab ha]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem locallyCompactSpace_iff (h : X ≃ₜ Y) :
    LocallyCompactSpace X ↔ LocallyCompactSpace Y

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ LocallyCompactSpace X ↔ LocallyCompactSpace Y

Tactic:
exact ⟨fun _ => h.symm.isOpenEmbedding.locallyCompactSpace,
  fun _ => h.isClosedEmbedding.locallyCompactSpace⟩

Result:
no goals
-- Mathlib/Data/Sym/Card.lean
theorem card_sym_eq_choose {α : Type*} [Fintype α] (k : ℕ) [Fintype (Sym α k)] :
    card (Sym α k) = (card α + k - 1).choose k

Proof state:
α : Type u_2
inst✝¹ : Fintype α
k : ℕ
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = (Fintype.card α + k - 1).choose k

Tactic:
rw [card_sym_eq_multichoose, Nat.multichoose_eq]

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem get_rowLens {μ : YoungDiagram} {i : Nat} {h : i < μ.rowLens.length} :
    μ.rowLens[i] = μ.rowLen i

Proof state:
μ : YoungDiagram
i : ℕ
h : i < μ.rowLens.length
⊢ μ.rowLens[i] = μ.rowLen i

Tactic:
simp only [rowLens, List.getElem_range, List.getElem_map]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem reflection_map_apply {E E' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E']
    [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (K : Submodule 𝕜 E)
    [HasOrthogonalProjection K] (x : E') :
    reflection (K.map (f.toLinearEquiv : E →ₗ[𝕜] E')) x = f (reflection K (f.symm x))

Proof state:
𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x : E'
⊢ (reflection (Submodule.map (↑f.toLinearEquiv) K)) x = f ((reflection K) (f.symm x))

Tactic:
simp [two_smul, reflection_apply, orthogonalProjection_map_apply f K x]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncGE.lean
lemma restrictionToTruncGE'_f_eq_iso_hom_iso_inv {i : ι} {i' : ι'} (hi' : e.f i = i')
    (hi : ¬ e.BoundaryGE i) :
    (K.restrictionToTruncGE' e).f i =
      (K.restrictionXIso e hi').hom ≫ (K.truncGE'XIso e hi' hi).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryGE i
⊢ (K.restrictionToTruncGE' e).f i = (K.restrictionXIso e hi').hom ≫ (K.truncGE'XIso e hi' hi).inv

Tactic:
apply restrictionToTruncGE'.f_eq_iso_hom_iso_inv

Result:
no goals
-- Mathlib/Order/Shrink.lean
@[simp]
lemma equivShrink_symm_bot [Bot α] : (equivShrink.{u} α).symm ⊥ = ⊥ :=
  (equivShrink.{u} α).injective (by simp)

Proof state:
α : Type v
inst✝¹ : Small.{u, v} α
inst✝ : Bot α
⊢ (equivShrink α) ((equivShrink α).symm ⊥) = (equivShrink α) ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/CharP/Two.lean
theorem list_sum_mul_self (l : List R) : l.sum * l.sum = (List.map (fun x => x * x) l).sum

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
l : List R
⊢ l.sum * l.sum = (List.map (fun x => x * x) l).sum

Tactic:
simp_rw [← pow_two, list_sum_sq]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem neg_lt_comm {a b : EReal} : -a < b ↔ -b < a

Proof state:
a b : EReal
⊢ -a < b ↔ -b < a

Tactic:
rw [← neg_lt_neg_iff, neg_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Cofork.coequalizer_ext (s : Cofork f g) {W : C} {k l : s.pt ⟶ W}
    (h : Cofork.π s ≫ k = Cofork.π s ≫ l) : ∀ j : WalkingParallelPair, s.ι.app j ≫ k = s.ι.app j ≫ l
  | zero => by simp only [s.app_zero_eq_comp_π_left, Category.assoc, h]
  | one => h

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Cofork f g
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
⊢ s.ι.app zero ≫ k = s.ι.app zero ≫ l

Tactic:
simp only [s.app_zero_eq_comp_π_left, Category.assoc, h]

Result:
no goals
-- Mathlib/Computability/NFA.lean
theorem stepSet_empty (a : α) : M.stepSet ∅ a = ∅

Proof state:
α : Type u
σ : Type v
M : NFA α σ
a : α
⊢ M.stepSet ∅ a = ∅

Tactic:
simp [stepSet]

Result:
no goals