harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem snd_iso_of_left_embedding_range_subset {X Y S : TopCat} {f : X ⟶ S} (hf : IsEmbedding f)
    (g : Y ⟶ S) (H : Set.range g ⊆ Set.range f) : IsIso (pullback.snd f g)

Proof state:
X Y S : TopCat
f : X ⟶ S
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
H : Set.range ⇑(ConcreteCategory.hom g) ⊆ Set.range ⇑(ConcreteCategory.hom f)
esto : ↑(pullback f g) ≃ₜ ↑Y :=
  (Homeomorph.ofIsEmbedding ⇑(ConcreteCategory.hom (pullback.snd f g)) ⋯).trans
    { toFun := Subtype.val, invFun := fun x => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }
⊢ IsIso (pullback.snd f g)

Tactic:
convert (isoOfHomeo esto).isIso_hom

Result:
no goals

Proof state:
X Y S : TopCat
f : X ⟶ S
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
H : Set.range ⇑(ConcreteCategory.hom g) ⊆ Set.range ⇑(ConcreteCategory.hom f)
⊢ IsIso (pullback.snd f g)

Tactic:
let esto : (pullback f g : TopCat) ≃ₜ Y :=
  (Homeomorph.ofIsEmbedding _ (snd_isEmbedding_of_left hf g)).trans
    { toFun := Subtype.val
      invFun := fun x =>
        ⟨x, by
          rw [pullback_snd_range]
          exact ⟨_, (H (Set.mem_range_self x)).choose_spec⟩⟩
      left_inv := fun ⟨_, _⟩ => rfl
      right_inv := fun x => rfl }

Result:
X Y S : TopCat
f : X ⟶ S
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
H : Set.range ⇑(ConcreteCategory.hom g) ⊆ Set.range ⇑(ConcreteCategory.hom f)
esto : ↑(pullback f g) ≃ₜ ↑Y :=
  (Homeomorph.ofIsEmbedding ⇑(ConcreteCategory.hom (pullback.snd f g)) ⋯).trans
    { toFun := Subtype.val, invFun := fun x => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }
⊢ IsIso (pullback.snd f g)

Proof state:
X Y S : TopCat
f : X ⟶ S
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
H : Set.range ⇑(ConcreteCategory.hom g) ⊆ Set.range ⇑(ConcreteCategory.hom f)
x : ↑Y
⊢ x ∈ {y | ∃ x, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}

Tactic:
exact ⟨_, (H (Set.mem_range_self x)).choose_spec⟩

Result:
no goals

Proof state:
X Y S : TopCat
f : X ⟶ S
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
H : Set.range ⇑(ConcreteCategory.hom g) ⊆ Set.range ⇑(ConcreteCategory.hom f)
x : ↑Y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
rw [pullback_snd_range]

Result:
X Y S : TopCat
f : X ⟶ S
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
H : Set.range ⇑(ConcreteCategory.hom g) ⊆ Set.range ⇑(ConcreteCategory.hom f)
x : ↑Y
⊢ x ∈ {y | ∃ x, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem cardFactors_one : Ω 1 = 0

Proof state:
⊢ Ω 1 = 0

Tactic:
simp [cardFactors_apply]

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
private lemma piEquivOfFintype_comp_ofTensorProduct_eq :
    piEquivOfFintype I (fun _ : ι ↦ R) ∘ₗ ofTensorProduct I (ι → R) =
      (TensorProduct.piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).toLinearMap

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
k : ℕ
h : (if j = i then 1 else 0) = ↑(if j = i then 1 else 0) k
⊢ ↑(((AlgebraTensorModule.curry (↑(piEquivOfFintype I fun x => R) ∘ₗ ofTensorProduct I (ι → R))) 1 ∘ₗ
            LinearMap.single R (fun i => R) i)
          1 j)
      k =
    ↑(((AlgebraTensorModule.curry ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)) 1 ∘ₗ
            LinearMap.single R (fun i => R) i)
          1 j)
      k

Tactic:
simpa [Pi.single_apply, -smul_eq_mul, -Algebra.id.smul_eq_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑(piEquivOfFintype I fun x => R) ∘ₗ ofTensorProduct I (ι → R) =
    ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)

Tactic:
ext i j k

Result:
case a.h.h.h.h.h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
k : ℕ
⊢ ↑(((AlgebraTensorModule.curry (↑(piEquivOfFintype I fun x => R) ∘ₗ ofTensorProduct I (ι → R))) 1 ∘ₗ
            LinearMap.single R (fun i => R) i)
          1 j)
      k =
    ↑(((AlgebraTensorModule.curry ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)) 1 ∘ₗ
            LinearMap.single R (fun i => R) i)
          1 j)
      k

Proof state:
case a.h.h.h.h.h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
k : ℕ
⊢ ↑(((AlgebraTensorModule.curry (↑(piEquivOfFintype I fun x => R) ∘ₗ ofTensorProduct I (ι → R))) 1 ∘ₗ
            LinearMap.single R (fun i => R) i)
          1 j)
      k =
    ↑(((AlgebraTensorModule.curry ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)) 1 ∘ₗ
            LinearMap.single R (fun i => R) i)
          1 j)
      k

Tactic:
suffices h : (if j = i then 1 else 0) = (if j = i then 1 else 0 : AdicCompletion I R).val k by
  simpa [Pi.single_apply, -smul_eq_mul, -Algebra.id.smul_eq_mul]

Result:
case a.h.h.h.h.h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
k : ℕ
⊢ (if j = i then 1 else 0) = ↑(if j = i then 1 else 0) k

Proof state:
case a.h.h.h.h.h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
k : ℕ
⊢ (if j = i then 1 else 0) = ↑(if j = i then 1 else 0) k

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
theorem IsSRGWith.card_commonNeighbors_eq_of_not_adj_compl (h : G.IsSRGWith n k ℓ μ) {v w : V}
    (hn : v ≠ w) (hna : ¬Gᶜ.Adj v w) :
    Fintype.card (Gᶜ.commonNeighbors v w) = n - (2 * k - ℓ)

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)

Tactic:
have h2' := hna hn

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Gᶜ.Adj v w
⊢ Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - ℓ)

Tactic:
simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl,
  Set.toFinset_diff, Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Gᶜ.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
⊢ #((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) = n - (2 * k - ℓ)

Tactic:
rwa [← Finset.compl_union, card_compl, h.card_neighborFinset_union_of_adj, ← h.card]

Result:
no goals

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)

Tactic:
simp_rw [compl_neighborFinset_sdiff_inter_eq, sdiff_compl_neighborFinset_inter_eq h2']

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
⊢ #((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) = n - (2 * k - ℓ)

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Gᶜ.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)

Tactic:
simp only [not_and, Classical.not_not, compl_adj] at hna

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)
-- Mathlib/LinearAlgebra/Reflection.lean
/-- A formula for $(r_1 r_2)^m$, where $m$ is an integer. -/
lemma reflection_mul_reflection_zpow (m : ℤ)
    (t : R := f y * g x - 2) (ht : t = f y * g x - 2

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℤ
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
z : M
⊢ ↑((reflection hf * reflection hg) ^ m) z =
    (LinearMap.id +
          (Polynomial.eval t (S R ((m - 2) / 2)) *
              (Polynomial.eval t (S R ((m - 1) / 2)) + Polynomial.eval t (S R ((m - 3) / 2)))) •
            (LinearMap.smulRight (g x • f - g) y - LinearMap.smulRight f x) +
        (Polynomial.eval t (S R ((m - 1) / 2)) *
            (Polynomial.eval t (S R (m / 2)) + Polynomial.eval t (S R ((m - 2) / 2)))) •
          (LinearMap.smulRight (f y • g - f) x - LinearMap.smulRight g y))
      z

Tactic:
simpa using reflection_mul_reflection_zpow_apply hf hg m z t ht

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℤ
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
⊢ ↑((reflection hf * reflection hg) ^ m) =
    LinearMap.id +
        (Polynomial.eval t (S R ((m - 2) / 2)) *
            (Polynomial.eval t (S R ((m - 1) / 2)) + Polynomial.eval t (S R ((m - 3) / 2)))) •
          (LinearMap.smulRight (g x • f - g) y - LinearMap.smulRight f x) +
      (Polynomial.eval t (S R ((m - 1) / 2)) *
          (Polynomial.eval t (S R (m / 2)) + Polynomial.eval t (S R ((m - 2) / 2)))) •
        (LinearMap.smulRight (f y • g - f) x - LinearMap.smulRight g y)

Tactic:
ext z

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℤ
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
z : M
⊢ ↑((reflection hf * reflection hg) ^ m) z =
    (LinearMap.id +
          (Polynomial.eval t (S R ((m - 2) / 2)) *
              (Polynomial.eval t (S R ((m - 1) / 2)) + Polynomial.eval t (S R ((m - 3) / 2)))) •
            (LinearMap.smulRight (g x • f - g) y - LinearMap.smulRight f x) +
        (Polynomial.eval t (S R ((m - 1) / 2)) *
            (Polynomial.eval t (S R (m / 2)) + Polynomial.eval t (S R ((m - 2) / 2)))) •
          (LinearMap.smulRight (f y • g - f) x - LinearMap.smulRight g y))
      z
-- Mathlib/LinearAlgebra/QuadraticForm/Basis.lean
theorem toQuadraticMap_toBilin (Q : QuadraticMap R M N) (bm : Basis ι R M) :
    (Q.toBilin bm).toQuadraticMap = Q

Proof state:
case H.h
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x✝ : M
x : ι × ι
hx : x ∈ (bm.repr x✝).support.offDiag
⊢ ¬x.1 = x.2

Tactic:
rw [Finset.mem_offDiag] at hx

Result:
case H.h
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x✝ : M
x : ι × ι
hx : x.1 ∈ (bm.repr x✝).support ∧ x.2 ∈ (bm.repr x✝).support ∧ x.1 ≠ x.2
⊢ ¬x.1 = x.2

Proof state:
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
⊢ (Q.toBilin bm).toQuadraticMap = Q

Tactic:
ext x

Result:
case H
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (Q.toBilin bm).toQuadraticMap x = Q x

Proof state:
case H
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ((Q.toBilin bm) (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)) (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a) =
    Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)

Tactic:
simp_rw [LinearMap.map_sum₂, map_sum, LinearMap.map_smul₂, _root_.map_smul, toBilin_apply,
  smul_ite, smul_zero, ← Finset.sum_product', ← Finset.diag_union_offDiag,
  Finset.sum_union (Finset.disjoint_diag_offDiag _), Finset.sum_diag, if_true]

Result:
case H
ι : Type u_4
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ x_1 ∈ (bm.repr x).support.offDiag,
        if x_1.1 = x_1.2 then (bm.repr x) x_1.1 • (bm.repr x) x_1.2 • Q (bm x_1.1)
        else if x_1.1 < x_1.2 then (bm.repr x) x_1.1 • (bm.repr x) x_1.2 • polar (⇑Q) (bm x_1.1) (bm x_1.2) else 0) =
    Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)
-- Mathlib/Data/Finsupp/Single.lean
theorem single_zero (a : α) : (single a 0 : α →₀ M) = 0 :=
  DFunLike.coe_injective <| by
    classical simpa only [single_eq_update, coe_zero] using Function.update_eq_self a (0 : α → M)

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
⊢ (fun f => ⇑f) (single a 0) = (fun f => ⇑f) 0

Tactic:
simpa only [single_eq_update, coe_zero] using Function.update_eq_self a (0 : α → M)

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
⊢ (fun f => ⇑f) (single a 0) = (fun f => ⇑f) 0

Tactic:
classical simpa only [single_eq_update, coe_zero] using Function.update_eq_self a (0 : α → M)

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem reindexFinsetRange_self (i : ι) (h := Finset.mem_image_of_mem b (Finset.mem_univ i)) :
    b.reindexFinsetRange ⟨b i, h⟩ = b i

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
h : optParam (b i ∈ Finset.image (⇑b) Finset.univ) ⋯
⊢ ↑(((Equiv.refl M).subtypeEquiv ⋯).symm ⟨b i, h⟩) = b i

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
h : optParam (b i ∈ Finset.image (⇑b) Finset.univ) ⋯
⊢ b.reindexFinsetRange ⟨b i, h⟩ = b i

Tactic:
rw [reindexFinsetRange, reindex_apply, reindexRange_apply]

Result:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
h : optParam (b i ∈ Finset.image (⇑b) Finset.univ) ⋯
⊢ ↑(((Equiv.refl M).subtypeEquiv ⋯).symm ⟨b i, h⟩) = b i
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem balance2_toList {l : RBNode α} {v r} :
    (l.balance2 v r).toList = l.toList ++ v :: r.toList

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balance2 v r).toList = l.toList ++ v :: r.toList

Tactic:
unfold balance2

Result:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (match l, v, r with
      | a, x, node red b y (node red c z d) => node red (node black a x b) y (node black c z d)
      | a, x, node red (node red b y c) z d => node red (node black a x b) y (node black c z d)
      | a, x, b => node black a x b).toList =
    l.toList ++ v :: r.toList

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (match l, v, r with
      | a, x, node red b y (node red c z d) => node red (node black a x b) y (node black c z d)
      | a, x, node red (node red b y c) z d => node red (node black a x b) y (node black c z d)
      | a, x, b => node black a x b).toList =
    l.toList ++ v :: r.toList

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getMsbD_add {i : Nat} {i_lt : i < w} {x y : BitVec w} :
    getMsbD (x + y) i =
      Bool.xor (getMsbD x i) (Bool.xor (getMsbD y i) (carry (w - 1 - i) x y false))

Proof state:
w i : Nat
i_lt : i < w
x y : BitVec w
⊢ w - 1 - i < w

Tactic:
omega

Result:
no goals

Proof state:
w i : Nat
i_lt : i < w
x y : BitVec w
⊢ (x + y).getMsbD i = (x.getMsbD i ^^ (y.getMsbD i ^^ carry (w - 1 - i) x y false))

Tactic:
simp [getMsbD, getLsbD_add, i_lt, show w - 1 - i < w by omega]

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
lemma toRight_image_swap : (u.image Sum.swap).toRight = u.toLeft

Proof state:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (image Sum.swap u).toRight = u.toLeft

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (image Sum.swap u).toRight ↔ x ∈ u.toLeft

Proof state:
case h
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (image Sum.swap u).toRight ↔ x ∈ u.toLeft

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : map f l₁ <+ map f l₂

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
ih : map f l₁✝ <+ map f l₂✝
⊢ map f l₁✝ <+ map f (a :: l₂✝)

Tactic:
simpa using cons (f a) ih

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ : List α
s : l₁ <+ l₂
⊢ map f l₁ <+ map f l₂

Tactic:
induction s with
| slnil => simp
| cons a s ih =>
  simpa using cons (f a) ih
| cons₂ a s ih =>
  simpa using cons₂ (f a) ih

Result:
no goals

Proof state:
case slnil
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ : List α
⊢ map f [] <+ map f []

Tactic:
simp

Result:
no goals

Proof state:
case cons₂
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
ih : map f l₁✝ <+ map f l₂✝
⊢ map f (a :: l₁✝) <+ map f (a :: l₂✝)

Tactic:
simpa using cons₂ (f a) ih

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem adjoin_simple_eq_bot_iff : F⟮α⟯ = ⊥ ↔ α ∈ (⊥ : IntermediateField F E)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ F⟮α⟯ = ⊥ ↔ α ∈ ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/IsConnected.lean
theorem isConnected_of_equivalent {K : Type u₂} [Category.{v₂} K] (e : J ≌ K) [IsConnected J] :
    IsConnected K :=
  { is_nonempty := Nonempty.map e.functor.obj (by infer_instance)
    toIsPreconnected := isPreconnected_of_equivalent e }

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
e : J ≌ K
inst✝ : IsConnected J
⊢ Nonempty J

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_dropLast (f : α → β) (l : List α) : l.dropLast.map f = (l.map f).dropLast

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
x : α
xs : List α
ih : map f xs.dropLast = (map f xs).dropLast
⊢ map f (x :: xs).dropLast = (map f (x :: xs)).dropLast

Tactic:
cases xs <;> simp [ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l.dropLast = (map f l).dropLast

Tactic:
induction l with
| nil => rfl
| cons x xs ih => cases xs <;> simp [ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ map f [].dropLast = (map f []).dropLast

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_comp_mul_deriv'' {f f' g : ℝ → ℝ} (hf : ContinuousOn f [[a, b]])
    (hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x)
    (hf' : ContinuousOn f' [[a, b]]) (hg : ContinuousOn g (f '' [[a, b]])) :
    (∫ x in a..b, (g ∘ f) x * f' x) = ∫ u in f a..f b, g u

Proof state:
a b : ℝ
f f' g : ℝ → ℝ
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g (f '' [[a, b]])
⊢ ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
simpa [mul_comm] using integral_comp_smul_deriv'' hf hff' hf' hg

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem iterateFrobeniusEquiv_symm :
    (iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n

Proof state:
R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ (iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n

Tactic:
rw [iterateFrobeniusEquiv_eq_pow]

Result:
R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ (frobeniusEquiv R p ^ n).symm = (frobeniusEquiv R p).symm ^ n

Proof state:
R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ (frobeniusEquiv R p ^ n).symm = (frobeniusEquiv R p).symm ^ n

Tactic:
exact (inv_pow _ _).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem isHashSelf_replaceₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β)
    (h : Raw.WFImp m.1) (a : α) (b : β a) : IsHashSelf (m.replaceₘ a b).1.buckets

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
l : AssocList α β
p : (a : α) × β a
hp : p ∈ (AssocList.replace a b l).toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
exact Or.inl (by simpa using containsKey_of_mem hp)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ IsHashSelf (m.replaceₘ a b).val.buckets

Tactic:
apply h.buckets_hash_self.updateBucket (fun l p hp => ?_)

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
l : AssocList α β
p : (a : α) × β a
hp : p ∈ (AssocList.replace a b l).toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
l : AssocList α β
p : (a : α) × β a
hp : p ∈ (AssocList.replace a b l).toList
⊢ containsKey p.fst l.toList = true

Tactic:
simpa using containsKey_of_mem hp

Result:
no goals