harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Sigma.lean
theorem perm_dlookup (a : α) {l₁ l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys)
    (p : l₁ ~ l₂) : dlookup a l₁ = dlookup a l₂

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
nd₂ : l₂.NodupKeys
p : l₁ ~ l₂
⊢ dlookup a l₁ = dlookup a l₂

Tactic:
ext b

Result:
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
nd₂ : l₂.NodupKeys
p : l₁ ~ l₂
b : β a
⊢ b ∈ dlookup a l₁ ↔ b ∈ dlookup a l₂

Proof state:
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
nd₂ : l₂.NodupKeys
p : l₁ ~ l₂
b : β a
⊢ b ∈ dlookup a l₁ ↔ b ∈ dlookup a l₂

Tactic:
simp only [mem_dlookup_iff nd₁, mem_dlookup_iff nd₂]

Result:
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
nd₂ : l₂.NodupKeys
p : l₁ ~ l₂
b : β a
⊢ ⟨a, b⟩ ∈ l₁ ↔ ⟨a, b⟩ ∈ l₂

Proof state:
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
nd₂ : l₂.NodupKeys
p : l₁ ~ l₂
b : β a
⊢ ⟨a, b⟩ ∈ l₁ ↔ ⟨a, b⟩ ∈ l₂

Tactic:
exact p.mem_iff

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncGE.lean
lemma truncGE'Map_f_eq_opcyclesMap {i : ι} (hi : e.BoundaryGE i) {i' : ι'} (h : e.f i = i') :
    (truncGE'Map φ e).f i =
      (K.truncGE'XIsoOpcycles e h hi).hom ≫ opcyclesMap φ i' ≫
        (L.truncGE'XIsoOpcycles e h hi).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryGE i
i' : ι'
h : e.f i = i'
⊢ (truncGE'Map φ e).f i = (K.truncGE'XIsoOpcycles e h hi).hom ≫ opcyclesMap φ i' ≫ (L.truncGE'XIsoOpcycles e h hi).inv

Tactic:
subst h

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryGE i
⊢ (truncGE'Map φ e).f i =
    (K.truncGE'XIsoOpcycles e ⋯ hi).hom ≫ opcyclesMap φ (e.f i) ≫ (L.truncGE'XIsoOpcycles e ⋯ hi).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryGE i
⊢ (truncGE'Map φ e).f i =
    (K.truncGE'XIsoOpcycles e ⋯ hi).hom ≫ opcyclesMap φ (e.f i) ≫ (L.truncGE'XIsoOpcycles e ⋯ hi).inv

Tactic:
exact dif_pos hi

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem tail_zip (l₁ : List α) (l₂ : List β) :
    (zip l₁ l₂).tail = zip l₁.tail l₂.tail

Proof state:
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
⊢ (l₁.zip l₂).tail = l₁.tail.zip l₂.tail

Tactic:
cases l₁ <;> cases l₂ <;> simp

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem graph_injective : Injective (graph : (α → β) → Rel α β)

Proof state:
case h
α : Type u_1
β : Type u_2
a₁✝ g : α → β
h : graph a₁✝ = graph g
x : α
h2 : graph a₁✝ x (g x) = graph g x (g x)
⊢ a₁✝ x = g x

Tactic:
simp only [graph_def, eq_iff_iff, iff_true] at h2

Result:
case h
α : Type u_1
β : Type u_2
a₁✝ g : α → β
h : graph a₁✝ = graph g
x : α
h2 : a₁✝ x = g x
⊢ a₁✝ x = g x

Proof state:
case h
α : Type u_1
β : Type u_2
a₁✝ g : α → β
h : graph a₁✝ = graph g
x : α
h2 : a₁✝ x = g x
⊢ a₁✝ x = g x

Tactic:
exact h2

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
a₁✝ g : α → β
h : graph a₁✝ = graph g
x : α
⊢ a₁✝ x = g x

Tactic:
have h2 := congr_fun₂ h x (g x)

Result:
case h
α : Type u_1
β : Type u_2
a₁✝ g : α → β
h : graph a₁✝ = graph g
x : α
h2 : graph a₁✝ x (g x) = graph g x (g x)
⊢ a₁✝ x = g x

Proof state:
α : Type u_1
β : Type u_2
a₁✝ g : α → β
h : graph a₁✝ = graph g
⊢ a₁✝ = g

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
a₁✝ g : α → β
h : graph a₁✝ = graph g
x : α
⊢ a₁✝ x = g x

Proof state:
α : Type u_1
β : Type u_2
⊢ Injective graph

Tactic:
intro _ g h

Result:
α : Type u_1
β : Type u_2
a₁✝ g : α → β
h : graph a₁✝ = graph g
⊢ a₁✝ = g
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Pairwise.lean
theorem pwFilter_eq_self [DecidableRel (α := α) R] {l : List α} :
    pwFilter R l = l ↔ Pairwise R l

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
p : Pairwise R l
⊢ pwFilter R l = l

Tactic:
induction l with
| nil => rfl
| cons x l IH =>
  let ⟨al, p⟩ := pairwise_cons.1 p
  rw [pwFilter_cons_of_pos fun b hb => ?_, IH p]
  rw [IH p] at hb
  exact al _ hb

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
⊢ pwFilter R l = l ↔ Pairwise R l

Tactic:
refine ⟨fun e => e ▸ pairwise_pwFilter l, fun p => ?_⟩

Result:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
p : Pairwise R l
⊢ pwFilter R l = l

Proof state:
case cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
x : α
l : List α
IH : Pairwise R l → pwFilter R l = l
p✝ : Pairwise R (x :: l)
al : ∀ (a' : α), a' ∈ l → R x a'
p : Pairwise R l
⊢ pwFilter R (x :: l) = x :: l

Tactic:
rw [pwFilter_cons_of_pos fun b hb => ?_, IH p]

Result:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
x : α
l : List α
IH : Pairwise R l → pwFilter R l = l
p✝ : Pairwise R (x :: l)
al : ∀ (a' : α), a' ∈ l → R x a'
p : Pairwise R l
b : α
hb : b ∈ pwFilter R l
⊢ R x b

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
x : α
l : List α
IH : Pairwise R l → pwFilter R l = l
p✝ : Pairwise R (x :: l)
al : ∀ (a' : α), a' ∈ l → R x a'
p : Pairwise R l
b : α
hb : b ∈ pwFilter R l
⊢ R x b

Tactic:
rw [IH p] at hb

Result:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
x : α
l : List α
IH : Pairwise R l → pwFilter R l = l
p✝ : Pairwise R (x :: l)
al : ∀ (a' : α), a' ∈ l → R x a'
p : Pairwise R l
b : α
hb : b ∈ l
⊢ R x b

Proof state:
case cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
x : α
l : List α
IH : Pairwise R l → pwFilter R l = l
p : Pairwise R (x :: l)
⊢ pwFilter R (x :: l) = x :: l

Tactic:
let ⟨al, p⟩ := pairwise_cons.1 p

Result:
case cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
x : α
l : List α
IH : Pairwise R l → pwFilter R l = l
p✝ : Pairwise R (x :: l)
al : ∀ (a' : α), a' ∈ l → R x a'
p : Pairwise R l
⊢ pwFilter R (x :: l) = x :: l

Proof state:
case nil
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
p : Pairwise R []
⊢ pwFilter R [] = []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
x : α
l : List α
IH : Pairwise R l → pwFilter R l = l
p✝ : Pairwise R (x :: l)
al : ∀ (a' : α), a' ∈ l → R x a'
p : Pairwise R l
b : α
hb : b ∈ l
⊢ R x b

Tactic:
exact al _ hb

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
theorem EuclideanSpace.volume_preserving_measurableEquiv :
    MeasurePreserving (EuclideanSpace.measurableEquiv ι)

Proof state:
ι : Type u_4
inst✝ : Fintype ι
this : volume = map (⇑(EuclideanSpace.measurableEquiv ι).symm) volume
⊢ MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume

Tactic:
convert ((EuclideanSpace.measurableEquiv ι).symm.measurable.measurePreserving _).symm

Result:
no goals

Proof state:
ι : Type u_4
inst✝ : Fintype ι
⊢ MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume

Tactic:
suffices volume = map (EuclideanSpace.measurableEquiv ι).symm volume by
  convert ((EuclideanSpace.measurableEquiv ι).symm.measurable.measurePreserving _).symm

Result:
ι : Type u_4
inst✝ : Fintype ι
⊢ volume = map (⇑(EuclideanSpace.measurableEquiv ι).symm) volume

Proof state:
ι : Type u_4
inst✝ : Fintype ι
⊢ volume = ((Pi.basisFun ℝ ι).map (PiLp.continuousLinearEquiv 2 ℝ fun a => ℝ).symm.toLinearEquiv).addHaar

Tactic:
exact (EuclideanSpace.basisFun _ _).addHaar_eq_volume.symm

Result:
no goals

Proof state:
ι : Type u_4
inst✝ : Fintype ι
⊢ volume = map (⇑(EuclideanSpace.measurableEquiv ι).symm) volume

Tactic:
rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar_def,
  coe_measurableEquiv_symm, ← PiLp.continuousLinearEquiv_symm_apply 2 ℝ, Basis.map_addHaar]

Result:
ι : Type u_4
inst✝ : Fintype ι
⊢ volume = ((Pi.basisFun ℝ ι).map (PiLp.continuousLinearEquiv 2 ℝ fun a => ℝ).symm.toLinearEquiv).addHaar
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_append_left {a : α} (pa : p a) :
    ∀ {l₁ : List α} l₂, a ∈ l₁ → (l₁++l₂).eraseP p = l₁.eraseP p ++ l₂
  | x :: xs, l₂, h => by
    by_cases h' : p x <;> simp [h']
    rw [eraseP_append_left pa l₂ ((mem_cons.1 h).resolve_left (mt _ h'))]
    intro | rfl => exact pa

Proof state:
α : Type u_1
p : α → Bool
a : α
pa : p a = true
x : α
xs l₂ : List α
x✝ : a = x
h : a ∈ a :: xs
h' : ¬p a = true
⊢ p a = true

Tactic:
exact pa

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
pa : p a = true
x : α
xs l₂ : List α
h : a ∈ x :: xs
h' : ¬p x = true
⊢ a = x → p x = true

Tactic:
intro | rfl => exact pa

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
pa : p a = true
x : α
xs l₂ : List α
h : a ∈ x :: xs
⊢ eraseP p (x :: xs ++ l₂) = eraseP p (x :: xs) ++ l₂

Tactic:
by_cases h' : p x <;> simp [h']

Result:
case neg
α : Type u_1
p : α → Bool
a : α
pa : p a = true
x : α
xs l₂ : List α
h : a ∈ x :: xs
h' : ¬p x = true
⊢ eraseP p (xs ++ l₂) = eraseP p xs ++ l₂

Proof state:
case neg
α : Type u_1
p : α → Bool
a : α
pa : p a = true
x : α
xs l₂ : List α
h : a ∈ x :: xs
h' : ¬p x = true
⊢ eraseP p (xs ++ l₂) = eraseP p xs ++ l₂

Tactic:
rw [eraseP_append_left pa l₂ ((mem_cons.1 h).resolve_left (mt _ h'))]

Result:
α : Type u_1
p : α → Bool
a : α
pa : p a = true
x : α
xs l₂ : List α
h : a ∈ x :: xs
h' : ¬p x = true
⊢ a = x → p x = true
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two (x y : V) :
    ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ inner x y = 0 ↔ angle x y = π / 2

Tactic:
exact inner_eq_zero_iff_angle_eq_pi_div_two x y

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2

Tactic:
rw [norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ inner x y = 0 ↔ angle x y = π / 2
-- Mathlib/RingTheory/RootsOfUnity/Lemmas.lean
/-- If `μ` is a primitive `n`th root of unity in `R`, then `(-1)^(n-1) * ∏(1≤k<n) (μ^k-1) = n`.
(Stated with `n+1` in place of `n` to avoid the condition `n ≠ 0`.) -/
lemma prod_pow_sub_one_eq_order {n : ℕ} {μ : R} (hμ : IsPrimitiveRoot μ (n + 1)) :
    (-1) ^ n * ∏ k ∈ range n, (μ ^ (k + 1) - 1) = n + 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : (-1) ^ n = ∏ k ∈ range n, -1
⊢ (-1) ^ n * ∏ k ∈ range n, (μ ^ (k + 1) - 1) = ↑n + 1

Tactic:
simp only [this, ← prod_mul_distrib, neg_one_mul, neg_sub, ← prod_one_sub_pow_eq_order hμ]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
⊢ (-1) ^ n * ∏ k ∈ range n, (μ ^ (k + 1) - 1) = ↑n + 1

Tactic:
have : (-1 : R) ^ n = ∏ k ∈ range n, -1 := by rw [prod_const, card_range]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : (-1) ^ n = ∏ k ∈ range n, -1
⊢ (-1) ^ n * ∏ k ∈ range n, (μ ^ (k + 1) - 1) = ↑n + 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
⊢ (-1) ^ n = ∏ k ∈ range n, -1

Tactic:
rw [prod_const, card_range]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem of_basis_right {ι : Type*} (n : Basis ι R N)
    (H : LinearMap.ker (mulRightMap M n) = ⊥) : M.LinearDisjoint N

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis ι R ↥N
H : LinearMap.ker (M.mulRightMap ⇑n) = ⊥
⊢ M.LinearDisjoint N

Tactic:
letI : AddCommGroup (ι →₀ M) := Finsupp.instAddCommGroup

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis ι R ↥N
H : LinearMap.ker (M.mulRightMap ⇑n) = ⊥
this : AddCommGroup (ι →₀ ↥M) := Finsupp.instAddCommGroup
⊢ M.LinearDisjoint N

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
n : Basis ι R ↥N
H : LinearMap.ker (M.mulRightMap ⇑n) = ⊥
this : AddCommGroup (ι →₀ ↥M) := Finsupp.instAddCommGroup
⊢ M.LinearDisjoint N

Tactic:
exact of_basis_right' M N n (LinearMap.ker_eq_bot.1 H)

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
@[simp, norm_cast] lemma one_lt_coe : 1 < (r : ℝ) ↔ 1 < r

Proof state:
r : ℝ≥0
⊢ 1 < ↑r ↔ 1 < r

Tactic:
rw [← coe_lt_coe, coe_one]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem MulOneClass.ext {M : Type u} : ∀ ⦃m₁ m₂ : MulOneClass M⦄, m₁.mul = m₂.mul → m₁ = m₂

Proof state:
case mk.mk.mk.mk.mk.mk.refl
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ one₁ = one₂

Tactic:
exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂)

Result:
no goals

Proof state:
case mk.mk.mk.mk.mk.mk.refl
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ mk one_mul₁ mul_one₁ = mk one_mul₂ mul_one₂

Tactic:
suffices one₁ = one₂ by cases this; rfl

Result:
case mk.mk.mk.mk.mk.mk.refl
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ one₁ = one₂

Proof state:
M : Type u
⊢ ∀ ⦃m₁ m₂ : MulOneClass M⦄, Mul.mul = Mul.mul → m₁ = m₂

Tactic:
rintro @⟨⟨one₁⟩, ⟨mul₁⟩, one_mul₁, mul_one₁⟩ @⟨⟨one₂⟩, ⟨mul₂⟩, one_mul₂, mul_one₂⟩ ⟨rfl⟩

Result:
case mk.mk.mk.mk.mk.mk.refl
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ mk one_mul₁ mul_one₁ = mk one_mul₂ mul_one₂

Proof state:
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
this : one₁ = one₂
⊢ mk one_mul₁ mul_one₁ = mk one_mul₂ mul_one₂

Tactic:
cases this

Result:
case refl
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ mk one_mul₁ mul_one₁ = mk one_mul₂ mul_one₂

Proof state:
case refl
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ mk one_mul₁ mul_one₁ = mk one_mul₂ mul_one₂

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem closedPoint_mem_iff (U : TopologicalSpace.Opens <| PrimeSpectrum R) :
    closedPoint R ∈ U ↔ U = ⊤

Proof state:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → ⊤ ≤ U

Tactic:
exact fun h x _ => (specializes_closedPoint x).mem_open U.2 h

Result:
no goals

Proof state:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → U = ⊤

Tactic:
rw [eq_top_iff]

Result:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → ⊤ ≤ U

Proof state:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ closedPoint R ∈ ⊤

Tactic:
trivial

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U ↔ U = ⊤

Tactic:
constructor

Result:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → U = ⊤

case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ U = ⊤ → closedPoint R ∈ U

Proof state:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ U = ⊤ → closedPoint R ∈ U

Tactic:
rintro rfl

Result:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ closedPoint R ∈ ⊤
-- Mathlib/Data/Num/Lemmas.lean
theorem le_iff_cmp {m n} : m ≤ n ↔ cmp m n ≠ Ordering.gt :=
  not_congr <| lt_iff_cmp.trans <| by rw [← cmp_swap]; cases cmp m n <;> decide

Proof state:
m n : Num
⊢ (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
cases cmp m n <;> decide

Result:
no goals

Proof state:
m n : Num
⊢ n.cmp m = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
rw [← cmp_swap]

Result:
m n : Num
⊢ (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt
-- Mathlib/Algebra/Field/Basic.lean
theorem div_sub_div_same (a b c : K) : a / c - b / c = (a - b) / c

Proof state:
K : Type u_1
inst✝ : DivisionRing K
a b c : K
⊢ a / c - b / c = (a - b) / c

Tactic:
rw [sub_eq_add_neg, ← neg_div, div_add_div_same, sub_eq_add_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
theorem epi_inl_of_is_pushout_of_epi {t : PushoutCocone f g} (ht : IsColimit t) [Epi g] :
    Epi t.inl :=
  ⟨fun {W} h k i => IsColimit.hom_ext ht i (by simp [← cancel_epi g, ← t.condition_assoc, i])⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
inst✝ : Epi g
W : C
h k : t.pt ⟶ W
i : t.inl ≫ h = t.inl ≫ k
⊢ t.inr ≫ h = t.inr ≫ k

Tactic:
simp [← cancel_epi g, ← t.condition_assoc, i]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem natTrailingDegree_reverse (f : R[X]) : f.reverse.natTrailingDegree = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.natTrailingDegree = 0

Tactic:
rw [natTrailingDegree_eq_zero, reverse_eq_zero, coeff_zero_reverse, leadingCoeff_ne_zero]

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f = 0 ∨ f ≠ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f = 0 ∨ f ≠ 0

Tactic:
exact eq_or_ne _ _

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem prodMap_map_product {δ : Type*} (f : α ↪ β) (g : γ ↪ δ) (s : Finset α) (t : Finset γ) :
    (s ×ˢ t).map (f.prodMap g) = s.map f ×ˢ t.map g

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α ↪ β
g : γ ↪ δ
s : Finset α
t : Finset γ
⊢ map (f.prodMap g) (s ×ˢ t) = map f s ×ˢ map g t

Tactic:
simpa [← coe_inj] using Set.prodMap_image_prod f g s t

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
lemma toRight_inter : (u ∩ v).toRight = u.toRight ∩ v.toRight

Proof state:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∩ v).toRight = u.toRight ∩ v.toRight

Tactic:
ext x

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

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

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem get?_of_eq_some_of_succ_get?_intFractPair_stream {ifp_succ_n : IntFractPair K}
    (stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n) :
    (of v).s.get? n = some ⟨1, ifp_succ_n.b⟩

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ (of v).s.get? n = some { a := 1, b := ↑ifp_succ_n.b }

Tactic:
unfold of IntFractPair.seq1

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ (match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
          | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).s.get?
      n =
    some { a := 1, b := ↑ifp_succ_n.b }

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ (match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
          | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).s.get?
      n =
    some { a := 1, b := ↑ifp_succ_n.b }

Tactic:
simp [Stream'.Seq.map_tail, Stream'.Seq.get?_tail, Stream'.Seq.map_get?, stream_succ_nth_eq]

Result:
no goals
-- Mathlib/Data/Set/Card/Arithmetic.lean
theorem Finset.exists_disjoint_union_of_even_card_iff [DecidableEq α] (s : Finset α) :
    Even #s ↔ ∃ (t u : Finset α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u :=
  ⟨Finset.exists_disjoint_union_of_even_card, by
    rintro ⟨t, u, rfl, hdtu, hctu⟩
    simp_all⟩

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
t u : Finset α
hdtu : Disjoint t u
hctu : #t = #u
⊢ Even #(t ∪ u)

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ (∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #t = #u) → Even #s

Tactic:
rintro ⟨t, u, rfl, hdtu, hctu⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
t u : Finset α
hdtu : Disjoint t u
hctu : #t = #u
⊢ Even #(t ∪ u)