harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/SetSemiring.lean
theorem accumulate_mem (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ i, s i ∈ C) (n : ℕ) :
    Accumulate s n ∈ C

Proof state:
case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : Accumulate s n ∈ C
⊢ Accumulate s (n + 1) ∈ C

Tactic:
rw [accumulate_succ]

Result:
case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : Accumulate s n ∈ C
⊢ Accumulate s n ∪ s (n + 1) ∈ C

Proof state:
case zero
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
⊢ Accumulate s 0 ∈ C

Tactic:
simp [hs 0]

Result:
no goals

Proof state:
case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : Accumulate s n ∈ C
⊢ Accumulate s n ∪ s (n + 1) ∈ C

Tactic:
exact hC.union_mem hn (hs _)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
⊢ Accumulate s n ∈ C

Tactic:
induction n with
| zero => simp [hs 0]
| succ n hn => rw [accumulate_succ]; exact hC.union_mem hn (hs _)

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem mem_im_iff (hφ : Function.Injective φ.obj) {c d : D} (f : c ⟶ d) :
    f ∈ (im φ hφ).arrows c d ↔
      ∃ (a b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d),
        f = eqToHom ha.symm ≫ φ.map g ≫ eqToHom hb

Proof state:
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_2.h.a
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
c d : D
f : c ⟶ d
x✝⁴ x✝³ : C
x✝² : x✝⁴ ⟶ x✝³
x✝¹ : φ.obj x✝⁴ = c
x✝ : φ.obj x✝³ = d
⊢ f = eqToHom ⋯ ≫ φ.map x✝² ≫ eqToHom x✝ ↔ ∃ (_ : x✝² ∈ ⊤.arrows x✝⁴ x✝³), f = eqToHom ⋯ ≫ φ.map x✝² ≫ eqToHom x✝

Tactic:
simp only [Top.top, mem_univ, exists_true_left]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
c d : D
f : c ⟶ d
⊢ f ∈ (im φ hφ).arrows c d ↔ ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
convert Map.arrows_iff φ hφ ⊤ f

Result:
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_2.h.a
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
c d : D
f : c ⟶ d
x✝⁴ x✝³ : C
x✝² : x✝⁴ ⟶ x✝³
x✝¹ : φ.obj x✝⁴ = c
x✝ : φ.obj x✝³ = d
⊢ f = eqToHom ⋯ ≫ φ.map x✝² ≫ eqToHom x✝ ↔ ∃ (_ : x✝² ∈ ⊤.arrows x✝⁴ x✝³), f = eqToHom ⋯ ≫ φ.map x✝² ≫ eqToHom x✝
-- Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
lemma hasRightDerivedFunctor_iff_of_iso :
    HasRightDerivedFunctor F W ↔ HasRightDerivedFunctor F' W

Proof state:
C : Type u_1
H : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} H
F F' : C ⥤ H
e : F ≅ F'
W : MorphismProperty C
⊢ F.HasRightDerivedFunctor W ↔ F'.HasRightDerivedFunctor W

Tactic:
rw [hasRightDerivedFunctor_iff F W.Q W, hasRightDerivedFunctor_iff F' W.Q W,
  hasLeftExtension_iff_of_iso₂ W.Q e]

Result:
no goals
-- Mathlib/Data/Fintype/Quotient.lean
/-- Choice-free induction principle for quotients indexed by a finite type.
  See `Quotient.induction_on_pi` for the general version assuming `Classical.choice`. -/
@[elab_as_elim]
lemma ind_fintype_pi {C : (∀ i, Quotient (S i)) → Prop}
    (f : ∀ a : ∀ i, α i, C (⟦a ·⟧)) (q : ∀ i, Quotient (S i)) : C q

Proof state:
case a
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C✝ : ((i : ι) → Quotient (S i)) → Prop
f : ∀ (a : (i : ι) → α i), C✝ fun x => ⟦a x⟧
q : (i : ι) → Quotient (S i)
a✝ : List ι
C : ((i : ι) → i ∈ ⟦a✝⟧ → Quotient (S i)) → Prop
⊢ (∀ (a : (i : ι) → i ∈ ⟦a✝⟧ → α i), C fun x1 x2 => ⟦a x1 x2⟧) → ∀ (q : (i : ι) → i ∈ ⟦a✝⟧ → Quotient (S i)), C q

Tactic:
exact list_ind

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C✝ : ((i : ι) → Quotient (S i)) → Prop
f : ∀ (a : (i : ι) → α i), C✝ fun x => ⟦a x⟧
q : (i : ι) → Quotient (S i)
m : Multiset ι
C : ((i : ι) → i ∈ m → Quotient (S i)) → Prop
⊢ (∀ (a : (i : ι) → i ∈ m → α i), C fun x1 x2 => ⟦a x1 x2⟧) → ∀ (q : (i : ι) → i ∈ m → Quotient (S i)), C q

Tactic:
induction m using Quotient.ind

Result:
case a
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C✝ : ((i : ι) → Quotient (S i)) → Prop
f : ∀ (a : (i : ι) → α i), C✝ fun x => ⟦a x⟧
q : (i : ι) → Quotient (S i)
a✝ : List ι
C : ((i : ι) → i ∈ ⟦a✝⟧ → Quotient (S i)) → Prop
⊢ (∀ (a : (i : ι) → i ∈ ⟦a✝⟧ → α i), C fun x1 x2 => ⟦a x1 x2⟧) → ∀ (q : (i : ι) → i ∈ ⟦a✝⟧ → Quotient (S i)), C q
-- Mathlib/Algebra/Order/Ring/Basic.lean
lemma Odd.pow_neg_iff (hn : Odd n) : a ^ n < 0 ↔ a < 0

Proof state:
case intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
inst✝ : ExistsAddOfLE R
ha : a < 0
k : ℕ
⊢ a ^ (2 * k + 1) < 0

Tactic:
rw [pow_succ]

Result:
case intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
inst✝ : ExistsAddOfLE R
ha : a < 0
k : ℕ
⊢ a ^ (2 * k) * a < 0

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
ha : a < 0
⊢ a ^ n < 0

Tactic:
obtain ⟨k, rfl⟩ := hn

Result:
case intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
inst✝ : ExistsAddOfLE R
ha : a < 0
k : ℕ
⊢ a ^ (2 * k + 1) < 0

Proof state:
case intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
inst✝ : ExistsAddOfLE R
ha : a < 0
k : ℕ
⊢ a ^ (2 * k) * a < 0

Tactic:
exact mul_neg_of_pos_of_neg ((even_two_mul _).pow_pos ha.ne) ha

Result:
no goals
-- Mathlib/Data/List/Lookmap.lean
theorem length_lookmap (l : List α) : length (l.lookmap f) = length l

Proof state:
case h
α : Type u_1
f : α → Option α
l : List α
⊢ ∀ (a b : α), b ∈ f a → () = ()

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
f : α → Option α
l : List α
⊢ (lookmap f l).length = l.length

Tactic:
rw [← length_map, lookmap_map_eq _ fun _ => (), length_map]

Result:
case h
α : Type u_1
f : α → Option α
l : List α
⊢ ∀ (a b : α), b ∈ f a → () = ()
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_fiberwise_eq_prod_filter' (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : κ → α) :
    ∏ j ∈ t, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s with g i ∈ t, f (g i)

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : κ → α
j : κ
x✝ : j ∈ t
i : ι
hi : i ∈ filter (fun i => g i = j) s
⊢ f j = f (g i)

Tactic:
rw [(mem_filter.1 hi).2]

Result:
no goals

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : κ → α
⊢ ∏ j ∈ t, ∏ i ∈ filter (fun i => g i = j) s, f j = ∏ i ∈ filter (fun i => g i ∈ t) s, f (g i)

Tactic:
calc
  _ = ∏ j ∈ t, ∏ i ∈ s with g i = j, f (g i) :=
      prod_congr rfl fun j _ ↦ prod_congr rfl fun i hi ↦ by rw [(mem_filter.1 hi).2]
  _ = _ := prod_fiberwise_eq_prod_filter _ _ _ _

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive (attr := simp)]
lemma mul_smul_one {M N} [MulOneClass N] [SMul M N] [SMulCommClass M N N] (x : M) (y : N) :
    y * x • (1 : N) = x • y

Proof state:
M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : SMulCommClass M N N
x : M
y : N
⊢ y * x • 1 = x • y

Tactic:
rw [← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem image_coe_nnreal_ennreal (h : t.OrdConnected) : ((↑) '' t : Set ℝ≥0∞).OrdConnected

Proof state:
case intro.intro
t : Set ℝ≥0
h : t.OrdConnected
x : ℝ≥0
hx : x ∈ t
y : ℝ≥0
hy : y ∈ t
z : ℝ≥0
hz : ↑z ∈ Icc ↑x ↑y
⊢ ↑z ∈ ofNNReal '' t

Tactic:
exact mem_image_of_mem _ (h.out hx hy ⟨ENNReal.coe_le_coe.1 hz.1, ENNReal.coe_le_coe.1 hz.2⟩)

Result:
no goals

Proof state:
t : Set ℝ≥0
h : t.OrdConnected
⊢ (ofNNReal '' t).OrdConnected

Tactic:
refine ⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩

Result:
t : Set ℝ≥0
h : t.OrdConnected
x : ℝ≥0
hx : x ∈ t
y : ℝ≥0
hy : y ∈ t
z : ℝ≥0∞
hz : z ∈ Icc ↑x ↑y
⊢ z ∈ ofNNReal '' t

Proof state:
t : Set ℝ≥0
h : t.OrdConnected
x : ℝ≥0
hx : x ∈ t
y : ℝ≥0
hy : y ∈ t
z : ℝ≥0∞
hz : z ∈ Icc ↑x ↑y
⊢ z ∈ ofNNReal '' t

Tactic:
rcases ENNReal.le_coe_iff.1 hz.2 with ⟨z, rfl, -⟩

Result:
case intro.intro
t : Set ℝ≥0
h : t.OrdConnected
x : ℝ≥0
hx : x ∈ t
y : ℝ≥0
hy : y ∈ t
z : ℝ≥0
hz : ↑z ∈ Icc ↑x ↑y
⊢ ↑z ∈ ofNNReal '' t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem max?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) :
    (replicate n a).max? = if n = 0 then none else some a

Proof state:
case zero
α : Type u_1
inst✝ : Max α
a : α
w : max a a = a
⊢ (replicate 0 a).max? = if 0 = 0 then none else some a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Max α
n : Nat
a : α
w : max a a = a
⊢ (replicate n a).max? = if n = 0 then none else some a

Tactic:
induction n with
| zero => rfl
| succ n ih => cases n <;> simp_all [replicate_succ, max?_cons']

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : Max α
a : α
w : max a a = a
n : Nat
ih : (replicate n a).max? = if n = 0 then none else some a
⊢ (replicate (n + 1) a).max? = if n + 1 = 0 then none else some a

Tactic:
cases n <;> simp_all [replicate_succ, max?_cons']

Result:
no goals
-- Mathlib/Data/List/TakeDrop.lean
theorem takeD_left (l₁ l₂ : List α) (a : α) : takeD (length l₁) (l₁ ++ l₂) a = l₁ :=
  (takeD_eq_take a (by simp only [length_append, Nat.le_add_right])).trans (take_left _ _)

Proof state:
α : Type u
l₁ l₂ : List α
a : α
⊢ l₁.length ≤ (l₁ ++ l₂).length

Tactic:
simp only [length_append, Nat.le_add_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_flatMap (l : Array α) (f : α → Array β) :
    (l.flatMap f).size = sum (map (fun a => (f a).size) l)

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
l : List α
⊢ (flatMap f { toList := l }).size = (map (fun a => (f a).size) { toList := l }).sum

Tactic:
simp [Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → Array β
⊢ (flatMap f l).size = (map (fun a => (f a).size) l).sum

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
l : List α
⊢ (flatMap f { toList := l }).size = (map (fun a => (f a).size) { toList := l }).sum
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Ici_eq_Ioi_iInf {R : Type*} [CompleteLinearOrder R] {f : ι → R}
    (no_least_elem : ⨅ i, f i ∉ range f) : ⋃ i : ι, Ici (f i) = Ioi (⨅ i, f i)

Proof state:
ι : Sort u
R : Type u_1
inst✝ : CompleteLinearOrder R
f : ι → R
no_least_elem : ⨅ i, f i ∉ range f
⊢ ⋃ i, Ici (f i) = Ioi (⨅ i, f i)

Tactic:
simp only [← IsGLB.biUnion_Ici_eq_Ioi (@isGLB_iInf _ _ _ f) no_least_elem, mem_range,
  iUnion_exists, iUnion_iUnion_eq']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem attachWith_reverse {P : α → Prop} {xs : List α}
    {H : ∀ (a : α), a ∈ xs.reverse → P a} :
    xs.reverse.attachWith P H =
      (xs.attachWith P (fun a h => H a (by simpa using h))).reverse :=
  pmap_reverse ..

Proof state:
α : Type ?u.78229
P : α → Prop
xs : List α
H : ∀ (a : α), a ∈ xs.reverse → P a
a : α
h : a ∈ xs
⊢ a ∈ xs.reverse

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/Matrix/Defs.lean
theorem map_map {M : Matrix m n α} {β γ : Type*} {f : α → β} {g : β → γ} :
    (M.map f).map g = M.map (g ∘ f)

Proof state:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
β : Type u_10
γ : Type u_11
f : α → β
g : β → γ
⊢ (M.map f).map g = M.map (g ∘ f)

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
β : Type u_10
γ : Type u_11
f : α → β
g : β → γ
i✝ : m
j✝ : n
⊢ (M.map f).map g i✝ j✝ = M.map (g ∘ f) i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
β : Type u_10
γ : Type u_11
f : α → β
g : β → γ
i✝ : m
j✝ : n
⊢ (M.map f).map g i✝ j✝ = M.map (g ∘ f) i✝ j✝

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem comul_comp_snd :
    comul ∘ₗ .snd R A B = TensorProduct.map (.snd R A B) (.snd R A B) ∘ₗ comul

Proof state:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (comul ∘ₗ LinearMap.snd R A B) ∘ₗ inr R A B =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inr R A B

Tactic:
rw [comp_assoc, snd_comp_inr, comp_id, comp_assoc, comul_comp_inr, ← comp_assoc,
  ← TensorProduct.map_comp, snd_comp_inr, TensorProduct.map_id, id_comp]

Result:
no goals

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul ∘ₗ LinearMap.snd R A B = TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul

Tactic:
ext : 1

Result:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (comul ∘ₗ LinearMap.snd R A B) ∘ₗ inl R A B =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B

case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (comul ∘ₗ LinearMap.snd R A B) ∘ₗ inr R A B =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inr R A B

Proof state:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (comul ∘ₗ LinearMap.snd R A B) ∘ₗ inl R A B =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B

Tactic:
rw [comp_assoc, snd_comp_inl, comp_zero, comp_assoc, comul_comp_inl, ← comp_assoc,
  ← TensorProduct.map_comp, snd_comp_inl, TensorProduct.map_zero_left, zero_comp]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Conformal.lean
theorem IsConformalMap.preserves_angle {f' : E →L[ℝ] F} (h : IsConformalMap f') (u v : E) :
    angle (f' u) (f' v) = angle u v

Proof state:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f' : E →L[ℝ] F
h : IsConformalMap f'
u v : E
⊢ angle (f' u) (f' v) = angle u v

Tactic:
obtain ⟨c, hc, li, rfl⟩ := h

Result:
case intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
u v : E
c : ℝ
hc : c ≠ 0
li : E →ₗᵢ[ℝ] F
⊢ angle ((c • li.toContinuousLinearMap) u) ((c • li.toContinuousLinearMap) v) = angle u v

Proof state:
case intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
u v : E
c : ℝ
hc : c ≠ 0
li : E →ₗᵢ[ℝ] F
⊢ angle ((c • li.toContinuousLinearMap) u) ((c • li.toContinuousLinearMap) v) = angle u v

Tactic:
exact (angle_smul_smul hc _ _).trans (li.angle_map _ _)

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem UniformCauchySeqOnFilter.mono_right {p'' : Filter α} (hf : UniformCauchySeqOnFilter F p p')
    (hp : p'' ≤ p') : UniformCauchySeqOnFilter F p p'' := fun u hu =>
  have := (hf u hu).filter_mono ((p ×ˢ p).prod_mono_right hp)
  this.mono (by simp)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' p'' : Filter α
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
this : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p'', (F x.1.1 x.2, F x.1.2 x.2) ∈ u
⊢ ∀ (x : (ι × ι) × α), (F x.1.1 x.2, F x.1.2 x.2) ∈ u → (F x.1.1 x.2, F x.1.2 x.2) ∈ u

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
private lemma continuousAt_mul_symm1 {a b : EReal}
    (h : ContinuousAt (fun p : EReal × EReal ↦ p.1 * p.2) (a, b)) :
    ContinuousAt (fun p : EReal × EReal ↦ p.1 * p.2) (-a, b)

Proof state:
a b : EReal
h : ContinuousAt (fun p => p.1 * p.2) (a, b)
this : (fun p => p.1 * p.2) = (fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)
⊢ ContinuousAt ((fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)) (-a, b)

Tactic:
apply ContinuousAt.comp (Continuous.continuousAt continuous_neg)
  <| ContinuousAt.comp _ (ContinuousAt.prodMap (Continuous.continuousAt continuous_neg)
    (Continuous.continuousAt continuous_id))

Result:
a b : EReal
h : ContinuousAt (fun p => p.1 * p.2) (a, b)
this : (fun p => p.1 * p.2) = (fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)
⊢ ContinuousAt (fun p => p.1 * p.2) (Prod.map (fun a => -a) id (-a, b))

Proof state:
a b : EReal
h : ContinuousAt (fun p => p.1 * p.2) (a, b)
this : (fun p => p.1 * p.2) = (fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)
⊢ ContinuousAt (fun p => p.1 * p.2) (-a, b)

Tactic:
rw [this]

Result:
a b : EReal
h : ContinuousAt (fun p => p.1 * p.2) (a, b)
this : (fun p => p.1 * p.2) = (fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)
⊢ ContinuousAt ((fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)) (-a, b)

Proof state:
a b : EReal
h : ContinuousAt (fun p => p.1 * p.2) (a, b)
⊢ (fun p => p.1 * p.2) = (fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)

Tactic:
ext p

Result:
case h
a b : EReal
h : ContinuousAt (fun p => p.1 * p.2) (a, b)
p : EReal × EReal
⊢ p.1 * p.2 = ((fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)) p

Proof state:
case h
a b : EReal
h : ContinuousAt (fun p => p.1 * p.2) (a, b)
p : EReal × EReal
⊢ p.1 * p.2 = ((fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)) p

Tactic:
simp

Result:
no goals

Proof state:
a b : EReal
h : ContinuousAt (fun p => p.1 * p.2) (a, b)
⊢ ContinuousAt (fun p => p.1 * p.2) (-a, b)

Tactic:
have : (fun p : EReal × EReal ↦ p.1 * p.2) = (fun x : EReal ↦ -x)
    ∘ (fun p : EReal × EReal ↦ p.1 * p.2) ∘ (fun p : EReal × EReal ↦ (-p.1, p.2)) := by
  ext p
  simp

Result:
a b : EReal
h : ContinuousAt (fun p => p.1 * p.2) (a, b)
this : (fun p => p.1 * p.2) = (fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)
⊢ ContinuousAt (fun p => p.1 * p.2) (-a, b)

Proof state:
a b : EReal
h : ContinuousAt (fun p => p.1 * p.2) (a, b)
this : (fun p => p.1 * p.2) = (fun x => -x) ∘ (fun p => p.1 * p.2) ∘ fun p => (-p.1, p.2)
⊢ ContinuousAt (fun p => p.1 * p.2) (Prod.map (fun a => -a) id (-a, b))

Tactic:
simp [h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
@[simp]
lemma inr_rel'_inr_iff (x₂ y₂ : X₂) :
    Rel' f g (Sum.inr x₂) (Sum.inr y₂) ↔ x₂ = y₂

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr y₂) ↔ x₂ = y₂

Tactic:
constructor

Result:
case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr y₂) → x₂ = y₂

case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ x₂ = y₂ → Rel' f g (Sum.inr x₂) (Sum.inr y₂)

Proof state:
case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr y₂) → x₂ = y₂

Tactic:
rintro ⟨_⟩

Result:
case mp.refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ : X₂
⊢ x₂ = x₂

Proof state:
case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr x₂)

Tactic:
apply Rel'.refl

Result:
no goals

Proof state:
case mp.refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ : X₂
⊢ x₂ = x₂

Tactic:
rfl

Result:
no goals

Proof state:
case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ x₂ = y₂ → Rel' f g (Sum.inr x₂) (Sum.inr y₂)

Tactic:
rintro rfl

Result:
case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr x₂)
-- Mathlib/Analysis/Calculus/FDeriv/Comp.lean
theorem HasStrictFDerivAt.comp {g : F → G} {g' : F →L[𝕜] G}
    (hg : HasStrictFDerivAt g g' (f x)) (hf : HasStrictFDerivAt f f' x) :
    HasStrictFDerivAt (fun x => g (f x)) (g'.comp f') x :=
  .of_isLittleO <|
    ((hg.isLittleO.comp_tendsto (hf.continuousAt.prodMap' hf.continuousAt)).trans_isBigO
        hf.isBigO_sub).triangle <| by
      simpa only [g'.map_sub, f'.coe_comp'] using (g'.isBigO_comp _ _).trans_isLittleO hf.isLittleO

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
g : F → G
g' : F →L[𝕜] G
hg : HasStrictFDerivAt g g' (f x)
hf : HasStrictFDerivAt f f' x
⊢ (fun x => g' ((Prod.map f f x).1 - (Prod.map f f x).2) - (g'.comp f') (x.1 - x.2)) =o[𝓝 (x, x)] fun p => p.1 - p.2

Tactic:
simpa only [g'.map_sub, f'.coe_comp'] using (g'.isBigO_comp _ _).trans_isLittleO hf.isLittleO

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Completion.lean
theorem mk_eq_zero {f : CauSeq _ abv} : mk f = 0 ↔ LimZero f

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
⊢ mk f = 0 ↔ f.LimZero

Tactic:
have : mk f = 0 ↔ LimZero (f - 0) := Quotient.eq

Result:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
this : mk f = 0 ↔ (f - 0).LimZero
⊢ mk f = 0 ↔ f.LimZero

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
this : mk f = 0 ↔ (f - 0).LimZero
⊢ mk f = 0 ↔ f.LimZero

Tactic:
rwa [sub_zero] at this

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_one_sub' (hx : 0 ≤ x) (h : 1 - y ≠ 0) : x ^ (1 - y) = x / x ^ y

Proof state:
x y : ℝ
hx : 0 ≤ x
h : 1 - y ≠ 0
⊢ x ^ (1 - y) = x / x ^ y

Tactic:
rw [rpow_sub' hx h, rpow_one]

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
/-- A column partitioned matrix when transposed gives a row partitioned matrix with columns of the
initial matrix transposed to become rows. -/
lemma transpose_fromCols (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
    transpose (fromCols A₁ A₂) = fromRows (transpose A₁) (transpose A₂)

Proof state:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
⊢ (A₁.fromCols A₂)ᵀ = A₁ᵀ.fromRows A₂ᵀ

Tactic:
ext (i | i) j <;> simp

Result:
no goals
-- Mathlib/GroupTheory/CosetCover.lean
theorem finiteIndex_of_leftCoset_cover_const : H.FiniteIndex

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
⊢ H.FiniteIndex

Tactic:
simp_rw [leftCoset_cover_const_iff_surjOn] at hcovers

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Set.SurjOn (fun x => ↑(g x)) (↑s) Set.univ
⊢ H.FiniteIndex

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Set.SurjOn (fun x => ↑(g x)) (↑s) Set.univ
this : Finite (G ⧸ H)
⊢ H.FiniteIndex

Tactic:
exact H.finiteIndex_of_finite_quotient

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Set.SurjOn (fun x => ↑(g x)) (↑s) Set.univ
⊢ H.FiniteIndex

Tactic:
have := Set.finite_univ_iff.mp <| Set.Finite.of_surjOn _ hcovers s.finite_toSet

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Set.SurjOn (fun x => ↑(g x)) (↑s) Set.univ
this : Finite (G ⧸ H)
⊢ H.FiniteIndex