harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/LocalProperties/Exactness.lean
theorem injective_of_isLocalized_maximal
    (H : ∀ (P : Ideal R) [P.IsMaximal], Function.Injective (map P.primeCompl (f P) (g P) F)) :
    Function.Injective F :=
  fun x y eq ↦ Module.eq_of_localization_maximal _ f _ _ fun P _ ↦ H P <| by simp [eq]

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
Nₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_6
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (g P)
F : M →ₗ[R] N
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Function.Injective ⇑((IsLocalizedModule.map P.primeCompl (f P) (g P)) F)
x y : M
eq : F x = F y
P : Ideal R
x✝ : P.IsMaximal
⊢ ((IsLocalizedModule.map P.primeCompl (f P) (g P)) F) ((f P) x) =
    ((IsLocalizedModule.map P.primeCompl (f P) (g P)) F) ((f P) y)

Tactic:
simp [eq]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Types.lean
theorem Presieve.isSheaf_yoneda' {α : Type u} :
    Presieve.IsSheaf typesGrothendieckTopology (yoneda.obj α) :=
  fun β _ hs x hx =>
  ⟨fun y => x _ (hs y) PUnit.unit, fun γ f h =>
    funext fun z => by
      convert congr_fun (hx (𝟙 _) (fun _ => z) (hs <| f z) h rfl) PUnit.unit using 1,
    fun f hf => funext fun y => by convert congr_fun (hf _ (hs y)) PUnit.unit⟩

Proof state:
α β : Type u
x✝ : Sieve β
hs : x✝ ∈ typesGrothendieckTopology β
x : FamilyOfElements (yoneda.obj α) x✝.arrows
hx : x.Compatible
γ : Type u
f : γ ⟶ β
h : x✝.arrows f
z : Opposite.unop (Opposite.op γ)
⊢ (yoneda.obj α).map f.op (fun y => x (fun x => y) ⋯ PUnit.unit) z = x f h z

Tactic:
convert congr_fun (hx (𝟙 _) (fun _ => z) (hs <| f z) h rfl) PUnit.unit using 1

Result:
no goals

Proof state:
α β : Type u
x✝ : Sieve β
hs : x✝ ∈ typesGrothendieckTopology β
x : FamilyOfElements (yoneda.obj α) x✝.arrows
hx : x.Compatible
f : (yoneda.obj α).obj (Opposite.op β)
hf : (fun t => x.IsAmalgamation t) f
y : Opposite.unop (Opposite.op β)
⊢ f y = x (fun x => y) ⋯ PUnit.unit

Tactic:
convert congr_fun (hf _ (hs y)) PUnit.unit

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Interval.lean
theorem concatCM_left {x : Icc a c} (hx : x ≤ b)
    {fg : {fg : C(Icc a b, E) × C(Icc b c, E) // fg.1 ⊤ = fg.2 ⊥}} :
    concatCM fg x = fg.1.1 ⟨x.1, x.2.1, hx⟩

Proof state:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
x : ↑(Icc a c)
hx : ↑x ≤ b
fg : { fg // fg.1 ⊤ = fg.2 ⊥ }
⊢ (concatCM fg) x = (↑fg).1 ⟨↑x, ⋯⟩

Tactic:
exact concat_left fg.2 hx

Result:
no goals
-- Mathlib/Data/Finset/Filter.lean
lemma filter_eq_self : s.filter p = s ↔ ∀ x ∈ s, p x

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ filter p s = s ↔ ∀ x ∈ s, p x

Tactic:
simp [Finset.ext_iff]

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem le_coe_unbotD (x : WithBot α) (b : α) : x ≤ x.unbotD b

Proof state:
α : Type u_1
inst✝ : Preorder α
x : WithBot α
b : α
⊢ x ≤ ↑(unbotD b x)

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnected.lean
theorem ordConnected_iff_uIcc_subset_right (hx : x ∈ s) :
    OrdConnected s ↔ ∀ ⦃y⦄, y ∈ s → [[y, x]] ⊆ s

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
hx : x ∈ s
⊢ s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → [[y, x]] ⊆ s

Tactic:
simp_rw [ordConnected_iff_uIcc_subset_left hx, uIcc_comm]

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem add_mul_self_eq (a b : α) : (a + b) * (a + b) = a * a + 2 * a * b + b * b

Proof state:
α : Type u
inst✝ : CommSemiring α
a b : α
⊢ (a + b) * (a + b) = a * a + 2 * a * b + b * b

Tactic:
simp only [two_mul, add_mul, mul_add, add_assoc, mul_comm b]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_add_emod (a b : Int) : b * (a / b) + a % b = a

Proof state:
a b : Int
⊢ a % b + b * (a / b) = a

Tactic:
exact emod_add_ediv ..

Result:
no goals

Proof state:
a b : Int
⊢ b * (a / b) + a % b = a

Tactic:
rw [Int.add_comm]

Result:
a b : Int
⊢ a % b + b * (a / b) = a
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem iff_isSplitMono_eq_zero {X Y : C} (f : X ⟶ Y) [IsSplitMono f] : IsZero X ↔ f = 0

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
h : f = 0
⊢ 𝟙 X = 0

Tactic:
rw [← IsSplitMono.id f]

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
h : f = 0
⊢ f ≫ retraction f = 0

Proof state:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
⊢ 𝟙 X = 0 → f = 0

Tactic:
intro h

Result:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
h : 𝟙 X = 0
⊢ f = 0

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
h : f = 0
⊢ f ≫ retraction f = 0

Tactic:
simp only [h, zero_comp]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
⊢ 𝟙 X = 0 ↔ f = 0

Tactic:
constructor

Result:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
⊢ 𝟙 X = 0 → f = 0

case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
⊢ f = 0 → 𝟙 X = 0

Proof state:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
h : 𝟙 X = 0
⊢ f = 0

Tactic:
rw [← Category.id_comp f, h, zero_comp]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
⊢ IsZero X ↔ f = 0

Tactic:
rw [iff_id_eq_zero]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
⊢ 𝟙 X = 0 ↔ f = 0

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
⊢ f = 0 → 𝟙 X = 0

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
h : f = 0
⊢ 𝟙 X = 0
-- Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean
theorem exists_factors (a : α) :
    a ≠ 0 → ∃ f : Multiset α, (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a :=
  induction_on_irreducible a (fun h => (h rfl).elim)
    (fun _ hu _ => ⟨0, fun _ h => False.elim (Multiset.not_mem_zero _ h), hu.unit, one_mul _⟩)
    fun a i ha0 hi ih _ =>
    let ⟨s, hs⟩ := ih ha0
    ⟨i ::ₘ s, fun b H => (Multiset.mem_cons.1 H).elim (fun h => h.symm ▸ hi) (hs.1 b), by
      rw [s.prod_cons i]
      exact hs.2.mul_left i⟩

Proof state:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a✝ a i : α
ha0 : a ≠ 0
hi : Irreducible i
ih : a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
x✝ : i * a ≠ 0
s : Multiset α
hs : (∀ b ∈ s, Irreducible b) ∧ s.prod ~ᵤ a
⊢ (i ::ₘ s).prod ~ᵤ i * a

Tactic:
rw [s.prod_cons i]

Result:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a✝ a i : α
ha0 : a ≠ 0
hi : Irreducible i
ih : a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
x✝ : i * a ≠ 0
s : Multiset α
hs : (∀ b ∈ s, Irreducible b) ∧ s.prod ~ᵤ a
⊢ i * s.prod ~ᵤ i * a

Proof state:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a✝ a i : α
ha0 : a ≠ 0
hi : Irreducible i
ih : a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
x✝ : i * a ≠ 0
s : Multiset α
hs : (∀ b ∈ s, Irreducible b) ∧ s.prod ~ᵤ a
⊢ i * s.prod ~ᵤ i * a

Tactic:
exact hs.2.mul_left i

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem maximum_le_of_forall_le {b : WithBot α} (h : ∀ a ∈ l, a ≤ b) : l.maximum ≤ b

Proof state:
case cons
α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithBot α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ↑a ≤ b) → l.maximum ≤ b
h : ∀ (a_1 : α), a_1 ∈ a :: l → ↑a_1 ≤ b
⊢ (a :: l).maximum ≤ b

Tactic:
simp only [maximum_cons, max_le_iff]

Result:
case cons
α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithBot α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ↑a ≤ b) → l.maximum ≤ b
h : ∀ (a_1 : α), a_1 ∈ a :: l → ↑a_1 ≤ b
⊢ ↑a ≤ b ∧ l.maximum ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
b : WithBot α
h : ∀ (a : α), a ∈ l → ↑a ≤ b
⊢ l.maximum ≤ b

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  simp only [maximum_cons, max_le_iff]
  exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : LinearOrder α
l : List α
b : WithBot α
h : ∀ (a : α), a ∈ [] → ↑a ≤ b
⊢ [].maximum ≤ b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithBot α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ↑a ≤ b) → l.maximum ≤ b
h : ∀ (a_1 : α), a_1 ∈ a :: l → ↑a_1 ≤ b
⊢ a ∈ a :: l

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithBot α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ↑a ≤ b) → l.maximum ≤ b
h : ∀ (a_1 : α), a_1 ∈ a :: l → ↑a_1 ≤ b
⊢ ↑a ≤ b ∧ l.maximum ≤ b

Tactic:
exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Gcd.lean
theorem gcd_neg {a b : Int} : gcd a (-b) = gcd a b

Proof state:
a b : Int
⊢ a.gcd (-b) = a.gcd b

Tactic:
simp [gcd]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem foldrM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → β → m β} {g : α → β → m β} {x : β}
    (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) (w : start = l.size) :
    l.foldrM f x start 0 = l.unattach.foldrM g x start 0

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → β → m β
g : α → β → m β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
l : List { x // p x }
⊢ List.foldrM (fun x y => f x y) x l = List.foldrM (fun x y => g x y) x l.unattach

Tactic:
rw [List.foldrM_subtype hf]

Result:
no goals

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → β → m β
g : α → β → m β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
l : List { x // p x }
⊢ foldrM f x { toList := l } = foldrM g x { toList := l }.unattach { toList := l }.size

Tactic:
simp

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → β → m β
g : α → β → m β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
l : List { x // p x }
⊢ List.foldrM (fun x y => f x y) x l = List.foldrM (fun x y => g x y) x l.unattach

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : Array { x // p x }
f : { x // p x } → β → m β
g : α → β → m β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
⊢ foldrM f x l = foldrM g x l.unattach l.size

Tactic:
rcases l with ⟨l⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → β → m β
g : α → β → m β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
l : List { x // p x }
⊢ foldrM f x { toList := l } = foldrM g x { toList := l }.unattach { toList := l }.size

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
start : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : Array { x // p x }
f : { x // p x } → β → m β
g : α → β → m β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
w : start = l.size
⊢ foldrM f x l start = foldrM g x l.unattach start

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : Array { x // p x }
f : { x // p x } → β → m β
g : α → β → m β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
⊢ foldrM f x l = foldrM g x l.unattach l.size
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
lemma opensRange_comp_of_isIso {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
    [IsIso f] [IsOpenImmersion g] : (f ≫ g).opensRange = g.opensRange

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsOpenImmersion g
⊢ opensRange (f ≫ g) = opensRange g

Tactic:
rw [opensRange_comp, opensRange_of_isIso, image_top_eq_opensRange]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem modEq_iff_eq_mod_zmultiples : a ≡ b [PMOD p] ↔ (b : α ⧸ AddSubgroup.zmultiples p) = a

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b : α
⊢ a ≡ b [PMOD p] ↔ ↑b = ↑a

Tactic:
simp_rw [modEq_iff_eq_add_zsmul, QuotientAddGroup.eq_iff_sub_mem, AddSubgroup.mem_zmultiples_iff,
  eq_sub_iff_add_eq', eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_cons_some {f : α → Option β} {a : α} {l : List α} {b : β} (h : f a = some b) :
    filterMap f (a :: l) = b :: filterMap f l

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
a : α
l : List α
b : β
h : f a = some b
⊢ filterMap f (a :: l) = b :: filterMap f l

Tactic:
simp only [filterMap, h]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_top_mul (a : ℝ≥0∞) : ENNReal.toReal (∞ * a) = 0

Proof state:
a : ℝ≥0∞
⊢ (⊤ * a).toReal = 0

Tactic:
rw [mul_comm]

Result:
a : ℝ≥0∞
⊢ (a * ⊤).toReal = 0

Proof state:
a : ℝ≥0∞
⊢ (a * ⊤).toReal = 0

Tactic:
exact toReal_mul_top _

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffAt_one_iff :
    ContDiffAt 𝕜 1 f x ↔
      ∃ f' : E → E →L[𝕜] F, ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ ContDiffAt 𝕜 (↑0 + 1) f x ↔ ∃ f', ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x

Tactic:
simp_rw [contDiffAt_succ_iff_hasFDerivAt, show ((0 : ℕ) : WithTop ℕ∞) = 0 from rfl,
  contDiffAt_zero, exists_mem_and_iff antitone_bforall antitone_continuousOn, and_comm]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ ContDiffAt 𝕜 1 f x ↔ ∃ f', ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x

Tactic:
rw [show (1 : WithTop ℕ∞) = (0 : ℕ) + 1 from rfl]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ ContDiffAt 𝕜 (↑0 + 1) f x ↔ ∃ f', ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem toList_append (arr arr' : Array α) :
    (arr ++ arr').toList = arr.toList ++ arr'.toList

Proof state:
α : Type u_1
arr arr' : Array α
⊢ (arr ++ arr').toList = arr.toList ++ arr'.toList

Tactic:
rw [← append_eq_append]

Result:
α : Type u_1
arr arr' : Array α
⊢ (arr.append arr').toList = arr.toList ++ arr'.toList

Proof state:
α : Type u_1
arr arr' : Array α
⊢ (arr.append arr').toList = arr.toList ++ arr'.toList

Tactic:
unfold Array.append

Result:
α : Type u_1
arr arr' : Array α
⊢ (foldl (fun r v => r.push v) arr arr').toList = arr.toList ++ arr'.toList

Proof state:
α : Type u_1
arr arr' : Array α
⊢ (foldl (fun r v => r.push v) arr arr').toList = arr.toList ++ arr'.toList

Tactic:
rw [← foldl_toList]

Result:
α : Type u_1
arr arr' : Array α
⊢ (List.foldl (fun r v => r.push v) arr arr'.toList).toList = arr.toList ++ arr'.toList

Proof state:
α : Type u_1
arr arr' : Array α
⊢ (List.foldl (fun r v => r.push v) arr arr'.toList).toList = arr.toList ++ arr'.toList

Tactic:
induction arr'.toList generalizing arr <;> simp [*]

Result:
no goals
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem powQuotSuccInclusion_injective (i : ℕ) :
    Function.Injective (powQuotSuccInclusion p P i)

Proof state:
case mk
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
i : ℕ
x : S ⧸ P ^ e
hx : x ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hx0 : ↑((p.powQuotSuccInclusion P i) ⟨x, hx⟩) = ↑0
⊢ ↑⟨x, hx⟩ = ↑0

Tactic:
rwa [powQuotSuccInclusion_apply_coe] at hx0

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
i : ℕ
⊢ ∀ (m : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))), (p.powQuotSuccInclusion P i) m = 0 → m = 0

Tactic:
rintro ⟨x, hx⟩ hx0

Result:
case mk
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
i : ℕ
x : S ⧸ P ^ e
hx : x ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hx0 : (p.powQuotSuccInclusion P i) ⟨x, hx⟩ = 0
⊢ ⟨x, hx⟩ = 0

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
i : ℕ
⊢ Function.Injective ⇑(p.powQuotSuccInclusion P i)

Tactic:
rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']

Result:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
i : ℕ
⊢ ∀ (m : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))), (p.powQuotSuccInclusion P i) m = 0 → m = 0

Proof state:
case mk
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
i : ℕ
x : S ⧸ P ^ e
hx : x ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hx0 : (p.powQuotSuccInclusion P i) ⟨x, hx⟩ = 0
⊢ ⟨x, hx⟩ = 0

Tactic:
rw [Subtype.ext_iff] at hx0 ⊢

Result:
case mk
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
i : ℕ
x : S ⧸ P ^ e
hx : x ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hx0 : ↑((p.powQuotSuccInclusion P i) ⟨x, hx⟩) = ↑0
⊢ ↑⟨x, hx⟩ = ↑0
-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem succ_nth_fib_le_of_nth_den (hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)) :
    (fib (n + 1) : K) ≤ (of v).dens n

Proof state:
case succ
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
hyp : n + 1 = 0 ∨ ¬(of v).TerminatedAt (n + 1 - 1)
⊢ n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 - 1)

Tactic:
exact Or.inr (Or.resolve_left hyp n.succ_ne_zero)

Result:
no goals

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
this : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ ↑(fib (n + 1)) ≤ ((of v).contsAux (n + 1)).b

Tactic:
exact fib_le_of_contsAux_b this

Result:
no goals

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1)

Tactic:
cases n with
| zero => exact Or.inl <| le_refl 1
| succ n => exact Or.inr (Or.resolve_left hyp n.succ_ne_zero)

Result:
no goals

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ ↑(fib (n + 1)) ≤ (of v).dens n

Tactic:
rw [den_eq_conts_b, nth_cont_eq_succ_nth_contAux]

Result:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ ↑(fib (n + 1)) ≤ ((of v).contsAux (n + 1)).b

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ ↑(fib (n + 1)) ≤ ((of v).contsAux (n + 1)).b

Tactic:
have : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1) := by
  cases n with
  | zero => exact Or.inl <| le_refl 1
  | succ n => exact Or.inr (Or.resolve_left hyp n.succ_ne_zero)

Result:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
this : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ ↑(fib (n + 1)) ≤ ((of v).contsAux (n + 1)).b

Proof state:
case zero
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
hyp : 0 = 0 ∨ ¬(of v).TerminatedAt (0 - 1)
⊢ 0 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (0 - 1)

Tactic:
exact Or.inl <| le_refl 1

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.ι_map {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j)
    (j : J) : biproduct.ι f j ≫ biproduct.map p = p j ≫ biproduct.ι g j

Proof state:
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
j : J
⊢ ι f j ≫ map p = p j ≫ ι g j

Tactic:
rw [biproduct.map_eq_map']

Result:
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
j : J
⊢ ι f j ≫ map' p = p j ≫ ι g j

Proof state:
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
j : J
⊢ ι f j ≫ map' p = p j ≫ ι g j

Tactic:
apply
  Limits.IsColimit.ι_map (biproduct.isColimit f) (biproduct.bicone g).toCocone
  (Discrete.natTrans fun j => p j.as) (Discrete.mk j)

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma sub_add_cancel_right {a : EReal} {b : Real} : b - (a + b) = -a

Proof state:
a : EReal
b : ℝ
⊢ ↑b - (a + ↑b) = -a

Tactic:
cases a <;> norm_cast

Result:
case h_real
b a✝ : ℝ
⊢ b - (a✝ + b) = -a✝

Proof state:
case h_real
b a✝ : ℝ
⊢ b - (a✝ + b) = -a✝

Tactic:
exact _root_.sub_add_cancel_right _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem add_eq_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b = c + d) = (a = c + (d - b))

Proof state:
a c b d : Nat
h : b ≤ d
⊢ (a + b = c + d) = (a = c + (d - b))

Tactic:
have g : b ≤ c + d := Nat.le_trans h (le_add_left d c)

Result:
a c b d : Nat
h : b ≤ d
g : b ≤ c + d
⊢ (a + b = c + d) = (a = c + (d - b))

Proof state:
a c b d : Nat
h : b ≤ d
g : b ≤ c + d
⊢ (a + b = c + d) = (a = c + (d - b))

Tactic:
rw [← Nat.add_sub_assoc h, @Eq.comm _ a, Nat.sub_eq_iff_eq_add g, @Eq.comm _ (a + b)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toArray_beq_toArray [BEq α] (a : Vector α n) (b : Vector α n) :
    (a.toArray == b.toArray) = (a == b)

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
a b : Vector α n
⊢ (a.toArray == b.toArray) = (a == b)

Tactic:
simp [instBEq, isEqv, Array.instBEq, Array.isEqv, a.2, b.2]

Result:
no goals