harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Quiver/Prefunctor.lean
theorem homOfEq_map {U V : Type*} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} (f : X ⟶ Y)
    {X' Y' : U} (hX : X = X') (hY : Y = Y') :
    F.map (Quiver.homOfEq f hX hY) =
      Quiver.homOfEq (F.map f) (congr_arg F.obj hX) (congr_arg F.obj hY)

Proof state:
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f : X ⟶ Y
X' Y' : U
hX : X = X'
hY : Y = Y'
⊢ F.map (Quiver.homOfEq f hX hY) = Quiver.homOfEq (F.map f) ⋯ ⋯

Tactic:
subst hX hY

Result:
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f : X ⟶ Y
⊢ F.map (Quiver.homOfEq f ⋯ ⋯) = Quiver.homOfEq (F.map f) ⋯ ⋯

Proof state:
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f : X ⟶ Y
⊢ F.map (Quiver.homOfEq f ⋯ ⋯) = Quiver.homOfEq (F.map f) ⋯ ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem neg_rotation (θ : Real.Angle) (x : V) : -o.rotation θ x = o.rotation (π + θ) x

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ -(o.rotation θ) x = (o.rotation (↑π + θ)) x

Tactic:
rw [← o.rotation_pi_apply, rotation_rotation]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_comp_succAbove (i : Fin (n + 1)) (x : β) (p : Fin n → β) :
    insertNth i x p ∘ i.succAbove = p :=
  funext (by unfold comp; exact insertNth_apply_succAbove i _ _)

Proof state:
n : ℕ
β : Sort u_2
i : Fin (n + 1)
x : β
p : Fin n → β
⊢ ∀ (x_1 : Fin n), i.insertNth x p (i.succAbove x_1) = p x_1

Tactic:
exact insertNth_apply_succAbove i _ _

Result:
no goals

Proof state:
n : ℕ
β : Sort u_2
i : Fin (n + 1)
x : β
p : Fin n → β
⊢ ∀ (x_1 : Fin n), (i.insertNth x p ∘ i.succAbove) x_1 = p x_1

Tactic:
unfold comp

Result:
n : ℕ
β : Sort u_2
i : Fin (n + 1)
x : β
p : Fin n → β
⊢ ∀ (x_1 : Fin n), i.insertNth x p (i.succAbove x_1) = p x_1
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Univ.lean
@[simp]
lemma univ_coeff_card : (univ R n).coeff (Fintype.card n) = 1

Proof state:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
this : (univ ℤ n).coeff (Fintype.card n) = 1
⊢ (univ R n).coeff (Fintype.card n) = 1

Tactic:
rw [← univ_map_map n (Int.castRingHom R), Polynomial.coeff_map, this, _root_.map_one]

Result:
no goals

Proof state:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ (univ R n).coeff (Fintype.card n) = 1

Tactic:
suffices Polynomial.coeff (univ ℤ n) (Fintype.card n) = 1 by
  rw [← univ_map_map n (Int.castRingHom R), Polynomial.coeff_map, this, _root_.map_one]

Result:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ (univ ℤ n).coeff (Fintype.card n) = 1

Proof state:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ (univ ℤ n).coeff (Fintype.card n) = 1

Tactic:
rw [← univ_natDegree ℤ n]

Result:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ (univ ℤ n).coeff (univ ℤ n).natDegree = 1

Proof state:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ (univ ℤ n).coeff (univ ℤ n).natDegree = 1

Tactic:
exact (univ_monic ℤ n).leadingCoeff

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Spaces.lean
theorem pretopology_toGrothendieck :
    Pretopology.toGrothendieck _ (Opens.pretopology T) = Opens.grothendieckTopology T

Proof state:
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.toGrothendieck (Opens T) (pretopology T) = grothendieckTopology T

Tactic:
rw [← pretopology_ofGrothendieck]

Result:
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.toGrothendieck (Opens T) (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)) =
    grothendieckTopology T

Proof state:
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.toGrothendieck (Opens T) (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)) =
    grothendieckTopology T

Tactic:
apply (Pretopology.gi (Opens T)).l_u_eq

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem interior_setOf_im_le (a : ℝ) : interior { z : ℂ | z.im ≤ a } = { z | z.im < a }

Proof state:
a : ℝ
⊢ interior {z | z.im ≤ a} = {z | z.im < a}

Tactic:
simpa only [interior_Iic] using interior_preimage_im (Iic a)

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem IsSt.st_eq {x : ℝ*} {r : ℝ} (hxr : IsSt x r) : st x = r

Proof state:
x : ℝ*
r : ℝ
hxr : x.IsSt r
h : ∃ r, x.IsSt r
⊢ Classical.choose h = r

Tactic:
exact (Classical.choose_spec h).unique hxr

Result:
no goals

Proof state:
x : ℝ*
r : ℝ
hxr : x.IsSt r
h : ∃ r, x.IsSt r
⊢ x.st = r

Tactic:
rw [st, dif_pos h]

Result:
x : ℝ*
r : ℝ
hxr : x.IsSt r
h : ∃ r, x.IsSt r
⊢ Classical.choose h = r

Proof state:
x : ℝ*
r : ℝ
hxr : x.IsSt r
⊢ x.st = r

Tactic:
have h : ∃ r, IsSt x r := ⟨r, hxr⟩

Result:
x : ℝ*
r : ℝ
hxr : x.IsSt r
h : ∃ r, x.IsSt r
⊢ x.st = r
-- Mathlib/GroupTheory/Index.lean
theorem relindex_inf_ne_zero (hH : H.relindex L ≠ 0) (hK : K.relindex L ≠ 0) :
    (H ⊓ K).relindex L ≠ 0

Proof state:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : H.relindex L ≠ 0
hK : K.relindex L ≠ 0
⊢ (H ⊓ K).relindex L ≠ 0

Tactic:
replace hH : H.relindex (K ⊓ L) ≠ 0 := mt (relindex_eq_zero_of_le_right inf_le_right) hH

Result:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : K.relindex L ≠ 0
hH : H.relindex (K ⊓ L) ≠ 0
⊢ (H ⊓ K).relindex L ≠ 0

Proof state:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : (K ⊓ L).relindex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relindex (K ⊓ L) ≠ 0
⊢ (H ⊓ (K ⊓ L)).relindex L ≠ 0

Tactic:
exact relindex_ne_zero_trans hH hK

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : (K ⊓ L).relindex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relindex (K ⊓ L) ≠ 0
⊢ (H ⊓ K ⊓ L).relindex L ≠ 0

Tactic:
rw [inf_assoc]

Result:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : (K ⊓ L).relindex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relindex (K ⊓ L) ≠ 0
⊢ (H ⊓ (K ⊓ L)).relindex L ≠ 0

Proof state:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : K.relindex L ≠ 0
hH : H.relindex (K ⊓ L) ≠ 0
⊢ (H ⊓ K).relindex L ≠ 0

Tactic:
rw [← inf_relindex_right] at hH hK ⊢

Result:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : (K ⊓ L).relindex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relindex (K ⊓ L) ≠ 0
⊢ (H ⊓ K ⊓ L).relindex L ≠ 0
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.map_comp_id {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryCoproduct Z W]
    [HasBinaryCoproduct Y W] [HasBinaryCoproduct X W] :
    coprod.map (f ≫ g) (𝟙 W) = coprod.map f (𝟙 W) ≫ coprod.map g (𝟙 W)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasBinaryCoproduct Z W
inst✝¹ : HasBinaryCoproduct Y W
inst✝ : HasBinaryCoproduct X W
⊢ map (f ≫ g) (𝟙 W) = map f (𝟙 W) ≫ map g (𝟙 W)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/IntermediateValue.lean
theorem IsClosed.Icc_subset_of_forall_mem_nhdsWithin {a b : α} {s : Set α}
    (hs : IsClosed (s ∩ Icc a b)) (ha : a ∈ s) (hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x) :
    Icc a b ⊆ s

Proof state:
case intro
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x
x : α
hxs : x ∈ s
hxab : x ∈ Ico a b
y : α
hyxb : y ∈ Ioi x
this : s ∩ Ioc x y ∈ 𝓝[>] x
⊢ (s ∩ Ioc x y).Nonempty

Tactic:
exact (nhdsGT_neBot_of_exists_gt ⟨b, hxab.2⟩).nonempty_of_mem this

Result:
no goals

Proof state:
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x
⊢ Icc a b ⊆ s

Tactic:
apply hs.Icc_subset_of_forall_exists_gt ha

Result:
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x
⊢ ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty

Proof state:
case intro
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x
x : α
hxs : x ∈ s
hxab : x ∈ Ico a b
y : α
hyxb : y ∈ Ioi x
⊢ (s ∩ Ioc x y).Nonempty

Tactic:
have : s ∩ Ioc x y ∈ 𝓝[>] x := inter_mem (hgt x ⟨hxs, hxab⟩) (Ioc_mem_nhdsGT hyxb)

Result:
case intro
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x
x : α
hxs : x ∈ s
hxab : x ∈ Ico a b
y : α
hyxb : y ∈ Ioi x
this : s ∩ Ioc x y ∈ 𝓝[>] x
⊢ (s ∩ Ioc x y).Nonempty

Proof state:
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x
⊢ ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty

Tactic:
rintro x ⟨hxs, hxab⟩ y hyxb

Result:
case intro
α : Type u
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x
x : α
hxs : x ∈ s
hxab : x ∈ Ico a b
y : α
hyxb : y ∈ Ioi x
⊢ (s ∩ Ioc x y).Nonempty
-- Mathlib/Order/PiLex.lean
theorem toLex_monotone : Monotone (@toLex (∀ i, β i)) := fun a b h =>
  or_iff_not_imp_left.2 fun hne =>
    let ⟨i, hi, hl⟩ := IsWellFounded.wf.has_min (r := (· < ·)) { i | a i ≠ b i }
      (Function.ne_iff.1 hne)
    ⟨i, fun j hj => by
      contrapose! hl
      exact ⟨j, hl, hj⟩, (h i).lt_of_ne hi⟩

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
a b : (i : ι) → β i
h : a ≤ b
hne : ¬toLex a = toLex b
i : ι
hi : i ∈ {i | a i ≠ b i}
hl : ∀ x ∈ {i | a i ≠ b i}, ¬x < i
j : ι
hj : (fun x1 x2 => x1 < x2) j i
⊢ toLex a j = toLex b j

Tactic:
contrapose! hl

Result:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
a b : (i : ι) → β i
h : a ≤ b
hne : ¬toLex a = toLex b
i : ι
hi : i ∈ {i | a i ≠ b i}
j : ι
hj : (fun x1 x2 => x1 < x2) j i
hl : toLex a j ≠ toLex b j
⊢ ∃ x ∈ {i | a i ≠ b i}, x < i

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
a b : (i : ι) → β i
h : a ≤ b
hne : ¬toLex a = toLex b
i : ι
hi : i ∈ {i | a i ≠ b i}
j : ι
hj : (fun x1 x2 => x1 < x2) j i
hl : toLex a j ≠ toLex b j
⊢ ∃ x ∈ {i | a i ≠ b i}, x < i

Tactic:
exact ⟨j, hl, hj⟩

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean
theorem quadratic_reciprocity_three_mod_four (hp : p % 4 = 3) (hq : q % 4 = 3) :
    legendreSym q p = -legendreSym p q

Proof state:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ legendreSym q ↑p = -legendreSym p ↑q

Tactic:
rw [quadratic_reciprocity', pow_mul, nop hp, nop hq, neg_one_mul] <;>
rwa [← Prime.mod_two_eq_one_iff_ne_two, odd_of_mod_four_eq_three]

Result:
no goals

Proof state:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
⊢ legendreSym q ↑p = -legendreSym p ↑q

Tactic:
let nop := @neg_one_pow_div_two_of_three_mod_four

Result:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ legendreSym q ↑p = -legendreSym p ↑q
-- Mathlib/Order/Filter/AtTopBot/Defs.lean
lemma atTop_eq_generate_of_not_bddAbove [LinearOrder α] {s : Set α} (hs : ¬ BddAbove s) :
    (atTop : Filter α) = generate (Ici '' s)

Proof state:
case intro.intro
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ¬BddAbove s
x y : α
hy : y ∈ s
hy' : x < y
⊢ ∃ y ∈ s, x ≤ y

Tactic:
exact ⟨y, hy, hy'.le⟩

Result:
no goals

Proof state:
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ¬BddAbove s
x : α
⊢ ∃ y ∈ s, x ≤ y

Tactic:
obtain ⟨y, hy, hy'⟩ := not_bddAbove_iff.mp hs x

Result:
case intro.intro
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ¬BddAbove s
x y : α
hy : y ∈ s
hy' : x < y
⊢ ∃ y ∈ s, x ≤ y

Proof state:
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ atTop = generate (Ici '' s)

Tactic:
refine atTop_eq_generate_of_forall_exists_le fun x ↦ ?_

Result:
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ¬BddAbove s
x : α
⊢ ∃ y ∈ s, x ≤ y
-- Mathlib/Probability/Kernel/Composition/Prod.lean
lemma prod_const (μ : Measure β) [SFinite μ] (ν : Measure γ) [SFinite ν] :
    const α μ ×ₖ const α ν = const α (μ.prod ν)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure β
inst✝¹ : SFinite μ
ν : Measure γ
inst✝ : SFinite ν
⊢ const α μ ×ₖ const α ν = const α (μ.prod ν)

Tactic:
ext x

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure β
inst✝¹ : SFinite μ
ν : Measure γ
inst✝ : SFinite ν
x : α
s✝ : Set (β × γ)
a✝ : MeasurableSet s✝
⊢ ((const α μ ×ₖ const α ν) x) s✝ = ((const α (μ.prod ν)) x) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure β
inst✝¹ : SFinite μ
ν : Measure γ
inst✝ : SFinite ν
x : α
s✝ : Set (β × γ)
a✝ : MeasurableSet s✝
⊢ ((const α μ ×ₖ const α ν) x) s✝ = ((const α (μ.prod ν)) x) s✝

Tactic:
rw [const_apply, prod_apply, const_apply, const_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
    (m.erase k).1.isEmpty = (m.1.isEmpty || (m.1.size == 1 && m.contains k))

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
⊢ (m.erase k).val.isEmpty = (m.val.isEmpty || m.val.size == 1 && m.contains k)

Tactic:
simp_to_model [erase] using List.isEmpty_eraseKey

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem inner_map_map_iff_adjoint_comp_self (u : H →L[𝕜] K) :
    (∀ x y : H, ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜) ↔ adjoint u ∘L u = 1

Proof state:
case refine_1
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
u : H →L[𝕜] K
h : ∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜
x : H
⊢ ((adjoint u).comp u) x = 1 x

Tactic:
refine ext_inner_right 𝕜 fun y ↦ ?_

Result:
case refine_1
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
u : H →L[𝕜] K
h : ∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜
x y : H
⊢ ⟪((adjoint u).comp u) x, y⟫_𝕜 = ⟪1 x, y⟫_𝕜

Proof state:
case refine_1
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
u : H →L[𝕜] K
h : ∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜
x y : H
⊢ ⟪((adjoint u).comp u) x, y⟫_𝕜 = ⟪1 x, y⟫_𝕜

Tactic:
simpa [star_eq_adjoint, adjoint_inner_left] using h x y

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
u : H →L[𝕜] K
h : (adjoint u).comp u = 1
⊢ ∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜

Tactic:
simp [← adjoint_inner_left, ← comp_apply, h]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
u : H →L[𝕜] K
⊢ (∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜) ↔ (adjoint u).comp u = 1

Tactic:
refine ⟨fun h ↦ ext fun x ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
u : H →L[𝕜] K
h : ∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜
x : H
⊢ ((adjoint u).comp u) x = 1 x

case refine_2
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
u : H →L[𝕜] K
h : (adjoint u).comp u = 1
⊢ ∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem leftUnitor_comp_inv (f : a ⟶ b) (g : b ⟶ c) :
    (λ_ (f ≫ g)).inv = (λ_ f).inv ▷ g ≫ (α_ (𝟙 a) f g).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ (f ≫ g)).inv = (λ_ f).inv ▷ g ≫ (α_ (𝟙 a) f g).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem map_natDegree_eq_natDegree {S F : Type*} [Semiring S]
    [FunLike F R[X] S[X]] [AddMonoidHomClass F R[X] S[X]]
    {φ : F} (p) (φ_mon_nat : ∀ n c, c ≠ 0 → (φ (monomial n c)).natDegree = n) :
    (φ p).natDegree = p.natDegree :=
  (map_natDegree_eq_sub (fun _ h => (Nat.not_lt_zero _ h).elim) (by simpa)).trans
    p.natDegree.sub_zero

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = n
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = n - 0

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_const {c : M} (hc : c ≠ 1) : (mulSupport fun _ : α => c) = Set.univ

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : One M
c : M
hc : c ≠ 1
x : α
⊢ (x ∈ mulSupport fun x => c) ↔ x ∈ univ

Tactic:
simp [hc]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : One M
c : M
hc : c ≠ 1
⊢ (mulSupport fun x => c) = univ

Tactic:
ext x

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : One M
c : M
hc : c ≠ 1
x : α
⊢ (x ∈ mulSupport fun x => c) ↔ x ∈ univ
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem mem_inv_smul_set_iff : x ∈ a⁻¹ • A ↔ a • x ∈ A

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A : Set β
a : α
x : β
⊢ x ∈ a⁻¹ • A ↔ a • x ∈ A

Tactic:
simp only [← image_smul, mem_image, inv_smul_eq_iff, exists_eq_right]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
lemma fst_sum {ι : Type*} (μ : ι → Measure (α × β)) : (sum μ).fst = sum (fun n ↦ (μ n).fst)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
s : Set α
hs : MeasurableSet s
⊢ ∑' (i : ι), (μ i) (Prod.fst ⁻¹' s) = ∑' (i : ι), (μ i).fst s

Tactic:
simp_rw [fst_apply hs]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
s : Set α
hs : MeasurableSet s
⊢ (sum μ).fst s = (sum fun n => (μ n).fst) s

Tactic:
rw [fst_apply hs, sum_apply, sum_apply _ hs]

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
s : Set α
hs : MeasurableSet s
⊢ ∑' (i : ι), (μ i) (Prod.fst ⁻¹' s) = ∑' (i : ι), (μ i).fst s

case h.hs
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (Prod.fst ⁻¹' s)

Proof state:
case h.hs
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (Prod.fst ⁻¹' s)

Tactic:
exact measurable_fst hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
⊢ (sum μ).fst = sum fun n => (μ n).fst

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
s : Set α
hs : MeasurableSet s
⊢ (sum μ).fst s = (sum fun n => (μ n).fst) s
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem card_edgeFinset_induce_of_support_subset (h : G.support ⊆ s) :
    #(G.induce s).edgeFinset = #G.edgeFinset

Proof state:
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.support ⊆ s
⊢ #(induce s G).edgeFinset = #G.edgeFinset

Tactic:
rw [← map_edgeFinset_induce_of_support_subset h, card_map]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
protected lemma Monotone.iInf (hf : ∀ i, Monotone (f i)) : Monotone (⨅ i, f i) :=
  Monotone.sInf (by simpa)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), Monotone (f i)
⊢ ∀ f_1 ∈ range fun i => f i, Monotone f_1

Tactic:
simpa

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem Filter.HasBasis.biInter_biUnion_ball {p : ι → Prop} {U : ι → Set (α × α)}
    (h : HasBasis (𝓤 α) p U) (s : Set α) :
    (⋂ (i) (_ : p i), ⋃ x ∈ s, ball x (U i)) = closure s

Proof state:
case h
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
U : ι → Set (α × α)
h : (𝓤 α).HasBasis p U
s : Set α
x : α
⊢ x ∈ ⋂ i, ⋂ (_ : p i), ⋃ x ∈ s, ball x (U i) ↔ x ∈ closure s

Tactic:
simp [mem_closure_iff_nhds_basis (nhds_basis_uniformity h), ball]

Result:
no goals

Proof state:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
U : ι → Set (α × α)
h : (𝓤 α).HasBasis p U
s : Set α
⊢ ⋂ i, ⋂ (_ : p i), ⋃ x ∈ s, ball x (U i) = closure s

Tactic:
ext x

Result:
case h
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
U : ι → Set (α × α)
h : (𝓤 α).HasBasis p U
s : Set α
x : α
⊢ x ∈ ⋂ i, ⋂ (_ : p i), ⋃ x ∈ s, ball x (U i) ↔ x ∈ closure s