harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem map_rightUnitor (X : C) :
    F.map (ρ_ X).hom = δ F X (𝟙_ C) ≫ F.obj X ◁ η F ≫ (ρ_ (F.obj X)).hom

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X : C
⊢ F.map (ρ_ X).hom = δ F X (𝟙_ C) ≫ F.obj X ◁ η F ≫ (ρ_ (F.obj X)).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma restrictSubtype_ground_isBase_iff {B : Set M.E} :
    (M.restrictSubtype M.E).IsBase B ↔ M.IsBase B

Proof state:
α : Type u_1
M : Matroid α
B : Set ↑M.E
⊢ (M.restrictSubtype M.E).IsBase B ↔ M.IsBase (Subtype.val '' B)

Tactic:
rw [restrictSubtype_isBase_iff, isBasis'_iff_isBasis, isBasis_ground_iff]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
lemma rTensor_apply_X_tmul (s : σ) (n : N) (d : σ →₀ ℕ) :
    rTensor (X s ⊗ₜ[R] n) d = if Finsupp.single s 1 = d then (1 : S) ⊗ₜ[R] n else 0

Proof state:
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : DecidableEq σ
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : σ
n : N
d : σ →₀ ℕ
⊢ (rTensor (X s ⊗ₜ[R] n)) d = if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0

Tactic:
rw [rTensor_apply_tmul_apply, coeff_X', ite_tmul]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem mul_assoc (L : Matrix l m α) (M : Matrix m n α) (N : Matrix n o α) :
    L * M * N = L * (M * N)

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
L : Matrix l m α
M : Matrix m n α
N : Matrix n o α
i✝ : l
j✝ : o
⊢ (L * M * N) i✝ j✝ = (L * (M * N)) i✝ j✝

Tactic:
apply dotProduct_assoc

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
L : Matrix l m α
M : Matrix m n α
N : Matrix n o α
⊢ L * M * N = L * (M * N)

Tactic:
ext

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
L : Matrix l m α
M : Matrix m n α
N : Matrix n o α
i✝ : l
j✝ : o
⊢ (L * M * N) i✝ j✝ = (L * (M * N)) i✝ j✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toArray_swap (a : Vector α n) (i j) (hi hj) : (a.swap i j).toArray =
    a.toArray.swap i j (by simp [hi, hj]) (by simp [hi, hj]) := rfl

Proof state:
α : Type ?u.47508
n : Nat
a : Vector α n
i j : Nat
hi : j < n
hj : i < n
⊢ j < a.size

Tactic:
simp [hi, hj]

Result:
no goals

Proof state:
α : Type ?u.47508
n : Nat
a : Vector α n
i j : Nat
hi : j < n
hj : i < n
⊢ i < a.size

Tactic:
simp [hi, hj]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem aequiv_trans {U : Type*} [CommRing U] [Algebra R U] (h : IsAdjoinRoot S f)
    (h' : IsAdjoinRoot T f) (h'' : IsAdjoinRoot U f) :
    (h.aequiv h').trans (h'.aequiv h'') = h.aequiv h''

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
U : Type u_2
inst✝¹ : CommRing U
inst✝ : Algebra R U
h : IsAdjoinRoot S f
h' : IsAdjoinRoot T f
h'' : IsAdjoinRoot U f
⊢ (h.aequiv h').trans (h'.aequiv h'') = h.aequiv h''

Tactic:
ext z

Result:
case h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
U : Type u_2
inst✝¹ : CommRing U
inst✝ : Algebra R U
h : IsAdjoinRoot S f
h' : IsAdjoinRoot T f
h'' : IsAdjoinRoot U f
z : S
⊢ ((h.aequiv h').trans (h'.aequiv h'')) z = (h.aequiv h'') z

Proof state:
case h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
U : Type u_2
inst✝¹ : CommRing U
inst✝ : Algebra R U
h : IsAdjoinRoot S f
h' : IsAdjoinRoot T f
h'' : IsAdjoinRoot U f
z : S
⊢ ((h.aequiv h').trans (h'.aequiv h'')) z = (h.aequiv h'') z

Tactic:
exact h.aequiv_aequiv h' h'' z

Result:
no goals
-- Mathlib/Analysis/Convex/Continuous.lean
protected lemma ConvexOn.locallyLipschitz (hf : ConvexOn ℝ univ f) : LocallyLipschitz f

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hf : ConvexOn ℝ univ f
⊢ LocallyLipschitz f

Tactic:
simpa using hf.locallyLipschitzOn_interior

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Map.lean
theorem map_decl_eq {aig : AIG α} (target : MapTarget aig len) :
    ∀ idx (h1 : idx < aig.decls.size) (h2),
      (map aig target).1.decls[idx]'h2
        =
      aig.decls[idx]'h1

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : MapTarget aig len
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (map aig target).aig.decls.size
⊢ (map.go aig 0 ⋯ empty target.vec target.func).aig.decls[idx✝] = aig.decls[idx✝]

Tactic:
apply map.go_decl_eq

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : MapTarget aig len
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (map aig target).aig.decls.size),
    (map aig target).aig.decls[idx] = aig.decls[idx]

Tactic:
intros

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : MapTarget aig len
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (map aig target).aig.decls.size
⊢ (map aig target).aig.decls[idx✝] = aig.decls[idx✝]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : MapTarget aig len
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (map aig target).aig.decls.size
⊢ (map aig target).aig.decls[idx✝] = aig.decls[idx✝]

Tactic:
unfold map

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : MapTarget aig len
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (map aig target).aig.decls.size
⊢ (map.go aig 0 ⋯ empty target.vec target.func).aig.decls[idx✝] = aig.decls[idx✝]
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem forall_mem_map {f : α → β} {l : Array α} {P : β → Prop} :
    (∀ (i) (_ : i ∈ l.map f), P i) ↔ ∀ (j) (_ : j ∈ l), P (f j)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
P : β → Prop
⊢ (∀ (i : β), i ∈ map f l → P i) ↔ ∀ (j : α), j ∈ l → P (f j)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem nndist_eq_sum {p : ℝ≥0∞} [Fact (1 ≤ p)] {β : ι → Type*} [∀ i, PseudoMetricSpace (β i)]
    (hp : p ≠ ∞) (x y : PiLp p β) :
    nndist x y = (∑ i : ι, nndist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) :=
  -- Porting note: was `Subtype.ext`
  NNReal.eq <| by
    push_cast
    exact dist_eq_sum (p.toReal_pos_iff_ne_top.mpr hp) _ _

Proof state:
ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
inst✝ : (i : ι) → PseudoMetricSpace (β i)
hp : p ≠ ⊤
x y : PiLp p β
⊢ ↑(nndist x y) = ↑((∑ i : ι, nndist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal))

Tactic:
push_cast

Result:
ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
inst✝ : (i : ι) → PseudoMetricSpace (β i)
hp : p ≠ ⊤
x y : PiLp p β
⊢ dist x y = (∑ x_1 : ι, dist (x x_1) (y x_1) ^ p.toReal) ^ (1 / p.toReal)

Proof state:
ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
inst✝ : (i : ι) → PseudoMetricSpace (β i)
hp : p ≠ ⊤
x y : PiLp p β
⊢ dist x y = (∑ x_1 : ι, dist (x x_1) (y x_1) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
exact dist_eq_sum (p.toReal_pos_iff_ne_top.mpr hp) _ _

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem mem_vadd_const_affineSegment {x y z : V} (p : P) :
    z +ᵥ p ∈ affineSegment R (x +ᵥ p) (y +ᵥ p) ↔ z ∈ affineSegment R x y

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
x y z : V
p : P
⊢ z +ᵥ p ∈ affineSegment R (x +ᵥ p) (y +ᵥ p) ↔ z ∈ affineSegment R x y

Tactic:
rw [← affineSegment_vadd_const_image, (vadd_right_injective p).mem_set_image]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem Disjoint.cycleOf_mul_distrib [DecidableRel f.SameCycle] [DecidableRel g.SameCycle]
    [DecidableRel (f * g).SameCycle] [DecidableRel (g * f).SameCycle] (h : f.Disjoint g) (x : α) :
    (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

Proof state:
α : Type u_2
f g : Perm α
inst✝³ : DecidableRel f.SameCycle
inst✝² : DecidableRel g.SameCycle
inst✝¹ : DecidableRel (f * g).SameCycle
inst✝ : DecidableRel (g * f).SameCycle
h : f.Disjoint g
x : α
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

Tactic:
rcases (disjoint_iff_eq_or_eq.mp h) x with hfx | hgx

Result:
case inl
α : Type u_2
f g : Perm α
inst✝³ : DecidableRel f.SameCycle
inst✝² : DecidableRel g.SameCycle
inst✝¹ : DecidableRel (f * g).SameCycle
inst✝ : DecidableRel (g * f).SameCycle
h : f.Disjoint g
x : α
hfx : f x = x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

case inr
α : Type u_2
f g : Perm α
inst✝³ : DecidableRel f.SameCycle
inst✝² : DecidableRel g.SameCycle
inst✝¹ : DecidableRel (f * g).SameCycle
inst✝ : DecidableRel (g * f).SameCycle
h : f.Disjoint g
x : α
hgx : g x = x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

Proof state:
case inr
α : Type u_2
f g : Perm α
inst✝³ : DecidableRel f.SameCycle
inst✝² : DecidableRel g.SameCycle
inst✝¹ : DecidableRel (f * g).SameCycle
inst✝ : DecidableRel (g * f).SameCycle
h : f.Disjoint g
x : α
hgx : g x = x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

Tactic:
simp [cycleOf_mul_of_apply_right_eq_self h.commute, hgx]

Result:
no goals

Proof state:
case inl
α : Type u_2
f g : Perm α
inst✝³ : DecidableRel f.SameCycle
inst✝² : DecidableRel g.SameCycle
inst✝¹ : DecidableRel (f * g).SameCycle
inst✝ : DecidableRel (g * f).SameCycle
h : f.Disjoint g
x : α
hfx : f x = x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

Tactic:
simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem comp_inv_eq (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : f ≫ α.inv = g ↔ f = g ≫ α.hom :=
  ⟨fun H => by simp [H.symm], fun H => by simp [H]⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : Z ⟶ Y
g : Z ⟶ X
H : f ≫ α.inv = g
⊢ f = g ≫ α.hom

Tactic:
simp [H.symm]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : Z ⟶ Y
g : Z ⟶ X
H : f = g ≫ α.hom
⊢ f ≫ α.inv = g

Tactic:
simp [H]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem coe_tsum {f : α → ℝ≥0} : Summable f → ↑(tsum f) = ∑' a, (f a : ℝ≥0∞)
  | ⟨r, hr⟩ => by rw [hr.tsum_eq, ENNReal.tsum_coe_eq hr]

Proof state:
α : Type u_1
f : α → ℝ≥0
r : ℝ≥0
hr : HasSum f r
⊢ ↑(tsum f) = ∑' (a : α), ↑(f a)

Tactic:
rw [hr.tsum_eq, ENNReal.tsum_coe_eq hr]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem support_single_ne_bot (i : α) (h : b ≠ 0) : (single i b).support ≠ ⊥

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
b : M
i : α
h : b ≠ 0
⊢ (single i b).support ≠ ⊥

Tactic:
simpa only [support_single_ne_zero _ h] using singleton_ne_empty _

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem next_reverse_eq_prev (s : Cycle α) (hs : Nodup s) (x : α) (hx : x ∈ s) :
    s.reverse.next (nodup_reverse_iff.mpr hs) x (mem_reverse_iff.mpr hx) = s.prev hs x hx

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.reverse.next ⋯ x ⋯ = s.prev hs x hx

Tactic:
simp [← prev_reverse_eq_next]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
@[simp] lemma C_apply (t : R) (n : ℤ) : C t n = if n = 0 then t else 0

Proof state:
R : Type u_1
inst✝ : Semiring R
t : R
n : ℤ
⊢ (if 0 = n then t else 0) = if n = 0 then t else 0

Tactic:
aesop

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
t : R
n : ℤ
⊢ (C t) n = if n = 0 then t else 0

Tactic:
rw [← single_eq_C, Finsupp.single_apply]

Result:
R : Type u_1
inst✝ : Semiring R
t : R
n : ℤ
⊢ (if 0 = n then t else 0) = if n = 0 then t else 0
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_eq_prod_plift_of_mulSupport_subset {f : α → M} {s : Finset (PLift α)}
    (hs : mulSupport (f ∘ PLift.down) ⊆ s) : ∏ᶠ i, f i = ∏ i ∈ s, f i.down :=
  finprod_eq_prod_plift_of_mulSupport_toFinset_subset (s.finite_toSet.subset hs) fun x hx => by
    rw [Finite.mem_toFinset] at hx
    exact hs hx

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ mulSupport (f ∘ PLift.down)
⊢ x ∈ s

Tactic:
exact hs hx

Result:
no goals

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ ⋯.toFinset
⊢ x ∈ s

Tactic:
rw [Finite.mem_toFinset] at hx

Result:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ mulSupport (f ∘ PLift.down)
⊢ x ∈ s
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup'_map {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : (s.map f).Nonempty) :
    (s.map f).sup' hs g = s.sup' (map_nonempty.1 hs) (g ∘ f)

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset γ
f : γ ↪ β
g : β → α
hs : (map f s).Nonempty
⊢ (map f s).sup' hs g = s.sup' ⋯ (g ∘ ⇑f)

Tactic:
rw [← WithBot.coe_eq_coe, coe_sup', sup_map, coe_sup']

Result:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset γ
f : γ ↪ β
g : β → α
hs : (map f s).Nonempty
⊢ s.sup ((WithBot.some ∘ g) ∘ ⇑f) = s.sup (WithBot.some ∘ g ∘ ⇑f)

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset γ
f : γ ↪ β
g : β → α
hs : (map f s).Nonempty
⊢ s.sup ((WithBot.some ∘ g) ∘ ⇑f) = s.sup (WithBot.some ∘ g ∘ ⇑f)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
/-- Rectangles formed by π-systems form a π-system. -/
lemma IsPiSystem.prod {C : Set (Set α)} {D : Set (Set β)} (hC : IsPiSystem C) (hD : IsPiSystem D) :
    IsPiSystem (image2 (· ×ˢ ·) C D)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
hs₁ : s₁ ∈ C
t₁ : Set β
ht₁ : t₁ ∈ D
s₂ : Set α
hs₂ : s₂ ∈ C
t₂ : Set β
ht₂ : t₂ ∈ D
hst : (s₁ ∩ s₂).Nonempty ∧ (t₁ ∩ t₂).Nonempty
⊢ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) ∈ image2 (fun x1 x2 => x1 ×ˢ x2) C D

Tactic:
exact mem_image2_of_mem (hC _ hs₁ _ hs₂ hst.1) (hD _ ht₁ _ ht₂ hst.2)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
⊢ IsPiSystem (image2 (fun x1 x2 => x1 ×ˢ x2) C D)

Tactic:
rintro _ ⟨s₁, hs₁, t₁, ht₁, rfl⟩ _ ⟨s₂, hs₂, t₂, ht₂, rfl⟩ hst

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
hs₁ : s₁ ∈ C
t₁ : Set β
ht₁ : t₁ ∈ D
s₂ : Set α
hs₂ : s₂ ∈ C
t₂ : Set β
ht₂ : t₂ ∈ D
hst : ((fun x1 x2 => x1 ×ˢ x2) s₁ t₁ ∩ (fun x1 x2 => x1 ×ˢ x2) s₂ t₂).Nonempty
⊢ (fun x1 x2 => x1 ×ˢ x2) s₁ t₁ ∩ (fun x1 x2 => x1 ×ˢ x2) s₂ t₂ ∈ image2 (fun x1 x2 => x1 ×ˢ x2) C D

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
hs₁ : s₁ ∈ C
t₁ : Set β
ht₁ : t₁ ∈ D
s₂ : Set α
hs₂ : s₂ ∈ C
t₂ : Set β
ht₂ : t₂ ∈ D
hst : ((s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)).Nonempty
⊢ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) ∈ image2 (fun x1 x2 => x1 ×ˢ x2) C D

Tactic:
rw [prod_nonempty_iff] at hst

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
hs₁ : s₁ ∈ C
t₁ : Set β
ht₁ : t₁ ∈ D
s₂ : Set α
hs₂ : s₂ ∈ C
t₂ : Set β
ht₂ : t₂ ∈ D
hst : (s₁ ∩ s₂).Nonempty ∧ (t₁ ∩ t₂).Nonempty
⊢ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) ∈ image2 (fun x1 x2 => x1 ×ˢ x2) C D

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
hs₁ : s₁ ∈ C
t₁ : Set β
ht₁ : t₁ ∈ D
s₂ : Set α
hs₂ : s₂ ∈ C
t₂ : Set β
ht₂ : t₂ ∈ D
hst : ((fun x1 x2 => x1 ×ˢ x2) s₁ t₁ ∩ (fun x1 x2 => x1 ×ˢ x2) s₂ t₂).Nonempty
⊢ (fun x1 x2 => x1 ×ˢ x2) s₁ t₁ ∩ (fun x1 x2 => x1 ×ˢ x2) s₂ t₂ ∈ image2 (fun x1 x2 => x1 ×ˢ x2) C D

Tactic:
rw [prod_inter_prod] at hst ⊢

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
hs₁ : s₁ ∈ C
t₁ : Set β
ht₁ : t₁ ∈ D
s₂ : Set α
hs₂ : s₂ ∈ C
t₂ : Set β
ht₂ : t₂ ∈ D
hst : ((s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)).Nonempty
⊢ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) ∈ image2 (fun x1 x2 => x1 ×ˢ x2) C D
-- Mathlib/Analysis/NormedSpace/HomeomorphBall.lean
theorem univBall_symm_apply_center (c : P) (r : ℝ) : (univBall c r).symm c = 0

Proof state:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ 0 ∈ (univBall c r).source

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(univBall c r).symm c = 0

Tactic:
have : 0 ∈ (univBall c r).source := by simp

Result:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
this : 0 ∈ (univBall c r).source
⊢ ↑(univBall c r).symm c = 0

Proof state:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
this : 0 ∈ (univBall c r).source
⊢ ↑(univBall c r).symm c = 0

Tactic:
simpa only [univBall_apply_zero] using (univBall c r).left_inv this

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem id_tensorHom (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) :
    𝟙 X ⊗ f = X ◁ f

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : C
f : Y₁ ⟶ Y₂
⊢ 𝟙 X ⊗ f = X ◁ f

Tactic:
simp [tensorHom_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem prefix_append_right_inj (l) : l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂ :=
  exists_congr fun r => by rw [append_assoc, append_right_inj]

Proof state:
α✝ : Type u_1
l₁ l₂ l r : List α✝
⊢ l ++ l₁ ++ r = l ++ l₂ ↔ l₁ ++ r = l₂

Tactic:
rw [append_assoc, append_right_inj]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/SheafHom.lean
lemma Presheaf.IsSheaf.hom (hG : Presheaf.IsSheaf J G) :
    Presheaf.IsSheaf J (presheafHom F G)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
⊢ Presieve.IsSheaf J (presheafHom F G)

Tactic:
intro X S hS

Result:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor (presheafHom F G) S.arrows

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor (presheafHom F G) S.arrows

Tactic:
exact presheafHom_isSheafFor F G S
  (fun _ _ => ((Presheaf.isSheaf_iff_isLimit J G).1 hG _ (J.pullback_stable _ hS)).some)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
⊢ IsSheaf J (presheafHom F G)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
⊢ Presieve.IsSheaf J (presheafHom F G)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_insertMany_list_of_contains_eq_false [LawfulBEq α] (h : m.WF)
    {l : List ((a : α) × β a)} {k : α} {fallback : β k}
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (m.insertMany l).getD k fallback = m.getD k fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k : α
fallback : β k
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (m.insertMany l).getD k fallback = m.getD k fallback

Tactic:
simp_to_raw using Raw₀.getD_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean
theorem inr_inr_pushoutRightPushoutInlIso_hom :
    pushout.inr _ _ ≫ pushout.inr _ _ ≫ (pushoutRightPushoutInlIso f g f').hom =
      pushout.inr _ _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout f' (pushout.inl f g)
⊢ (pushout.inr f g ≫ pushout.inr f' (pushout.inl f g)) ≫ (pushoutRightPushoutInlIso f g f').hom = pushout.inr (f ≫ f') g

Tactic:
apply IsColimit.comp_coconePointUniqueUpToIso_hom (pasteVertIsPushout rfl _ _) _ WalkingSpan.right

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout f' (pushout.inl f g)
⊢ pushout.inr f g ≫ pushout.inr f' (pushout.inl f g) ≫ (pushoutRightPushoutInlIso f g f').hom = pushout.inr (f ≫ f') g

Tactic:
rw [← Category.assoc]

Result:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout f' (pushout.inl f g)
⊢ (pushout.inr f g ≫ pushout.inr f' (pushout.inl f g)) ≫ (pushoutRightPushoutInlIso f g f').hom = pushout.inr (f ≫ f') g
-- Mathlib/Computability/PostTuringMachine.lean
theorem eval_maximal₁ {σ} {f : σ → Option σ} {a b} (h : b ∈ eval f a) (c) : ¬Reaches₁ f b c
  | bc => by
    let ⟨_, b0⟩ := mem_eval.1 h
    let ⟨b', h', _⟩ := TransGen.head'_iff.1 bc
    cases b0.symm.trans h'

Proof state:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
x✝ : Reaches₁ f b c
bc : Reaches₁ f b c := x✝
left✝ : Reaches f a b
b0 : f b = none
b' : σ
h' : b' ∈ f b
right✝ : ReflTransGen (fun a b => b ∈ f a) b' c
⊢ False

Tactic:
cases b0.symm.trans h'

Result:
no goals

Proof state:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
x✝ : Reaches₁ f b c
bc : Reaches₁ f b c := x✝
left✝ : Reaches f a b
b0 : f b = none
⊢ False

Tactic:
let ⟨b', h', _⟩ := TransGen.head'_iff.1 bc

Result:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
x✝ : Reaches₁ f b c
bc : Reaches₁ f b c := x✝
left✝ : Reaches f a b
b0 : f b = none
b' : σ
h' : b' ∈ f b
right✝ : ReflTransGen (fun a b => b ∈ f a) b' c
⊢ False

Proof state:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
x✝ : Reaches₁ f b c
bc : Reaches₁ f b c := x✝
⊢ False

Tactic:
let ⟨_, b0⟩ := mem_eval.1 h

Result:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
x✝ : Reaches₁ f b c
bc : Reaches₁ f b c := x✝
left✝ : Reaches f a b
b0 : f b = none
⊢ False
-- Mathlib/SetTheory/Cardinal/Basic.lean
lemma mk_lt_aleph0_iff : #α < ℵ₀ ↔ Finite α

Proof state:
α : Type u
⊢ #α < ℵ₀ ↔ Finite α

Tactic:
simp [← not_le, aleph0_le_mk_iff]

Result:
no goals
-- Mathlib/Data/Int/Cast/Lemmas.lean
lemma cast_commute : ∀ (n : ℤ) (a : α), Commute ↑n a
  | (n : ℕ), x => by simpa using n.cast_commute x
  | -[n+1], x => by
    simpa only [cast_negSucc, Commute.neg_left_iff, Commute.neg_right_iff] using
      (n + 1).cast_commute (-x)

Proof state:
α : Type u_3
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑↑n) x

Tactic:
simpa using n.cast_commute x

Result:
no goals

Proof state:
α : Type u_3
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑-[n+1]) x

Tactic:
simpa only [cast_negSucc, Commute.neg_left_iff, Commute.neg_right_iff] using
  (n + 1).cast_commute (-x)

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem forall_mem_pair {P : α → Prop} {a b : α} : (∀ x ∈ s(a, b), P x) ↔ P a ∧ P b

Proof state:
α : Type u_1
P : α → Prop
a b : α
⊢ (∀ x ∈ s(a, b), P x) ↔ P a ∧ P b

Tactic:
simp only [mem_iff, forall_eq_or_imp, forall_eq]

Result:
no goals