harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem map_nullHomotopicMap {W : Type*} [Category W] [Preadditive W] (G : V ⥤ W) [G.Additive]
    (hom : ∀ i j, C.X i ⟶ D.X j) :
    (G.mapHomologicalComplex c).map (nullHomotopicMap hom) =
      nullHomotopicMap (fun i j => by exact G.map (hom i j))

Proof state:
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (G.mapHomologicalComplex c).map (nullHomotopicMap hom) = nullHomotopicMap fun i j => G.map (hom i j)

Tactic:
ext i

Result:
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → C.X i ⟶ D.X j
i : ι
⊢ ((G.mapHomologicalComplex c).map (nullHomotopicMap hom)).f i = (nullHomotopicMap fun i j => G.map (hom i j)).f i

Proof state:
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → C.X i ⟶ D.X j
i : ι
⊢ ((G.mapHomologicalComplex c).map (nullHomotopicMap hom)).f i = (nullHomotopicMap fun i j => G.map (hom i j)).f i

Tactic:
dsimp [nullHomotopicMap, dNext, prevD]

Result:
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → C.X i ⟶ D.X j
i : ι
⊢ G.map (C.d i (c.next i) ≫ hom (c.next i) i + hom i (c.prev i) ≫ D.d (c.prev i) i) =
    G.map (C.d i (c.next i)) ≫ G.map (hom (c.next i) i) + G.map (hom i (c.prev i)) ≫ G.map (D.d (c.prev i) i)

Proof state:
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.118044, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
⊢ ((G.mapHomologicalComplex c).obj C).X i ⟶ ((G.mapHomologicalComplex c).obj D).X j

Tactic:
exact G.map (hom i j)

Result:
no goals

Proof state:
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → C.X i ⟶ D.X j
i : ι
⊢ G.map (C.d i (c.next i) ≫ hom (c.next i) i + hom i (c.prev i) ≫ D.d (c.prev i) i) =
    G.map (C.d i (c.next i)) ≫ G.map (hom (c.next i) i) + G.map (hom i (c.prev i)) ≫ G.map (D.d (c.prev i) i)

Tactic:
simp only [G.map_comp, Functor.map_add]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem tensorμ_natural_left {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (Z₁ Z₂ : C) :
    (f₁ ⊗ f₂) ▷ (Z₁ ⊗ Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂ =
      tensorμ X₁ X₂ Z₁ Z₂ ≫ (f₁ ▷ Z₁ ⊗ f₂ ▷ Z₂)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
⊢ (f₁ ⊗ f₂) ▷ (Z₁ ⊗ Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂ = tensorμ X₁ X₂ Z₁ Z₂ ≫ (f₁ ▷ Z₁ ⊗ f₂ ▷ Z₂)

Tactic:
convert tensorμ_natural f₁ f₂ (𝟙 Z₁) (𝟙 Z₂) using 1 <;> simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem fromSpec_preimage_basicOpen' :
    hU.fromSpec ⁻¹ᵁ X.basicOpen f = (Spec Γ(X, U)).basicOpen ((Scheme.ΓSpecIso Γ(X, U)).inv f)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen
      ((ConcreteCategory.hom ((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op)) f) =
    (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)

Tactic:
exact Scheme.basicOpen_res_eq _ _ (eqToHom hU.fromSpec_preimage_self).op

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f = (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)

Tactic:
rw [Scheme.preimage_basicOpen, hU.fromSpec_app_self]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen
      ((ConcreteCategory.hom ((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op)) f) =
    (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)
-- Mathlib/Logic/Function/Basic.lean
theorem extend_def (f : α → β) (g : α → γ) (e' : β → γ) (b : β) [Decidable (∃ a, f a = b)] :
    extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ (if h : ∃ a, f a = b then g (Classical.choose h) else e' b) =
    if h : ∃ a, f a = b then g (Classical.choose h) else e' b

Tactic:
congr

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b

Tactic:
unfold extend

Result:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ (if h : ∃ a, f a = b then g (Classical.choose h) else e' b) =
    if h : ∃ a, f a = b then g (Classical.choose h) else e' b
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_div_dvd' (p : K[X]) {q : K[X]} (hq : q ≠ 0) :
    C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∣ p

Proof state:
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∣ p

Tactic:
simpa using num_div_dvd p hq

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem not_monotoneOn_not_antitoneOn_iff_exists_lt_lt :
    ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
      ∃ᵉ (a ∈ s) (b ∈ s) (c ∈ s), a < b ∧ b < c ∧
        (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Proof state:
α : Type u
β : Type v
s : Set α
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
    ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, and_assoc, exists_and_left,
  not_monotone_not_antitone_iff_exists_lt_lt, @and_left_comm (_ ∈ s)]

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
lemma comap_basicOpen (f : R →+* S) (x : R) :
    comap f (PrimeSpectrum.basicOpen x) (PrimeSpectrum.basicOpen (f x))
        (PrimeSpectrum.comap_basicOpen f x).le =
      IsLocalization.map (M := .powers x) (T := .powers (f x)) _ f
        (Submonoid.powers_le.mpr (Submonoid.mem_powers _)) :=
  IsLocalization.ringHom_ext (.powers x) <| by
    simpa [CommRingCat.hom_ext_iff] using toOpen_comp_comap f _

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
x : R
⊢ (comap f (PrimeSpectrum.basicOpen x) (PrimeSpectrum.basicOpen (f x)) ⋯).comp
      (algebraMap R ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen x)))) =
    (IsLocalization.map (↑((structureSheaf S).val.obj (op (PrimeSpectrum.basicOpen (f x))))) f ⋯).comp
      (algebraMap R ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen x))))

Tactic:
simpa [CommRingCat.hom_ext_iff] using toOpen_comp_comap f _

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Domain.lean
@[simp]
lemma natDegree_pow (p : R[X]) (n : ℕ) : natDegree (p ^ n) = n * natDegree p

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.leadingCoeff ^ n ≠ 0

Tactic:
rw [← leadingCoeff_pow, Ne, leadingCoeff_eq_zero]

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ¬p ^ n = 0

Proof state:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
n : ℕ
⊢ (0 ^ n).natDegree = n * natDegree 0

Tactic:
obtain rfl | hn := eq_or_ne n 0 <;> simp [*]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
obtain rfl | hp := eq_or_ne p 0

Result:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
n : ℕ
⊢ (0 ^ n).natDegree = n * natDegree 0

case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ (p ^ n).natDegree = n * p.natDegree

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
exact natDegree_pow' <| by
  rw [← leadingCoeff_pow, Ne, leadingCoeff_eq_zero]; exact pow_ne_zero _ hp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ¬p ^ n = 0

Tactic:
exact pow_ne_zero _ hp

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem mem_map {f : α → β} {b : β} {z : Sym2 α} : b ∈ Sym2.map f z ↔ ∃ a, a ∈ z ∧ f a = b

Proof state:
α : Type u_1
β : Type u_2
f : α → β
b : β
z : Sym2 α
⊢ b ∈ map f z ↔ ∃ a ∈ z, f a = b

Tactic:
induction' z with x y

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
b : β
x y : α
⊢ b ∈ map f s(x, y) ↔ ∃ a ∈ s(x, y), f a = b

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
b : β
x y : α
⊢ b = f x ∨ b = f y ↔ f x = b ∨ f y = b

Tactic:
aesop

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
b : β
x y : α
⊢ b ∈ map f s(x, y) ↔ ∃ a ∈ s(x, y), f a = b

Tactic:
simp only [map_pair_eq, mem_iff, exists_eq_or_imp, exists_eq_left]

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
b : β
x y : α
⊢ b = f x ∨ b = f y ↔ f x = b ∨ f y = b
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_le_rpow_of_exponent_ge (hx0 : 0 < x) (hx1 : x ≤ 1) (hyz : z ≤ y) : x ^ y ≤ x ^ z

Proof state:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ x ^ y ≤ x ^ z

Tactic:
repeat' rw [rpow_def_of_pos hx0]

Result:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ rexp (log x * y) ≤ rexp (log x * z)

Proof state:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ log x * y ≤ log x * z

Tactic:
exact mul_le_mul_of_nonpos_left hyz (log_nonpos (le_of_lt hx0) hx1)

Result:
no goals

Proof state:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ rexp (log x * y) ≤ x ^ z

Tactic:
rw [rpow_def_of_pos hx0]

Result:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ rexp (log x * y) ≤ rexp (log x * z)

Proof state:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ rexp (log x * y) ≤ rexp (log x * z)

Tactic:
rw [exp_le_exp]

Result:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ log x * y ≤ log x * z
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem forallLTEqZero_supp_BddBelow (f : Γ → R) (n : Γ) (hn : ∀(m : Γ), m < n → f m = 0) :
    BddBelow (Function.support f)

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
⊢ ∃ x, x ∈ {x | ∀ ⦃a : Γ⦄, a ∈ Function.support f → x ≤ a}

Tactic:
use n

Result:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
⊢ n ∈ {x | ∀ ⦃a : Γ⦄, a ∈ Function.support f → x ≤ a}

Proof state:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
m : Γ
hm : m ∈ Function.support f
⊢ n ≤ m

Tactic:
rw [Function.mem_support, ne_eq] at hm

Result:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
m : Γ
hm : ¬f m = 0
⊢ n ≤ m

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
⊢ BddBelow (Function.support f)

Tactic:
simp only [BddBelow, Set.Nonempty, lowerBounds]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
⊢ ∃ x, x ∈ {x | ∀ ⦃a : Γ⦄, a ∈ Function.support f → x ≤ a}

Proof state:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
m : Γ
hm : ¬f m = 0
⊢ n ≤ m

Tactic:
exact not_lt.mp (mt (hn m) hm)

Result:
no goals

Proof state:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
⊢ n ∈ {x | ∀ ⦃a : Γ⦄, a ∈ Function.support f → x ≤ a}

Tactic:
intro m hm

Result:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
m : Γ
hm : m ∈ Function.support f
⊢ n ≤ m
-- Mathlib/Data/Stream/Init.lean
theorem unfolds_eq (g : α → β) (f : α → α) (a : α) : unfolds g f a = g a :: unfolds g f (f a)

Proof state:
α : Type u
β : Type v
g : α → β
f : α → α
a : α
⊢ unfolds g f a = g a :: unfolds g f (f a)

Tactic:
unfold unfolds

Result:
α : Type u
β : Type v
g : α → β
f : α → α
a : α
⊢ corec g f a = g a :: corec g f (f a)

Proof state:
α : Type u
β : Type v
g : α → β
f : α → α
a : α
⊢ corec g f a = g a :: corec g f (f a)

Tactic:
rw [corec_eq]

Result:
no goals
-- Mathlib/Data/List/Perm/Basic.lean
lemma count_eq_count_filter_add [DecidableEq α] (P : α → Prop) [DecidablePred P]
    (l : List α) (a : α) :
    count a l = count a (l.filter P) + count a (l.filter (¬ P ·))

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
P : α → Prop
inst✝ : DecidablePred P
l : List α
a : α
⊢ count a l = count a (filter (fun b => decide (P b)) l) + count a (filter (fun x => decide ¬P x) l)

Tactic:
convert countP_eq_countP_filter_add l _ P

Result:
case h.e'_3.h.e'_6.h.e'_1.h.e'_2.h
α : Type u_1
inst✝¹ : DecidableEq α
P : α → Prop
inst✝ : DecidablePred P
l : List α
a x✝ : α
⊢ (decide ¬P x✝) = !decide (P x✝)

Proof state:
case h.e'_3.h.e'_6.h.e'_1.h.e'_2.h
α : Type u_1
inst✝¹ : DecidableEq α
P : α → Prop
inst✝ : DecidablePred P
l : List α
a x✝ : α
⊢ (decide ¬P x✝) = !decide (P x✝)

Tactic:
simp only [decide_not]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem some_getElem_eq_getElem?_iff (a : Vector α n) (i : Nat) (h : i < n) :
    (some a[i] = a[i]?) ↔ True

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
h : i < n
⊢ some a[i] = a[i]? ↔ True

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_Prop {β} [CommMonoid β] (f : Prop → β) :
    ∏ p, f p = f True * f False

Proof state:
β : Type u_9
inst✝ : CommMonoid β
f : Prop → β
⊢ ∏ p : Prop, f p = f True * f False

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/QExpansion.lean
lemma qExpansion_coeff (m : ℕ) :
    (qExpansion n f).coeff ℂ m = (↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction n f) 0

Proof state:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
n : ℕ
f : F
m : ℕ
⊢ (PowerSeries.coeff ℂ m) (qExpansion n f) = (↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction n f) 0

Tactic:
simp [qExpansion]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attachWith_map_subtype_val {p : α → Prop} (l : Vector α n) (H : ∀ a ∈ l, p a) :
    (l.attachWith p H).map Subtype.val = l

Proof state:
α : Type u_1
n : Nat
p : α → Prop
l : Vector α n
H : ∀ (a : α), a ∈ l → p a
⊢ map Subtype.val (l.attachWith p H) = l

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
p : α → Prop
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ map Subtype.val ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith p H) =
    { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Prop
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ map Subtype.val ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith p H) =
    { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem ExprCnstr.eq_false_of_isUnsat (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isUnsat) : c.denote ctx = False

Proof state:
ctx : Context
c : ExprCnstr
h : c.toNormPoly.isUnsat = true
this : PolyCnstr.denote ctx c.toNormPoly = False
⊢ denote ctx c = False

Tactic:
simp [-eq_iff_iff] at this

Result:
ctx : Context
c : ExprCnstr
h : c.toNormPoly.isUnsat = true
this : denote ctx c = False
⊢ denote ctx c = False

Proof state:
ctx : Context
c : ExprCnstr
h : c.toNormPoly.isUnsat = true
⊢ denote ctx c = False

Tactic:
have := PolyCnstr.eq_false_of_isUnsat ctx h

Result:
ctx : Context
c : ExprCnstr
h : c.toNormPoly.isUnsat = true
this : PolyCnstr.denote ctx c.toNormPoly = False
⊢ denote ctx c = False

Proof state:
ctx : Context
c : ExprCnstr
h : c.toNormPoly.isUnsat = true
this : denote ctx c = False
⊢ denote ctx c = False

Tactic:
assumption

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_true_or_eq_false_self : ∀(b : Bool), (b = true ∨ b = false) ↔ True

Proof state:
⊢ ∀ (b : Bool), b = true ∨ b = false ↔ True

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem univ_pow [Fintype α] (hn : n ≠ 0) : (univ : Finset α) ^ n = univ :=
  coe_injective <| by rw [coe_pow, coe_univ, Set.univ_pow hn]

Proof state:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid α
n : ℕ
inst✝ : Fintype α
hn : n ≠ 0
⊢ ↑(univ ^ n) = ↑univ

Tactic:
rw [coe_pow, coe_univ, Set.univ_pow hn]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
@[simp] lemma coprime_two_left : Coprime 2 n ↔ Odd n

Proof state:
n : ℕ
⊢ Coprime 2 n ↔ Odd n

Tactic:
rw [prime_two.coprime_iff_not_dvd, ← not_even_iff_odd, even_iff_two_dvd]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem neighborSet_iSup (f : ι → G.Subgraph) (v : V) :
    (⨆ i, f i).neighborSet v = ⋃ i, (f i).neighborSet v

Proof state:
ι : Sort u_1
V : Type u
G : SimpleGraph V
f : ι → G.Subgraph
v : V
⊢ (⨆ i, f i).neighborSet v = ⋃ i, (f i).neighborSet v

Tactic:
simp [iSup]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Basic.lean
theorem cast_lt_one : (n : α) < 1 ↔ n = 0

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑n < 1 ↔ n = 0

Tactic:
rw [← cast_one, cast_lt, Nat.lt_succ_iff, le_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem insertEntry_of_perm [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k}
    (hl : DistinctKeys l) (h : Perm l l') : Perm (insertEntry k v l) (insertEntry k v l')

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l l' : List ((a : α) × β a)
k : α
v : β k
hl : DistinctKeys l
h : l.Perm l'
⊢ (insertEntry k v l).Perm (insertEntry k v l')

Tactic:
apply getEntry?_ext hl.insertEntry (hl.perm h.symm).insertEntry

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l l' : List ((a : α) × β a)
k : α
v : β k
hl : DistinctKeys l
h : l.Perm l'
⊢ ∀ (a : α), getEntry? a (insertEntry k v l) = getEntry? a (insertEntry k v l')

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l l' : List ((a : α) × β a)
k : α
v : β k
hl : DistinctKeys l
h : l.Perm l'
⊢ ∀ (a : α), getEntry? a (insertEntry k v l) = getEntry? a (insertEntry k v l')

Tactic:
simp [getEntry?_insertEntry, getEntry?_of_perm hl h]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem triangle_assoc_comp_left_inv (f : a ⟶ b) (g : b ⟶ c) :
    f ◁ (λ_ g).inv ≫ (α_ f (𝟙 b) g).inv = (ρ_ f).inv ▷ g

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (λ_ g).inv ≫ (α_ f (𝟙 b) g).inv = (ρ_ f).inv ▷ g

Tactic:
simp [← cancel_mono ((ρ_ f).hom ▷ g)]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem equiv_apply : b.equiv b' e (b i) = b' (e i)

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
i : ι
b' : Basis ι' R M'
e : ι ≃ ι'
⊢ (b.equiv b' e) (b i) = b' (e i)

Tactic:
simp [Basis.equiv]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem moveRight_neg_symm {x : PGame} (i) :
    x.moveRight (toLeftMovesNeg.symm i) = -(-x).moveLeft i

Proof state:
x : PGame
i : (-x).LeftMoves
⊢ x.moveRight (toLeftMovesNeg.symm i) = -(-x).moveLeft i

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Prod.lean
@[simp]
lemma swap_prod {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel α γ} [IsSFiniteKernel η] :
    (swap β γ) ∘ₖ (κ ×ₖ η) = (η ×ₖ κ)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
⊢ swap β γ ∘ₖ (κ ×ₖ η) = η ×ₖ κ

Tactic:
rw [swap_comp_eq_map, map_prod_swap]

Result:
no goals
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
theorem toDualRight_symm_comp_toDualLeft :
    p.toDualRight.symm.dualMap ∘ₗ (p.toDualLeft : M →ₗ[R] Dual R N) = Dual.eval R M

Proof state:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
x : M
⊢ (↑p.toDualRight.symm.dualMap ∘ₗ ↑p.toDualLeft) x = (Dual.eval R M) x

Tactic:
exact p.toDualRight_symm_toDualLeft x

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
⊢ ↑p.toDualRight.symm.dualMap ∘ₗ ↑p.toDualLeft = Dual.eval R M

Tactic:
ext1 x

Result:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
x : M
⊢ (↑p.toDualRight.symm.dualMap ∘ₗ ↑p.toDualLeft) x = (Dual.eval R M) x
-- Mathlib/Probability/Distributions/Gaussian.lean
lemma gaussianReal_absolutelyContinuous (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) :
    gaussianReal μ v ≪ volume

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ gaussianReal μ v ≪ ℙ

Tactic:
rw [gaussianReal_of_var_ne_zero _ hv]

Result:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ℙ.withDensity (gaussianPDF μ v) ≪ ℙ

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ℙ.withDensity (gaussianPDF μ v) ≪ ℙ

Tactic:
exact withDensity_absolutelyContinuous _ _

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem sizeUpTo_ofLength_le (i : ℕ) (h : c.length ≤ i) : c.sizeUpTo i = n

Proof state:
n : ℕ
c : Composition n
i : ℕ
h : c.length ≤ i
⊢ (take i c.blocks).sum = n

Tactic:
convert c.blocks_sum

Result:
case h.e'_2.h.e'_4
n : ℕ
c : Composition n
i : ℕ
h : c.length ≤ i
⊢ take i c.blocks = c.blocks

Proof state:
n : ℕ
c : Composition n
i : ℕ
h : c.length ≤ i
⊢ c.sizeUpTo i = n

Tactic:
dsimp [sizeUpTo]

Result:
n : ℕ
c : Composition n
i : ℕ
h : c.length ≤ i
⊢ (take i c.blocks).sum = n

Proof state:
case h.e'_2.h.e'_4
n : ℕ
c : Composition n
i : ℕ
h : c.length ≤ i
⊢ take i c.blocks = c.blocks

Tactic:
exact take_of_length_le h

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
@[simp]
lemma Scheme.Opens.toSpecΓ_top {X : Scheme} :
    (⊤ : X.Opens).toSpecΓ = (⊤ : X.Opens).ι ≫ X.toSpecΓ

Proof state:
X : Scheme
⊢ (↑⊤).toSpecΓ ≫ Spec.map (X.presheaf.map (eqToHom ⋯)) = (↑⊤).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op)

Tactic:
rfl

Result:
no goals

Proof state:
X : Scheme
⊢ ⊤.toSpecΓ = ⊤.ι ≫ X.toSpecΓ

Tactic:
simp [Scheme.Opens.toSpecΓ, toSpecΓ_naturality]

Result:
X : Scheme
⊢ (↑⊤).toSpecΓ ≫ Spec.map (X.presheaf.map (eqToHom ⋯)) = (↑⊤).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op)