harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/ModEq.lean
theorem add_div {a b c : ℕ} (hc0 : 0 < c) :
    (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0

Proof state:
a b c : ℕ
hc0 : 0 < c
⊢ a + (b + ((a + b) % c + if c ≤ a % c + b % c then c else 0)) =
    (a + b + if c ≤ a % c + b % c then c * 1 else c * 0) + (a + b) % c

Tactic:
simp only [mul_one, mul_zero]

Result:
a b c : ℕ
hc0 : 0 < c
⊢ a + (b + ((a + b) % c + if c ≤ a % c + b % c then c else 0)) =
    (a + b + if c ≤ a % c + b % c then c else 0) + (a + b) % c

Proof state:
a b c : ℕ
hc0 : 0 < c
⊢ a + (b + ((a + b) % c + if c ≤ a % c + b % c then c else 0)) =
    (a + b + if c ≤ a % c + b % c then c else 0) + (a + b) % c

Tactic:
ac_rfl

Result:
no goals

Proof state:
a b c : ℕ
hc0 : 0 < c
⊢ (a + b) % c + c * ((a + b) / c) + a % c + b % c =
    (a % c + c * (a / c) + (b % c + c * (b / c)) + c * if c ≤ a % c + b % c then 1 else 0) + (a + b) % c

Tactic:
rw [mod_add_div, mod_add_div, mod_add_div, mul_ite, add_assoc, add_assoc]

Result:
a b c : ℕ
hc0 : 0 < c
⊢ a + (b + (a % c + b % c)) = (a + b + if c ≤ a % c + b % c then c * 1 else c * 0) + (a + b) % c

Proof state:
a b c : ℕ
hc0 : 0 < c
⊢ (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0

Tactic:
rw [← mul_right_inj' hc0.ne', ← @add_left_cancel_iff _ _ _ ((a + b) % c + a % c + b % c)]

Result:
a b c : ℕ
hc0 : 0 < c
⊢ (a + b) % c + a % c + b % c + c * ((a + b) / c) =
    (a + b) % c + a % c + b % c + c * (a / c + b / c + if c ≤ a % c + b % c then 1 else 0)

Proof state:
a b c : ℕ
hc0 : 0 < c
⊢ a + (b + (a % c + b % c)) = (a + b + if c ≤ a % c + b % c then c * 1 else c * 0) + (a + b) % c

Tactic:
conv_lhs => rw [← add_mod_add_ite]

Result:
a b c : ℕ
hc0 : 0 < c
⊢ a + (b + ((a + b) % c + if c ≤ a % c + b % c then c else 0)) =
    (a + b + if c ≤ a % c + b % c then c * 1 else c * 0) + (a + b) % c

Proof state:
a b c : ℕ
hc0 : 0 < c
⊢ (a + b) % c + a % c + b % c + c * ((a + b) / c) =
    (a + b) % c + a % c + b % c + c * (a / c + b / c + if c ≤ a % c + b % c then 1 else 0)

Tactic:
suffices
  (a + b) % c + c * ((a + b) / c) + a % c + b % c =
    (a % c + c * (a / c) + (b % c + c * (b / c)) + c * if c ≤ a % c + b % c then 1 else 0) +
      (a + b) % c
  by simpa only [mul_add, add_comm, add_left_comm, add_assoc]

Result:
a b c : ℕ
hc0 : 0 < c
⊢ (a + b) % c + c * ((a + b) / c) + a % c + b % c =
    (a % c + c * (a / c) + (b % c + c * (b / c)) + c * if c ≤ a % c + b % c then 1 else 0) + (a + b) % c

Proof state:
a b c : ℕ
hc0 : 0 < c
this :
  (a + b) % c + c * ((a + b) / c) + a % c + b % c =
    (a % c + c * (a / c) + (b % c + c * (b / c)) + c * if c ≤ a % c + b % c then 1 else 0) + (a + b) % c
⊢ (a + b) % c + a % c + b % c + c * ((a + b) / c) =
    (a + b) % c + a % c + b % c + c * (a / c + b / c + if c ≤ a % c + b % c then 1 else 0)

Tactic:
simpa only [mul_add, add_comm, add_left_comm, add_assoc]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem balance1_eq {l : RBNode α} {v : α} {r : RBNode α}
    (hl : l.Balanced c n) : balance1 l v r = node black l v r

Proof state:
α : Type u_1
c : RBColor
n : Nat
l : RBNode α
v : α
r : RBNode α
hl : l.Balanced c n
⊢ (match l, v, r with
    | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d)
    | node red a x (node red b y c), z, d => node red (node black a x b) y (node black c z d)
    | a, x, b => node black a x b) =
    node black l v r

Tactic:
split <;> first | rfl | nomatch hl

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
n : Nat
l : RBNode α
v : α
r : RBNode α
hl : l.Balanced c n
⊢ l.balance1 v r = node black l v r

Tactic:
unfold balance1

Result:
α : Type u_1
c : RBColor
n : Nat
l : RBNode α
v : α
r : RBNode α
hl : l.Balanced c n
⊢ (match l, v, r with
    | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d)
    | node red a x (node red b y c), z, d => node red (node black a x b) y (node black c z d)
    | a, x, b => node black a x b) =
    node black l v r

Proof state:
case h_3
α : Type u_1
c : RBColor
n : Nat
l : RBNode α
v : α
r : RBNode α
hl : l.Balanced c n
x✝⁴ : RBNode α
x✝³ : α
x✝² : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α), l = node red (node red a x b) y c → False
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α), l = node red a x (node red b y c) → False
⊢ node black l v r = node black l v r

Tactic:
rfl

Result:
no goals

Proof state:
case h_2
α : Type u_1
c : RBColor
n : Nat
v : α
r x✝⁴ : RBNode α
x✝³ : α
x✝² a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), a✝ = node red a x b → False
hl : (node red a✝ x✝¹ (node red b✝ y✝ c✝)).Balanced c n
⊢ node red (node black a✝ x✝¹ b✝) y✝ (node black c✝ v r) = node black (node red a✝ x✝¹ (node red b✝ y✝ c✝)) v r

Tactic:
nomatch hl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma IsCycle.ne_bot : ∀ {p : G.Walk u u}, p.IsCycle → G ≠ ⊥
  | nil, hp => by cases hp.ne_nil rfl
  | cons h _, hp => by rintro rfl; exact h

Proof state:
V : Type u
u v✝ : V
h : ⊥.Adj u v✝
p✝ : ⊥.Walk v✝ u
hp : (cons h p✝).IsCycle
⊢ False

Tactic:
exact h

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
hp : nil.IsCycle
⊢ G ≠ ⊥

Tactic:
cases hp.ne_nil rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p✝ : G.Walk v✝ u
hp : (cons h p✝).IsCycle
⊢ G ≠ ⊥

Tactic:
rintro rfl

Result:
V : Type u
u v✝ : V
h : ⊥.Adj u v✝
p✝ : ⊥.Walk v✝ u
hp : (cons h p✝).IsCycle
⊢ False
-- Mathlib/LinearAlgebra/Dual.lean
theorem toDual_toDual : b.dualBasis.toDual.comp b.toDual = Dual.eval R M

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ ((b.dualBasis.toDual ∘ₗ b.toDual) (b i)) (b.dualBasis j) = ((Dual.eval R M) (b i)) (b.dualBasis j)

Tactic:
rw [LinearMap.comp_apply, toDual_apply_left, coe_toDual_self, ← coe_dualBasis,
  Dual.eval_apply, Basis.repr_self, Finsupp.single_apply, dualBasis_apply_self]

Result:
no goals

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
⊢ b.dualBasis.toDual ∘ₗ b.toDual = Dual.eval R M

Tactic:
refine b.ext fun i => b.dualBasis.ext fun j => ?_

Result:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ ((b.dualBasis.toDual ∘ₗ b.toDual) (b i)) (b.dualBasis j) = ((Dual.eval R M) (b i)) (b.dualBasis j)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_congr {xs ys : Vector α n} (w : xs = ys)
    (f : (i : Nat) → α → (h : i < n) → β) :
    mapFinIdx xs f = mapFinIdx ys f

Proof state:
α : Type u_1
n : Nat
β : Type u_2
xs ys : Vector α n
w : xs = ys
f : (i : Nat) → α → i < n → β
⊢ xs.mapFinIdx f = ys.mapFinIdx f

Tactic:
subst w

Result:
α : Type u_1
n : Nat
β : Type u_2
xs : Vector α n
f : (i : Nat) → α → i < n → β
⊢ xs.mapFinIdx f = xs.mapFinIdx f

Proof state:
α : Type u_1
n : Nat
β : Type u_2
xs : Vector α n
f : (i : Nat) → α → i < n → β
⊢ xs.mapFinIdx f = xs.mapFinIdx f

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Inv.lean
theorem derivWithin_div (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x)
    (hx : d x ≠ 0) :
    derivWithin (fun x => c x / d x) s x =
      (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2

Proof state:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x => c x / d x) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2

Tactic:
exact (hc.hasDerivWithinAt.div hd.hasDerivWithinAt hx).derivWithin hxs

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
⊢ derivWithin (fun x => c x / d x) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x => c x / d x) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2

case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun x => c x / d x) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2

Proof state:
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun x => c x / d x) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/LeftDerived.lean
/-- The higher derived functors vanish on projective objects. -/
lemma Functor.isZero_leftDerived_obj_projective_succ
    (F : C ⥤ D) [F.Additive] (n : ℕ) (X : C) [Projective X] :
    IsZero ((F.leftDerived (n + 1)).obj X)

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Projective X
⊢ IsZero ((F.leftDerived (n + 1)).obj X)

Tactic:
refine IsZero.of_iso ?_ ((ProjectiveResolution.self X).isoLeftDerivedObj F (n + 1))

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Projective X
⊢ IsZero
    ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) (n + 1)).obj
      ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (ProjectiveResolution.self X).complex))

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Projective X
⊢ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (ProjectiveResolution.self X).complex).ExactAt (n + 1)

Tactic:
exact ShortComplex.exact_of_isZero_X₂ _ (F.map_isZero (by apply isZero_zero))

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Projective X
⊢ IsZero
    ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) (n + 1)).obj
      ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (ProjectiveResolution.self X).complex))

Tactic:
erw [← HomologicalComplex.exactAt_iff_isZero_homology]

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Projective X
⊢ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (ProjectiveResolution.self X).complex).ExactAt (n + 1)

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Projective X
⊢ IsZero ((ProjectiveResolution.self X).complex.X (n + 1))

Tactic:
apply isZero_zero

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem map_eq_comap {p : Submodule R M} :
    (p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂) = p.comap (e.symm : M₂ →ₛₗ[σ₂₁] M) :=
  SetLike.coe_injective <| by simp [e.image_eq_preimage]

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝³ : Semiring R
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
⊢ ↑(Submodule.map (↑e) p) = ↑(Submodule.comap (↑e.symm) p)

Tactic:
simp [e.image_eq_preimage]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem _root_.Function.Injective.injOn_range (h : Injective (g ∘ f)) : InjOn g (range f)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
h : Injective (g ∘ f)
x y : α
H : g (f x) = g (f y)
⊢ f x = f y

Tactic:
exact congr_arg f (h H)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
h : Injective (g ∘ f)
⊢ InjOn g (range f)

Tactic:
rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ H

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
h : Injective (g ∘ f)
x y : α
H : g (f x) = g (f y)
⊢ f x = f y
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma leadingCoeff_preΨ' {n : ℕ} (h : (n : R) ≠ 0) :
    (W.preΨ' n).leadingCoeff = if Even n then n / 2 else n

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑n ≠ 0
⊢ (W.preΨ' n).leadingCoeff = ↑(if Even n then n / 2 else n)

Tactic:
rw [leadingCoeff, W.natDegree_preΨ' h, coeff_preΨ']

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem _root_.Fin.edist_append_eq_max_edist (m n : ℕ) {x x2 : Fin m → α} {y y2 : Fin n → α} :
    edist (Fin.append x y) (Fin.append x2 y2) = max (edist x x2) (edist y y2)

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
m n : ℕ
x x2 : Fin m → α
y y2 : Fin n → α
⊢ edist (Fin.append x y) (Fin.append x2 y2) = edist x x2 ⊔ edist y y2

Tactic:
simp [edist_pi_def, Finset.sup_univ_eq_iSup, ← Equiv.iSup_comp (e := finSumFinEquiv),
  Prod.edist_eq, iSup_sum]

Result:
no goals
-- Mathlib/RingTheory/WittVector/InitTail.lean
theorem init_zsmul (m : ℤ) (x : 𝕎 R) (n : ℕ) : init n (m • x) = init n (m • init n x)

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℤ
x : 𝕎 R
n : ℕ
⊢ init n (m • x) = init n (m • init n x)

Tactic:
init_ring using fun p [Fact (Nat.Prime p)] n => wittZSMul_vars p m n

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Constructions.lean
@[to_additive pi_norm_le_iff_of_nonempty]
lemma pi_norm_le_iff_of_nonempty' [Nonempty ι] : ‖f‖ ≤ r ↔ ∀ b, ‖f b‖ ≤ r

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedGroup (π i)
f : (i : ι) → π i
r : ℝ
inst✝ : Nonempty ι
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

Tactic:
by_cases hr : 0 ≤ r

Result:
case pos
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedGroup (π i)
f : (i : ι) → π i
r : ℝ
inst✝ : Nonempty ι
hr : 0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

case neg
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedGroup (π i)
f : (i : ι) → π i
r : ℝ
inst✝ : Nonempty ι
hr : ¬0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

Proof state:
case pos
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedGroup (π i)
f : (i : ι) → π i
r : ℝ
inst✝ : Nonempty ι
hr : 0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

Tactic:
exact pi_norm_le_iff_of_nonneg' hr

Result:
no goals

Proof state:
case neg
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedGroup (π i)
f : (i : ι) → π i
r : ℝ
inst✝ : Nonempty ι
hr : ¬0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

Tactic:
exact
  iff_of_false (fun h => hr <| (norm_nonneg' _).trans h) fun h =>
    hr <| (norm_nonneg' _).trans <| h <| Classical.arbitrary _

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_relabel {m n : ℕ} {φ : L.BoundedFormula α n} {g : α → β ⊕ (Fin m)} {v : β → M}
    {xs : Fin (m + n) → M} :
    (φ.relabel g).Realize v xs ↔
      φ.Realize (Sum.elim v (xs ∘ Fin.castAdd n) ∘ g) (xs ∘ Fin.natAdd m)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
m n : ℕ
φ : L.BoundedFormula α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
⊢ (relabel g φ).Realize v xs ↔ φ.Realize (Sum.elim v (xs ∘ castAdd n) ∘ g) (xs ∘ natAdd m)

Tactic:
apply realize_mapTermRel_add_castLe <;> simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_insert_right (h : a < b) : insert b (Ioo a b) = Ioc a b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a < b
⊢ insert b (Ioo a b) = Ioc a b

Tactic:
rw [insert_eq, union_comm, Ioo_union_right h]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
@[simp]
lemma detp_one_one : detp 1 (1 : Matrix n n R) = 1

Proof state:
case h
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ 1 ∈ ofSign 1

Tactic:
simp [ofSign]

Result:
no goals

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ ∏ k : n, 1 k (1 k) = 1

Tactic:
simp [one_apply]

Result:
no goals

Proof state:
case h₀
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ ∀ b ∈ ofSign 1, b ≠ 1 → ∏ k : n, 1 k (b k) = 0

Tactic:
rintro σ - hσ1

Result:
case h₀
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ1 : σ ≠ 1
⊢ ∏ k : n, 1 k (σ k) = 0

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ detp 1 1 = 1

Tactic:
rw [detp, sum_eq_single_of_mem 1]

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ ∏ k : n, 1 k (1 k) = 1

case h
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ 1 ∈ ofSign 1

case h₀
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ ∀ b ∈ ofSign 1, b ≠ 1 → ∏ k : n, 1 k (b k) = 0

Proof state:
case h₀.intro
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ1 : σ ≠ 1
i : n
hi : ¬σ i = 1 i
⊢ ∏ k : n, 1 k (σ k) = 0

Tactic:
exact prod_eq_zero (mem_univ i) (one_apply_ne' hi)

Result:
no goals

Proof state:
case h₀
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ1 : σ ≠ 1
⊢ ∏ k : n, 1 k (σ k) = 0

Tactic:
obtain ⟨i, hi⟩ := not_forall.mp (mt Perm.ext_iff.mpr hσ1)

Result:
case h₀.intro
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ1 : σ ≠ 1
i : n
hi : ¬σ i = 1 i
⊢ ∏ k : n, 1 k (σ k) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.isEmpty = true → m.getKey? a = none

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
⊢ m.isEmpty = true → m.getKey? a = none

Tactic:
simp_to_raw using Raw₀.getKey?_of_isEmpty ⟨m, _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem isSuffixOf_nil_left [BEq α] : isSuffixOf ([] : List α) l = true

Proof state:
α : Type u
l : List α
inst✝ : BEq α
⊢ nil.isSuffixOf l = true

Tactic:
simp [isSuffixOf]

Result:
no goals
-- Mathlib/RingTheory/Nullstellensatz.lean
theorem vanishingIdeal_pointToPoint (V : Set (σ → k)) :
    PrimeSpectrum.vanishingIdeal (pointToPoint '' V) = MvPolynomial.vanishingIdeal V :=
  le_antisymm
    (fun _ hp x hx =>
      (((PrimeSpectrum.mem_vanishingIdeal _ _).1 hp) ⟨vanishingIdeal {x}, by infer_instance⟩ <| by
          exact ⟨x, ⟨hx, rfl⟩⟩) -- Porting note: tactic mode code compiles but term mode does not
        x rfl)
    fun _ hp =>
    (PrimeSpectrum.mem_vanishingIdeal _ _).2 fun _ hI =>
      let ⟨x, hx⟩ := hI
      hx.2 ▸ fun _ hx' => (Set.mem_singleton_iff.1 hx').symm ▸ hp x hx.1

Proof state:
k : Type u_1
inst✝ : Field k
σ : Type u_2
V : Set (σ → k)
x✝ : MvPolynomial σ k
hp : x✝ ∈ PrimeSpectrum.vanishingIdeal (pointToPoint '' V)
x : σ → k
hx : x ∈ V
⊢ (vanishingIdeal {x}).IsPrime

Tactic:
infer_instance

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
σ : Type u_2
V : Set (σ → k)
x✝ : MvPolynomial σ k
hp : x✝ ∈ PrimeSpectrum.vanishingIdeal (pointToPoint '' V)
x : σ → k
hx : x ∈ V
⊢ { asIdeal := vanishingIdeal {x}, isPrime := ⋯ } ∈ pointToPoint '' V

Tactic:
exact ⟨x, ⟨hx, rfl⟩⟩

Result:
no goals
-- Mathlib/RingTheory/Finiteness/TensorProduct.lean
lemma Module.exists_isPrincipal_quotient_of_finite  :
    ∃ N : Submodule R M, N ≠ ⊤ ∧ Submodule.IsPrincipal (⊤ : Submodule R (M ⧸ N))

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal

Tactic:
have hs := Nat.sSup_mem hs₁ hs₂

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' (Fin.val ⁻¹' Set.Iio m)) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal