harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma inl_fst_assoc {K : CochainComplex C ℤ} {d e : ℤ} (γ : Cochain F K d) (he : 1 + d = e) :
    (inl φ).comp ((fst φ).1.comp γ he) (by rw [← he, neg_add_cancel_left]) = γ

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
⊢ -1 + 1 + d = d

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
⊢ (inl φ).comp ((↑(fst φ)).comp γ he) ⋯ = γ

Tactic:
rw [← Cochain.comp_assoc _ _ _ (neg_add_cancel 1) (by omega) (by omega), inl_fst,
  Cochain.id_comp]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.42580, u_1} C
inst✝³ : Category.{?u.42584, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
⊢ -1 + e = d

Tactic:
rw [← he, neg_add_cancel_left]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
⊢ 1 + d = e

Tactic:
omega

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem support_ne_nil {u v : V} (p : G.Walk u v) : p.support ≠ []

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support ≠ []

Tactic:
cases p <;> simp

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
lemma ExpChar.exists [Ring R] [IsDomain R] : ∃ q, ExpChar R q

Proof state:
case inl
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
h✝ : CharZero R
⊢ ∃ q, ExpChar R q

case inr.intro.intro.mk
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
p : ℕ
right✝ : CharP R p
hp : Nat.Prime p
⊢ ∃ q, ExpChar R q

Tactic:
exacts [⟨1, .zero⟩, ⟨p, .prime hp⟩]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
⊢ ∃ q, ExpChar R q

Tactic:
obtain _ | ⟨p, ⟨hp⟩, _⟩ := CharP.exists' R

Result:
case inl
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
h✝ : CharZero R
⊢ ∃ q, ExpChar R q

case inr.intro.intro.mk
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
p : ℕ
right✝ : CharP R p
hp : Nat.Prime p
⊢ ∃ q, ExpChar R q
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
protected lemma neg_iff {f : ℝ → ℝ} : GrowsPolynomially f ↔ GrowsPolynomially (-f) :=
  ⟨fun hf => hf.neg, fun hf => by rw [← neg_neg f]; exact hf.neg⟩

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially (-f)
⊢ GrowsPolynomially (- -f)

Tactic:
exact hf.neg

Result:
no goals

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially (-f)
⊢ GrowsPolynomially f

Tactic:
rw [← neg_neg f]

Result:
f : ℝ → ℝ
hf : GrowsPolynomially (-f)
⊢ GrowsPolynomially (- -f)
-- Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
lemma boundary_disjointUnion : ModelWithCorners.boundary (I := I) (M ⊕ M') =
      Sum.inl '' (ModelWithCorners.boundary (I := I) M)
      ∪ Sum.inr '' (ModelWithCorners.boundary (I := I) M')

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
⊢ ModelWithCorners.boundary (M ⊕ M') = Sum.inl '' ModelWithCorners.boundary M ∪ Sum.inr '' ModelWithCorners.boundary M'

Tactic:
simp only [← ModelWithCorners.compl_interior, interior_disjointUnion, inl_compl_union_inr_compl]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
@[simp]
lemma LSeries_zero : LSeries 0 = 0

Proof state:
⊢ LSeries 0 = 0

Tactic:
ext

Result:
case h
x✝ : ℂ
⊢ LSeries 0 x✝ = 0 x✝

Proof state:
case h
x✝ : ℂ
⊢ LSeries 0 x✝ = 0 x✝

Tactic:
simp [LSeries, LSeries.term]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
theorem associator_hom_snd_snd (X Y Z : C) :
    (α_ X Y Z).hom ≫ prod.snd ≫ prod.snd = prod.snd

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y Z : C
⊢ (α_ X Y Z).hom ≫ prod.snd ≫ prod.snd = prod.snd

Tactic:
simp [associator_hom]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem iInf_adj_of_nonempty [Nonempty ι] {f : ι → SimpleGraph V} :
    (⨅ i, f i).Adj a b ↔ ∀ i, (f i).Adj a b

Proof state:
ι : Sort u_1
V : Type u
a b : V
inst✝ : Nonempty ι
f : ι → SimpleGraph V
⊢ (⨅ i, f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b

Tactic:
rw [iInf, sInf_adj_of_nonempty (Set.range_nonempty _), Set.forall_mem_range]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem comp_mul_left_iff {c : ℝ} (hc : c ≠ 0) :
    IntervalIntegrable (fun x ↦ f (c * x)) volume (a / c) (b / c) ↔
      IntervalIntegrable f volume a b :=
  ⟨fun h ↦ by simpa [hc] using h.comp_mul_left c⁻¹, (comp_mul_left · c)⟩

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b c : ℝ
hc : c ≠ 0
h : IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)
⊢ IntervalIntegrable f volume a b

Tactic:
simpa [hc] using h.comp_mul_left c⁻¹

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem add_iff_left :
    a₁ ≡ b₁ [PMOD p] → (a₁ + a₂ ≡ b₁ + b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p]) := fun ⟨m, hm⟩ =>
  (Equiv.addLeft m).symm.exists_congr_left.trans <| by simp [add_sub_add_comm, hm, add_smul, ModEq]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a₁ a₂ b₁ b₂ : α
x✝ : a₁ ≡ b₁ [PMOD p]
m : ℤ
hm : b₁ - a₁ = m • p
⊢ (∃ b, b₁ + b₂ - (a₁ + a₂) = (Equiv.symm (Equiv.addLeft m)).symm b • p) ↔ a₂ ≡ b₂ [PMOD p]

Tactic:
simp [add_sub_add_comm, hm, add_smul, ModEq]

Result:
no goals
-- Mathlib/GroupTheory/FiniteAbelian/Basic.lean
theorem equiv_prod_multiplicative_zmod_of_finite (G : Type*) [CommGroup G] [Finite G] :
    ∃ (ι : Type) (_ : Fintype ι) (n : ι → ℕ),
       (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Finite G
⊢ ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))

Tactic:
obtain ⟨ι, inst, n, h₁, h₂⟩ := AddCommGroup.equiv_directSum_zmod_of_finite' (Additive G)

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Finite G
ι : Type
inst : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (Additive G ≃+ ⨁ (i : ι), ZMod (n i))
⊢ ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Finite G
ι : Type
inst : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (Additive G ≃+ ⨁ (i : ι), ZMod (n i))
⊢ ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))

Tactic:
exact ⟨ι, inst, n, h₁, ⟨MulEquiv.toAdditive.symm <| h₂.some.trans <|
  (DirectSum.addEquivProd _).trans <| MulEquiv.toAdditive'' <| MulEquiv.piMultiplicative _⟩⟩

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma ofHom_v_comp_d (φ : F ⟶ G) (p q q' : ℤ) (hpq : p + 0 = q) :
    (ofHom φ).v p q hpq ≫ G.d q q' = φ.f p ≫ G.d p q'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
p q q' : ℤ
hpq : p + 0 = q
⊢ (ofHom φ).v p q hpq ≫ G.d q q' = φ.f p ≫ G.d p q'

Tactic:
simp only [ofHom, ofHoms_v_comp_d]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma toMvPolynomial_comp (g : M₂ →ₗ[R] M₃) (f : M₁ →ₗ[R] M₂) (i : ι₃) :
    (g ∘ₗ f).toMvPolynomial b₁ b₃ i =
      bind₁ (f.toMvPolynomial b₁ b₂) (g.toMvPolynomial b₂ b₃ i)

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
ι₁ : Type u_5
ι₂ : Type u_6
ι₃ : Type u_7
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Fintype ι₁
inst✝³ : Fintype ι₂
inst✝² : Finite ι₃
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
b₃ : Basis ι₃ R M₃
g : M₂ →ₗ[R] M₃
f : M₁ →ₗ[R] M₂
i : ι₃
⊢ (bind₁ ((toMatrix b₁ b₂) f).toMvPolynomial) (((toMatrix b₂ b₃) g).toMvPolynomial i) =
    (bind₁ (toMvPolynomial b₁ b₂ f)) (((toMatrix b₂ b₃) g).toMvPolynomial i)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
ι₁ : Type u_5
ι₂ : Type u_6
ι₃ : Type u_7
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Fintype ι₁
inst✝³ : Fintype ι₂
inst✝² : Finite ι₃
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
b₃ : Basis ι₃ R M₃
g : M₂ →ₗ[R] M₃
f : M₁ →ₗ[R] M₂
i : ι₃
⊢ toMvPolynomial b₁ b₃ (g ∘ₗ f) i = (bind₁ (toMvPolynomial b₁ b₂ f)) (toMvPolynomial b₂ b₃ g i)

Tactic:
simp only [toMvPolynomial, toMatrix_comp b₁ b₂ b₃, Matrix.toMvPolynomial_mul]

Result:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
ι₁ : Type u_5
ι₂ : Type u_6
ι₃ : Type u_7
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Fintype ι₁
inst✝³ : Fintype ι₂
inst✝² : Finite ι₃
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
b₃ : Basis ι₃ R M₃
g : M₂ →ₗ[R] M₃
f : M₁ →ₗ[R] M₂
i : ι₃
⊢ (bind₁ ((toMatrix b₁ b₂) f).toMvPolynomial) (((toMatrix b₂ b₃) g).toMvPolynomial i) =
    (bind₁ (toMvPolynomial b₁ b₂ f)) (((toMatrix b₂ b₃) g).toMvPolynomial i)
-- Mathlib/Probability/Martingale/Basic.lean
theorem martingale_const (ℱ : Filtration ι m0) (μ : Measure Ω) [IsFiniteMeasure μ] (x : E) :
    Martingale (fun _ _ => x) ℱ μ :=
  ⟨adapted_const ℱ _, fun i j _ => by rw [condExp_const (ℱ.le _)]⟩

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ℱ : Filtration ι m0
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
x : E
i j : ι
x✝ : i ≤ j
⊢ μ[(fun x_1 x_2 => x) j|↑ℱ i] =ᶠ[ae μ] (fun x_1 x_2 => x) i

Tactic:
rw [condExp_const (ℱ.le _)]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem left_ne_zero_of_oangle_sign_eq_neg_one {x y : V} (h : (o.oangle x y).sign = -1) : x ≠ 0 :=
  o.left_ne_zero_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0)

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = -1
⊢ -1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem filter_ne_eq_erase' (f : Π₀ i, β i) (i : ι) : f.filter (i ≠ ·) = f.erase i

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ filter (fun x => i ≠ x) f = filter (fun x => x ≠ i) f

Tactic:
congr with j

Result:
case e_p.h.a
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
⊢ i ≠ j ↔ j ≠ i

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ filter (fun x => i ≠ x) f = erase i f

Tactic:
rw [← filter_ne_eq_erase f i]

Result:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ filter (fun x => i ≠ x) f = filter (fun x => x ≠ i) f

Proof state:
case e_p.h.a
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
⊢ i ≠ j ↔ j ≠ i

Tactic:
exact ne_comm

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem partiallyWellOrderedOn_insert :
    PartiallyWellOrderedOn (insert a s) r ↔ PartiallyWellOrderedOn s r

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
a : α
inst✝ : IsRefl α r
⊢ (insert a s).PartiallyWellOrderedOn r ↔ s.PartiallyWellOrderedOn r

Tactic:
simp only [← singleton_union, partiallyWellOrderedOn_union,
  partiallyWellOrderedOn_singleton, true_and]

Result:
no goals
-- Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean
lemma isoClosure_le_iff [IsClosedUnderIsomorphisms Q] : isoClosure P ≤ Q ↔ P ≤ Q :=
  ⟨(le_isoClosure P).trans,
    fun h => (monotone_isoClosure h).trans (by rw [isoClosure_eq_self])⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P Q : ObjectProperty C
inst✝ : Q.IsClosedUnderIsomorphisms
h : P ≤ Q
⊢ Q.isoClosure ≤ Q

Tactic:
rw [isoClosure_eq_self]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Defs.lean
theorem eq_of_nndist_eq_zero {x y : γ} : nndist x y = 0 → x = y

Proof state:
γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ nndist x y = 0 → x = y

Tactic:
simp only [NNReal.eq_iff, ← dist_nndist, imp_self, NNReal.coe_zero, dist_eq_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem ext {f g : Lp E p μ} (h : f =ᵐ[μ] g) : f = g

Proof state:
case mk.mk
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
val✝¹ : α →ₘ[μ] E
property✝¹ : val✝¹ ∈ Lp E p μ
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p μ
h : ↑↑⟨val✝¹, property✝¹⟩ =ᶠ[ae μ] ↑↑⟨val✝, property✝⟩
⊢ ⟨val✝¹, property✝¹⟩ = ⟨val✝, property✝⟩

Tactic:
simp only [Subtype.mk_eq_mk]

Result:
case mk.mk
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
val✝¹ : α →ₘ[μ] E
property✝¹ : val✝¹ ∈ Lp E p μ
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p μ
h : ↑↑⟨val✝¹, property✝¹⟩ =ᶠ[ae μ] ↑↑⟨val✝, property✝⟩
⊢ val✝¹ = val✝

Proof state:
case mk
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
g : ↥(Lp E p μ)
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p μ
h : ↑↑⟨val✝, property✝⟩ =ᶠ[ae μ] ↑↑g
⊢ ⟨val✝, property✝⟩ = g

Tactic:
cases g

Result:
case mk.mk
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
val✝¹ : α →ₘ[μ] E
property✝¹ : val✝¹ ∈ Lp E p μ
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p μ
h : ↑↑⟨val✝¹, property✝¹⟩ =ᶠ[ae μ] ↑↑⟨val✝, property✝⟩
⊢ ⟨val✝¹, property✝¹⟩ = ⟨val✝, property✝⟩

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
h : ↑↑f =ᶠ[ae μ] ↑↑g
⊢ f = g

Tactic:
cases f

Result:
case mk
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
g : ↥(Lp E p μ)
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p μ
h : ↑↑⟨val✝, property✝⟩ =ᶠ[ae μ] ↑↑g
⊢ ⟨val✝, property✝⟩ = g

Proof state:
case mk.mk
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
val✝¹ : α →ₘ[μ] E
property✝¹ : val✝¹ ∈ Lp E p μ
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p μ
h : ↑↑⟨val✝¹, property✝¹⟩ =ᶠ[ae μ] ↑↑⟨val✝, property✝⟩
⊢ val✝¹ = val✝

Tactic:
exact AEEqFun.ext h

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean
theorem norm_eq (h : f 0 = 0) : ‖f‖ = ‖f.contLinear‖ :=
  calc
    ‖f‖ = max ‖f 0‖ ‖f.contLinear‖

Proof state:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedAddCommGroup W
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
f : V →ᴬ[𝕜] W
h : f 0 = 0
⊢ ‖f‖ = ‖f 0‖ ⊔ ‖f.contLinear‖

Tactic:
rw [norm_def]

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedAddCommGroup W
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
f : V →ᴬ[𝕜] W
h : f 0 = 0
⊢ ‖f 0‖ ⊔ ‖f.contLinear‖ = 0 ⊔ ‖f.contLinear‖

Tactic:
rw [h, norm_zero]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem Coprime.gcd_mul_left_cancel (m : Nat) (H : Coprime k n) : gcd (k * m) n = gcd m n :=
  have H1 : Coprime (gcd (k * m) n) k

Proof state:
k n m : Nat
H : k.Coprime n
⊢ ((k * m).gcd n).Coprime k

Tactic:
rw [Coprime, Nat.gcd_assoc, H.symm.gcd_eq_one, gcd_one_right]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal_one [DecidableEq m] [One α] : blockDiagonal (1 : o → Matrix m m α) = 1 :=
  show (blockDiagonal fun _ : o => diagonal fun _ : m => (1 : α)) = diagonal fun _ => 1 by
    rw [blockDiagonal_diagonal]

Proof state:
m : Type u_2
o : Type u_4
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : One α
⊢ (blockDiagonal fun x => diagonal fun x => 1) = diagonal fun x => 1

Tactic:
rw [blockDiagonal_diagonal]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_addY :
    (W'.map f).toAffine.addY (f x₁) (f x₂) (f y₁) (f ℓ) = f (W'.toAffine.addY x₁ x₂ y₁ ℓ)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x₁ y₁ x₂ ℓ : R
⊢ (map W' f).toAffine.addY (f x₁) (f x₂) (f y₁) (f ℓ) = f ((toAffine W').addY x₁ x₂ y₁ ℓ)

Tactic:
simp only [addY, map_negAddY, map_addX, map_negY]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem orElse_none' (x : Option α) : x.orElse (fun _ ↦ none) = x

Proof state:
α : Type u_1
x : Option α
⊢ (x.orElse fun x => none) = x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem Fin.conjTranspose_circulant [Star α] :
    ∀ {n} (v : Fin n → α), (circulant v)ᴴ = circulant (star fun i => v (-i))
  | 0 => by simp [Injective, eq_iff_true_of_subsingleton]
  | _ + 1 => Matrix.conjTranspose_circulant

Proof state:
α : Type u_1
inst✝ : Star α
⊢ ∀ (v : Fin 0 → α), (circulant v)ᴴ = circulant (star fun i => v (-i))

Tactic:
simp [Injective, eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
lemma disjiUnion_filter_eq_of_maps_to (h : ∀ x ∈ s, f x ∈ t) :
    t.disjiUnion (fun a ↦ s.filter (f · = a)) pairwiseDisjoint_fibers = s

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
h : ∀ x ∈ s, f x ∈ t
⊢ t.disjiUnion (fun a => filter (fun x => f x = a) s) ⋯ = s

Tactic:
simpa [filter_eq_self]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem X_pow_add_C_ne_zero {n : ℕ} (hn : 0 < n) (a : R) : (X : R[X]) ^ n + C a ≠ 0 :=
  mt degree_eq_bot.2
    (show degree ((X : R[X]) ^ n + C a) ≠ ⊥ by
      rw [degree_X_pow_add_C hn a]; exact WithBot.coe_ne_bot)

Proof state:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ ↑n ≠ ⊥

Tactic:
exact WithBot.coe_ne_bot

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ (X ^ n + C a).degree ≠ ⊥

Tactic:
rw [degree_X_pow_add_C hn a]

Result:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ ↑n ≠ ⊥
-- Mathlib/Logic/Relation.lean
lemma reflGen_minimal {r' : α → α → Prop} (hr' : Reflexive r') (h : ∀ x y, r x y → r' x y) {x y : α}
    (hxy : ReflGen r x y) : r' x y

Proof state:
α : Type u_1
r r' : α → α → Prop
hr' : Reflexive r'
h : ∀ (x y : α), r x y → r' x y
x y : α
hxy : ReflGen r x y
⊢ r' x y

Tactic:
simpa [reflGen_eq_self hr'] using ReflGen.mono h hxy

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem get?_take {s : Stream' α} : ∀ {k n}, k < n → (s.take n).get? k = s.get k
  | 0, _+1, _ => rfl
  | k+1, n+1, h => by rw [take_succ, List.get?, get?_take (Nat.lt_of_succ_lt_succ h), get_succ]

Proof state:
α : Type u
s : Stream' α
k n : ℕ
h : k + 1 < n + 1
⊢ (take (n + 1) s).get? (k + 1) = some (s.get (k + 1))

Tactic:
rw [take_succ, List.get?, get?_take (Nat.lt_of_succ_lt_succ h), get_succ]

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
lemma forall_mem_insertNone {s : Finset α} {p : Option α → Prop} :
    (∀ a ∈ insertNone s, p a) ↔ p none ∧ ∀ a ∈ s, p a

Proof state:
α : Type u_1
s : Finset α
p : Option α → Prop
⊢ (∀ a ∈ insertNone s, p a) ↔ p none ∧ ∀ a ∈ s, p (some a)

Tactic:
simp [Option.forall]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem BinaryCofan.isColimit_iff_isIso_inr {X Y : C} (h : IsInitial X) (c : BinaryCofan X Y) :
    Nonempty (IsColimit c) ↔ IsIso c.inr

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial X
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ IsIso c.inr

Tactic:
refine Iff.trans ?_ (BinaryCofan.isColimit_iff_isIso_inl h (BinaryCofan.mk c.inr c.inl))

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial X
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ Nonempty (IsColimit (mk c.inr c.inl))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial X
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ Nonempty (IsColimit (mk c.inr c.inl))

Tactic:
exact
  ⟨fun h => ⟨BinaryCofan.isColimitFlip h.some⟩, fun h =>
    ⟨(BinaryCofan.isColimitFlip h.some).ofIsoColimit (isoBinaryCofanMk c).symm⟩⟩

Result:
no goals
-- Mathlib/Probability/CondVar.lean
lemma condVar_of_not_sigmaFinite (hμm : ¬SigmaFinite (μ.trim hm)) :
    Var[X; μ | m] = 0

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
hm : m ≤ m₀
X : Ω → ℝ
μ : Measure Ω
hμm : ¬SigmaFinite (μ.trim hm)
⊢ Var[X; μ | m] = 0

Tactic:
rw [condVar, condExp_of_not_sigmaFinite hm hμm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem foldrM_attachWith [Monad m] [LawfulMonad m]
    (l : Vector α n) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x} → β → m β} {b} :
    (l.attachWith q H).foldrM f b = l.attach.foldrM (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Vector α n
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : { x // q x } → β → m β
b : β
⊢ foldrM f b (l.attachWith q H) = foldrM (fun a acc => f ⟨a.val, ⋯⟩ acc) b l.attach

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
q : α → Prop
f : { x // q x } → β → m β
b : β
l : Array α
H : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → q a
⊢ foldrM f b ({ toArray := l, size_toArray := ⋯ }.attachWith q H) =
    foldrM (fun a acc => f ⟨a.val, ⋯⟩ acc) b { toArray := l, size_toArray := ⋯ }.attach

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
q : α → Prop
f : { x // q x } → β → m β
b : β
l : Array α
H : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → q a
⊢ foldrM f b ({ toArray := l, size_toArray := ⋯ }.attachWith q H) =
    foldrM (fun a acc => f ⟨a.val, ⋯⟩ acc) b { toArray := l, size_toArray := ⋯ }.attach

Tactic:
simp [Array.foldrM_map]

Result:
no goals
-- Mathlib/Data/Finset/PImage.lean
theorem pimage_some (s : Finset α) (f : α → β) [∀ x, Decidable (Part.some <| f x).Dom] :
    (s.pimage fun x => Part.some (f x)) = s.image f

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → β
inst✝ : (x : α) → Decidable (Part.some (f x)).Dom
a✝ : β
⊢ a✝ ∈ pimage (fun x => Part.some (f x)) s ↔ a✝ ∈ image f s

Tactic:
simp [eq_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → β
inst✝ : (x : α) → Decidable (Part.some (f x)).Dom
⊢ pimage (fun x => Part.some (f x)) s = image f s

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → β
inst✝ : (x : α) → Decidable (Part.some (f x)).Dom
a✝ : β
⊢ a✝ ∈ pimage (fun x => Part.some (f x)) s ↔ a✝ ∈ image f s
-- Mathlib/MeasureTheory/Group/Action.lean
theorem measure_smul_eq_zero_iff {s} (c : G) : μ (c • s) = 0 ↔ μ s = 0

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
c : G
⊢ μ (c • s) = 0 ↔ μ s = 0

Tactic:
rw [measure_smul]

Result:
no goals
-- Mathlib/Order/BooleanSubalgebra.lean
lemma himp_mem (ha : a ∈ L) (hb : b ∈ L) : a ⇨ b ∈ L

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a ⇨ b ∈ L

Tactic:
simpa [himp_eq] using L.supClosed hb (compl_mem ha)

Result:
no goals