harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/VectorField.lean
/-- The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]`. -/
lemma leibniz_identity_lieBracket (hn : minSmoothness 𝕜 2 ≤ n) {U V W : E → E} {x : E}
    (hU : ContDiffAt 𝕜 n U x) (hV : ContDiffAt 𝕜 n V x) (hW : ContDiffAt 𝕜 n W x) :
    lieBracket 𝕜 U (lieBracket 𝕜 V W) x =
      lieBracket 𝕜 (lieBracket 𝕜 U V) W x + lieBracket 𝕜 V (lieBracket 𝕜 U W) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
x : E
hU : ContDiffWithinAt 𝕜 n U univ x
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
⊢ x ∈ closure (interior univ)

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
x : E
hU : ContDiffAt 𝕜 n U x
hV : ContDiffAt 𝕜 n V x
hW : ContDiffAt 𝕜 n W x
⊢ lieBracket 𝕜 U (lieBracket 𝕜 V W) x = lieBracket 𝕜 (lieBracket 𝕜 U V) W x + lieBracket 𝕜 V (lieBracket 𝕜 U W) x

Tactic:
simp only [← lieBracketWithin_univ, ← contDiffWithinAt_univ] at hU hV hW ⊢

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
x : E
hU : ContDiffWithinAt 𝕜 n U univ x
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
⊢ lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W univ) univ x =
    lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V univ) W univ x +
      lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W univ) univ x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
x : E
hU : ContDiffWithinAt 𝕜 n U univ x
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
⊢ lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W univ) univ x =
    lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V univ) W univ x +
      lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W univ) univ x

Tactic:
exact leibniz_identity_lieBracketWithin hn uniqueDiffOn_univ (by simp) (mem_univ _) hU hV hW

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem induction_of_closure_eq_top_left {s : Set M} {p : M → Prop} (hs : closure s = ⊤) (x : M)
    (one : p 1) (mul : ∀ x ∈ s, ∀ (y), p y → p (x * y)) : p x

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
one : p 1
mul : ∀ x ∈ s, ∀ (y : M), p y → p (x * y)
⊢ x ∈ closure s

Tactic:
simp [hs]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
one : p 1
mul : ∀ x ∈ s, ∀ (y : M), p y → p (x * y)
⊢ p x

Tactic:
have : x ∈ closure s := by simp [hs]

Result:
M : Type u_1
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
one : p 1
mul : ∀ x ∈ s, ∀ (y : M), p y → p (x * y)
this : x ∈ closure s
⊢ p x

Proof state:
case mul_left
M : Type u_1
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x✝ : M
one : p 1
mul : ∀ x ∈ s, ∀ (y : M), p y → p (x * y)
x : M
hx : x ∈ s
y : M
hy✝ : y ∈ closure s
ih : p y
⊢ p (x * y)

Tactic:
exact mul x hx y ih

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
one : p 1
mul : ∀ x ∈ s, ∀ (y : M), p y → p (x * y)
this : x ∈ closure s
⊢ p x

Tactic:
induction this using closure_induction_left with
| one => exact one
| mul_left x hx y _ ih => exact mul x hx y ih

Result:
no goals

Proof state:
case one
M : Type u_1
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
one : p 1
mul : ∀ x ∈ s, ∀ (y : M), p y → p (x * y)
⊢ p 1

Tactic:
exact one

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem mul_right_eq_one (x : tsze R M) (r : R) (h : x.fst * r = 1) :
    x * (inl r + inr (-(r •> (x.snd <• r)))) = 1

Proof state:
case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ x.fst •> (0 + -(r •> (x.snd <• r))) + (op r + 0) •> x.snd = 0

Tactic:
rw [add_zero, zero_add, smul_neg, smul_smul, h, one_smul, neg_add_cancel]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ x * (inl r + inr (-(r •> (x.snd <• r)))) = 1

Tactic:
ext <;> dsimp

Result:
case h1
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ x.fst * (r + 0) = 1

case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ x.fst •> (0 + -(r •> (x.snd <• r))) + (op r + 0) •> x.snd = 0

Proof state:
case h1
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ x.fst * (r + 0) = 1

Tactic:
rw [add_zero, h]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean
@[simp]
lemma map_self : IsCartesian.map p f φ φ = 𝟙 a

Proof state:
case map.hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCartesian (p.map φ) φ
⊢ 𝟙 a✝ ≫ φ = φ

Tactic:
simp only [id_comp]

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
⊢ IsCartesian.map p f φ φ = 𝟙 a

Tactic:
subst_hom_lift p f φ

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCartesian (p.map φ) φ
⊢ IsCartesian.map p (p.map φ) φ φ = 𝟙 a✝

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCartesian (p.map φ) φ
⊢ 𝟙 a✝ = IsCartesian.map p (p.map φ) φ φ

Tactic:
apply map_uniq

Result:
case map.hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCartesian (p.map φ) φ
⊢ 𝟙 a✝ ≫ φ = φ

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCartesian (p.map φ) φ
⊢ IsCartesian.map p (p.map φ) φ φ = 𝟙 a✝

Tactic:
symm

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCartesian (p.map φ) φ
⊢ 𝟙 a✝ = IsCartesian.map p (p.map φ) φ φ
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
theorem denote_blastAdd (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
      (input : BinaryRefVec aig w)
      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
      ∀ (idx : Nat) (hidx : idx < w),
          ⟦(blastAdd aig input).aig, (blastAdd aig input).vec.get idx hidx, assign⟧
            =
          (lhs + rhs).getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign, { aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.get idx✝ hidx✝ }⟧ = rhs.getLsbD idx✝

Tactic:
simp only [BinaryRefVec.rhs_get_cast, Ref.cast_eq]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign, { aig := (aig.mkConstCached false).aig, ref := { gate := (input.rhs.get idx✝ hidx✝).gate, hgate := ⋯ } }⟧ =
    rhs.getLsbD idx✝

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (blastAdd aig input).aig, ref := (blastAdd aig input).vec.get idx hidx }⟧ =
    (⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ ^^ (rhs.getLsbD idx ^^ BitVec.carry idx lhs rhs false))

Tactic:
rw [← hright idx hidx]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (blastAdd aig input).aig, ref := (blastAdd aig input).vec.get idx hidx }⟧ =
    (⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ ^^
      (⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ ^^ BitVec.carry idx lhs rhs false))
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_pi_eq_bot {I : Set ι} {s : ∀ i, Set (π i)} {x : ∀ i, π i} :
    𝓝[pi I s] x = ⊥ ↔ ∃ i ∈ I, 𝓝[s i] x i = ⊥

Proof state:
ι : Type u_5
π : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (π i)
I : Set ι
s : (i : ι) → Set (π i)
x : (i : ι) → π i
⊢ 𝓝[I.pi s] x = ⊥ ↔ ∃ i ∈ I, 𝓝[s i] x i = ⊥

Tactic:
simp only [nhdsWithin, nhds_pi, pi_inf_principal_pi_eq_bot]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_zero (l : List α) : l.rotate 0 = l

Proof state:
α : Type u
l : List α
⊢ l.rotate 0 = l

Tactic:
simp [rotate]

Result:
no goals
-- Mathlib/Order/OrderIsoNat.lean
theorem WellFounded.iSup_eq_monotonicSequenceLimit [CompleteLattice α]
    (h : WellFounded ((· > ·) : α → α → Prop)) (a : ℕ →o α) :
    iSup a = monotonicSequenceLimit a

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x1 x2 => x1 > x2
a : ℕ →o α
this : WellFoundedGT α
⊢ iSup ⇑a = monotonicSequenceLimit a

Tactic:
exact WellFoundedGT.iSup_eq_monotonicSequenceLimit a

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x1 x2 => x1 > x2
a : ℕ →o α
⊢ iSup ⇑a = monotonicSequenceLimit a

Tactic:
have : WellFoundedGT α := ⟨h⟩

Result:
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x1 x2 => x1 > x2
a : ℕ →o α
this : WellFoundedGT α
⊢ iSup ⇑a = monotonicSequenceLimit a
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem cos_eq_cos_iff {x y : ℂ} : cos x = cos y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = 2 * k * π - x :=
  calc
    cos x = cos y ↔ cos x - cos y = 0 := sub_eq_zero.symm
    _ ↔ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0

Proof state:
x y : ℂ
⊢ sin ((x - y) / 2) = 0 ∨ sin ((x + y) / 2) = 0 ↔ (∃ k, y = 2 * ↑k * ↑π + x) ∨ ∃ k, y = 2 * ↑k * ↑π - x

Tactic:
apply or_congr <;>
  field_simp [sin_eq_zero_iff, (by norm_num : -(2 : ℂ) ≠ 0), eq_sub_iff_add_eq',
    sub_eq_iff_eq_add, mul_comm (2 : ℂ), mul_right_comm _ (2 : ℂ)]

Result:
case h₁
x y : ℂ
⊢ (∃ k, x = ↑k * ↑π * 2 + y) ↔ ∃ k, y = ↑k * ↑π * 2 + x

Proof state:
case h₁.mpr.intro
x : ℂ
k : ℤ
⊢ ∃ k_1, x = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + x)

Tactic:
use -k

Result:
case h
x : ℂ
k : ℤ
⊢ x = ↑(-k) * ↑π * 2 + (↑k * ↑π * 2 + x)

Proof state:
x y : ℂ
⊢ cos x - cos y = 0 ↔ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0

Tactic:
rw [cos_sub_cos]

Result:
no goals

Proof state:
x y : ℂ
⊢ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0 ↔ sin ((x + y) / 2) = 0 ∨ sin ((x - y) / 2) = 0

Tactic:
simp [(by norm_num : (2 : ℂ) ≠ 0)]

Result:
no goals

Proof state:
case h
x : ℂ
k : ℤ
⊢ x = ↑(-k) * ↑π * 2 + (↑k * ↑π * 2 + x)

Tactic:
simp

Result:
no goals

Proof state:
x y : ℂ
⊢ -2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
x y : ℂ
⊢ 2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case h₁.mpr
x y : ℂ
⊢ (∃ k, y = ↑k * ↑π * 2 + x) → ∃ k, x = ↑k * ↑π * 2 + y

Tactic:
rintro ⟨k, rfl⟩

Result:
case h₁.mpr.intro
x : ℂ
k : ℤ
⊢ ∃ k_1, x = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + x)
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
theorem quasiCompact_over_affine_iff {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] :
    QuasiCompact f ↔ CompactSpace X

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
⊢ QuasiCompact f ↔ CompactSpace ↑↑X.toPresheafedSpace

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @QuasiCompact)]

Result:
no goals
-- Mathlib/Order/BooleanSubalgebra.lean
@[simp] lemma mem_sInf {S : Set (BooleanSubalgebra α)} : a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a : α
S : Set (BooleanSubalgebra α)
⊢ a ∈ ↑(sInf S) ↔ ∀ L ∈ S, a ∈ L

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a : α
S : Set (BooleanSubalgebra α)
⊢ a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L

Tactic:
rw [← SetLike.mem_coe]

Result:
α : Type u_2
inst✝ : BooleanAlgebra α
a : α
S : Set (BooleanSubalgebra α)
⊢ a ∈ ↑(sInf S) ↔ ∀ L ∈ S, a ∈ L
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem hasColimitsOfShape_of_equivalence {J' : Type u₂} [Category.{v₂} J'] (e : J ≌ J')
    [HasColimitsOfShape J C] : HasColimitsOfShape J' C

Proof state:
case has_colimit
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
F : J' ⥤ C
⊢ HasColimit F

Tactic:
apply hasColimit_of_equivalence_comp e

Result:
no goals

Proof state:
case has_colimit
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
⊢ autoParam (∀ (F : J' ⥤ C), HasColimit F) _auto✝

Tactic:
intro F

Result:
case has_colimit
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
F : J' ⥤ C
⊢ HasColimit F

Proof state:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J' C

Tactic:
constructor

Result:
case has_colimit
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
⊢ autoParam (∀ (F : J' ⥤ C), HasColimit F) _auto✝
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_addXYZ (P Q : Fin 3 → R) :
    (W'.map f).toJacobian.addXYZ (f ∘ P) (f ∘ Q) = f ∘ addXYZ W' P Q

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ (map W' f).toJacobian.addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W'.addXYZ P Q

Tactic:
simp only [addXYZ, map_addX, map_addY, map_addZ, comp_fin3]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem commute_nat_add (n : ℕ) : Function.Commute f (n + ·)

Proof state:
f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ⇑f fun x => ↑n + x

Tactic:
simpa only [nsmul_one, add_left_iterate] using Function.Commute.iterate_right f.map_one_add n

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem continuous_congr_of_inseparable (h : ∀ x, f x ~ᵢ g x) :
    Continuous f ↔ Continuous g

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : X → Y
h : ∀ (x : X), f x ~ᵢ g x
⊢ Continuous (SeparationQuotient.mk ∘ f) ↔ Continuous (SeparationQuotient.mk ∘ g)

Tactic:
exact continuous_congr fun x ↦ SeparationQuotient.mk_eq_mk.mpr (h x)

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : X → Y
h : ∀ (x : X), f x ~ᵢ g x
⊢ Continuous f ↔ Continuous g

Tactic:
simp_rw [SeparationQuotient.isInducing_mk.continuous_iff (Y := Y)]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : X → Y
h : ∀ (x : X), f x ~ᵢ g x
⊢ Continuous (SeparationQuotient.mk ∘ f) ↔ Continuous (SeparationQuotient.mk ∘ g)
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_sub_const_Ioi : (fun x => x - a) '' Ioi b = Ioi (b - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => x - a) '' Ioi b = Ioi (b - a)

Tactic:
simp [sub_eq_neg_add]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma toAffine_of_singular {P : Fin 3 → F} (hP : ¬W.Nonsingular P) : toAffine W P = 0

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : ¬W.Nonsingular P
⊢ toAffine W P = 0

Tactic:
rw [toAffine, dif_neg <| not_and_of_not_left _ hP]

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_relabelEquiv {g : α ≃ β} {k} {φ : L.BoundedFormula α k} {v : β → M}
    {xs : Fin k → M} : (relabelEquiv g φ).Realize v xs ↔ φ.Realize (v ∘ g) xs

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs : Fin k → M
⊢ ((relabelEquiv g) φ).Realize v xs ↔ φ.Realize (v ∘ ⇑g) xs

Tactic:
simp only [relabelEquiv, mapTermRelEquiv_apply, Equiv.coe_refl]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs : Fin k → M
⊢ (mapTermRel (fun n => ⇑(Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl (Fin n))))) (fun n => id) (fun x => id)
          φ).Realize
      v xs ↔
    φ.Realize (v ∘ ⇑g) xs

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
⊢ Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n))) = Sum.elim (v ∘ ⇑g) xs

Tactic:
ext (i | i) <;> rfl

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
⊢ realize (Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n)))) t = realize (Sum.elim (v ∘ ⇑g) xs) t

Tactic:
refine congr (congr rfl ?_) rfl

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
⊢ Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n))) = Sum.elim (v ∘ ⇑g) xs

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
⊢ realize (Sum.elim v xs) ((Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl (Fin n)))) t) =
    realize (Sum.elim (v ∘ ⇑g) xs) t

Tactic:
simp only [relabelEquiv_apply, Term.realize_relabel]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
⊢ realize (Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n)))) t = realize (Sum.elim (v ∘ ⇑g) xs) t

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs : Fin k → M
⊢ (mapTermRel (fun n => ⇑(Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl (Fin n))))) (fun n => id) (fun x => id)
          φ).Realize
      v xs ↔
    φ.Realize (v ∘ ⇑g) xs

Tactic:
refine realize_mapTermRel_id (fun n t xs => ?_) fun _ _ _ => rfl

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
⊢ realize (Sum.elim v xs) ((Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl (Fin n)))) t) =
    realize (Sum.elim (v ∘ ⇑g) xs) t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem ult_eq_not_carry (x y : BitVec w) : x.ult y = !carry w x (~~~y) true

Proof state:
w : Nat
x y : BitVec w
⊢ x.toNat < y.toNat ↔ x.toNat + (2 ^ w - 1 - y.toNat) % 2 ^ w + 1 < 2 ^ w

Tactic:
rw [Nat.mod_eq_of_lt (by omega)]

Result:
w : Nat
x y : BitVec w
⊢ x.toNat < y.toNat ↔ x.toNat + (2 ^ w - 1 - y.toNat) + 1 < 2 ^ w

Proof state:
w : Nat
x y : BitVec w
⊢ x.ult y = !carry w x (~~~y) true

Tactic:
simp only [BitVec.ult, carry, toNat_mod_cancel, toNat_not, toNat_true, ge_iff_le, ← decide_not,
  Nat.not_le, decide_eq_decide]

Result:
w : Nat
x y : BitVec w
⊢ x.toNat < y.toNat ↔ x.toNat + (2 ^ w - 1 - y.toNat) % 2 ^ w + 1 < 2 ^ w

Proof state:
w : Nat
x y : BitVec w
⊢ 2 ^ w - 1 - y.toNat < 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x.toNat < y.toNat ↔ x.toNat + (2 ^ w - 1 - y.toNat) + 1 < 2 ^ w

Tactic:
omega

Result:
no goals
-- Mathlib/SetTheory/Surreal/Basic.lean
theorem moveLeft {x : PGame} (o : Numeric x) (i : x.LeftMoves) : Numeric (x.moveLeft i)

Proof state:
x : PGame
o : x.Numeric
i : x.LeftMoves
⊢ (x.moveLeft i).Numeric

Tactic:
cases x

Result:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
o : (PGame.mk α✝ β✝ a✝¹ a✝).Numeric
i : (PGame.mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ ((PGame.mk α✝ β✝ a✝¹ a✝).moveLeft i).Numeric

Proof state:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
o : (PGame.mk α✝ β✝ a✝¹ a✝).Numeric
i : (PGame.mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ ((PGame.mk α✝ β✝ a✝¹ a✝).moveLeft i).Numeric

Tactic:
exact o.2.1 i

Result:
no goals
-- Mathlib/Algebra/Order/Module/Algebra.lean
lemma algebraMap_nonneg (ha : 0 ≤ a) : 0 ≤ algebraMap α β a

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : OrderedCommSemiring α
inst✝² : OrderedSemiring β
inst✝¹ : Algebra α β
inst✝ : SMulPosMono α β
a : α
ha : 0 ≤ a
⊢ 0 ≤ (algebraMap α β) a

Tactic:
simpa using algebraMap_mono β ha

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma floorRoot_one_left (a : ℕ) : floorRoot 1 a = a

Proof state:
a : ℕ
⊢ floorRoot 1 a = a

Tactic:
simp [floorRoot]

Result:
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun p k => p ^ k) = a

Proof state:
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun p k => p ^ k) = a

Tactic:
split_ifs <;> simp [*]

Result:
no goals