harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem getElem?_zipIdx (l : Vector α n) (n m) : (zipIdx l n)[m]? = l[m]?.map fun a => (a, n + m)

Proof state:
α : Type u_1
n✝ : Nat
l : Vector α n✝
n m : Nat
⊢ (l.zipIdx n)[m]? = Option.map (fun a => (a, n + m)) l[m]?

Tactic:
simp [getElem?_def]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem disjoint {ν ν' : ι → ℤ} :
    ν ≠ ν' ↔ Disjoint (box n ν).toSet (box n ν').toSet

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν ν' : ι → ℤ
⊢ (∃ x ∈ ↑(box n ν), x ∈ ↑(box n ν')) ↔ ν = ν'

Tactic:
refine ⟨fun ⟨x, hx, hx'⟩ ↦ ?_, fun h ↦ ⟨tag n ν, tag_mem n ν, h ▸ tag_mem n ν⟩⟩

Result:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν ν' : ι → ℤ
x✝ : ∃ x ∈ ↑(box n ν), x ∈ ↑(box n ν')
x : ι → ℝ
hx : x ∈ ↑(box n ν)
hx' : x ∈ ↑(box n ν')
⊢ ν = ν'

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν ν' : ι → ℤ
⊢ ν ≠ ν' ↔ Disjoint ↑(box n ν) ↑(box n ν')

Tactic:
rw [not_iff_comm, Set.not_disjoint_iff]

Result:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν ν' : ι → ℤ
⊢ (∃ x ∈ ↑(box n ν), x ∈ ↑(box n ν')) ↔ ν = ν'

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν ν' : ι → ℤ
x✝ : ∃ x ∈ ↑(box n ν), x ∈ ↑(box n ν')
x : ι → ℝ
hx : x ∈ ↑(box n ν)
hx' : x ∈ ↑(box n ν')
⊢ ν = ν'

Tactic:
rw [← mem_box_iff_index.mp hx, ← mem_box_iff_index.mp hx']

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma P1_of_lt (h₁ : P3 x₃ x₂ y₂ y₃) (h₂ : P3 x₁ x₃ y₂ y₁) : P1 x₁ x₂ x₃ y₁ y₂ y₃

Proof state:
x₁ x₂ x₃ y₁ y₂ y₃ : PGame
h₁ : P3 x₃ x₂ y₂ y₃
h₂ : P3 x₁ x₃ y₂ y₁
⊢ P1 x₁ x₂ x₃ y₁ y₂ y₃

Tactic:
rw [P1, sub_lt_sub_iff, ← add_lt_add_iff_left ⟦x₃ * y₂⟧]

Result:
x₁ x₂ x₃ y₁ y₂ y₃ : PGame
h₁ : P3 x₃ x₂ y₂ y₃
h₂ : P3 x₁ x₃ y₂ y₁
⊢ ⟦x₃ * y₂⟧ + (⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧ + ⟦x₃ * y₃⟧) < ⟦x₃ * y₂⟧ + (⟦x₃ * y₁⟧ + ⟦x₂ * y₃⟧ + ⟦x₁ * y₂⟧)

Proof state:
x₁ x₂ x₃ y₁ y₂ y₃ : PGame
h₁ : P3 x₃ x₂ y₂ y₃
h₂ : P3 x₁ x₃ y₂ y₁
⊢ ⟦x₃ * y₂⟧ + (⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧ + ⟦x₃ * y₃⟧) < ⟦x₃ * y₂⟧ + (⟦x₃ * y₁⟧ + ⟦x₂ * y₃⟧ + ⟦x₁ * y₂⟧)

Tactic:
convert add_lt_add h₁ h₂ using 1 <;> abel

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp) zsmul_empty]
lemma empty_zpow (hn : n ≠ 0) : (∅ : Finset α) ^ n = ∅

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Tactic:
cases n <;> aesop

Result:
no goals
-- Mathlib/CategoryTheory/Localization/HomEquiv.lean
@[simp]
lemma homEquiv_map (f : X ⟶ Y) : homEquiv W L₁ L₂ (L₁.map f) = L₂.map f

Proof state:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{u_8, u_1} C
inst✝³ : Category.{u_10, u_5} D₁
inst✝² : Category.{u_9, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X Y : C
f : X ⟶ Y
⊢ (homEquiv W L₁ L₂) (L₁.map f) = L₂.map f

Tactic:
simp [homEquiv_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Bounded.lean
@[to_additive (attr := simp) comap_norm_atTop]
lemma comap_norm_atTop' : comap norm atTop = cobounded E

Proof state:
E : Type u_2
inst✝ : SeminormedGroup E
⊢ comap norm atTop = cobounded E

Tactic:
simpa only [dist_one_right] using comap_dist_right_atTop (1 : E)

Result:
no goals
-- Mathlib/Topology/Order/IntermediateValue.lean
theorem ContinuousOn.surjOn_uIcc {s : Set α} [hs : OrdConnected s] {f : α → δ}
    (hf : ContinuousOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
    SurjOn f s (uIcc (f a) (f b))

Proof state:
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
s : Set α
hs : s.OrdConnected
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ SurjOn f s [[f a, f b]]

Tactic:
rcases le_total (f a) (f b) with hab | hab <;> simp [hf.surjOn_Icc, *]

Result:
no goals
-- Mathlib/Combinatorics/Additive/CovBySMul.lean
@[to_additive (attr := simp, refl)]
lemma CovBySMul.rfl : CovBySMul M 1 A A := ⟨1, by simp⟩

Proof state:
M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
A : Set X
⊢ ↑(#1) ≤ 1 ∧ A ⊆ ↑1 • A

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem mem_toSubtype_iff {p : β → Prop} {f : α → β} {a : α} {b : Subtype p} :
    b ∈ toSubtype p f a ↔ ↑b = f a

Proof state:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
b : Subtype p
⊢ b ∈ toSubtype p f a ↔ ↑b = f a

Tactic:
rw [toSubtype_apply, Part.mem_mk_iff, exists_subtype_mk_eq_iff, eq_comm]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_comap_comap_eq_relrank_of_le
    {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) (h : B ≤ f.fieldRange) :
    relrank (A.comap f) (B.comap f) = relrank A B

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
h : B ≤ f.fieldRange
⊢ (comap f A).relrank (comap f B) = A.relrank B

Tactic:
simpa only [lift_id] using lift_relrank_comap_comap_eq_lift_relrank_of_le A B f h

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem dist_pointReflection_self' (x y : P) :
    dist (pointReflection 𝕜 x y) y = ‖2 • (x -ᵥ y)‖

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
⊢ dist ((pointReflection 𝕜 x) y) y = ‖2 • (x -ᵥ y)‖

Tactic:
rw [pointReflection_apply, dist_eq_norm_vsub V, vadd_vsub_assoc, two_nsmul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem set_eq_nil_iff {l : List α} (n : Nat) (a : α) : l.set n a = [] ↔ l = []

Proof state:
α : Type u_1
l : List α
n : Nat
a : α
⊢ l.set n a = [] ↔ l = []

Tactic:
cases l <;> cases n <;> simp [set]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem absorbent_ball (hpr : p x < r) : Absorbent 𝕜 (ball p x r)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
y : E
hy : p y < r - p x
⊢ y ∈ p.ball x r

Tactic:
exact p.mem_ball.2 ((map_sub_le_add p _ _).trans_lt <| add_lt_of_lt_sub_right hy)

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
⊢ Absorbent 𝕜 (p.ball x r)

Tactic:
refine (p.absorbent_ball_zero <| sub_pos.2 hpr).mono fun y hy => ?_

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
y : E
hy : y ∈ p.ball 0 (r - p x)
⊢ y ∈ p.ball x r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
y : E
hy : y ∈ p.ball 0 (r - p x)
⊢ y ∈ p.ball x r

Tactic:
rw [p.mem_ball_zero] at hy

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
y : E
hy : p y < r - p x
⊢ y ∈ p.ball x r
-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem sphere_ext_iff (u v : sphere (0 : E) 1) : u = v ↔ ⟪(u : E), v⟫_ℝ = 1

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
u v : ↑(sphere 0 1)
⊢ u = v ↔ ⟪↑u, ↑v⟫_ℝ = 1

Tactic:
simp [Subtype.ext_iff, inner_eq_one_iff_of_norm_one]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem span_pair_mul_span_pair (w x y z : R) :
    (span {w, x} : Ideal R) * span {y, z} = span {w * y, w * z, x * y, x * z}

Proof state:
R : Type u
inst✝ : CommSemiring R
w x y z : R
⊢ span {w, x} * span {y, z} = span {w * y, w * z, x * y, x * z}

Tactic:
simp_rw [span_insert, sup_mul, mul_sup, span_singleton_mul_span_singleton, sup_assoc]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem inverse_mul_cancel_right (x y : M₀) (h : IsUnit x) : y * inverse x * x = y

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y * inverse x * x = y

Tactic:
rw [mul_assoc, inverse_mul_cancel x h, mul_one]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_ite {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f g : α → β) :
    ∏ x ∈ s, (if p x then f x else g x) = (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, g x

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
p : α → Prop
hp : DecidablePred p
f g : α → β
⊢ (∏ x ∈ s, if p x then f x else g x) = (∏ x ∈ filter (fun x => p x) s, f x) * ∏ x ∈ filter (fun x => ¬p x) s, g x

Tactic:
simp [prod_apply_ite _ _ fun x => x]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem nthRoots_zero_right {R} [CommRing R] [IsDomain R] (n : ℕ) :
    nthRoots n (0 : R) = Multiset.replicate n 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ nthRoots n 0 = replicate n 0

Tactic:
rw [nthRoots, C.map_zero, sub_zero, roots_pow, roots_X, Multiset.nsmul_singleton]

Result:
no goals
-- Mathlib/Order/Birkhoff.lean
@[simp] lemma birkhoffSet_inf (a b : α) : birkhoffSet (a ⊓ b) = birkhoffSet a ∩ birkhoffSet b

Proof state:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
⊢ birkhoffSet (a ⊓ b) = birkhoffSet a ∩ birkhoffSet b

Tactic:
unfold OrderEmbedding.birkhoffSet

Result:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
⊢ (if h : IsEmpty α then ofIsEmpty
      else
        let_fun this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊓ b) =
    (if h : IsEmpty α then ofIsEmpty
        else
          let_fun this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∩
      (if h : IsEmpty α then ofIsEmpty
        else
          let_fun this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b

Proof state:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
⊢ (if h : IsEmpty α then ofIsEmpty
      else
        let_fun this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊓ b) =
    (if h : IsEmpty α then ofIsEmpty
        else
          let_fun this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∩
      (if h : IsEmpty α then ofIsEmpty
        else
          let_fun this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b

Tactic:
split <;> simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/GroupTheory/Sylow.lean
theorem characteristic_of_normal {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G)
    (h : P.Normal) : P.Characteristic

Proof state:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
this : Unique (Sylow p G)
⊢ ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom ↑P = ↑P

Tactic:
intro Φ

Result:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
this : Unique (Sylow p G)
Φ : G ≃* G
⊢ Subgroup.map Φ.toMonoidHom ↑P = ↑P

Proof state:
case e_self
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
this : Unique (Sylow p G)
Φ : G ≃* G
⊢ Φ • P = P

Tactic:
simp [eq_iff_true_of_subsingleton]

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
h : (↑P).Normal
this : Unique (Sylow p G)
⊢ (↑P).Characteristic

Tactic:
rw [characteristic_iff_map_eq]

Result:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
this : Unique (Sylow p G)
⊢ ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom ↑P = ↑P

Proof state:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
this : Unique (Sylow p G)
Φ : G ≃* G
⊢ Subgroup.map Φ.toMonoidHom ↑P = ↑P

Tactic:
show (Φ • P).toSubgroup = P.toSubgroup

Result:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
this : Unique (Sylow p G)
Φ : G ≃* G
⊢ ↑(Φ • P) = ↑P

Proof state:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
this : Unique (Sylow p G)
Φ : G ≃* G
⊢ ↑(Φ • P) = ↑P

Tactic:
congr

Result:
case e_self
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
this : Unique (Sylow p G)
Φ : G ≃* G
⊢ Φ • P = P

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

Tactic:
haveI := unique_of_normal P h

Result:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
this : Unique (Sylow p G)
⊢ (↑P).Characteristic
-- Mathlib/Data/Multiset/Fold.lean
theorem fold_cons'_right (b a : α) (s : Multiset α) : (a ::ₘ s).fold op b = s.fold op (b * a)

Proof state:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op b a) s

Tactic:
rw [fold_eq_foldl, foldl_cons, ← fold_eq_foldl]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma comapOn_isBase_iff_of_surjOn (h : SurjOn f E N.E) :
    (N.comapOn E f).IsBase B ↔ (N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E

Tactic:
simp_rw [comapOn_isBase_iff, and_congr_left_iff, and_imp, isBasis'_iff_isBasis_inter_ground,
  inter_eq_self_of_subset_right h, isBasis_ground_iff, implies_true]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem length_empty : f.length ∅ = 0 :=
  nonpos_iff_eq_zero.1 <| iInf_le_of_le 0 <| iInf_le_of_le 0 <| by simp

Proof state:
f : StieltjesFunction
⊢ ⨅ (_ : ∅ ⊆ Ioc 0 0), ofReal (↑f 0 - ↑f 0) ≤ 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem pentagon_hom_hom_inv_inv_hom :
    (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv =
      (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom :=
  eq_of_inv_eq_inv (by simp)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ inv ((α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv) =
    inv ((α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom)

Tactic:
simp

Result:
no goals
-- Mathlib/ModelTheory/Types.lean
theorem iInter_setOf_subset {ι : Type*} (S : ι → L[[α]].Theory) :
    ⋂ i : ι, { p : T.CompleteType α | S i ⊆ p } =
      { p : T.CompleteType α | ⋃ i : ι, S i ⊆ p }

Proof state:
L : Language
T : L.Theory
α : Type w
ι : Type u_1
S : ι → L[[α]].Theory
⊢ ⋂ i, {p | S i ⊆ ↑p} = {p | ⋃ i, S i ⊆ ↑p}

Tactic:
ext

Result:
case h
L : Language
T : L.Theory
α : Type w
ι : Type u_1
S : ι → L[[α]].Theory
x✝ : T.CompleteType α
⊢ x✝ ∈ ⋂ i, {p | S i ⊆ ↑p} ↔ x✝ ∈ {p | ⋃ i, S i ⊆ ↑p}

Proof state:
case h
L : Language
T : L.Theory
α : Type w
ι : Type u_1
S : ι → L[[α]].Theory
x✝ : T.CompleteType α
⊢ x✝ ∈ ⋂ i, {p | S i ⊆ ↑p} ↔ x✝ ∈ {p | ⋃ i, S i ⊆ ↑p}

Tactic:
simp only [mem_iInter, mem_setOf_eq, iUnion_subset_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option β → Option β}
    (h : m.WF) (h₁ : k ∈ m) (h₂ : (f (Const.get? m k)).isSome) :
    (Const.alter m k f).size = m.size

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ k ∈ m → (f (get? m k)).isSome = true → (alter m k f).size = m.size

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ m.contains k = true → (f (get? m k)).isSome = true → (alter m k f).size = m.size

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
h₁ : k ∈ m
h₂ : (f (get? m k)).isSome = true
⊢ (alter m k f).size = m.size

Tactic:
revert h₁ h₂

Result:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ k ∈ m → (f (get? m k)).isSome = true → (alter m k f).size = m.size

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ m.contains k = true → (f (get? m k)).isSome = true → (alter m k f).size = m.size

Tactic:
simp_to_raw using Raw₀.Const.size_alter_eq_self_of_mem

Result:
no goals
-- Mathlib/Analysis/Asymptotics/TVS.lean
lemma isLittleOTVS_sup : f =o[𝕜; l₁ ⊔ l₂] g ↔ f =o[𝕜; l₁] g ∧ f =o[𝕜; l₂] g

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l₁ l₂ : Filter α
f : α → E
g : α → F
⊢ f =o[𝕜;l₁ ⊔ l₂] g ↔ f =o[𝕜;l₁] g ∧ f =o[𝕜;l₂] g

Tactic:
simp only [isLittleOTVS_iff_smallSets, ← forall_and, ← eventually_and, eventually_sup]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mk_eq_normalize (num den nz c) : ⟨num, den, nz, c⟩ = normalize num den nz

Proof state:
num : Int
den : Nat
nz : den ≠ 0
c : num.natAbs.Coprime den
⊢ { num := num, den := den, den_nz := nz, reduced := c } = normalize num den nz

Tactic:
simp [normalize_eq, c.gcd_eq_one]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
@[simp] lemma piTensorHomMap_tprod_tprod (f : Π i, s i →ₗ[R] t i) (x : Π i, s i) :
    piTensorHomMap (tprod R f) (tprod R x) = tprod R fun i ↦ f i (x i)

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
x : (i : ι) → s i
⊢ (piTensorHomMap ((tprod R) f)) ((tprod R) x) = ⨂ₜ[R] (i : ι), (f i) (x i)

Tactic:
simp [piTensorHomMap]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem p_nonzero [Nontrivial R] [CharP R p] : (p : 𝕎 R) ≠ 0

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
⊢ ↑p ≠ 0

Tactic:
intro h

Result:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
h : ↑p = 0
⊢ False

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
h : ↑p = 0
⊢ False

Tactic:
simpa only [h, zero_coeff, zero_ne_one] using coeff_p_one p R

Result:
no goals
-- Mathlib/Probability/CondVar.lean
lemma condVar_bot' [NeZero μ] (X : Ω → ℝ) :
    Var[X; μ | ⊥] = fun _ => ⨍ ω, (X ω - ⨍ ω', X ω' ∂μ) ^ 2 ∂μ

Proof state:
Ω : Type u_1
m₀ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : NeZero μ
X : Ω → ℝ
⊢ Var[X; μ | ⊥] = fun x => ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂μ) ^ 2 ∂μ

Tactic:
ext ω

Result:
case h
Ω : Type u_1
m₀ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : NeZero μ
X : Ω → ℝ
ω : Ω
⊢ Var[X; μ | ⊥] ω = ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂μ) ^ 2 ∂μ

Proof state:
case h
Ω : Type u_1
m₀ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : NeZero μ
X : Ω → ℝ
ω : Ω
⊢ Var[X; μ | ⊥] ω = ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂μ) ^ 2 ∂μ

Tactic:
simp [condVar, condExp_bot', average]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Basic.lean
lemma absorbs_iff_norm : Absorbs 𝕜 A B ↔ ∃ r, ∀ c : 𝕜, r ≤ ‖c‖ → B ⊆ c • A :=
  Filter.atTop_basis.cobounded_of_norm.eventually_iff.trans <| by simp only [true_and]; rfl

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
A B : Set E
⊢ (∃ i, True ∧ ∀ ⦃x : 𝕜⦄, x ∈ norm ⁻¹' Ici i → B ⊆ x • A) ↔ ∃ r, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A

Tactic:
simp only [true_and]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
A B : Set E
⊢ (∃ i, ∀ ⦃x : 𝕜⦄, x ∈ norm ⁻¹' Ici i → B ⊆ x • A) ↔ ∃ r, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
A B : Set E
⊢ (∃ i, ∀ ⦃x : 𝕜⦄, x ∈ norm ⁻¹' Ici i → B ⊆ x • A) ↔ ∃ r, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem span_neg (s : Set M) : span R (-s) = span R s :=
  calc
    span R (-s) = span R ((-LinearMap.id : M →ₗ[R] M) '' s)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) = span R (⇑(-LinearMap.id) '' s)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ map (-LinearMap.id) (span R s) = span R s

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem interior_sInter_subset (S : Set (Set X)) : interior (⋂₀ S) ⊆ ⋂ s ∈ S, interior s :=
  calc
    interior (⋂₀ S) = interior (⋂ s ∈ S, s)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
⊢ interior (⋂₀ S) = interior (⋂ s ∈ S, s)

Tactic:
rw [sInter_eq_biInter]

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_convexJoin_convexJoin_comm (s t u v : Set E) :
    convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) =
      convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u v : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)

Tactic:
simp_rw [← convexJoin_assoc, convexJoin_right_comm]

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem WCovBy.Ioc_subset (h : a ⩿ b) : Ioc a b ⊆ {b}

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Ioc a b ⊆ {b}

Tactic:
rw [← Icc_diff_left, h.Icc_eq, diff_singleton_subset_iff]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean
@[simp]
lemma N₂_map_isoΓ₀_hom_app_f (X : ChainComplex C ℕ) :
    (N₂.map (isoΓ₀.hom.app X)).f = PInfty

Proof state:
case h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
i✝ : ℕ
⊢ (N₂.map (isoΓ₀.hom.app X)).f.f i✝ = PInfty.f i✝

Tactic:
apply comp_id

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
⊢ (N₂.map (isoΓ₀.hom.app X)).f = PInfty

Tactic:
ext

Result:
case h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
i✝ : ℕ
⊢ (N₂.map (isoΓ₀.hom.app X)).f.f i✝ = PInfty.f i✝
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Iio_add_one_eq_Iic (b : α) : Iio (b + 1) = Iic b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
b : α
⊢ Iio (b + 1) = Iic b

Tactic:
simpa [succ_eq_add_one] using Iio_succ_eq_Iic b

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
lemma not_nil_iff_lt_length {p : G.Walk v w} : ¬ p.Nil ↔ 0 < p.length

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ ¬p.Nil ↔ 0 < p.length

Tactic:
cases p <;> simp

Result:
no goals