harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Bicategory/Functor/Lax.lean
@[reassoc, to_app]
lemma mapComp_assoc_left {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
    F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h = (α_ (F.map f) (F.map g) (F.map h)).hom ≫
      F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h) ≫ F.map₂ (α_ f g h).inv

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : LaxFunctor B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h =
    F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h ≫ F.map₂ ((α_ f g h).hom ≫ (α_ f g h).inv)

Tactic:
simp only [Iso.hom_inv_id, PrelaxFunctor.map₂_id, comp_id]

Result:
no goals

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : LaxFunctor B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h =
    (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h) ≫ F.map₂ (α_ f g h).inv

Tactic:
rw [← F.map₂_associator_assoc, ← F.map₂_comp]

Result:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : LaxFunctor B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h =
    F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h ≫ F.map₂ ((α_ f g h).hom ≫ (α_ f g h).inv)
-- Mathlib/RingTheory/RootsOfUnity/Basic.lean
theorem rootsOfUnity_le_of_dvd (h : k ∣ l) : rootsOfUnity k M ≤ rootsOfUnity l M

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k l : ℕ
h : k ∣ l
⊢ rootsOfUnity k M ≤ rootsOfUnity l M

Tactic:
obtain ⟨d, rfl⟩ := h

Result:
case intro
M : Type u_1
inst✝ : CommMonoid M
k d : ℕ
⊢ rootsOfUnity k M ≤ rootsOfUnity (k * d) M

Proof state:
case intro
M : Type u_1
inst✝ : CommMonoid M
k d : ℕ
⊢ rootsOfUnity k M ≤ rootsOfUnity (k * d) M

Tactic:
intro ζ h

Result:
case intro
M : Type u_1
inst✝ : CommMonoid M
k d : ℕ
ζ : Mˣ
h : ζ ∈ rootsOfUnity k M
⊢ ζ ∈ rootsOfUnity (k * d) M

Proof state:
case intro
M : Type u_1
inst✝ : CommMonoid M
k d : ℕ
ζ : Mˣ
h : ζ ∈ rootsOfUnity k M
⊢ ζ ∈ rootsOfUnity (k * d) M

Tactic:
simp_all only [mem_rootsOfUnity, pow_mul, one_pow]

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Lattice.lean
theorem pairwiseDisjoint_prod_left {s : Set ι} {t : Set ι'} {f : ι × ι' → α} :
    (s ×ˢ t : Set (ι × ι')).PairwiseDisjoint f ↔
      (s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')) ∧
        t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')

Proof state:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
⊢ (s ×ˢ t).PairwiseDisjoint f ↔
    (s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')) ∧ t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')

Tactic:
refine
    ⟨fun h => ⟨fun i hi j hj hij => ?_, fun i hi j hj hij => ?_⟩, fun h => h.1.prod_left h.2⟩ <;>
  simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff] <;>
  intro i' hi' j' hj'

Result:
case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
i' : ι'
hi' : i' ∈ t
j' : ι'
hj' : j' ∈ t
⊢ Disjoint (f (i, i')) (f (j, j'))

case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
j' : ι
hj' : j' ∈ s
⊢ Disjoint (f (i', i)) (f (j', j))

Proof state:
case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
i' : ι'
hi' : i' ∈ t
j' : ι'
hj' : j' ∈ t
⊢ Disjoint (f (i, i')) (f (j, j'))

Tactic:
exact h (mk_mem_prod hi hi') (mk_mem_prod hj hj') (ne_of_apply_ne Prod.fst hij)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
j' : ι
hj' : j' ∈ s
⊢ Disjoint (f (i', i)) (f (j', j))

Tactic:
exact h (mk_mem_prod hi' hi) (mk_mem_prod hj' hj) (ne_of_apply_ne Prod.snd hij)

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem ne₁₃_of_not_collinear {p₁ p₂ p₃ : P} (h : ¬Collinear k ({p₁, p₂, p₃} : Set P)) :
    p₁ ≠ p₃

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : ¬Collinear k {p₁, p₂, p₃}
⊢ p₁ ≠ p₃

Tactic:
rintro rfl

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
h : ¬Collinear k {p₁, p₂, p₁}
⊢ False

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
h : ¬Collinear k {p₁, p₂, p₁}
⊢ False

Tactic:
simp [collinear_pair] at h

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem zpow_lt_top (ha : a ≠ 0) (h'a : a ≠ ∞) (n : ℤ) : a ^ n < ∞

Proof state:
case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ a ^ Int.ofNat a✝ < ⊤

Tactic:
simpa using ENNReal.pow_lt_top h'a.lt_top _

Result:
no goals

Proof state:
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ⊤
n : ℤ
⊢ a ^ n < ⊤

Tactic:
cases n

Result:
case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ a ^ Int.ofNat a✝ < ⊤

case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ a ^ Int.negSucc a✝ < ⊤

Proof state:
case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ a ^ Int.negSucc a✝ < ⊤

Tactic:
simp only [ENNReal.pow_pos ha.bot_lt, zpow_negSucc, inv_lt_top]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
lemma ceilRoot_ne_zero : ceilRoot n a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0

Proof state:
a n : ℕ
⊢ n.ceilRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0

Tactic:
simp +contextual [ceilRoot_def, not_imp_not, not_or]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0)
    (him : z.im = 0) : Tendsto arg (𝓝[{ z : ℂ | 0 ≤ z.im }] z) (𝓝 π)

Proof state:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto arg (𝓝[{z | 0 ≤ z.im}] z) (𝓝 π)

Tactic:
simpa only [arg_eq_pi_iff.2 ⟨hre, him⟩] using
  (continuousWithinAt_arg_of_re_neg_of_im_zero hre him).tendsto

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma sq_eq_sq_iff_abs_eq_abs (a b : α) : a ^ 2 = b ^ 2 ↔ |a| = |b|

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ a ^ 2 = b ^ 2 ↔ |a| = |b|

Tactic:
simp only [le_antisymm_iff, sq_le_sq]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
theorem tensorFunc_obj_map (Z : F C) {n n' : N C} (f : n ⟶ n') :
    ((tensorFunc C).obj Z).map f = inclusion.map f ▷ Z

Proof state:
case mk
C : Type u
Z : F C
n' : (Discrete ∘ NormalMonoidalObject) C
as✝ : NormalMonoidalObject C
f : { as := as✝ } ⟶ n'
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ▷ Z

Tactic:
cases n'

Result:
case mk.mk
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
f : { as := as✝¹ } ⟶ { as := as✝ }
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ▷ Z

Proof state:
case mk.mk.up.up
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
h : as✝¹ = as✝
⊢ ((tensorFunc C).obj Z).map { down := { down := h } } = inclusion.map { down := { down := h } } ▷ Z

Tactic:
subst h

Result:
case mk.mk.up.up
C : Type u
Z : F C
as✝ : NormalMonoidalObject C
⊢ ((tensorFunc C).obj Z).map { down := { down := ⋯ } } = inclusion.map { down := { down := ⋯ } } ▷ Z

Proof state:
C : Type u
Z : F C
n n' : (Discrete ∘ NormalMonoidalObject) C
f : n ⟶ n'
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ▷ Z

Tactic:
cases n

Result:
case mk
C : Type u
Z : F C
n' : (Discrete ∘ NormalMonoidalObject) C
as✝ : NormalMonoidalObject C
f : { as := as✝ } ⟶ n'
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ▷ Z

Proof state:
case mk.mk.up.up
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
h : { as := as✝¹ }.as = { as := as✝ }.as
⊢ ((tensorFunc C).obj Z).map { down := { down := h } } = inclusion.map { down := { down := h } } ▷ Z

Tactic:
dsimp at h

Result:
case mk.mk.up.up
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
h : as✝¹ = as✝
⊢ ((tensorFunc C).obj Z).map { down := { down := h } } = inclusion.map { down := { down := h } } ▷ Z

Proof state:
case mk.mk.up.up
C : Type u
Z : F C
as✝ : NormalMonoidalObject C
⊢ ((tensorFunc C).obj Z).map { down := { down := ⋯ } } = inclusion.map { down := { down := ⋯ } } ▷ Z

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
f : { as := as✝¹ } ⟶ { as := as✝ }
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ▷ Z

Tactic:
rcases f with ⟨⟨h⟩⟩

Result:
case mk.mk.up.up
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
h : { as := as✝¹ }.as = { as := as✝ }.as
⊢ ((tensorFunc C).obj Z).map { down := { down := h } } = inclusion.map { down := { down := h } } ▷ Z
-- Mathlib/Algebra/Group/Units/Equiv.lean
theorem isLocalHom_equiv [Monoid M] [Monoid N] [EquivLike F M N]
    [MulEquivClass F M N] (f : F) : IsLocalHom f where
  map_nonunit a ha

Proof state:
case h.e'_3
F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
a : M
ha : IsUnit (f a)
⊢ ↑f a = f a

Tactic:
rfl

Result:
no goals

Proof state:
F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
a : M
ha : IsUnit (f a)
⊢ IsUnit a

Tactic:
convert ha.map (f : M ≃* N).symm

Result:
case h.e'_3
F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
a : M
ha : IsUnit (f a)
⊢ a = (↑f).symm (f a)

Proof state:
case h.e'_3
F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
a : M
ha : IsUnit (f a)
⊢ a = (↑f).symm (f a)

Tactic:
rw [MulEquiv.eq_symm_apply]

Result:
case h.e'_3
F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
a : M
ha : IsUnit (f a)
⊢ ↑f a = f a
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousAt.comp₂_continuousWithinAt_of_eq {f : β × γ → δ} {g : α → β}
    {h : α → γ} {x : α} {s : Set α} {y : β × γ} (hf : ContinuousAt f y)
    (hg : ContinuousWithinAt g s x) (hh : ContinuousWithinAt h s x) (e : (g x, h x) = y) :
    ContinuousWithinAt (fun x ↦ f (g x, h x)) s x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
y : β × γ
hf : ContinuousAt f y
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
e : (g x, h x) = y
⊢ ContinuousWithinAt (fun x => f (g x, h x)) s x

Tactic:
rw [← e] at hf

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
y : β × γ
hf : ContinuousAt f (g x, h x)
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
e : (g x, h x) = y
⊢ ContinuousWithinAt (fun x => f (g x, h x)) s x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
y : β × γ
hf : ContinuousAt f (g x, h x)
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
e : (g x, h x) = y
⊢ ContinuousWithinAt (fun x => f (g x, h x)) s x

Tactic:
exact hf.comp₂_continuousWithinAt hg hh

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Ergodic.lean
theorem preErgodic_of_preErgodic_conjugate (hg : MeasurePreserving g μ μ') (hf : PreErgodic f μ)
    {f' : β → β} (h_comm : Semiconj g f f') : PreErgodic f' μ' where
  aeconst_set s hs₀ hs₁

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ EventuallyConst (g ⁻¹' s) (ae μ)

Tactic:
apply hf.aeconst_set (hg.measurable hs₀)

Result:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ f ⁻¹' (g ⁻¹' s) = g ⁻¹' s

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ EventuallyConst s (ae μ')

Tactic:
rw [← hg.aeconst_preimage hs₀.nullMeasurableSet]

Result:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ EventuallyConst (g ⁻¹' s) (ae μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ f ⁻¹' (g ⁻¹' s) = g ⁻¹' s

Tactic:
rw [← preimage_comp, h_comm.comp_eq, preimage_comp, hs₁]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem prodComparison_comp {E : Type u₂} [Category.{v₂} E] [ChosenFiniteProducts E] (G : D ⥤ E) :
    prodComparison (F ⋙ G) A B =
      G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F : C ⥤ D
A B : C
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : ChosenFiniteProducts E
G : D ⥤ E
⊢ prodComparison (F ⋙ G) A B = G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B)

Tactic:
unfold prodComparison

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F : C ⥤ D
A B : C
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : ChosenFiniteProducts E
G : D ⥤ E
⊢ lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd A B)) =
    G.map (lift (F.map (fst A B)) (F.map (snd A B))) ≫
      lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.obj B)))

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F : C ⥤ D
A B : C
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : ChosenFiniteProducts E
G : D ⥤ E
⊢ lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd A B)) =
    G.map (lift (F.map (fst A B)) (F.map (snd A B))) ≫
      lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.obj B)))

Tactic:
ext <;> simp [← G.map_comp]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma IsBasis'.closure_eq_closure (h : M.IsBasis' I X) : M.closure I = M.closure X

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
⊢ M.closure I = M.closure X

Tactic:
rw [← closure_inter_ground _ X, h.isBasis_inter_ground.closure_eq_closure]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_nnnorm_equiv (f : WithLp ∞ (α × β)) : ‖WithLp.equiv ⊤ _ f‖₊ = ‖f‖₊

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
f : WithLp ⊤ (α × β)
⊢ ‖(WithLp.equiv ⊤ (α × β)) f‖₊ = ‖f‖₊

Tactic:
rw [prod_nnnorm_eq_sup, Prod.nnnorm_def, equiv_fst, equiv_snd]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem setLaverage_eq (f : α → ℝ≥0∞) (s : Set α) :
    ⨍⁻ x in s, f x ∂μ = (∫⁻ x in s, f x ∂μ) / μ s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ⨍⁻ (x : α) in s, f x ∂μ = (∫⁻ (x : α) in s, f x ∂μ) / μ s

Tactic:
rw [laverage_eq, restrict_apply_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem coprod_inl (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : (coprod f g).comp (inl R M M₂) = f

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
⊢ f.coprod g ∘ₗ inl R M M₂ = f

Tactic:
ext

Result:
case h
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
x✝ : M
⊢ (f.coprod g ∘ₗ inl R M M₂) x✝ = f x✝

Proof state:
case h
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
x✝ : M
⊢ (f.coprod g ∘ₗ inl R M M₂) x✝ = f x✝

Tactic:
simp only [map_zero, add_zero, coprod_apply, inl_apply, comp_apply]

Result:
no goals
-- Mathlib/Data/Fintype/Option.lean
theorem Fintype.card_option {α : Type*} [Fintype α] :
    Fintype.card (Option α) = Fintype.card α + 1 :=
  (Finset.card_cons (by simp)).trans <| congr_arg₂ _ (card_map _) rfl

Proof state:
α : Type u_3
inst✝ : Fintype α
⊢ none ∉ map Embedding.some univ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pi_div_two_sub (x : ℂ) : sin (π / 2 - x) = cos x

Proof state:
x : ℂ
⊢ sin (↑π / 2 - x) = cos x

Tactic:
simp [sub_eq_add_neg, sin_add]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem moveRight_neg {x : PGame} (i) :
    (-x).moveRight i = -x.moveLeft (toRightMovesNeg.symm i)

Proof state:
x : PGame
i : (-x).RightMoves
⊢ (-x).moveRight i = -x.moveLeft (toRightMovesNeg.symm i)

Tactic:
cases x

Result:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (-mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (-mk α✝ β✝ a✝¹ a✝).moveRight i = -(mk α✝ β✝ a✝¹ a✝).moveLeft (toRightMovesNeg.symm i)

Proof state:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (-mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (-mk α✝ β✝ a✝¹ a✝).moveRight i = -(mk α✝ β✝ a✝¹ a✝).moveLeft (toRightMovesNeg.symm i)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem hsum_smul_module {R} {V} [Semiring R] [AddCommMonoid V] [Module R V] {x : HahnSeries Γ R}
    {s : SummableFamily Γ' V α} :
    (x • s).hsum = (of R).symm (x • of R s.hsum)

Proof state:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
x : HahnSeries Γ R
s : SummableFamily Γ' V α
⊢ (x • s).hsum = (of R).symm (x • (of R) s.hsum)

Tactic:
rw [smul_eq, hsum_equiv, smul_hsum, hsum_single]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem mu_bdd (n : ℕ) : (mu μ hn n : ℝ) / n ∈ Set.Icc (0 : ℝ) 1

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : ¬n = 0
⊢ ↑(mu μ hn n) / ↑n ≤ 1

Tactic:
rw [div_le_one (cast_pos.mpr (Nat.pos_of_ne_zero hn0)), cast_le]

Result:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : ¬n = 0
⊢ mu μ hn n ≤ n

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
⊢ ↑(mu μ hn n) / ↑n ∈ Set.Icc 0 1

Tactic:
refine Set.mem_Icc.mpr ⟨div_nonneg (cast_nonneg (mu μ hn n)) (cast_nonneg n), ?_⟩

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
⊢ ↑(mu μ hn n) / ↑n ≤ 1

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : ¬n = 0
⊢ mu μ hn n ≤ n

Tactic:
exact mu_le _ _ _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
⊢ ↑(mu μ hn n) / ↑n ≤ 1

Tactic:
by_cases hn0 : n = 0

Result:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : n = 0
⊢ ↑(mu μ hn n) / ↑n ≤ 1

case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : ¬n = 0
⊢ ↑(mu μ hn n) / ↑n ≤ 1

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : n = 0
⊢ ↑(mu μ hn n) / ↑n ≤ 1

Tactic:
rw [hn0, cast_zero, div_zero]

Result:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : n = 0
⊢ 0 ≤ 1

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : n = 0
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finsupp.lean
theorem mk_finsupp_of_infinite (α β : Type u) [Infinite α] [Zero β] [Nontrivial β] :
    #(α →₀ β) = max #α #β

Proof state:
α β : Type u
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α →₀ β) = #α ⊔ #β

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_cons {l : List α} {a : α} :
    mapIdx f (a :: l) = f 0 a :: mapIdx (fun i => f (i + 1)) l

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
a : α
⊢ mapIdx f (a :: l) = f 0 a :: mapIdx (fun i => f (i + 1)) l

Tactic:
simp [mapIdx_eq_zipIdx_map, List.zipIdx_succ]

Result:
no goals