harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullbackDiagonalMapIdIso_inv_snd_fst :
    (pullbackDiagonalMapIdIso f g i).inv ≫ pullback.snd _ _ ≫ pullback.fst _ _ =
      pullback.fst _ _

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).inv ≫
      snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i) =
    fst f g

Tactic:
rw [Iso.inv_comp_eq]

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i) =
    (pullbackDiagonalMapIdIso f g i).hom ≫ fst f g

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i) =
    (pullbackDiagonalMapIdIso f g i).hom ≫ fst f g

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem concat_append {u v w x : V} (p : G.Walk u v) (h : G.Adj v w) (q : G.Walk w x) :
    (p.concat h).append q = p.append (cons h q)

Proof state:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
h : G.Adj v w
q : G.Walk w x
⊢ (p.concat h).append q = p.append (cons h q)

Tactic:
rw [concat_eq_append, ← append_assoc, cons_nil_append]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem midpoint_vsub (p₁ p₂ p : P) :
    midpoint R p₁ p₂ -ᵥ p = (⅟ 2 : 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₂ -ᵥ p = ⅟2 • (p₁ -ᵥ p) + ⅟2 • (p₂ -ᵥ p)

Tactic:
rw [← vsub_sub_vsub_cancel_right p₁ p p₂, smul_sub, sub_eq_add_neg, ← smul_neg,
  neg_vsub_eq_vsub_rev, add_assoc, invOf_two_smul_add_invOf_two_smul, ← vadd_vsub_assoc,
  midpoint_comm, midpoint, lineMap_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Basic.lean
theorem submodule_eq (v : ℙ K V) : v.submodule = K ∙ v.rep

Proof state:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ (mk K v.rep ⋯).submodule = Submodule.span K {v.rep}

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ v.submodule = Submodule.span K {v.rep}

Tactic:
conv_lhs => rw [← v.mk_rep]

Result:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ (mk K v.rep ⋯).submodule = Submodule.span K {v.rep}
-- Mathlib/Computability/TMConfig.lean
theorem head_eval (v) : head.eval v = pure [v.headI]

Proof state:
v : List ℕ
⊢ head.eval v = pure [v.headI]

Tactic:
simp [head]

Result:
no goals
-- Mathlib/GroupTheory/Torsion.lean
lemma isTorsionFree_iff_noZeroSMulDivisors_int [AddGroup G] :
    IsTorsionFree G ↔ NoZeroSMulDivisors ℤ G

Proof state:
G : Type u_1
inst✝ : AddGroup G
⊢ IsTorsionFree G ↔ NoZeroSMulDivisors ℤ G

Tactic:
simp_rw [AddMonoid.IsTorsionFree, isOfFinAddOrder_iff_zsmul_eq_zero, not_exists, not_and,
  noZeroSMulDivisors_iff, forall_swap (β := ℤ)]

Result:
G : Type u_1
inst✝ : AddGroup G
⊢ (∀ (y : ℤ) (x : G), x ≠ 0 → y ≠ 0 → ¬y • x = 0) ↔ ∀ {c : ℤ} {x : G}, c • x = 0 → c = 0 ∨ x = 0

Proof state:
G : Type u_1
inst✝ : AddGroup G
⊢ (∀ (y : ℤ) (x : G), x ≠ 0 → y ≠ 0 → ¬y • x = 0) ↔ ∀ {c : ℤ} {x : G}, c • x = 0 → c = 0 ∨ x = 0

Tactic:
exact forall₂_congr fun _ _ ↦ by tauto

Result:
no goals

Proof state:
G : Type u_1
inst✝ : AddGroup G
x✝¹ : ℤ
x✝ : G
⊢ x✝ ≠ 0 → x✝¹ ≠ 0 → ¬x✝¹ • x✝ = 0 ↔ x✝¹ • x✝ = 0 → x✝¹ = 0 ∨ x✝ = 0

Tactic:
tauto

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem HasLimit.isoOfEquivalence_hom_π {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit G]
    (e : J ≌ K) (w : e.functor ⋙ G ≅ F) (k : K) :
    (HasLimit.isoOfEquivalence e w).hom ≫ limit.π G k =
      limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ limit.lift G
        ((Cones.postcompose (whiskerLeft e.inverse w.inv ≫ (e.invFunIdAssoc G).hom)).obj
          (Cone.whisker e.inverse (limit.cone F))) ≫
      limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k)

Tactic:
simp

Result:
no goals

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ (isoOfEquivalence e w).hom ≫ limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k)

Tactic:
simp only [HasLimit.isoOfEquivalence, IsLimit.conePointsIsoOfEquivalence_hom]

Result:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ (limit.isLimit G).lift
        ((Cones.equivalenceOfReindexing e.symm ((isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G)).functor.obj
          (limit.cone F)) ≫
      limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ (limit.isLimit G).lift
        ((Cones.equivalenceOfReindexing e.symm ((isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G)).functor.obj
          (limit.cone F)) ≫
      limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k)

Tactic:
dsimp

Result:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ limit.lift G
        ((Cones.postcompose (whiskerLeft e.inverse w.inv ≫ (e.invFunIdAssoc G).hom)).obj
          (Cone.whisker e.inverse (limit.cone F))) ≫
      limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k)
-- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
theorem polarBilin_pi (Q : ∀ i, QuadraticMap R (Mᵢ i) P) :
    (pi Q).polarBilin = ∑ i, (Q i).polarBilin.compl₁₂ (.proj i) (.proj i) :=
  LinearMap.ext₂ fun x y => (polar_pi _ _ _).trans <| by simp

Proof state:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝³ : AddCommGroup P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
x y : (i : ι) → Mᵢ i
⊢ ∑ i : ι, polar (⇑(Q i)) (x i) (y i) =
    ((∑ i : ι, LinearMap.compl₁₂ (Q i).polarBilin (LinearMap.proj i) (LinearMap.proj i)) x) y

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma disjoint_sUnion_disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C)
    (hI : ↑I ⊆ C) :
    Disjoint (⋃₀ (I : Set (Set α))) (⋃₀ hC.disjointOfDiffUnion hs hI)

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ Disjoint (⋃₀ ↑I) (⋃₀ ↑(hC.disjointOfDiffUnion hs hI))

Tactic:
rw [← hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ Disjoint (⋃₀ ↑I) (s \ ⋃₀ ↑I)

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ Disjoint (⋃₀ ↑I) (s \ ⋃₀ ↑I)

Tactic:
exact Set.disjoint_sdiff_right

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_neg_Ioi : Neg.neg '' Ioi a = Iio (-a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a : α
⊢ Neg.neg '' Ioi a = Iio (-a)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem map_ext' {f g : AdicCompletion I M →ₗ[AdicCompletion I R] T}
    (h : ∀ (a : AdicCauchySequence I M),
      f (AdicCompletion.mk I M a) = g (AdicCompletion.mk I M a)) :
    f = g

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f g : AdicCompletion I M →ₗ[AdicCompletion I R] T
h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)
x : AdicCompletion I M
⊢ f x = g x

Tactic:
apply induction_on I M x h

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f g : AdicCompletion I M →ₗ[AdicCompletion I R] T
h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)
⊢ f = g

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f g : AdicCompletion I M →ₗ[AdicCompletion I R] T
h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)
x : AdicCompletion I M
⊢ f x = g x
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem isOfFinOrder_inv_iff {x : G} : IsOfFinOrder x⁻¹ ↔ IsOfFinOrder x

Proof state:
G : Type u_1
inst✝ : Group G
x : G
⊢ IsOfFinOrder x⁻¹ ↔ IsOfFinOrder x

Tactic:
simp [isOfFinOrder_iff_pow_eq_one]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_add_const_uIcc : (fun x => x + a) '' [[b, c]] = [[b + a, c + a]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) '' [[b, c]] = [[b + a, c + a]]

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
lemma eq_disjSum_iff : u = s.disjSum t ↔ u.toLeft = s ∧ u.toRight = t :=
  ⟨fun h => by simp [h], fun h => by simp [← h, toLeft_disjSum_toRight]⟩

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : u.toLeft = s ∧ u.toRight = t
⊢ u = s.disjSum t

Tactic:
simp [← h, toLeft_disjSum_toRight]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : u = s.disjSum t
⊢ u.toLeft = s ∧ u.toRight = t

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem lintegral_swapRight (κ : Kernel α (β × γ)) (a : α) {g : γ × β → ℝ≥0∞} (hg : Measurable g) :
    ∫⁻ c, g c ∂swapRight κ a = ∫⁻ bc : β × γ, g bc.swap ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
g : γ × β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : γ × β), g c ∂κ.swapRight a = ∫⁻ (bc : β × γ), g bc.swap ∂κ a

Tactic:
rw [swapRight_eq, lintegral_map _ measurable_swap a hg]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_eq_restrict_biUnion_iff (s : ι → Set α) {t : Set ι} (ht : t.Countable) (f g : α → δ) :
    f =ᵐ[μ.restrict (⋃ i ∈ t, s i)] g ↔ ∀ i ∈ t, f =ᵐ[μ.restrict (s i)] g

Proof state:
α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
f g : α → δ
⊢ f =ᶠ[ae (μ.restrict (⋃ i ∈ t, s i))] g ↔ ∀ i ∈ t, f =ᶠ[ae (μ.restrict (s i))] g

Tactic:
simp_rw [ae_restrict_biUnion_eq s ht, EventuallyEq, eventually_iSup]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.trans_left_ne [NoZeroSMulDivisors R V] {w x y z : P} (h₁ : Wbtw R w y z)
    (h₂ : Wbtw R w x y) (h : y ≠ z) : x ≠ z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y : P
h₂ : Wbtw R w x y
h₁ : Wbtw R w y x
h : y ≠ x
⊢ False

Tactic:
exact h (h₁.swap_right_iff.1 h₂)

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y z : P
h₁ : Wbtw R w y z
h₂ : Wbtw R w x y
h : y ≠ z
⊢ x ≠ z

Tactic:
rintro rfl

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y : P
h₂ : Wbtw R w x y
h₁ : Wbtw R w y x
h : y ≠ x
⊢ False
-- Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean
theorem iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute (hA : A.IsSymmetric)
    (hB : B.IsSymmetric) (hAB : Commute A B) :
    (⨆ α, ⨆ γ, eigenspace A α ⊓ eigenspace B γ) = ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hA : A.IsSymmetric
hB : B.IsSymmetric
hAB : Commute A B
⊢ ⨆ α, ⨆ γ, eigenspace A α ⊓ eigenspace B γ = ⊤

Tactic:
simpa [iSup_eigenspace_inf_eigenspace_of_commute hB hAB] using
  Submodule.orthogonal_eq_bot_iff.mp <| hA.orthogonalComplement_iSup_eigenspaces_eq_bot

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.modify_eq [BEq α] [EquivBEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF) {k : α} {f : β → β} :
    Raw.Const.modify m k f = Raw₀.Const.modify ⟨m, h.size_buckets_pos⟩ k f

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Hashable α
m : Raw α fun x => β
h : m.WF
k : α
f : β → β
⊢ Raw.Const.modify m k f = (Raw₀.Const.modify ⟨m, ⋯⟩ k f).val

Tactic:
simp [Raw.Const.modify, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_eq_zero_symm {x y : E} : ⟪x, y⟫ = 0 ↔ ⟪y, x⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, y⟫_𝕜 = 0 ↔ ⟪y, x⟫_𝕜 = 0

Tactic:
rw [← inner_conj_symm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ (starRingEnd 𝕜) ⟪y, x⟫_𝕜 = 0 ↔ ⟪y, x⟫_𝕜 = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ (starRingEnd 𝕜) ⟪y, x⟫_𝕜 = 0 ↔ ⟪y, x⟫_𝕜 = 0

Tactic:
exact star_eq_zero

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem eq_mpr_bijective {α β : Sort _} (h : α = β) : Function.Bijective (Eq.mpr h)

Proof state:
α β : Sort u_3
h : α = β
⊢ Bijective h.mpr

Tactic:
cases h

Result:
case refl
α : Sort u_3
⊢ Bijective ⋯.mpr

Proof state:
case refl
α : Sort u_3
⊢ Bijective ⋯.mpr

Tactic:
exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Monadic.lean
theorem forIn'_yield_eq_pelim [Monad m] [LawfulMonad m] (o : Option α)
    (f : (a : α) → a ∈ o → β → m γ) (g : (a : α) → a ∈ o → β → γ → β) (b : β) :
    forIn' o b (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
      o.pelim (pure b) (fun a h => g a h b <$> f a h b)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
o : Option α
f : (a : α) → a ∈ o → β → m γ
g : (a : α) → a ∈ o → β → γ → β
b : β
⊢ (forIn' o b fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) =
    o.pelim (pure b) fun a h => g a h b <$> f a h b

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/RingHom.lean
theorem preimage_specComap_zeroLocus_aux (f : R →+* S) (s : Set R) :
    f.specComap ⁻¹' zeroLocus s = zeroLocus (f '' s)

Proof state:
case h
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
s : Set R
x : PrimeSpectrum S
⊢ x ∈ f.specComap ⁻¹' zeroLocus s ↔ x ∈ zeroLocus (⇑f '' s)

Tactic:
simp only [mem_zeroLocus, Set.image_subset_iff, Set.mem_preimage, mem_zeroLocus, Ideal.coe_comap]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
s : Set R
⊢ f.specComap ⁻¹' zeroLocus s = zeroLocus (⇑f '' s)

Tactic:
ext x

Result:
case h
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
s : Set R
x : PrimeSpectrum S
⊢ x ∈ f.specComap ⁻¹' zeroLocus s ↔ x ∈ zeroLocus (⇑f '' s)
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem apply_symm_apply_eq_coordChangeL (e e' : Trivialization F (π F E)) [e.IsLinear R]
    [e'.IsLinear R] {b : B} (hb : b ∈ e.baseSet ∩ e'.baseSet) (v : F) :
    e' (e.toPartialHomeomorph.symm (b, v)) = (b, e.coordChangeL R e' b v)

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ↑e' (↑e.symm (b, v)) = (b, (coordChangeL R e e' b) v)

Tactic:
rw [e.mk_coordChangeL e' hb, e.mk_symm hb.1]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem MemLp.integrable_sq {f : α → ℝ} (h : MemLp f 2 μ) : Integrable (fun x => f x ^ 2) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : MemLp f 2 μ
⊢ Integrable (fun x => f x ^ 2) μ

Tactic:
simpa [← memLp_one_iff_integrable] using h.norm_rpow two_ne_zero ENNReal.ofNat_ne_top

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Diam.lean
theorem diam_triple : diam ({x, y, z} : Set α) = max (max (edist x y) (edist x z)) (edist y z)

Proof state:
α : Type u_1
x y z : α
inst✝ : PseudoEMetricSpace α
⊢ diam {x, y, z} = edist x y ⊔ edist x z ⊔ edist y z

Tactic:
simp only [diam_insert, iSup_insert, iSup_singleton, diam_singleton, ENNReal.max_zero_right]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem toTopologicalSpace_sInf {s : Set (UniformSpace α)} :
    (sInf s).toTopologicalSpace = ⨅ i ∈ s, @UniformSpace.toTopologicalSpace α i

Proof state:
α : Type ua
s : Set (UniformSpace α)
⊢ toTopologicalSpace = ⨅ i ∈ s, toTopologicalSpace

Tactic:
simp only [← toTopologicalSpace_iInf]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem HasFDerivAt.fderiv (h : HasFDerivAt f f' x) : fderiv 𝕜 f x = f'

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
⊢ fderiv 𝕜 f x = f'

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
x✝ : E
⊢ (fderiv 𝕜 f x) x✝ = f' x✝

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
x✝ : E
⊢ (fderiv 𝕜 f x) x✝ = f' x✝

Tactic:
rw [h.unique h.differentiableAt.hasFDerivAt]

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
theorem xor_right_injective {n : ℕ} : Function.Injective (HXor.hXor n : ℕ → ℕ) := fun m m' h => by
  rw [← xor_cancel_left n m, ← xor_cancel_left n m', h]

Proof state:
n m m' : ℕ
h : n ^^^ m = n ^^^ m'
⊢ m = m'

Tactic:
rw [← xor_cancel_left n m, ← xor_cancel_left n m', h]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem self_sub_toIcoMod (a b : α) : b - toIcoMod hp a b = toIcoDiv hp a b • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIcoMod hp a b = toIcoDiv hp a b • p

Tactic:
rw [toIcoMod, sub_sub_cancel]

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem isRelPrime_mul_unit_right_left : IsRelPrime (y * x) z ↔ IsRelPrime y z

Proof state:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (y * x) z ↔ IsRelPrime y z

Tactic:
rw [mul_comm, isRelPrime_mul_unit_left_left hu]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem last_zero : (Fin.last 0 : Fin 1) = 0

Proof state:
case h

⊢ ↑(last 0) = ↑0

Tactic:
simp

Result:
no goals

Proof state:
⊢ last 0 = 0

Tactic:
ext

Result:
case h

⊢ ↑(last 0) = ↑0
-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.isOpen {s : Set α} {b : Set (Set α)}
    (hb : IsTopologicalBasis b) (hs : s ∈ b) : IsOpen s

Proof state:
α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
⊢ IsOpen s

Tactic:
exact .basic s hs

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem pushforward_le_bind_of_mem (S : Presieve X) (R : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → Sieve Y)
    (f : Y ⟶ X) (h : S f) : (R h).pushforward f ≤ bind S R

Proof state:
case intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
Z : C
g : Z ⟶ Y
hg : (R h).arrows g
⊢ (bind S R).arrows (g ≫ f)

Tactic:
exact ⟨_, g, f, h, hg, rfl⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ pushforward f (R h) ≤ bind S R

Tactic:
rintro Z _ ⟨g, rfl, hg⟩

Result:
case intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
Z : C
g : Z ⟶ Y
hg : (R h).arrows g
⊢ (bind S R).arrows (g ≫ f)
-- Mathlib/SetTheory/Game/Nim.lean
theorem moveRight_toRightMovesNim {o : Ordinal} (i) :
    (nim o).moveRight (toRightMovesNim i) = nim i

Proof state:
o : Ordinal.{u_1}
i : ↑(Set.Iio o)
⊢ (nim o).moveRight (toRightMovesNim i) = nim ↑i

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem quotEquivQuotMap_apply_mk (f g : R[X]) (I : Ideal R) :
    AdjoinRoot.quotEquivQuotMap f I (Ideal.Quotient.mk (Ideal.map (of f) I) (AdjoinRoot.mk f g)) =
      Ideal.Quotient.mk (Ideal.span ({Polynomial.map (Ideal.Quotient.mk I) f} : Set (R ⧸ I)[X]))
      (g.map (Ideal.Quotient.mk I))

Proof state:
R : Type u
inst✝ : CommRing R
f g : R[X]
I : Ideal R
⊢ (quotEquivQuotMap f I) ((Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) g)) =
    (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)

Tactic:
rw [AdjoinRoot.quotEquivQuotMap_apply, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of]

Result:
no goals