harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_eq (hb : 0 ≤ b) : |a| = b ↔ a = b ∨ a = -b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
hb : 0 ≤ b
⊢ |a| = b ↔ a = b ∨ a = -b

Tactic:
refine ⟨eq_or_eq_neg_of_abs_eq, ?_⟩

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
hb : 0 ≤ b
⊢ a = b ∨ a = -b → |a| = b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
hb : 0 ≤ b
⊢ a = b ∨ a = -b → |a| = b

Tactic:
rintro (rfl | rfl) <;> simp only [abs_neg, abs_of_nonneg hb]

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem Sorted.gt_of_ge [PartialOrder α] {l : List α} (h₁ : l.Sorted (· ≥ ·))
    (h₂ : l.Nodup) : l.Sorted (· > ·) :=
  h₁.imp₂ (fun _ _ => lt_of_le_of_ne) <| by simp_rw [ne_comm]; exact h₂

Proof state:
α : Type u
inst✝ : PartialOrder α
l : List α
h₁ : Sorted (fun x1 x2 => x1 ≥ x2) l
h₂ : l.Nodup
⊢ Pairwise (fun x x_1 => x_1 ≠ x) l

Tactic:
simp_rw [ne_comm]

Result:
α : Type u
inst✝ : PartialOrder α
l : List α
h₁ : Sorted (fun x1 x2 => x1 ≥ x2) l
h₂ : l.Nodup
⊢ Pairwise (fun x x_1 => x ≠ x_1) l

Proof state:
α : Type u
inst✝ : PartialOrder α
l : List α
h₁ : Sorted (fun x1 x2 => x1 ≥ x2) l
h₂ : l.Nodup
⊢ Pairwise (fun x x_1 => x ≠ x_1) l

Tactic:
exact h₂

Result:
no goals
-- Mathlib/Algebra/Exact.lean
@[simp]
lemma exact_zero_iff_surjective {M N : Type*} (P : Type*)
    [AddCommGroup M] [AddCommGroup N] [AddCommMonoid P] [Module R N] [Module R M]
    [Module R P] (f : M →ₗ[R] N) :
    Function.Exact f (0 : N →ₗ[R] P) ↔ Function.Surjective f

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_8
N : Type u_9
P : Type u_10
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommMonoid P
inst✝² : Module R N
inst✝¹ : Module R M
inst✝ : Module R P
f : M →ₗ[R] N
⊢ Exact ⇑f ⇑0 ↔ Surjective ⇑f

Tactic:
simp [← range_eq_top, exact_iff, eq_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem isTheta_exp_comp_exp_comp {f g : α → ℝ} :
    ((fun x => exp (f x)) =Θ[l] fun x => exp (g x)) ↔
      IsBoundedUnder (· ≤ ·) l fun x => |f x - g x|

Proof state:
α : Type u_1
l : Filter α
f g : α → ℝ
⊢ ((fun x => rexp (f x)) =Θ[l] fun x => rexp (g x)) ↔ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => |f x - g x|

Tactic:
simp only [isBoundedUnder_le_abs, ← isBoundedUnder_le_neg, neg_sub, IsTheta,
  isBigO_exp_comp_exp_comp, Pi.sub_def]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem mapIso_hom_app (f g : X ⟶ Y) (h : f = g) (U : Opens Y) :
    (mapIso f g h).hom.app U = eqToHom (by rw [h]) :=
  rfl

Proof state:
X Y Z : TopCat
U✝ V W : Opens ↑X
f g : X ⟶ Y
h : f = g
U : Opens ↑Y
⊢ (map f).obj U = (map g).obj U

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem map {n f} {g : List.Vector ℕ (n + 1) → ℕ} (hf : @Partrec' n f)
    (hg : @Partrec' (n + 1) g) : @Partrec' n fun v => (f v).map fun a => g (a ::ᵥ v)

Proof state:
n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' f
hg : Partrec' ↑g
⊢ Partrec' fun v => Part.map (fun a => g (a ::ᵥ v)) (f v)

Tactic:
simpa [(Part.bind_some_eq_map _ _).symm] using hf.bind hg

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem length_mul_mod_two (w₁ w₂ : W) : ℓ (w₁ * w₂) % 2 = (ℓ w₁ + ℓ w₂) % 2

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length (w₁ * w₂) % 2 = (cs.length w₁ + cs.length w₂) % 2

Tactic:
rw [← ZMod.natCast_eq_natCast_iff', Nat.cast_add]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ ↑(cs.length (w₁ * w₂)) = ↑(cs.length w₁) + ↑(cs.length w₂)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ ↑(cs.length (w₁ * w₂)) = ↑(cs.length w₁) + ↑(cs.length w₂)

Tactic:
simpa only [lengthParity_eq_ofAdd_length, ofAdd_add] using map_mul cs.lengthParity w₁ w₂

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem div_pow (dvd : p ^ a ∣ b) : padicValNat p (b / p ^ a) = padicValNat p b - a

Proof state:
p a b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ^ a ∣ b
⊢ padicValNat p (b / p ^ a) = padicValNat p b - a

Tactic:
rw [padicValNat.div_of_dvd dvd, padicValNat.prime_pow]

Result:
no goals
-- Mathlib/Algebra/Field/Rat.lean
protected lemma zpow_nonneg {a : ℚ} (ha : 0 ≤ a) : ∀ n : ℤ, 0 ≤ a ^ n
  | Int.ofNat n => by simp [ha]
  | Int.negSucc n => by simpa using Rat.inv_nonneg (pow_nonneg ha (n + 1))

Proof state:
a : ℚ
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ Int.negSucc n

Tactic:
simpa using Rat.inv_nonneg (pow_nonneg ha (n + 1))

Result:
no goals

Proof state:
a : ℚ
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ Int.ofNat n

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive]
lemma norm_mul_eq_norm_left (x : E) {y : E} (h : ‖y‖ = 0) : ‖x * y‖ = ‖x‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x * y‖ ≤ ‖x‖

Tactic:
simpa [h] using norm_mul_le' x y

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x * y‖ = ‖x‖

Tactic:
apply le_antisymm ?_ ?_

Result:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x * y‖ ≤ ‖x‖

E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x‖ ≤ ‖x * y‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x‖ ≤ ‖x * y‖

Tactic:
simpa [h] using norm_le_mul_norm_add x y

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem unifIntegrable_finite [Finite ι] (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) {f : ι → α → β}
    (hf : ∀ i, MemLp (f i) p μ) : UnifIntegrable f p μ

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
n : ℕ
hn : Nonempty (ι ≃ Fin n)
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := f ∘ ⇑hn.some.symm
hg : ∀ (i : Fin n), MemLp (g i) p μ
δ : ℝ
hδpos : 0 < δ
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
hδ : eLpNorm (s.indicator (g (hn.some i))) p μ ≤ ENNReal.ofReal ε
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
simp_rw [g, Function.comp_apply, Equiv.symm_apply_apply] at hδ

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
n : ℕ
hn : Nonempty (ι ≃ Fin n)
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := f ∘ ⇑hn.some.symm
hg : ∀ (i : Fin n), MemLp (g i) p μ
δ : ℝ
hδpos : 0 < δ
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
hδ : eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Proof state:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
n : ℕ
hn : Nonempty (ι ≃ Fin n)
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := f ∘ ⇑hn.some.symm
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
have hg : ∀ i, MemLp (g i) p μ := fun _ => hf _

Result:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
n : ℕ
hn : Nonempty (ι ≃ Fin n)
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := f ∘ ⇑hn.some.symm
hg : ∀ (i : Fin n), MemLp (g i) p μ
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffWithinAt.comp_of_eq {s : Set E} {t : Set F} {g : F → G} {f : E → F} {y : F} (x : E)
    (hg : ContDiffWithinAt 𝕜 n g t y) (hf : ContDiffWithinAt 𝕜 n f s x) (st : MapsTo f s t)
    (hy : f x = y) :
    ContDiffWithinAt 𝕜 n (g ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
st : MapsTo f s t
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
exact hg.comp x hf st

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
st : MapsTo f s t
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
subst hy

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
st : MapsTo f s t
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x
-- Mathlib/CategoryTheory/LiftingProperties/Adjunction.lean
theorem right_adjoint_hasLift_iff : HasLift (sq.right_adjoint adj) ↔ HasLift sq

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Nonempty ⋯.LiftStruct ↔ Nonempty sq.LiftStruct

Tactic:
exact Equiv.nonempty_congr (sq.rightAdjointLiftStructEquiv adj).symm

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ ⋯.HasLift ↔ sq.HasLift

Tactic:
simp only [HasLift.iff]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Nonempty ⋯.LiftStruct ↔ Nonempty sq.LiftStruct
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
    (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (mem_of_getElem? H)

Proof state:
case cons.succ
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
⊢ (pmap f (hd :: tl) h)[n✝ + 1]? = Option.pmap f (hd :: tl)[n✝ + 1]? ⋯

Tactic:
simp only [hl, pmap, Option.pmap, getElem?_cons_succ]

Result:
case cons.succ
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
⊢ (match tl[n✝]?, ⋯ with
    | none, x => none
    | some a, H => some (f a ⋯)) =
    match (hd :: tl)[n✝ + 1]?, ⋯ with
    | none, x => none
    | some a, H => some (f a ⋯)

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n : Nat
⊢ (pmap f (hd :: tl) h)[n]? = Option.pmap f (hd :: tl)[n]? ⋯

Tactic:
rcases n with ⟨n⟩

Result:
case cons.zero
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
⊢ (pmap f (hd :: tl) h)[0]? = Option.pmap f (hd :: tl)[0]? ⋯

case cons.succ
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
⊢ (pmap f (hd :: tl) h)[n✝ + 1]? = Option.pmap f (hd :: tl)[n✝ + 1]? ⋯
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_filter_le_of_right_le [DecidablePred (b ≤ ·)] :
    ((Ico a b).filter fun x => b ≤ x) = ∅

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x => b ≤ x
⊢ filter (fun x => b ≤ x) (Ico a b) = ∅

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_right_le]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x => b ≤ x
⊢ ∅.val = ∅

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x => b ≤ x
⊢ ∅.val = ∅

Tactic:
rfl

Result:
no goals
-- Mathlib/Logic/Relation.lean
@[simp] lemma map_map (r : α → β → Prop) (f₁ : α → γ) (g₁ : β → δ) (f₂ : γ → ε) (g₂ : δ → ζ) :
    Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁)

Proof state:
case h.h.a.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → β → Prop
f₁ : α → γ
g₁ : β → δ
f₂ : γ → ε
g₂ : δ → ζ
a✝ : ε
b✝ : ζ
a : α
b : β
hab : r a b
h : f₂ (f₁ a) = a✝ ∧ g₂ (g₁ b) = b✝
⊢ r a b ∧ f₂ (f₁ a) = a✝ ∧ g₂ (g₁ b) = b✝

Tactic:
exact ⟨hab, h⟩

Result:
no goals

Proof state:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → β → Prop
f₁ : α → γ
g₁ : β → δ
f₂ : γ → ε
g₂ : δ → ζ
a✝ : ε
b✝ : ζ
a : α
b : β
⊢ (∃ b_1 a_1, (r a b ∧ f₁ a = b_1 ∧ g₁ b = a_1) ∧ f₂ b_1 = a✝ ∧ g₂ a_1 = b✝) → r a b ∧ f₂ (f₁ a) = a✝ ∧ g₂ (g₁ b) = b✝

Tactic:
rintro ⟨_, _, ⟨hab, rfl, rfl⟩, h⟩

Result:
case h.h.a.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → β → Prop
f₁ : α → γ
g₁ : β → δ
f₂ : γ → ε
g₂ : δ → ζ
a✝ : ε
b✝ : ζ
a : α
b : β
hab : r a b
h : f₂ (f₁ a) = a✝ ∧ g₂ (g₁ b) = b✝
⊢ r a b ∧ f₂ (f₁ a) = a✝ ∧ g₂ (g₁ b) = b✝

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → β → Prop
f₁ : α → γ
g₁ : β → δ
f₂ : γ → ε
g₂ : δ → ζ
⊢ Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁)

Tactic:
ext a b

Result:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → β → Prop
f₁ : α → γ
g₁ : β → δ
f₂ : γ → ε
g₂ : δ → ζ
a : ε
b : ζ
⊢ Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ a b ↔ Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁) a b

Proof state:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → β → Prop
f₁ : α → γ
g₁ : β → δ
f₂ : γ → ε
g₂ : δ → ζ
a : ε
b : ζ
⊢ (∃ b_1 b_2 b_3 a_1, (r b_1 b_2 ∧ f₁ b_1 = b_3 ∧ g₁ b_2 = a_1) ∧ f₂ b_3 = a ∧ g₂ a_1 = b) ↔
    ∃ a_1 b_1, r a_1 b_1 ∧ f₂ (f₁ a_1) = a ∧ g₂ (g₁ b_1) = b

Tactic:
refine exists₂_congr fun a b ↦ ⟨?_, fun h ↦ ⟨_, _, ⟨⟨h.1, rfl, rfl⟩, h.2⟩⟩⟩

Result:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → β → Prop
f₁ : α → γ
g₁ : β → δ
f₂ : γ → ε
g₂ : δ → ζ
a✝ : ε
b✝ : ζ
a : α
b : β
⊢ (∃ b_1 a_1, (r a b ∧ f₁ a = b_1 ∧ g₁ b = a_1) ∧ f₂ b_1 = a✝ ∧ g₂ a_1 = b✝) → r a b ∧ f₂ (f₁ a) = a✝ ∧ g₂ (g₁ b) = b✝

Proof state:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → β → Prop
f₁ : α → γ
g₁ : β → δ
f₂ : γ → ε
g₂ : δ → ζ
a : ε
b : ζ
⊢ Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ a b ↔ Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁) a b

Tactic:
simp_rw [Relation.Map, Function.comp_apply, ← exists_and_right, @exists_comm γ, @exists_comm δ]

Result:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → β → Prop
f₁ : α → γ
g₁ : β → δ
f₂ : γ → ε
g₂ : δ → ζ
a : ε
b : ζ
⊢ (∃ b_1 b_2 b_3 a_1, (r b_1 b_2 ∧ f₁ b_1 = b_3 ∧ g₁ b_2 = a_1) ∧ f₂ b_3 = a ∧ g₂ a_1 = b) ↔
    ∃ a_1 b_1, r a_1 b_1 ∧ f₂ (f₁ a_1) = a ∧ g₂ (g₁ b_1) = b
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem tsupport_iteratedFDeriv_subset (n : ℕ) : tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f

Proof state:
case zero
𝕜 : 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
⊢ tsupport (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) ⊆ tsupport f

Tactic:
exact closure_minimal ((support_comp_subset (LinearIsometryEquiv.map_zero _) _).trans
  subset_closure) isClosed_closure

Result:
no goals

Proof state:
case zero
𝕜 : 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
⊢ tsupport (iteratedFDeriv 𝕜 0 f) ⊆ tsupport f

Tactic:
rw [iteratedFDeriv_zero_eq_comp]

Result:
case zero
𝕜 : 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
⊢ tsupport (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) ⊆ tsupport f

Proof state:
case succ
𝕜 : 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
n : ℕ
IH : tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
⊢ tsupport (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) ⊆ tsupport f

Tactic:
exact closure_minimal ((support_comp_subset (LinearIsometryEquiv.map_zero _) _).trans
  ((support_fderiv_subset 𝕜).trans IH)) isClosed_closure

Result:
no goals

Proof state:
case succ
𝕜 : 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
n : ℕ
IH : tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
⊢ tsupport (iteratedFDeriv 𝕜 (n + 1) f) ⊆ tsupport f

Tactic:
rw [iteratedFDeriv_succ_eq_comp_left]

Result:
case succ
𝕜 : 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
n : ℕ
IH : tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
⊢ tsupport (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) ⊆ tsupport f

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
n : ℕ
⊢ tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f

Tactic:
induction n with
| zero =>
  rw [iteratedFDeriv_zero_eq_comp]
  exact closure_minimal ((support_comp_subset (LinearIsometryEquiv.map_zero _) _).trans
    subset_closure) isClosed_closure
| succ n IH =>
  rw [iteratedFDeriv_succ_eq_comp_left]
  exact closure_minimal ((support_comp_subset (LinearIsometryEquiv.map_zero _) _).trans
    ((support_fderiv_subset 𝕜).trans IH)) isClosed_closure

Result:
no goals
-- Mathlib/Topology/NoetherianSpace.lean
theorem NoetherianSpace.finite_irreducibleComponents [NoetherianSpace α] :
    (irreducibleComponents α).Finite

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
⊢ (irreducibleComponents α).Finite

Tactic:
obtain ⟨S : Set (Set α), hSf, hSc, hSi, hSU⟩ :=
  NoetherianSpace.exists_finite_set_isClosed_irreducible isClosed_univ (α := α)

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
S : Set (Set α)
hSf : S.Finite
hSc : ∀ t ∈ S, IsClosed t
hSi : ∀ t ∈ S, IsIrreducible t
hSU : Set.univ = ⋃₀ S
⊢ (irreducibleComponents α).Finite

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ t ∈ ↑S, IsClosed t
hSi : ∀ t ∈ ↑S, IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
t : Set α
htS : t ∈ S
ht : s ⊆ t
⊢ s ∈ ↑S

Tactic:
rwa [ht.antisymm (hs.2 (hSi _ htS) ht)]

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
S : Set (Set α)
hSf : S.Finite
hSc : ∀ t ∈ S, IsClosed t
hSi : ∀ t ∈ S, IsIrreducible t
hSU : Set.univ = ⋃₀ S
s : Set α
hs : s ∈ irreducibleComponents α
⊢ s ∈ S

Tactic:
lift S to Finset (Set α) using hSf

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ t ∈ ↑S, IsClosed t
hSi : ∀ t ∈ ↑S, IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
⊢ s ∈ ↑S

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ t ∈ ↑S, IsClosed t
hSi : ∀ t ∈ ↑S, IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
⊢ s ∈ ↑S

Tactic:
rcases isIrreducible_iff_sUnion_isClosed.1 hs.1 S hSc (hSU ▸ Set.subset_univ _) with ⟨t, htS, ht⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ t ∈ ↑S, IsClosed t
hSi : ∀ t ∈ ↑S, IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
t : Set α
htS : t ∈ S
ht : s ⊆ t
⊢ s ∈ ↑S

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
S : Set (Set α)
hSf : S.Finite
hSc : ∀ t ∈ S, IsClosed t
hSi : ∀ t ∈ S, IsIrreducible t
hSU : Set.univ = ⋃₀ S
⊢ (irreducibleComponents α).Finite

Tactic:
refine hSf.subset fun s hs => ?_

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
S : Set (Set α)
hSf : S.Finite
hSc : ∀ t ∈ S, IsClosed t
hSi : ∀ t ∈ S, IsIrreducible t
hSU : Set.univ = ⋃₀ S
s : Set α
hs : s ∈ irreducibleComponents α
⊢ s ∈ S
-- Mathlib/FieldTheory/Differential/Basic.lean
lemma logDeriv_mul (ha : a ≠ 0) (hb : b ≠ 0) : logDeriv (a * b) = logDeriv a + logDeriv b

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b′ + b * a′ = a′ * b + b′ * a

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b)′ / (a * b) = a′ / a + b′ / b

Tactic:
field_simp

Result:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b′ + b * a′ = a′ * b + b′ * a

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ logDeriv (a * b) = logDeriv a + logDeriv b

Tactic:
unfold logDeriv

Result:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b)′ / (a * b) = a′ / a + b′ / b