harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/GDelta/Basic.lean
/-- The empty set is nowhere dense. -/
@[simp]
lemma isNowhereDense_empty : IsNowhereDense (∅ : Set X)

Proof state:
X : Type u_5
inst✝ : TopologicalSpace X
⊢ IsNowhereDense ∅

Tactic:
rw [IsNowhereDense, closure_empty, interior_empty]

Result:
no goals
-- Mathlib/CategoryTheory/IsConnected.lean
theorem IsPreconnected.of_constant_of_preserves_morphisms
    (h : ∀ {α : Type u₁} (F : J → α),
      (∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ j j' : J, F j = F j') :
    IsPreconnected J :=
  IsPreconnected.of_any_functor_const_on_obj fun F =>
    h F.obj fun f => by ext; exact Discrete.eq_of_hom (F.map f)

Proof state:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
α✝ : Type u₁
F : J ⥤ Discrete α✝
j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ F.obj j₁✝ = F.obj j₂✝

Tactic:
ext

Result:
case as
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
α✝ : Type u₁
F : J ⥤ Discrete α✝
j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ (F.obj j₁✝).as = (F.obj j₂✝).as

Proof state:
case as
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
α✝ : Type u₁
F : J ⥤ Discrete α✝
j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ (F.obj j₁✝).as = (F.obj j₂✝).as

Tactic:
exact Discrete.eq_of_hom (F.map f)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem balance2_All {l : RBNode α} {v : α} {r : RBNode α} :
    (balance2 l v r).All p ↔ p v ∧ l.All p ∧ r.All p

Proof state:
α : Type u_1
p : α → Prop
l : RBNode α
v : α
r : RBNode α
⊢ All p (l.balance2 v r) ↔ p v ∧ All p l ∧ All p r

Tactic:
unfold balance2

Result:
α : Type u_1
p : α → Prop
l : RBNode α
v : α
r : RBNode α
⊢ All p
      (match l, v, r with
      | a, x, node red b y (node red c z d) => node red (node black a x b) y (node black c z d)
      | a, x, node red (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) ↔
    p v ∧ All p l ∧ All p r

Proof state:
α : Type u_1
p : α → Prop
l : RBNode α
v : α
r : RBNode α
⊢ All p
      (match l, v, r with
      | a, x, node red b y (node red c z d) => node red (node black a x b) y (node black c z d)
      | a, x, node red (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) ↔
    p v ∧ All p l ∧ All p r

Tactic:
split <;> simp [and_assoc, and_left_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean
@[reassoc (attr := simp)]
lemma φ_π : φ f g ≫ π f g = 0

Proof state:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inr ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inr ≫ 0

Tactic:
simp

Result:
no goals

Proof state:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inl ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inl ≫ 0

Tactic:
rw [biprod.inl_desc_assoc, assoc, biprod.inl_desc, comp_zero,
  ← assoc, cokernel.condition]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ φ f g ≫ π f g = 0

Tactic:
dsimp [φ, π]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) = 0

Tactic:
ext

Result:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inl ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inl ≫ 0

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inr ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inr ≫ 0
-- Mathlib/Algebra/Lie/Engel.lean
theorem exists_smul_add_of_span_sup_eq_top (y : L) : ∃ t : R, ∃ z ∈ I, y = t • x + z

Proof state:
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
y : L
⊢ ∃ t, ∃ z ∈ I, y = t • x + z

Tactic:
have hy : y ∈ (⊤ : Submodule R L) := Submodule.mem_top

Result:
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
y : L
hy : y ∈ ⊤
⊢ ∃ t, ∃ z ∈ I, y = t • x + z

Proof state:
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
y : L
hy : ∃ y_1, (∃ a, a • x = y_1) ∧ ∃ z ∈ (LieIdeal.toLieSubalgebra R L I).toSubmodule, y_1 + z = y
⊢ ∃ t, ∃ z ∈ I, y = t • x + z

Tactic:
obtain ⟨-, ⟨t, rfl⟩, z, hz, rfl⟩ := hy

Result:
case intro.intro.intro.intro.intro
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
t : R
z : L
hz : z ∈ (LieIdeal.toLieSubalgebra R L I).toSubmodule
⊢ ∃ t_1, ∃ z_1 ∈ I, t • x + z = t_1 • x + z_1

Proof state:
case intro.intro.intro.intro.intro
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
t : R
z : L
hz : z ∈ (LieIdeal.toLieSubalgebra R L I).toSubmodule
⊢ ∃ t_1, ∃ z_1 ∈ I, t • x + z = t_1 • x + z_1

Tactic:
exact ⟨t, z, hz, rfl⟩

Result:
no goals

Proof state:
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
y : L
hy : y ∈ ⊤
⊢ ∃ t, ∃ z ∈ I, y = t • x + z

Tactic:
simp only [← hxI, Submodule.mem_sup, Submodule.mem_span_singleton] at hy

Result:
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
y : L
hy : ∃ y_1, (∃ a, a • x = y_1) ∧ ∃ z ∈ (LieIdeal.toLieSubalgebra R L I).toSubmodule, y_1 + z = y
⊢ ∃ t, ∃ z ∈ I, y = t • x + z
-- Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
@[reassoc (attr := simp)]
lemma biprod_inr_desc_f (α : K ⟶ M) (β : L ⟶ M) (i : ι) :
    (biprod.inr : L ⟶ K ⊞ L).f i ≫ (biprod.desc α β).f i = β.f i

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
M : HomologicalComplex C c
α : K ⟶ M
β : L ⟶ M
i : ι
⊢ biprod.inr.f i ≫ (biprod.desc α β).f i = β.f i

Tactic:
rw [← comp_f, biprod.inr_desc]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem Bornology.IsBounded.mul (hs : IsBounded s) (ht : IsBounded t) : IsBounded (s * t)

Proof state:
case intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
⊢ IsBounded (s * t)

Tactic:
refine isBounded_iff_forall_norm_le'.2 ⟨Rs + Rt, ?_⟩

Result:
case intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
⊢ ∀ x ∈ s * t, ‖x‖ ≤ Rs + Rt

Proof state:
case intro
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
⊢ IsBounded (s * t)

Tactic:
obtain ⟨Rt, hRt⟩ : ∃ R, ∀ x ∈ t, ‖x‖ ≤ R := ht.exists_norm_le'

Result:
case intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
⊢ IsBounded (s * t)

Proof state:
case intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
⊢ ∀ x ∈ s * t, ‖x‖ ≤ Rs + Rt

Tactic:
rintro z ⟨x, hx, y, hy, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
x : E
hx : x ∈ s
y : E
hy : y ∈ t
⊢ ‖(fun x1 x2 => x1 * x2) x y‖ ≤ Rs + Rt

Proof state:
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
x : E
hx : x ∈ s
y : E
hy : y ∈ t
⊢ ‖(fun x1 x2 => x1 * x2) x y‖ ≤ Rs + Rt

Tactic:
exact norm_mul_le_of_le' (hRs x hx) (hRt y hy)

Result:
no goals

Proof state:
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
⊢ IsBounded (s * t)

Tactic:
obtain ⟨Rs, hRs⟩ : ∃ R, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le'

Result:
case intro
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
⊢ IsBounded (s * t)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma neg_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W'.neg P ≈ W'.neg Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.neg P ≈ W'.neg Q

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
Q : Fin 3 → R
u : Rˣ
⊢ W'.neg ((fun m => m • Q) u) ≈ W'.neg Q

Proof state:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
Q : Fin 3 → R
u : Rˣ
⊢ W'.neg ((fun m => m • Q) u) ≈ W'.neg Q

Tactic:
exact neg_smul_equiv Q u.isUnit

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem decomp (f : V1 →ᵃ[k] V2) : (f : V1 → V2) = ⇑f.linear + fun _ => f 0

Proof state:
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
⊢ ⇑f = ⇑f.linear + fun x => f 0

Tactic:
ext x

Result:
case h
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
x : V1
⊢ f x = (⇑f.linear + fun x => f 0) x

Proof state:
case h
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
x : V1
⊢ f x = (⇑f.linear + fun x => f 0) x

Tactic:
calc
  f x = f.linear x +ᵥ f 0 := by rw [← f.map_vadd, vadd_eq_add, add_zero]
  _ = (f.linear + fun _ : V1 => f 0) x := rfl

Result:
no goals

Proof state:
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
x : V1
⊢ f x = f.linear x +ᵥ f 0

Tactic:
rw [← f.map_vadd, vadd_eq_add, add_zero]

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem log_natCast (b : ℕ) (n : ℕ) : log b (n : R) = Nat.log b n

Proof state:
case zero
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ log b ↑0 = ↑(Nat.log b 0)

Tactic:
simp [log_of_right_le_one]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ log b ↑(n✝ + 1) = ↑(Nat.log b (n✝ + 1))

Tactic:
rw [log_of_one_le_right, Nat.floor_natCast]

Result:
case succ.hr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ 1 ≤ ↑(n✝ + 1)

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ log b ↑n = ↑(Nat.log b n)

Tactic:
cases n

Result:
case zero
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ log b ↑0 = ↑(Nat.log b 0)

case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ log b ↑(n✝ + 1) = ↑(Nat.log b (n✝ + 1))

Proof state:
case succ.hr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ 1 ≤ ↑(n✝ + 1)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem two_lt_ncard_iff (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ 2 < s.ncard ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_rw [ncard_eq_toFinset_card _ hs, Finset.two_lt_card_iff, Finite.mem_toFinset]

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem root_isInv (r : R) : of _ r * root (C r * X - 1) = 1

Proof state:
R : Type u
inst✝ : CommRing R
r : R
⊢ (of (C r * X - 1)) r * root (C r * X - 1) = 1

Tactic:
convert sub_eq_zero.1 ((eval₂_sub _).symm.trans <| eval₂_root <| C r * X - 1) <;>
  simp only [eval₂_mul, eval₂_C, eval₂_X, eval₂_one]

Result:
no goals
-- Mathlib/Data/Finset/PImage.lean
theorem pimage_subset {t : Finset β} : s.pimage f ⊆ t ↔ ∀ x ∈ s, ∀ y ∈ f x, y ∈ t

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
s : Finset α
t : Finset β
⊢ pimage f s ⊆ t ↔ ∀ x ∈ s, ∀ y ∈ f x, y ∈ t

Tactic:
simp [subset_iff, @forall_swap _ β]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_eq_zero_iff_of_nonneg (hx : 0 ≤ x) : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Proof state:
x y : ℝ
hx : 0 ≤ x
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp only [rpow_def_of_nonneg hx]

Result:
x y : ℝ
hx : 0 ≤ x
⊢ (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0

Proof state:
x y : ℝ
hx : 0 ≤ x
⊢ (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
split_ifs <;> simp [*, exp_ne_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
theorem pullback_fst_of_right (hP' : Q.IsStableUnderBaseChange)
    {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsAffine S] (H : Q g) :
    P (pullback.fst f g)

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : IsAffine S
H : Q g
this : Q.IsLocal := isLocal_affineProperty P
⊢ P (pullback.fst f g)

Tactic:
rw [iff_of_openCover (P := P) X.affineCover]

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : IsAffine S
H : Q g
this : Q.IsLocal := isLocal_affineProperty P
⊢ ∀ (i : X.affineCover.1), Q (Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i)
-- Mathlib/Data/Finset/Max.lean
theorem max_eq_bot {s : Finset α} : s.max = ⊥ ↔ s = ∅ :=
  ⟨fun h ↦ s.eq_empty_or_nonempty.elim id fun H ↦ by
      obtain ⟨a, ha⟩ := max_of_nonempty H
      rw [h] at ha; cases ha; , -- the `;` is needed since the `cases` syntax allows `cases a, b`
    fun h ↦ h.symm ▸ max_empty⟩

Proof state:
case intro
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
a : α
ha : ⊥ = ↑a
⊢ s = ∅

Tactic:
cases ha

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
⊢ s = ∅

Tactic:
obtain ⟨a, ha⟩ := max_of_nonempty H

Result:
case intro
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
a : α
ha : s.max = ↑a
⊢ s = ∅

Proof state:
case intro
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
a : α
ha : s.max = ↑a
⊢ s = ∅

Tactic:
rw [h] at ha

Result:
case intro
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
a : α
ha : ⊥ = ↑a
⊢ s = ∅
-- Mathlib/RingTheory/AdicCompletion/Basic.lean
theorem subsingleton (h : IsHausdorff (⊤ : Ideal R) M) : Subsingleton M :=
  ⟨fun x y => eq_of_sub_eq_zero <| h.haus (x - y) fun n => by
    rw [Ideal.top_pow, top_smul]
    exact SModEq.top⟩

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsHausdorff ⊤ M
x y : M
n : ℕ
⊢ x - y ≡ 0 [SMOD ⊤ ^ n • ⊤]

Tactic:
rw [Ideal.top_pow, top_smul]

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsHausdorff ⊤ M
x y : M
n : ℕ
⊢ x - y ≡ 0 [SMOD ⊤]

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsHausdorff ⊤ M
x y : M
n : ℕ
⊢ x - y ≡ 0 [SMOD ⊤]

Tactic:
exact SModEq.top

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma apply_le_nnnorm_cfc_nnreal (f : ℝ≥0 → ℝ≥0) (a : A) ⦃x : ℝ≥0⦄ (hx : x ∈ σ ℝ≥0 a)
    (hf : ContinuousOn f (σ ℝ≥0 a)

Proof state:
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
x : ℝ≥0
hx : x ∈ σ ℝ≥0 a
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
⊢ f x ≤ ‖cfc f a‖₊

Tactic:
revert hx

Result:
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
x : ℝ≥0
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
⊢ x ∈ σ ℝ≥0 a → f x ≤ ‖cfc f a‖₊

Proof state:
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
x : ℝ≥0
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
⊢ x ∈ σ ℝ≥0 a → f x ≤ ‖cfc f a‖₊

Tactic:
nontriviality A

Result:
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
x : ℝ≥0
hf : autoParam (ContinuousOn f (σ ℝ≥0 a)) _auto✝
ha : autoParam (0 ≤ a) _auto✝
a✝ : Nontrivial A
⊢ x ∈ σ ℝ≥0 a → f x ≤ ‖cfc f a‖₊
-- Mathlib/Data/Complex/Basic.lean
theorem inv_im (z : ℂ) : z⁻¹.im = -z.im / normSq z

Proof state:
z : ℂ
⊢ z⁻¹.im = -z.im / normSq z

Tactic:
simp [inv_def, division_def, ofReal]

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem isPath_cons {xs : Path F} {a a'} {f : F.B a → M F} {i : F.B a'} :
    IsPath (⟨a', i⟩ :: xs) (M.mk ⟨a, f⟩) → a = a'

Proof state:
F : PFunctor.{u}
xs : Path F
a a' : F.A
f : F.B a → F.M
i : F.B a'
⊢ IsPath (⟨a', i⟩ :: xs) (M.mk ⟨a, f⟩) → a = a'

Tactic:
generalize h : M.mk ⟨a, f⟩ = x

Result:
F : PFunctor.{u}
xs : Path F
a a' : F.A
f : F.B a → F.M
i : F.B a'
x : F.M
h : M.mk ⟨a, f⟩ = x
⊢ IsPath (⟨a', i⟩ :: xs) x → a = a'

Proof state:
case cons.refl
F : PFunctor.{u}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
a✝ : IsPath xs (f i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a, f⟩
⊢ a = a

Tactic:
rfl

Result:
no goals

Proof state:
F : PFunctor.{u}
xs : Path F
a a' : F.A
f : F.B a → F.M
i : F.B a'
x : F.M
h : M.mk ⟨a, f⟩ = x
⊢ IsPath (⟨a', i⟩ :: xs) x → a = a'

Tactic:
rintro (_ | ⟨_, _, _, _, rfl, _⟩)

Result:
case cons
F : PFunctor.{u}
xs : Path F
a a' : F.A
f : F.B a → F.M
i : F.B a'
f✝ : F.B a' → F.M
a✝ : IsPath xs (f✝ i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a', f✝⟩
⊢ a = a'

Proof state:
case cons
F : PFunctor.{u}
xs : Path F
a a' : F.A
f : F.B a → F.M
i : F.B a'
f✝ : F.B a' → F.M
a✝ : IsPath xs (f✝ i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a', f✝⟩
⊢ a = a'

Tactic:
cases mk_inj h

Result:
case cons.refl
F : PFunctor.{u}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
a✝ : IsPath xs (f i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a, f⟩
⊢ a = a
-- Mathlib/Logic/Equiv/Basic.lean
theorem piCongrLeft_sumInr {ι ι' ι''} (π : ι'' → Type*) (e : ι ⊕ ι' ≃ ι'') (f : ∀ i, π (e (inl i)))
    (g : ∀ i, π (e (inr i))) (j : ι') :
    piCongrLeft π e (sumPiEquivProdPi (fun x => π (e x)) |>.symm (f, g)) (e (inr j)) = g j

Proof state:
ι : Type u_10
ι' : Type u_11
ι'' : Sort u_12
π : ι'' → Type u_9
e : ι ⊕ ι' ≃ ι''
f : (i : ι) → π (e (inl i))
g : (i : ι') → π (e (inr i))
j : ι'
⊢ (piCongrLeft π e) ((sumPiEquivProdPi fun x => π (e x)).symm (f, g)) (e (inr j)) = g j

Tactic:
simp_rw [piCongrLeft_apply_eq_cast, sumPiEquivProdPi_symm_apply,
  sum_rec_congr _ _ _ (e.symm_apply_apply (inr j)), cast_cast, cast_eq]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem rightMoves_nim (o : Ordinal) : (nim o).RightMoves = o.toType

Proof state:
o : Ordinal.{u_1}
⊢ (mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)).RightMoves =
    o.toType

Tactic:
rfl

Result:
no goals

Proof state:
o : Ordinal.{u_1}
⊢ (nim o).RightMoves = o.toType

Tactic:
rw [nim]

Result:
o : Ordinal.{u_1}
⊢ (mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)).RightMoves =
    o.toType
-- Mathlib/Algebra/Homology/Additive.lean
theorem singleMapHomologicalComplex_inv_app_ne {i j : ι} (h : i ≠ j) (X : W₁) :
    ((singleMapHomologicalComplex F c j).inv.app X).f i = 0

Proof state:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{u_6, u_3} W₁
inst✝⁶ : Category.{u_5, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
X : W₁
⊢ ((singleMapHomologicalComplex F c j).inv.app X).f i = 0

Tactic:
simp [singleMapHomologicalComplex, h]

Result:
no goals