harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem AEMeasurable.biSup {ι} {μ : Measure δ} (s : Set ι) {f : ι → δ → α} (hs : s.Countable)
    (hf : ∀ i ∈ s, AEMeasurable (f i) μ) : AEMeasurable (fun b => ⨆ i ∈ s, f i b) μ

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
g : ι → δ → α := fun i => if hi : i ∈ s then mk (f i) ⋯ else fun _b => sSup ∅
this : ∀ i ∈ s, Measurable (g i)
i : ι
hi : i ∈ s
⊢ ∀ᵐ (b : δ) ∂μ, f i b = g i b

Tactic:
simpa [g, hi] using (hf i hi).ae_eq_mk

Result:
no goals

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
⊢ AEMeasurable (fun b => ⨆ i ∈ s, f i b) μ

Tactic:
let g : ι → δ → α := fun i ↦ if hi : i ∈ s then (hf i hi).mk (f i) else fun _b ↦ sSup ∅

Result:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
g : ι → δ → α := fun i => if hi : i ∈ s then mk (f i) ⋯ else fun _b => sSup ∅
⊢ AEMeasurable (fun b => ⨆ i ∈ s, f i b) μ
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem RingHom.pNilradical_le_ker_of_perfectRing [ExpChar L p] [PerfectRing L p] :
    pNilradical K p ≤ RingHom.ker i := fun x h ↦ by
  obtain ⟨n, h⟩ := mem_pNilradical.1 h
  replace h := congr((iterateFrobeniusEquiv L p n).symm (i $h))
  rwa [map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply,
    map_zero, map_zero] at h

Proof state:
case intro
K : Type u_1
L : Type u_2
inst✝³ : CommSemiring K
inst✝² : CommSemiring L
i : K →+* L
p : ℕ
inst✝¹ : ExpChar L p
inst✝ : PerfectRing L p
x : K
h✝ : x ∈ pNilradical K p
n : ℕ
h : x ^ p ^ n = 0
⊢ x ∈ ker i

Tactic:
replace h := congr((iterateFrobeniusEquiv L p n).symm (i $h))

Result:
case intro
K : Type u_1
L : Type u_2
inst✝³ : CommSemiring K
inst✝² : CommSemiring L
i : K →+* L
p : ℕ
inst✝¹ : ExpChar L p
inst✝ : PerfectRing L p
x : K
h✝ : x ∈ pNilradical K p
n : ℕ
h : (iterateFrobeniusEquiv L p n).symm (i (x ^ p ^ n)) = (iterateFrobeniusEquiv L p n).symm (i 0)
⊢ x ∈ ker i

Proof state:
case intro
K : Type u_1
L : Type u_2
inst✝³ : CommSemiring K
inst✝² : CommSemiring L
i : K →+* L
p : ℕ
inst✝¹ : ExpChar L p
inst✝ : PerfectRing L p
x : K
h✝ : x ∈ pNilradical K p
n : ℕ
h : (iterateFrobeniusEquiv L p n).symm (i (x ^ p ^ n)) = (iterateFrobeniusEquiv L p n).symm (i 0)
⊢ x ∈ ker i

Tactic:
rwa [map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply,
  map_zero, map_zero] at h

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : CommSemiring K
inst✝² : CommSemiring L
i : K →+* L
p : ℕ
inst✝¹ : ExpChar L p
inst✝ : PerfectRing L p
x : K
h : x ∈ pNilradical K p
⊢ x ∈ ker i

Tactic:
obtain ⟨n, h⟩ := mem_pNilradical.1 h

Result:
case intro
K : Type u_1
L : Type u_2
inst✝³ : CommSemiring K
inst✝² : CommSemiring L
i : K →+* L
p : ℕ
inst✝¹ : ExpChar L p
inst✝ : PerfectRing L p
x : K
h✝ : x ∈ pNilradical K p
n : ℕ
h : x ^ p ^ n = 0
⊢ x ∈ ker i
-- Mathlib/Analysis/Convex/Basic.lean
theorem ite_eq_mem_stdSimplex (i : ι) : (if i = · then (1 : 𝕜) else 0) ∈ stdSimplex 𝕜 ι

Proof state:
𝕜 : Type u_1
ι : Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ (fun x => if i = x then 1 else 0) ∈ stdSimplex 𝕜 ι

Tactic:
simpa only [@eq_comm _ i, ← Pi.single_apply] using single_mem_stdSimplex 𝕜 i

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem Units.mk0_mul (x y : G₀) (hxy) :
    Units.mk0 (x * y) hxy =
      Units.mk0 x (mul_ne_zero_iff.mp hxy).1 * Units.mk0 y (mul_ne_zero_iff.mp hxy).2

Proof state:
case a
G₀ : Type u_3
inst✝ : GroupWithZero G₀
x y : G₀
hxy : x * y ≠ 0
⊢ ↑(mk0 (x * y) hxy) = ↑(mk0 x ⋯ * mk0 y ⋯)

Tactic:
rfl

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
x y : G₀
hxy : x * y ≠ 0
⊢ mk0 (x * y) hxy = mk0 x ⋯ * mk0 y ⋯

Tactic:
ext

Result:
case a
G₀ : Type u_3
inst✝ : GroupWithZero G₀
x y : G₀
hxy : x * y ≠ 0
⊢ ↑(mk0 (x * y) hxy) = ↑(mk0 x ⋯ * mk0 y ⋯)
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_eq_zero_or_eq_pi_iff_not_linearIndependent {x y : V} :
    o.oangle x y = 0 ∨ o.oangle x y = π ↔ ¬LinearIndependent ℝ ![x, y]

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle x y = 0 ∨ o.oangle x y = ↑π ↔ ¬LinearIndependent ℝ ![x, y]

Tactic:
rw [oangle_eq_zero_iff_sameRay, oangle_eq_pi_iff_sameRay_neg,
  sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent]

Result:
no goals
-- Mathlib/Analysis/Complex/Periodic.lean
theorem qParam_tendsto (hh : 0 < h) : Tendsto (qParam h) I∞ (𝓝[≠] 0)

Proof state:
h : ℝ
hh : 0 < h
⊢ Tendsto (𝕢 h) I∞ (𝓝[≠] 0)

Tactic:
refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_
  (.of_forall fun q ↦ exp_ne_zero _)

Result:
h : ℝ
hh : 0 < h
⊢ Tendsto (𝕢 h) I∞ (𝓝 0)

Proof state:
h : ℝ
hh : 0 < h
⊢ Tendsto (fun y => rexp (-2 * π * y / h)) atTop (𝓝 0)

Tactic:
refine Real.tendsto_exp_atBot.comp (.atBot_div_const hh (tendsto_id.const_mul_atTop_of_neg ?_))

Result:
h : ℝ
hh : 0 < h
⊢ -2 * π < 0

Proof state:
h : ℝ
hh : 0 < h
⊢ -2 * π < 0

Tactic:
simpa using Real.pi_pos

Result:
no goals

Proof state:
h : ℝ
hh : 0 < h
⊢ Tendsto (fun x => rexp (-2 * π * x.im / h)) I∞ (𝓝 0)

Tactic:
apply (tendsto_comap'_iff (m := fun y ↦ Real.exp (-2 * π * y / h)) (range_im ▸ univ_mem)).mpr

Result:
h : ℝ
hh : 0 < h
⊢ Tendsto (fun y => rexp (-2 * π * y / h)) atTop (𝓝 0)

Proof state:
h : ℝ
hh : 0 < h
⊢ Tendsto (fun x => ‖𝕢 h x‖) I∞ (𝓝 0)

Tactic:
simp only [norm_qParam]

Result:
h : ℝ
hh : 0 < h
⊢ Tendsto (fun x => rexp (-2 * π * x.im / h)) I∞ (𝓝 0)

Proof state:
h : ℝ
hh : 0 < h
⊢ Tendsto (𝕢 h) I∞ (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Result:
h : ℝ
hh : 0 < h
⊢ Tendsto (fun x => ‖𝕢 h x‖) I∞ (𝓝 0)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.add_const_right' (a b c : BitVec w) : (a + b) + c = (b + c) + a

Proof state:
w : Nat
a b c : BitVec w
⊢ a + b + c = b + c + a

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_neg_mul_emod_self {a b c : Int} : (a + -(b * c)) % c = a % c

Proof state:
a b c : Int
⊢ (a + -(b * c)) % c = a % c

Tactic:
rw [Int.neg_mul_eq_neg_mul, add_mul_emod_self]

Result:
no goals
-- Mathlib/Order/Filter/Cofinite.lean
theorem countable_compl_ker [l.IsCountablyGenerated] (h : cofinite ≤ l) : Set.Countable l.kerᶜ

Proof state:
case intro
α : Type u_2
l : Filter α
inst✝ : l.IsCountablyGenerated
h : cofinite ≤ l
s : ℕ → Set α
hs : l.HasAntitoneBasis s
⊢ l.kerᶜ.Countable

Tactic:
simp only [hs.ker, iInter_true, compl_iInter]

Result:
case intro
α : Type u_2
l : Filter α
inst✝ : l.IsCountablyGenerated
h : cofinite ≤ l
s : ℕ → Set α
hs : l.HasAntitoneBasis s
⊢ (⋃ i, (s i)ᶜ).Countable

Proof state:
α : Type u_2
l : Filter α
inst✝ : l.IsCountablyGenerated
h : cofinite ≤ l
⊢ l.kerᶜ.Countable

Tactic:
rcases exists_antitone_basis l with ⟨s, hs⟩

Result:
case intro
α : Type u_2
l : Filter α
inst✝ : l.IsCountablyGenerated
h : cofinite ≤ l
s : ℕ → Set α
hs : l.HasAntitoneBasis s
⊢ l.kerᶜ.Countable

Proof state:
case intro
α : Type u_2
l : Filter α
inst✝ : l.IsCountablyGenerated
h : cofinite ≤ l
s : ℕ → Set α
hs : l.HasAntitoneBasis s
⊢ (⋃ i, (s i)ᶜ).Countable

Tactic:
exact countable_iUnion fun n ↦ Set.Finite.countable <| h <| hs.mem _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_mapFinIdx {l : List α}
    {f : (i : Nat) → α → (h : i < l.length) → β}
    {g : (i : Nat) → β → (h : i < (l.mapFinIdx f).length) → γ} :
    (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i a h => g i (f i a h) (by simpa))

Proof state:
α : Type ?u.66761
β : Type ?u.66789
γ : Type ?u.66835
l : List α
f : (i : Nat) → α → i < l.length → β
g : (i : Nat) → β → i < (l.mapFinIdx f).length → γ
i : Nat
a : α
h : i < l.length
⊢ i < (l.mapFinIdx f).length

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
f : (i : Nat) → α → i < l.length → β
g : (i : Nat) → β → i < (l.mapFinIdx f).length → γ
⊢ (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx fun i a h => g i (f i a h) ⋯

Tactic:
simp [mapFinIdx_eq_iff]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/InjSurj.lean
theorem Function.Injective.isLeftCancelMulZero
    [IsLeftCancelMulZero M₀'] : IsLeftCancelMulZero M₀ where
  mul_left_cancel_of_ne_zero Hne He

Proof state:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
⊢ b✝ = c✝

Tactic:
have := congr_arg f He

Result:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
this : f (a✝ * b✝) = f (a✝ * c✝)
⊢ b✝ = c✝

Proof state:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
this : f a✝ * f b✝ = f a✝ * f c✝
⊢ b✝ = c✝

Tactic:
exact hf (mul_left_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)

Result:
no goals

Proof state:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
this : f a✝ * f b✝ = f a✝ * f c✝
Hfa : f a✝ = 0
⊢ f a✝ = f 0

Tactic:
rw [Hfa, zero]

Result:
no goals

Proof state:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
this : f (a✝ * b✝) = f (a✝ * c✝)
⊢ b✝ = c✝

Tactic:
rw [mul, mul] at this

Result:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
this : f a✝ * f b✝ = f a✝ * f c✝
⊢ b✝ = c✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mem_enum {x : α} {i : Nat} {xs : List α} (h : (i, x) ∈ xs.enum) :
    i < xs.length ∧ x = xs[i]'(fst_lt_of_mem_enum h) :=
  by simpa using mem_enumFrom h

Proof state:
α : Type u_1
x : α
i : Nat
xs : List α
h : (i, x) ∈ xs.enum
⊢ i < xs.length ∧ x = xs[i]

Tactic:
simpa using mem_enumFrom h

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem core_res (f : α → β) (s : Set α) (t : Set β) : (res f s).core t = sᶜ ∪ f ⁻¹' t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (res f s).core t = sᶜ ∪ f ⁻¹' t

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ (res f s).core t ↔ x ∈ sᶜ ∪ f ⁻¹' t

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ (res f s).core t ↔ x ∈ sᶜ ∪ f ⁻¹' t

Tactic:
rw [mem_core_res]

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t

Tactic:
by_cases h : x ∈ s <;> simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range'_inj : range' s n = range' s' n ↔ (n = 0 ∨ s = s')

Proof state:
s n s' : Nat
⊢ (range' s n).toArray = (range' s' n).toArray ↔ n = 0 ∨ s = s'

Tactic:
simp [List.range'_inj]

Result:
no goals

Proof state:
s n s' : Nat
⊢ range' s n = range' s' n ↔ n = 0 ∨ s = s'

Tactic:
rw [← toArray_inj]

Result:
s n s' : Nat
⊢ (range' s n).toArray = (range' s' n).toArray ↔ n = 0 ∨ s = s'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_reverse {x : α} {as : Vector α n} : x ∈ as.reverse ↔ x ∈ as

Proof state:
case mk
α : Type u_1
n : Nat
x : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse ↔
    x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
x : α
as : Vector α n
⊢ x ∈ as.reverse ↔ x ∈ as

Tactic:
cases as

Result:
case mk
α : Type u_1
n : Nat
x : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse ↔
    x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_add_pi_div_two (x : ℝ) : cos (x + π / 2) = -sin x

Proof state:
x : ℝ
⊢ cos (x + π / 2) = -sin x

Tactic:
simp [cos_add]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem normal_iInf_normal {ι : Type*} {a : ι → Subgroup G}
    (norm : ∀ i : ι, (a i).Normal) : (iInf a).Normal

Proof state:
case conj_mem
G : Type u_1
inst✝ : Group G
ι : Type u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : ∀ (i : ι), g ∈ a i
h : G
⊢ ∀ (i : ι), h * g * h⁻¹ ∈ a i

Tactic:
intro i

Result:
case conj_mem
G : Type u_1
inst✝ : Group G
ι : Type u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : ∀ (i : ι), g ∈ a i
h : G
i : ι
⊢ h * g * h⁻¹ ∈ a i

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
⊢ (iInf a).Normal

Tactic:
constructor

Result:
case conj_mem
G : Type u_1
inst✝ : Group G
ι : Type u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
⊢ ∀ n ∈ iInf a, ∀ (g : G), g * n * g⁻¹ ∈ iInf a

Proof state:
case conj_mem
G : Type u_1
inst✝ : Group G
ι : Type u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
⊢ ∀ n ∈ iInf a, ∀ (g : G), g * n * g⁻¹ ∈ iInf a

Tactic:
intro g g_in_iInf h

Result:
case conj_mem
G : Type u_1
inst✝ : Group G
ι : Type u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : g ∈ iInf a
h : G
⊢ h * g * h⁻¹ ∈ iInf a

Proof state:
case conj_mem
G : Type u_1
inst✝ : Group G
ι : Type u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : ∀ (i : ι), g ∈ a i
h : G
i : ι
⊢ h * g * h⁻¹ ∈ a i

Tactic:
exact (norm i).conj_mem g (g_in_iInf i) h

Result:
no goals

Proof state:
case conj_mem
G : Type u_1
inst✝ : Group G
ι : Type u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : g ∈ iInf a
h : G
⊢ h * g * h⁻¹ ∈ iInf a

Tactic:
rw [Subgroup.mem_iInf] at g_in_iInf ⊢

Result:
case conj_mem
G : Type u_1
inst✝ : Group G
ι : Type u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : ∀ (i : ι), g ∈ a i
h : G
⊢ ∀ (i : ι), h * g * h⁻¹ ∈ a i
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_left_midpoint (p₁ p₂ : P) : dist p₁ (midpoint 𝕜 p₁ p₂) = ‖(2 : 𝕜)‖⁻¹ * dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ : P
⊢ dist p₁ (midpoint 𝕜 p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
rw [midpoint, dist_comm, dist_lineMap_left, invOf_eq_inv, ← norm_inv]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem psum_zero : psum σ R 0 = Fintype.card σ

Proof state:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ psum σ R 0 = ↑(Fintype.card σ)

Tactic:
simp [psum]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompNotation.lean
@[simp]
lemma comp_apply_univ [IsMarkovKernel κ] : (κ ∘ₘ μ) Set.univ = μ Set.univ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ (⇑κ ∘ₘ μ) Set.univ = μ Set.univ

Tactic:
simp [bind_apply .univ κ.measurable]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
@[reassoc]
lemma associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε}
    (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
    ((f₁ ⊗ f₂) ⊗ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ f₂ ⊗ f₃)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
h₁ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).obj Y₂).map f₃ ≫
      (((associator L W ε).hom.app Y₁).app Y₂).app Y₃ =
    (((associator L W ε).hom.app Y₁).app Y₂).app X₃ ≫
      (((bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).obj Y₂).map f₃
⊢ ((f₁ ⊗ f₂) ⊗ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ f₂ ⊗ f₃)

Tactic:
have h₂ := NatTrans.congr_app (((associator L W ε).hom.app Y₁).naturality f₂) X₃

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
h₁ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).obj Y₂).map f₃ ≫
      (((associator L W ε).hom.app Y₁).app Y₂).app Y₃ =
    (((associator L W ε).hom.app Y₁).app Y₂).app X₃ ≫
      (((bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).obj Y₂).map f₃
h₂ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).map f₂ ≫
          ((associator L W ε).hom.app Y₁).app Y₂).app
      X₃ =
    (((associator L W ε).hom.app Y₁).app X₂ ≫
          ((bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).map f₂).app
      X₃
⊢ ((f₁ ⊗ f₂) ⊗ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ f₂ ⊗ f₃)
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem index_elim {K V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) :
    ∃ t : Finset G, (K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V) ∧ Finset.card t = index K V

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
this :
  sInf (Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}) ∈
    Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
⊢ ∃ t, K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V ∧ t.card = index K V

Tactic:
rwa [mem_image] at this

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
⊢ ∃ t, K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V ∧ t.card = index K V

Tactic:
have := Nat.sInf_mem (index_defined hK hV)

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
this :
  sInf (Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}) ∈
    Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
⊢ ∃ t, K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V ∧ t.card = index K V
-- Mathlib/Data/Int/ModEq.lean
theorem existsUnique_equiv (a : ℤ) {b : ℤ} (hb : 0 < b) :
    ∃ z : ℤ, 0 ≤ z ∧ z < b ∧ z ≡ a [ZMOD b] :=
  ⟨a % b, emod_nonneg _ (ne_of_gt hb),
    by
      have : a % b < |b| := emod_lt _ (ne_of_gt hb)
      rwa [abs_of_pos hb] at this, by simp [ModEq]⟩

Proof state:
a b : ℤ
hb : 0 < b
⊢ a % b < b

Tactic:
have : a % b < |b| := emod_lt _ (ne_of_gt hb)

Result:
a b : ℤ
hb : 0 < b
this : a % b < |b|
⊢ a % b < b

Proof state:
a b : ℤ
hb : 0 < b
this : a % b < |b|
⊢ a % b < b

Tactic:
rwa [abs_of_pos hb] at this

Result:
no goals

Proof state:
a b : ℤ
hb : 0 < b
⊢ a % b ≡ a [ZMOD b]

Tactic:
simp [ModEq]

Result:
no goals
-- Mathlib/Topology/Algebra/Support.lean
theorem mulTSupport_eq_empty_iff {f : X → α} : mulTSupport f = ∅ ↔ f = 1

Proof state:
X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
f : X → α
⊢ mulTSupport f = ∅ ↔ f = 1

Tactic:
rw [mulTSupport, closure_empty_iff, mulSupport_eq_empty_iff]

Result:
no goals
-- Mathlib/Data/ENNReal/Action.lean
lemma nnreal_smul_lt_top {x : ℝ≥0} {y : ℝ≥0∞} (hy : y < ⊤) : x • y < ⊤ := mul_lt_top (by simp) hy

Proof state:
x : ℝ≥0
y : ℝ≥0∞
hy : y < ⊤
⊢ ↑ofNNRealHom.toMonoidWithZeroHom x < ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
@[simp] lemma cliqueNum_compl : Gᶜ.cliqueNum = G.indepNum

Proof state:
α : Type u_3
G : SimpleGraph α
⊢ Gᶜ.cliqueNum = G.indepNum

Tactic:
simp [indepNum, cliqueNum]

Result:
no goals