harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_flatMap {f : α → List β} {b} {l : List α} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a

Proof state:
α : Type u_1
β : Type u_2
f : α → List β
b : β
l : List α
⊢ (∃ l_1, (∃ a, a ∈ l ∧ f a = l_1) ∧ b ∈ l_1) ↔ ∃ a, a ∈ l ∧ b ∈ f a

Tactic:
exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → List β
b : β
l : List α
⊢ b ∈ flatMap f l ↔ ∃ a, a ∈ l ∧ b ∈ f a

Tactic:
simp [flatMap_def, mem_flatten]

Result:
α : Type u_1
β : Type u_2
f : α → List β
b : β
l : List α
⊢ (∃ l_1, (∃ a, a ∈ l ∧ f a = l_1) ∧ b ∈ l_1) ↔ ∃ a, a ∈ l ∧ b ∈ f a
-- Mathlib/Logic/Function/FiberPartition.lean
lemma fiber_nonempty (f : Y → Z) (a : Fiber f) : Set.Nonempty a.val

Proof state:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
⊢ preimage f a ∈ ↑a

Tactic:
rw [mem_iff_eq_image, ← map_preimage_eq_image]

Result:
no goals

Proof state:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
⊢ (↑a).Nonempty

Tactic:
refine ⟨preimage f a, ?_⟩

Result:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
⊢ preimage f a ∈ ↑a
-- Mathlib/Probability/Kernel/RadonNikodym.lean
@[simp]
lemma singularPart_self (κ : Kernel α γ) [IsFiniteKernel κ] : κ.singularPart κ = 0

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ : Kernel α γ
inst✝ : IsFiniteKernel κ
⊢ κ.singularPart κ = 0

Tactic:
ext : 1

Result:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ : Kernel α γ
inst✝ : IsFiniteKernel κ
a✝ : α
⊢ (κ.singularPart κ) a✝ = 0 a✝

Proof state:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ : Kernel α γ
inst✝ : IsFiniteKernel κ
a✝ : α
⊢ (κ.singularPart κ) a✝ = 0 a✝

Tactic:
rw [zero_apply, singularPart_eq_zero_iff_absolutelyContinuous]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_eq_iff_eq_add {c : Nat} (h : b ≤ a) : a - b = c ↔ a = c + b :=
  ⟨fun | rfl => by rw [Nat.sub_add_cancel h], fun heq => by rw [heq, Nat.add_sub_cancel]⟩

Proof state:
b a c : Nat
h : b ≤ a
⊢ a = a - b + b

Tactic:
rw [Nat.sub_add_cancel h]

Result:
no goals

Proof state:
b a c : Nat
h : b ≤ a
heq : a = c + b
⊢ a - b = c

Tactic:
rw [heq, Nat.add_sub_cancel]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Properties.lean
theorem affine_isReduced_iff (R : CommRingCat) :
    IsReduced (Spec R) ↔ _root_.IsReduced R

Proof state:
R : CommRingCat
h : IsReduced (Spec R)
⊢ _root_.IsReduced ↑R

Tactic:
exact isReduced_of_injective (Scheme.ΓSpecIso R).inv.hom
  (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv.injective

Result:
no goals

Proof state:
R : CommRingCat
⊢ IsReduced (Spec R) ↔ _root_.IsReduced ↑R

Tactic:
refine ⟨?_, fun h => inferInstance⟩

Result:
R : CommRingCat
⊢ IsReduced (Spec R) → _root_.IsReduced ↑R

Proof state:
R : CommRingCat
⊢ IsReduced (Spec R) → _root_.IsReduced ↑R

Tactic:
intro h

Result:
R : CommRingCat
h : IsReduced (Spec R)
⊢ _root_.IsReduced ↑R
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthInf_zero : expGrowthInf 0 = ⊥

Proof state:
⊢ expGrowthInf 0 = ⊥

Tactic:
apply le_bot_iff.1

Result:
⊢ expGrowthInf 0 ≤ ⊥

Proof state:
⊢ expGrowthInf 0 ≤ ⊥

Tactic:
rw [← expGrowthSup_zero]

Result:
⊢ expGrowthInf 0 ≤ expGrowthSup 0

Proof state:
⊢ expGrowthInf 0 ≤ expGrowthSup 0

Tactic:
exact expGrowthInf_le_expGrowthSup

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem HasFPowerSeriesWithinOnBall.hasFDerivWithinAt [CompleteSpace F]
    (h : HasFPowerSeriesWithinOnBall f p s x r)
    {y : E} (hy : (‖y‖₊ : ℝ≥0∞) < r) (h'y : x + y ∈ insert x s) :
    HasFDerivWithinAt f (continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin y 1))
      (insert x s) (x + y)

Proof state:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (insert (x + y) s) (x + y)
⊢ s ∈ 𝓝[s] (x + y)

Tactic:
exact self_mem_nhdsWithin

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem cthickening_thickening_subset (hε : 0 ≤ ε) (δ : ℝ) (s : Set α) :
    cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s

Proof state:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
⊢ x ∈ cthickening ε (thickening δ s) → x ∈ cthickening (ε + δ) s

Tactic:
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ]

Result:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
⊢ infEdist x (thickening δ s) ≤ ENNReal.ofReal ε → infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
⊢ cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s

Tactic:
obtain hδ | hδ := le_total δ 0

Result:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : δ ≤ 0
⊢ cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s

case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
⊢ cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s

Proof state:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : δ ≤ 0
⊢ cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s

Tactic:
simp only [thickening_of_nonpos hδ, cthickening_empty, empty_subset]

Result:
no goals

Proof state:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
⊢ infEdist x (thickening δ s) ≤ ENNReal.ofReal ε → infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
exact fun hx => infEdist_le_infEdist_thickening_add.trans (add_le_add_right hx _)

Result:
no goals

Proof state:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
⊢ cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s

Tactic:
intro x

Result:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
⊢ x ∈ cthickening ε (thickening δ s) → x ∈ cthickening (ε + δ) s
-- Mathlib/RingTheory/Smooth/Locus.lean
lemma smoothLocus_eq_univ_iff [FinitePresentation R A] :
    smoothLocus R A = Set.univ ↔ Algebra.FormallySmooth R A

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
⊢ Submonoid.powers 1 ≤ IsUnit.submonoid A

Tactic:
simp

Result:
no goals

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
⊢ smoothLocus R A = Set.univ ↔ FormallySmooth R A

Tactic:
have := IsLocalization.atUnits A (.powers 1) (S := Localization.Away (1 : A)) (by simp)

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
this : A ≃ₐ[A] Localization.Away 1
⊢ smoothLocus R A = Set.univ ↔ FormallySmooth R A

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
this : A ≃ₐ[A] Localization.Away 1
⊢ smoothLocus R A = Set.univ ↔ ↑(PrimeSpectrum.basicOpen 1) ⊆ smoothLocus R A

Tactic:
simp

Result:
no goals

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
this : A ≃ₐ[A] Localization.Away 1
⊢ smoothLocus R A = Set.univ ↔ FormallySmooth R A

Tactic:
rw [Algebra.FormallySmooth.iff_of_equiv (this.restrictScalars R),
  ← basicOpen_subset_smoothLocus_iff]

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
this : A ≃ₐ[A] Localization.Away 1
⊢ smoothLocus R A = Set.univ ↔ ↑(PrimeSpectrum.basicOpen 1) ⊆ smoothLocus R A
-- Mathlib/Algebra/Algebra/Operations.lean
theorem mem_mul_span_singleton {x y : A} : x ∈ P * span R {y} ↔ ∃ z ∈ P, z * y = x

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
P : Submodule R A
x y : A
⊢ x ∈ map ((LinearMap.mul R A).flip y) P ↔ ∃ z ∈ P, Mul.mul z y = x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem IsSumSq.mul_self [AddZeroClass R] [Mul R] (a : R) : IsSumSq (a * a)

Proof state:
R : Type u_1
inst✝¹ : AddZeroClass R
inst✝ : Mul R
a : R
⊢ IsSumSq (a * a)

Tactic:
simpa using sq_add a zero

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma mk_snd (s : yoneda.obj X ⟶ A) (x : F.obj (op (CostructuredArrow.mk s))) :
    (mk s x).snd = F.map (eqToHom <| by rw [YonedaCollection.mk_fst]) x :=
  rfl

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : yoneda.obj X ⟶ A
x : F.obj (op (CostructuredArrow.mk s))
⊢ op (CostructuredArrow.mk s) = op (CostructuredArrow.mk (mk s x).fst)

Tactic:
rw [YonedaCollection.mk_fst]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
lemma cauchy_iInf_uniformSpace {ι : Sort*} [Nonempty ι] {u : ι → UniformSpace β}
    {l : Filter β} :
    Cauchy (uniformSpace := ⨅ i, u i) l ↔ ∀ i, Cauchy (uniformSpace := u i) l

Proof state:
β : Type v
ι : Sort u_1
inst✝ : Nonempty ι
u : ι → UniformSpace β
l : Filter β
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy l

Tactic:
unfold Cauchy

Result:
β : Type v
ι : Sort u_1
inst✝ : Nonempty ι
u : ι → UniformSpace β
l : Filter β
⊢ l.NeBot ∧ l ×ˢ l ≤ 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β

Proof state:
β : Type v
ι : Sort u_1
inst✝ : Nonempty ι
u : ι → UniformSpace β
l : Filter β
⊢ l.NeBot ∧ l ×ˢ l ≤ 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β

Tactic:
rw [iInf_uniformity, le_iInf_iff, forall_and, forall_const]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Module.lean
theorem ContinuousLinearEquiv.hasSum' {f : ι → M} (e : M ≃SL[σ] M₂) {x : M} :
    HasSum (fun b : ι ↦ e (f b)) (e x) ↔ HasSum f x

Proof state:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
f : ι → M
e : M ≃SL[σ] M₂
x : M
⊢ HasSum (fun b => e (f b)) (e x) ↔ HasSum f x

Tactic:
rw [e.hasSum, ContinuousLinearEquiv.symm_apply_apply]

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem algebraMap_finiteType_iff_algebra_finiteType {R A : Type*} [CommRing R] [CommRing A]
    [Algebra R A] : (algebraMap R A).FiniteType ↔ Algebra.FiniteType R A

Proof state:
case h.e'_5.h
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Algebra.FiniteType R A
⊢ ∀ (r : R), (algebraMap R A) r = (algebraMap R A) r

Tactic:
exact congrFun rfl

Result:
no goals

Proof state:
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Algebra.FiniteType R A
⊢ Algebra.FiniteType R A

Tactic:
convert h

Result:
case h.e'_5
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Algebra.FiniteType R A
⊢ (algebraMap R A).toAlgebra = inst✝

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (algebraMap R A).FiniteType ↔ Algebra.FiniteType R A

Tactic:
dsimp [RingHom.FiniteType]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Algebra.FiniteType R A ↔ Algebra.FiniteType R A

Proof state:
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Algebra.FiniteType R A → Algebra.FiniteType R A

Tactic:
intro h

Result:
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Algebra.FiniteType R A
⊢ Algebra.FiniteType R A

Proof state:
case h.e'_5
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Algebra.FiniteType R A
⊢ (algebraMap R A).toAlgebra = inst✝

Tactic:
apply Algebra.algebra_ext

Result:
case h.e'_5.h
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Algebra.FiniteType R A
⊢ ∀ (r : R), (algebraMap R A) r = (algebraMap R A) r

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Algebra.FiniteType R A ↔ Algebra.FiniteType R A

Tactic:
constructor <;> (intro h; convert h; apply Algebra.algebra_ext; exact congrFun rfl)

Result:
no goals
-- Mathlib/Analysis/RCLike/Lemmas.lean
lemma RCLike.rank_le_two : Module.rank ℝ K ≤ 2 :=
  calc
    _ = Module.rank ℝ ↥(Submodule.span ℝ ({1, I} : Set K))

Proof state:
K : Type u_1
inst✝ : RCLike K
⊢ Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ ↑(#{1, I})

Tactic:
have := rank_span_finset_le (R := ℝ) (M := K) {1, I}

Result:
K : Type u_1
inst✝ : RCLike K
this : Module.rank ℝ ↥(Submodule.span ℝ ↑{1, I}) ≤ ↑(#{1, I})
⊢ Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ ↑(#{1, I})

Proof state:
K : Type u_1
inst✝ : RCLike K
⊢ Module.rank ℝ K = Module.rank ℝ ↥⊤

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
this : Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ ↑(#{1, I})
⊢ Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ ↑(#{1, I})

Tactic:
simpa [span_one_I] using this

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
this : Module.rank ℝ ↥(Submodule.span ℝ ↑{1, I}) ≤ ↑(#{1, I})
⊢ Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ ↑(#{1, I})

Tactic:
rw [Finset.coe_pair] at this

Result:
K : Type u_1
inst✝ : RCLike K
this : Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ ↑(#{1, I})
⊢ Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ ↑(#{1, I})

Proof state:
K : Type u_1
inst✝ : RCLike K
⊢ Module.rank ℝ K = Module.rank ℝ ↥(Submodule.span ℝ {1, I})

Tactic:
rw [span_one_I]

Result:
K : Type u_1
inst✝ : RCLike K
⊢ Module.rank ℝ K = Module.rank ℝ ↥⊤
-- Mathlib/Order/SuccPred/Basic.lean
theorem Icc_succ_right (h : a ≤ succ b) : Icc a (succ b) = insert (succ b) (Icc a b)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
⊢ Icc a (succ b) = insert (succ b) (Icc a b)

Tactic:
simp_rw [← Ici_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ici.2 h)]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem HasBasis.lift' {ι} {p : ι → Prop} {s} (hf : f.HasBasis p s) (hh : Monotone h) :
    (f.lift' h).HasBasis p (h ∘ s) :=
  ⟨fun t => (hf.mem_lift_iff (fun i => hasBasis_principal (h (s i)))
    (monotone_principal.comp hh)).trans <| by simp only [exists_const, true_and, comp]⟩

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
ι : Sort u_5
p : ι → Prop
s : ι → Set α
hf : f.HasBasis p s
hh : Monotone h
t : Set β
⊢ (∃ i, p i ∧ ∃ x, True ∧ h (s i) ⊆ t) ↔ ∃ i, p i ∧ (h ∘ s) i ⊆ t

Tactic:
simp only [exists_const, true_and, comp]

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive (attr := simp)]
lemma stabilizer_finset_univ [Fintype α] : stabilizer G (Finset.univ : Finset α) = ⊤

Proof state:
G : Type u_1
α : Type u_3
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ stabilizer G Finset.univ = ⊤

Tactic:
ext

Result:
case h
G : Type u_1
α : Type u_3
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : G
⊢ x✝ ∈ stabilizer G Finset.univ ↔ x✝ ∈ ⊤

Proof state:
case h
G : Type u_1
α : Type u_3
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : G
⊢ x✝ ∈ stabilizer G Finset.univ ↔ x✝ ∈ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma toHom_comp {ι₁ M₁ N₁ ι₂ M₂ N₂ : Type*} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁]
    [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
    {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂}
    (g : RootPairing.Equiv P₁ P₂) (f : RootPairing.Equiv P P₁) :
    (Equiv.comp g f).toHom = Hom.comp g.toHom f.toHom

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ ↑(g.comp f) = (↑g).comp ↑f

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Final.lean
theorem final_of_adjunction {L : C ⥤ D} {R : D ⥤ C} (adj : L ⊣ R) : Final R :=
  { out := fun c =>
      let u : StructuredArrow c R := StructuredArrow.mk (adj.unit.app c)
      @zigzag_isConnected _ _ ⟨u⟩ fun f g =>
        Relation.ReflTransGen.trans
          (Relation.ReflTransGen.single
            (show Zag f u from
              Or.inr ⟨StructuredArrow.homMk ((adj.homEquiv c f.right).symm f.hom) (by simp [u])⟩))
          (Relation.ReflTransGen.single
            (show Zag u g from
              Or.inl ⟨StructuredArrow.homMk ((adj.homEquiv c g.right).symm g.hom) (by simp [u])⟩)) }

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
c : C
u : StructuredArrow c R := StructuredArrow.mk (adj.unit.app c)
f g : StructuredArrow c R
⊢ u.hom ≫ R.map ((adj.homEquiv c f.right).symm f.hom) = f.hom

Tactic:
simp [u]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
c : C
u : StructuredArrow c R := StructuredArrow.mk (adj.unit.app c)
f g : StructuredArrow c R
⊢ u.hom ≫ R.map ((adj.homEquiv c g.right).symm g.hom) = g.hom

Tactic:
simp [u]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_neg (f : α →₁[μ] E) : integral (-f) = -integral f

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integral (-f) = -integral f

Tactic:
simp only [integral]

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integralCLM (-f) = -integralCLM f

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integralCLM (-f) = -integralCLM f

Tactic:
exact map_neg integralCLM f

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem intValuation_ne_zero (x : R) (hx : x ≠ 0) : v.intValuationDef x ≠ 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors))) ≠ 0

Tactic:
exact WithZero.coe_ne_zero

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ v.intValuationDef x ≠ 0

Tactic:
rw [intValuationDef, if_neg hx]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors))) ≠ 0
-- Mathlib/RingTheory/HahnSeries/HEval.lean
theorem heval_unit (u : (PowerSeries R)ˣ) : IsUnit (heval hx u)

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
u : R⟦X⟧ˣ
⊢ ∃ b, (heval hx) ↑u * b = 1

Tactic:
use heval hx u.inv

Result:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
u : R⟦X⟧ˣ
⊢ (heval hx) ↑u * (heval hx) u.inv = 1

Proof state:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
u : R⟦X⟧ˣ
⊢ (heval hx) ↑u * (heval hx) u.inv = 1

Tactic:
rw [← heval_mul, Units.val_inv, map_one]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
u : R⟦X⟧ˣ
⊢ IsUnit ((heval hx) ↑u)

Tactic:
refine isUnit_iff_exists_inv.mpr ?_

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
u : R⟦X⟧ˣ
⊢ ∃ b, (heval hx) ↑u * b = 1
-- Mathlib/Order/Interval/Set/OrderEmbedding.lean
theorem preimage_Icc : e ⁻¹' Icc (e x) (e y) = Icc x y

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Icc (e x) (e y) ↔ x✝ ∈ Icc x y

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' Icc (e x) (e y) = Icc x y

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Icc (e x) (e y) ↔ x✝ ∈ Icc x y
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma powerset_sups_powerset_self (s : Finset α) :
    s.powerset ⊻ s.powerset = s.powerset

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ s.powerset ⊻ s.powerset = s.powerset

Tactic:
simp [← powerset_union]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Lemmas.lean
theorem testBit_ofBits_ge (f : Fin n → Bool) (i : Nat) (h : n ≤ i) :
    (ofBits f).testBit i = false

Proof state:
case lt
n : Nat
f : Fin n → Bool
i : Nat
h : n ≤ i
⊢ ofBits f < 2 ^ i

Tactic:
apply Nat.lt_of_lt_of_le

Result:
case lt.a
n : Nat
f : Fin n → Bool
i : Nat
h : n ≤ i
⊢ ofBits f < ?lt.m

case lt.a
n : Nat
f : Fin n → Bool
i : Nat
h : n ≤ i
⊢ ?lt.m ≤ 2 ^ i

case lt.m
n : Nat
f : Fin n → Bool
i : Nat
h : n ≤ i
⊢ Nat

Proof state:
case lt.a
n : Nat
f : Fin n → Bool
i : Nat
h : n ≤ i
⊢ ofBits f < ?lt.m

Tactic:
exact ofBits_lt_two_pow f

Result:
no goals

Proof state:
n : Nat
f : Fin n → Bool
i : Nat
h : n ≤ i
⊢ (ofBits f).testBit i = false

Tactic:
apply testBit_lt_two_pow

Result:
case lt
n : Nat
f : Fin n → Bool
i : Nat
h : n ≤ i
⊢ ofBits f < 2 ^ i

Proof state:
case lt.a
n : Nat
f : Fin n → Bool
i : Nat
h : n ≤ i
⊢ 2 ^ n ≤ 2 ^ i

Tactic:
exact pow_le_pow_of_le_right Nat.zero_lt_two h

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem injective_iff {α : Sort*} {f : Bool → α} : Function.Injective f ↔ f false ≠ f true :=
  ⟨fun Hinj Heq ↦ false_ne_true (Hinj Heq), fun H x y hxy ↦ by
    cases x <;> cases y
    · rfl
    · exact (H hxy).elim
    · exact (H hxy.symm).elim
    · rfl⟩

Proof state:
case true.true
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f true = f true
⊢ true = true

Tactic:
rfl

Result:
no goals

Proof state:
case false.true
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f false = f true
⊢ false = true

Tactic:
exact (H hxy).elim

Result:
no goals

Proof state:
case true.false
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f true = f false
⊢ true = false

Tactic:
exact (H hxy.symm).elim

Result:
no goals

Proof state:
case false.false
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f false = f false
⊢ false = false

Tactic:
rfl

Result:
no goals

Proof state:
α : Sort u_1
f : Bool → α
H : f false ≠ f true
x y : Bool
hxy : f x = f y
⊢ x = y

Tactic:
cases x <;> cases y

Result:
case false.false
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f false = f false
⊢ false = false

case false.true
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f false = f true
⊢ false = true

case true.false
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f true = f false
⊢ true = false

case true.true
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f true = f true
⊢ true = true