harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Part.lean
theorem elim_toOption {α β : Type*} (a : Part α) [Decidable a.Dom] (b : β) (f : α → β) :
    a.toOption.elim b f = if h : a.Dom then f (a.get h) else b

Proof state:
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
⊢ a.toOption.elim b f = if h : a.Dom then f (a.get h) else b

Tactic:
split_ifs with h

Result:
case pos
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ a.toOption.elim b f = f (a.get h)

case neg
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ a.toOption.elim b f = b

Proof state:
case neg
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ Option.none.elim b f = b

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ a.toOption.elim b f = f (a.get h)

Tactic:
rw [h.toOption]

Result:
case pos
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ (Option.some (a.get h)).elim b f = f (a.get h)

Proof state:
case neg
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ a.toOption.elim b f = b

Tactic:
rw [Part.toOption_eq_none_iff.2 h]

Result:
case neg
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ Option.none.elim b f = b

Proof state:
case pos
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ (Option.some (a.get h)).elim b f = f (a.get h)

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem apply_lt_nfpBFamily (H : ∀ i hi, IsNormal (f i hi)) {a b} (hb : b < nfpBFamily.{u, v} o f a)
    (i hi) : f i hi b < nfpBFamily.{u, v} o f a

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
hb : b < o.nfpBFamily f a
i : Ordinal.{u}
hi : i < o
⊢ o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩) b < o.nfpBFamily f a

Tactic:
apply apply_lt_nfpFamily (fun _ => H _ _) hb

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
hb : b < o.nfpBFamily f a
i : Ordinal.{u}
hi : i < o
⊢ f i hi b < o.nfpBFamily f a

Tactic:
rw [← familyOfBFamily_enum o f]

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a b : Ordinal.{max u v}
hb : b < o.nfpBFamily f a
i : Ordinal.{u}
hi : i < o
⊢ o.familyOfBFamily f ((enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩) b < o.nfpBFamily f a
-- Mathlib/RingTheory/Adjoin/Basic.lean
lemma commute_of_mem_adjoin_of_forall_mem_commute {a b : A} {s : Set A}
    (hb : b ∈ adjoin R s) (h : ∀ b ∈ s, Commute a b) :
    Commute a b

Proof state:
case mem
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
x : A
hx : x ∈ s
⊢ Commute a x

Tactic:
exact h x hx

Result:
no goals

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : A
s : Set A
hb : b ∈ adjoin R s
h : ∀ b ∈ s, Commute a b
⊢ Commute a b

Tactic:
induction hb using adjoin_induction with
| mem x hx => exact h x hx
| algebraMap r => exact commutes r a |>.symm
| add y z _ _ hy hz => exact hy.add_right hz
| mul y z _ _ hy hz => exact hy.mul_right hz

Result:
no goals

Proof state:
case algebraMap
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
r : R
⊢ Commute a ((algebraMap R A) r)

Tactic:
exact commutes r a |>.symm

Result:
no goals

Proof state:
case mul
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
y z : A
hx✝ : y ∈ adjoin R s
hy✝ : z ∈ adjoin R s
hy : Commute a y
hz : Commute a z
⊢ Commute a (y * z)

Tactic:
exact hy.mul_right hz

Result:
no goals

Proof state:
case add
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
y z : A
hx✝ : y ∈ adjoin R s
hy✝ : z ∈ adjoin R s
hy : Commute a y
hz : Commute a z
⊢ Commute a (y + z)

Tactic:
exact hy.add_right hz

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem eq_of_eqOnSource_univ (e e' : PartialEquiv α β) (h : e ≈ e') (s : e.source = univ)
    (t : e.target = univ) : e = e'

Proof state:
case refine_1.a
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ univ

Tactic:
exact mem_univ _

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ ↑e.symm x = ↑e'.symm x

Tactic:
apply h.symm'.2

Result:
case refine_2.a
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ e.symm.source

Proof state:
case refine_2.a
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ e.symm.source

Tactic:
rw [symm_source, t]

Result:
case refine_2.a
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ univ

Proof state:
case refine_2.a
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ univ

Tactic:
exact mem_univ _

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ ↑e x = ↑e' x

Tactic:
apply h.2

Result:
case refine_1.a
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ e.source

Proof state:
case refine_1.a
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ e.source

Tactic:
rw [s]

Result:
case refine_1.a
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ univ

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
⊢ e = e'

Tactic:
refine PartialEquiv.ext (fun x => ?_) (fun x => ?_) h.1

Result:
case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ ↑e x = ↑e' x

case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ ↑e.symm x = ↑e'.symm x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zip_mkArray {a : α} {b : β} {m n : Nat} :
    zip (mkArray m a) (mkArray n b) = mkArray (min m n) (a, b)

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
m n : Nat
⊢ (mkArray m a).zip (mkArray n b) = mkArray (min m n) (a, b)

Tactic:
simp [← List.toArray_replicate]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Subcategory.lean
lemma W.mk' {T : Triangle C} (hT : T ∈ distTriang C) (h : S.P T.obj₁) : S.W T.mor₂

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : S.P T.obj₁
⊢ ∃ X f h, ∃ (_ : Triangle.mk f T.mor₂ h ∈ distinguishedTriangles), S.P X

Tactic:
exact ⟨_, _, _, hT, h⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : S.P T.obj₁
⊢ S.W T.mor₂

Tactic:
rw [W_iff']

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : S.P T.obj₁
⊢ ∃ X f h, ∃ (_ : Triangle.mk f T.mor₂ h ∈ distinguishedTriangles), S.P X
-- Mathlib/Algebra/Order/Floor.lean
theorem le_floor_add (a b : α) : ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋

Tactic:
rw [le_floor, Int.cast_add]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ↑⌊a⌋ + ↑⌊b⌋ ≤ a + b

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ↑⌊a⌋ + ↑⌊b⌋ ≤ a + b

Tactic:
gcongr <;> apply floor_le

Result:
no goals
-- Mathlib/Tactic/Module.lean
theorem atom_eq_eval [AddMonoid M] (x : M) : x = NF.eval [(1, x)]

Proof state:
M : Type u_3
inst✝ : AddMonoid M
x : M
⊢ x = eval [(1, x)]

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_dblU (P : Fin 3 → R) : (W'.map f).toJacobian.dblU (f ∘ P) = f (W'.dblU P)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toJacobian.a₁ * (⇑f ∘ P) y * (⇑f ∘ P) z -
      (3 * (⇑f ∘ P) x ^ 2 + 2 * (map W' f).toJacobian.a₂ * (⇑f ∘ P) x * (⇑f ∘ P) z ^ 2 +
        (map W' f).toJacobian.a₄ * (⇑f ∘ P) z ^ 4) =
    f (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4))

Tactic:
map_simp

Result:
no goals

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

Tactic:
simp only [dblU_eq]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toJacobian.a₁ * (⇑f ∘ P) y * (⇑f ∘ P) z -
      (3 * (⇑f ∘ P) x ^ 2 + 2 * (map W' f).toJacobian.a₂ * (⇑f ∘ P) x * (⇑f ∘ P) z ^ 2 +
        (map W' f).toJacobian.a₄ * (⇑f ∘ P) z ^ 4) =
    f (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4))
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_lineMap_right (p₁ p₂ : P) (c : 𝕜) :
    dist (lineMap p₁ p₂ c) p₂ = ‖1 - c‖ * dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
⊢ dist ((lineMap p₁ p₂) c) p₂ = ‖1 - c‖ * dist p₁ p₂

Tactic:
simpa only [lineMap_apply_one, dist_eq_norm'] using dist_lineMap_lineMap p₁ p₂ c 1

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem δ_comp_σ_of_gt' {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) :
    δ i ≫ σ j = σ (j.castLT ((add_lt_add_iff_right 1).mp (lt_of_lt_of_le H i.is_le))) ≫
      δ (i.pred fun (hi : i = 0) => by simp only [Fin.not_lt_zero, hi] at H)

Proof state:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ δ i ≫ σ j = σ (j.castLT ⋯) ≫ δ (i.pred ⋯)

Tactic:
rw [← δ_comp_σ_of_gt]

Result:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ δ i ≫ σ j = δ (i.pred ⋯).succ ≫ σ (j.castLT ⋯).castSucc

n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ (j.castLT ⋯).castSucc < i.pred ⋯

Proof state:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
hi : i = 0
⊢ False

Tactic:
simp only [Fin.not_lt_zero, hi] at H

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ (j.castLT ⋯).castSucc < i.pred ⋯

Tactic:
rw [Fin.castSucc_castLT, ← Fin.succ_lt_succ_iff, Fin.succ_pred]

Result:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ j.succ < i

Proof state:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ j.succ < i

Tactic:
exact H

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ δ i ≫ σ j = δ (i.pred ⋯).succ ≫ σ (j.castLT ⋯).castSucc

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
lemma NNReal.ball_zero_eq_Ico (c : ℝ) :
    Metric.ball (0 : ℝ≥0) c = Set.Ico 0 c.toNNReal

Proof state:
case pos
c : ℝ
c_pos : 0 < c
⊢ ball 0 c = Ico 0 c.toNNReal

Tactic:
convert NNReal.ball_zero_eq_Ico' ⟨c, c_pos.le⟩

Result:
case h.e'_3.h.e'_4
c : ℝ
c_pos : 0 < c
⊢ c.toNNReal = ⟨c, ⋯⟩

Proof state:
case neg
c : ℝ
c_pos : ¬0 < c
⊢ ball 0 c = Ico 0 c.toNNReal

Tactic:
simp [not_lt.mp c_pos]

Result:
no goals

Proof state:
case h.e'_3.h.e'_4
c : ℝ
c_pos : 0 < c
⊢ c.toNNReal = ⟨c, ⋯⟩

Tactic:
simp [Real.toNNReal, c_pos.le]

Result:
no goals

Proof state:
c : ℝ
⊢ ball 0 c = Ico 0 c.toNNReal

Tactic:
by_cases c_pos : 0 < c

Result:
case pos
c : ℝ
c_pos : 0 < c
⊢ ball 0 c = Ico 0 c.toNNReal

case neg
c : ℝ
c_pos : ¬0 < c
⊢ ball 0 c = Ico 0 c.toNNReal
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zipWith_foldr_eq_zip_foldr {f : α → β → γ} (i : δ):
    (zipWith f l₁ l₂).foldr g i = (zip l₁ l₂).foldr (fun p r => g (f p.1 p.2) r) i

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
g : γ → δ → δ
f : α → β → γ
i : δ
l₁ : Array α
l₂ : Vector β l₁.size
⊢ foldr g i (zipWith f { toArray := l₁, size_toArray := ⋯ } l₂) =
    foldr (fun p r => g (f p.fst p.snd) r) i ({ toArray := l₁, size_toArray := ⋯ }.zip l₂)

Tactic:
rcases l₂ with ⟨l₂, h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
g : γ → δ → δ
f : α → β → γ
i : δ
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ foldr g i (zipWith f { toArray := l₁, size_toArray := ⋯ } { toArray := l₂, size_toArray := h }) =
    foldr (fun p r => g (f p.fst p.snd) r) i
      ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h })

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
n✝ : Nat
l₁ : Vector α n✝
l₂ : Vector β n✝
g : γ → δ → δ
f : α → β → γ
i : δ
⊢ foldr g i (zipWith f l₁ l₂) = foldr (fun p r => g (f p.fst p.snd) r) i (l₁.zip l₂)

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
g : γ → δ → δ
f : α → β → γ
i : δ
l₁ : Array α
l₂ : Vector β l₁.size
⊢ foldr g i (zipWith f { toArray := l₁, size_toArray := ⋯ } l₂) =
    foldr (fun p r => g (f p.fst p.snd) r) i ({ toArray := l₁, size_toArray := ⋯ }.zip l₂)

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
g : γ → δ → δ
f : α → β → γ
i : δ
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ foldr g i (zipWith f { toArray := l₁, size_toArray := ⋯ } { toArray := l₂, size_toArray := h }) =
    foldr (fun p r => g (f p.fst p.snd) r) i
      ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h })

Tactic:
simpa using Array.zipWith_foldr_eq_zip_foldr _

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem Subperm.filter (p : α → Bool) ⦃l l' : List α⦄ (h : l <+~ l') :
    filter p l <+~ filter p l'

Proof state:
α : Type u_1
p : α → Bool
l l' : List α
h✝ : l <+~ l'
xs : List α
hp : xs ~ l
h : xs <+ l'
⊢ List.filter p l <+~ List.filter p l'

Tactic:
exact ⟨_, hp.filter p, h.filter p⟩

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l l' : List α
h : l <+~ l'
⊢ List.filter p l <+~ List.filter p l'

Tactic:
let ⟨xs, hp, h⟩ := h

Result:
α : Type u_1
p : α → Bool
l l' : List α
h✝ : l <+~ l'
xs : List α
hp : xs ~ l
h : xs <+ l'
⊢ List.filter p l <+~ List.filter p l'
-- Mathlib/Algebra/RingQuot.lean
theorem mkAlgHom_surjective (s : A → A → Prop) : Function.Surjective (mkAlgHom S s)

Proof state:
case mk.mk
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
toQuot✝ : Quot (Rel s)
a : A
⊢ ∃ a_1, (fun x => { toQuot := Quot.mk (Rel s) x }) a_1 = { toQuot := Quot.mk (Rel s) a }

Tactic:
use a

Result:
no goals

Proof state:
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
⊢ Function.Surjective ⇑(mkAlgHom S s)

Tactic:
suffices Function.Surjective fun x ↦ (⟨.mk (Rel s) x⟩ : RingQuot s) by
  simpa [mkAlgHom_def, mkRingHom_def]

Result:
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
⊢ Function.Surjective fun x => { toQuot := Quot.mk (Rel s) x }

Proof state:
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
⊢ Function.Surjective fun x => { toQuot := Quot.mk (Rel s) x }

Tactic:
rintro ⟨⟨a⟩⟩

Result:
case mk.mk
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
toQuot✝ : Quot (Rel s)
a : A
⊢ ∃ a_1, (fun x => { toQuot := Quot.mk (Rel s) x }) a_1 = { toQuot := Quot.mk (Rel s) a }

Proof state:
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
this : Function.Surjective fun x => { toQuot := Quot.mk (Rel s) x }
⊢ Function.Surjective ⇑(mkAlgHom S s)

Tactic:
simpa [mkAlgHom_def, mkRingHom_def]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem map_int_of_map_zero (n : ℤ) : f n = f 0 + n

Proof state:
f : CircleDeg1Lift
n : ℤ
⊢ f ↑n = f 0 + ↑n

Tactic:
rw [← f.map_add_int, zero_add]

Result:
no goals
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem Wequiv.refl (x : q.P.W) : Wequiv x x

Proof state:
F : Type u → Type u
q : QPF F
x : (P F).W
⊢ Wequiv x x

Tactic:
obtain ⟨a, f⟩ := x

Result:
case mk
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
⊢ Wequiv (WType.mk a f) (WType.mk a f)

Proof state:
case mk
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
⊢ Wequiv (WType.mk a f) (WType.mk a f)

Tactic:
exact Wequiv.abs a f a f rfl

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Hermite/Gaussian.lean
theorem hermite_eq_deriv_gaussian' (n : ℕ) (x : ℝ) : aeval x (hermite n) =
    (-1 : ℝ) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)

Proof state:
n : ℕ
x : ℝ
⊢ (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x / (Real.exp (x ^ 2 / 2))⁻¹ =
    (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)

Tactic:
field_simp [Real.exp_ne_zero]

Result:
no goals

Proof state:
n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) = (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)

Tactic:
rw [hermite_eq_deriv_gaussian, Real.exp_neg]

Result:
n : ℕ
x : ℝ
⊢ (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x / (Real.exp (x ^ 2 / 2))⁻¹ =
    (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)
-- Mathlib/GroupTheory/Index.lean
theorem index_mul_card : H.index * Nat.card H = Nat.card G

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index * Nat.card ↥H = Nat.card G

Tactic:
rw [mul_comm, card_mul_index]

Result:
no goals
-- Mathlib/CategoryTheory/Quotient.lean
theorem functor_map_eq_iff [h : Congruence r] {X Y : C} (f f' : X ⟶ Y) :
    (functor r).map f = (functor r).map f' ↔ r f f'

Proof state:
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ _root_.Equivalence (CompClosure r)

Tactic:
simpa only [compClosure_eq_self r] using h.equivalence

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ (functor r).map f = (functor r).map f' ↔ r f f'

Tactic:
dsimp [functor]

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ Quot.mk (CompClosure r) f = Quot.mk (CompClosure r) f' ↔ r f f'

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ Quot.mk (CompClosure r) f = Quot.mk (CompClosure r) f' ↔ r f f'

Tactic:
rw [Equivalence.quot_mk_eq_iff, compClosure_eq_self r]

Result:
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ _root_.Equivalence (CompClosure r)
-- Mathlib/CategoryTheory/Triangulated/Basic.lean
lemma Triangle.eqToHom_hom₃ {A B : Triangle C} (h : A = B) :
    (eqToHom h).hom₃ = eqToHom (by subst h; rfl)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A : Triangle C
⊢ A.obj₃ = A.obj₃

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A : Triangle C
⊢ (eqToHom ⋯).hom₃ = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
h : A = B
⊢ (eqToHom h).hom₃ = eqToHom ⋯

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A : Triangle C
⊢ (eqToHom ⋯).hom₃ = eqToHom ⋯

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A B : Triangle C
h : A = B
⊢ A.obj₃ = B.obj₃

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A : Triangle C
⊢ A.obj₃ = A.obj₃
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp] lemma one_le_zpow_iff_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) : 1 ≤ a ^ n ↔ n ≤ 0

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ 1 ≤ a ^ n ↔ n ≤ 0

Tactic:
simp [← zpow_le_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
lemma schnirelmannDensity_le_one : schnirelmannDensity A ≤ 1 :=
  schnirelmannDensity_le_of_le 1 one_ne_zero <|
    by rw [Nat.cast_one, div_one, Nat.cast_le_one]; exact card_filter_le _ _

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ ↑(#(filter (fun a => a ∈ A) (Ioc 0 1))) / ↑1 ≤ 1

Tactic:
rw [Nat.cast_one, div_one, Nat.cast_le_one]

Result:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ #(filter (fun a => a ∈ A) (Ioc 0 1)) ≤ 1

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ #(filter (fun a => a ∈ A) (Ioc 0 1)) ≤ 1

Tactic:
exact card_filter_le _ _

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_mul_C (a0 : a ≠ 0) : (p * C a).natDegree = p.natDegree

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
a0 : a ≠ 0
⊢ (p * C a).natDegree = p.natDegree

Tactic:
simp only [natDegree, degree_mul_C a0]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
theorem zmodChar_apply' {n : ℕ} [NeZero n] {ζ : C} (hζ : ζ ^ n = 1) (a : ℕ) :
    zmodChar n hζ a = ζ ^ a

Proof state:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
hζ : ζ ^ n = 1
a : ℕ
⊢ (zmodChar n hζ) ↑a = ζ ^ a

Tactic:
rw [pow_eq_pow_mod a hζ, zmodChar_apply, ZMod.val_natCast a]

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem Polynomial.quotQuotEquivComm_symm_mk_mk (p : R[X]) :
    (Polynomial.quotQuotEquivComm I f).symm (Ideal.Quotient.mk (span
    ({(Ideal.Quotient.mk (I.map C)) f} : Set (R[X] ⧸ (I.map C)))) (Ideal.Quotient.mk (I.map C) p)) =
      Ideal.Quotient.mk (span {f.map (Ideal.Quotient.mk I)}) (p.map (Ideal.Quotient.mk I))

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotQuotEquivComm I f).symm
      ((Ideal.Quotient.mk (span {(Ideal.Quotient.mk (Ideal.map C I)) f})) ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
    (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)

Tactic:
simp only [Polynomial.quotQuotEquivComm, quotientEquiv_symm_mk,
  polynomialQuotientEquivQuotientPolynomial_symm_mk]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem im_inv_neg_coe_pos (z : ℍ) : 0 < (-z : ℂ)⁻¹.im

Proof state:
z : ℍ
⊢ 0 < (-↑z)⁻¹.im

Tactic:
simpa using div_pos z.property (normSq_pos z)

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_erase_right (a b : α) : (Icc a b).erase b = Ico a b

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Icc a b).erase b = Ico a b

Tactic:
simp [← coe_inj]

Result:
no goals