harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem mem_verts_toSubgraph (p : G.Walk u v) : w ∈ p.toSubgraph.verts ↔ w ∈ p.support

Proof state:
V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w = y ∨ w ∈ p'.support → w ∈ p'.support

Tactic:
rintro (rfl | h) <;> simp [*]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w ∈ p'.support → w = y ∨ w ∈ p'.support

Tactic:
simp (config := { contextual := true })

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.toSubgraph.verts ↔ w ∈ p.support

Tactic:
induction p with
| nil => simp
| cons h p' ih =>
  rename_i x y z
  have : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support :=
    ⟨by rintro (rfl | h) <;> simp [*], by simp (config := { contextual := true })⟩
  simp [ih, or_assoc, this]

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w ∈ (cons h p').toSubgraph.verts ↔ w ∈ (cons h p').support

Tactic:
rename_i x y z

Result:
case cons
V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w ∈ (cons h p').toSubgraph.verts ↔ w ∈ (cons h p').support

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
⊢ w ∈ nil.toSubgraph.verts ↔ w ∈ nil.support

Tactic:
simp

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
this : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support
⊢ w ∈ (cons h p').toSubgraph.verts ↔ w ∈ (cons h p').support

Tactic:
simp [ih, or_assoc, this]

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w ∈ (cons h p').toSubgraph.verts ↔ w ∈ (cons h p').support

Tactic:
have : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support :=
  ⟨by rintro (rfl | h) <;> simp [*], by simp (config := { contextual := true })⟩

Result:
case cons
V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
this : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support
⊢ w ∈ (cons h p').toSubgraph.verts ↔ w ∈ (cons h p').support
-- Mathlib/Data/Fintype/Inv.lean
theorem invFun_restrict [Nonempty α] : (Set.range f).restrict (invFun f) = f.invOfMemRange

Proof state:
case h.mk.a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α ↪ β
inst✝ : Nonempty α
b : β
h : b ∈ Set.range ⇑f
⊢ f ((Set.range ⇑f).restrict (invFun ⇑f) ⟨b, h⟩) = f (f.invOfMemRange ⟨b, h⟩)

Tactic:
simp [f.left_inv_of_invOfMemRange, @invFun_eq _ _ _ f b (Set.mem_range.mp h)]

Result:
no goals

Proof state:
case h.mk
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α ↪ β
inst✝ : Nonempty α
b : β
h : b ∈ Set.range ⇑f
⊢ (Set.range ⇑f).restrict (invFun ⇑f) ⟨b, h⟩ = f.invOfMemRange ⟨b, h⟩

Tactic:
apply f.injective

Result:
case h.mk.a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α ↪ β
inst✝ : Nonempty α
b : β
h : b ∈ Set.range ⇑f
⊢ f ((Set.range ⇑f).restrict (invFun ⇑f) ⟨b, h⟩) = f (f.invOfMemRange ⟨b, h⟩)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α ↪ β
inst✝ : Nonempty α
⊢ (Set.range ⇑f).restrict (invFun ⇑f) = f.invOfMemRange

Tactic:
ext ⟨b, h⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α ↪ β
inst✝ : Nonempty α
b : β
h : b ∈ Set.range ⇑f
⊢ (Set.range ⇑f).restrict (invFun ⇑f) ⟨b, h⟩ = f.invOfMemRange ⟨b, h⟩
-- Mathlib/Algebra/Star/Module.lean
theorem skewAdjointPart_comp_subtype_skewAdjoint :
    (skewAdjointPart R).comp (skewAdjoint.submodule R A).subtype = .id :=
  LinearMap.ext fun ⟨x, (hx : _ = _)⟩ ↦ Subtype.eq <| by
    simp only [LinearMap.comp_apply, Submodule.subtype_apply, skewAdjointPart_apply_coe, hx,
      sub_neg_eq_add, smul_add, invOf_two_smul_add_invOf_two_smul]; rfl

Proof state:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ ↑((skewAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype) ⟨x, hx⟩) = ↑(LinearMap.id ⟨x, hx⟩)

Tactic:
simp only [LinearMap.comp_apply, Submodule.subtype_apply, skewAdjointPart_apply_coe, hx,
  sub_neg_eq_add, smul_add, invOf_two_smul_add_invOf_two_smul]

Result:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ x = ↑(LinearMap.id ⟨x, hx⟩)

Proof state:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ x = ↑(LinearMap.id ⟨x, hx⟩)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem filter_eq_filterTR : @filter = @filterTR

Proof state:
case h

⊢ ∀ (x : Type u_1), filter = filterTR

Tactic:
intro α

Result:
case h
α : Type u_1
⊢ filter = filterTR

Proof state:
case h.h.h
α : Type u_1
p : α → Bool
as : List α
⊢ filter p as = filterTR p as

Tactic:
simp [filterTR, filterTR_loop_eq]

Result:
no goals

Proof state:
case h.h
α : Type u_1
⊢ ∀ (x : α → Bool), filter x = filterTR x

Tactic:
intro p

Result:
case h.h
α : Type u_1
p : α → Bool
⊢ filter p = filterTR p

Proof state:
case h.h.h
α : Type u_1
p : α → Bool
⊢ ∀ (x : List α), filter p x = filterTR p x

Tactic:
intro as

Result:
case h.h.h
α : Type u_1
p : α → Bool
as : List α
⊢ filter p as = filterTR p as

Proof state:
case h.h
α : Type u_1
p : α → Bool
⊢ filter p = filterTR p

Tactic:
apply funext

Result:
case h.h.h
α : Type u_1
p : α → Bool
⊢ ∀ (x : List α), filter p x = filterTR p x

Proof state:
case h
α : Type u_1
⊢ filter = filterTR

Tactic:
apply funext

Result:
case h.h
α : Type u_1
⊢ ∀ (x : α → Bool), filter x = filterTR x

Proof state:
⊢ @filter = @filterTR

Tactic:
apply funext

Result:
case h

⊢ ∀ (x : Type u_1), filter = filterTR
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_log_le_self (b : Ordinal) {x : Ordinal} (hx : x ≠ 0) : b ^ log b x ≤ x

Proof state:
b x : Ordinal.{u_1}
hx : x ≠ 0
⊢ b ^ log b x ≤ x

Tactic:
rcases eq_or_ne b 0 with (rfl | b0)

Result:
case inl
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ 0 ^ log 0 x ≤ x

case inr
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
⊢ b ^ log b x ≤ x

Proof state:
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
⊢ b ^ log b x ≤ x

Tactic:
refine le_of_not_lt fun h => (lt_succ (log b x)).not_le ?_

Result:
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
h : x < b ^ log b x
⊢ succ (log b x) ≤ log b x

Proof state:
case inl
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ 0 ^ log 0 x ≤ x

Tactic:
exact (zero_opow_le _).trans (one_le_iff_ne_zero.2 hx)

Result:
no goals

Proof state:
case inr.inr
x : Ordinal.{u_1}
hx : x ≠ 0
b0 : 1 ≠ 0
⊢ 1 ^ log 1 x ≤ x

Tactic:
rwa [one_opow, one_le_iff_ne_zero]

Result:
no goals

Proof state:
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
h : x < b ^ log b x
this : sInf {o | x < b ^ o} ≤ log b x
⊢ succ (log b x) ≤ log b x

Tactic:
rwa [← succ_log_def hb hx] at this

Result:
no goals

Proof state:
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
h : x < b ^ log b x
⊢ succ (log b x) ≤ log b x

Tactic:
have := @csInf_le' _ _ { o | x < b ^ o } _ h

Result:
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
h : x < b ^ log b x
this : sInf {o | x < b ^ o} ≤ log b x
⊢ succ (log b x) ≤ log b x

Proof state:
case inr
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
⊢ b ^ log b x ≤ x

Tactic:
rcases lt_or_eq_of_le (one_le_iff_ne_zero.2 b0) with (hb | rfl)

Result:
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
⊢ b ^ log b x ≤ x

case inr.inr
x : Ordinal.{u_1}
hx : x ≠ 0
b0 : 1 ≠ 0
⊢ 1 ^ log 1 x ≤ x
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_add_mul_self (x y : E) :
    ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2

Tactic:
exact norm_add_sq _ _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖

Tactic:
repeat' rw [← sq (M := ℝ)]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem Sum.one_le_dist_inr_inl {x : X} {y : Y} : 1 ≤ Sum.dist (.inr y) (.inl x)

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ Sum.dist (Sum.inl x) (Sum.inr y)

Tactic:
exact Sum.one_le_dist_inl_inr

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ Sum.dist (Sum.inr y) (Sum.inl x)

Tactic:
rw [Sum.dist_comm]

Result:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ Sum.dist (Sum.inl x) (Sum.inr y)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma nonsingular_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W'.Nonsingular P ↔ W'.Nonsingular Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.Nonsingular P ↔ W'.Nonsingular Q

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
W' : Jacobian R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Nonsingular ((fun m => m • Q) u) ↔ W'.Nonsingular Q

Proof state:
case intro
R : Type r
inst✝ : CommRing R
W' : Jacobian R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Nonsingular ((fun m => m • Q) u) ↔ W'.Nonsingular Q

Tactic:
exact nonsingular_smul Q u.isUnit

Result:
no goals
-- Mathlib/RingTheory/Localization/Integral.lean
theorem ideal_span_singleton_map_subset {L : Type*} [IsDomain R] [IsDomain S] [Field K] [Field L]
    [Algebra R K] [Algebra R L] [Algebra S L] [Algebra.IsAlgebraic R S] [IsFractionRing S L]
    [Algebra K L] [IsScalarTower R S L] [IsScalarTower R K L] {a : S} {b : Set S}
    (inj : Function.Injective (algebraMap R L))
    (h : (Ideal.span ({a} : Set S) : Set S) ⊆ Submodule.span R b) :
    (Ideal.span ({algebraMap S L a} : Set L) : Set L) ⊆ Submodule.span K (algebraMap S L '' b)

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ (algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
have mk_yz_eq : IsLocalization.mk' L y' z' = IsLocalization.mk' L y ⟨_, hz0'⟩ := by
  rw [Algebra.smul_def, mul_comm _ y, mul_comm _ y'] at yz_eq
  exact IsLocalization.mk'_eq_of_eq (by rw [mul_comm _ y, mul_comm _ y', yz_eq])

Result:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
⊢ (algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_rename [DecidableEq τ] (f : σ → τ) (φ : MvPolynomial σ R) :
    (rename f φ).vars ⊆ φ.vars.image f

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
⊢ ((rename f) φ).vars ⊆ Finset.image f φ.vars

Tactic:
intro i hi

Result:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ ((rename f) φ).vars
⊢ i ∈ Finset.image f φ.vars

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ ((rename f) φ).vars
⊢ i ∈ Finset.image f φ.vars

Tactic:
simp only [vars_def, exists_prop, Multiset.mem_toFinset, Finset.mem_image] at hi ⊢

Result:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ ((rename f) φ).degrees
⊢ ∃ a ∈ φ.degrees, f a = i

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ ((rename f) φ).degrees
⊢ ∃ a ∈ φ.degrees, f a = i

Tactic:
simpa only [Multiset.mem_map] using degrees_rename _ _ hi

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
⊢ ((rename f) φ).vars ⊆ Finset.image f φ.vars

Tactic:
classical
intro i hi
simp only [vars_def, exists_prop, Multiset.mem_toFinset, Finset.mem_image] at hi ⊢
simpa only [Multiset.mem_map] using degrees_rename _ _ hi

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
theorem biproduct.mapBiproduct_hom_desc (g : ∀ j, f j ⟶ W) :
    ((F.mapBiproduct f).hom ≫ biproduct.desc fun j => F.map (g j)) = F.map (biproduct.desc g)

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ ((F.mapBiproduct f).hom ≫ desc fun j => F.map (g j)) = F.map (desc g)

Tactic:
rw [← biproduct.mapBiproduct_inv_map_desc, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_symmDiff [DecidableEq α] (hs : s.Finite) (ht : t.Finite)
    (h : (s ∆ t).Finite) : h.toFinset = hs.toFinset ∆ ht.toFinset

Proof state:
case h
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∆ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset ∆ ht.toFinset

Tactic:
simp [mem_symmDiff, Finset.mem_symmDiff]

Result:
no goals

Proof state:
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∆ t).Finite
⊢ h.toFinset = hs.toFinset ∆ ht.toFinset

Tactic:
ext

Result:
case h
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∆ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset ∆ ht.toFinset
-- Mathlib/CategoryTheory/Sites/Grothendieck.lean
theorem arrow_intersect (f : Y ⟶ X) (S R : Sieve X) (hS : J.Covers S f) (hR : J.Covers R f) :
    J.Covers (S ⊓ R) f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
hS : J.Covers S f
hR : J.Covers R f
⊢ J.Covers (S ⊓ R) f

Tactic:
simpa [covers_iff] using And.intro hS hR

Result:
no goals
-- Mathlib/RingTheory/LocalRing/RingHom/Basic.lean
theorem of_surjective [CommSemiring R] [IsLocalRing R] [CommSemiring S] [Nontrivial S] (f : R →+* S)
    [IsLocalHom f] (hf : Function.Surjective f) : IsLocalRing S :=
  of_isUnit_or_isUnit_of_isUnit_add (by
    intro a b hab
    obtain ⟨a, rfl⟩ := hf a
    obtain ⟨b, rfl⟩ := hf b
    rw [← map_add] at hab
    exact
      (isUnit_or_isUnit_of_isUnit_add <| IsLocalHom.map_nonunit _ hab).imp f.isUnit_map
        f.isUnit_map)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
⊢ ∀ (a b : S), IsUnit (a + b) → IsUnit a ∨ IsUnit b

Tactic:
intro a b hab

Result:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
a b : S
hab : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
a b : R
hab : IsUnit (f a + f b)
⊢ IsUnit (f a) ∨ IsUnit (f b)

Tactic:
rw [← map_add] at hab

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
a b : R
hab : IsUnit (f (a + b))
⊢ IsUnit (f a) ∨ IsUnit (f b)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
a b : S
hab : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b

Tactic:
obtain ⟨a, rfl⟩ := hf a

Result:
case intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
b : S
a : R
hab : IsUnit (f a + b)
⊢ IsUnit (f a) ∨ IsUnit b

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
b : S
a : R
hab : IsUnit (f a + b)
⊢ IsUnit (f a) ∨ IsUnit b

Tactic:
obtain ⟨b, rfl⟩ := hf b

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
a b : R
hab : IsUnit (f a + f b)
⊢ IsUnit (f a) ∨ IsUnit (f b)

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
a b : R
hab : IsUnit (f (a + b))
⊢ IsUnit (f a) ∨ IsUnit (f b)

Tactic:
exact
  (isUnit_or_isUnit_of_isUnit_add <| IsLocalHom.map_nonunit _ hab).imp f.isUnit_map
    f.isUnit_map

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem intervalIntegrable_one_div_one_add_sq :
    IntervalIntegrable (fun x : ℝ => 1 / (↑1 + x ^ 2)) μ a b

Proof state:
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
⊢ IntervalIntegrable (fun x => 1 / (1 + x ^ 2)) μ a b

Tactic:
refine (continuous_const.div ?_ fun x => ?_).intervalIntegrable a b

Result:
case refine_1
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous fun x => 1 + x ^ 2

case refine_2
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
x : ℝ
⊢ 1 + x ^ 2 ≠ 0

Proof state:
case refine_1
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous fun x => 1 + x ^ 2

Tactic:
fun_prop

Result:
no goals

Proof state:
case refine_2
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
x : ℝ
⊢ 1 + x ^ 2 ≠ 0

Tactic:
nlinarith

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k}
    (h : m.WF) {hc : k ∈ m.modify k f} : (m.modify k f).getKey k hc = k

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : β k → β k
h : m.WF
hc : k ∈ m.modify k f
⊢ (m.modify k f).getKey k hc = k

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : β k → β k
h : m.WF
hc✝ : k ∈ m.modify k f
hc : (m.modify k f).contains k = true
⊢ (m.modify k f).getKey k hc✝ = k

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : β k → β k
h : m.WF
hc : k ∈ m.modify k f
⊢ (m.modify k f).contains k = true → (m.modify k f).getKey k hc = k

Tactic:
simp_to_raw using Raw₀.getKey_modify_self

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : β k → β k
h : m.WF
hc✝ : k ∈ m.modify k f
hc : (m.modify k f).contains k = true
⊢ (m.modify k f).getKey k hc✝ = k

Tactic:
revert hc

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : β k → β k
h : m.WF
hc : k ∈ m.modify k f
⊢ (m.modify k f).contains k = true → (m.modify k f).getKey k hc = k
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l : Vector α n) (H) :
    pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun _ h => H _ (mem_map_of_mem _ h)

Proof state:
case mk
β : Type u_1
γ : Type u_2
α : Type u_3
p : β → Prop
g : (b : β) → p b → γ
f : α → β
l : Array α
H : ∀ (a : β), a ∈ map f { toArray := l, size_toArray := ⋯ } → p a
⊢ pmap g (map f { toArray := l, size_toArray := ⋯ }) H =
    pmap (fun a h => g (f a) h) { toArray := l, size_toArray := ⋯ } ⋯

Tactic:
simp [Array.pmap_map]

Result:
no goals

Proof state:
β : Type u_1
γ : Type u_2
α : Type u_3
n : Nat
p : β → Prop
g : (b : β) → p b → γ
f : α → β
l : Vector α n
H : ∀ (a : β), a ∈ map f l → p a
⊢ pmap g (map f l) H = pmap (fun a h => g (f a) h) l ⋯

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
β : Type u_1
γ : Type u_2
α : Type u_3
p : β → Prop
g : (b : β) → p b → γ
f : α → β
l : Array α
H : ∀ (a : β), a ∈ map f { toArray := l, size_toArray := ⋯ } → p a
⊢ pmap g (map f { toArray := l, size_toArray := ⋯ }) H =
    pmap (fun a h => g (f a) h) { toArray := l, size_toArray := ⋯ } ⋯