harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/DFinsupp/Defs.lean
theorem extendWith_single_zero [DecidableEq ι] [∀ i, Zero (α i)] (i : ι) (x : α (some i)) :
    (single i x).extendWith 0 = single (some i) x

Proof state:
case h.none
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
⊢ (extendWith 0 (single i x)) none = (single (some i) x) none

Tactic:
rw [extendWith_none, single_eq_of_ne (Option.some_ne_none _)]

Result:
no goals

Proof state:
case h.some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
⊢ (extendWith 0 (single i x)) (some j) = (single (some i) x) (some j)

Tactic:
rw [extendWith_some]

Result:
case h.some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
⊢ (single i x) j = (single (some i) x) (some j)

Proof state:
case h.some.inl
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
⊢ (single i x) i = (single (some i) x) (some i)

Tactic:
rw [single_eq_same, single_eq_same]

Result:
no goals

Proof state:
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
⊢ extendWith 0 (single i x) = single (some i) x

Tactic:
ext (_ | j)

Result:
case h.none
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
⊢ (extendWith 0 (single i x)) none = (single (some i) x) none

case h.some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
⊢ (extendWith 0 (single i x)) (some j) = (single (some i) x) (some j)

Proof state:
case h.some.inr
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
hij : i ≠ j
⊢ (single i x) j = (single (some i) x) (some j)

Tactic:
rw [single_eq_of_ne hij, single_eq_of_ne ((Option.some_injective _).ne hij)]

Result:
no goals

Proof state:
case h.some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
⊢ (single i x) j = (single (some i) x) (some j)

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Result:
case h.some.inl
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
⊢ (single i x) i = (single (some i) x) (some i)

case h.some.inr
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
hij : i ≠ j
⊢ (single i x) j = (single (some i) x) (some j)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁} :
    get (m.insertIfNew k v) a h₁ =
      if h₂ : k == a ∧ ¬k ∈ m then v
      else get m a (mem_of_mem_insertIfNew' h h₁ h₂)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β
h₁ : a ∈ m.insertIfNew k v
⊢ get (m.insertIfNew k v) a h₁ = if h : (k == a) = true ∧ m.contains k = false then v else get m a ⋯

Tactic:
simp_to_raw using Raw₀.Const.get_insertIfNew ⟨m, _⟩

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β
h₁ : a ∈ m.insertIfNew k v
⊢ get (m.insertIfNew k v) a h₁ = if h₂ : (k == a) = true ∧ ¬k ∈ m then v else get m a ⋯

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β
h₁ : a ∈ m.insertIfNew k v
⊢ get (m.insertIfNew k v) a h₁ = if h : (k == a) = true ∧ m.contains k = false then v else get m a ⋯
-- Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean
lemma dualSubmodule_dualSubmodule_flip_of_basis {ι : Type*} [Finite ι]
    (hB : B.Nondegenerate) (b : Basis ι S M) :
    B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range b))) =
      Submodule.span R (Set.range b)

Proof state:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
⊢ B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
classical
letI := FiniteDimensional.of_fintype_basis b
rw [dualSubmodule_span_of_basis _ hB.flip, dualSubmodule_span_of_basis B hB,
  dualBasis_dualBasis_flip B hB]

Result:
no goals

Proof state:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
⊢ B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
letI := FiniteDimensional.of_fintype_basis b

Result:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := FiniteDimensional.of_fintype_basis b
⊢ B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Proof state:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := FiniteDimensional.of_fintype_basis b
⊢ B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
rw [dualSubmodule_span_of_basis _ hB.flip, dualSubmodule_span_of_basis B hB,
  dualBasis_dualBasis_flip B hB]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem apply_zero {P Q : C} (f : P ⟶ Q) : f 0 = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ pseudoApply f 0 = 0

Tactic:
rw [pseudoZero_def, pseudoApply_mk']

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ ⟦Over.mk ((Over.mk 0).hom ≫ f)⟧ = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ ⟦Over.mk ((Over.mk 0).hom ≫ f)⟧ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma PosSMulReflectLE.lift [PosSMulReflectLE α γ]
    (hf : ∀ {b₁ b₂}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂)
    (smul : ∀ (a : α) b, f (a • b) = a • f b) : PosSMulReflectLE α β where
  elim a ha b₁ b₂ h := hf.1 <| le_of_smul_le_smul_left (by simpa only [smul] using hf.2 h) ha

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 < a
b₁ b₂ : β
h : a • b₁ ≤ a • b₂
⊢ a • f b₁ ≤ a • f b₂

Tactic:
simpa only [smul] using hf.2 h

Result:
no goals
-- Mathlib/Data/List/Dedup.lean
theorem headI_dedup [Inhabited α] (l : List α) :
    l.dedup.headI = if l.headI ∈ l.tail then l.tail.dedup.headI else l.headI :=
  match l with
  | [] => rfl
  | a :: l => by by_cases ha : a ∈ l <;> simp [ha, List.dedup_cons_of_mem]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI

Tactic:
by_cases ha : a ∈ l <;> simp [ha, List.dedup_cons_of_mem]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma ceilRoot_zero_left (a : ℕ) : ceilRoot 0 a = 0

Proof state:
a : ℕ
⊢ ceilRoot 0 a = 0

Tactic:
simp [ceilRoot]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_iff_isZero_homology [S.HasHomology] :
    S.Exact ↔ IsZero S.homology

Proof state:
case mp.mk.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h' : S.HomologyData
z : IsZero h'.left.H
⊢ IsZero S.homology

Tactic:
exact IsZero.of_iso z h'.left.homologyIso

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.Exact ↔ IsZero S.homology

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.Exact → IsZero S.homology

case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ IsZero S.homology → S.Exact

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ IsZero S.homology → S.Exact

Tactic:
intro h

Result:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : IsZero S.homology
⊢ S.Exact

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : IsZero S.homology
⊢ S.Exact

Tactic:
exact ⟨⟨_, h⟩⟩

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.Exact → IsZero S.homology

Tactic:
rintro ⟨⟨h', z⟩⟩

Result:
case mp.mk.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h' : S.HomologyData
z : IsZero h'.left.H
⊢ IsZero S.homology
-- Mathlib/CategoryTheory/Functor/ReflectsIso.lean
lemma reflectsIsomorphisms_of_comp (F : C ⥤ D) (G : D ⥤ E)
    [(F ⋙ G).ReflectsIsomorphisms] : F.ReflectsIsomorphisms where
  reflects f _

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : (F ⋙ G).ReflectsIsomorphisms
A✝ B✝ : C
f : A✝ ⟶ B✝
x✝ : IsIso (F.map f)
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso _ (F ⋙ G)]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : (F ⋙ G).ReflectsIsomorphisms
A✝ B✝ : C
f : A✝ ⟶ B✝
x✝ : IsIso (F.map f)
⊢ IsIso ((F ⋙ G).map f)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : (F ⋙ G).ReflectsIsomorphisms
A✝ B✝ : C
f : A✝ ⟶ B✝
x✝ : IsIso (F.map f)
⊢ IsIso (G.map (F.map f))

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : (F ⋙ G).ReflectsIsomorphisms
A✝ B✝ : C
f : A✝ ⟶ B✝
x✝ : IsIso (F.map f)
⊢ IsIso ((F ⋙ G).map f)

Tactic:
dsimp

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : (F ⋙ G).ReflectsIsomorphisms
A✝ B✝ : C
f : A✝ ⟶ B✝
x✝ : IsIso (F.map f)
⊢ IsIso (G.map (F.map f))
-- Mathlib/Data/List/Rotate.lean
theorem isRotated_singleton_iff {x : α} : l ~r [x] ↔ l = [x] :=
  ⟨fun ⟨n, hn⟩ => by simpa using hn, fun h => h ▸ by rfl⟩

Proof state:
α : Type u
l : List α
x : α
h : l = [x]
⊢ l ~r l

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
x✝ : l ~r [x]
n : ℕ
hn : l.rotate n = [x]
⊢ l = [x]

Tactic:
simpa using hn

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Permanent.lean
theorem permanent_smul (M : Matrix n n R) (c : R) :
    permanent (c • M) = c ^ Fintype.card n * permanent M

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
⊢ (c • M).permanent = c ^ Fintype.card n * M.permanent

Tactic:
simp only [permanent, smul_apply, smul_eq_mul, Finset.mul_sum]

Result:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
⊢ ∑ x : Perm n, ∏ x_1 : n, c * M (x x_1) x_1 = ∑ i : Perm n, c ^ Fintype.card n * ∏ i_1 : n, M (i i_1) i_1

Proof state:
case e_f.h
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
⊢ ∏ x : n, M (x✝ x) x * c = (∏ i : n, M (x✝ i) i) * c ^ Fintype.card n

Tactic:
exact prod_mul_pow_card.symm

Result:
no goals

Proof state:
case e_f.h
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
⊢ ∏ x : n, c * M (x✝ x) x = c ^ Fintype.card n * ∏ i : n, M (x✝ i) i

Tactic:
rw [mul_comm]

Result:
case e_f.h
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
⊢ ∏ x : n, c * M (x✝ x) x = (∏ i : n, M (x✝ i) i) * c ^ Fintype.card n

Proof state:
case e_f.h
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
⊢ ∏ x : n, c * M (x✝ x) x = (∏ i : n, M (x✝ i) i) * c ^ Fintype.card n

Tactic:
conv in ∏ _ , c * _ => simp [mul_comm c];

Result:
case e_f.h
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
⊢ ∏ x : n, M (x✝ x) x * c = (∏ i : n, M (x✝ i) i) * c ^ Fintype.card n

Proof state:
case e_f
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
⊢ (fun x => ∏ x_1 : n, c * M (x x_1) x_1) = fun i => c ^ Fintype.card n * ∏ i_1 : n, M (i i_1) i_1

Tactic:
ext

Result:
case e_f.h
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
⊢ ∏ x : n, c * M (x✝ x) x = c ^ Fintype.card n * ∏ i : n, M (x✝ i) i

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
⊢ ∑ x : Perm n, ∏ x_1 : n, c * M (x x_1) x_1 = ∑ i : Perm n, c ^ Fintype.card n * ∏ i_1 : n, M (i i_1) i_1

Tactic:
congr

Result:
case e_f
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
⊢ (fun x => ∏ x_1 : n, c * M (x x_1) x_1) = fun i => c ^ Fintype.card n * ∏ i_1 : n, M (i i_1) i_1
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem iUnion_eq_empty : π₁.iUnion = ∅ ↔ π₁ = ⊥

Proof state:
ι : Type u_1
I : Box ι
π₁ : Prepartition I
⊢ π₁.iUnion = ∅ ↔ π₁ = ⊥

Tactic:
simp [← injective_boxes.eq_iff, Finset.ext_iff, Prepartition.iUnion, imp_false]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_append (l₁ l₂ : List α) :
    (l₁ ++ l₂).eraseP p = if l₁.any p then l₁.eraseP p ++ l₂ else l₁ ++ l₂.eraseP p

Proof state:
case isTrue
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁.any p = true
⊢ eraseP p (l₁ ++ l₂) = eraseP p l₁ ++ l₂

Tactic:
simp only [any_eq_true] at h

Result:
case isTrue
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : ∃ x, x ∈ l₁ ∧ p x = true
⊢ eraseP p (l₁ ++ l₂) = eraseP p l₁ ++ l₂

Proof state:
case isFalse
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : ¬∃ x, x ∈ l₁ ∧ p x = true
⊢ eraseP p (l₁ ++ l₂) = l₁ ++ eraseP p l₂

Tactic:
rw [eraseP_append_right _]

Result:
case isFalse
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : ¬∃ x, x ∈ l₁ ∧ p x = true
⊢ ∀ (b : α), b ∈ l₁ → ¬p b = true

Proof state:
case isTrue.intro.intro
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x : α
m : x ∈ l₁
h : p x = true
⊢ eraseP p (l₁ ++ l₂) = eraseP p l₁ ++ l₂

Tactic:
rw [eraseP_append_left h _ m]

Result:
no goals

Proof state:
case isFalse
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : ¬l₁.any p = true
⊢ eraseP p (l₁ ++ l₂) = l₁ ++ eraseP p l₂

Tactic:
simp only [any_eq_true] at h

Result:
case isFalse
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : ¬∃ x, x ∈ l₁ ∧ p x = true
⊢ eraseP p (l₁ ++ l₂) = l₁ ++ eraseP p l₂

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ eraseP p (l₁ ++ l₂) = if l₁.any p = true then eraseP p l₁ ++ l₂ else l₁ ++ eraseP p l₂

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁.any p = true
⊢ eraseP p (l₁ ++ l₂) = eraseP p l₁ ++ l₂

case isFalse
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : ¬l₁.any p = true
⊢ eraseP p (l₁ ++ l₂) = l₁ ++ eraseP p l₂

Proof state:
case isFalse
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : ¬∃ x, x ∈ l₁ ∧ p x = true
⊢ ∀ (b : α), b ∈ l₁ → ¬p b = true

Tactic:
simp_all

Result:
no goals

Proof state:
case isTrue
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : ∃ x, x ∈ l₁ ∧ p x = true
⊢ eraseP p (l₁ ++ l₂) = eraseP p l₁ ++ l₂

Tactic:
obtain ⟨x, m, h⟩ := h

Result:
case isTrue.intro.intro
α : Type u_1
p : α → Bool
l₁ l₂ : List α
x : α
m : x ∈ l₁
h : p x = true
⊢ eraseP p (l₁ ++ l₂) = eraseP p l₁ ++ l₂
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem norm_coe_le_norm (x : α) : ‖f x‖ ≤ ‖f‖ :=
  calc
    ‖f x‖ = dist (f x) ((0 : α →ᵇ β) x)

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
x : α
⊢ ‖f x‖ = dist (f x) (0 x)

Tactic:
simp [dist_zero_right]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem inclusion'_top_functor (X : TopCat) :
    (@Opens.isOpenEmbedding X ⊤).isOpenMap.functor = map (inclusionTopIso X).inv

Proof state:
case refine_1
X : TopCat
⊢ ∀ (X_1 : Opens ↑((toTopCat X).obj ⊤)), ⋯.functor.obj X_1 = (map (inclusionTopIso X).inv).obj X_1

Tactic:
intro U

Result:
case refine_1
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
⊢ ⋯.functor.obj U = (map (inclusionTopIso X).inv).obj U

Proof state:
case refine_1
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
⊢ ⋯.functor.obj U = (map (inclusionTopIso X).inv).obj U

Tactic:
ext x

Result:
case refine_1.h.h
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
x : ↑X
⊢ x ∈ ↑(⋯.functor.obj U) ↔ x ∈ ↑((map (inclusionTopIso X).inv).obj U)

Proof state:
case refine_1.h.h
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
x : ↑X
⊢ x ∈ ↑(⋯.functor.obj U) ↔ x ∈ ↑((map (inclusionTopIso X).inv).obj U)

Tactic:
exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨x, trivial⟩, h, rfl⟩⟩

Result:
no goals

Proof state:
X : TopCat
⊢ ⋯.functor = map (inclusionTopIso X).inv

Tactic:
refine CategoryTheory.Functor.ext ?_ ?_

Result:
case refine_1
X : TopCat
⊢ ∀ (X_1 : Opens ↑((toTopCat X).obj ⊤)), ⋯.functor.obj X_1 = (map (inclusionTopIso X).inv).obj X_1

case refine_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    ⋯.functor.map f = eqToHom ⋯ ≫ (map (inclusionTopIso X).inv).map f ≫ eqToHom ⋯

Proof state:
case refine_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    ⋯.functor.map f = eqToHom ⋯ ≫ (map (inclusionTopIso X).inv).map f ≫ eqToHom ⋯

Tactic:
subsingleton

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem isCoprime_tfae : TFAE [IsCoprime I J, Codisjoint I J, I + J = 1,
    ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤]

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ [IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J].TFAE

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ [IsCoprime I J, Codisjoint I J, I + J = 1, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE

Tactic:
rw [← isCoprime_iff_codisjoint, ← isCoprime_iff_add, ← isCoprime_iff_exists,
    ← isCoprime_iff_sup_eq]

Result:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ [IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J].TFAE
-- Mathlib/Data/Set/Image.lean
theorem range_inter_ssubset_iff_preimage_ssubset {f : α → β} {S S' : Set β} :
  range f ∩ S ⊂ range f ∩ S' ↔ f ⁻¹' S ⊂ f ⁻¹' S'

Proof state:
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
⊢ (range f ∩ S ⊆ range f ∩ S' ∧ ∃ x ∈ range f ∩ S', x ∉ range f ∩ S) ↔ f ⁻¹' S ⊆ f ⁻¹' S' ∧ ∃ x ∈ f ⁻¹' S', x ∉ f ⁻¹' S

Tactic:
apply and_congr ?_ (by aesop)

Result:
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
⊢ range f ∩ S ⊆ range f ∩ S' ↔ f ⁻¹' S ⊆ f ⁻¹' S'

Proof state:
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
⊢ range f ∩ S ⊂ range f ∩ S' ↔ f ⁻¹' S ⊂ f ⁻¹' S'

Tactic:
simp only [Set.ssubset_iff_exists]

Result:
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
⊢ (range f ∩ S ⊆ range f ∩ S' ∧ ∃ x ∈ range f ∩ S', x ∉ range f ∩ S) ↔ f ⁻¹' S ⊆ f ⁻¹' S' ∧ ∃ x ∈ f ⁻¹' S', x ∉ f ⁻¹' S

Proof state:
case mpr
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
r : f ⁻¹' S ⊆ f ⁻¹' S'
x : β
hx : x ∈ range f ∩ S
⊢ x ∈ range f ∩ S'

Tactic:
simp_all only [subset_inter_iff, inter_subset_left, true_and, mem_preimage,
  mem_inter_iff, mem_range, true_and]

Result:
case mpr
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
r : f ⁻¹' S ⊆ f ⁻¹' S'
x : β
hx : (∃ y, f y = x) ∧ x ∈ S
⊢ x ∈ S'

Proof state:
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
⊢ range f ∩ S ⊆ range f ∩ S' ↔ f ⁻¹' S ⊆ f ⁻¹' S'

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
⊢ range f ∩ S ⊆ range f ∩ S' → f ⁻¹' S ⊆ f ⁻¹' S'

case mpr
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
⊢ f ⁻¹' S ⊆ f ⁻¹' S' → range f ∩ S ⊆ range f ∩ S'

Proof state:
case mpr
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
r : f ⁻¹' S ⊆ f ⁻¹' S'
x : β
hx : (∃ y, f y = x) ∧ x ∈ S
⊢ x ∈ S'

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
⊢ (∃ x ∈ range f ∩ S', x ∉ range f ∩ S) ↔ ∃ x ∈ f ⁻¹' S', x ∉ f ⁻¹' S

Tactic:
aesop

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
⊢ range f ∩ S ⊆ range f ∩ S' → f ⁻¹' S ⊆ f ⁻¹' S'

case mpr
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
⊢ f ⁻¹' S ⊆ f ⁻¹' S' → range f ∩ S ⊆ range f ∩ S'

Tactic:
all_goals
  intro r x hx
  simp_all only [subset_inter_iff, inter_subset_left, true_and, mem_preimage,
    mem_inter_iff, mem_range, true_and]
  aesop

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
⊢ f ⁻¹' S ⊆ f ⁻¹' S' → range f ∩ S ⊆ range f ∩ S'

Tactic:
intro r x hx

Result:
case mpr
α : Type u_1
β : Type u_2
f : α → β
S S' : Set β
r : f ⁻¹' S ⊆ f ⁻¹' S'
x : β
hx : x ∈ range f ∩ S
⊢ x ∈ range f ∩ S'
-- Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean
lemma concaveOn_rpow {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) :
    ConcaveOn ℝ (Set.Ici 0) fun x : ℝ ↦ x ^ p

Proof state:
case inr.inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p

Tactic:
exact (strictConcaveOn_rpow hp₀ hp₁).concaveOn

Result:
no goals

Proof state:
case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p

Tactic:
rcases eq_or_lt_of_le hp₁ with (rfl | hp₁)

Result:
case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ 1

case inr.inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p

Proof state:
case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ 0

Tactic:
simpa only [rpow_zero] using concaveOn_const (c := 1) (convex_Ici _)

Result:
no goals

Proof state:
case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ 1

Tactic:
simpa only [rpow_one] using concaveOn_id (convex_Ici _)

Result:
no goals

Proof state:
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p

Tactic:
rcases eq_or_lt_of_le hp₀ with (rfl | hp₀)

Result:
case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ 0

case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p