harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/FixedPointFree.lean
theorem commutatorMap_injective (hφ : FixedPointFree φ) : Function.Injective (commutatorMap φ)

Proof state:
F : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : FunLike F G G
inst✝ : MonoidHomClass F G G
φ : F
hφ : FixedPointFree ⇑φ
⊢ Function.Injective (commutatorMap ⇑φ)

Tactic:
refine fun x y h ↦ inv_mul_eq_one.mp <| hφ _ ?_

Result:
F : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : FunLike F G G
inst✝ : MonoidHomClass F G G
φ : F
hφ : FixedPointFree ⇑φ
x y : G
h : commutatorMap (⇑φ) x = commutatorMap (⇑φ) y
⊢ φ (x⁻¹ * y) = x⁻¹ * y

Proof state:
F : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : FunLike F G G
inst✝ : MonoidHomClass F G G
φ : F
hφ : FixedPointFree ⇑φ
x y : G
h : commutatorMap (⇑φ) x = commutatorMap (⇑φ) y
⊢ φ (x⁻¹ * y) = x⁻¹ * y

Tactic:
rwa [map_mul, map_inv, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← eq_div_iff_mul_eq', ← division_def]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem IsCoprime.prod_right : (∀ i ∈ t, IsCoprime x (s i)) → IsCoprime x (∏ i ∈ t, s i)

Proof state:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ (∀ i ∈ t, IsCoprime x (s i)) → IsCoprime x (∏ i ∈ t, s i)

Tactic:
simpa only [isCoprime_comm] using IsCoprime.prod_left (R := R)

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem dite_ne_left_iff : dite P (fun _ ↦ a) B ≠ a ↔ ∃ h, a ≠ B h

Proof state:
α : Sort u_1
P : Prop
inst✝ : Decidable P
a : α
B : ¬P → α
⊢ dite P (fun x => a) B ≠ a ↔ ∃ h, a ≠ B h

Tactic:
rw [Ne, dite_eq_left_iff, not_forall]

Result:
α : Sort u_1
P : Prop
inst✝ : Decidable P
a : α
B : ¬P → α
⊢ (∃ x, ¬B x = a) ↔ ∃ h, a ≠ B h

Proof state:
α : Sort u_1
P : Prop
inst✝ : Decidable P
a : α
B : ¬P → α
⊢ (∃ x, ¬B x = a) ↔ ∃ h, a ≠ B h

Tactic:
exact exists_congr fun h ↦ by rw [ne_comm]

Result:
no goals

Proof state:
α : Sort u_1
P : Prop
inst✝ : Decidable P
a : α
B : ¬P → α
h : ¬P
⊢ ¬B h = a ↔ a ≠ B h

Tactic:
rw [ne_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.comp_diag {X Y : C} [HasBinaryProduct Y Y] (f : X ⟶ Y) :
    f ≫ diag Y = prod.lift f f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct Y Y
f : X ⟶ Y
⊢ f ≫ diag Y = lift f f

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem AffineMap.lineMap_mem {k V P : Type*} [Ring k] [AddCommGroup V] [Module k V]
    [AddTorsor V P] {Q : AffineSubspace k P} {p₀ p₁ : P} (c : k) (h₀ : p₀ ∈ Q) (h₁ : p₁ ∈ Q) :
    AffineMap.lineMap p₀ p₁ c ∈ Q

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
Q : AffineSubspace k P
p₀ p₁ : P
c : k
h₀ : p₀ ∈ Q
h₁ : p₁ ∈ Q
⊢ c • (p₁ -ᵥ p₀) +ᵥ p₀ ∈ Q

Tactic:
exact Q.smul_vsub_vadd_mem c h₁ h₀ h₀

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
Q : AffineSubspace k P
p₀ p₁ : P
c : k
h₀ : p₀ ∈ Q
h₁ : p₁ ∈ Q
⊢ (lineMap p₀ p₁) c ∈ Q

Tactic:
rw [AffineMap.lineMap_apply]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
Q : AffineSubspace k P
p₀ p₁ : P
c : k
h₀ : p₀ ∈ Q
h₁ : p₁ ∈ Q
⊢ c • (p₁ -ᵥ p₀) +ᵥ p₀ ∈ Q
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
lemma isClique_singleton (a : α) : G.IsClique {a}

Proof state:
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.IsClique {a}

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem convex_vadd (a : E) : Convex 𝕜 (a +ᵥ s) ↔ Convex 𝕜 s :=
  ⟨fun h ↦ by simpa using h.vadd (-a), fun h ↦ h.vadd _⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : E
h : Convex 𝕜 (a +ᵥ s)
⊢ Convex 𝕜 s

Tactic:
simpa using h.vadd (-a)

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive (attr := simp)]
lemma stabilizer_univ : stabilizer G (Set.univ : Set α) = ⊤

Proof state:
case h
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : G
⊢ x✝ ∈ stabilizer G univ ↔ x✝ ∈ ⊤

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ stabilizer G univ = ⊤

Tactic:
ext

Result:
case h
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : G
⊢ x✝ ∈ stabilizer G univ ↔ x✝ ∈ ⊤
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem charmatrix_apply_natDegree_le (i j : n) :
    (charmatrix M i j).natDegree ≤ ite (i = j) 1 0

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
⊢ (M.charmatrix i j).natDegree ≤ if i = j then 1 else 0

Tactic:
split_ifs with h <;> simp [h, natDegree_X_le]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem congToClass_empty : congToClass ∅ = ∅

Proof state:
⊢ congToClass ∅ = ∅

Tactic:
ext z

Result:
case a
z : ZFSet.{u_1}
⊢ congToClass ∅ z ↔ ∅ z

Proof state:
case a
z : ZFSet.{u_1}
⊢ congToClass ∅ z ↔ ∅ z

Tactic:
simp only [congToClass, not_empty_hom, iff_false]

Result:
case a
z : ZFSet.{u_1}
⊢ ¬{y | ↑y ∈ ∅} z

Proof state:
case a
z : ZFSet.{u_1}
⊢ ¬{y | ↑y ∈ ∅} z

Tactic:
exact Set.not_mem_empty z

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_insert_pos {l : List α} {a : α} : 0 < (l.insert a).length

Proof state:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ 0 < (List.insert a l).length

Tactic:
rw [length_insert_of_mem h]

Result:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ 0 < l.length

Proof state:
case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ 0 < (List.insert a l).length

Tactic:
rw [length_insert_of_not_mem h]

Result:
case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ 0 < l.length + 1

Proof state:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ 0 < l.length

Tactic:
exact length_pos_of_mem h

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ 0 < l.length + 1

Tactic:
exact Nat.zero_lt_succ _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ 0 < (List.insert a l).length

Tactic:
by_cases h : a ∈ l

Result:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ 0 < (List.insert a l).length

case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ 0 < (List.insert a l).length
-- Mathlib/FieldTheory/Differential/Basic.lean
@[simp]
lemma logDeriv_one : logDeriv (1 : R) = 0

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
⊢ logDeriv 1 = 0

Tactic:
simp [logDeriv]

Result:
no goals
-- Mathlib/Topology/Instances/Sign.lean
theorem continuousAt_sign_of_neg {a : α} (h : a < 0) : ContinuousAt SignType.sign a

Proof state:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ ∃ t, (∀ y ∈ t, -1 = SignType.sign y) ∧ IsOpen t ∧ a ∈ t

Tactic:
exact ⟨{ x | x < 0 }, fun x hx => (sign_neg hx).symm, isOpen_gt' 0, h⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ (fun x => -1) =ᶠ[nhds a] ⇑SignType.sign

Tactic:
rw [Filter.EventuallyEq, eventually_nhds_iff]

Result:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ ∃ t, (∀ y ∈ t, -1 = SignType.sign y) ∧ IsOpen t ∧ a ∈ t

Proof state:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ ContinuousAt (⇑SignType.sign) a

Tactic:
refine (continuousAt_const : ContinuousAt (fun x => (-1 : SignType)) a).congr ?_

Result:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ (fun x => -1) =ᶠ[nhds a] ⇑SignType.sign
-- Mathlib/Topology/Path.lean
theorem refl_range {a : X} : range (Path.refl a) = {a}

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a : X
⊢ range ⇑(refl a) = {a}

Tactic:
simp [Path.refl, CoeFun.coe]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem map_swap_product (s : Finset α) (t : Finset β) :
    (t ×ˢ s).map ⟨Prod.swap, Prod.swap_injective⟩ = s ×ˢ t :=
  coe_injective <| by
    push_cast
    exact Set.image_swap_prod _ _

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ↑(map { toFun := Prod.swap, inj' := ⋯ } (t ×ˢ s)) = ↑(s ×ˢ t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ⇑{ toFun := Prod.swap, inj' := ⋯ } '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ⇑{ toFun := Prod.swap, inj' := ⋯ } '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t

Tactic:
exact Set.image_swap_prod _ _

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean
lemma map_apply {m₁ m₂ : SimplexCategoryᵒᵖ} (f : m₁ ⟶ m₂) {n : SimplexCategory}
    (x : (stdSimplex.{u}.obj n).obj m₁) :
    (stdSimplex.{u}.obj n).map f x = (objEquiv _ _).symm (f.unop ≫ (objEquiv _ _) x)

Proof state:
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
n : SimplexCategory
x : (stdSimplex.obj n).obj m₁
⊢ (stdSimplex.obj n).map f x = (objEquiv n m₂).symm (f.unop ≫ (objEquiv n m₁) x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/QPF/Multivariate/Basic.lean
theorem comp_map {α β γ : TypeVec n} (f : α ⟹ β) (g : β ⟹ γ) (x : F α) :
    (g ⊚ f) <$$> x = g <$$> f <$$> x

Proof state:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α β γ : TypeVec.{u} n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ (g ⊚ f) <$$> x = g <$$> f <$$> x

Tactic:
rw [← abs_repr x, ← abs_map, ← abs_map, ← abs_map]

Result:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α β γ : TypeVec.{u} n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ abs ((g ⊚ f) <$$> repr x) = abs (g <$$> f <$$> repr x)

Proof state:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α β γ : TypeVec.{u} n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ abs ((g ⊚ f) <$$> repr x) = abs (g <$$> f <$$> repr x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem exists_conts_b_of_den {B : K} (nth_denom_eq : g.dens n = B) :
    ∃ conts, g.conts n = conts ∧ conts.b = B

Proof state:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
B : K
nth_denom_eq : g.dens n = B
⊢ ∃ conts, g.conts n = conts ∧ conts.b = B

Tactic:
simpa

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
theorem ContinuousMultilinearMap.uncurry_curryRight (f : ContinuousMultilinearMap 𝕜 Ei G) :
    f.curryRight.uncurryRight = f

Proof state:
case H
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n.succ) → Ei i
⊢ f.curryRight.uncurryRight m = f m

Tactic:
rw [uncurryRight_apply, curryRight_apply, snoc_init_self]

Result:
no goals

Proof state:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
⊢ f.curryRight.uncurryRight = f

Tactic:
ext m

Result:
case H
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n.succ) → Ei i
⊢ f.curryRight.uncurryRight m = f m
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_Ici {a : ℝ} : volume (Ici a) = ∞

Proof state:
a : ℝ
⊢ volume (Ioi a) = ⊤

Tactic:
simp

Result:
no goals

Proof state:
a : ℝ
⊢ volume (Ici a) = ⊤

Tactic:
rw [← measure_congr Ioi_ae_eq_Ici]

Result:
a : ℝ
⊢ volume (Ioi a) = ⊤
-- Mathlib/Data/Fin/Basic.lean
theorem min_val {a : Fin n} : min (a : ℕ) n = a

Proof state:
n : ℕ
a : Fin n
⊢ ↑a ⊓ n = ↑a

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem WfDvdMonoid.of_wellFounded_associates [CancelCommMonoidWithZero α]
    (h : WellFounded ((· < ·) : Associates α → Associates α → Prop)) : WfDvdMonoid α :=
  WfDvdMonoid.of_wfDvdMonoid_associates
    ⟨by
      convert h
      ext
      exact Associates.dvdNotUnit_iff_lt⟩

Proof state:
case h.e'_2.h.h.h.e.h.h.a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
h : WellFounded fun x1 x2 => x1 < x2
x✝³ x✝² x✝¹ x✝ : Associates α
⊢ DvdNotUnit x✝¹ x✝ ↔ x✝¹ < x✝

Tactic:
exact Associates.dvdNotUnit_iff_lt

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
h : WellFounded fun x1 x2 => x1 < x2
⊢ WellFounded DvdNotUnit

Tactic:
convert h

Result:
case h.e'_2.h.h.h.e
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
h : WellFounded fun x1 x2 => x1 < x2
x✝¹ x✝ : Associates α
⊢ DvdNotUnit = LT.lt

Proof state:
case h.e'_2.h.h.h.e
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
h : WellFounded fun x1 x2 => x1 < x2
x✝¹ x✝ : Associates α
⊢ DvdNotUnit = LT.lt

Tactic:
ext

Result:
case h.e'_2.h.h.h.e.h.h.a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
h : WellFounded fun x1 x2 => x1 < x2
x✝³ x✝² x✝¹ x✝ : Associates α
⊢ DvdNotUnit x✝¹ x✝ ↔ x✝¹ < x✝
-- Mathlib/RepresentationTheory/Character.lean
theorem char_mul_comm (V : FDRep k G) (g : G) (h : G) :
    V.character (h * g) = V.character (g * h)

Proof state:
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V : FDRep k G
g h : G
⊢ V.character (h * g) = V.character (g * h)

Tactic:
simp only [trace_mul_comm, character, map_mul]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lsub_typein (o : Ordinal) : lsub.{u, u} (typein (α := o.toType) (· < ·)) = o :=
  (lsub_le.{u, u} typein_lt_self).antisymm
    (by
      by_contra! h
      -- Porting note: `nth_rw` → `conv_rhs` & `rw`
      conv_rhs at h => rw [← type_lt o]
      simpa [typein_enum] using lt_lsub.{u, u} (typein (· < ·)) (enum (· < ·) ⟨_, h⟩))

Proof state:
o : Ordinal.{u}
h : lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding < o
⊢ False

Tactic:
conv_rhs at h => rw [← type_lt o]

Result:
o : Ordinal.{u}
h : lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding < type fun x1 x2 => x1 < x2
⊢ False

Proof state:
o : Ordinal.{u}
⊢ o ≤ lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding

Tactic:
by_contra! h

Result:
o : Ordinal.{u}
h : lsub ⇑(typein fun x1 x2 => x1 < x2).toRelEmbedding < o
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Log/Summable.lean
lemma Complex.multipliable_one_add_of_summable (f : ι → ℂ) (hf : Summable f)
    (hff : ∀ n : ι, 1 + f n ≠ 0) : Multipliable (fun n : ι => 1 + f n)

Proof state:
ι : Type u_1
f : ι → ℂ
hf : Summable f
hff : ∀ (n : ι), 1 + f n ≠ 0
⊢ Summable fun n => log ((fun n => 1 + f n) n)

Tactic:
simpa only [forall_const] using Complex.summable_log_one_add_of_summable hf

Result:
no goals

Proof state:
ι : Type u_1
f : ι → ℂ
hf : Summable f
hff : ∀ (n : ι), 1 + f n ≠ 0
⊢ ∀ (n : ι), (fun n => 1 + f n) n ≠ 0

Tactic:
simpa

Result:
no goals

Proof state:
ι : Type u_1
f : ι → ℂ
hf : Summable f
hff : ∀ (n : ι), 1 + f n ≠ 0
⊢ Multipliable fun n => 1 + f n

Tactic:
refine Complex.multipliable_of_summable_log (fun n => 1 + f n) (by simpa) ?_

Result:
ι : Type u_1
f : ι → ℂ
hf : Summable f
hff : ∀ (n : ι), 1 + f n ≠ 0
⊢ Summable fun n => log ((fun n => 1 + f n) n)
-- Mathlib/SetTheory/Nimber/Basic.lean
theorem exists_of_lt_add (h : c < a + b) : (∃ a' < a, a' + b = c) ∨ ∃ b' < b, a + b' = c

Proof state:
a b c : Nimber
h : c < a + b
⊢ (∃ a' < a, a' + b = c) ∨ ∃ b' < b, a + b' = c

Tactic:
rw [add_def] at h

Result:
a b c : Nimber
h : c < sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ
⊢ (∃ a' < a, a' + b = c) ∨ ∃ b' < b, a + b' = c

Proof state:
a b c : Nimber
h : c < sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ
this : c ∉ {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ
⊢ (∃ a' < a, a' + b = c) ∨ ∃ b' < b, a + b' = c

Tactic:
rwa [Set.mem_compl_iff, not_not] at this

Result:
no goals

Proof state:
a b c : Nimber
h : c < sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ
⊢ (∃ a' < a, a' + b = c) ∨ ∃ b' < b, a + b' = c

Tactic:
have := not_mem_of_lt_csInf' h

Result:
a b c : Nimber
h : c < sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ
this : c ∉ {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ
⊢ (∃ a' < a, a' + b = c) ∨ ∃ b' < b, a + b' = c
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma comp_smul (f : R →+* S) (P : Fin 3 → R) (u : R) : f ∘ (u • P) = f u • f ∘ P

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ⇑f ∘ (u • P) = f u • ⇑f ∘ P

Tactic:
ext n

Result:
case h
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
n : Fin 3
⊢ (⇑f ∘ (u • P)) n = (f u • ⇑f ∘ P) n

Proof state:
case h
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
n : Fin 3
⊢ (⇑f ∘ (u • P)) n = (f u • ⇑f ∘ P) n

Tactic:
fin_cases n <;> simp only [smul_fin3, comp_fin3] <;> map_simp

Result:
no goals
-- Mathlib/RingTheory/Localization/AtPrime.lean
lemma Ideal.under_map_of_isLocalizationAtPrime {p : Ideal R} [p.IsPrime] (hpq : p ≤ q) :
    (p.map (algebraMap R S)).under R = p

Proof state:
R : Type u_4
inst✝⁵ : CommRing R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
⊢ under R (map (algebraMap R S) p) = p

Tactic:
have disj : Disjoint (q.primeCompl : Set R) p := by
  simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left, hpq]

Result:
R : Type u_4
inst✝⁵ : CommRing R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
disj : Disjoint ↑q.primeCompl ↑p
⊢ under R (map (algebraMap R S) p) = p

Proof state:
R : Type u_4
inst✝⁵ : CommRing R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
⊢ Disjoint ↑q.primeCompl ↑p

Tactic:
simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left, hpq]

Result:
no goals

Proof state:
R : Type u_4
inst✝⁵ : CommRing R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
disj : Disjoint ↑q.primeCompl ↑p
⊢ p.IsPrime

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u_4
inst✝⁵ : CommRing R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
disj : Disjoint ↑q.primeCompl ↑p
⊢ under R (map (algebraMap R S) p) = p

Tactic:
exact IsLocalization.comap_map_of_isPrime_disjoint _ _ p (by simpa) disj

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma homologyOpIso_inv_naturality [S₁.HasHomology] [S₂.HasHomology] :
    (homologyMap φ).op ≫ (S₁.homologyOpIso).inv =
      S₂.homologyOpIso.inv ≫ homologyMap (opMap φ)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ (homologyMap φ).op ≫ S₁.homologyOpIso.inv = S₂.homologyOpIso.inv ≫ homologyMap (opMap φ)

Tactic:
simp [homologyMap_op]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem iteratedFDeriv_succ_const (n : ℕ) (c : F) :
    (iteratedFDeriv 𝕜 (n + 1) fun _ : E ↦ c) = 0 :=
  iteratedFDeriv_const_of_ne (by simp) _

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
c : F
⊢ n + 1 ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem div_rpow (hx : 0 ≤ x) (hy : 0 ≤ y) (z : ℝ) : (x / y) ^ z = x ^ z / y ^ z

Proof state:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
z : ℝ
⊢ (x / y) ^ z = x ^ z / y ^ z

Tactic:
simp only [div_eq_mul_inv, mul_rpow hx (inv_nonneg.2 hy), inv_rpow hy]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem Codisjoint.himp_inf_cancel_left (h : Codisjoint a b) : b ⇨ a ⊓ b = a

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ b ⇨ a ⊓ b = a

Tactic:
rw [himp_inf_distrib, himp_self, inf_top_eq, h.himp_eq_right]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem const_lt {x y : α} : const x < const y ↔ x < y :=
  show Pos _ ↔ _ by rw [← const_sub, const_pos, sub_pos]

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
x y : α
⊢ (const y - const x).Pos ↔ x < y

Tactic:
rw [← const_sub, const_pos, sub_pos]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousWithinAt.prod_map {f : α → γ} {g : β → δ} {s : Set α} {t : Set β} {x : α} {y : β}
    (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g t y) :
    ContinuousWithinAt (Prod.map f g) (s ×ˢ t) (x, y)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → γ
g : β → δ
s : Set α
t : Set β
x : α
y : β
hf : Tendsto f (𝓝[s] x) (𝓝 (f x))
hg : Tendsto g (𝓝[t] y) (𝓝 (g y))
⊢ Tendsto (Prod.map f g) (𝓝[s ×ˢ t] (x, y)) (𝓝 (Prod.map f g (x, y)))

Tactic:
rw [nhdsWithin_prod_eq, Prod.map, nhds_prod_eq]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → γ
g : β → δ
s : Set α
t : Set β
x : α
y : β
hf : Tendsto f (𝓝[s] x) (𝓝 (f x))
hg : Tendsto g (𝓝[t] y) (𝓝 (g y))
⊢ Tendsto (Prod.map f g) (𝓝[s] x ×ˢ 𝓝[t] y) (𝓝 (f x) ×ˢ 𝓝 (g y))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → γ
g : β → δ
s : Set α
t : Set β
x : α
y : β
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g t y
⊢ ContinuousWithinAt (Prod.map f g) (s ×ˢ t) (x, y)

Tactic:
unfold ContinuousWithinAt at *

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → γ
g : β → δ
s : Set α
t : Set β
x : α
y : β
hf : Tendsto f (𝓝[s] x) (𝓝 (f x))
hg : Tendsto g (𝓝[t] y) (𝓝 (g y))
⊢ Tendsto (Prod.map f g) (𝓝[s ×ˢ t] (x, y)) (𝓝 (Prod.map f g (x, y)))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → γ
g : β → δ
s : Set α
t : Set β
x : α
y : β
hf : Tendsto f (𝓝[s] x) (𝓝 (f x))
hg : Tendsto g (𝓝[t] y) (𝓝 (g y))
⊢ Tendsto (Prod.map f g) (𝓝[s] x ×ˢ 𝓝[t] y) (𝓝 (f x) ×ˢ 𝓝 (g y))

Tactic:
exact hf.prod_map hg

Result:
no goals