harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_right_eq_arctan_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    ∡ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)

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₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂))

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs,
  angle_eq_arctan_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (right_ne_of_oangle_eq_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 : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).sign = 1

Tactic:
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

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 : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂))

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

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₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂))
-- Mathlib/Data/NNRat/Floor.lean
theorem floor_def (q : ℚ≥0) : ⌊q⌋₊ = q.num / q.den

Proof state:
q : ℚ≥0
⊢ ⌊q⌋₊ = q.num / q.den

Tactic:
rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def, Int.ofNat_ediv, den_coe, num_coe]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem Real.closedBall_eq_Icc {x r : ℝ} : closedBall x r = Icc (x - r) (x + r)

Proof state:
case h
x r y : ℝ
⊢ y ∈ closedBall x r ↔ y ∈ Icc (x - r) (x + r)

Tactic:
rw [mem_closedBall, dist_comm, Real.dist_eq, abs_sub_le_iff, mem_Icc, ← sub_le_iff_le_add',
  sub_le_comm]

Result:
no goals

Proof state:
x r : ℝ
⊢ closedBall x r = Icc (x - r) (x + r)

Tactic:
ext y

Result:
case h
x r y : ℝ
⊢ y ∈ closedBall x r ↔ y ∈ Icc (x - r) (x + r)
-- Mathlib/LinearAlgebra/Dual.lean
theorem quotAnnihilatorEquiv_apply (W : Subspace K V) (φ : Module.Dual K V) :
    W.quotAnnihilatorEquiv (Submodule.Quotient.mk φ) = W.dualRestrict φ

Proof state:
case h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
φ : Dual K V
x✝ : ↥W
⊢ (W.quotAnnihilatorEquiv (Submodule.Quotient.mk φ)) x✝ = ((dualRestrict W) φ) x✝

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
φ : Dual K V
⊢ W.quotAnnihilatorEquiv (Submodule.Quotient.mk φ) = (dualRestrict W) φ

Tactic:
ext

Result:
case h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
φ : Dual K V
x✝ : ↥W
⊢ (W.quotAnnihilatorEquiv (Submodule.Quotient.mk φ)) x✝ = ((dualRestrict W) φ) x✝
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem span_range_inclusion_restrictScalars_eq_top :
    span S (range (inclusion <| span_le_restrictScalars R S s)) = ⊤ :=
  span_range_inclusion_eq_top _ _ _ <| by simp

Proof state:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
s : Set M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
⊢ span S s ≤ span S ↑(span R s)

Tactic:
simp

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

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

Tactic:
simp [H.symm]

Result:
no goals

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

Tactic:
simp [H]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem filterMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → m (Option β)} {g : α → m (Option β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.filterMapM f = l.unattach.filterMapM g

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → m (Option β)
g : α → m (Option β)
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ filterMapM f l = filterMapM g (map (fun x => x.val) l)

Tactic:
induction l with
| nil => simp
| cons a l ih => simp [ih, hf, filterMapM_cons]

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → m (Option β)
g : α → m (Option β)
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : filterMapM f l = filterMapM g (map (fun x => x.val) l)
⊢ filterMapM f (a :: l) = filterMapM g (map (fun x => x.val) (a :: l))

Tactic:
simp [ih, hf, filterMapM_cons]

Result:
no goals

Proof state:
case nil
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → m (Option β)
g : α → m (Option β)
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ filterMapM f [] = filterMapM g (map (fun x => x.val) [])

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → m (Option β)
g : α → m (Option β)
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ filterMapM f l = filterMapM g l.unattach

Tactic:
unfold unattach

Result:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → m (Option β)
g : α → m (Option β)
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ filterMapM f l = filterMapM g (map (fun x => x.val) l)
-- Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
theorem Cotrident.condition (j₁ j₂ : J) (t : Cotrident f) : f j₁ ≫ t.π = f j₂ ≫ t.π

Proof state:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Cotrident f
⊢ f j₁ ≫ t.π = f j₂ ≫ t.π

Tactic:
rw [t.app_one, t.app_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
lemma differentiableAt_iff_comp_const_sub {a b : 𝕜} :
    DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (b - x)) (b - a)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x => f (b - x)) (b - a)

Tactic:
simp [differentiableAt_comp_const_sub]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem succ_singleton {n : ℕ} : Ico n (n + 1) = [n]

Proof state:
n : ℕ
⊢ range' n (n + 1 - n) = [n]

Tactic:
simp [range', Nat.add_sub_cancel_left]

Result:
no goals

Proof state:
n : ℕ
⊢ Ico n (n + 1) = [n]

Tactic:
dsimp [Ico]

Result:
n : ℕ
⊢ range' n (n + 1 - n) = [n]
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem Multiset.untrop_prod [AddCommMonoid R] (s : Multiset (Tropical R)) :
    untrop s.prod = Multiset.sum (s.map untrop) :=
  Quotient.inductionOn s (by simpa using List.untrop_prod)

Proof state:
R : Type u_1
inst✝ : AddCommMonoid R
s : Multiset (Tropical R)
⊢ ∀ (a : List (Tropical R)), untrop (prod ⟦a⟧) = (map untrop ⟦a⟧).sum

Tactic:
simpa using List.untrop_prod

Result:
no goals
-- Mathlib/Topology/Algebra/FilterBasis.lean
theorem nhds_hasBasis (B : GroupFilterBasis G) (x₀ : G) :
    HasBasis (@nhds G B.topology x₀) (fun V : Set G ↦ V ∈ B) fun V ↦ (fun y ↦ x₀ * y) '' V

Proof state:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ (𝓝 x₀).HasBasis (fun V => V ∈ B) fun V => (fun y => x₀ * y) '' V

Tactic:
rw [B.nhds_eq]

Result:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ (B.N x₀).HasBasis (fun V => V ∈ B) fun V => (fun y => x₀ * y) '' V

Proof state:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ (B.N x₀).HasBasis (fun V => V ∈ B) fun V => (fun y => x₀ * y) '' V

Tactic:
apply B.hasBasis

Result:
no goals
-- Mathlib/RingTheory/Unramified/Locus.lean
lemma basicOpen_subset_unramifiedLocus_iff {f : A} :
    ↑(PrimeSpectrum.basicOpen f) ⊆ unramifiedLocus R A ↔
      Algebra.FormallyUnramified R (Localization.Away f)

Proof state:
R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ unramifiedLocus R A ↔ FormallyUnramified R (Localization.Away f)

Tactic:
rw [unramifiedLocus_eq_compl_support, Set.subset_compl_comm,
  PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl,
  ← LocalizedModule.subsingleton_iff_support_subset, Algebra.formallyUnramified_iff]

Result:
R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ Subsingleton (LocalizedModule (Submonoid.powers f) (Ω[A⁄R])) ↔ Subsingleton (Ω[Localization.Away f⁄R])

Proof state:
R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ Subsingleton (LocalizedModule (Submonoid.powers f) (Ω[A⁄R])) ↔ Subsingleton (Ω[Localization.Away f⁄R])

Tactic:
exact (IsLocalizedModule.iso (.powers f)
  (KaehlerDifferential.map R R A (Localization.Away f))).subsingleton_congr

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Permanent.lean
theorem permanent_transpose (M : Matrix n n R) : Mᵀ.permanent = M.permanent

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
⊢ Mᵀ.permanent = M.permanent

Tactic:
refine sum_bijective _ inv_involutive.bijective _ _ ?_

Result:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
⊢ ∀ (x : Perm n), ∏ i : n, Mᵀ (x i) i = ∏ i : n, M (x⁻¹ i) i

Proof state:
case h
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
σ : Perm n
⊢ ∀ (x : n), Mᵀ (σ x) x = M (σ⁻¹ (σ x)) (σ x)

Tactic:
simp

Result:
no goals

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
σ : Perm n
⊢ ∏ i : n, Mᵀ (σ i) i = ∏ i : n, M (σ⁻¹ i) i

Tactic:
apply Fintype.prod_equiv σ

Result:
case h
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
σ : Perm n
⊢ ∀ (x : n), Mᵀ (σ x) x = M (σ⁻¹ (σ x)) (σ x)

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
⊢ ∀ (x : Perm n), ∏ i : n, Mᵀ (x i) i = ∏ i : n, M (x⁻¹ i) i

Tactic:
intro σ

Result:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
σ : Perm n
⊢ ∏ i : n, Mᵀ (σ i) i = ∏ i : n, M (σ⁻¹ i) i
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_lt_d4 : π < 3.1416

Proof state:
⊢ π < 3.1416

Tactic:
pi_upper_bound [
  4756/3363, 14965/8099, 21183/10799, 49188/24713, 2-53/22000, 2-71/117869, 2-47/312092,
  2-17/451533, 2-4/424971]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[ext]
lemma cycles_ext {A : C} (f₁ f₂ : A ⟶ S.cycles) (h : f₁ ≫ S.iCycles = f₂ ≫ S.iCycles) :
    f₁ = f₂

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
f₁ f₂ : A ⟶ S.cycles
h : f₁ ≫ S.iCycles = f₂ ≫ S.iCycles
⊢ f₁ = f₂

Tactic:
simpa only [cycles_ext_iff] using h

Result:
no goals
-- Mathlib/Data/Int/Order/Units.lean
theorem neg_one_pow_ne_zero {n : ℕ} : (-1 : ℤ) ^ n ≠ 0

Proof state:
n : ℕ
⊢ (-1) ^ n ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
@[simp]
lemma genEigenspace_zero_nat (f : End R M) (k : ℕ) :
    f.genEigenspace 0 k = LinearMap.ker (f ^ k)

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
k : ℕ
⊢ (f.genEigenspace 0) ↑k = LinearMap.ker (f ^ k)

Tactic:
ext

Result:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
k : ℕ
x✝ : M
⊢ x✝ ∈ (f.genEigenspace 0) ↑k ↔ x✝ ∈ LinearMap.ker (f ^ k)

Proof state:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
k : ℕ
x✝ : M
⊢ x✝ ∈ (f.genEigenspace 0) ↑k ↔ x✝ ∈ LinearMap.ker (f ^ k)

Tactic:
simp [mem_genEigenspace_nat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.erase (a : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁.erase a ~ l₂.erase a :=
  if h₁ : a ∈ l₁ then
    have h₂ : a ∈ l₂ := p.subset h₁
    .cons_inv <| (perm_cons_erase h₁).symm.trans <| p.trans (perm_cons_erase h₂)
  else by
    have h₂ : a ∉ l₂ := mt p.mem_iff.2 h₁
    rw [erase_of_not_mem h₁, erase_of_not_mem h₂]; exact p

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
h₁ : ¬a ∈ l₁
⊢ l₁.erase a ~ l₂.erase a

Tactic:
have h₂ : a ∉ l₂ := mt p.mem_iff.2 h₁

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
h₁ : ¬a ∈ l₁
h₂ : ¬a ∈ l₂
⊢ l₁.erase a ~ l₂.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
h₁ : ¬a ∈ l₁
h₂ : ¬a ∈ l₂
⊢ l₁ ~ l₂

Tactic:
exact p

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
h₁ : ¬a ∈ l₁
h₂ : ¬a ∈ l₂
⊢ l₁.erase a ~ l₂.erase a

Tactic:
rw [erase_of_not_mem h₁, erase_of_not_mem h₂]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
h₁ : ¬a ∈ l₁
h₂ : ¬a ∈ l₂
⊢ l₁ ~ l₂
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem DistinctKeys.mapUnit [BEq α]
    {l : List α} (distinct: l.Pairwise (fun a b => (a == b) = false)) :
    DistinctKeys (l.map (⟨·, ()⟩))

Proof state:
α : Type u
inst✝ : BEq α
l : List α
distinct : List.Pairwise (fun a b => (a == b) = false) l
⊢ DistinctKeys (List.map (fun x => ⟨x, ()⟩) l)

Tactic:
rw [DistinctKeys.def]

Result:
α : Type u
inst✝ : BEq α
l : List α
distinct : List.Pairwise (fun a b => (a == b) = false) l
⊢ List.Pairwise (fun a b => (a.fst == b.fst) = false) (List.map (fun x => ⟨x, ()⟩) l)

Proof state:
α : Type u
inst✝ : BEq α
l : List α
distinct : List.Pairwise (fun a b => (a == b) = false) l
⊢ List.Pairwise (fun a b => (a.fst == b.fst) = false) (List.map (fun x => ⟨x, ()⟩) l)

Tactic:
refine List.Pairwise.map ?_ ?_ distinct

Result:
α : Type u
inst✝ : BEq α
l : List α
distinct : List.Pairwise (fun a b => (a == b) = false) l
⊢ ∀ (a b : α), (a == b) = false → (⟨a, ()⟩.fst == ⟨b, ()⟩.fst) = false

Proof state:
α : Type u
inst✝ : BEq α
l : List α
distinct : List.Pairwise (fun a b => (a == b) = false) l
⊢ ∀ (a b : α), (a == b) = false → (⟨a, ()⟩.fst == ⟨b, ()⟩.fst) = false

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem set_mkVector_self : (mkVector n a).set i a h = mkVector n a

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
h : i < n
⊢ (mkVector n a).set i a h = mkVector n a

Tactic:
rw [← toArray_inj]

Result:
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
h : i < n
⊢ ((mkVector n a).set i a h).toArray = (mkVector n a).toArray

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
h : i < n
⊢ ((mkVector n a).set i a h).toArray = (mkVector n a).toArray

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem convex (K : Submodule 𝕜 E) : Convex 𝕜 (↑K : Set E)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝⁵ : x✝ ∈ ↑K
y✝ : E
a✝⁴ : y✝ ∈ ↑K
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ a✝³ • x✝ + b✝ • y✝ ∈ ↑K

Tactic:
refine add_mem (smul_mem _ _ ?_) (smul_mem _ _ ?_) <;> assumption

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
⊢ Convex 𝕜 ↑K

Tactic:
repeat' intro

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝⁵ : x✝ ∈ ↑K
y✝ : E
a✝⁴ : y✝ ∈ ↑K
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ a✝³ • x✝ + b✝ • y✝ ∈ ↑K

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝⁴ : x✝ ∈ ↑K
y✝ : E
a✝³ : y✝ ∈ ↑K
a✝² b✝ : 𝕜
a✝¹ : 0 ≤ a✝²
a✝ : 0 ≤ b✝
⊢ a✝² + b✝ = 1 → a✝² • x✝ + b✝ • y✝ ∈ ↑K

Tactic:
intro

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝⁵ : x✝ ∈ ↑K
y✝ : E
a✝⁴ : y✝ ∈ ↑K
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ a✝³ • x✝ + b✝ • y✝ ∈ ↑K
-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem prodIsoProd_inv_snd (X Y : TopCat.{u}) :
    (prodIsoProd X Y).inv ≫ Limits.prod.snd = prodSnd

Proof state:
X Y : TopCat
⊢ (X.prodIsoProd Y).inv ≫ prod.snd = prodSnd

Tactic:
simp [Iso.inv_comp_eq]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffOn.continuousOn_derivWithin (h : ContDiffOn 𝕜 n f₂ s₂) (hs : UniqueDiffOn 𝕜 s₂)
    (hn : 1 ≤ n) : ContinuousOn (derivWithin f₂ s₂) s₂

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
h : ContDiffOn 𝕜 n f₂ s₂
hs : UniqueDiffOn 𝕜 s₂
hn : 0 + 1 ≤ n
⊢ ContinuousOn (derivWithin f₂ s₂) s₂

Tactic:
exact ((contDiffOn_succ_iff_derivWithin hs).1 (h.of_le hn)).2.2.continuousOn

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
h : ContDiffOn 𝕜 n f₂ s₂
hs : UniqueDiffOn 𝕜 s₂
hn : 1 ≤ n
⊢ ContinuousOn (derivWithin f₂ s₂) s₂

Tactic:
rw [show (1 : WithTop ℕ∞) = 0 + 1 from rfl] at hn

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
h : ContDiffOn 𝕜 n f₂ s₂
hs : UniqueDiffOn 𝕜 s₂
hn : 0 + 1 ≤ n
⊢ ContinuousOn (derivWithin f₂ s₂) s₂
-- Mathlib/RingTheory/Localization/Defs.lean
theorem mk'_pow (x : R) (y : M) (n : ℕ) : mk' S (x ^ n) (y ^ n) = mk' S x y ^ n

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
n : ℕ
⊢ (algebraMap R S) x ^ n = (mk' S x y * (algebraMap R S) ↑y) ^ n

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
n : ℕ
⊢ mk' S (x ^ n) (y ^ n) = mk' S x y ^ n

Tactic:
simp_rw [IsLocalization.mk'_eq_iff_eq_mul, SubmonoidClass.coe_pow, map_pow, ← mul_pow]

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
n : ℕ
⊢ (algebraMap R S) x ^ n = (mk' S x y * (algebraMap R S) ↑y) ^ n
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
lemma hasExt_of_hasDerivedCategory [HasDerivedCategory.{w} C] : HasExt.{w} C

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ ∀ (X Y : C) (n : ℤ),
    Small.{w, w} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ HasExt C

Tactic:
rw [hasExt_iff.{w}]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ ∀ (X Y : C) (n : ℤ),
    Small.{w, w} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
theorem Pi.lift_π {β : Type w} {f : β → C} [HasProduct f] {P : C} (p : ∀ b, P ⟶ f b) (b : β) :
    Pi.lift p ≫ Pi.π f b = p b

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
β : Type w
f : β → C
inst✝ : HasProduct f
P : C
p : (b : β) → P ⟶ f b
b : β
⊢ lift p ≫ π f b = p b

Tactic:
simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem tendsto_atTop' : Tendsto f atTop l ↔ ∀ s ∈ l, ∃ a, ∀ b ≥ a, f b ∈ s

Proof state:
α : Type u_3
β : Type u_4
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
f : α → β
l : Filter β
⊢ Tendsto f atTop l ↔ ∀ s ∈ l, ∃ a, ∀ b ≥ a, f b ∈ s

Tactic:
simp only [tendsto_def, mem_atTop_sets, mem_preimage]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_ofNat (x w : Nat) : (BitVec.ofNat w x).toNat = x % 2^w

Proof state:
x w : Nat
⊢ (BitVec.ofNat w x).toNat = x % 2 ^ w

Tactic:
simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.smtSDiv_smtUDiv (x y : BitVec w) :
    x.smtSDiv y =
      bif x.getLsbD (w - 1) then
        bif y.getLsbD (w - 1) then
          (-x).smtUDiv (-y)
        else
          -((-x).smtUDiv y)
      else
        bif y.getLsbD (w - 1) then
          -(x.smtUDiv (-y))
        else
          x.smtUDiv y

Proof state:
w : Nat
x y : BitVec w
⊢ x.smtSDiv y =
    bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then (-x).smtUDiv (-y) else -(-x).smtUDiv y
    else bif y.getLsbD (w - 1) then -x.smtUDiv (-y) else x.smtUDiv y

Tactic:
rw [BitVec.smtSDiv_eq, ← BitVec.msb_eq_getLsbD_last, ← BitVec.msb_eq_getLsbD_last]

Result:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.smtUDiv y
    | false, true => -x.smtUDiv (-y)
    | true, false => -(-x).smtUDiv y
    | true, true => (-x).smtUDiv (-y)) =
    bif x.msb then bif y.msb then (-x).smtUDiv (-y) else -(-x).smtUDiv y
    else bif y.msb then -x.smtUDiv (-y) else x.smtUDiv y

Proof state:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.smtUDiv y
    | false, true => -x.smtUDiv (-y)
    | true, false => -(-x).smtUDiv y
    | true, true => (-x).smtUDiv (-y)) =
    bif x.msb then bif y.msb then (-x).smtUDiv (-y) else -(-x).smtUDiv y
    else bif y.msb then -x.smtUDiv (-y) else x.smtUDiv y

Tactic:
cases x.msb <;> cases y.msb <;> simp

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem lcm_assoc (i j k : ℤ) : lcm (lcm i j) k = lcm i (lcm j k)

Proof state:
i j k : ℤ
⊢ (↑(i.lcm j)).lcm k = i.lcm ↑(j.lcm k)

Tactic:
rw [Int.lcm, Int.lcm, Int.lcm, Int.lcm, natAbs_ofNat, natAbs_ofNat]

Result:
i j k : ℤ
⊢ (i.natAbs.lcm j.natAbs).lcm k.natAbs = i.natAbs.lcm (j.natAbs.lcm k.natAbs)

Proof state:
i j k : ℤ
⊢ (i.natAbs.lcm j.natAbs).lcm k.natAbs = i.natAbs.lcm (j.natAbs.lcm k.natAbs)

Tactic:
apply Nat.lcm_assoc

Result:
no goals