harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem lcm_add (s₁ s₂ : Multiset α) : (s₁ + s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm :=
  Eq.trans (by simp [lcm]) (fold_add _ _ _ _ _)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ s₂ : Multiset α
⊢ (s₁ + s₂).lcm = fold GCDMonoid.lcm (GCDMonoid.lcm 1 1) (s₁ + s₂)

Tactic:
simp [lcm]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
theorem single_comp_single {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (r s : R) :
    (single f r ≫ single g s : Free.of R X ⟶ Free.of R Z) = single (f ≫ g) (r * s)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
r s : R
⊢ ((single f r).sum fun f' s_1 => (single g s).sum fun g' t => single (f' ≫ g') (s_1 * t)) = single (f ≫ g) (r * s)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
r s : R
⊢ single f r ≫ single g s = single (f ≫ g) (r * s)

Tactic:
dsimp [CategoryTheory.categoryFree]

Result:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
r s : R
⊢ ((single f r).sum fun f' s_1 => (single g s).sum fun g' t => single (f' ≫ g') (s_1 * t)) = single (f ≫ g) (r * s)
-- Mathlib/Algebra/Ring/Ext.lean
theorem ext ⦃inst₁ inst₂ : NonAssocRing R⦄
    (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
    (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) :
    inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toNonUnitalNonAssocRing = toNonUnitalNonAssocRing

Tactic:
ext : 1 <;> assumption

Result:
no goals

Proof state:
case mk.mk
R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
toOne✝¹ : One R
one_mul✝¹ : ∀ (a : R), 1 * a = a
mul_one✝¹ : ∀ (a : R), a * 1 = a
toNatCast✝¹ : NatCast R
natCast_zero✝¹ : NatCast.natCast 0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
toIntCast✝ : IntCast R
intCast_ofNat✝ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
h₂ : toNonAssocSemiring = toNonAssocSemiring
h₃ : toAddCommGroupWithOne = toAddCommGroupWithOne
⊢ mk one_mul✝¹ mul_one✝¹ natCast_zero✝¹ natCast_succ✝¹ intCast_ofNat✝¹ intCast_negSucc✝¹ =
    mk one_mul✝ mul_one✝ natCast_zero✝ natCast_succ✝ intCast_ofNat✝ intCast_negSucc✝

Tactic:
congr <;> solve| injection h₁ | injection h₂ | injection h₃

Result:
no goals

Proof state:
R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
⊢ toNonAssocSemiring = toNonAssocSemiring

Tactic:
ext : 1 <;> assumption

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem map_findSome? (f : α → Option β) (g : β → γ) (l : Vector α n) :
    (l.findSome? f).map g = l.findSome? (Option.map g ∘ f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → Option β
g : β → γ
l : Vector α n
⊢ Option.map g (findSome? f l) = findSome? (Option.map g ∘ f) l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → Option β
g : β → γ
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Option.map g (findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    findSome? (Option.map g ∘ f) { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → Option β
g : β → γ
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Option.map g (findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    findSome? (Option.map g ∘ f) { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
lemma orthogonal_eq_bot_iff
    (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) (b₃ : B.Nondegenerate) :
    B.orthogonal W = ⊥ ↔ W = ⊤

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
h : W = ⊤
x : V
hx : x ∈ B.orthogonal ⊤
y : V
⊢ (B y) x = 0

Tactic:
simpa using hx y

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
h : W = ⊤
⊢ B.orthogonal W = ⊥

Tactic:
rw [h, eq_bot_iff]

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
h : W = ⊤
⊢ B.orthogonal ⊤ ≤ ⊥

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
h : W = ⊤
⊢ B.orthogonal ⊤ ≤ ⊥

Tactic:
exact fun x hx ↦ b₃ x fun y ↦ b₁ y x <| by simpa using hx y

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
⊢ B.orthogonal W = ⊥ ↔ W = ⊤

Tactic:
refine ⟨eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot b₁ b₂, fun h ↦ ?_⟩

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
h : W = ⊤
⊢ B.orthogonal W = ⊥
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem X_pow_mul_monomial (k n : ℕ) (r : R) : X ^ k * monomial n r = monomial (n + k) r

Proof state:
R : Type u
inst✝ : Semiring R
k n : ℕ
r : R
⊢ X ^ k * (monomial n) r = (monomial (n + k)) r

Tactic:
rw [X_pow_mul, monomial_mul_X_pow]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
@[to_additive] lemma min_lt_max_of_mul_lt_mul
    [MulLeftMono α] [MulRightMono α]
    (h : a * b < c * d) : min a b < max c d

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
h : a * b < c * d
⊢ a ⊓ b < c ⊔ d

Tactic:
simp_rw [min_lt_iff, lt_max_iff]

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
h : a * b < c * d
⊢ (a < c ∨ a < d) ∨ b < c ∨ b < d

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
h : a * b < c * d
⊢ (a < c ∨ a < d) ∨ b < c ∨ b < d

Tactic:
contrapose! h

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
h : (c ≤ a ∧ d ≤ a) ∧ c ≤ b ∧ d ≤ b
⊢ c * d ≤ a * b

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
h : (c ≤ a ∧ d ≤ a) ∧ c ≤ b ∧ d ≤ b
⊢ c * d ≤ a * b

Tactic:
exact mul_le_mul' h.1.1 h.2.2

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem padicNorm_of_prime_of_ne {q : ℕ} [p_prime : Fact p.Prime] [q_prime : Fact q.Prime]
    (neq : p ≠ q) : padicNorm p q = 1

Proof state:
p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
neq : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ padicNorm p✝ ↑q = 1

Tactic:
rw [padicNorm, p]

Result:
p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
neq : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ (if ↑q = 0 then 0 else ↑p✝ ^ (-0)) = 1

Proof state:
p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
neq : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ (if ↑q = 0 then 0 else ↑p✝ ^ (-0)) = 1

Tactic:
simp [q_prime.1.ne_zero]

Result:
no goals

Proof state:
p q : ℕ
p_prime : Fact (Nat.Prime p)
q_prime : Fact (Nat.Prime q)
neq : p ≠ q
⊢ padicNorm p ↑q = 1

Tactic:
have p : padicValRat p q = 0 := mod_cast padicValNat_primes neq

Result:
p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
neq : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ padicNorm p✝ ↑q = 1
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_zero (f : R[X]) : taylor 0 f = f

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (taylor 0) f = f

Tactic:
rw [taylor_zero', LinearMap.id_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
/-- `Finset.expect_equiv` is a specialization of `Finset.expect_bij` that automatically fills in
most arguments. -/
lemma expect_equiv (e : ι ≃ κ) (hst : ∀ i, i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) :
    𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Proof state:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
t : Finset κ
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Tactic:
simp_rw [expect, card_equiv e hst, sum_equiv e hst hfg]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Colon.lean
theorem annihilator_quotient {N : Submodule R M} :
    Module.annihilator R (M ⧸ N) = N.colon ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ Module.annihilator R (M ⧸ N) = N.colon ⊤

Tactic:
simp_rw [SetLike.ext_iff, Module.mem_annihilator, ← annihilator_map_mkQ_eq_colon, mem_annihilator,
  map_top, LinearMap.range_eq_top.mpr (mkQ_surjective N), mem_top, forall_true_left,
  forall_const]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem Finset.aemeasurable_prod (s : Finset ι) (hf : ∀ i ∈ s, AEMeasurable (f i) μ) :
    AEMeasurable (fun a => ∏ i ∈ s, f i a) μ

Proof state:
M : Type u_2
ι : Type u_3
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, AEMeasurable (f i) μ
⊢ AEMeasurable (fun a => ∏ i ∈ s, f i a) μ

Tactic:
simpa only [← Finset.prod_apply] using s.aemeasurable_prod' hf

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean
theorem epi_of_epi_of_epi_of_mono (hR₁ : R₁.Exact) (hR₂ : R₂.Exact)
    (h₀ : Epi (app' φ 0)) (h₂ : Epi (app' φ 2)) (h₃ : Mono (app' φ 3)) :
    Epi (app' φ 1) :=
  epi_of_epi_of_epi_of_mono' φ (hR₁.exact 1).exact_toComposableArrows
    (hR₂.exact 0).exact_toComposableArrows
    (by simpa only [R₂.map'_comp 1 2 3] using hR₂.toIsComplex.zero 1) h₀ h₂ h₃

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
h₀ : Epi (app' φ 0 ⋯)
h₂ : Epi (app' φ 2 ⋯)
h₃ : Mono (app' φ 3 ⋯)
⊢ R₂.map' 1 3 ⋯ ⋯ = 0

Tactic:
simpa only [R₂.map'_comp 1 2 3] using hR₂.toIsComplex.zero 1

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem ball_mul : ball x δ * s = x • thickening δ s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ ball x δ * s = x • thickening δ s

Tactic:
rw [mul_comm, mul_ball]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem toOrderMonoidHom_injective : Injective (toOrderMonoidHom : _ → α →*o β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulZeroOneClass α
inst✝ : MulZeroOneClass β
f g : α →*₀o β
h : f.toOrderMonoidHom = g.toOrderMonoidHom
⊢ ∀ (a : α), f a = g a

Tactic:
convert DFunLike.ext_iff.1 h using 0

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Spaces.lean
theorem pretopology_ofGrothendieck :
    Pretopology.ofGrothendieck _ (Opens.grothendieckTopology T) = Opens.pretopology T

Proof state:
case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)).coverings X
x : T
hx : x ∈ X
⊢ ∃ U f, R f ∧ x ∈ U

Tactic:
rcases hR x hx with ⟨U, f, ⟨V, g₁, g₂, hg₂, _⟩, hU⟩

Result:
case a.intro.intro.intro.intro.intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)).coverings X
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hU : x ∈ U
V : Opens T
g₁ : U ⟶ V
g₂ : V ⟶ X
hg₂ : R g₂
right✝ : g₁ ≫ g₂ = f
⊢ ∃ U f, R f ∧ x ∈ U

Proof state:
case a
T : Type u
inst✝ : TopologicalSpace T
⊢ pretopology T ≤ Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)

Tactic:
intro X R hR x hx

Result:
case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ (pretopology T).coverings X
x : T
hx : x ∈ X
⊢ ∃ U f, (Sieve.generate R).arrows f ∧ x ∈ U

Proof state:
case a.intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ (pretopology T).coverings X
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : R f
hU : x ∈ U
⊢ ∃ U f, (Sieve.generate R).arrows f ∧ x ∈ U

Tactic:
exact ⟨U, f, Sieve.le_generate R U hf, hU⟩

Result:
no goals

Proof state:
case a.intro.intro.intro.intro.intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)).coverings X
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hU : x ∈ U
V : Opens T
g₁ : U ⟶ V
g₂ : V ⟶ X
hg₂ : R g₂
right✝ : g₁ ≫ g₂ = f
⊢ ∃ U f, R f ∧ x ∈ U

Tactic:
exact ⟨V, g₂, hg₂, g₁.le hU⟩

Result:
no goals

Proof state:
case a
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T) ≤ pretopology T

Tactic:
intro X R hR x hx

Result:
case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)).coverings X
x : T
hx : x ∈ X
⊢ ∃ U f, R f ∧ x ∈ U

Proof state:
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T) = pretopology T

Tactic:
apply le_antisymm

Result:
case a
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T) ≤ pretopology T

case a
T : Type u
inst✝ : TopologicalSpace T
⊢ pretopology T ≤ Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)

Proof state:
case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ (pretopology T).coverings X
x : T
hx : x ∈ X
⊢ ∃ U f, (Sieve.generate R).arrows f ∧ x ∈ U

Tactic:
rcases hR x hx with ⟨U, f, hf, hU⟩

Result:
case a.intro.intro.intro
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ (pretopology T).coverings X
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : R f
hU : x ∈ U
⊢ ∃ U f, (Sieve.generate R).arrows f ∧ x ∈ U
-- Mathlib/Data/Finsupp/Weight.lean
theorem weight_single_one_apply [DecidableEq σ] (s : σ) (f : σ →₀ R) :
    weight (Pi.single s 1) f = f s

Proof state:
σ : Type u_1
R : Type u_3
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
s : σ
f : σ →₀ R
⊢ (weight (Pi.single s 1)) f = f s

Tactic:
rw [weight_single_index, smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/CompatiblePlus.lean
theorem toPlus_comp_plusCompIso_inv :
    J.toPlus _ ≫ (J.plusCompIso F P).inv = whiskerRight (J.toPlus _) _

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
⊢ J.toPlus (P ⋙ F) ≫ (J.plusCompIso F P).inv = whiskerRight (J.toPlus P) F

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem decide_eq_false {b : Bool} [Decidable (b = false)] : decide (b = false) = !b

Proof state:
b : Bool
inst✝ : Decidable (b = false)
⊢ decide (b = false) = !b

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_monomial_mul (n : ℕ) :
    (monomial n r * p).smeval x = r • (x ^ n * p.smeval x)

Proof state:
case h_add
R : Type u_1
inst✝⁵ : Semiring R
r✝ : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
r s : R[X]
hr : ((monomial n) r✝ * r).smeval x = r✝ • (x ^ n * r.smeval x)
hs : ((monomial n) r✝ * s).smeval x = r✝ • (x ^ n * s.smeval x)
⊢ ((monomial n) r✝ * (r + s)).smeval x = r✝ • (x ^ n * (r + s).smeval x)

Tactic:
simp only [add_comp, hr, hs, smeval_add, add_mul]

Result:
case h_add
R : Type u_1
inst✝⁵ : Semiring R
r✝ : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
r s : R[X]
hr : ((monomial n) r✝ * r).smeval x = r✝ • (x ^ n * r.smeval x)
hs : ((monomial n) r✝ * s).smeval x = r✝ • (x ^ n * s.smeval x)
⊢ ((monomial n) r✝ * (r + s)).smeval x = r✝ • (x ^ n * (r.smeval x + s.smeval x))

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
r : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ ((monomial n) r * p).smeval x = r • (x ^ n * p.smeval x)

Tactic:
induction p using Polynomial.induction_on' with
| h_add r s hr hs =>
  simp only [add_comp, hr, hs, smeval_add, add_mul]
  rw [← C_mul_X_pow_eq_monomial, mul_assoc, smeval_C_mul, smeval_X_pow_mul, smeval_add]
| h_monomial n a =>
  rw [smeval_monomial, monomial_mul_monomial, smeval_monomial, npow_add, mul_smul, mul_smul_comm]

Result:
no goals

Proof state:
case h_monomial
R : Type u_1
inst✝⁵ : Semiring R
r : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n✝ n : ℕ
a : R
⊢ ((monomial n✝) r * (monomial n) a).smeval x = r • (x ^ n✝ * ((monomial n) a).smeval x)

Tactic:
rw [smeval_monomial, monomial_mul_monomial, smeval_monomial, npow_add, mul_smul, mul_smul_comm]

Result:
no goals

Proof state:
case h_add
R : Type u_1
inst✝⁵ : Semiring R
r✝ : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
r s : R[X]
hr : ((monomial n) r✝ * r).smeval x = r✝ • (x ^ n * r.smeval x)
hs : ((monomial n) r✝ * s).smeval x = r✝ • (x ^ n * s.smeval x)
⊢ ((monomial n) r✝ * (r + s)).smeval x = r✝ • (x ^ n * (r.smeval x + s.smeval x))

Tactic:
rw [← C_mul_X_pow_eq_monomial, mul_assoc, smeval_C_mul, smeval_X_pow_mul, smeval_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ
     (x y i : Nat) (c : Bool) : x % 2^i + (y % 2^i + c.toNat) < 2^(i+1)

Proof state:
x y i : Nat
c : Bool
this : c.toNat ≤ 1
⊢ x % 2 ^ i + (y % 2 ^ i + c.toNat) < 2 ^ (i + 1)

Tactic:
rw [Nat.pow_succ]

Result:
x y i : Nat
c : Bool
this : c.toNat ≤ 1
⊢ x % 2 ^ i + (y % 2 ^ i + c.toNat) < 2 ^ i * 2

Proof state:
x y i : Nat
c : Bool
⊢ x % 2 ^ i + (y % 2 ^ i + c.toNat) < 2 ^ (i + 1)

Tactic:
have : c.toNat ≤ 1 := Bool.toNat_le c

Result:
x y i : Nat
c : Bool
this : c.toNat ≤ 1
⊢ x % 2 ^ i + (y % 2 ^ i + c.toNat) < 2 ^ (i + 1)

Proof state:
x y i : Nat
c : Bool
this : c.toNat ≤ 1
⊢ x % 2 ^ i + (y % 2 ^ i + c.toNat) < 2 ^ i * 2

Tactic:
omega

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp]
lemma ofENat_toENat_eq_self {a : Cardinal} : toENat a = a ↔ a ≤ ℵ₀

Proof state:
a : Cardinal.{u_1}
⊢ ↑(toENat a) = a ↔ a ≤ ℵ₀

Tactic:
rw [eq_comm, ← enat_gc.exists_eq_l]

Result:
a : Cardinal.{u_1}
⊢ (∃ a_1, a = ↑a_1) ↔ a ≤ ℵ₀

Proof state:
a : Cardinal.{u_1}
⊢ (∃ a_1, a = ↑a_1) ↔ a ≤ ℵ₀

Tactic:
simpa only [mem_range, eq_comm] using Set.ext_iff.1 range_ofENat a

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem reverse_attachWith {P : α → Prop} {xs : Vector α n}
    {H : ∀ (a : α), a ∈ xs → P a} :
    (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h)))

Proof state:
α : Type ?u.58821
n : Nat
P : α → Prop
xs : Vector α n
H : ∀ (a : α), a ∈ xs → P a
a : α
h : a ∈ xs.reverse
⊢ a ∈ xs

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
n : Nat
P : α → Prop
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → P a
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith P H).reverse =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse.attachWith P ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
P : α → Prop
xs : Vector α n
H : ∀ (a : α), a ∈ xs → P a
⊢ (xs.attachWith P H).reverse = xs.reverse.attachWith P ⋯

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : Nat
P : α → Prop
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → P a
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith P H).reverse =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse.attachWith P ⋯
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
@[simp]
lemma equivPullbackObj_symm_apply_snd (x : Types.PullbackObj f g) :
    c.snd ((equivPullbackObj hc).symm x) = x.1.2

Proof state:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : Types.PullbackObj f g
⊢ c.snd ((equivPullbackObj hc).symm x) = (↑x).2

Tactic:
obtain ⟨x, rfl⟩ := (equivPullbackObj hc).surjective x

Result:
case intro
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : c.pt
⊢ c.snd ((equivPullbackObj hc).symm ((equivPullbackObj hc) x)) = (↑((equivPullbackObj hc) x)).2

Proof state:
case intro
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : c.pt
⊢ c.snd ((equivPullbackObj hc).symm ((equivPullbackObj hc) x)) = (↑((equivPullbackObj hc) x)).2

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem dist_coe_le (z w : ℍ) : dist (z : ℂ) w ≤ w.im * (Real.exp (dist z w) - 1) :=
  calc
    dist (z : ℂ) w ≤ dist (z : ℂ) (w.center (dist z w)) + dist (w : ℂ) (w.center (dist z w)) :=
      dist_triangle_right _ _ _
    _ = w.im * (Real.exp (dist z w) - 1)

Proof state:
z w : ℍ
⊢ dist ↑z ↑(w.center (dist z w)) + dist ↑w ↑(w.center (dist z w)) = w.im * (rexp (dist z w) - 1)

Tactic:
rw [dist_center_dist, dist_self_center, ← mul_add, ← add_sub_assoc, Real.sinh_add_cosh]

Result:
no goals