harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/GaugeRescale.lean
theorem gauge_gaugeRescale (s : Set E) {t : Set E} (hta : Absorbent ℝ t) (htb : IsVonNBounded ℝ t)
    (x : E) : gauge t (gaugeRescale s t x) = gauge s x

Proof state:
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ gauge t (gaugeRescale s t x) = gauge s x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Result:
case inl
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
⊢ gauge t (gaugeRescale s t 0) = gauge s 0

case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gauge t (gaugeRescale s t x) = gauge s x

Proof state:
case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gauge t (gaugeRescale s t x) = gauge s x

Tactic:
exact gauge_gaugeRescale' s ((gauge_pos hta htb).2 hx).ne'

Result:
no goals

Proof state:
case inl
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
⊢ gauge t (gaugeRescale s t 0) = gauge s 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem right_vsub_midpoint (p₁ p₂ : P) : p₂ -ᵥ midpoint R p₁ p₂ = (⅟ 2 : R) • (p₂ -ᵥ p₁)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ : P
⊢ p₂ -ᵥ midpoint R p₁ p₂ = ⅟2 • (p₂ -ᵥ p₁)

Tactic:
rw [midpoint_comm, left_vsub_midpoint]

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
lemma doubleDualEmb_injective : Injective (doubleDualEmb : α → AddChar (AddChar α ℂ) ℂ) :=
  doubleDualEmb.ker_eq_bot_iff.1 <| eq_bot_iff.2 fun a ha ↦
    forall_apply_eq_zero.1 fun ψ ↦ by simpa using DFunLike.congr_fun ha (Additive.ofMul ψ)

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Finite α
a : α
ha : a ∈ doubleDualEmb.ker
ψ : AddChar α ℂ
⊢ ψ a = 1

Tactic:
simpa using DFunLike.congr_fun ha (Additive.ofMul ψ)

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem minimal_mem_image (f : α ↪o β) (hx : Minimal (· ∈ s) x) : Minimal (· ∈ f '' s) (f x) :=
  _root_.minimal_mem_image_monotone (by simp [f.le_iff_le]) hx

Proof state:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α ↪o β
hx : Minimal (fun x => x ∈ s) x
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma inv_le_one_iff₀ : a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a

Proof state:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulStrictMono G₀
⊢ a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a

Tactic:
simp only [← not_lt, one_lt_inv_iff₀, not_and_or]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem eval_preimage' [DecidableEq ι] {s : Set (α i)} :
    eval i ⁻¹' s = pi {i} (update (fun _ => univ) i s)

Proof state:
ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
⊢ eval i ⁻¹' s = {i}.pi (update (fun x => univ) i s)

Tactic:
ext

Result:
case h
ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
x✝ : (x : ι) → α x
⊢ x✝ ∈ eval i ⁻¹' s ↔ x✝ ∈ {i}.pi (update (fun x => univ) i s)

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
x✝ : (x : ι) → α x
⊢ x✝ ∈ eval i ⁻¹' s ↔ x✝ ∈ {i}.pi (update (fun x => univ) i s)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finite/Card.lean
theorem card_eq_coe_natCard (α : Type*) [Finite α] : card α = Nat.card α

Proof state:
case a
α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = Cardinal.toENat (Cardinal.mk α)

Tactic:
rw [Cardinal.natCast_eq_toENat_iff]

Result:
case a
α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = Cardinal.mk α

Proof state:
case a
α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = Cardinal.mk α

Tactic:
exact Nat.cast_card

Result:
no goals

Proof state:
α : Type u_4
inst✝ : Finite α
⊢ card α = ↑(Nat.card α)

Tactic:
unfold ENat.card

Result:
α : Type u_4
inst✝ : Finite α
⊢ Cardinal.toENat (Cardinal.mk α) = ↑(Nat.card α)

Proof state:
α : Type u_4
inst✝ : Finite α
⊢ Cardinal.toENat (Cardinal.mk α) = ↑(Nat.card α)

Tactic:
apply symm

Result:
case a
α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = Cardinal.toENat (Cardinal.mk α)
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem second_iso {X Y : Submodule R M} (_ : X ⋖ X ⊔ Y) :
    Iso (X,X ⊔ Y) (X ⊓ Y,Y)

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ Iso (X, X ⊔ Y) (X ⊓ Y, Y)

Tactic:
constructor

Result:
case val
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ (↥(X, X ⊔ Y).2 ⧸ Submodule.comap (X, X ⊔ Y).2.subtype (X, X ⊔ Y).1) ≃ₗ[R]
    ↥(X ⊓ Y, Y).2 ⧸ Submodule.comap (X ⊓ Y, Y).2.subtype (X ⊓ Y, Y).1

Proof state:
case val
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ (↥(X, X ⊔ Y).2 ⧸ Submodule.comap (X, X ⊔ Y).2.subtype (X, X ⊔ Y).1) ≃ₗ[R]
    ↥(X ⊓ Y, Y).2 ⧸ Submodule.comap (X ⊓ Y, Y).2.subtype (X ⊓ Y, Y).1

Tactic:
rw [sup_comm, inf_comm]

Result:
case val
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ (↥(X, Y ⊔ X).2 ⧸ Submodule.comap (X, Y ⊔ X).2.subtype (X, Y ⊔ X).1) ≃ₗ[R]
    ↥(Y ⊓ X, Y).2 ⧸ Submodule.comap (Y ⊓ X, Y).2.subtype (Y ⊓ X, Y).1

Proof state:
case val
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ (↥(X, Y ⊔ X).2 ⧸ Submodule.comap (X, Y ⊔ X).2.subtype (X, Y ⊔ X).1) ≃ₗ[R]
    ↥(Y ⊓ X, Y).2 ⧸ Submodule.comap (Y ⊓ X, Y).2.subtype (Y ⊓ X, Y).1

Tactic:
dsimp

Result:
case val
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ (↥(Y ⊔ X) ⧸ Submodule.comap (Y ⊔ X).subtype X) ≃ₗ[R] ↥Y ⧸ Submodule.comap Y.subtype Y ⊓ Submodule.comap Y.subtype X

Proof state:
case val
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ (↥(Y ⊔ X) ⧸ Submodule.comap (Y ⊔ X).subtype X) ≃ₗ[R] ↥Y ⧸ Submodule.comap Y.subtype Y ⊓ Submodule.comap Y.subtype X

Tactic:
exact (LinearMap.quotientInfEquivSupQuotient Y X).symm

Result:
no goals
-- Mathlib/Data/Finsupp/SMul.lean
theorem filter_smul {_ : Monoid R} [AddMonoid M] [DistribMulAction R M] {b : R} {v : α →₀ M} :
    (b • v).filter p = b • v.filter p :=
  DFunLike.coe_injective <| by
    simp only [filter_eq_indicator, coe_smul]
    exact Set.indicator_const_smul { x | p x } b v

Proof state:
α : Type u_1
M : Type u_3
R : Type u_6
p : α → Prop
inst✝² : DecidablePred p
x✝ : Monoid R
inst✝¹ : AddMonoid M
inst✝ : DistribMulAction R M
b : R
v : α →₀ M
⊢ (fun f => ⇑f) (filter p (b • v)) = (fun f => ⇑f) (b • filter p v)

Tactic:
simp only [filter_eq_indicator, coe_smul]

Result:
α : Type u_1
M : Type u_3
R : Type u_6
p : α → Prop
inst✝² : DecidablePred p
x✝ : Monoid R
inst✝¹ : AddMonoid M
inst✝ : DistribMulAction R M
b : R
v : α →₀ M
⊢ {x | p x}.indicator (b • ⇑v) = b • {x | p x}.indicator ⇑v

Proof state:
α : Type u_1
M : Type u_3
R : Type u_6
p : α → Prop
inst✝² : DecidablePred p
x✝ : Monoid R
inst✝¹ : AddMonoid M
inst✝ : DistribMulAction R M
b : R
v : α →₀ M
⊢ {x | p x}.indicator (b • ⇑v) = b • {x | p x}.indicator ⇑v

Tactic:
exact Set.indicator_const_smul { x | p x } b v

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem dist_reflection_eq_of_mem (s : AffineSubspace ℝ P) [Nonempty s]
    [HasOrthogonalProjection s.direction] {p₁ : P} (hp₁ : p₁ ∈ s) (p₂ : P) :
    dist p₁ (reflection s p₂) = dist p₁ p₂

Proof state:
case h.e'_2.h.e'_3
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ : P
hp₁ : (reflection s) p₁ = p₁
p₂ : P
⊢ p₁ = (reflection s) p₁

Tactic:
rw [hp₁]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ : P
hp₁ : (reflection s) p₁ = p₁
p₂ : P
⊢ dist p₁ ((reflection s) p₂) = dist p₁ p₂

Tactic:
convert (reflection s).dist_map p₁ p₂

Result:
case h.e'_2.h.e'_3
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ : P
hp₁ : (reflection s) p₁ = p₁
p₂ : P
⊢ p₁ = (reflection s) p₁

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
⊢ dist p₁ ((reflection s) p₂) = dist p₁ p₂

Tactic:
rw [← reflection_eq_self_iff p₁] at hp₁

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ : P
hp₁ : (reflection s) p₁ = p₁
p₂ : P
⊢ dist p₁ ((reflection s) p₂) = dist p₁ p₂
-- Mathlib/Logic/Equiv/Basic.lean
theorem prodCongrLeft_trans_prodComm :
    (prodCongrLeft e).trans (prodComm _ _) = (prodComm _ _).trans (prodCongrRight e)

Proof state:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : β₁
b : α₁
⊢ ((prodCongrLeft e).trans (prodComm β₂ α₁)) (a, b) = ((prodComm β₁ α₁).trans (prodCongrRight e)) (a, b)

Tactic:
simp

Result:
no goals

Proof state:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (prodCongrLeft e).trans (prodComm β₂ α₁) = (prodComm β₁ α₁).trans (prodCongrRight e)

Tactic:
ext ⟨a, b⟩ : 1

Result:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : β₁
b : α₁
⊢ ((prodCongrLeft e).trans (prodComm β₂ α₁)) (a, b) = ((prodComm β₁ α₁).trans (prodCongrRight e)) (a, b)
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem subset_smul_finset_iff : s ⊆ a • t ↔ a⁻¹ • s ⊆ t

Proof state:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ ↑s ⊆ a • ↑t ↔ a⁻¹ • ↑s ⊆ ↑t

Tactic:
exact Set.subset_smul_set_iff

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ ↑s ⊆ ↑(a • t) ↔ ↑(a⁻¹ • s) ⊆ ↑t

Tactic:
push_cast

Result:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ ↑s ⊆ a • ↑t ↔ a⁻¹ • ↑s ⊆ ↑t

Proof state:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ s ⊆ a • t ↔ a⁻¹ • s ⊆ t

Tactic:
simp_rw [← coe_subset]

Result:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ ↑s ⊆ ↑(a • t) ↔ ↑(a⁻¹ • s) ⊆ ↑t
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Cofork.app_zero_eq_comp_π_right (s : Cofork f g) : s.ι.app zero = g ≫ s.π

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

Tactic:
rw [← s.app_one_eq_π, ← s.w right, parallelPair_map_right]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem integral_comp_polarCoord_symm {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] (f : ℂ → E) :
    (∫ p in polarCoord.target, p.1 • f (Complex.polarCoord.symm p)) = ∫ p, f p

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑Complex.polarCoord.symm p) =
    ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (measurableEquivRealProd.symm (↑polarCoord.symm p))

Tactic:
simp_rw [measurableEquivRealProd_symm_polarCoord_symm_apply]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑Complex.polarCoord.symm p) = ∫ (p : ℂ), f p

Tactic:
rw [← (Complex.volume_preserving_equiv_real_prod.symm).integral_comp
  measurableEquivRealProd.symm.measurableEmbedding, ← integral_comp_polarCoord_symm]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑Complex.polarCoord.symm p) =
    ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (measurableEquivRealProd.symm (↑polarCoord.symm p))
-- Mathlib/Analysis/Calculus/LogDeriv.lean
@[simp]
lemma logDeriv_zpow (x : 𝕜) (n : ℤ) : logDeriv (· ^ n) x = n / x

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ logDeriv (fun x => x ^ n) x = ↑n / x

Tactic:
rw [logDeriv_fun_zpow (by fun_prop), logDeriv_id', mul_one_div]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ DifferentiableAt 𝕜 (fun x => x) x

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem mem_nhds_top_iff {s : Set EReal} : s ∈ 𝓝 (⊤ : EReal) ↔ ∃ y : ℝ, Ioi (y : EReal) ⊆ s :=
  nhds_top_basis.mem_iff.trans <| by simp only [true_and]

Proof state:
s : Set EReal
⊢ (∃ i, True ∧ Ioi ↑i ⊆ s) ↔ ∃ y, Ioi ↑y ⊆ s

Tactic:
simp only [true_and]

Result:
no goals
-- Mathlib/GroupTheory/Sylow.lean
theorem not_dvd_index' [hp : Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G)
    (hP : P.relindex P.normalizer ≠ 0) : ¬ p ∣ P.index

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : (↑P).relindex (↑P).normalizer ≠ 0
this✝ : (↑(P.subtype ⋯)).Normal
this : (↑(P.subtype ⋯)).FiniteIndex
⊢ ¬p ∣ (↑P).relindex (↑P).normalizer * Nat.card (Sylow p G)

Tactic:
replace hP := not_dvd_index_aux (P.subtype le_normalizer)

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this✝ : (↑(P.subtype ⋯)).Normal
this : (↑(P.subtype ⋯)).FiniteIndex
hP : ¬p ∣ (↑(P.subtype ⋯)).index
⊢ ¬p ∣ (↑P).relindex (↑P).normalizer * Nat.card (Sylow p G)

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this✝ : (↑(P.subtype ⋯)).Normal
this : (↑(P.subtype ⋯)).FiniteIndex
hP : ¬p ∣ (↑(P.subtype ⋯)).index
⊢ ¬p ∣ (↑P).relindex (↑P).normalizer * Nat.card (Sylow p G)

Tactic:
exact hp.1.not_dvd_mul hP (not_dvd_card_sylow p G)

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : (↑P).relindex (↑P).normalizer ≠ 0
this : (↑(P.subtype ⋯)).Normal
⊢ ¬p ∣ (↑P).relindex (↑P).normalizer * Nat.card (Sylow p G)

Tactic:
haveI : (P.subtype le_normalizer).FiniteIndex := ⟨hP⟩

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : (↑P).relindex (↑P).normalizer ≠ 0
this✝ : (↑(P.subtype ⋯)).Normal
this : (↑(P.subtype ⋯)).FiniteIndex
⊢ ¬p ∣ (↑P).relindex (↑P).normalizer * Nat.card (Sylow p G)

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : (↑P).relindex (↑P).normalizer ≠ 0
⊢ ¬p ∣ (↑P).index

Tactic:
rw [← relindex_mul_index le_normalizer, ← card_eq_index_normalizer]

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : (↑P).relindex (↑P).normalizer ≠ 0
⊢ ¬p ∣ (↑P).relindex (↑P).normalizer * Nat.card (Sylow p G)

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : (↑P).relindex (↑P).normalizer ≠ 0
⊢ ¬p ∣ (↑P).relindex (↑P).normalizer * Nat.card (Sylow p G)

Tactic:
haveI : (P.subtype le_normalizer).Normal :=
  Subgroup.normal_in_normalizer

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : (↑P).relindex (↑P).normalizer ≠ 0
this : (↑(P.subtype ⋯)).Normal
⊢ ¬p ∣ (↑P).relindex (↑P).normalizer * Nat.card (Sylow p G)
-- Mathlib/AlgebraicGeometry/Scheme.lean
@[simp]
lemma Scheme.iso_inv_base_hom_base_apply {X Y : Scheme.{u}} (e : X ≅ Y) (y : Y) :
    (e.hom.base (e.inv.base y)) = y

Proof state:
X Y : Scheme
e : X ≅ Y
y : ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom (e.inv.base ≫ e.hom.base)) y = (ConcreteCategory.hom (𝟙 Y.toPresheafedSpace).base) y

Tactic:
simp

Result:
no goals

Proof state:
X Y : Scheme
e : X ≅ Y
y : ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y) = y

Tactic:
show (e.inv.base ≫ e.hom.base) y = 𝟙 Y.toPresheafedSpace y

Result:
X Y : Scheme
e : X ≅ Y
y : ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom (e.inv.base ≫ e.hom.base)) y = (ConcreteCategory.hom (𝟙 Y.toPresheafedSpace).base) y
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem quotQuotEquivQuotOfLE_symm_comp_mk (h : I ≤ J) :
    RingHom.comp (↑(quotQuotEquivQuotOfLE h).symm) (Ideal.Quotient.mk J) = quotQuotMk I J

Proof state:
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ (↑(quotQuotEquivQuotOfLE h).symm).comp (Ideal.Quotient.mk J) = quotQuotMk I J

Tactic:
ext

Result:
case a
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ ((↑(quotQuotEquivQuotOfLE h).symm).comp (Ideal.Quotient.mk J)) x✝ = (quotQuotMk I J) x✝

Proof state:
case a
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ ((↑(quotQuotEquivQuotOfLE h).symm).comp (Ideal.Quotient.mk J)) x✝ = (quotQuotMk I J) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem piIsoPi_inv_π {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι) :
    (piIsoPi α).inv ≫ Pi.π α i = piπ α i

Proof state:
ι : Type v
α : ι → TopCat
i : ι
⊢ (piIsoPi α).inv ≫ Pi.π α i = piπ α i

Tactic:
simp [piIsoPi]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem aeval_gen_minpoly (α : E) : aeval (AdjoinSimple.gen F α) (minpoly F α) = 0

Proof state:
case h.e'_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ↑((aeval (AdjoinSimple.gen F α)) (minpoly F α)) = (aeval α) (minpoly F α)

Tactic:
conv in aeval α => rw [← AdjoinSimple.algebraMap_gen F α]

Result:
case h.e'_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ↑((aeval (AdjoinSimple.gen F α)) (minpoly F α)) =
    (aeval ((algebraMap (↥F⟮α⟯) E) (AdjoinSimple.gen F α))) (minpoly F α)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ (aeval (AdjoinSimple.gen F α)) (minpoly F α) = 0

Tactic:
ext

Result:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ↑((aeval (AdjoinSimple.gen F α)) (minpoly F α)) = ↑0

Proof state:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ↑((aeval (AdjoinSimple.gen F α)) (minpoly F α)) = ↑0

Tactic:
convert minpoly.aeval F α

Result:
case h.e'_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ↑((aeval (AdjoinSimple.gen F α)) (minpoly F α)) = (aeval α) (minpoly F α)

Proof state:
case h.e'_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ ↑((aeval (AdjoinSimple.gen F α)) (minpoly F α)) =
    (aeval ((algebraMap (↥F⟮α⟯) E) (AdjoinSimple.gen F α))) (minpoly F α)

Tactic:
exact (aeval_algebraMap_apply E (AdjoinSimple.gen F α) _).symm

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Adjunction.lean
@[simp]
lemma localization_unit_app (X₁ : C₁) :
    (adj.localization L₁ W₁ L₂ W₂ G' F').unit.app (L₁.obj X₁) =
    L₁.map (adj.unit.app X₁) ≫ (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫
      F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_6, u_1} C₁
inst✝⁶ : Category.{u_8, u_2} C₂
inst✝⁵ : Category.{u_5, u_3} D₁
inst✝⁴ : Category.{u_7, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
⊢ (adj.localization L₁ W₁ L₂ W₂ G' F').unit.app (L₁.obj X₁) =
    L₁.map (adj.unit.app X₁) ≫
      (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫ F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)

Tactic:
apply Localization.ε_app

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma ext_iff' {χ₁ χ₂ : Weight R L M} : (χ₁ : L → R) = χ₂ ↔ χ₁ = χ₂

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : Weight R L M
⊢ ⇑χ₁ = ⇑χ₂ ↔ χ₁ = χ₂

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Opposite.lean
theorem unop_mem_unop {s : Set αᵒᵖ} {a : αᵒᵖ} : unop a ∈ s.unop ↔ a ∈ s

Proof state:
α : Type u_1
s : Set αᵒᵖ
a : αᵒᵖ
⊢ unop a ∈ s.unop ↔ a ∈ s

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Kernel/Invariance.lean
theorem Invariant.comp (hκ : Invariant κ μ) (hη : Invariant η μ) :
    Invariant (κ ∘ₖ η) μ

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
⊢ (κ ∘ₖ η).Invariant μ

Tactic:
simp_rw [Invariant, ← comp_const_apply_eq_bind (κ ∘ₖ η) μ hα.some, comp_assoc, hη.comp_const,
  hκ.comp_const, const_apply]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
⊢ (κ ∘ₖ η).Invariant μ

Tactic:
rcases isEmpty_or_nonempty α with _ | hα

Result:
case inl
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
h✝ : IsEmpty α
⊢ (κ ∘ₖ η).Invariant μ

case inr
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
⊢ (κ ∘ₖ η).Invariant μ

Proof state:
case inl
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
h✝ : IsEmpty α
⊢ (κ ∘ₖ η).Invariant μ

Tactic:
exact Subsingleton.elim _ _

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_filter_lt_of_le_right [DecidablePred (· < c)] (hcb : c ≤ b) :
    {x ∈ Ico a b | x < c} = Ico a c

Proof state:
α : Type u_2
a b c : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a c

Tactic:
ext x

Result:
case h
α : Type u_2
a b c : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
x : α
⊢ x ∈ filter (fun x => x < c) (Ico a b) ↔ x ∈ Ico a c

Proof state:
case h
α : Type u_2
a b c : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
x : α
⊢ x ∈ filter (fun x => x < c) (Ico a b) ↔ x ∈ Ico a c

Tactic:
rw [mem_filter, mem_Ico, mem_Ico, and_right_comm]

Result:
case h
α : Type u_2
a b c : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
x : α
⊢ (a ≤ x ∧ x < c) ∧ x < b ↔ a ≤ x ∧ x < c

Proof state:
case h
α : Type u_2
a b c : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
x : α
⊢ (a ≤ x ∧ x < c) ∧ x < b ↔ a ≤ x ∧ x < c

Tactic:
exact and_iff_left_of_imp fun h => h.2.trans_le hcb

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Girth.lean
@[simp] lemma egirth_bot : egirth (⊥ : SimpleGraph α) = ⊤

Proof state:
α : Type u_1
⊢ ⊥.egirth = ⊤

Tactic:
simp

Result:
no goals