harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc]
lemma d_sndX (i j : ι) (hij : c.Rel i j) :
    d φ i j ≫ sndX φ j = fstX φ i j hij ≫ φ.f j + sndX φ i ≫ G.d i j

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
⊢ (if hij : c.Rel i j then
        (if hj : c.Rel j (c.next j) then -fstX φ i j hij ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hj else 0) +
            fstX φ i j hij ≫ φ.f j ≫ inrX φ j +
          sndX φ i ≫ G.d i j ≫ inrX φ j
      else 0) ≫
      sndX φ j =
    fstX φ i j hij ≫ φ.f j + sndX φ i ≫ G.d i j

Tactic:
split_ifs with hij <;> simp

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
⊢ d φ i j ≫ sndX φ j = fstX φ i j hij ≫ φ.f j + sndX φ i ≫ G.d i j

Tactic:
dsimp [d]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
⊢ (if hij : c.Rel i j then
        (if hj : c.Rel j (c.next j) then -fstX φ i j hij ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hj else 0) +
            fstX φ i j hij ≫ φ.f j ≫ inrX φ j +
          sndX φ i ≫ G.d i j ≫ inrX φ j
      else 0) ≫
      sndX φ j =
    fstX φ i j hij ≫ φ.f j + sndX φ i ≫ G.d i j
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem map_iff [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β]
    [BorelSpace β] (f : α ≃ₜ β) :
    Regular (Measure.map f μ) ↔ Regular μ

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
⊢ (map (⇑f) μ).Regular ↔ μ.Regular

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.map f⟩

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).Regular
⊢ μ.Regular

Proof state:
case h.e'_4
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).Regular
⊢ μ = map (⇑f.symm) (map (⇑f) μ)

Tactic:
rw [map_map f.symm.continuous.measurable f.continuous.measurable]

Result:
case h.e'_4
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).Regular
⊢ μ = map (⇑f.symm ∘ ⇑f) μ

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).Regular
⊢ μ.Regular

Tactic:
convert h.map f.symm

Result:
case h.e'_4
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).Regular
⊢ μ = map (⇑f.symm) (map (⇑f) μ)

Proof state:
case h.e'_4
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).Regular
⊢ μ = map (⇑f.symm ∘ ⇑f) μ

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem sign_eq_and_abs_eq_iff_eq {x y : EReal} :
    x.abs = y.abs ∧ sign x = sign y ↔ x = y

Proof state:
case mp
x y : EReal
⊢ x.abs = y.abs ∧ sign x = sign y → x = y

Tactic:
rintro ⟨habs, hsign⟩

Result:
case mp.intro
x y : EReal
habs : x.abs = y.abs
hsign : sign x = sign y
⊢ x = y

Proof state:
case mp.intro
x y : EReal
habs : x.abs = y.abs
hsign : sign x = sign y
⊢ x = y

Tactic:
rw [← x.sign_mul_abs, ← y.sign_mul_abs, habs, hsign]

Result:
no goals

Proof state:
case mpr
x : EReal
⊢ x.abs = x.abs ∧ sign x = sign x

Tactic:
exact ⟨rfl, rfl⟩

Result:
no goals

Proof state:
x y : EReal
⊢ x.abs = y.abs ∧ sign x = sign y ↔ x = y

Tactic:
constructor

Result:
case mp
x y : EReal
⊢ x.abs = y.abs ∧ sign x = sign y → x = y

case mpr
x y : EReal
⊢ x = y → x.abs = y.abs ∧ sign x = sign y

Proof state:
case mpr
x y : EReal
⊢ x = y → x.abs = y.abs ∧ sign x = sign y

Tactic:
rintro rfl

Result:
case mpr
x : EReal
⊢ x.abs = x.abs ∧ sign x = sign x
-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
lemma freeYonedaEquiv_symm_app (M : PresheafOfModules.{v} R) (X : C)
    (x : M.obj (Opposite.op X)) :
    (freeYonedaEquiv.symm x).app (Opposite.op X) (ModuleCat.freeMk (𝟙 _)) = x

Proof state:
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : C
x : ↑(M.obj (Opposite.op X))
⊢ (ConcreteCategory.hom (𝟙 (M.presheaf.obj (Opposite.op X)))) x = x

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : C
x : ↑(M.obj (Opposite.op X))
⊢ (ConcreteCategory.hom (ModuleCat.freeDesc fun f => (ConcreteCategory.hom (M.presheaf.map f.op)) x))
      (ModuleCat.freeMk (𝟙 X)) =
    x

Tactic:
rw [ModuleCat.freeDesc_apply, op_id, M.presheaf.map_id]

Result:
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : C
x : ↑(M.obj (Opposite.op X))
⊢ (ConcreteCategory.hom (𝟙 (M.presheaf.obj (Opposite.op X)))) x = x

Proof state:
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : C
x : ↑(M.obj (Opposite.op X))
⊢ (ConcreteCategory.hom ((freeYonedaEquiv.symm x).app (Opposite.op X)))
      (ModuleCat.freeMk (𝟙 (Opposite.unop (Opposite.op X)))) =
    x

Tactic:
dsimp [freeYonedaEquiv, freeHomEquiv, yonedaEquiv]

Result:
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : C
x : ↑(M.obj (Opposite.op X))
⊢ (ConcreteCategory.hom (ModuleCat.freeDesc fun f => (ConcreteCategory.hom (M.presheaf.map f.op)) x))
      (ModuleCat.freeMk (𝟙 X)) =
    x
-- Mathlib/Topology/Irreducible.lean
theorem IsPreirreducible.subset_irreducible {S U : Set X} (ht : IsPreirreducible t)
    (hU : U.Nonempty) (hU' : IsOpen U) (h₁ : U ⊆ S) (h₂ : S ⊆ t) : IsIrreducible S

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen u
hv : IsOpen v
x✝ : X
hx : x✝ ∈ S
hx'✝ : x✝ ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
x : X
hx' : x ∈ U ∧ x ∈ u ∧ x ∈ v
⊢ (S ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨x, h₁ hx'.1, hx'.2⟩

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem map_sup [SemilatticeSup β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
    f (x ⊔ y) = f x ⊔ f y

Proof state:
case inr.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ x ∈ s

Tactic:
assumption

Result:
no goals

Proof state:
case inr.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
this : f y ≤ f x
⊢ f (x ⊔ y) = f x ⊔ f y

Tactic:
simp only [*, sup_of_le_left, sup_of_le_right]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ f (x ⊔ y) = f x ⊔ f y

Tactic:
cases le_total x y <;> have := hf ?_ ?_ ‹_› <;>
  first
  | assumption
  | simp only [*, sup_of_le_left, sup_of_le_right]

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fib_le_fib_succ {n : ℕ} : fib n ≤ fib (n + 1)

Proof state:
n : ℕ
⊢ fib n ≤ fib (n + 1)

Tactic:
cases n <;> simp [fib_add_two]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/PowerBasis.lean
theorem repr_gen_pow_isIntegral (hB : IsIntegral R B.gen) [IsDomain S]
    (hmin : minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)) (n : ℕ) :
    ∀ i, IsIntegral R (B.basis.repr (B.gen ^ n) i)

Proof state:
case pos
S : Type u_2
inst✝⁷ : CommRing S
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : ⟨j, hj⟩ = i
⊢ IsIntegral R (Q.coeff j • 1)

Tactic:
rw [Algebra.smul_def, mul_one]

Result:
case pos
S : Type u_2
inst✝⁷ : CommRing S
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : ⟨j, hj⟩ = i
⊢ IsIntegral R ((algebraMap R S) (Q.coeff j))

Proof state:
case pos
S : Type u_2
inst✝⁷ : CommRing S
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : Q = 0
⊢ IsIntegral R ((B.basis.repr (B.gen ^ n)) i)

Tactic:
simp [this, hQ, isIntegral_zero]

Result:
no goals
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem supp_map (h : q.IsUniform) {α β : Type u} (g : α → β) (x : F α) :
    supp (g <$> x) = g '' supp x

Proof state:
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
⊢ supp (g <$> x) = g '' supp x

Tactic:
rw [← abs_repr x]

Result:
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
⊢ supp (g <$> abs (repr x)) = g '' supp (abs (repr x))

Proof state:
case mk
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ supp (g <$> abs ⟨a, f⟩) = g '' supp (abs ⟨a, f⟩)

Tactic:
rw [← abs_map, PFunctor.map_eq]

Result:
case mk
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, g ∘ f⟩) = g '' supp (abs ⟨a, f⟩)

Proof state:
case mk
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, g ∘ f⟩) = g '' supp (abs ⟨a, f⟩)

Tactic:
rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, image_comp]

Result:
no goals

Proof state:
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
⊢ supp (g <$> abs (repr x)) = g '' supp (abs (repr x))

Tactic:
obtain ⟨a, f⟩ := repr x

Result:
case mk
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ supp (g <$> abs ⟨a, f⟩) = g '' supp (abs ⟨a, f⟩)
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem MemLp.integral_indicator_norm_ge_le (hf : MemLp f 1 μ) (hmeas : StronglyMeasurable f)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ M : ℝ, (∫⁻ x, ‖{ x | M ≤ ‖f x‖₊ }.indicator f x‖₊ ∂μ) ≤ ENNReal.ofReal ε

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
⊢ ∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε

Tactic:
have hbound : HasFiniteIntegral (fun x => ‖f x‖) μ := by
  rw [memLp_one_iff_integrable] at hf
  exact hf.norm.2

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x => ‖f x‖) μ
⊢ ∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem monic_X_pow_add_C {n : ℕ} (h : n ≠ 0) : (X ^ n + C a).Monic :=
   monic_X_pow_add <| (lt_of_le_of_lt degree_C_le
     (by simp only [Nat.cast_pos, Nat.pos_iff_ne_zero, ne_eq, h, not_false_eq_true]))

Proof state:
R : Type u
a : R
inst✝ : Semiring R
n : ℕ
h : n ≠ 0
⊢ 0 < ↑n

Tactic:
simp only [Nat.cast_pos, Nat.pos_iff_ne_zero, ne_eq, h, not_false_eq_true]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
@[simp]
lemma baseChange_id : (.id : M →ₗ[R] M).baseChange A = .id

Proof state:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A id)) 1) x✝ = ((AlgebraTensorModule.curry id) 1) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ baseChange A id = id

Tactic:
ext

Result:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A id)) 1) x✝ = ((AlgebraTensorModule.curry id) 1) x✝
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem Δ_of_isCharTwoJNeZeroNF_of_char_two : W.Δ = W.a₆

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ -1 ^ 2 * W.a₆ - 8 * 0 ^ 3 - 27 * 0 ^ 2 + 9 * 1 * 0 * 0 = W.a₆

Tactic:
linear_combination -W.a₆ * CharP.cast_eq_zero R 2

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.Δ = W.a₆

Tactic:
rw [Δ, b₂_of_isCharTwoJNeZeroNF_of_char_two, b₄_of_isCharTwoJNeZeroNF,
  b₆_of_isCharTwoJNeZeroNF_of_char_two, b₈_of_isCharTwoJNeZeroNF_of_char_two]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ -1 ^ 2 * W.a₆ - 8 * 0 ^ 3 - 27 * 0 ^ 2 + 9 * 1 * 0 * 0 = W.a₆
-- Mathlib/Data/List/DropRight.lean
theorem rdropWhile_singleton (x : α) : rdropWhile p [x] = if p x then [] else [x]

Proof state:
α : Type u_1
p : α → Bool
x : α
⊢ rdropWhile p [x] = if p x = true then [] else [x]

Tactic:
rw [← nil_append [x], rdropWhile_concat, rdropWhile_nil]

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem nnnorm_map_eq (A : Matrix m n α) (f : α → β) (hf : ∀ a, ‖f a‖₊ = ‖a‖₊) :
    ‖A.map f‖₊ = ‖A‖₊

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊
⊢ ‖A.map f‖₊ = ‖A‖₊

Tactic:
simp only [nnnorm_def, Pi.nnnorm_def, Matrix.map_apply, hf]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem le_mul_prod_of_opNorm_le_of_le {f : ContinuousMultilinearMap 𝕜 E G}
    {m : ∀ i, E i} {C : ℝ} {b : ι → ℝ} (hC : ‖f‖ ≤ C) (hm : ∀ i, ‖m i‖ ≤ b i) :
    ‖f m‖ ≤ C * ∏ i, b i :=
  (f.le_opNorm m).trans <| by gcongr; exacts [f.opNorm_nonneg.trans hC, hm _]

Proof state:
case b0
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
C : ℝ
b : ι → ℝ
hC : ‖f‖ ≤ C
hm : ∀ (i : ι), ‖m i‖ ≤ b i
⊢ 0 ≤ C

case h₂.h1
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
C : ℝ
b : ι → ℝ
hC : ‖f‖ ≤ C
hm : ∀ (i : ι), ‖m i‖ ≤ b i
i✝ : ι
a✝ : i✝ ∈ univ
⊢ ‖m i✝‖ ≤ b i✝

Tactic:
exacts [f.opNorm_nonneg.trans hC, hm _]

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
C : ℝ
b : ι → ℝ
hC : ‖f‖ ≤ C
hm : ∀ (i : ι), ‖m i‖ ≤ b i
⊢ ‖f‖ * ∏ i : ι, ‖m i‖ ≤ C * ∏ i : ι, b i

Tactic:
gcongr

Result:
case b0
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
C : ℝ
b : ι → ℝ
hC : ‖f‖ ≤ C
hm : ∀ (i : ι), ‖m i‖ ≤ b i
⊢ 0 ≤ C

case h₂.h1
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
C : ℝ
b : ι → ℝ
hC : ‖f‖ ≤ C
hm : ∀ (i : ι), ‖m i‖ ≤ b i
i✝ : ι
a✝ : i✝ ∈ univ
⊢ ‖m i✝‖ ≤ b i✝
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem circleIntegrable_sub_inv_iff {c w : ℂ} {R : ℝ} :
    CircleIntegrable (fun z => (z - w)⁻¹) c R ↔ R = 0 ∨ w ∉ sphere c |R|

Proof state:
c w : ℂ
R : ℝ
⊢ CircleIntegrable (fun z => (z - w)⁻¹) c R ↔ R = 0 ∨ w ∉ sphere c |R|

Tactic:
simp only [← zpow_neg_one, circleIntegrable_sub_zpow_iff]

Result:
c w : ℂ
R : ℝ
⊢ R = 0 ∨ 0 ≤ -1 ∨ w ∉ sphere c |R| ↔ R = 0 ∨ w ∉ sphere c |R|

Proof state:
c w : ℂ
R : ℝ
⊢ R = 0 ∨ 0 ≤ -1 ∨ w ∉ sphere c |R| ↔ R = 0 ∨ w ∉ sphere c |R|

Tactic:
norm_num

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem card_rootsOfUnity' {n : ℕ} [NeZero n] (h : IsPrimitiveRoot ζ n) :
    Fintype.card (rootsOfUnity n R) = n

Proof state:
R : Type u_4
inst✝² : CommRing R
ζ : Rˣ
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
⊢ Fintype.card ↥(rootsOfUnity n R) = n

Tactic:
let e := h.zmodEquivZPowers

Result:
R : Type u_4
inst✝² : CommRing R
ζ : Rˣ
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
e : ZMod n ≃+ Additive ↥(Subgroup.zpowers ζ) := h.zmodEquivZPowers
⊢ Fintype.card ↥(rootsOfUnity n R) = n

Proof state:
R : Type u_4
inst✝² : CommRing R
ζ : Rˣ
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
e : ZMod n ≃+ Additive ↥(Subgroup.zpowers ζ) := h.zmodEquivZPowers
this : Fintype ↥(Subgroup.zpowers ζ)
⊢ ↥(rootsOfUnity n R) ≃ ↥(Subgroup.zpowers ζ)

Tactic:
rw [h.zpowers_eq]

Result:
no goals

Proof state:
R : Type u_4
inst✝² : CommRing R
ζ : Rˣ
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
e : ZMod n ≃+ Additive ↥(Subgroup.zpowers ζ) := h.zmodEquivZPowers
⊢ Fintype.card ↥(rootsOfUnity n R) = n

Tactic:
have : Fintype (Subgroup.zpowers ζ) := Fintype.ofEquiv _ e.toEquiv

Result:
R : Type u_4
inst✝² : CommRing R
ζ : Rˣ
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
e : ZMod n ≃+ Additive ↥(Subgroup.zpowers ζ) := h.zmodEquivZPowers
this : Fintype ↥(Subgroup.zpowers ζ)
⊢ Fintype.card ↥(rootsOfUnity n R) = n

Proof state:
R : Type u_4
inst✝² : CommRing R
ζ : Rˣ
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
e : ZMod n ≃+ Additive ↥(Subgroup.zpowers ζ) := h.zmodEquivZPowers
this : Fintype ↥(Subgroup.zpowers ζ)
⊢ Fintype.card ↥(rootsOfUnity n R) = n

Tactic:
calc
  Fintype.card (rootsOfUnity n R) = Fintype.card (Subgroup.zpowers ζ) :=
    Fintype.card_congr <| by rw [h.zpowers_eq]
  _ = Fintype.card (ZMod n) := Fintype.card_congr e.toEquiv.symm
  _ = n := ZMod.card n

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean
theorem naturality_inv {p f g pf : C} {η : f ≅ g}
    (η_f : p ⊗ f ≅ pf) (η_g : p ⊗ g ≅ pf) (ih : p ◁ η ≪≫ η_g = η_f) :
    p ◁ η.symm ≪≫ η_f = η_g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g pf : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ η_f = η_g

Tactic:
rw [← ih]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g pf : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g = η_g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g pf : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g = η_g

Tactic:
apply Iso.ext

Result:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g pf : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g).hom = η_g.hom

Proof state:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g pf : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g).hom = η_g.hom

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a

Proof state:
α : Type u_1
a : α
inst✝ : Inhabited α
l : List α
⊢ (a :: l)[0]! = a

Tactic:
rw [getElem!_pos] <;> simp

Result:
no goals