harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
theorem denote_bitblast (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦(bitblast aig expr).aig, (bitblast aig expr).vec.get idx hidx, assign.toAIGAssignment⟧
          =
        (expr.eval assign).getLsbD idx

Proof state:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign.toAIGAssignment,
      { aig := (bitblast.go aig expr).val.aig, ref := (bitblast.go aig expr).val.vec.get idx✝ hidx✝ }⟧ =
    (eval assign expr).getLsbD idx✝

Tactic:
rw [bitblast.go_denote_eq]

Result:
no goals

Proof state:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := (bitblast aig expr).aig, ref := (bitblast aig expr).vec.get idx hidx }⟧ =
      (eval assign expr).getLsbD idx

Tactic:
intros

Result:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign.toAIGAssignment, { aig := (bitblast aig expr).aig, ref := (bitblast aig expr).vec.get idx✝ hidx✝ }⟧ =
    (eval assign expr).getLsbD idx✝

Proof state:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign.toAIGAssignment, { aig := (bitblast aig expr).aig, ref := (bitblast aig expr).vec.get idx✝ hidx✝ }⟧ =
    (eval assign expr).getLsbD idx✝

Tactic:
rw [← bitblast.go_val_eq_bitblast]

Result:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign.toAIGAssignment,
      { aig := (bitblast.go aig expr).val.aig, ref := (bitblast.go aig expr).val.vec.get idx✝ hidx✝ }⟧ =
    (eval assign expr).getLsbD idx✝
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobjectIsoComp_inv_arrow {X' : C} (f : X' ⟶ X) [IsIso f] (g : X ⟶ Y) [HasKernel g] :
    (kernelSubobjectIsoComp f g).inv ≫ (kernelSubobject (f ≫ g)).arrow =
      (kernelSubobject g).arrow ≫ inv f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasZeroMorphisms C
X' : C
f : X' ⟶ X
inst✝¹ : IsIso f
g : X ⟶ Y
inst✝ : HasKernel g
⊢ (kernelSubobjectIsoComp f g).inv ≫ (kernelSubobject (f ≫ g)).arrow = (kernelSubobject g).arrow ≫ inv f

Tactic:
simp [kernelSubobjectIsoComp]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem Complex.map_isometryOfOrthonormal (v : OrthonormalBasis (Fin 2) ℝ F) (f : F ≃ₗᵢ[ℝ] F') :
    Complex.isometryOfOrthonormal (v.map f) = (Complex.isometryOfOrthonormal v).trans f

Proof state:
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
F' : Type u_6
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
v : OrthonormalBasis (Fin 2) ℝ F
f : F ≃ₗᵢ[ℝ] F'
⊢ orthonormalBasisOneI.repr.trans (v.repr.symm.trans f) = (orthonormalBasisOneI.repr.trans v.repr.symm).trans f

Tactic:
rw [LinearIsometryEquiv.trans_assoc]

Result:
no goals

Proof state:
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
F' : Type u_6
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
v : OrthonormalBasis (Fin 2) ℝ F
f : F ≃ₗᵢ[ℝ] F'
⊢ isometryOfOrthonormal (v.map f) = (isometryOfOrthonormal v).trans f

Tactic:
simp only [isometryOfOrthonormal, OrthonormalBasis.map, LinearIsometryEquiv.symm_trans,
  LinearIsometryEquiv.symm_symm]

Result:
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
F' : Type u_6
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
v : OrthonormalBasis (Fin 2) ℝ F
f : F ≃ₗᵢ[ℝ] F'
⊢ orthonormalBasisOneI.repr.trans (v.repr.symm.trans f) = (orthonormalBasisOneI.repr.trans v.repr.symm).trans f
-- Mathlib/Control/Monad/Cont.lean
theorem StateT.goto_mkLabel {α β σ : Type u} (x : Label (α × σ) m (β × σ)) (i : α) :
    goto (StateT.mkLabel x) i = StateT.mk (fun s => goto x (i, s))

Proof state:
m : Type u → Type v
α β σ : Type u
x : Label (α × σ) m (β × σ)
i : α
⊢ goto (mkLabel x) i = StateT.mk fun s => goto x (i, s)

Tactic:
cases x

Result:
case mk
m : Type u → Type v
α β σ : Type u
i : α
apply✝ : α × σ → m (β × σ)
⊢ goto (mkLabel { apply := apply✝ }) i = StateT.mk fun s => goto { apply := apply✝ } (i, s)

Proof state:
case mk
m : Type u → Type v
α β σ : Type u
i : α
apply✝ : α × σ → m (β × σ)
⊢ goto (mkLabel { apply := apply✝ }) i = StateT.mk fun s => goto { apply := apply✝ } (i, s)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Algebra/Tower.lean
theorem Algebra.ext {S : Type u} {A : Type v} [CommSemiring S] [Semiring A] (h1 h2 : Algebra S A)
    (h : ∀ (r : S) (x : A), (by have I := h1; exact r • x) = r • x) : h1 = h2 :=
  Algebra.algebra_ext _ _ fun r => by
    simpa only [@Algebra.smul_def _ _ _ _ h1, @Algebra.smul_def _ _ _ _ h2, mul_one] using h r 1

Proof state:
R : Type u
S✝ : Type v
A✝ : Type w
B : Type u₁
M : Type v₁
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S✝
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S✝
inst✝⁷ : Algebra S✝ A✝
inst✝⁶ : Algebra S✝ B
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R S✝ A✝
inst✝² : IsScalarTower R S✝ B
S : Type u
A : Type v
inst✝¹ : CommSemiring S
inst✝ : Semiring A
h1 h2 : Algebra S A
r : S
x : A
⊢ A

Tactic:
have I := h1

Result:
R : Type u
S✝ : Type v
A✝ : Type w
B : Type u₁
M : Type v₁
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S✝
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S✝
inst✝⁷ : Algebra S✝ A✝
inst✝⁶ : Algebra S✝ B
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R S✝ A✝
inst✝² : IsScalarTower R S✝ B
S : Type u
A : Type v
inst✝¹ : CommSemiring S
inst✝ : Semiring A
h1 h2 : Algebra S A
r : S
x : A
I : Algebra S A
⊢ A

Proof state:
R : Type u
S✝ : Type v
A✝ : Type w
B : Type u₁
M : Type v₁
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S✝
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S✝
inst✝⁷ : Algebra S✝ A✝
inst✝⁶ : Algebra S✝ B
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R S✝ A✝
inst✝² : IsScalarTower R S✝ B
S : Type u
A : Type v
inst✝¹ : CommSemiring S
inst✝ : Semiring A
h1 h2 : Algebra S A
r : S
x : A
I : Algebra S A
⊢ A

Tactic:
exact r • x

Result:
no goals

Proof state:
S : Type u
A : Type v
inst✝¹ : CommSemiring S
inst✝ : Semiring A
h1 h2 : Algebra S A
h :
  ∀ (r : S) (x : A),
    (let_fun I := h1;
      r • x) =
      r • x
r : S
⊢ (algebraMap S A) r = (algebraMap S A) r

Tactic:
simpa only [@Algebra.smul_def _ _ _ _ h1, @Algebra.smul_def _ _ _ _ h2, mul_one] using h r 1

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem not_isMin_succ [Nontrivial α] (a : α) : ¬ IsMin (succ a)

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : Nontrivial α
a : α
⊢ ¬IsMin (succ a)

Tactic:
obtain ha | ha := (le_succ a).eq_or_lt

Result:
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : Nontrivial α
a : α
ha : a = succ a
⊢ ¬IsMin (succ a)

case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : Nontrivial α
a : α
ha : a < succ a
⊢ ¬IsMin (succ a)

Proof state:
case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : Nontrivial α
a : α
ha : a < succ a
⊢ ¬IsMin (succ a)

Tactic:
exact not_isMin_of_lt ha

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : Nontrivial α
a : α
ha : a = succ a
⊢ ¬IsMin (succ a)

Tactic:
exact (ha ▸ succ_eq_iff_isMax.1 ha.symm).not_isMin

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem modifyKey_eq_alterKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β k)
    (l : List ((a : α) × β a)) : modifyKey k f l = alterKey k (·.map f) l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
⊢ (match getValueCast? k l with
    | none => l
    | some v => replaceEntry k (f v) l) =
    match
      match getValueCast? k l with
      | some x => some (f x)
      | none => none with
    | none => eraseKey k l
    | some v => insertEntry k v l

Tactic:
split <;> next h =>
  simp [h, insertEntry, containsKey_eq_isSome_getValueCast?, eraseKey_of_containsKey_eq_false]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
⊢ modifyKey k f l = alterKey k (fun x => Option.map f x) l

Tactic:
rw [modifyKey, alterKey, Option.map.eq_def]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
⊢ (match getValueCast? k l with
    | none => l
    | some v => replaceEntry k (f v) l) =
    match
      match getValueCast? k l with
      | some x => some (f x)
      | none => none with
    | none => eraseKey k l
    | some v => insertEntry k v l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
x✝ : Option (β k)
v✝ : β k
h : getValueCast? k l = some v✝
⊢ replaceEntry k (f v✝) l =
    match
      match getValueCast? k l with
      | some x => some (f x)
      | none => none with
    | none => eraseKey k l
    | some v => insertEntry k v l

Tactic:
simp [h, insertEntry, containsKey_eq_isSome_getValueCast?, eraseKey_of_containsKey_eq_false]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem ContDiffWithinAt.dist (hf : ContDiffWithinAt ℝ n f s x) (hg : ContDiffWithinAt ℝ n g s x)
    (hne : f x ≠ g x) : ContDiffWithinAt ℝ n (fun y => dist (f y) (g y)) s x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
s : Set G
x : G
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
hg : ContDiffWithinAt ℝ n g s x
hne : f x ≠ g x
⊢ ContDiffWithinAt ℝ n (fun y => Dist.dist (f y) (g y)) s x

Tactic:
simp only [dist_eq_norm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
s : Set G
x : G
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
hg : ContDiffWithinAt ℝ n g s x
hne : f x ≠ g x
⊢ ContDiffWithinAt ℝ n (fun y => ‖f y - g y‖) s x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
s : Set G
x : G
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
hg : ContDiffWithinAt ℝ n g s x
hne : f x ≠ g x
⊢ ContDiffWithinAt ℝ n (fun y => ‖f y - g y‖) s x

Tactic:
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem _root_.Summable.countable_support_nnreal (f : α → ℝ≥0) (h : Summable f) :
    f.support.Countable

Proof state:
α : Type u_1
f : α → ℝ≥0
h : Summable fun a => ↑(f a)
⊢ (support f).Countable

Tactic:
simpa [support] using h.countable_support

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ≥0
h : Summable f
⊢ (support f).Countable

Tactic:
rw [← NNReal.summable_coe] at h

Result:
α : Type u_1
f : α → ℝ≥0
h : Summable fun a => ↑(f a)
⊢ (support f).Countable
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem Right.one_le_inv_iff : 1 ≤ a⁻¹ ↔ a ≤ 1

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ 1 * a ≤ a⁻¹ * a ↔ a ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
rw [← mul_le_mul_iff_right a]

Result:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ 1 * a ≤ a⁻¹ * a ↔ a ≤ 1
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem mem_span_image_iff_linearCombination {s : Set α} {x : M} :
    x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, linearCombination R v l = x

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
⊢ x ∈ map (linearCombination R v) (supported R R s) ↔ ∃ l ∈ supported R R s, (linearCombination R v) l = x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
⊢ x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, (linearCombination R v) l = x

Tactic:
rw [span_image_eq_map_linearCombination]

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
⊢ x ∈ map (linearCombination R v) (supported R R s) ↔ ∃ l ∈ supported R R s, (linearCombination R v) l = x
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- `t` is in the upper shadow of `𝒜` iff `t` is exactly one element less than something from `𝒜`.

See also `Finset.mem_upShadow_iff_exists_sdiff`. -/
lemma mem_upShadow_iff_exists_mem_card_add_one :
    t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + 1

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + 1

Tactic:
refine mem_upShadow_iff_exists_sdiff.trans <| exists_congr fun t ↦ and_congr_right fun _ ↦
  and_congr_right fun hst ↦ ?_

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #(t✝ \ t) = 1 ↔ #t✝ = #t + 1

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t ≤ #t✝

Tactic:
exact card_mono hst

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #(t✝ \ t) = 1 ↔ #t✝ = #t + 1

Tactic:
rw [card_sdiff hst, tsub_eq_iff_eq_add_of_le, add_comm]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t ≤ #t✝
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem inclusion.injective {x y : Subgraph G} (h : x ≤ y) : Function.Injective (inclusion h)

Proof state:
V : Type u
G : SimpleGraph V
x y : G.Subgraph
h✝ : x ≤ y
v w : ↑x.verts
h : (inclusion h✝) v = (inclusion h✝) w
⊢ v = w

Tactic:
rw [inclusion, DFunLike.coe, Subtype.mk_eq_mk] at h

Result:
V : Type u
G : SimpleGraph V
x y : G.Subgraph
h✝ : x ≤ y
v w : ↑x.verts
h :
  ↑(RelHom.instFunLike.1 { toFun := fun v => ⟨↑v, ⋯⟩, map_rel' := ⋯ } v) =
    ↑(RelHom.instFunLike.1 { toFun := fun v => ⟨↑v, ⋯⟩, map_rel' := ⋯ } w)
⊢ v = w

Proof state:
V : Type u
G : SimpleGraph V
x y : G.Subgraph
h : x ≤ y
⊢ Function.Injective ⇑(inclusion h)

Tactic:
intro v w h

Result:
V : Type u
G : SimpleGraph V
x y : G.Subgraph
h✝ : x ≤ y
v w : ↑x.verts
h : (inclusion h✝) v = (inclusion h✝) w
⊢ v = w

Proof state:
V : Type u
G : SimpleGraph V
x y : G.Subgraph
h✝ : x ≤ y
v w : ↑x.verts
h :
  ↑(RelHom.instFunLike.1 { toFun := fun v => ⟨↑v, ⋯⟩, map_rel' := ⋯ } v) =
    ↑(RelHom.instFunLike.1 { toFun := fun v => ⟨↑v, ⋯⟩, map_rel' := ⋯ } w)
⊢ v = w

Tactic:
exact Subtype.ext h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem unzip_eq_unzipTR : @unzip = @unzipTR

Proof state:
case h.h.h
α : Type u_2
β : Type u_1
⊢ ∀ (x : List (α × β)), x.unzip = x.unzipTR

Tactic:
intro l

Result:
case h.h.h
α : Type u_2
β : Type u_1
l : List (α × β)
⊢ l.unzip = l.unzipTR

Proof state:
case h

⊢ ∀ (x : Type u_2), @unzip x = @unzipTR x

Tactic:
intro α

Result:
case h
α : Type u_2
⊢ @unzip α = @unzipTR α

Proof state:
case h.h
α : Type u_2
⊢ ∀ (x : Type u_1), unzip = unzipTR

Tactic:
intro β

Result:
case h.h
α : Type u_2
β : Type u_1
⊢ unzip = unzipTR

Proof state:
case h.h
α : Type u_2
β : Type u_1
⊢ unzip = unzipTR

Tactic:
apply funext

Result:
case h.h.h
α : Type u_2
β : Type u_1
⊢ ∀ (x : List (α × β)), x.unzip = x.unzipTR

Proof state:
case h.h.h
α : Type u_2
β : Type u_1
l : List (α × β)
⊢ l.unzip = foldr (fun x x_1 => { fst := x.fst :: x_1.fst, snd := x.snd :: x_1.snd }) { fst := nil, snd := nil } l

Tactic:
induction l <;> simp [*]

Result:
no goals

Proof state:
case h.h.h
α : Type u_2
β : Type u_1
l : List (α × β)
⊢ l.unzip = l.unzipTR

Tactic:
simp [unzipTR]

Result:
case h.h.h
α : Type u_2
β : Type u_1
l : List (α × β)
⊢ l.unzip = foldr (fun x x_1 => { fst := x.fst :: x_1.fst, snd := x.snd :: x_1.snd }) { fst := nil, snd := nil } l

Proof state:
⊢ @unzip = @unzipTR

Tactic:
apply funext

Result:
case h

⊢ ∀ (x : Type u_2), @unzip x = @unzipTR x

Proof state:
case h
α : Type u_2
⊢ @unzip α = @unzipTR α

Tactic:
apply funext

Result:
case h.h
α : Type u_2
⊢ ∀ (x : Type u_1), unzip = unzipTR
-- Mathlib/Data/List/Perm/Basic.lean
theorem perm_comp_perm : (Perm ∘r Perm : List α → List α → Prop) = Perm

Proof state:
case h.h
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c = (a ~ c)

Tactic:
apply propext

Result:
case h.h.a
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c ↔ a ~ c

Proof state:
case h.h.a
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c ↔ a ~ c

Tactic:
constructor

Result:
case h.h.a.mp
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c → a ~ c

case h.h.a.mpr
α : Type u_1
a c : List α
⊢ a ~ c → (Perm ∘r Perm) a c

Proof state:
case h.h.a.mpr
α : Type u_1
a c : List α
⊢ a ~ c → (Perm ∘r Perm) a c

Tactic:
exact fun h => ⟨a, Perm.refl a, h⟩

Result:
no goals

Proof state:
α : Type u_1
⊢ Perm ∘r Perm = Perm

Tactic:
funext a c

Result:
case h.h
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c = (a ~ c)

Proof state:
case h.h.a.mp
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c → a ~ c

Tactic:
exact fun ⟨b, hab, hba⟩ => Perm.trans hab hba

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
@[simp] lemma zmod_zero : zmod n 0 = 1 :=
  DFunLike.ext _ _ <| by simp [ZMod.intCast_surjective.forall, zmod]

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ ∀ (x : ZMod n), (zmod n 0) x = 1 x

Tactic:
simp [ZMod.intCast_surjective.forall, zmod]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
theorem adjoin_toSubalgebra_of_isAlgebraic (L : IntermediateField F K)
    (halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F L) :
    (adjoin E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K)

Proof state:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i
hi : ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'
⊢ Subalgebra.restrictScalars F (adjoin E ↑L).toSubalgebra = Subalgebra.restrictScalars F (Algebra.adjoin E ↑L)

Tactic:
erw [← restrictScalars_toSubalgebra, restrictScalars_adjoin_of_algEquiv i' hi,
  Algebra.restrictScalars_adjoin_of_algEquiv i' hi, restrictScalars_adjoin,
  Algebra.restrictScalars_adjoin]

Result:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i
hi : ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'
⊢ (adjoin F (↑E' ∪ ↑L)).toSubalgebra = Algebra.adjoin F (↑E'.toSubalgebra ∪ ↑L)
-- Mathlib/Analysis/Convex/Cone/InnerDual.lean
theorem innerDualCone_iUnion {ι : Sort*} (f : ι → Set H) :
    (⋃ i, f i).innerDualCone = ⨅ i, (f i).innerDualCone

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
ι : Sort u_2
f : ι → Set H
x : H
hx : x ∈ ⨅ i, (f i).innerDualCone
y : H
hy : y ∈ ⋃ i, f i
⊢ 0 ≤ inner y x

Tactic:
rw [ConvexCone.mem_iInf] at hx

Result:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
ι : Sort u_2
f : ι → Set H
x : H
hx : ∀ (i : ι), x ∈ (f i).innerDualCone
y : H
hy : y ∈ ⋃ i, f i
⊢ 0 ≤ inner y x

Proof state:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
ι : Sort u_2
f : ι → Set H
x : H
hx : ∀ (i : ι), x ∈ (f i).innerDualCone
y : H
hy : y ∈ ⋃ i, f i
j : ι
hj : y ∈ f j
⊢ 0 ≤ inner y x

Tactic:
exact hx _ _ hj

Result:
no goals

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
ι : Sort u_2
f : ι → Set H
x : H
hx : ∀ (i : ι), x ∈ (f i).innerDualCone
y : H
hy : y ∈ ⋃ i, f i
⊢ 0 ≤ inner y x

Tactic:
obtain ⟨j, hj⟩ := mem_iUnion.mp hy

Result:
case intro
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
ι : Sort u_2
f : ι → Set H
x : H
hx : ∀ (i : ι), x ∈ (f i).innerDualCone
y : H
hy : y ∈ ⋃ i, f i
j : ι
hj : y ∈ f j
⊢ 0 ≤ inner y x

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
ι : Sort u_2
f : ι → Set H
⊢ ⨅ i, (f i).innerDualCone ≤ (⋃ i, f i).innerDualCone

Tactic:
intro x hx y hy

Result:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
ι : Sort u_2
f : ι → Set H
x : H
hx : x ∈ ⨅ i, (f i).innerDualCone
y : H
hy : y ∈ ⋃ i, f i
⊢ 0 ≤ inner y x

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
ι : Sort u_2
f : ι → Set H
⊢ (⋃ i, f i).innerDualCone = ⨅ i, (f i).innerDualCone

Tactic:
refine le_antisymm (le_iInf fun i x hx y hy => hx _ <| mem_iUnion_of_mem _ hy) ?_

Result:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
ι : Sort u_2
f : ι → Set H
⊢ ⨅ i, (f i).innerDualCone ≤ (⋃ i, f i).innerDualCone
-- Mathlib/Computability/Tape.lean
theorem Tape.map_write {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (b : Γ) :
    ∀ T : Tape Γ, (T.write b).map f = (T.map f).write (f b)

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
b : Γ
⊢ ∀ (T : Tape Γ), map f (write b T) = write (f.f b) (map f T)

Tactic:
rintro ⟨⟩

Result:
case mk
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
b head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ map f (write b { head := head✝, left := left✝, right := right✝ }) =
    write (f.f b) (map f { head := head✝, left := left✝, right := right✝ })

Proof state:
case mk
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
b head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ map f (write b { head := head✝, left := left✝, right := right✝ }) =
    write (f.f b) (map f { head := head✝, left := left✝, right := right✝ })

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
@[simp]
lemma attachWith_map_subtypeVal {s : Sym2 α} {P : α → Prop} (h : ∀ a ∈ s, P a) :
    (s.attachWith h).map Subtype.val = s

Proof state:
case h
α : Type u_1
P : α → Prop
x y : α
h : ∀ a ∈ s(x, y), P a
⊢ map Subtype.val (s(x, y).attachWith h) = s(x, y)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
s : Sym2 α
P : α → Prop
h : ∀ a ∈ s, P a
⊢ map Subtype.val (s.attachWith h) = s

Tactic:
induction' s with x y

Result:
case h
α : Type u_1
P : α → Prop
x y : α
h : ∀ a ∈ s(x, y), P a
⊢ map Subtype.val (s(x, y).attachWith h) = s(x, y)
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem monomial_zero_eq_C : ⇑(monomial R 0) = C R

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ ⇑(monomial R 0) = ⇑(C R)

Tactic:
rw [monomial, Finsupp.single_zero, MvPowerSeries.monomial_zero_eq_C]

Result:
R : Type u_1
inst✝ : Semiring R
⊢ ⇑(MvPowerSeries.C Unit R) = ⇑(C R)

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ ⇑(MvPowerSeries.C Unit R) = ⇑(C R)

Tactic:
rfl

Result:
no goals