harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_eq_of_bijective {f : α → M} {g : β → M} (e : α → β) (he₀ : Bijective e)
    (he₁ : ∀ x, f x = g (e x)) : ∏ᶠ i, f i = ∏ᶠ j, g j

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ univ), f i = ∏ᶠ (i : β) (_ : i ∈ univ), g i

Tactic:
exact finprod_mem_eq_of_bijOn _ (bijective_iff_bijOn_univ.mp he₀) fun x _ => he₁ x

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ ∏ᶠ (i : α), f i = ∏ᶠ (j : β), g j

Tactic:
rw [← finprod_mem_univ f, ← finprod_mem_univ g]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ univ), f i = ∏ᶠ (i : β) (_ : i ∈ univ), g i
-- Mathlib/Algebra/Ring/Ext.lean
theorem ext ⦃inst₁ inst₂ : Ring R⦄
    (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
    (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) :
    inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
⊢ inst₁ = inst₂

Tactic:
have h₂ : inst₁.toNonAssocRing = inst₂.toNonAssocRing := by
  ext : 1 <;> assumption

Result:
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
h₂ : toNonAssocRing = toNonAssocRing
⊢ inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toSemiring = toSemiring

Tactic:
ext : 1 <;> assumption

Result:
no goals

Proof state:
case mk.mk.e_toIntCast
R : Type u
toSemiring✝¹ : Semiring R
toNeg✝¹ : Neg R
toSub✝¹ : Sub R
sub_eq_add_neg✝¹ : ∀ (a b : R), a - b = a + -b
zsmul✝¹ : ℤ → R → R
zsmul_zero'✝¹ : ∀ (a : R), zsmul✝¹ 0 a = 0
zsmul_succ'✝¹ : ∀ (n : ℕ) (a : R), zsmul✝¹ (↑n.succ) a = zsmul✝¹ (↑n) a + a
zsmul_neg'✝¹ : ∀ (n : ℕ) (a : R), zsmul✝¹ (Int.negSucc n) a = -zsmul✝¹ (↑n.succ) a
neg_add_cancel✝¹ : ∀ (a : R), -a + a = 0
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toSemiring✝ : Semiring R
toNeg✝ : Neg R
toSub✝ : Sub R
sub_eq_add_neg✝ : ∀ (a b : R), a - b = a + -b
zsmul✝ : ℤ → R → R
zsmul_zero'✝ : ∀ (a : R), zsmul✝ 0 a = 0
zsmul_succ'✝ : ∀ (n : ℕ) (a : R), zsmul✝ (↑n.succ) a = zsmul✝ (↑n) a + a
zsmul_neg'✝ : ∀ (n : ℕ) (a : R), zsmul✝ (Int.negSucc n) a = -zsmul✝ (↑n.succ) a
neg_add_cancel✝ : ∀ (a : R), -a + a = 0
toIntCast✝ : IntCast R
intCast_ofNat✝ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ : AddGroup.toSubNegMonoid = AddGroup.toSubNegMonoid
⊢ toIntCast✝¹ = toIntCast✝

Tactic:
injection h₂

Result:
no goals

Proof state:
case h_mul
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
h₂ : toNonAssocRing = toNonAssocRing
⊢ Add.add = Add.add

Tactic:
exact h_add

Result:
no goals

Proof state:
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
have h₁ : inst₁.toSemiring = inst₂.toSemiring := by
  ext : 1 <;> assumption

Result:
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
⊢ inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toSemiring = toSemiring
⊢ toNonAssocRing = toNonAssocRing

Tactic:
ext : 1 <;> assumption

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq {p₁ p₂ p₃ : P}
    (h : dist p₁ p₂ = dist p₁ p₃) : |(∡ p₁ p₂ p₃).toReal| < π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ |(o.oangle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃))).toReal| < π / 2

Tactic:
exact o.abs_oangle_sub_right_toReal_lt_pi_div_two h

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : dist p₁ p₂ = dist p₁ p₃
⊢ |(∡ p₁ p₂ p₃).toReal| < π / 2

Tactic:
simp_rw [dist_eq_norm_vsub V] at h

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ |(∡ p₁ p₂ p₃).toReal| < π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ |(∡ p₁ p₂ p₃).toReal| < π / 2

Tactic:
rw [oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ |(o.oangle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃))).toReal| < π / 2
-- Mathlib/Algebra/GeomSum.lean
theorem nat_sub_dvd_pow_sub_pow (x y n : ℕ) : x - y ∣ x ^ n - y ^ n

Proof state:
case inr
x y n : ℕ
h : x < y
this : x ^ n ≤ y ^ n
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)

Result:
no goals

Proof state:
x y n : ℕ
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
rcases le_or_lt y x with h | h

Result:
case inl
x y n : ℕ
h : y ≤ x
⊢ x - y ∣ x ^ n - y ^ n

case inr
x y n : ℕ
h : x < y
⊢ x - y ∣ x ^ n - y ^ n

Proof state:
case inl
x y n : ℕ
h : y ≤ x
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
have : y ^ n ≤ x ^ n := Nat.pow_le_pow_left h _

Result:
case inl
x y n : ℕ
h : y ≤ x
this : y ^ n ≤ x ^ n
⊢ x - y ∣ x ^ n - y ^ n

Proof state:
case inr
x y n : ℕ
h : x < y
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
have : x ^ n ≤ y ^ n := Nat.pow_le_pow_left h.le _

Result:
case inr
x y n : ℕ
h : x < y
this : x ^ n ≤ y ^ n
⊢ x - y ∣ x ^ n - y ^ n

Proof state:
case inl
x y n : ℕ
h : y ≤ x
this : y ^ n ≤ x ^ n
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
exact mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem not_mem_empty (a : α) : ¬ a ∈ #[]

Proof state:
α : Type u_1
a : α
⊢ ¬a ∈ #[]

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
theorem weight_vector_multiplication (M₁ M₂ M₃ : Type*)
    [AddCommGroup M₁] [Module R M₁] [LieRingModule L M₁] [LieModule R L M₁] [AddCommGroup M₂]
    [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] [AddCommGroup M₃] [Module R M₃]
    [LieRingModule L M₃] [LieModule R L M₃] (g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃) (χ₁ χ₂ : R) (x : L) :
    LinearMap.range ((g : M₁ ⊗[R] M₂ →ₗ[R] M₃).comp (mapIncl 𝕎(M₁, χ₁, x) 𝕎(M₂, χ₂, x))) ≤
      𝕎(M₃, χ₁ + χ₂, x)

Proof state:
case refine_2.mk.mk
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
hm₁ : m₁ ∈ 𝕎(M₁, χ₁, x)
m₂ : M₂
hm₂ : m₂ ∈ 𝕎(M₂, χ₂, x)
⊢ ∃ k, (F ^ k) (↑g (m₁ ⊗ₜ[R] m₂)) = 0

Tactic:
let f₁ : Module.End R (M₁ ⊗[R] M₂) := (toEnd R L M₁ x - χ₁ • ↑1).rTensor M₂

Result:
case refine_2.mk.mk
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
hm₁ : m₁ ∈ 𝕎(M₁, χ₁, x)
m₂ : M₂
hm₂ : m₂ ∈ 𝕎(M₂, χ₂, x)
f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)
⊢ ∃ k, (F ^ k) (↑g (m₁ ⊗ₜ[R] m₂)) = 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] {t : RBNode α} :
    t.foldlM (m := m) f init = t.toList.foldlM f init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
a✝ : Type u_1
f : a✝ → α → m a✝
init : a✝
inst✝¹ : Monad m
inst✝ : LawfulMonad m
t : RBNode α
⊢ foldlM f init t = List.foldlM f init t.toList

Tactic:
induction t generalizing init <;> simp [*]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
lemma IsCompact.elim_nhds_subcover_nhdsSet (hs : IsCompact s) {U : X → Set X}
    (hU : ∀ x ∈ s, U x ∈ 𝓝 x) : ∃ t : Finset X, (∀ x ∈ t, x ∈ s) ∧ (⋃ x ∈ t, U x) ∈ 𝓝ˢ s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Finset ↑s
ht : ⋃ x ∈ t, U ↑x ∈ 𝓝ˢ s
⊢ ⋃ x ∈ Finset.image Subtype.val t, U x ∈ 𝓝ˢ s

Tactic:
rwa [Finset.set_biUnion_finset_image]

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Finset ↑s
ht : ⋃ x ∈ t, U ↑x ∈ 𝓝ˢ s
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s

Tactic:
classical
exact ⟨t.image (↑), fun x hx =>
  let ⟨y, _, hyx⟩ := Finset.mem_image.1 hx
  hyx ▸ y.2,
  by rwa [Finset.set_biUnion_finset_image]⟩

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Finset ↑s
ht : ⋃ x ∈ t, U ↑x ∈ 𝓝ˢ s
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s

Tactic:
exact ⟨t.image (↑), fun x hx =>
  let ⟨y, _, hyx⟩ := Finset.mem_image.1 hx
  hyx ▸ y.2,
  by rwa [Finset.set_biUnion_finset_image]⟩

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s

Tactic:
let ⟨t, ht⟩ := hs.elim_nhds_subcover_nhdsSet' (fun x _ => U x) hU

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Finset ↑s
ht : ⋃ x ∈ t, U ↑x ∈ 𝓝ˢ s
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s
-- Mathlib/Data/Set/Function.lean
lemma SurjOn.comp_left (hf : SurjOn f s t) (g : β → γ) : SurjOn (g ∘ f) s (g '' t)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ g '' t ⊆ g '' (f '' s)

Tactic:
exact image_subset _ hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ SurjOn (g ∘ f) s (g '' t)

Tactic:
rw [SurjOn, image_comp g f]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ g '' t ⊆ g '' (f '' s)
-- Mathlib/Combinatorics/Derangements/Basic.lean
theorem RemoveNone.fiber_none : RemoveNone.fiber (@none α) = ∅

Proof state:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : Perm α), x ∉ fiber none

Tactic:
intro f hyp

Result:
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hyp : f ∈ fiber none
⊢ False

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = none
right✝ : removeNone F = f
⊢ False

Tactic:
exact F_derangement none F_none

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hyp : f ∈ fiber none
⊢ False

Tactic:
rw [RemoveNone.mem_fiber] at hyp

Result:
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hyp : ∃ F ∈ derangements (Option α), F none = none ∧ removeNone F = f
⊢ False

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hyp : ∃ F ∈ derangements (Option α), F none = none ∧ removeNone F = f
⊢ False

Tactic:
rcases hyp with ⟨F, F_derangement, F_none, _⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = none
right✝ : removeNone F = f
⊢ False

Proof state:
α : Type u_1
inst✝ : DecidableEq α
⊢ fiber none = ∅

Tactic:
rw [Set.eq_empty_iff_forall_not_mem]

Result:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : Perm α), x ∉ fiber none
-- Mathlib/Topology/SeparatedMap.lean
protected lemma Topology.IsEmbedding.toPullbackDiag (f : X → Y) : IsEmbedding (toPullbackDiag f) :=
  .mk' _ (injective_toPullbackDiag f) fun x ↦ by
    rw [toPullbackDiag, nhds_induced, Filter.comap_comap, nhds_prod_eq, Filter.comap_prod]
    erw [Filter.comap_id, inf_idem]

Proof state:
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x : X
⊢ Filter.comap (toPullbackDiag f) (𝓝 (toPullbackDiag f x)) = 𝓝 x

Tactic:
rw [toPullbackDiag, nhds_induced, Filter.comap_comap, nhds_prod_eq, Filter.comap_prod]

Result:
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x : X
⊢ Filter.comap (Prod.fst ∘ Subtype.val ∘ toPullbackDiag f) (𝓝 x) ⊓
      Filter.comap (Prod.snd ∘ Subtype.val ∘ toPullbackDiag f) (𝓝 x) =
    𝓝 x

Proof state:
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x : X
⊢ Filter.comap (Prod.fst ∘ Subtype.val ∘ toPullbackDiag f) (𝓝 x) ⊓
      Filter.comap (Prod.snd ∘ Subtype.val ∘ toPullbackDiag f) (𝓝 x) =
    𝓝 x

Tactic:
erw [Filter.comap_id, inf_idem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem toList_swap (a : Array α) (i j : Nat) (hi hj) :
    (a.swap i j hi hj).toList = (a.toList.set i a[j]).set j a[i]

Proof state:
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ (a.swap i j hi hj).toList = (a.toList.set i a[j]).set j a[i]

Tactic:
simp [swap_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem mul_smul_left {i : Int} {xs ys : IntList} : (i * xs) * ys = i * (xs * ys)

Proof state:
case cons.nil
i x : Int
xs : List Int
ih : ∀ {ys : IntList}, i * xs * ys = i * (xs * ys)
⊢ i * (x :: xs) * [] = i * ((x :: xs) * [])

Tactic:
simp

Result:
no goals

Proof state:
i : Int
xs ys : IntList
⊢ i * xs * ys = i * (xs * ys)

Tactic:
induction xs generalizing ys with
| nil => simp
| cons x xs ih =>
  cases ys with
  | nil => simp
  | cons y ys => simp_all [Int.mul_assoc]

Result:
no goals

Proof state:
case nil
i : Int
ys : IntList
⊢ i * [] * ys = i * ([] * ys)

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
i x : Int
xs : List Int
ih : ∀ {ys : IntList}, i * xs * ys = i * (xs * ys)
y : Int
ys : List Int
⊢ i * (x :: xs) * (y :: ys) = i * ((x :: xs) * (y :: ys))

Tactic:
simp_all [Int.mul_assoc]

Result:
no goals

Proof state:
case cons
i x : Int
xs : List Int
ih : ∀ {ys : IntList}, i * xs * ys = i * (xs * ys)
ys : IntList
⊢ i * (x :: xs) * ys = i * ((x :: xs) * ys)

Tactic:
cases ys with
| nil => simp
| cons y ys => simp_all [Int.mul_assoc]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/UV.lean
theorem sup_sdiff_mem_of_mem_compression (ha : a ∈ 𝓒 u v s) (hva : v ≤ a) (hua : Disjoint u a) :
    (a ⊔ u) \ v ∈ s

Proof state:
case inl.intro
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hua : Disjoint u a
left✝ : a ∈ s
ha : (a ⊔ u) \ v ∈ s
⊢ (a ⊔ u) \ v ∈ s

Tactic:
exact ha

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∈ 𝓒 u v s
hva : v ≤ a
hua : Disjoint u a
⊢ (a ⊔ u) \ v ∈ s

Tactic:
rw [mem_compression, compress_of_disjoint_of_le hua hva] at ha

Result:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∈ s ∧ (a ⊔ u) \ v ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
hva : v ≤ a
hua : Disjoint u a
⊢ (a ⊔ u) \ v ∈ s

Proof state:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∈ s ∧ (a ⊔ u) \ v ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
hva : v ≤ a
hua : Disjoint u a
⊢ (a ⊔ u) \ v ∈ s

Tactic:
obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := ha

Result:
case inl.intro
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hua : Disjoint u a
left✝ : a ∈ s
ha : (a ⊔ u) \ v ∈ s
⊢ (a ⊔ u) \ v ∈ s

case inr.intro.intro.intro
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
s : Finset α
u v : α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : compress u v b ∉ s
⊢ (compress u v b ⊔ u) \ v ∈ s
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem conGen_eq (r : M → M → Prop) : conGen r = sInf { s : Con M | ∀ x y, r x y → s x y } :=
  le_antisymm
    (le_sInf (fun s hs x y (hxy : (conGen r) x y) =>
      show s x y by
        apply ConGen.Rel.recOn (motive := fun x y _ => s x y) hxy
        · exact fun x y h => hs x y h
        · exact s.refl'
        · exact fun _ => s.symm'
        · exact fun _ _ => s.trans'
        · exact fun _ _ => s.mul))
    (sInf_le ConGen.Rel.of)

Proof state:
case trans
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → s x y → s y z → s x z

Tactic:
exact fun _ _ => s.trans'

Result:
no goals

Proof state:
case of
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ (x y : M), r x y → s x y

Tactic:
exact fun x y h => hs x y h

Result:
no goals

Proof state:
case refl
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ (x : M), s x x

Tactic:
exact s.refl'

Result:
no goals

Proof state:
case symm
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → s x y → s y x

Tactic:
exact fun _ => s.symm'

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ s x y

Tactic:
apply ConGen.Rel.recOn (motive := fun x y _ => s x y) hxy

Result:
case of
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ (x y : M), r x y → s x y

case refl
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ (x : M), s x x

case symm
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → s x y → s y x

case trans
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → s x y → s y z → s x z

case mul
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → s w x → s y z → s (w * y) (x * z)

Proof state:
case mul
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → s w x → s y z → s (w * y) (x * z)

Tactic:
exact fun _ _ => s.mul

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem le_rpow_inv_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
    x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z

Proof state:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z

Tactic:
rw [← rpow_le_rpow_iff_of_neg _ hx hz, rpow_inv_rpow _ hz.ne] <;> positivity

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma one_add_le_iff : 1 + m ≤ n ↔ m < n

Proof state:
m n : ℕ
⊢ 1 + m ≤ n ↔ m < n

Tactic:
simp only [Nat.add_comm, add_one_le_iff]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_singleton : image₂ f {a} {b} = {f a b}

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
a : α
b : β
⊢ image₂ f {a} {b} = {f a b}

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Pullback.lean
lemma pullbackShiftFunctorAdd'_hom_app :
    (shiftFunctorAdd' _ a₁ a₂ a₃ h).hom.app X =
      (pullbackShiftIso C φ a₃ b₃ h₃).hom.app X ≫
      (shiftFunctorAdd' C b₁ b₂ b₃ (by rw [h₁, h₂, h₃, ← h, φ.map_add])).hom.app X ≫
      (pullbackShiftIso C φ a₂ b₂ h₂).inv.app _ ≫
      (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).inv.app X)

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ 𝟙 ((shiftFunctor (PullbackShift C φ) a₁ ⋙ shiftFunctor (PullbackShift C φ) a₂).obj X) =
    𝟙 ((shiftFunctor (PullbackShift C φ) a₂).obj ((shiftFunctor (PullbackShift C φ) a₁).obj X))

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{?u.31265, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ b₁ + b₂ = b₃

Tactic:
rw [h₁, h₂, h₃, ← h, φ.map_add]

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ a₃ h).hom.app X =
    (pullbackShiftIso C φ a₃ b₃ h₃).hom.app X ≫
      (shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app X ≫
        (pullbackShiftIso C φ a₂ b₂ h₂).inv.app ((shiftFunctor C b₁).obj X) ≫
          (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).inv.app X)

Tactic:
rw [← cancel_epi ((shiftFunctorAdd' _ a₁ a₂ a₃ h).inv.app X), Iso.inv_hom_id_app,
  pullbackShiftFunctorAdd'_inv_app φ X a₁ a₂ a₃ h b₁ b₂ b₃ h₁ h₂ h₃, assoc, assoc, assoc,
  Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app_assoc, Iso.hom_inv_id_app_assoc,
  ← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ 𝟙 ((shiftFunctor (PullbackShift C φ) a₁ ⋙ shiftFunctor (PullbackShift C φ) a₂).obj X) =
    𝟙 ((shiftFunctor (PullbackShift C φ) a₂).obj ((shiftFunctor (PullbackShift C φ) a₁).obj X))