harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Real/EReal.lean
lemma le_mul_of_forall_lt (h₁ : 0 < a ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ 0 < b)
    (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b

Proof state:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd : a * b < d
⊢ c ≤ d

Tactic:
obtain ⟨a', aa', hd⟩ := exists_mul_left_lt (h₁.imp_left ne_of_gt) h₂ hd

Result:
case intro.intro
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd✝ : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd : a' * b < d
⊢ c ≤ d

Proof state:
case intro.intro
a b c : EReal
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd✝ : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
h₂ : a' ≠ ⊤ ∨ b ≠ 0
⊢ c ≤ d

Tactic:
obtain ⟨b', bb', hd⟩ := exists_mul_right_lt h₁ h₂ hd

Result:
case intro.intro.intro.intro
a b c : EReal
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd✝¹ : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd✝ : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
h₂ : a' ≠ ⊤ ∨ b ≠ 0
b' : EReal
bb' : b' ∈ Ioo b ⊤
hd : a' * b' < d
⊢ c ≤ d

Proof state:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_

Result:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd : a * b < d
⊢ c ≤ d

Proof state:
case intro.intro
a b c : EReal
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd✝ : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
⊢ c ≤ d

Tactic:
replace h₂ : a' ≠ ⊤ ∨ b ≠ 0 := Or.inl (mem_Ioo.1 aa').2.ne

Result:
case intro.intro
a b c : EReal
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd✝ : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
h₂ : a' ≠ ⊤ ∨ b ≠ 0
⊢ c ≤ d

Proof state:
case intro.intro
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd✝ : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd : a' * b < d
⊢ c ≤ d

Tactic:
replace h₁ : 0 < a' ∨ b ≠ ⊤ := h₁.imp_left fun a0 ↦ a0.trans (mem_Ioo.1 aa').1

Result:
case intro.intro
a b c : EReal
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd✝ : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
⊢ c ≤ d

Proof state:
case intro.intro.intro.intro
a b c : EReal
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd✝¹ : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd✝ : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
h₂ : a' ≠ ⊤ ∨ b ≠ 0
b' : EReal
bb' : b' ∈ Ioo b ⊤
hd : a' * b' < d
⊢ c ≤ d

Tactic:
exact (h a' (mem_Ioo.1 aa').1 b' (mem_Ioo.1 bb').1).trans hd.le

Result:
no goals
-- Mathlib/Data/Set/Opposite.lean
theorem op_mem_op {s : Set α} {a : α} : op a ∈ s.op ↔ a ∈ s

Proof state:
α : Type u_1
s : Set α
a : α
⊢ op a ∈ s.op ↔ a ∈ s

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem isInitial_ord (c : Cardinal) : IsInitial c.ord

Proof state:
c : Cardinal.{u_1}
⊢ c.ord.IsInitial

Tactic:
rw [IsInitial, card_ord]

Result:
no goals
-- Mathlib/Data/Set/Functor.lean
theorem mem_of_mem_image_val (ha : a ∈ (γ : Set α)) : ⟨a, image_val_subset ha⟩ ∈ γ

Proof state:
α : Type u
β : Set α
γ : Set ↑β
a : α
ha : a ∈ Subtype.val '' γ
⊢ ⟨a, ⋯⟩ ∈ γ

Tactic:
rcases ha with ⟨_, ha, rfl⟩

Result:
case intro.intro
α : Type u
β : Set α
γ : Set ↑β
w✝ : { x // x ∈ β }
ha : w✝ ∈ γ
⊢ ⟨↑w✝, ⋯⟩ ∈ γ

Proof state:
case intro.intro
α : Type u
β : Set α
γ : Set ↑β
w✝ : { x // x ∈ β }
ha : w✝ ∈ γ
⊢ ⟨↑w✝, ⋯⟩ ∈ γ

Tactic:
exact ha

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_apply₀ (f : ι → Measure α) {s : Set α} (hs : NullMeasurableSet s (sum f)) :
    sum f s = ∑' i, f i s

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
⊢ (sum f) s ≤ ∑' (i : ι), (f i) s

Tactic:
rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, t_meas, ht⟩

Result:
case intro.intro.intro
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
t : Set α
ts : t ⊆ s
t_meas : MeasurableSet t
ht : t =ᶠ[ae (sum f)] s
⊢ (sum f) s ≤ ∑' (i : ι), (f i) s

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
⊢ (sum f) s = ∑' (i : ι), (f i) s

Tactic:
apply le_antisymm ?_ (le_sum_apply _ _)

Result:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
⊢ (sum f) s ≤ ∑' (i : ι), (f i) s

Proof state:
case intro.intro.intro
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
t : Set α
ts : t ⊆ s
t_meas : MeasurableSet t
ht : t =ᶠ[ae (sum f)] s
⊢ (sum f) s ≤ ∑' (i : ι), (f i) s

Tactic:
calc
sum f s = sum f t := measure_congr ht.symm
_ = ∑' i, f i t := sum_apply _ t_meas
_ ≤ ∑' i, f i s := ENNReal.tsum_le_tsum fun i ↦ measure_mono ts

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
lemma exists_lt_of_expect_lt (hs : s.Nonempty) (h : 𝔼 i ∈ s, f i < a) : ∃ x ∈ s, f x < a

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : LinearOrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : 𝔼 i ∈ s, f i < a
⊢ ∃ x ∈ s, f x < a

Tactic:
contrapose! h

Result:
ι : Type u_1
α : Type u_2
inst✝² : LinearOrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ a ≤ 𝔼 i ∈ s, f i

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : LinearOrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ a ≤ 𝔼 i ∈ s, f i

Tactic:
exact le_expect hs h

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
lemma S_mul_S_eq : (S : Matrix (Fin 2) (Fin 2) ℤ) * S = -1

Proof state:
⊢ !![-1, 0; 0, -1] = -1

Tactic:
exact Eq.symm (eta_fin_two (-1))

Result:
no goals

Proof state:
⊢ ↑S * ↑S = -1

Tactic:
simp only [S, Int.reduceNeg, pow_two, coe_mul, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd,
  vecMul_cons, head_cons, zero_smul, tail_cons, neg_smul, one_smul, neg_cons, neg_zero, neg_empty,
  empty_vecMul, add_zero, zero_add, empty_mul, Equiv.symm_apply_apply]

Result:
⊢ !![-1, 0; 0, -1] = -1
-- Mathlib/Data/Sigma/Basic.lean
theorem Function.Injective.sigma_map {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
    (h₁ : Injective f₁) (h₂ : ∀ a, Injective (f₂ a)) : Injective (Sigma.map f₁ f₂)
  | ⟨i, x⟩, ⟨j, y⟩, h => by
    obtain rfl : i = j := h₁ (Sigma.mk.inj_iff.mp h).1
    obtain rfl : x = y := h₂ i (sigma_mk_injective h)
    rfl

Proof state:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
j : α₁
y : β₁ j
h : Sigma.map f₁ f₂ ⟨i, x⟩ = Sigma.map f₁ f₂ ⟨j, y⟩
⊢ ⟨i, x⟩ = ⟨j, y⟩

Tactic:
obtain rfl : i = j := h₁ (Sigma.mk.inj_iff.mp h).1

Result:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x y : β₁ i
h : Sigma.map f₁ f₂ ⟨i, x⟩ = Sigma.map f₁ f₂ ⟨i, y⟩
⊢ ⟨i, x⟩ = ⟨i, y⟩

Proof state:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
h : Sigma.map f₁ f₂ ⟨i, x⟩ = Sigma.map f₁ f₂ ⟨i, x⟩
⊢ ⟨i, x⟩ = ⟨i, x⟩

Tactic:
rfl

Result:
no goals

Proof state:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x y : β₁ i
h : Sigma.map f₁ f₂ ⟨i, x⟩ = Sigma.map f₁ f₂ ⟨i, y⟩
⊢ ⟨i, x⟩ = ⟨i, y⟩

Tactic:
obtain rfl : x = y := h₂ i (sigma_mk_injective h)

Result:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
h : Sigma.map f₁ f₂ ⟨i, x⟩ = Sigma.map f₁ f₂ ⟨i, x⟩
⊢ ⟨i, x⟩ = ⟨i, x⟩
-- Mathlib/Topology/Order/Lattice.lean
lemma ContinuousWithinAt.finset_sup
    (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) : ContinuousWithinAt (s.sup f) t x

Proof state:
L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.sup f) t x

Tactic:
simpa only [← Finset.sup_apply] using finset_sup_apply hs

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem sSup_disjoint_iff {s : Set α} : Disjoint (sSup s) a ↔ ∀ b ∈ s, Disjoint b a

Proof state:
α : Type u
inst✝ : Frame α
a : α
s : Set α
⊢ Disjoint (sSup s) a ↔ ∀ b ∈ s, Disjoint b a

Tactic:
simp only [disjoint_iff, sSup_inf_eq, iSup_eq_bot]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma image_inv [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Set α) :
    f '' s⁻¹ = (f '' s)⁻¹

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' s⁻¹ = (⇑f '' s)⁻¹

Tactic:
rw [← image_inv_eq_inv, ← image_inv_eq_inv]

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' ((fun x => x⁻¹) '' s) = (fun x => x⁻¹) '' (⇑f '' s)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' ((fun x => x⁻¹) '' s) = (fun x => x⁻¹) '' (⇑f '' s)

Tactic:
exact image_comm (map_inv _)

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_self_closure : hausdorffDist s (closure s) = 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ hausdorffDist s (closure s) = 0

Tactic:
simp [hausdorffDist]

Result:
no goals
-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem Cofix.bisim₂ {α : TypeVec n} (r : Cofix F α → Cofix F α → Prop)
    (h : ∀ x y, r x y → LiftR' (RelLast' α r) (Cofix.dest x) (Cofix.dest y)) :
    ∀ x y, r x y → x = y :=
  Cofix.bisim r <| by intros; rw [← LiftR_RelLast_iff]; apply h; assumption

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR (fun {i} => α.RelLast r) x✝.dest y✝.dest

Tactic:
rw [← LiftR_RelLast_iff]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR' (α.RelLast' r) x✝.dest y✝.dest

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR' (α.RelLast' r) x✝.dest y✝.dest

Tactic:
apply h

Result:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ r x✝ y✝

Proof state:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ r x✝ y✝

Tactic:
assumption

Result:
no goals

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
⊢ ∀ (x y : Cofix F α), r x y → LiftR (fun {i} => α.RelLast r) x.dest y.dest

Tactic:
intros

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR (fun {i} => α.RelLast r) x✝.dest y✝.dest
-- Mathlib/GroupTheory/Sylow.lean
theorem normalizer_normalizer {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) :
    P.normalizer.normalizer = P.normalizer

Proof state:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : True → (↑P).normalizer.subgroupOf (↑P).normalizer.normalizer = ⊤
⊢ (↑P).normalizer.normalizer = (↑P).normalizer

Tactic:
rw [← range_subtype P.normalizer.normalizer, MonoidHom.range_eq_map,
  ← this trivial]

Result:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : True → (↑P).normalizer.subgroupOf (↑P).normalizer.normalizer = ⊤
⊢ Subgroup.map (↑P).normalizer.normalizer.subtype ((↑P).normalizer.subgroupOf (↑P).normalizer.normalizer) =
    (↑P).normalizer

Proof state:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ (↑P).normalizer.normalizer = (↑P).normalizer

Tactic:
have := normal_of_normalizer_normal (P.subtype (le_normalizer.trans le_normalizer))

Result:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : (↑(P.subtype ⋯)).normalizer.Normal → (↑(P.subtype ⋯)).Normal
⊢ (↑P).normalizer.normalizer = (↑P).normalizer

Proof state:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : True → (↑P).normalizer.subgroupOf (↑P).normalizer.normalizer = ⊤
⊢ Subgroup.map (↑P).normalizer.normalizer.subtype ((↑P).normalizer.subgroupOf (↑P).normalizer.normalizer) =
    (↑P).normalizer

Tactic:
exact map_comap_eq_self (le_normalizer.trans (ge_of_eq (range_subtype _)))

Result:
no goals

Proof state:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : (↑(P.subtype ⋯)).normalizer.Normal → (↑(P.subtype ⋯)).Normal
⊢ (↑P).normalizer.normalizer = (↑P).normalizer

Tactic:
simp_rw [← normalizer_eq_top_iff, coe_subtype, ← subgroupOf_normalizer_eq le_normalizer, ←
  subgroupOf_normalizer_eq le_rfl, subgroupOf_self] at this

Result:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : True → (↑P).normalizer.subgroupOf (↑P).normalizer.normalizer = ⊤
⊢ (↑P).normalizer.normalizer = (↑P).normalizer
-- Mathlib/Data/Fintype/Sets.lean
theorem filter_mem_univ_eq_toFinset [Fintype α] (s : Set α) [Fintype s] [DecidablePred (· ∈ s)] :
    Finset.univ.filter (· ∈ s) = s.toFinset

Proof state:
α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ filter (fun x => x ∈ s) Finset.univ = s.toFinset

Tactic:
ext

Result:
case h
α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x => x ∈ s
a✝ : α
⊢ a✝ ∈ filter (fun x => x ∈ s) Finset.univ ↔ a✝ ∈ s.toFinset

Proof state:
case h
α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x => x ∈ s
a✝ : α
⊢ a✝ ∈ filter (fun x => x ∈ s) Finset.univ ↔ a✝ ∈ s.toFinset

Tactic:
simp only [Finset.mem_univ, decide_eq_true_eq, forall_true_left, mem_filter,
  true_and, mem_toFinset]

Result:
no goals
-- Mathlib/Algebra/Ring/Divisibility/Basic.lean
theorem map_dvd_iff (f : F) {a b} : f a ∣ f b ↔ a ∣ b :=
  let f := MulEquivClass.toMulEquiv f
  ⟨fun h ↦ by rw [← f.left_inv a, ← f.left_inv b]; exact map_dvd f.symm h, map_dvd f⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Semigroup α
inst✝² : Semigroup β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f✝ : F
a b : α
f : α ≃* β := ↑f✝
h : f✝ a ∣ f✝ b
⊢ f.invFun (f.toFun a) ∣ f.invFun (f.toFun b)

Tactic:
exact map_dvd f.symm h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Semigroup α
inst✝² : Semigroup β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f✝ : F
a b : α
f : α ≃* β := ↑f✝
h : f✝ a ∣ f✝ b
⊢ a ∣ b

Tactic:
rw [← f.left_inv a, ← f.left_inv b]

Result:
α : Type u_1
β : Type u_2
inst✝³ : Semigroup α
inst✝² : Semigroup β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f✝ : F
a b : α
f : α ≃* β := ↑f✝
h : f✝ a ∣ f✝ b
⊢ f.invFun (f.toFun a) ∣ f.invFun (f.toFun b)
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma liftCycles_comp_cyclesMap {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j)
    (hk : k ≫ K.d i j = 0) (φ : K ⟶ L) :
    K.liftCycles k j hj hk ≫ cyclesMap φ i = L.liftCycles (k ≫ φ.f i) j hj
      (by rw [assoc, φ.comm, reassoc_of% hk, zero_comp])

Proof state:
C : Type u_1
inst✝⁴ : Category.{?u.107537, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ✝ : K ⟶ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
φ : K ⟶ L
⊢ (k ≫ φ.f i) ≫ L.d i j = 0

Tactic:
rw [assoc, φ.comm, reassoc_of% hk, zero_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex C c
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
φ : K ⟶ L
⊢ K.liftCycles k j hj hk ≫ cyclesMap φ i = L.liftCycles (k ≫ φ.f i) j hj ⋯

Tactic:
simp only [← cancel_mono (L.iCycles i), assoc, cyclesMap_i, liftCycles_i_assoc, liftCycles_i]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
protected lemma exists_congr_right : (∃ a, q (e a)) ↔ ∃ b, q b :=
  ⟨fun ⟨_, h⟩ ↦ ⟨_, h⟩, fun ⟨a, h⟩ ↦ ⟨e.symm a, by simpa using h⟩⟩

Proof state:
α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
x✝ : ∃ b, q b
a : β
h : q a
⊢ q (e (e.symm a))

Tactic:
simpa using h

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Trim.lean
lemma trim_eq_map (hm : m ≤ m0) : μ.trim hm = @Measure.map _ _ _ m id μ

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
⊢ μ.trim hm = Measure.map id μ

Tactic:
refine @Measure.ext α m _ _ (fun s hs ↦ ?_)

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
⊢ (μ.trim hm) s = (Measure.map id μ) s

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
⊢ (μ.trim hm) s = (Measure.map id μ) s

Tactic:
rw [Measure.map_apply (measurable_id'' hm) hs, trim_measurableSet_eq hm hs, Set.preimage_id]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean
theorem whiskerRight_naturality_id (f : G.obj a ⟶ a') :
    η.naturality (𝟙 a) ▷ f ≫ (α_ _ _ _).hom ≫ η.app a ◁ G.mapId a ▷ f =
    F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ _ _ _).hom

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η : OplaxNatTrans F G
a : B
a' : C
f : G.obj a ⟶ a'
⊢ (F.mapId a ▷ η.app a ≫ (λ_ (η.app a)).hom ≫ (ρ_ (η.app a)).inv) ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom =
    F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom

Tactic:
simp

Result:
no goals

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η : OplaxNatTrans F G
a : B
a' : C
f : G.obj a ⟶ a'
⊢ η.naturality (𝟙 a) ▷ f ≫ (α_ (η.app a) (G.map (𝟙 a)) f).hom ≫ η.app a ◁ G.mapId a ▷ f =
    F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom

Tactic:
rw [← associator_naturality_middle, ← comp_whiskerRight_assoc, naturality_id]

Result:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η : OplaxNatTrans F G
a : B
a' : C
f : G.obj a ⟶ a'
⊢ (F.mapId a ▷ η.app a ≫ (λ_ (η.app a)).hom ≫ (ρ_ (η.app a)).inv) ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom =
    F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
@[simp]
lemma inner_smul_left_complex {z : ℂ} {x y : E} : ⟪z • x, y⟫ = star z • ⟪x, y⟫

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℂ
x y : E
⊢ inner (z •> x) y = star z •> inner x y

Tactic:
rw [← star_inner]

Result:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℂ
x y : E
⊢ star (inner y (z •> x)) = star z •> inner x y

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℂ
x y : E
⊢ star (inner y (z •> x)) = star z •> inner x y

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem Basis.det_inv (b : Basis ι A M) (b' : Basis ι A M) :
    (b.isUnit_det b').unit⁻¹ = b'.det b

Proof state:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b b' : Basis ι A M
⊢ ↑⋯.unit⁻¹ = b'.det ⇑b

Tactic:
rw [← Units.mul_eq_one_iff_inv_eq, IsUnit.unit_spec, ← Basis.det_basis, ← Basis.det_basis]

Result:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b b' : Basis ι A M
⊢ LinearMap.det ↑(b.equiv b' (Equiv.refl ι)) * LinearMap.det ↑(b'.equiv b (Equiv.refl ι)) = 1

Proof state:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b b' : Basis ι A M
⊢ LinearMap.det ↑(b.equiv b' (Equiv.refl ι)) * LinearMap.det ↑(b'.equiv b (Equiv.refl ι)) = 1

Tactic:
exact LinearEquiv.det_mul_det_symm _

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
@[simp] lemma map_add {f : Ω → Ω'} (f_mble : Measurable f) (ν₁ ν₂ : FiniteMeasure Ω) :
    (ν₁ + ν₂).map f = ν₁.map f + ν₂.map f

Proof state:
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
f_mble : Measurable f
ν₁ ν₂ : FiniteMeasure Ω
⊢ (ν₁ + ν₂).map f = ν₁.map f + ν₂.map f

Tactic:
ext s s_mble

Result:
case h
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
f_mble : Measurable f
ν₁ ν₂ : FiniteMeasure Ω
s : Set Ω'
s_mble : MeasurableSet s
⊢ ↑((ν₁ + ν₂).map f) s = ↑(ν₁.map f + ν₂.map f) s

Proof state:
case h
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
f_mble : Measurable f
ν₁ ν₂ : FiniteMeasure Ω
s : Set Ω'
s_mble : MeasurableSet s
⊢ ↑((ν₁ + ν₂).map f) s = ↑(ν₁.map f + ν₂.map f) s

Tactic:
simp only [map_apply' _ f_mble.aemeasurable s_mble, toMeasure_add, Measure.add_apply]

Result:
no goals