harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem union_quotToDoset (H K : Subgroup G) : ⋃ q, quotToDoset H K q = Set.univ

Proof state:
case h.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out (mk H K x) = h * x * k
⊢ x = h⁻¹ * Quotient.out (mk H K x) * k⁻¹

Tactic:
simp only [h5, Subgroup.coe_mk, ← mul_assoc, one_mul, inv_mul_cancel, mul_inv_cancel_right]

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
x : G
⊢ ∃ i, ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out i * y

Tactic:
use mk H K x

Result:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
x : G
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out (mk H K x) * y

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ⋃ q, quotToDoset H K q = Set.univ

Tactic:
ext x

Result:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
x : G
⊢ x ∈ ⋃ q, quotToDoset H K q ↔ x ∈ Set.univ

Proof state:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
x : G
⊢ x ∈ ⋃ q, quotToDoset H K q ↔ x ∈ Set.univ

Tactic:
simp only [Set.mem_iUnion, quotToDoset, mem_doset, SetLike.mem_coe, exists_prop, Set.mem_univ,
  iff_true]

Result:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
x : G
⊢ ∃ i, ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out i * y

Proof state:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
x : G
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out (mk H K x) * y

Tactic:
obtain ⟨h, k, h3, h4, h5⟩ := mk_out_eq_mul H K x

Result:
case h.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out (mk H K x) = h * x * k
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out (mk H K x) * y

Proof state:
case h.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out (mk H K x) = h * x * k
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out (mk H K x) * y

Tactic:
refine ⟨h⁻¹, H.inv_mem h3, k⁻¹, K.inv_mem h4, ?_⟩

Result:
case h.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out (mk H K x) = h * x * k
⊢ x = h⁻¹ * Quotient.out (mk H K x) * k⁻¹
-- Mathlib/Probability/Kernel/Basic.lean
lemma id_apply (a : α) : Kernel.id a = Measure.dirac a

Proof state:
α : Type u_1
mα : MeasurableSpace α
a : α
⊢ Kernel.id a = Measure.dirac a

Tactic:
rw [Kernel.id, deterministic_apply, id_def]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addY_of_Z_eq_zero_right {P Q : Fin 3 → R} (hQ : W'.Equation Q) (hQz : Q z = 0) :
    W'.addY P Q = (-(Q x * P z)) ^ 3 * P y

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.addY P Q = (-(Q x * P z)) ^ 3 * P y

Tactic:
rw [addY, negY_eq, negAddY_of_Z_eq_zero_right hQ hQz, negY, addX_of_Z_eq_zero_right hQz,
  addZ_of_Z_eq_zero_right hQz]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -((-(Q x * P z)) ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) -
        W'.a₁ * ((-(Q x * P z)) ^ 2 * P x) * (-(Q x * P z) * P z) -
      W'.a₃ * (-(Q x * P z) * P z) ^ 3 =
    (-(Q x * P z)) ^ 3 * P y

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -((-(Q x * P z)) ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) -
        W'.a₁ * ((-(Q x * P z)) ^ 2 * P x) * (-(Q x * P z) * P z) -
      W'.a₃ * (-(Q x * P z) * P z) ^ 3 =
    (-(Q x * P z)) ^ 3 * P y

Tactic:
ring1

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
lemma ext (h : ∀ (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x),
    MapEq F G k₁ k₂ h₁₂ h₂) :
    F = G

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
h : ∀ (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x), MapEq F G k₁ k₂ h₁₂ h₂
⊢ ∀ ⦃X Y : ↑(Set.Iic x)⦄ (f : X ⟶ Y), F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)

Tactic:
rintro ⟨k₁, _⟩ ⟨k₂, h₂⟩ f

Result:
case h.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
h : ∀ (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x), MapEq F G k₁ k₂ h₁₂ h₂
k₁ : K
property✝ : k₁ ∈ Set.Iic x
k₂ : K
h₂ : k₂ ∈ Set.Iic x
f : ⟨k₁, property✝⟩ ⟶ ⟨k₂, h₂⟩
⊢ F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)

Proof state:
case h.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
h : ∀ (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x), MapEq F G k₁ k₂ h₁₂ h₂
k₁ : K
property✝ : k₁ ∈ Set.Iic x
k₂ : K
h₂ : k₂ ∈ Set.Iic x
f : ⟨k₁, property✝⟩ ⟶ ⟨k₂, h₂⟩
⊢ F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)

Tactic:
apply h

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
h : ∀ (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x), MapEq F G k₁ k₂ h₁₂ h₂
⊢ F = G

Tactic:
apply Arrow.functor_ext

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
h : ∀ (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x), MapEq F G k₁ k₂ h₁₂ h₂
⊢ ∀ ⦃X Y : ↑(Set.Iic x)⦄ (f : X ⟶ Y), F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)
-- Mathlib/Topology/ContinuousMap/Basic.lean
theorem liftCover_coe' {s : Set α} {hs : s ∈ A} (x : s) : liftCover' A F hF hA x = F s hs x :=
  let x' : ((↑) : A → Set α) ⟨s, hs⟩ := x
  by delta liftCover'; exact liftCover_coe x'

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
A : Set (Set α)
F : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    (F s hs) ⟨x, hxi⟩ = (F t ht) ⟨x, hxj⟩
hA : ∀ (x : α), ∃ i ∈ A, i ∈ 𝓝 x
s : Set α
hs : s ∈ A
x : ↑s
x' : ↑↑⟨s, hs⟩ := x
⊢ (liftCover' A F hF hA) ↑x = (F s hs) x

Tactic:
delta liftCover'

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
A : Set (Set α)
F : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    (F s hs) ⟨x, hxi⟩ = (F t ht) ⟨x, hxj⟩
hA : ∀ (x : α), ∃ i ∈ A, i ∈ 𝓝 x
s : Set α
hs : s ∈ A
x : ↑s
x' : ↑↑⟨s, hs⟩ := x
⊢ (let S := Subtype.val;
      let F_1 := fun i => F ↑i ⋯;
      liftCover S F_1 ⋯ ⋯)
      ↑x =
    (F s hs) x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
A : Set (Set α)
F : (s : Set α) → s ∈ A → C(↑s, β)
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    (F s hs) ⟨x, hxi⟩ = (F t ht) ⟨x, hxj⟩
hA : ∀ (x : α), ∃ i ∈ A, i ∈ 𝓝 x
s : Set α
hs : s ∈ A
x : ↑s
x' : ↑↑⟨s, hs⟩ := x
⊢ (let S := Subtype.val;
      let F_1 := fun i => F ↑i ⋯;
      liftCover S F_1 ⋯ ⋯)
      ↑x =
    (F s hs) x

Tactic:
exact liftCover_coe x'

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma integral_tilted (f : α → ℝ) (g : α → E) :
    ∫ x, g x ∂(μ.tilted f) = ∫ x, (exp (f x) / ∫ x, exp (f x) ∂μ) • (g x) ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
⊢ ∫ (x : α), g x ∂μ.tilted f = ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
rw [← setIntegral_univ, setIntegral_tilted' f g MeasurableSet.univ, setIntegral_univ]

Result:
no goals
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_upper_bound_start (n : ℕ) {a}
    (h : (2 : ℝ) - ((a - 1 / (4 : ℝ) ^ n) / (2 : ℝ) ^ (n + 1)) ^ 2 ≤
        sqrtTwoAddSeries ((0 : ℕ) / (1 : ℕ)) n)
    (h₂ : (1 : ℝ) / (4 : ℝ) ^ n ≤ a) : π < a

Proof state:
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries 0 n

Tactic:
rwa [Nat.cast_zero, zero_div] at h

Result:
no goals

Proof state:
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 < 2 ^ (n + 1)

Tactic:
exact pow_pos zero_lt_two _

Result:
no goals

Proof state:
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ π < a

Tactic:
refine lt_of_lt_of_le (pi_lt_sqrtTwoAddSeries n) ?_

Result:
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n ≤ a

Proof state:
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n ≤ a

Tactic:
rw [← le_sub_iff_add_le, ← le_div_iff₀', sqrt_le_left, sub_le_comm]

Result:
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries 0 n

n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 ≤ (a - 1 / 4 ^ n) / 2 ^ (n + 1)

n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 < 2 ^ (n + 1)

Proof state:
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 ≤ (a - 1 / 4 ^ n) / 2 ^ (n + 1)

Tactic:
exact div_nonneg (sub_nonneg.2 h₂) (pow_nonneg (le_of_lt zero_lt_two) _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem head_mapIdx {l : List α} {f : Nat → α → β} {w : mapIdx f l ≠ []} :
    (mapIdx f l).head w = f 0 (l.head (by simpa using w))

Proof state:
case nil
α : Type u_1
β : Type u_2
f : Nat → α → β
w : mapIdx f [] ≠ []
⊢ (mapIdx f []).head w = f 0 ([].head ⋯)

Tactic:
simp at w

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : Nat → α → β
head✝ : α
tail✝ : List α
w : mapIdx f (head✝ :: tail✝) ≠ []
⊢ (mapIdx f (head✝ :: tail✝)).head w = f 0 ((head✝ :: tail✝).head ⋯)

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.97393
β : Type ?u.97404
l : List α
f : Nat → α → β
w : mapIdx f l ≠ []
⊢ l ≠ []

Tactic:
simpa using w

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
w : mapIdx f l ≠ []
⊢ (mapIdx f l).head w = f 0 (l.head ⋯)

Tactic:
cases l with
| nil => simp at w
| cons _ _ => simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem ofList_singleton {k : α} {v : β} :
    ofList [⟨k, v⟩] = (∅ : Raw α (fun _ => β)).insert k v

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
k : α
v : β
⊢ (Raw₀.Const.insertMany Raw₀.empty [(k, v)]).val.val = (Raw₀.insert ⟨Raw₀.empty.val, ⋯⟩ k v).val

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
k : α
v : β
⊢ ofList [(k, v)] = ∅.insert k v

Tactic:
simp_to_raw

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
k : α
v : β
⊢ (Raw₀.Const.insertMany Raw₀.empty [(k, v)]).val.val = (Raw₀.insert ⟨Raw₀.empty.val, ⋯⟩ k v).val
-- Mathlib/Logic/Equiv/Set.lean
theorem coe_ofInjective_symm {α β} {f : α → β} (hf : Injective f) :
    ((ofInjective f hf).symm : range f → α) = rangeSplitting f

Proof state:
case h.mk.intro
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
x : α
⊢ (ofInjective f hf).symm ⟨f x, ⋯⟩ = rangeSplitting f ⟨f x, ⋯⟩

Tactic:
apply hf

Result:
case h.mk.intro.a
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
x : α
⊢ f ((ofInjective f hf).symm ⟨f x, ⋯⟩) = f (rangeSplitting f ⟨f x, ⋯⟩)

Proof state:
case h.mk.intro.a
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
x : α
⊢ f ((ofInjective f hf).symm ⟨f x, ⋯⟩) = f (rangeSplitting f ⟨f x, ⋯⟩)

Tactic:
simp [apply_rangeSplitting f]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ ⇑(ofInjective f hf).symm = rangeSplitting f

Tactic:
ext ⟨y, x, rfl⟩

Result:
case h.mk.intro
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
x : α
⊢ (ofInjective f hf).symm ⟨f x, ⋯⟩ = rangeSplitting f ⟨f x, ⋯⟩
-- Mathlib/ModelTheory/Types.lean
theorem setOf_subset_eq_empty_iff (S : L[[α]].Theory) :
    { p : T.CompleteType α | S ⊆ ↑p } = ∅ ↔
      ¬((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable

Proof state:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ (∃ x, x ∈ {p | S ⊆ ↑p}) → ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable

Tactic:
rintro ⟨p, hp⟩

Result:
case intro
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
p : T.CompleteType α
hp : p ∈ {p | S ⊆ ↑p}
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable

Proof state:
case intro
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
p : T.CompleteType α
hp : p ∈ {p | S ⊆ ↑p}
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable

Tactic:
exact p.isMaximal.1.mono (union_subset p.subset hp)

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ {p | S ⊆ ↑p} = ∅ ↔ ¬((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable

Tactic:
rw [iff_not_comm, ← not_nonempty_iff_eq_empty, Classical.not_not, Set.Nonempty]

Result:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔ ∃ x, x ∈ {p | S ⊆ ↑p}

Proof state:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔ ∃ x, x ∈ {p | S ⊆ ↑p}

Tactic:
refine
  ⟨fun h =>
    ⟨⟨L[[α]].completeTheory h.some, (subset_union_left (t := S)).trans completeTheory.subset,
        completeTheory.isMaximal (L[[α]]) h.some⟩,
      (((L.lhomWithConstants α).onTheory T).subset_union_right).trans completeTheory.subset⟩,
    ?_⟩

Result:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ (∃ x, x ∈ {p | S ⊆ ↑p}) → ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable
-- Mathlib/RingTheory/Discriminant.lean
theorem discr_of_matrix_mulVec (b : ι → B) (P : Matrix ι ι A) :
    discr A (P.map (algebraMap A B) *ᵥ b) = P.det ^ 2 * discr A b

Proof state:
A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ discr A (P.map ⇑(algebraMap A B) *ᵥ b) = P.det ^ 2 * discr A b

Tactic:
rw [discr_def, traceMatrix_of_matrix_mulVec, det_mul, det_mul, det_transpose, mul_comm, ←
  mul_assoc, discr_def, pow_two]

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem Tape.write_move_right_n {Γ} [Inhabited Γ] (f : Γ → Γ) (L R : ListBlank Γ) (n : ℕ) :
    ((Tape.move Dir.right)^[n] (Tape.mk' L R)).write (f (R.nth n)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (R.modifyNth f n))

Proof state:
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L R : ListBlank Γ
⊢ write (f R.head) (mk' L R) = mk' L (ListBlank.cons (f R.head) R.tail)

Tactic:
rw [← Tape.write_mk', ListBlank.cons_head_tail]

Result:
no goals

Proof state:
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L R : ListBlank Γ
⊢ write (f (R.nth 0)) ((move Dir.right)^[0] (mk' L R)) = (move Dir.right)^[0] (mk' L (ListBlank.modifyNth f 0 R))

Tactic:
simp only [ListBlank.nth_zero, ListBlank.modifyNth, iterate_zero_apply]

Result:
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L R : ListBlank Γ
⊢ write (f R.head) (mk' L R) = mk' L (ListBlank.cons (f R.head) R.tail)

Proof state:
case succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH :
  ∀ (L R : ListBlank Γ),
    write (f (R.nth n)) ((move Dir.right)^[n] (mk' L R)) = (move Dir.right)^[n] (mk' L (ListBlank.modifyNth f n R))
L R : ListBlank Γ
⊢ write (f (R.nth (n + 1))) ((move Dir.right)^[n + 1] (mk' L R)) =
    (move Dir.right)^[n + 1] (mk' L (ListBlank.modifyNth f (n + 1) R))

Tactic:
simp only [ListBlank.head_cons, ListBlank.nth_succ, ListBlank.modifyNth, Tape.move_right_mk',
  ListBlank.tail_cons, iterate_succ_apply, IH]

Result:
no goals

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L R : ListBlank Γ
n : ℕ
⊢ write (f (R.nth n)) ((move Dir.right)^[n] (mk' L R)) = (move Dir.right)^[n] (mk' L (ListBlank.modifyNth f n R))

Tactic:
induction' n with n IH generalizing L R

Result:
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L R : ListBlank Γ
⊢ write (f (R.nth 0)) ((move Dir.right)^[0] (mk' L R)) = (move Dir.right)^[0] (mk' L (ListBlank.modifyNth f 0 R))

case succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH :
  ∀ (L R : ListBlank Γ),
    write (f (R.nth n)) ((move Dir.right)^[n] (mk' L R)) = (move Dir.right)^[n] (mk' L (ListBlank.modifyNth f n R))
L R : ListBlank Γ
⊢ write (f (R.nth (n + 1))) ((move Dir.right)^[n + 1] (mk' L R)) =
    (move Dir.right)^[n + 1] (mk' L (ListBlank.modifyNth f (n + 1) R))
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma _root_.SimpleGraph.Walk.toSubgraph_connected {u v : V} (p : G.Walk u v) :
    p.toSubgraph.Connected

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ w w✝ : V
h : G.Adj u✝ w
p : G.Walk w w✝
ih : p.toSubgraph.Connected
⊢ (G.subgraphOfAdj h ⊓ p.toSubgraph).verts.Nonempty

Tactic:
exists w

Result:
case cons
V : Type u
G : SimpleGraph V
u v u✝ w w✝ : V
h : G.Adj u✝ w
p : G.Walk w w✝
ih : p.toSubgraph.Connected
⊢ w ∈ (G.subgraphOfAdj h ⊓ p.toSubgraph).verts

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ w w✝ : V
h : G.Adj u✝ w
p : G.Walk w w✝
ih : p.toSubgraph.Connected
⊢ w ∈ (G.subgraphOfAdj h ⊓ p.toSubgraph).verts

Tactic:
simp

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ Walk.nil.toSubgraph.Connected

Tactic:
apply singletonSubgraph_connected

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.toSubgraph.Connected

Tactic:
induction p with
| nil => apply singletonSubgraph_connected
| @cons _ w _ h p ih =>
  apply (subgraphOfAdj_connected h).sup ih
  exists w
  simp

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ w w✝ : V
h : G.Adj u✝ w
p : G.Walk w w✝
ih : p.toSubgraph.Connected
⊢ (Walk.cons h p).toSubgraph.Connected

Tactic:
apply (subgraphOfAdj_connected h).sup ih

Result:
case cons
V : Type u
G : SimpleGraph V
u v u✝ w w✝ : V
h : G.Adj u✝ w
p : G.Walk w w✝
ih : p.toSubgraph.Connected
⊢ (G.subgraphOfAdj h ⊓ p.toSubgraph).verts.Nonempty
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem le_antisymm {x y : BitVec n} : x ≤ y → y ≤ x → x = y

Proof state:
n : Nat
x y : BitVec n
⊢ x ≤ y → y ≤ x → x = y

Tactic:
simp only [le_def, BitVec.toNat_eq]

Result:
n : Nat
x y : BitVec n
⊢ x.toNat ≤ y.toNat → y.toNat ≤ x.toNat → x.toNat = y.toNat

Proof state:
n : Nat
x y : BitVec n
⊢ x.toNat ≤ y.toNat → y.toNat ≤ x.toNat → x.toNat = y.toNat

Tactic:
apply Nat.le_antisymm

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_sub_left (x x' y : M) : polar Q (x - x') y = polar Q x y - polar Q x' y

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x x' y : M
⊢ polar (⇑Q) (x - x') y = polar (⇑Q) x y - polar (⇑Q) x' y

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_left, polar_neg_left]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Stalk.lean
lemma ΓSpecIso_hom_stalkClosedPointIso_inv :
    (Scheme.ΓSpecIso R).hom ≫ (stalkClosedPointIso R).inv =
      (Spec R).presheaf.germ ⊤ (closedPoint _) trivial

Proof state:
R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ StructureSheaf.toStalk (↑R) (closedPoint ↑R) =
    (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial

Tactic:
rfl

Result:
no goals

Proof state:
R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (Scheme.ΓSpecIso R).hom ≫ (stalkClosedPointIso R).inv = (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial

Tactic:
rw [stalkClosedPointIso_inv, ← Iso.eq_inv_comp]

Result:
R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ StructureSheaf.toStalk (↑R) (closedPoint ↑R) =
    (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_eq_not_all_not (l : List α) (p : α → Bool) : l.any p = !l.all (!p .)

Proof state:
α : Type u_1
l : List α
p : α → Bool
⊢ l.any p = !l.all fun x => !p x

Tactic:
simp only [not_all_eq_any_not, Bool.not_not]

Result:
no goals
-- Mathlib/Topology/Connected/Clopen.lean
lemma isClopen_preimage_val {X : Type*} [TopologicalSpace X] {u v : Set X}
    (hu : IsOpen u) (huv : Disjoint (frontier u) v) : IsClopen (v ↓∩ u)

Proof state:
case a
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen u
huv : Disjoint (frontier u) v
⊢ v ∩ closure u = v ∩ u

Tactic:
rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_comm _ (frontier u),
  huv.inter_eq, union_empty]

Result:
no goals

Proof state:
case a
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen u
huv : Disjoint (frontier u) v
⊢ Subtype.val '' v ↓∩ closure u = Subtype.val '' v ↓∩ u

Tactic:
simp only [Subtype.image_preimage_coe]

Result:
case a
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen u
huv : Disjoint (frontier u) v
⊢ v ∩ closure u = v ∩ u

Proof state:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen u
huv : Disjoint (frontier u) v
⊢ IsClopen (v ↓∩ u)

Tactic:
refine ⟨?_, isOpen_induced hu (f := Subtype.val)⟩

Result:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen u
huv : Disjoint (frontier u) v
⊢ IsClosed (v ↓∩ u)

Proof state:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen u
huv : Disjoint (frontier u) v
⊢ IsClosed (v ↓∩ u)

Tactic:
refine isClosed_induced_iff.mpr ⟨closure u, isClosed_closure, ?_⟩

Result:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen u
huv : Disjoint (frontier u) v
⊢ v ↓∩ closure u = v ↓∩ u

Proof state:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen u
huv : Disjoint (frontier u) v
⊢ v ↓∩ closure u = v ↓∩ u

Tactic:
apply image_val_injective

Result:
case a
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen u
huv : Disjoint (frontier u) v
⊢ Subtype.val '' v ↓∩ closure u = Subtype.val '' v ↓∩ u
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem rotate_darts {u v : V} (c : G.Walk v v) (h : u ∈ c.support) :
    (c.rotate h).darts ~r c.darts

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.rotate h).darts ~r c.darts

Tactic:
simp only [rotate, darts_append]

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.dropUntil u h).darts ++ (c.takeUntil u h).darts ~r c.darts

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.dropUntil u h).darts ++ (c.takeUntil u h).darts ~r c.darts

Tactic:
apply List.IsRotated.trans List.isRotated_append

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.takeUntil u h).darts ++ (c.dropUntil u h).darts ~r c.darts

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.takeUntil u h).darts ++ (c.dropUntil u h).darts ~r c.darts

Tactic:
rw [← darts_append, take_spec]

Result:
no goals
-- Mathlib/Data/List/InsertIdx.lean
theorem insertIdx_subset_cons (n : ℕ) (a : α) (l : List α) : insertIdx n a l ⊆ a :: l

Proof state:
α : Type u
n : ℕ
a : α
l : List α
b : α
hb : b ∈ insertIdx n a l
⊢ b ∈ a :: l

Tactic:
simpa using eq_or_mem_of_mem_insertIdx hb

Result:
no goals

Proof state:
α : Type u
n : ℕ
a : α
l : List α
⊢ insertIdx n a l ⊆ a :: l

Tactic:
intro b hb

Result:
α : Type u
n : ℕ
a : α
l : List α
b : α
hb : b ∈ insertIdx n a l
⊢ b ∈ a :: l