harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean
lemma mem_homologicalKernel_iff [F.IsHomological] [F.ShiftSequence ℤ] (X : C) :
    F.homologicalKernel.P X ↔ ∀ (n : ℤ), IsZero ((F.shift n).obj X)

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X : C
⊢ F.homologicalKernel.P X ↔ ∀ (n : ℤ), IsZero ((shiftFunctor C n ⋙ F).obj X)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X : C
⊢ F.homologicalKernel.P X ↔ ∀ (n : ℤ), IsZero ((F.shift n).obj X)

Tactic:
simp only [← fun (n : ℤ) => Iso.isZero_iff ((F.isoShift n).app X)]

Result:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X : C
⊢ F.homologicalKernel.P X ↔ ∀ (n : ℤ), IsZero ((shiftFunctor C n ⋙ F).obj X)
-- Mathlib/Algebra/Group/Indicator.lean
theorem mem_range_mulIndicator {r : M} {s : Set α} {f : α → M} :
    r ∈ range (mulIndicator s f) ↔ r = 1 ∧ s ≠ univ ∨ r ∈ f '' s

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
r : M
s : Set α
f : α → M
⊢ r ∈ range (s.mulIndicator f) ↔ r = 1 ∧ s ≠ univ ∨ r ∈ f '' s

Tactic:
simp [mulIndicator, ite_eq_iff, exists_or, eq_univ_iff_forall, and_comm, or_comm,
  @eq_comm _ r 1]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Adjunction/Basic.lean
theorem right_triangle_of_left_triangle (h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv) :
    rightZigzag η.hom ε.hom = (ρ_ g).hom ≫ (λ_ g).inv

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
    rightZigzag η.hom ε.hom ⊗≫ rightZigzag η.hom ε.hom

Tactic:
bicategory

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ rightZigzag η.hom ε.hom = (ρ_ g).hom ≫ (λ_ g).inv

Tactic:
rw [← cancel_epi (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv)]

Result:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
    (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
    (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv

Tactic:
calc
  _ = rightZigzag η.hom ε.hom ⊗≫ rightZigzag η.hom ε.hom := by bicategory
  _ = rightZigzag η.hom ε.hom := rightZigzag_idempotent_of_left_triangle _ _ h
  _ = _ := by simp

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ rightZigzag η.hom ε.hom = (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem card_le_iff {o : Ordinal} {c : Cardinal} : o.card ≤ c ↔ o < (succ c).ord

Proof state:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
⊢ o.card ≤ c ↔ o < (succ c).ord

Tactic:
rw [lt_ord, lt_succ_iff]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
theorem ContinuousMultilinearMap.fin0_apply_norm (f : G[×0]→L[𝕜] G') {x : Fin 0 → G} :
    ‖f x‖ = ‖f‖

Proof state:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
m : Fin 0 → G
⊢ ‖(uncurry0 𝕜 G f.curry0) m‖ ≤ ‖f.curry0‖ * ∏ i : Fin 0, ‖m i‖

Tactic:
simp [-ContinuousMultilinearMap.apply_zero_uncurry0]

Result:
no goals

Proof state:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
⊢ ‖f 0‖ = ‖f‖

Tactic:
refine le_antisymm (by simpa using f.le_opNorm 0) ?_

Result:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
⊢ ‖f‖ ≤ ‖f 0‖

Proof state:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
x : Fin 0 → G
⊢ ‖f x‖ = ‖f‖

Tactic:
obtain rfl : x = 0 := Subsingleton.elim _ _

Result:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
⊢ ‖f 0‖ = ‖f‖

Proof state:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
this : ‖uncurry0 𝕜 G f.curry0‖ ≤ ‖f.curry0‖
⊢ ‖f‖ ≤ ‖f 0‖

Tactic:
simpa [-Matrix.zero_empty] using this

Result:
no goals

Proof state:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
⊢ ‖f 0‖ ≤ ‖f‖

Tactic:
simpa using f.le_opNorm 0

Result:
no goals

Proof state:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
⊢ ‖f‖ ≤ ‖f 0‖

Tactic:
have : ‖ContinuousMultilinearMap.uncurry0 𝕜 G f.curry0‖ ≤ ‖f.curry0‖ :=
  ContinuousMultilinearMap.opNorm_le_bound (norm_nonneg _) fun m => by
    simp [-ContinuousMultilinearMap.apply_zero_uncurry0]

Result:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
this : ‖uncurry0 𝕜 G f.curry0‖ ≤ ‖f.curry0‖
⊢ ‖f‖ ≤ ‖f 0‖
-- Mathlib/Analysis/Matrix.lean
theorem frobenius_norm_row (v : m → α) : ‖row ι v‖ = ‖(WithLp.equiv 2 _).symm v‖

Proof state:
m : Type u_3
α : Type u_5
ι : Type u_7
inst✝² : Fintype m
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ ‖row ι v‖ = ‖(WithLp.equiv 2 (m → α)).symm v‖

Tactic:
rw [frobenius_norm_def, Fintype.sum_unique, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]

Result:
m : Type u_3
α : Type u_5
ι : Type u_7
inst✝² : Fintype m
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ (∑ j : m, ‖row ι v default j‖ ^ 2) ^ (1 / 2) = (∑ i : m, ‖(WithLp.equiv 2 (m → α)).symm v i‖ ^ 2) ^ (1 / 2)

Proof state:
m : Type u_3
α : Type u_5
ι : Type u_7
inst✝² : Fintype m
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ (∑ j : m, ‖row ι v default j‖ ^ 2) ^ (1 / 2) = (∑ i : m, ‖(WithLp.equiv 2 (m → α)).symm v i‖ ^ 2) ^ (1 / 2)

Tactic:
simp only [row_apply, Real.rpow_two, WithLp.equiv_symm_pi_apply]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem vecMul_smul [Fintype n] [Monoid R] [NonUnitalNonAssocSemiring S] [DistribMulAction R S]
    [IsScalarTower R S S] (M : Matrix n m S) (b : R) (v : n → S) :
    (b • v) ᵥ* M = b • v ᵥ* M

Proof state:
case h
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst✝⁴ : Fintype n
inst✝³ : Monoid R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : DistribMulAction R S
inst✝ : IsScalarTower R S S
M : Matrix n m S
b : R
v : n → S
i : m
⊢ ((b • v) ᵥ* M) i = (b • v ᵥ* M) i

Tactic:
simp only [vecMul, dotProduct, Finset.smul_sum, Pi.smul_apply, smul_mul_assoc]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst✝⁴ : Fintype n
inst✝³ : Monoid R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : DistribMulAction R S
inst✝ : IsScalarTower R S S
M : Matrix n m S
b : R
v : n → S
⊢ (b • v) ᵥ* M = b • v ᵥ* M

Tactic:
ext i

Result:
case h
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst✝⁴ : Fintype n
inst✝³ : Monoid R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : DistribMulAction R S
inst✝ : IsScalarTower R S S
M : Matrix n m S
b : R
v : n → S
i : m
⊢ ((b • v) ᵥ* M) i = (b • v ᵥ* M) i
-- Mathlib/Order/SuccPred/Tree.lean
@[simp]
lemma findAtom_eq_bot {r : α} :
    findAtom r = ⊥ ↔ r = ⊥ where
  mp h

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : findAtom r = ⊥
⊢ r = ⊥

Tactic:
unfold findAtom at h

Result:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Order.pred^[Nat.find ⋯ - 1] r = ⊥
⊢ r = ⊥

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : r = ⊥
⊢ findAtom r = ⊥

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Order.pred^[Nat.find ⋯ - 1] r = ⊥
this : Nat.find ⋯ ≤ Nat.find ⋯ - 1
⊢ Nat.find ⋯ = 0

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Order.pred^[Nat.find ⋯ - 1] r = ⊥
this : Nat.find ⋯ ≤ Nat.find ⋯ - 1
⊢ r = ⊥

Tactic:
replace : Nat.find (bot_le (a := r)).exists_pred_iterate = 0 := by omega

Result:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Order.pred^[Nat.find ⋯ - 1] r = ⊥
this : Nat.find ⋯ = 0
⊢ r = ⊥

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Order.pred^[Nat.find ⋯ - 1] r = ⊥
this : Nat.find ⋯ = 0
⊢ r = ⊥

Tactic:
simpa [this] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Order.pred^[Nat.find ⋯ - 1] r = ⊥
⊢ r = ⊥

Tactic:
have := Nat.find_min' (bot_le (a := r)).exists_pred_iterate h

Result:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Order.pred^[Nat.find ⋯ - 1] r = ⊥
this : Nat.find ⋯ ≤ Nat.find ⋯ - 1
⊢ r = ⊥
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem exact_of_pseudo_exact (S : ShortComplex C)
    (hS : ∀ b, S.g b = 0 → ∃ a, S.f a = b) : S.Exact :=
  (S.exact_iff_kernel_ι_comp_cokernel_π_zero).2 (by
      -- If we apply `g` to the pseudoelement induced by its kernel, we get 0 (of course!).
      have : S.g (kernel.ι S.g) = 0 := apply_eq_zero_of_comp_eq_zero _ _ (kernel.condition _)
      -- By pseudo-exactness, we get a preimage.
      obtain ⟨a', ha⟩ := hS _ this
      obtain ⟨a, ha'⟩ := Quotient.exists_rep a'
      rw [← ha'] at ha
      obtain ⟨Z, r, q, _, eq, comm⟩ := Quotient.exact ha
      -- Consider the pullback of `kernel.ι (cokernel.π f)` and `kernel.ι g`.
      -- The commutative diagram given by the pseudo-equality `f a = b` induces
      -- a cone over this pullback, so we get a factorization `z`.
      obtain ⟨z, _, hz₂⟩ := @pullback.lift' _ _ _ _ _ _ (kernel.ι (cokernel.π S.f))
        (kernel.ι S.g) _ (r ≫ a.hom ≫ Abelian.factorThruImage S.f) q (by
          simp only [Category.assoc, Abelian.image.fac]
          exact comm)
      -- Let's give a name to the second pullback morphism.
      let j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g := pullback.snd _ _
      -- Since `q` is an epimorphism, in particular this means that `j` is an epimorphism.
      haveI pe : Epi j := epi_of_epi_fac hz₂
      -- But it is also a monomorphism, because `kernel.ι (cokernel.π f)` is: A kernel is
      -- always a monomorphism and the pullback of a monomorphism is a monomorphism.
      -- But mono + epi = iso, so `j` is an isomorphism.
      haveI : IsIso j := isIso_of_mono_of_epi _
      -- But then `kernel.ι g` can be expressed using all of the maps of the pullback square, and we
      -- are done.
      rw [(Iso.eq_inv_comp (asIso j)).2 pullback.condition.symm]
      simp only [Category.assoc, kernel.condition, HasZeroMorphisms.comp_zero])

Proof state:
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this✝ : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
Z : C
r : Z ⟶ ((fun g => app S.f g) a).left
q : Z ⟶ (Over.mk (kernel.ι S.g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
pe : Epi j
this : IsIso j
⊢ ((asIso j).inv ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ≫ kernel.ι (cokernel.π S.f)) ≫
      cokernel.π S.f =
    0

Tactic:
simp only [Category.assoc, kernel.condition, HasZeroMorphisms.comp_zero]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_norm_smul (hs : Balanced 𝕜 s) (r : 𝕜) (x : E) :
    gauge s (‖r‖ • x) = gauge s (r • x)

Proof state:
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
⊢ θ ∈ {r_1 | 0 < r_1 ∧ ‖r‖ • x ∈ r_1 • s} ↔ θ ∈ {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}

Tactic:
rw [@RCLike.real_smul_eq_coe_smul 𝕜]

Result:
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
⊢ θ ∈ {r_1 | 0 < r_1 ∧ ↑‖r‖ • x ∈ r_1 • s} ↔ θ ∈ {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ sInf {r_1 | 0 < r_1 ∧ ‖r‖ • x ∈ r_1 • s} = sInf {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}

Tactic:
congr with θ

Result:
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
⊢ θ ∈ {r_1 | 0 < r_1 ∧ ‖r‖ • x ∈ r_1 • s} ↔ θ ∈ {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}

Proof state:
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
⊢ θ ∈ {r_1 | 0 < r_1 ∧ ↑‖r‖ • x ∈ r_1 • s} ↔ θ ∈ {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}

Tactic:
refine and_congr_right fun hθ => (hs.smul _).smul_mem_iff ?_

Result:
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
hθ : 0 < θ
⊢ ‖↑‖r‖‖ = ‖r‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ gauge s (‖r‖ • x) = gauge s (r • x)

Tactic:
unfold gauge

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ sInf {r_1 | 0 < r_1 ∧ ‖r‖ • x ∈ r_1 • s} = sInf {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}

Proof state:
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
hθ : 0 < θ
⊢ ‖↑‖r‖‖ = ‖r‖

Tactic:
rw [RCLike.norm_ofReal, abs_norm]

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_Icc_left (f : ∀ i, α i) (i : ι) (a : α i) :
    update f i '' Icc a (f i) = Icc (update f i a) f

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Icc a (f i) = Icc (update f i a) f

Tactic:
simpa using image_update_Icc f i a (f i)

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem le_of_inf_le_sup_le (h₁ : x ⊓ z ≤ y ⊓ z) (h₂ : x ⊔ z ≤ y ⊔ z) : x ≤ y :=
  calc
    x ≤ y ⊓ z ⊔ x := le_sup_right
    _ = (y ⊔ x) ⊓ (x ⊔ z)

Proof state:
α : Type u
inst✝ : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ y ⊓ z ⊔ x = (y ⊔ x) ⊓ (x ⊔ z)

Tactic:
rw [sup_inf_right, sup_comm x]

Result:
no goals

Proof state:
α : Type u
inst✝ : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ (y ⊔ x) ⊓ (y ⊔ z) = y ⊔ x ⊓ z

Tactic:
rw [← sup_inf_left]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_map_eq_iff {f : R →+* S} {p : Polynomial R} :
    natDegree (map f p) = natDegree p ↔ f (p.leadingCoeff) ≠ 0 ∨ natDegree p = 0

Proof state:
case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

Tactic:
simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]

Result:
no goals

Proof state:
case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree ≠ 0
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

Tactic:
have h2 : p ≠ 0 := by rintro rfl; simp at h

Result:
case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree ≠ 0
h2 : p ≠ 0
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

Proof state:
case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree ≠ 0
h2 : p ≠ 0
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

Tactic:
simp_all [natDegree, WithBot.unbotD_eq_unbotD_iff]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
h : natDegree 0 ≠ 0
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree ≠ 0
⊢ p ≠ 0

Tactic:
rintro rfl

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
h : natDegree 0 ≠ 0
⊢ False

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

Tactic:
rcases eq_or_ne (natDegree p) 0 with h|h

Result:
case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree ≠ 0
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
-- Mathlib/Algebra/Regular/Basic.lean
@[simp] lemma IsRightRegular.mul_right_eq_zero_iff (hb : IsRightRegular b) : a * b = 0 ↔ a = 0

Proof state:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
ha : a = 0
⊢ a * b = 0 * b

Tactic:
rw [ha]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
⊢ a * b = 0 ↔ a = 0

Tactic:
nth_rw 1 [← zero_mul b]

Result:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
⊢ a * b = 0 * b ↔ a = 0

Proof state:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
⊢ a * b = 0 * b ↔ a = 0

Tactic:
exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_flatten {l : List (List α)} {p : α → Bool} :
    l.flatten.findIdx? p =
      (l.findIdx? (·.any p)).map
        fun i => ((l.take i).map List.length).sum +
          (l[i]?.map fun xs => xs.findIdx p).getD 0

Proof state:
case cons
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
⊢ (findIdx? p xs).or
      (Option.map (fun i => i + xs.length)
        (Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
          (findIdx? (fun x => x.any p) l))) =
    Option.map
      (fun i => (map length (take i (xs :: l))).sum + (Option.map (fun xs => findIdx p xs) (xs :: l)[i]?).getD 0)
      (if xs.any p = true then some 0 else Option.map (fun i => i + 1) (findIdx? (fun x => x.any p) l))

Tactic:
split <;> rename_i h

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
h : xs.any p = true
⊢ (findIdx? p xs).or
      (Option.map (fun i => i + xs.length)
        (Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
          (findIdx? (fun x => x.any p) l))) =
    Option.map
      (fun i => (map length (take i (xs :: l))).sum + (Option.map (fun xs => findIdx p xs) (xs :: l)[i]?).getD 0)
      (some 0)

case cons.isFalse
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
h : ¬xs.any p = true
⊢ (findIdx? p xs).or
      (Option.map (fun i => i + xs.length)
        (Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
          (findIdx? (fun x => x.any p) l))) =
    Option.map
      (fun i => (map length (take i (xs :: l))).sum + (Option.map (fun xs => findIdx p xs) (xs :: l)[i]?).getD 0)
      (Option.map (fun i => i + 1) (findIdx? (fun x => x.any p) l))

Proof state:
α : Type u_1
p : α → Bool
xs : List α
l : List (List α)
ih :
  findIdx? p l.flatten =
    Option.map (fun i => (map length (take i l)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)
h : ¬xs.any p = true
⊢ (findIdx? p xs).isNone = true

Tactic:
simp_all [findIdx?_isNone]

Result:
no goals