harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem pullbackIsoProdSubtype_hom_apply {f : X ⟶ Z} {g : Y ⟶ Z}
    (x : ↑(pullback f g)) :
    (pullbackIsoProdSubtype f g).hom x =
      ⟨⟨pullback.fst f g x, pullback.snd f g x⟩, by
        simpa using CategoryTheory.congr_fun pullback.condition x⟩

Proof state:
case a.fst
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(pullback f g)
⊢ (↑((ConcreteCategory.hom (pullbackIsoProdSubtype f g).hom) x)).1 =
    (↑⟨((ConcreteCategory.hom (pullback.fst f g)) x, (ConcreteCategory.hom (pullback.snd f g)) x), ⋯⟩).1

case a.snd
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(pullback f g)
⊢ (↑((ConcreteCategory.hom (pullbackIsoProdSubtype f g).hom) x)).2 =
    (↑⟨((ConcreteCategory.hom (pullback.fst f g)) x, (ConcreteCategory.hom (pullback.snd f g)) x), ⋯⟩).2

Tactic:
exacts [ConcreteCategory.congr_hom (pullbackIsoProdSubtype_hom_fst f g) x,
  ConcreteCategory.congr_hom (pullbackIsoProdSubtype_hom_snd f g) x]

Result:
no goals

Proof state:
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(pullback f g)
⊢ (ConcreteCategory.hom f)
      ((ConcreteCategory.hom (pullback.fst f g)) x, (ConcreteCategory.hom (pullback.snd f g)) x).1 =
    (ConcreteCategory.hom g)
      ((ConcreteCategory.hom (pullback.fst f g)) x, (ConcreteCategory.hom (pullback.snd f g)) x).2

Tactic:
simpa using CategoryTheory.congr_fun pullback.condition x

Result:
no goals

Proof state:
case a
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(pullback f g)
⊢ ↑((ConcreteCategory.hom (pullbackIsoProdSubtype f g).hom) x) =
    ↑⟨((ConcreteCategory.hom (pullback.fst f g)) x, (ConcreteCategory.hom (pullback.snd f g)) x), ⋯⟩

Tactic:
apply Prod.ext

Result:
case a.fst
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(pullback f g)
⊢ (↑((ConcreteCategory.hom (pullbackIsoProdSubtype f g).hom) x)).1 =
    (↑⟨((ConcreteCategory.hom (pullback.fst f g)) x, (ConcreteCategory.hom (pullback.snd f g)) x), ⋯⟩).1

case a.snd
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(pullback f g)
⊢ (↑((ConcreteCategory.hom (pullbackIsoProdSubtype f g).hom) x)).2 =
    (↑⟨((ConcreteCategory.hom (pullback.fst f g)) x, (ConcreteCategory.hom (pullback.snd f g)) x), ⋯⟩).2

Proof state:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(pullback f g)
⊢ (ConcreteCategory.hom (pullbackIsoProdSubtype f g).hom) x =
    ⟨((ConcreteCategory.hom (pullback.fst f g)) x, (ConcreteCategory.hom (pullback.snd f g)) x), ⋯⟩

Tactic:
apply Subtype.ext

Result:
case a
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(pullback f g)
⊢ ↑((ConcreteCategory.hom (pullbackIsoProdSubtype f g).hom) x) =
    ↑⟨((ConcreteCategory.hom (pullback.fst f g)) x, (ConcreteCategory.hom (pullback.snd f g)) x), ⋯⟩
-- Mathlib/Data/Matrix/Mul.lean
theorem mulVec_mulVec [Fintype n] [Fintype o] (v : o → α) (M : Matrix m n α) (N : Matrix n o α) :
    M *ᵥ N *ᵥ v = (M * N) *ᵥ v

Proof state:
case h
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
x✝ : m
⊢ ((M * N) *ᵥ v) x✝ = (M *ᵥ N *ᵥ v) x✝

Tactic:
apply dotProduct_assoc

Result:
no goals

Proof state:
case h
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
x✝ : m
⊢ (M *ᵥ N *ᵥ v) x✝ = ((M * N) *ᵥ v) x✝

Tactic:
symm

Result:
case h
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
x✝ : m
⊢ ((M * N) *ᵥ v) x✝ = (M *ᵥ N *ᵥ v) x✝

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
⊢ M *ᵥ N *ᵥ v = (M * N) *ᵥ v

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
x✝ : m
⊢ (M *ᵥ N *ᵥ v) x✝ = ((M * N) *ᵥ v) x✝
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingular_neg {P : Fin 3 → F} (hP : W.Nonsingular P) : W.Nonsingular <| W.neg P

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ W.Nonsingular (W.neg P)

Tactic:
simp only [neg_of_Z_ne_zero hPz, nonsingular_smul _ <| Ne.isUnit hPz,
  nonsingular_neg_of_Z_ne_zero hP hPz]

Result:
no goals

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.Nonsingular (W.neg P)

Tactic:
simp only [neg_of_Z_eq_zero hP.left hPz, nonsingular_smul _ (isUnit_Y_of_Z_eq_zero hP hPz).neg,
  nonsingular_zero]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
⊢ W.Nonsingular (W.neg P)

Tactic:
by_cases hPz : P z = 0

Result:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.Nonsingular (W.neg P)

case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ W.Nonsingular (W.neg P)
-- Mathlib/Analysis/Calculus/Deriv/Pow.lean
theorem hasStrictDerivAt_pow :
    ∀ (n : ℕ) (x : 𝕜), HasStrictDerivAt (fun x : 𝕜 ↦ x ^ n) ((n : 𝕜) * x ^ (n - 1)) x
  | 0, x => by simp [hasStrictDerivAt_const]
  | 1, x => by simpa using hasStrictDerivAt_id x
  | n + 1 + 1, x => by
    simpa [pow_succ, add_mul, mul_assoc] using
      (hasStrictDerivAt_pow (n + 1) x).mul (hasStrictDerivAt_id x)

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
⊢ HasStrictDerivAt (fun x => x ^ (n + 1 + 1)) (↑(n + 1 + 1) * x ^ (n + 1 + 1 - 1)) x

Tactic:
simpa [pow_succ, add_mul, mul_assoc] using
  (hasStrictDerivAt_pow (n + 1) x).mul (hasStrictDerivAt_id x)

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ HasStrictDerivAt (fun x => x ^ 0) (↑0 * x ^ (0 - 1)) x

Tactic:
simp [hasStrictDerivAt_const]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ HasStrictDerivAt (fun x => x ^ 1) (↑1 * x ^ (1 - 1)) x

Tactic:
simpa using hasStrictDerivAt_id x

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivWithinAt.smul_const (hc : HasFDerivWithinAt c c' s x) (f : F) :
    HasFDerivWithinAt (fun y => c y • f) (c'.smulRight f) s x

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : E
s : Set E
𝕜' : Type u_5
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivWithinAt c c' s x
f : F
⊢ HasFDerivWithinAt (fun y => c y • f) (c'.smulRight f) s x

Tactic:
simpa only [smul_zero, zero_add] using hc.smul (hasFDerivWithinAt_const f x s)

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map₂_none_right (f : α → β → γ) (a : Option α) : map₂ f a none = none

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
⊢ map₂ f a none = none

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₂_of_isShortNF : W.b₂ = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ W.b₂ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
lemma oneEquiv_naturality (f : M →ₗ[R] N) :
    (oneEquiv R N).comp (map 1 f) = f.comp (oneEquiv R M).toLinearMap

Proof state:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ ↑(oneEquiv R N) ∘ₗ map 1 f = f ∘ₗ ↑(oneEquiv R M)

Tactic:
aesop

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_mul [DecidableEq σ] :
    coeff R n (φ * ψ) = ∑ p ∈ antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
inst✝ : DecidableEq σ
⊢ (coeff R n) (φ * ψ) = ∑ p ∈ antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ

Tactic:
refine Finset.sum_congr ?_ fun _ _ => rfl

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
inst✝ : DecidableEq σ
⊢ antidiagonal n = antidiagonal n

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
inst✝ : DecidableEq σ
⊢ antidiagonal n = antidiagonal n

Tactic:
rw [Subsingleton.elim (Classical.decEq σ) ‹DecidableEq σ›]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem continuous_uliftMap [TopologicalSpace X] [TopologicalSpace Y]
    (f : X → Y) (hf : Continuous f) :
    Continuous (ULift.map f : ULift.{u'} X → ULift.{v'} Y)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
⊢ Continuous (ULift.map f)

Tactic:
change Continuous (ULift.up ∘ f ∘ ULift.down)

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
⊢ Continuous (ULift.up ∘ f ∘ ULift.down)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
⊢ Continuous (ULift.up ∘ f ∘ ULift.down)

Tactic:
continuity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem countP_pmap {p : α → Prop} (g : ∀ a, p a → β) (f : β → Bool) (l : Vector α n) (H₁) :
    (l.pmap g H₁).countP f =
      l.attach.countP (fun ⟨a, m⟩ => f (g a (H₁ a m)))

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
g : (a : α) → p a → β
f : β → Bool
l : Array α
H₁ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
⊢ Array.countP (fun x => f (g x.val ⋯)) l.attach =
    countP (fun x => f (g x.val ⋯)) { toArray := l, size_toArray := ⋯ }.attach

Tactic:
simp [Array.countP_eq_size_filter]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
g : (a : α) → p a → β
f : β → Bool
l : Vector α n
H₁ : ∀ (a : α), a ∈ l → p a
⊢ countP f (pmap g l H₁) =
    countP
      (fun x =>
        match x with
        | ⟨a, m⟩ => f (g a ⋯))
      l.attach

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
g : (a : α) → p a → β
f : β → Bool
l : Array α
H₁ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
⊢ countP f (pmap g { toArray := l, size_toArray := ⋯ } H₁) =
    countP
      (fun x =>
        match x with
        | ⟨a, m⟩ => f (g a ⋯))
      { toArray := l, size_toArray := ⋯ }.attach

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
g : (a : α) → p a → β
f : β → Bool
l : Array α
H₁ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
⊢ countP f (pmap g { toArray := l, size_toArray := ⋯ } H₁) =
    countP
      (fun x =>
        match x with
        | ⟨a, m⟩ => f (g a ⋯))
      { toArray := l, size_toArray := ⋯ }.attach

Tactic:
simp only [pmap_mk, countP_mk, Array.countP_pmap]

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
g : (a : α) → p a → β
f : β → Bool
l : Array α
H₁ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
⊢ Array.countP (fun x => f (g x.val ⋯)) l.attach =
    countP (fun x => f (g x.val ⋯)) { toArray := l, size_toArray := ⋯ }.attach
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_cons_right (h : a ≤ b) : b ::ₘ Ico a b = Icc a b

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ (Finset.Icc a b).val = Icc a b

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ b ::ₘ Ico a b = Icc a b

Tactic:
rw [Ico, ← Finset.insert_val_of_not_mem right_not_mem_Ico, Finset.Ico_insert_right h]

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ (Finset.Icc a b).val = Icc a b

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ b ::ₘ Ico a b = Icc a b

Tactic:
classical
  rw [Ico, ← Finset.insert_val_of_not_mem right_not_mem_Ico, Finset.Ico_insert_right h]
  rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LSum.lean
theorem sum_smul_index_linearMap' [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂]
    [Module R M₂] {v : α →₀ M} {c : R} {h : α → M →ₗ[R] M₂} :
    ((c • v).sum fun a => h a) = c • v.sum fun a => h a

Proof state:
α : Type u_1
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
i : α
⊢ (h i) 0 = 0

Tactic:
exact (h i).map_zero

Result:
no goals

Proof state:
α : Type u_1
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
⊢ ∀ (i : α), (h i) 0 = 0

Tactic:
intro i

Result:
α : Type u_1
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
i : α
⊢ (h i) 0 = 0

Proof state:
α : Type u_1
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
⊢ ((c • v).sum fun a => ⇑(h a)) = c • v.sum fun a => ⇑(h a)

Tactic:
rw [Finsupp.sum_smul_index', Finsupp.smul_sum]

Result:
α : Type u_1
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
⊢ (v.sum fun i c_1 => (h i) (c • c_1)) = v.sum fun a b => c • (h a) b

α : Type u_1
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
⊢ ∀ (i : α), (h i) 0 = 0

Proof state:
α : Type u_1
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
⊢ (v.sum fun i c_1 => (h i) (c • c_1)) = v.sum fun a b => c • (h a) b

Tactic:
simp only [map_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.lo_lo (u w v k₁ k₂ : Nat) : u + k₁ ≤ w → w + k₂ ≤ v → u + (k₁ + k₂) ≤ v

Proof state:
u w v k₁ k₂ : Nat
⊢ u + k₁ ≤ w → w + k₂ ≤ v → u + (k₁ + k₂) ≤ v

Tactic:
omega

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem infIrred_iff_not_isMax : InfIrred a ↔ ¬IsMax a :=
  and_iff_left fun _ _ => by simpa only [min_eq_iff] using Or.imp And.left And.left

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a x✝¹ x✝ : α
⊢ x✝¹ ⊓ x✝ = a → x✝¹ = a ∨ x✝ = a

Tactic:
simpa only [min_eq_iff] using Or.imp And.left And.left

Result:
no goals
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
lemma iff_flat_and_lTensor_reflects_triviality :
    FaithfullyFlat R M ↔
    (Flat R M ∧
      ∀ (N : Type max u v) [AddCommGroup N] [Module R N],
        Subsingleton (M ⊗[R] N) → Subsingleton N) :=
  iff_flat_and_lTensor_faithful R M |>.trans <| and_congr_right_iff.2 fun _ => iff_of_eq <|
    forall_congr fun N => forall_congr fun _ => forall_congr fun _ => iff_iff_eq.1 <| by
      simp only [← not_subsingleton_iff_nontrivial]; tauto

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝² : Flat R M
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
⊢ Nontrivial N → Nontrivial (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N

Tactic:
simp only [← not_subsingleton_iff_nontrivial]

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝² : Flat R M
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
⊢ ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝² : Flat R M
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
⊢ ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_and_mono_f_iff_of_iso (e : S₁ ≅ S₂) :
    S₁.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
⊢ S₁.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f

Tactic:
have : Mono S₁.f ↔ Mono S₂.f :=
  (MorphismProperty.monomorphisms C).arrow_mk_iso_iff
    (Arrow.isoMk (ShortComplex.π₁.mapIso e) (ShortComplex.π₂.mapIso e) e.hom.comm₁₂)

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
this : Mono S₁.f ↔ Mono S₂.f
⊢ S₁.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
this : Mono S₁.f ↔ Mono S₂.f
⊢ S₁.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f

Tactic:
rw [exact_iff_of_iso e, this]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_pos_iff {p} : 0 < countP p l ↔ ∃ a ∈ l, p a

Proof state:
α✝ : Type u_1
l : Array α✝
p : α✝ → Bool
⊢ 0 < countP p l ↔ ∃ a, a ∈ l ∧ p a = true

Tactic:
cases l

Result:
case mk
α✝ : Type u_1
p : α✝ → Bool
toList✝ : List α✝
⊢ 0 < countP p { toList := toList✝ } ↔ ∃ a, a ∈ { toList := toList✝ } ∧ p a = true

Proof state:
case mk
α✝ : Type u_1
p : α✝ → Bool
toList✝ : List α✝
⊢ 0 < countP p { toList := toList✝ } ↔ ∃ a, a ∈ { toList := toList✝ } ∧ p a = true

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Prod.lean
lemma tendsto_finset_prod_atTop :
    Tendsto (fun (p : Finset ι × Finset ι') ↦ p.1 ×ˢ p.2) atTop atTop

Proof state:
case hf
ι : Type u_1
ι' : Type u_2
p q : Finset ι × Finset ι'
hpq : p ≤ q
⊢ (fun p => p.1 ×ˢ p.2) p ≤ (fun p => p.1 ×ˢ p.2) q

Tactic:
simpa using Finset.product_subset_product hpq.1 hpq.2

Result:
no goals

Proof state:
case h
ι : Type u_1
ι' : Type u_2
b : Finset (ι × ι')
⊢ ∃ a, b ≤ a.1 ×ˢ a.2

Tactic:
use (Finset.image Prod.fst b, Finset.image Prod.snd b)

Result:
case h
ι : Type u_1
ι' : Type u_2
b : Finset (ι × ι')
⊢ b ≤ (Finset.image Prod.fst b, Finset.image Prod.snd b).1 ×ˢ (Finset.image Prod.fst b, Finset.image Prod.snd b).2

Proof state:
ι : Type u_1
ι' : Type u_2
⊢ Tendsto (fun p => p.1 ×ˢ p.2) atTop atTop

Tactic:
apply Monotone.tendsto_atTop_atTop

Result:
case hf
ι : Type u_1
ι' : Type u_2
⊢ Monotone fun p => p.1 ×ˢ p.2

case h
ι : Type u_1
ι' : Type u_2
⊢ ∀ (b : Finset (ι × ι')), ∃ a, b ≤ a.1 ×ˢ a.2

Proof state:
case hf
ι : Type u_1
ι' : Type u_2
⊢ Monotone fun p => p.1 ×ˢ p.2

Tactic:
intro p q hpq

Result:
case hf
ι : Type u_1
ι' : Type u_2
p q : Finset ι × Finset ι'
hpq : p ≤ q
⊢ (fun p => p.1 ×ˢ p.2) p ≤ (fun p => p.1 ×ˢ p.2) q

Proof state:
case h
ι : Type u_1
ι' : Type u_2
b : Finset (ι × ι')
⊢ b ≤ (Finset.image Prod.fst b, Finset.image Prod.snd b).1 ×ˢ (Finset.image Prod.fst b, Finset.image Prod.snd b).2

Tactic:
exact Finset.subset_product

Result:
no goals

Proof state:
case h
ι : Type u_1
ι' : Type u_2
⊢ ∀ (b : Finset (ι × ι')), ∃ a, b ≤ a.1 ×ˢ a.2

Tactic:
intro b

Result:
case h
ι : Type u_1
ι' : Type u_2
b : Finset (ι × ι')
⊢ ∃ a, b ≤ a.1 ×ˢ a.2
-- Mathlib/Data/Bool/Basic.lean
theorem or_inl {a b : Bool} (H : a) : a || b

Proof state:
a b : Bool
H : a = true
⊢ (a || b) = true

Tactic:
simp [H]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addX_of_Z_eq_zero_right {P Q : Fin 3 → R} (hQz : Q z = 0) :
    W'.addX P Q = (-(Q x * P z)) ^ 2 * P x

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ P x * Q x ^ 2 * P z ^ 2 - 2 * P y * Q y * P z * 0 + P x ^ 2 * Q x * 0 ^ 2 - W'.a₁ * P x * Q y * P z ^ 2 * 0 -
                  W'.a₁ * P y * Q x * P z * 0 ^ 2 +
                2 * W'.a₂ * P x * Q x * P z ^ 2 * 0 ^ 2 -
              W'.a₃ * Q y * P z ^ 4 * 0 -
            W'.a₃ * P y * P z * 0 ^ 4 +
          W'.a₄ * Q x * P z ^ 4 * 0 ^ 2 +
        W'.a₄ * P x * P z ^ 2 * 0 ^ 4 +
      2 * W'.a₆ * P z ^ 4 * 0 ^ 4 =
    (-(Q x * P z)) ^ 2 * P x

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ W'.addX P Q = (-(Q x * P z)) ^ 2 * P x

Tactic:
rw [addX, hQz]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ P x * Q x ^ 2 * P z ^ 2 - 2 * P y * Q y * P z * 0 + P x ^ 2 * Q x * 0 ^ 2 - W'.a₁ * P x * Q y * P z ^ 2 * 0 -
                  W'.a₁ * P y * Q x * P z * 0 ^ 2 +
                2 * W'.a₂ * P x * Q x * P z ^ 2 * 0 ^ 2 -
              W'.a₃ * Q y * P z ^ 4 * 0 -
            W'.a₃ * P y * P z * 0 ^ 4 +
          W'.a₄ * Q x * P z ^ 4 * 0 ^ 2 +
        W'.a₄ * P x * P z ^ 2 * 0 ^ 4 +
      2 * W'.a₆ * P z ^ 4 * 0 ^ 4 =
    (-(Q x * P z)) ^ 2 * P x
-- Mathlib/Data/Nat/Nth.lean
theorem nth_eq_zero_mono (h₀ : ¬p 0) {a b : ℕ} (hab : a ≤ b) (ha : nth p a = 0) : nth p b = 0

Proof state:
p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : nth p a = 0
⊢ nth p b = 0

Tactic:
simp only [nth_eq_zero, h₀, false_and, false_or] at ha ⊢

Result:
p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ a
⊢ ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b

Proof state:
p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ a
⊢ ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b

Tactic:
exact ha.imp fun hf hle => hle.trans hab

Result:
no goals
-- Mathlib/LinearAlgebra/Isomorphisms.lean
theorem quotientQuotientEquivQuotientAux_mk_mk (x : M) :
    quotientQuotientEquivQuotientAux S T h (Quotient.mk (Quotient.mk x)) = Quotient.mk x

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S T : Submodule R M
h : S ≤ T
x : M
⊢ (S.quotientQuotientEquivQuotientAux T h) (Quotient.mk (Quotient.mk x)) = Quotient.mk x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc]
lemma d_snd_v (i j : ℤ) (hij : i + 1 = j) :
    (mappingCone φ).d i j ≫ (snd φ).v j j (add_zero _) =
      (fst φ).1.v i j hij ≫ φ.f j + (snd φ).v i i (add_zero i) ≫ G.d i j

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
⊢ (mappingCone φ).d i j ≫ (snd φ).v j j ⋯ = (↑(fst φ)).v i j hij ≫ φ.f j + (snd φ).v i i ⋯ ≫ G.d i j

Tactic:
dsimp [mappingCone, snd, fst]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
⊢ homotopyCofiber.d φ i j ≫ (Cochain.ofHoms (homotopyCofiber.sndX φ)).v j j ⋯ =
    homotopyCofiber.fstX φ i j hij ≫ φ.f j + (Cochain.ofHoms (homotopyCofiber.sndX φ)).v i i ⋯ ≫ G.d i j

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
⊢ homotopyCofiber.d φ i j ≫ homotopyCofiber.sndX φ j =
    homotopyCofiber.fstX φ i j hij ≫ φ.f j + homotopyCofiber.sndX φ i ≫ G.d i j

Tactic:
apply homotopyCofiber.d_sndX

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
⊢ homotopyCofiber.d φ i j ≫ (Cochain.ofHoms (homotopyCofiber.sndX φ)).v j j ⋯ =
    homotopyCofiber.fstX φ i j hij ≫ φ.f j + (Cochain.ofHoms (homotopyCofiber.sndX φ)).v i i ⋯ ≫ G.d i j

Tactic:
simp only [Cochain.ofHoms_v]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
⊢ homotopyCofiber.d φ i j ≫ homotopyCofiber.sndX φ j =
    homotopyCofiber.fstX φ i j hij ≫ φ.f j + homotopyCofiber.sndX φ i ≫ G.d i j