harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProd_restrict_right {t : Set γ} (ht : MeasurableSet t) :
    κ ⊗ₖ Kernel.restrict η ht = Kernel.restrict (κ ⊗ₖ η) (MeasurableSet.univ.prod ht)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
⊢ κ ⊗ₖ η.restrict ht = κ.restrict ?hs ⊗ₖ η.restrict ?ht

Tactic:
congr

Result:
case e_κ
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
⊢ κ = κ.restrict ?hs

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
⊢ κ ⊗ₖ η.restrict ht = (κ ⊗ₖ η).restrict ⋯

Tactic:
rw [← compProd_restrict]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
⊢ κ ⊗ₖ η.restrict ht = κ.restrict ?hs ⊗ₖ η.restrict ?ht

case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
⊢ MeasurableSet Set.univ

case ht
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
⊢ MeasurableSet t

Proof state:
case e_κ
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
⊢ κ = κ.restrict ?hs

Tactic:
exact Kernel.restrict_univ.symm

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_prod_mk' (f : α → M × N) :
    mulSupport f = (mulSupport fun x => (f x).1) ∪ mulSupport fun x => (f x).2

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : One M
inst✝ : One N
f : α → M × N
⊢ mulSupport f = (mulSupport fun x => (f x).1) ∪ mulSupport fun x => (f x).2

Tactic:
simp only [← mulSupport_prod_mk]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.lean
theorem PreservesLimitPair.iso_inv_fst :
    (PreservesLimitPair.iso G X Y).inv ≫ G.map prod.fst = prod.fst

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ (iso G X Y).inv ≫ G.map prod.fst = prod.fst

Tactic:
rw [← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y), ← Category.assoc, Iso.hom_inv_id]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.fst = (iso G X Y).hom ≫ prod.fst

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.fst = (iso G X Y).hom ≫ prod.fst

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_natCast (x : ℝ) (n : ℕ) : x ^ (n : ℝ) = x ^ n

Proof state:
x : ℝ
n : ℕ
⊢ x ^ ↑n = x ^ n

Tactic:
simpa using rpow_intCast x n

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem le_logb_iff_rpow_le_of_base_lt_one (hy : 0 < y) : x ≤ logb b y ↔ y ≤ b ^ x

Proof state:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ x ≤ logb b y ↔ y ≤ b ^ x

Tactic:
rw [← rpow_le_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hy]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem and_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    (lhs' && rhs') = (lhs && rhs)

Proof state:
lhs rhs lhs' rhs' : Bool
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ (lhs' && rhs') = (lhs && rhs)

Tactic:
simp[*]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_ne_zero_eval_zero {n : ℕ} (h : n ≠ 0) : (ascPochhammer S n).eval 0 = 0

Proof state:
S : Type u
inst✝ : Semiring S
n : ℕ
h : n ≠ 0
⊢ eval 0 (ascPochhammer S n) = 0

Tactic:
simp [ascPochhammer_eval_zero, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List ((a : α) × β a)} {k : α}
    (h₁ : (l.map Sigma.fst).contains k = false)
    {h'} :
    (m.insertMany l).1.getKey k h' =
    m.getKey k (contains_of_contains_insertMany_list _ h h' h₁)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List ((a : α) × β a)
k : α
h₁ : (List.map Sigma.fst l).contains k = false
h' : (m.insertMany l).val.contains k = true
⊢ (m.insertMany l).val.getKey k h' = m.getKey k ⋯

Tactic:
simp_to_model [insertMany] using List.getKey_insertList_of_contains_eq_false

Result:
no goals
-- Mathlib/NumberTheory/SumTwoSquares.lean
theorem sq_add_sq_mul {R} [CommRing R] {a b x y u v : R} (ha : a = x ^ 2 + y ^ 2)
    (hb : b = u ^ 2 + v ^ 2) : ∃ r s : R, a * b = r ^ 2 + s ^ 2 :=
  ⟨x * u - y * v, x * v + y * u, by rw [ha, hb]; ring⟩

Proof state:
R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ (x ^ 2 + y ^ 2) * (u ^ 2 + v ^ 2) = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ a * b = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2

Tactic:
rw [ha, hb]

Result:
R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ (x ^ 2 + y ^ 2) * (u ^ 2 + v ^ 2) = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem toList_replace [BEq α] {l : AssocList α β} {a : α} {b : β a} :
    (l.replace a b).toList = replaceEntry a b l.toList

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
b : β a
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (replace a b tail✝).toList = replaceEntry a b tail✝.toList
⊢ (replace a b (cons key✝ value✝ tail✝)).toList = replaceEntry a b (cons key✝ value✝ tail✝).toList

Tactic:
next k v t ih => cases h : k == a <;> simp_all [replace, List.replaceEntry_cons]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : AssocList α β
a : α
b : β a
⊢ (replace a b l).toList = replaceEntry a b l.toList

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
b : β a
⊢ (replace a b nil).toList = replaceEntry a b nil.toList

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
b : β a
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (replace a b tail✝).toList = replaceEntry a b tail✝.toList
⊢ (replace a b (cons key✝ value✝ tail✝)).toList = replaceEntry a b (cons key✝ value✝ tail✝).toList

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
b : β a
⊢ (replace a b nil).toList = replaceEntry a b nil.toList

Tactic:
simp [replace]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
b : β a
k : α
v : β k
t : AssocList α β
ih : (replace a b t).toList = replaceEntry a b t.toList
⊢ (replace a b (cons k v t)).toList = replaceEntry a b (cons k v t).toList

Tactic:
cases h : k == a <;> simp_all [replace, List.replaceEntry_cons]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_eq_half_mul_C_comp_two_mul_X [Invertible (2 : R)] (n : ℤ) :
    T R n = Polynomial.C ⅟2 * (C R n).comp (2 * X)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
⊢ T R n = Polynomial.C ⅟2 * (C R n).comp (2 * X)

Tactic:
rw [C_comp_two_mul_X, ← mul_assoc, ← map_ofNat Polynomial.C 2, ← map_mul, invOf_mul_self',
  map_one, one_mul]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem toFinset_inter (s t : Multiset α) : toFinset (s ∩ t) = toFinset s ∩ toFinset t :=
  Finset.ext <| by simp

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ ∀ (a : α), a ∈ (s ∩ t).toFinset ↔ a ∈ s.toFinset ∩ t.toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem forIn_eq_forIn_toList [Monad m]
    (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
    forIn as b f = forIn as.toList b f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
as : Array α
b : β
f : α → β → m (ForInStep β)
⊢ forIn as b f = forIn as.toList b f

Tactic:
cases as

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b : β
f : α → β → m (ForInStep β)
toList✝ : List α
⊢ forIn { toList := toList✝ } b f = forIn { toList := toList✝ }.toList b f

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b : β
f : α → β → m (ForInStep β)
toList✝ : List α
⊢ forIn { toList := toList✝ } b f = forIn { toList := toList✝ }.toList b f

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option β → Option β}
    (h : k ∉ m) (h' : (f (Const.get? m k)).isSome) :
    (Const.alter m k f).size = m.size + 1

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : ¬k ∈ m
h' : (f (get? m k)).isSome = true
⊢ (alter m k f).size = m.size + 1

Tactic:
rw [mem_iff_contains, Bool.not_eq_true] at h

Result:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.contains k = false
h' : (f (get? m k)).isSome = true
⊢ (alter m k f).size = m.size + 1

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.contains k = false
h' : (f (get? m k)).isSome = true
⊢ (alter m k f).size = m.size + 1

Tactic:
exact Raw₀.Const.size_alter_eq_add_one ⟨m.1, _⟩ m.2 h h'

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Pretopology.lean
lemma sInf_ofGrothendieck (T : Set (GrothendieckTopology C)) :
    ofGrothendieck C (sInf T) = sInf (ofGrothendieck C '' T)

Proof state:
case coverings.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (GrothendieckTopology C)
X : C
S : Presieve X
⊢ S ∈ (ofGrothendieck C (sInf T)).coverings X ↔ S ∈ (sInf (ofGrothendieck C '' T)).coverings X

Tactic:
simp [mem_sInf, mem_ofGrothendieck, GrothendieckTopology.mem_sInf]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (GrothendieckTopology C)
⊢ ofGrothendieck C (sInf T) = sInf (ofGrothendieck C '' T)

Tactic:
ext X S

Result:
case coverings.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (GrothendieckTopology C)
X : C
S : Presieve X
⊢ S ∈ (ofGrothendieck C (sInf T)).coverings X ↔ S ∈ (sInf (ofGrothendieck C '' T)).coverings X
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualPairing_eq (W : Subspace K V₁) :
    W.dualPairing = W.quotAnnihilatorEquiv.toLinearMap

Proof state:
case h.h.h
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
x✝¹ : Dual K V₁
x✝ : ↥W
⊢ ((Submodule.dualPairing W ∘ₗ (dualAnnihilator W).mkQ) x✝¹) x✝ =
    ((↑W.quotAnnihilatorEquiv ∘ₗ (dualAnnihilator W).mkQ) x✝¹) x✝

Tactic:
rfl

Result:
no goals

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ Submodule.dualPairing W = ↑W.quotAnnihilatorEquiv

Tactic:
ext

Result:
case h.h.h
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
x✝¹ : Dual K V₁
x✝ : ↥W
⊢ ((Submodule.dualPairing W ∘ₗ (dualAnnihilator W).mkQ) x✝¹) x✝ =
    ((↑W.quotAnnihilatorEquiv ∘ₗ (dualAnnihilator W).mkQ) x✝¹) x✝
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
lemma dropLast_cons_of_not_nil (h : G.Adj u v) (p : G.Walk v w) (hp : ¬ p.Nil) :
    (cons h p).dropLast = cons h (p.dropLast.copy rfl (penultimate_cons_of_not_nil _ _ hp).symm) :=
  p.notNilRec (by simp) hp h

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
hp : ¬p.Nil
⊢ ∀ {u_1 v w : V} (h : G.Adj u_1 v) (q : G.Walk v w) (x : G.Adj u u_1),
    (cons x (cons h q)).dropLast = cons x ((cons h q).dropLast.copy ⋯ ⋯)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem nat_floor_real_sqrt_eq_nat_sqrt {a : ℕ} : ⌊√(a : ℝ)⌋₊ = Nat.sqrt a

Proof state:
a : ℕ
⊢ ↑a.sqrt ≤ √↑a ∧ √↑a < ↑a.sqrt + 1

Tactic:
exact ⟨nat_sqrt_le_real_sqrt, real_sqrt_lt_nat_sqrt_succ⟩

Result:
no goals

Proof state:
a : ℕ
⊢ ⌊√↑a⌋₊ = a.sqrt

Tactic:
rw [Nat.floor_eq_iff (sqrt_nonneg a)]

Result:
a : ℕ
⊢ ↑a.sqrt ≤ √↑a ∧ √↑a < ↑a.sqrt + 1
-- Mathlib/Order/WellQuasiOrder.lean
theorem wellQuasiOrdered_iff_exists_monotone_subseq [IsPreorder α r] :
    WellQuasiOrdered r ↔ ∀ f : ℕ → α, ∃ g : ℕ ↪o ℕ, ∀ m n : ℕ, m ≤ n → r (f (g m)) (f (g n))

Proof state:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
f : ℕ → α
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
obtain ⟨g, gmon⟩ := h f

Result:
case mpr.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
f : ℕ → α
g : ℕ ↪o ℕ
gmon : ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Proof state:
case mpr.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
f : ℕ → α
g : ℕ ↪o ℕ
gmon : ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
exact ⟨_, _, g.strictMono Nat.zero_lt_one, gmon _ _ (Nat.zero_le 1)⟩

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
⊢ WellQuasiOrdered r ↔ ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
constructor <;> intro h f

Result:
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
f : ℕ → α
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Proof state:
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
exact h.exists_monotone_subseq f

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem intCast_real_norm (x : ℤ[i]) : (x.norm : ℝ) = Complex.normSq (x : ℂ)

Proof state:
x : ℤ[i]
⊢ ↑(x.re * x.re - -1 * x.im * x.im) =
    { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1, map_one' := normSq.proof_2,
        map_mul' := normSq.proof_3 }
      (toComplex x)

Tactic:
simp

Result:
no goals

Proof state:
x : ℤ[i]
⊢ ↑(norm x) = normSq (toComplex x)

Tactic:
rw [Zsqrtd.norm, normSq]

Result:
x : ℤ[i]
⊢ ↑(x.re * x.re - -1 * x.im * x.im) =
    { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1, map_one' := normSq.proof_2,
        map_mul' := normSq.proof_3 }
      (toComplex x)
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub
    {f g : Perm α} (hf : f ∈ g.cycleFactorsFinset) :
    (g * f⁻¹).cycleType = g.cycleType - f.cycleType :=
  add_right_cancel (b := f.cycleType) <| by
    rw [← (disjoint_mul_inv_of_mem_cycleFactorsFinset hf).cycleType, inv_mul_cancel_right,
      tsub_add_cancel_of_le (cycleType_le_of_mem_cycleFactorsFinset hf)]

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
⊢ (g * f⁻¹).cycleType + f.cycleType = g.cycleType - f.cycleType + f.cycleType

Tactic:
rw [← (disjoint_mul_inv_of_mem_cycleFactorsFinset hf).cycleType, inv_mul_cancel_right,
  tsub_add_cancel_of_le (cycleType_le_of_mem_cycleFactorsFinset hf)]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem embDomain_notin_range (h : b ∉ Set.range f) : s.embDomain f b = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
β : Type u_8
s : SummableFamily Γ R α
f : α ↪ β
b : β
h : b ∉ Set.range ⇑f
⊢ (s.embDomain f) b = 0

Tactic:
rw [embDomain_apply, dif_neg h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem tendsto_stirlingSeq_sqrt_pi : Tendsto stirlingSeq atTop (𝓝 (√π))

Proof state:
case intro.intro
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto stirlingSeq atTop (𝓝 √π)

Tactic:
have hπ : π / 2 = a ^ 2 / 2 :=
  tendsto_nhds_unique Wallis.tendsto_W_nhds_pi_div_two (second_wallis_limit a hapos.ne' halimit)

Result:
case intro.intro
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
hπ : π / 2 = a ^ 2 / 2
⊢ Tendsto stirlingSeq atTop (𝓝 √π)

Proof state:
⊢ Tendsto stirlingSeq atTop (𝓝 √π)

Tactic:
obtain ⟨a, hapos, halimit⟩ := stirlingSeq_has_pos_limit_a

Result:
case intro.intro
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto stirlingSeq atTop (𝓝 √π)

Proof state:
case intro.intro
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
hπ : π / 2 = a ^ 2 / 2
⊢ Tendsto stirlingSeq atTop (𝓝 √π)

Tactic:
rwa [(div_left_inj' (two_ne_zero' ℝ)).mp hπ, sqrt_sq hapos.le]

Result:
no goals
-- Mathlib/Data/Matroid/Dual.lean
theorem IsBase.inter_isBasis_iff_compl_inter_isBasis_dual (hB : M.IsBase B)
    (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.IsBasis (B ∩ X) X ↔ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

Tactic:
refine ⟨hB.compl_inter_isBasis_of_inter_isBasis, fun h ↦ ?_⟩

Result:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hX : autoParam (X ⊆ M.E) _auto✝
h : M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ M.IsBasis (B ∩ X) X

Proof state:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hX : autoParam (X ⊆ M.E) _auto✝
h : M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ M.IsBasis (B ∩ X) X

Tactic:
simpa [inter_eq_self_of_subset_right hX, inter_eq_self_of_subset_right hB.subset_ground] using
  hB.compl_isBase_dual.compl_inter_isBasis_of_inter_isBasis h

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
private lemma pairMap_of_snd_mem_fst {t : Finset σ × σ} (h : t.snd ∈ t.fst) :
    pairMap σ t = (t.fst.erase t.snd, t.snd)

Proof state:
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h : t.2 ∈ t.1
⊢ MvPolynomial.NewtonIdentities.pairMap σ t = (t.1.erase t.2, t.2)

Tactic:
simp [pairMap, h]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Ring.lean
theorem tendsto_pow_atTop_iff {n : ℕ} : Tendsto (fun x : α => x ^ n) atTop atTop ↔ n ≠ 0 :=
  ⟨fun h hn => by simp only [hn, pow_zero, not_tendsto_const_atTop] at h, tendsto_pow_atTop⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemiring α
n : ℕ
h : Tendsto (fun x => x ^ n) atTop atTop
hn : n = 0
⊢ False

Tactic:
simp only [hn, pow_zero, not_tendsto_const_atTop] at h

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
@[simp]
lemma homOfDegreewiseSplit_f (n : ℤ) :
    (homOfDegreewiseSplit S σ).f n =
      (cocycleOfDegreewiseSplit S σ).1.v n (n + 1) rfl

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
n : ℤ
⊢ (homOfDegreewiseSplit S σ).f n = (↑(cocycleOfDegreewiseSplit S σ)).v n (n + 1) ⋯

Tactic:
simp [homOfDegreewiseSplit, Cochain.rightShift_v _ _ _ _ _ _ _ _ rfl]

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem of_apply_eq_base (i : ι) (x : H) : of i (φ i x) = base φ x

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ (of i) ((φ i) x) = (base φ) x

Tactic:
rw [← MonoidHom.comp_apply, of_comp_eq_base]

Result:
no goals
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMax.deriv_eq_zero (h : IsLocalMax f a) : deriv f a = 0

Proof state:
f : ℝ → ℝ
a : ℝ
h : IsLocalMax f a
⊢ deriv f a = 0

Tactic:
classical
exact if hf : DifferentiableAt ℝ f a then h.hasDerivAt_eq_zero hf.hasDerivAt
else deriv_zero_of_not_differentiableAt hf

Result:
no goals

Proof state:
f : ℝ → ℝ
a : ℝ
h : IsLocalMax f a
⊢ deriv f a = 0

Tactic:
exact if hf : DifferentiableAt ℝ f a then h.hasDerivAt_eq_zero hf.hasDerivAt
else deriv_zero_of_not_differentiableAt hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : List β) (init : α₁)
    (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init)

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g₁ : α₁ → β → α₁
g₂ : α₂ → β → α₂
l : List β
init : α₁
H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)
⊢ foldl g₂ (f init) l = f (foldl g₁ init l)

Tactic:
induction l generalizing init <;> simp [*, H]

Result:
no goals
-- Mathlib/CategoryTheory/Dialectica/Monoidal.lean
theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : Dial C}
    (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
    tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
    (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ tensorHom (tensorHom f₁ f₂) f₃ ≫ (Y₁.associator Y₂ Y₃).hom =
    (X₁.associator X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem map_smul_left (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : map (r • f) g = r • map f g

Proof state:
case H.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
r : R
f : M →ₗ[R] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ (map (r • f) g)) x✝¹) x✝ = (((mk R M N).compr₂ (r • map f g)) x✝¹) x✝

Tactic:
simp only [smul_tmul, compr₂_apply, mk_apply, map_tmul, smul_apply, tmul_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
r : R
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ map (r • f) g = r • map f g

Tactic:
ext

Result:
case H.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
r : R
f : M →ₗ[R] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ (map (r • f) g)) x✝¹) x✝ = (((mk R M N).compr₂ (r • map f g)) x✝¹) x✝
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem val_eq_one {a : αˣ} : (a : α) = 1 ↔ a = 1

Proof state:
α : Type u
inst✝ : Monoid α
a : αˣ
⊢ ↑a = 1 ↔ a = 1

Tactic:
rw [← Units.val_one, eq_iff]

Result:
no goals