harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive sub_one_zsmul]
lemma zpow_sub_one (a : G) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ :=
  calc
    a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹ := (mul_inv_cancel_right _ _).symm
    _ = a ^ n * a⁻¹

Proof state:
G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹

Tactic:
rw [← zpow_add_one, Int.sub_add_cancel]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infEdist_pos_iff_not_mem_closure {x : α} {E : Set α} :
    0 < infEdist x E ↔ x ∉ closure E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
⊢ 0 < infEdist x E ↔ x ∉ closure E

Tactic:
rw [mem_closure_iff_infEdist_zero, pos_iff_ne_zero]

Result:
no goals
-- Mathlib/Data/Nat/BinaryRec.lean
theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false

Proof state:
n : Nat
b : Bool
⊢ bit b n = 0 ↔ n = 0 ∧ b = false

Tactic:
cases n <;> cases b <;> simp [bit, Nat.shiftLeft_succ, Nat.two_mul, ← Nat.add_assoc]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem isEquiv_iff_val_sub_one_lt_one [LinearOrderedCommGroupWithZero Γ₀]
    [LinearOrderedCommGroupWithZero Γ'₀] {v : Valuation K Γ₀} {v' : Valuation K Γ'₀} :
    v.IsEquiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1

Proof state:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, v x < 1 ↔ v' x < 1) ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1

Tactic:
exact (Equiv.subRight 1).surjective.forall

Result:
no goals

Proof state:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ v.IsEquiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1

Tactic:
rw [isEquiv_iff_val_lt_one]

Result:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, v x < 1 ↔ v' x < 1) ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1
-- Mathlib/Topology/Constructions.lean
theorem tendsto_subtype_rng {Y : Type*} {p : X → Prop} {l : Filter Y} {f : Y → Subtype p} :
    ∀ {x : Subtype p}, Tendsto f l (𝓝 x) ↔ Tendsto (fun x => (f x : X)) l (𝓝 (x : X))
  | ⟨a, ha⟩ => by rw [nhds_subtype_eq_comap, tendsto_comap_iff]; rfl

Proof state:
X : Type u
inst✝ : TopologicalSpace X
Y : Type u_5
p : X → Prop
l : Filter Y
f : Y → Subtype p
a : X
ha : p a
⊢ Tendsto f l (𝓝 ⟨a, ha⟩) ↔ Tendsto (fun x => ↑(f x)) l (𝓝 ↑⟨a, ha⟩)

Tactic:
rw [nhds_subtype_eq_comap, tendsto_comap_iff]

Result:
X : Type u
inst✝ : TopologicalSpace X
Y : Type u_5
p : X → Prop
l : Filter Y
f : Y → Subtype p
a : X
ha : p a
⊢ Tendsto (Subtype.val ∘ f) l (𝓝 a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝 ↑⟨a, ha⟩)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
Y : Type u_5
p : X → Prop
l : Filter Y
f : Y → Subtype p
a : X
ha : p a
⊢ Tendsto (Subtype.val ∘ f) l (𝓝 a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝 ↑⟨a, ha⟩)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma mul_zero_subset (s : Finset α) : s * 0 ⊆ 0

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
s : Finset α
⊢ s * 0 ⊆ 0

Tactic:
simp [subset_iff, mem_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/LeftDerived.lean
theorem Functor.leftDerived_map_eq (F : C ⥤ D) [F.Additive] (n : ℕ) {X Y : C} (f : X ⟶ Y)
    {P : ProjectiveResolution X} {Q : ProjectiveResolution Y} (g : P.complex ⟶ Q.complex)
    (w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f) :
    (F.leftDerived n).map f =
      (P.isoLeftDerivedObj F n).hom ≫
        (F.mapHomologicalComplex _ ⋙ HomologicalComplex.homologyFunctor _ _ n).map g ≫
          (Q.isoLeftDerivedObj F n).inv

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 Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ g.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f

Tactic:
rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f,
  ChainComplex.single₀_map_f_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 Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (F.leftDerived n).map f =
    (P.isoLeftDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
          g ≫
        (Q.isoLeftDerivedObj F n).inv

Tactic:
rw [← cancel_mono (Q.isoLeftDerivedObj F n).hom,
  ProjectiveResolution.isoLeftDerivedObj_hom_naturality f P Q g _ F n,
  assoc, assoc, Iso.inv_hom_id, comp_id]

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 Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ g.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
-- Mathlib/Data/Sym/Sym2.lean
theorem fromRel_irreflexive {sym : Symmetric r} :
    Irreflexive r ↔ ∀ {z}, z ∈ fromRel sym → ¬IsDiag z :=
  { mp

Proof state:
case h
α : Type u_1
r : α → α → Prop
sym : Symmetric r
h : Irreflexive r
⊢ ∀ (x y : α), s(x, y) ∈ fromRel sym → ¬s(x, y).IsDiag

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
h : Irreflexive r
⊢ ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬z.IsDiag

Tactic:
apply Sym2.ind

Result:
case h
α : Type u_1
r : α → α → Prop
sym : Symmetric r
h : Irreflexive r
⊢ ∀ (x y : α), s(x, y) ∈ fromRel sym → ¬s(x, y).IsDiag

Proof state:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
⊢ Irreflexive r → ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬z.IsDiag

Tactic:
intro h

Result:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
h : Irreflexive r
⊢ ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬z.IsDiag
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem insert_compl_insert (ha : a ∉ s) : insert a (insert a s)ᶜ = sᶜ

Proof state:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ insert a (insert a s)ᶜ = sᶜ

Tactic:
simp_rw [compl_insert, insert_erase (mem_compl.2 ha)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_append_right {as : Vector α n} {bs : Vector α m} {i : Nat} (h : n ≤ i) :
    (as ++ bs)[i]? = bs[i - n]?

Proof state:
case mk
α : Type u_1
m : Nat
bs : Vector α m
i : Nat
as : Array α
h : as.size ≤ i
⊢ ({ toArray := as, size_toArray := ⋯ } ++ bs)[i]? = bs[i - as.size]?

Tactic:
rcases bs with ⟨bs, rfl⟩

Result:
case mk.mk
α : Type u_1
i : Nat
as : Array α
h : as.size ≤ i
bs : Array α
⊢ ({ toArray := as, size_toArray := ⋯ } ++ { toArray := bs, size_toArray := ⋯ })[i]? =
    { toArray := bs, size_toArray := ⋯ }[i - as.size]?

Proof state:
α : Type u_1
n m : Nat
as : Vector α n
bs : Vector α m
i : Nat
h : n ≤ i
⊢ (as ++ bs)[i]? = bs[i - n]?

Tactic:
rcases as with ⟨as, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
bs : Vector α m
i : Nat
as : Array α
h : as.size ≤ i
⊢ ({ toArray := as, size_toArray := ⋯ } ++ bs)[i]? = bs[i - as.size]?

Proof state:
case mk.mk
α : Type u_1
i : Nat
as : Array α
h : as.size ≤ i
bs : Array α
⊢ ({ toArray := as, size_toArray := ⋯ } ++ { toArray := bs, size_toArray := ⋯ })[i]? =
    { toArray := bs, size_toArray := ⋯ }[i - as.size]?

Tactic:
simp [Array.getElem?_append_right, h]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem lift_cof (o) : Cardinal.lift.{u, v} (cof o) = cof (Ordinal.lift.{u, v} o)

Proof state:
o : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ Cardinal.lift.{u, v} (type r).cof = (lift.{u, v} (type r)).cof

Tactic:
rw [← type_uLift, cof_type, cof_type, ← Cardinal.lift_id'.{v, u} (Order.cof _),
  ← Cardinal.lift_umax]

Result:
o : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ Cardinal.lift.{max v u, v} (Order.cof (swap rᶜ)) = Cardinal.lift.{v, max v u} (Order.cof (swap (ULift.down ⁻¹'o r)ᶜ))

Proof state:
o : Ordinal.{v}
⊢ Cardinal.lift.{u, v} o.cof = (lift.{u, v} o).cof

Tactic:
refine inductionOn o fun α r _ ↦ ?_

Result:
o : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ Cardinal.lift.{u, v} (type r).cof = (lift.{u, v} (type r)).cof

Proof state:
o : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ ∀ {a b : α}, swap (ULift.down ⁻¹'o r)ᶜ (Equiv.ulift.symm a) (Equiv.ulift.symm b) ↔ swap rᶜ a b

Tactic:
simp [swap]

Result:
no goals

Proof state:
o : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ Cardinal.lift.{max v u, v} (Order.cof (swap rᶜ)) = Cardinal.lift.{v, max v u} (Order.cof (swap (ULift.down ⁻¹'o r)ᶜ))

Tactic:
apply RelIso.cof_eq_lift ⟨Equiv.ulift.symm, _⟩

Result:
o : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ ∀ {a b : α}, swap (ULift.down ⁻¹'o r)ᶜ (Equiv.ulift.symm a) (Equiv.ulift.symm b) ↔ swap rᶜ a b
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem find?_isNone_iff {p : Fin n → Bool} : (find? p).isNone ↔ ∀ i, ¬ p i

Proof state:
n : Nat
p : Fin n → Bool
⊢ (find? p).isNone = true ↔ ∀ (i : Fin n), ¬p i = true

Tactic:
simp [find?, findSome?_isSome_iff]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
@[simp]
lemma smul_finset_neg (a : α) (t : Finset β) : a • -t = -(a • t)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
a : α
t : Finset β
⊢ a • -t = -(a • t)

Tactic:
simp only [← image_smul, ← image_neg_eq_neg, Function.comp_def, image_image, smul_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.not_not_eq {a b : Bool} : ¬(!a) = b ↔ a = b

Proof state:
a b : Bool
⊢ ¬(!a) = b ↔ a = b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem totient_eq_prod_factorization {n : ℕ} (hn : n ≠ 0) :
    φ n = n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)

Proof state:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.factorization.support
⊢ φ (p ^ n.factorization p) = p ^ (n.factorization p - 1) * (p - 1)

Tactic:
have h := zero_lt_iff.mpr (Finsupp.mem_support_iff.mp hp)

Result:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.factorization.support
h : 0 < n.factorization p
⊢ φ (p ^ n.factorization p) = p ^ (n.factorization p - 1) * (p - 1)

Proof state:
n : ℕ
hn : n ≠ 0
⊢ φ n = n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)

Tactic:
rw [multiplicative_factorization φ (@totient_mul) totient_one hn]

Result:
n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k => φ (p ^ k)) = n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)

Proof state:
n : ℕ
hn : n ≠ 0
⊢ ∀ x ∈ n.factorization.support, φ (x ^ n.factorization x) = x ^ (n.factorization x - 1) * (x - 1)

Tactic:
intro p hp

Result:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.factorization.support
⊢ φ (p ^ n.factorization p) = p ^ (n.factorization p - 1) * (p - 1)

Proof state:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.factorization.support
h : 0 < n.factorization p
⊢ φ (p ^ n.factorization p) = p ^ (n.factorization p - 1) * (p - 1)

Tactic:
rw [totient_prime_pow (prime_of_mem_primeFactors hp) h]

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k => φ (p ^ k)) = n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)

Tactic:
apply Finsupp.prod_congr _

Result:
n : ℕ
hn : n ≠ 0
⊢ ∀ x ∈ n.factorization.support, φ (x ^ n.factorization x) = x ^ (n.factorization x - 1) * (x - 1)
-- Mathlib/Data/Set/Function.lean
lemma InjOn.image_inter {s t u : Set α} (hf : u.InjOn f) (hs : s ⊆ u) (ht : t ⊆ u) :
    f '' (s ∩ t) = f '' s ∩ f '' t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' (s ∩ t) = f '' s ∩ f '' t

Tactic:
apply Subset.antisymm (image_inter_subset _ _ _)

Result:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t ⊆ f '' (s ∩ t)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t ⊆ f '' (s ∩ t)

Tactic:
intro x ⟨⟨y, ys, hy⟩, ⟨z, zt, hz⟩⟩

Result:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ x ∈ f '' (s ∩ t)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ f y = f z

Tactic:
rwa [← hz] at hy

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : y ∈ t
hz : f z = x
this : y = z
⊢ x ∈ f '' (s ∩ t)

Tactic:
exact ⟨y, ⟨ys, zt⟩, hy⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
this : y = z
⊢ x ∈ f '' (s ∩ t)

Tactic:
rw [← this] at zt

Result:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : y ∈ t
hz : f z = x
this : y = z
⊢ x ∈ f '' (s ∩ t)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ x ∈ f '' (s ∩ t)

Tactic:
have : y = z := by
  apply hf (hs ys) (ht zt)
  rwa [← hz] at hy

Result:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
this : y = z
⊢ x ∈ f '' (s ∩ t)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ y = z

Tactic:
apply hf (hs ys) (ht zt)

Result:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ f y = f z
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_self_left (p₁ p₂ : P) : ∡ p₁ p₁ p₂ = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ : P
⊢ ∡ p₁ p₁ p₂ = 0

Tactic:
simp [oangle]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Basic.lean
@[to_additive]
lemma ofHom_injective {X Y : Type u} [CommGroup X] [CommGroup Y] :
    Function.Injective (fun (f : X →* Y) ↦ ofHom f)

Proof state:
X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
⊢ Function.Injective fun f => ofHom f

Tactic:
intro _ _ h

Result:
X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
a₁✝ a₂✝ : X →* Y
h : (fun f => ofHom f) a₁✝ = (fun f => ofHom f) a₂✝
⊢ a₁✝ = a₂✝

Proof state:
X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
a₁✝ a₂✝ : X →* Y
h : (fun f => ofHom f) a₁✝ = (fun f => ofHom f) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext

Result:
case h
X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
a₁✝ a₂✝ : X →* Y
h : (fun f => ofHom f) a₁✝ = (fun f => ofHom f) a₂✝
x✝ : X
⊢ a₁✝ x✝ = a₂✝ x✝

Proof state:
case h
X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
a₁✝ a₂✝ : X →* Y
h : (fun f => ofHom f) a₁✝ = (fun f => ofHom f) a₂✝
x✝ : X
⊢ a₁✝ x✝ = a₂✝ x✝

Tactic:
apply ConcreteCategory.congr_hom h

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
@[simp]
lemma coe_dual_one :
    (dual A K (1 : FractionalIdeal B⁰ L) : Submodule B L) = 1ᵛ

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
⊢ ↑(dual A K 1) = 1ᵛ

Tactic:
rw [← coe_one, coe_dual]

Result:
case hI
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
⊢ 1 ≠ 0

Proof state:
case hI
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem derivedLitsInvariant_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
    (rupHints : Array Nat)
    (f'_assignments_size : (performRupCheck f rupHints).1.assignments.size = n) :
    let rupCheckRes := performRupCheck f rupHints
    DerivedLitsInvariant f f_assignments_size rupCheckRes.1.assignments f'_assignments_size rupCheckRes.2.1

Proof state:
case h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
l : Literal (PosFin n)
l_in_nil : l ∈ (f.assignments, [], false, false).snd.fst
⊢ l.fst.val ≠ ↑i

Tactic:
simp only [List.find?, List.not_mem_nil] at l_in_nil

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ motive 0 (f.assignments, [], false, false)

Tactic:
apply Exists.intro f_assignments_size

Result:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ f.DerivedLitsInvariant f_assignments_size (f.assignments, [], false, false).fst f_assignments_size
    (f.assignments, [], false, false).snd.fst
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem single_add (a : G) (b₁ b₂ : k) : single a (b₁ + b₂) = single a b₁ + single a b₂

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : G
b₁ b₂ : k
⊢ single a (b₁ + b₂) = single a b₁ + single a b₂

Tactic:
simp_rw [single, Finsupp.single_add]

Result:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : G
b₁ b₂ : k
⊢ { toFinsupp := Finsupp.single a b₁ + Finsupp.single a b₂ } =
    { toFinsupp := Finsupp.single a b₁ } + { toFinsupp := Finsupp.single a b₂ }

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : G
b₁ b₂ : k
⊢ { toFinsupp := Finsupp.single a b₁ + Finsupp.single a b₂ } =
    { toFinsupp := Finsupp.single a b₁ } + { toFinsupp := Finsupp.single a b₂ }

Tactic:
rw [← toFinsupp_add]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem w_integral {D : ℝ} (Dpos : 0 < D) : ∫ x : E, w D x ∂μ = 1

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ ∫ (x : E), w D x ∂μ = 1

Tactic:
simp_rw [w, integral_smul]

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ ((∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E)⁻¹ • ∫ (a : E), u (D⁻¹ • a) ∂μ = 1

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ ((∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E)⁻¹ • ∫ (a : E), u (D⁻¹ • a) ∂μ = 1

Tactic:
rw [integral_comp_inv_smul_of_nonneg μ (u : E → ℝ) Dpos.le, abs_of_nonneg Dpos.le, mul_comm]

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ (D ^ finrank ℝ E * ∫ (x : E), u x ∂μ)⁻¹ • D ^ finrank ℝ E • ∫ (x : E), u x ∂μ = 1

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ (D ^ finrank ℝ E * ∫ (x : E), u x ∂μ)⁻¹ • D ^ finrank ℝ E • ∫ (x : E), u x ∂μ = 1

Tactic:
field_simp [(u_int_pos E).ne']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_map' (f : β₁ → β₂) (g : α → β₂ → α) (l : Array β₁) (init : α) (w : stop = l.size) :
    (l.map f).foldl g init 0 stop = l.foldl (fun x y => g x (f y)) init

Proof state:
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
stop : Nat
f : β₁ → β₂
g : α → β₂ → α
l : Array β₁
init : α
w : stop = l.size
⊢ foldl g init (map f l) 0 stop = foldl (fun x y => g x (f y)) init l

Tactic:
subst w

Result:
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g : α → β₂ → α
l : Array β₁
init : α
⊢ foldl g init (map f l) 0 l.size = foldl (fun x y => g x (f y)) init l

Proof state:
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g : α → β₂ → α
l : Array β₁
init : α
⊢ foldl g init (map f l) 0 l.size = foldl (fun x y => g x (f y)) init l

Tactic:
cases l

Result:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g : α → β₂ → α
init : α
toList✝ : List β₁
⊢ foldl g init (map f { toList := toList✝ }) 0 { toList := toList✝ }.size =
    foldl (fun x y => g x (f y)) init { toList := toList✝ }

Proof state:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g : α → β₂ → α
init : α
toList✝ : List β₁
⊢ foldl g init (map f { toList := toList✝ }) 0 { toList := toList✝ }.size =
    foldl (fun x y => g x (f y)) init { toList := toList✝ }

Tactic:
simp [List.foldl_map]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem map_refl : map (OrderIso.refl α) = OrderIso.refl _

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ map (OrderIso.refl α) = OrderIso.refl (LowerSet α)

Tactic:
ext

Result:
case h.h.a.h
α : Type u_1
inst✝ : Preorder α
x✝¹ : LowerSet α
x✝ : α
⊢ x✝ ∈ ↑((map (OrderIso.refl α)) x✝¹) ↔ x✝ ∈ ↑((OrderIso.refl (LowerSet α)) x✝¹)

Proof state:
case h.h.a.h
α : Type u_1
inst✝ : Preorder α
x✝¹ : LowerSet α
x✝ : α
⊢ x✝ ∈ ↑((map (OrderIso.refl α)) x✝¹) ↔ x✝ ∈ ↑((OrderIso.refl (LowerSet α)) x✝¹)

Tactic:
simp

Result:
no goals