harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem conePointsIsoOfNatIso_inv_comp {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s)
    (Q : IsLimit t) (w : F ≅ G) (j : J) :
    (conePointsIsoOfNatIso P Q w).inv ≫ s.π.app j = t.π.app j ≫ w.inv.app j

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F G : J ⥤ C
s : Cone F
t : Cone G
P : IsLimit s
Q : IsLimit t
w : F ≅ G
j : J
⊢ (P.conePointsIsoOfNatIso Q w).inv ≫ s.π.app j = t.π.app j ≫ w.inv.app j

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_not {x : BitVec v} :
    (~~~x).getMsbD i = (decide (i < v) && ! x.getMsbD i)

Proof state:
v i : Nat
x : BitVec v
⊢ (~~~x).getMsbD i = (decide (i < v) && !x.getMsbD i)

Tactic:
by_cases h' : i < v <;> simp_all [not_def]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem card_support_extend_domain (f : α ≃ Subtype p) {g : Perm α} :
    #(g.extendDomain f).support = #g.support

Proof state:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
⊢ #(g.extendDomain f).support = #g.support

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem card_nat (n : ℕ) : card.{u} n = n

Proof state:
n : ℕ
⊢ (↑n).card = ↑n

Tactic:
induction n <;> [simp; simp only [card_add, card_one, Nat.cast_succ, *]]

Result:
no goals
-- Mathlib/Algebra/Free.lean
theorem traverse_mul (x y : FreeSemigroup α) :
    traverse F (x * y) = (· * ·) <$> traverse F x <*> traverse F y :=
  let ⟨x, L1⟩ := x
  let ⟨y, L2⟩ := y
  List.recOn L1 (fun _ ↦ rfl)
    (fun hd tl ih x ↦ show
        (· * ·) <$> pure <$> F x <*> traverse F (mk hd tl * mk y L2) =
          (· * ·) <$> ((· * ·) <$> pure <$> F x <*> traverse F (mk hd tl)) <*> traverse F (mk y L2)
        by rw [ih]; simp only [Function.comp_def, (mul_assoc _ _ _).symm, functor_norm])
    x

Proof state:
α β : Type u
m : Type u → Type u
inst✝¹ : Applicative m
F : α → m β
inst✝ : LawfulApplicative m
x✝¹ y✝ : FreeSemigroup α
x✝ : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl } * { head := y, tail := L2 }) =
      (fun x1 x2 => x1 * x2) <$> traverse F { head := x, tail := tl } <*> traverse F { head := y, tail := L2 }
x : α
⊢ (fun x1 x2 => x1 * x2) <$> pure <$> F x <*> traverse F ({ head := hd, tail := tl } * { head := y, tail := L2 }) =
    (fun x1 x2 => x1 * x2) <$> ((fun x1 x2 => x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 }

Tactic:
rw [ih]

Result:
α β : Type u
m : Type u → Type u
inst✝¹ : Applicative m
F : α → m β
inst✝ : LawfulApplicative m
x✝¹ y✝ : FreeSemigroup α
x✝ : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl } * { head := y, tail := L2 }) =
      (fun x1 x2 => x1 * x2) <$> traverse F { head := x, tail := tl } <*> traverse F { head := y, tail := L2 }
x : α
⊢ (fun x1 x2 => x1 * x2) <$> pure <$> F x <*>
      ((fun x1 x2 => x1 * x2) <$> traverse F { head := hd, tail := tl } <*> traverse F { head := y, tail := L2 }) =
    (fun x1 x2 => x1 * x2) <$> ((fun x1 x2 => x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 }

Proof state:
α β : Type u
m : Type u → Type u
inst✝¹ : Applicative m
F : α → m β
inst✝ : LawfulApplicative m
x✝¹ y✝ : FreeSemigroup α
x✝ : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl } * { head := y, tail := L2 }) =
      (fun x1 x2 => x1 * x2) <$> traverse F { head := x, tail := tl } <*> traverse F { head := y, tail := L2 }
x : α
⊢ (fun x1 x2 => x1 * x2) <$> pure <$> F x <*>
      ((fun x1 x2 => x1 * x2) <$> traverse F { head := hd, tail := tl } <*> traverse F { head := y, tail := L2 }) =
    (fun x1 x2 => x1 * x2) <$> ((fun x1 x2 => x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 }

Tactic:
simp only [Function.comp_def, (mul_assoc _ _ _).symm, functor_norm]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_dvd_of_mem_zpowers (h : y ∈ Subgroup.zpowers x) : orderOf y ∣ orderOf x

Proof state:
G : Type u_1
inst✝ : Group G
x y : G
h : y ∈ zpowers x
⊢ orderOf y ∣ orderOf x

Tactic:
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp h

Result:
case intro
G : Type u_1
inst✝ : Group G
x : G
k : ℤ
h : x ^ k ∈ zpowers x
⊢ orderOf (x ^ k) ∣ orderOf x

Proof state:
case intro
G : Type u_1
inst✝ : Group G
x : G
k : ℤ
h : x ^ k ∈ zpowers x
⊢ (x ^ k) ^ orderOf x = 1

Tactic:
exact zpow_pow_orderOf

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝ : Group G
x : G
k : ℤ
h : x ^ k ∈ zpowers x
⊢ orderOf (x ^ k) ∣ orderOf x

Tactic:
rw [orderOf_dvd_iff_pow_eq_one]

Result:
case intro
G : Type u_1
inst✝ : Group G
x : G
k : ℤ
h : x ^ k ∈ zpowers x
⊢ (x ^ k) ^ orderOf x = 1
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma ext_from (i j : ℤ) (hij : j + 1 = i) {A : C} {f g : (mappingCone φ).X j ⟶ A}
    (h₁ : (inl φ).v i j (by omega) ≫ f = (inl φ).v i j (by omega) ≫ g)
    (h₂ : (inr φ).f j ≫ f = (inr φ).f j ≫ g) :
    f = g :=
  homotopyCofiber.ext_from_X φ i j hij h₁ h₂

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.59375, u_1} C
inst✝³ : Category.{?u.59379, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : j + 1 = i
A : C
f g : (mappingCone φ).X j ⟶ A
⊢ i + -1 = j

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
lemma range_mapIncl (p : Submodule R P) (q : Submodule R Q) :
    LinearMap.range (mapIncl p q) = Submodule.span R (Set.image2 (· ⊗ₜ ·) p q)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_7
Q : Type u_8
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module R P
p : Submodule R P
q : Submodule R Q
⊢ range (mapIncl p q) = Submodule.span R (Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑p ↑q)

Tactic:
rw [mapIncl, map_range_eq_span_tmul]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_7
Q : Type u_8
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module R P
p : Submodule R P
q : Submodule R Q
⊢ Submodule.span R {t | ∃ m n, p.subtype m ⊗ₜ[R] q.subtype n = t} =
    Submodule.span R (Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑p ↑q)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_7
Q : Type u_8
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module R P
p : Submodule R P
q : Submodule R Q
⊢ Submodule.span R {t | ∃ m n, p.subtype m ⊗ₜ[R] q.subtype n = t} =
    Submodule.span R (Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑p ↑q)

Tactic:
congr

Result:
case e_s
R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_7
Q : Type u_8
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module R P
p : Submodule R P
q : Submodule R Q
⊢ {t | ∃ m n, p.subtype m ⊗ₜ[R] q.subtype n = t} = Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑p ↑q

Proof state:
case e_s
R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_7
Q : Type u_8
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module R P
p : Submodule R P
q : Submodule R Q
⊢ {t | ∃ m n, p.subtype m ⊗ₜ[R] q.subtype n = t} = Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑p ↑q

Tactic:
ext

Result:
case e_s.h
R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_7
Q : Type u_8
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module R P
p : Submodule R P
q : Submodule R Q
x✝ : P ⊗[R] Q
⊢ x✝ ∈ {t | ∃ m n, p.subtype m ⊗ₜ[R] q.subtype n = t} ↔ x✝ ∈ Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑p ↑q

Proof state:
case e_s.h
R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_7
Q : Type u_8
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Module R P
p : Submodule R P
q : Submodule R Q
x✝ : P ⊗[R] Q
⊢ x✝ ∈ {t | ∃ m n, p.subtype m ⊗ₜ[R] q.subtype n = t} ↔ x✝ ∈ Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑p ↑q

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_ne_top_iff : s.encard ≠ ⊤ ↔ s.Finite

Proof state:
α : Type u_1
s : Set α
⊢ s.encard ≠ ⊤ ↔ s.Finite

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Holder.lean
theorem holderOnWith_univ {C r : ℝ≥0} {f : X → Y} : HolderOnWith C r f univ ↔ HolderWith C r f

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
⊢ HolderOnWith C r f univ ↔ HolderWith C r f

Tactic:
simp only [HolderOnWith, HolderWith, mem_univ, true_imp_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
    ¬a ∈ m → getD m a fallback = fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
fallback : β
⊢ ¬a ∈ m → getD m a fallback = fallback

Tactic:
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h

Result:
no goals
-- Mathlib/Probability/Independence/ZeroOne.lean
theorem measure_zero_or_one_of_measurableSet_limsup_atTop
    (h_le : ∀ n, s n ≤ m0)
    (h_indep : iIndep s μ) {t : Set Ω} (ht_tail : MeasurableSet[limsup s atTop] t) :
    μ t = 0 ∨ μ t = 1

Proof state:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s μ
t : Set Ω
ht_tail : MeasurableSet t
⊢ μ t = 0 ∨ μ t = 1

Tactic:
simpa only [ae_dirac_eq, Filter.eventually_pure]
  using Kernel.measure_zero_or_one_of_measurableSet_limsup_atTop h_le h_indep ht_tail

Result:
no goals
-- Mathlib/RepresentationTheory/Invariants.lean
theorem mem_invariants (v : V) : v ∈ invariants ρ ↔ ∀ g : G, ρ g v = v

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
v : V
⊢ v ∈ ρ.invariants ↔ ∀ (g : G), (ρ g) v = v

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : ModuleCat R} (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:
R : Type u
inst✝ : CommRing R
X₁ : ModuleCat R
X₂ : ModuleCat R
X₃ : ModuleCat R
Y₁ : ModuleCat R
Y₂ : ModuleCat R
Y₃ : ModuleCat R
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₃)

Tactic:
ext : 1

Result:
case hf
R : Type u
inst✝ : CommRing R
X₁ : ModuleCat R
X₂ : ModuleCat R
X₃ : ModuleCat R
Y₁ : ModuleCat R
Y₂ : ModuleCat R
Y₃ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom) =
    Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))

Proof state:
case hf
R : Type u
inst✝ : CommRing R
X₁ : ModuleCat R
X₂ : ModuleCat R
X₃ : ModuleCat R
Y₁ : ModuleCat R
Y₂ : ModuleCat R
Y₃ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom) =
    Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))

Tactic:
apply TensorProduct.ext_threefold

Result:
case hf.H
R : Type u
inst✝ : CommRing R
X₁ : ModuleCat R
X₂ : ModuleCat R
X₃ : ModuleCat R
Y₁ : ModuleCat R
Y₂ : ModuleCat R
Y₃ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ∀ (x : ↑X₁) (y : ↑X₂) (z : ↑X₃),
    (Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      (Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
X₁ : ModuleCat R
X₂ : ModuleCat R
X₃ : ModuleCat R
Y₁ : ModuleCat R
Y₂ : ModuleCat R
Y₃ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ∀ (x : ↑X₁) (y : ↑X₂) (z : ↑X₃),
    (Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      (Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Tactic:
intro x y z

Result:
case hf.H
R : Type u
inst✝ : CommRing R
X₁ : ModuleCat R
X₂ : ModuleCat R
X₃ : ModuleCat R
Y₁ : ModuleCat R
Y₂ : ModuleCat R
Y₃ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
x : ↑X₁
y : ↑X₂
z : ↑X₃
⊢ (Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    (Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
X₁ : ModuleCat R
X₂ : ModuleCat R
X₃ : ModuleCat R
Y₁ : ModuleCat R
Y₂ : ModuleCat R
Y₃ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
x : ↑X₁
y : ↑X₂
z : ↑X₃
⊢ (Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    (Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem sInf_adj_of_nonempty {s : Set (SimpleGraph V)} (hs : s.Nonempty) :
    (sInf s).Adj a b ↔ ∀ G ∈ s, Adj G a b :=
  sInf_adj.trans <|
    and_iff_left_of_imp <| by
      obtain ⟨G, hG⟩ := hs
      exact fun h => (h _ hG).ne

Proof state:
V : Type u
a b : V
s : Set (SimpleGraph V)
hs : s.Nonempty
⊢ (∀ G ∈ s, G.Adj a b) → a ≠ b

Tactic:
obtain ⟨G, hG⟩ := hs

Result:
case intro
V : Type u
a b : V
s : Set (SimpleGraph V)
G : SimpleGraph V
hG : G ∈ s
⊢ (∀ G ∈ s, G.Adj a b) → a ≠ b

Proof state:
case intro
V : Type u
a b : V
s : Set (SimpleGraph V)
G : SimpleGraph V
hG : G ∈ s
⊢ (∀ G ∈ s, G.Adj a b) → a ≠ b

Tactic:
exact fun h => (h _ hG).ne

Result:
no goals
-- Mathlib/Computability/Language.lean
theorem map_map (g : β → γ) (f : α → β) (l : Language α) : map g (map f l) = map (g ∘ f) l

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
l : Language α
⊢ (map g) ((map f) l) = (map (g ∘ f)) l

Tactic:
simp [map, image_image]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_mul_cancel_left (a b : G) : a / (a * b) = b⁻¹

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a / (a * b) = b⁻¹

Tactic:
rw [← inv_div, mul_div_cancel_left]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.smul_measure_nnreal {f : α → β} (h : Integrable f μ) {c : ℝ≥0} :
    Integrable f (c • μ)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : Integrable f μ
c : ℝ≥0
⊢ ↑ofNNRealHom.toMonoidWithZeroHom c ≠ ⊤

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : Integrable f μ
c : ℝ≥0
⊢ Integrable f (c • μ)

Tactic:
apply h.smul_measure

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : Integrable f μ
c : ℝ≥0
⊢ ↑ofNNRealHom.toMonoidWithZeroHom c ≠ ⊤
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem comp_zero (g : M₂ →SL[σ₂₃] M₃) : g.comp (0 : M₁ →SL[σ₁₂] M₂) = 0

Proof state:
case h
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
x✝ : M₁
⊢ (g.comp 0) x✝ = 0 x✝

Tactic:
simp

Result:
no goals

Proof state:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
⊢ g.comp 0 = 0

Tactic:
ext

Result:
case h
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
x✝ : M₁
⊢ (g.comp 0) x✝ = 0 x✝
-- Mathlib/SetTheory/Cardinal/Divisibility.lean
theorem not_irreducible_of_aleph0_le (ha : ℵ₀ ≤ a) : ¬Irreducible a

Proof state:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
h : ∀ (a_1 b : Cardinal.{u}), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
⊢ False

Tactic:
simpa [mul_aleph0_eq ha, isUnit_iff, (one_lt_aleph0.trans_le ha).ne', one_lt_aleph0.ne'] using
  h a ℵ₀

Result:
no goals

Proof state:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬Irreducible a

Tactic:
rw [irreducible_iff, not_and_or]

Result:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬¬IsUnit a ∨ ¬∀ (a_1 b : Cardinal.{u}), a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Proof state:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬¬IsUnit a ∨ ¬∀ (a_1 b : Cardinal.{u}), a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Tactic:
refine Or.inr fun h => ?_

Result:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
h : ∀ (a_1 b : Cardinal.{u}), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
⊢ False
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem _root_.IsRelPrime.isCoprime (h : IsRelPrime x y) : IsCoprime x y

Proof state:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
h : IsRelPrime x y
⊢ IsUnit (gcd x y)

Tactic:
exact h (gcd_dvd_left x y) (gcd_dvd_right x y)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
h : IsRelPrime x y
⊢ IsCoprime x y

Tactic:
rw [← Ideal.isCoprime_span_singleton_iff, Ideal.isCoprime_iff_sup_eq, ← Ideal.span_union,
  Set.singleton_union, ← span_gcd, Ideal.span_singleton_eq_top]

Result:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
h : IsRelPrime x y
⊢ IsUnit (gcd x y)
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
lemma prod_rotate_eq_one_of_prod_eq_one :
    ∀ {l : List G} (_ : l.prod = 1) (n : ℕ), (l.rotate n).prod = 1
  | [], _, _ => by simp
  | a :: l, hl, n => by
    have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))
    rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl
    rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]

Proof state:
G : Type u_7
inst✝ : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
⊢ (a :: l).length > 0

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_7
inst✝ : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
⊢ ((a :: l).rotate n).prod = 1

Tactic:
have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))

Result:
G : Type u_7
inst✝ : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
this : n % (a :: l).length ≤ (a :: l).length
⊢ ((a :: l).rotate n).prod = 1

Proof state:
G : Type u_7
inst✝ : Group G
x✝¹ : [].prod = 1
x✝ : ℕ
⊢ ([].rotate x✝).prod = 1

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_7
inst✝ : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
this : n % (a :: l).length ≤ (a :: l).length
⊢ ((a :: l).rotate n).prod = 1

Tactic:
rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl

Result:
G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ ((a :: l).rotate n).prod = 1

Proof state:
G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ ((a :: l).rotate n).prod = 1

Tactic:
rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
  ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]

Result:
no goals
-- Mathlib/Data/Nat/Dist.lean
theorem dist_tri_right (n m : ℕ) : m ≤ n + dist n m

Proof state:
n m : ℕ
⊢ m ≤ n.dist m + n

Tactic:
apply dist_tri_left

Result:
no goals

Proof state:
n m : ℕ
⊢ m ≤ n + n.dist m

Tactic:
rw [add_comm]

Result:
n m : ℕ
⊢ m ≤ n.dist m + n
-- Mathlib/SetTheory/Game/Basic.lean
theorem quot_right_distrib (x y z : PGame) : (⟦(x + y) * z⟧ : Game) = ⟦x * z⟧ + ⟦y * z⟧

Proof state:
x y z : PGame
⊢ ⟦(x + y) * z⟧ = ⟦x * z⟧ + ⟦y * z⟧

Tactic:
simp only [quot_mul_comm, quot_left_distrib]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/CoversTop.lean
lemma familyOfElements_apply (hx : x.IsCompatible) {X Z : C} (f : Z ⟶ X) (i : I) (φ : Z ⟶ Y i) :
    familyOfElements x X f ⟨i, ⟨φ⟩⟩ = F.map φ.op (x i)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Z : C
f : Z ⟶ X
i : I
φ : Z ⟶ Y i
⊢ x.familyOfElements X f ⋯ = F.map φ.op (x i)

Tactic:
apply hx

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem find?_eq_zoom : ∀ {t : RBNode α} (p := .root), t.find? cut = (t.zoom cut p).1.root?
  | .nil, _ => rfl
  | .node .., _ => by unfold find? zoom; split <;> [apply find?_eq_zoom; apply find?_eq_zoom; rfl]

Proof state:
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : optParam (Path α) Path.root
⊢ (match cut v✝ with
    | Ordering.lt => find? cut l✝
    | Ordering.gt => find? cut r✝
    | Ordering.eq => some v✝) =
    (match cut v✝ with
        | Ordering.lt => zoom cut l✝ (Path.left c✝ x✝ v✝ r✝)
        | Ordering.gt => zoom cut r✝ (Path.right c✝ l✝ v✝ x✝)
        | Ordering.eq => (node c✝ l✝ v✝ r✝, x✝)).fst.root?

Tactic:
split <;> [apply find?_eq_zoom; apply find?_eq_zoom; rfl]

Result:
no goals

Proof state:
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : optParam (Path α) Path.root
⊢ find? cut (node c✝ l✝ v✝ r✝) = (zoom cut (node c✝ l✝ v✝ r✝) x✝).fst.root?

Tactic:
unfold find? zoom

Result:
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : optParam (Path α) Path.root
⊢ (match cut v✝ with
    | Ordering.lt => find? cut l✝
    | Ordering.gt => find? cut r✝
    | Ordering.eq => some v✝) =
    (match cut v✝ with
        | Ordering.lt => zoom cut l✝ (Path.left c✝ x✝ v✝ r✝)
        | Ordering.gt => zoom cut r✝ (Path.right c✝ l✝ v✝ x✝)
        | Ordering.eq => (node c✝ l✝ v✝ r✝, x✝)).fst.root?
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem toComplex_im (x y : ℤ) : ((⟨x, y⟩ : ℤ[i]) : ℂ).im = y

Proof state:
x y : ℤ
⊢ (toComplex { re := x, im := y }).im = ↑y

Tactic:
simp [toComplex_def]

Result:
no goals