harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem eqToHom_right {X Y : StructuredArrow S T} (h : X = Y) :
    (eqToHom h).right = eqToHom (by rw [h])

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' Y'' : C
T T' : C ⥤ D
X Y : StructuredArrow S T
h : X = Y
⊢ X.right = Y.right

Tactic:
rw [h]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
X Y : StructuredArrow S T
h : X = Y
⊢ (eqToHom h).right = eqToHom ⋯

Tactic:
subst h

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
X : StructuredArrow S T
⊢ (eqToHom ⋯).right = eqToHom ⋯

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
X : StructuredArrow S T
⊢ (eqToHom ⋯).right = eqToHom ⋯

Tactic:
simp only [eqToHom_refl, id_right]

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem Chain.sublist [IsTrans α R] (hl : l₂.Chain R a) (h : l₁ <+ l₂) :
    l₁.Chain R a

Proof state:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
a : α
inst✝ : IsTrans α R
hl : Pairwise R (a :: l₂)
h : l₁ <+ l₂
⊢ Pairwise R (a :: l₁)

Tactic:
exact hl.sublist (h.cons_cons a)

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
a : α
inst✝ : IsTrans α R
hl : Chain R a l₂
h : l₁ <+ l₂
⊢ Chain R a l₁

Tactic:
rw [chain_iff_pairwise] at hl ⊢

Result:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
a : α
inst✝ : IsTrans α R
hl : Pairwise R (a :: l₂)
h : l₁ <+ l₂
⊢ Pairwise R (a :: l₁)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem unzip_zip_right {l₁ : Array α} {l₂ : Array β} (h : l₂.size ≤ l₁.size) :
    (unzip (zip l₁ l₂)).2 = l₂

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
h : { toList := toList✝ }.size ≤ { toList := toList✝¹ }.size
⊢ ({ toList := toList✝¹ }.zip { toList := toList✝ }).unzip.snd = { toList := toList✝ }

Tactic:
simp_all only [size_toArray, List.zip_toArray, List.unzip_toArray, Prod.map_snd,
  List.unzip_zip_right]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size ≤ l₁.size
⊢ (l₁.zip l₂).unzip.snd = l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
h : l₂.size ≤ { toList := toList✝ }.size
⊢ ({ toList := toList✝ }.zip l₂).unzip.snd = l₂

Proof state:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
h : l₂.size ≤ { toList := toList✝ }.size
⊢ ({ toList := toList✝ }.zip l₂).unzip.snd = l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
h : { toList := toList✝ }.size ≤ { toList := toList✝¹ }.size
⊢ ({ toList := toList✝¹ }.zip { toList := toList✝ }).unzip.snd = { toList := toList✝ }
-- Mathlib/Data/Matrix/Diagonal.lean
theorem one_eq_pi_single {i j} : (1 : Matrix n n α) i j = Pi.single (f := fun _ => α) i 1 j

Proof state:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i j : n
⊢ 1 i j = Pi.single i 1 j

Tactic:
simp only [one_apply, Pi.single_apply, eq_comm]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem isUniformInducing_iff [PseudoEMetricSpace β] {f : α → β} :
    IsUniformInducing f ↔ UniformContinuous f ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ :=
  isUniformInducing_iff'.trans <| Iff.rfl.and <|
    ((uniformity_basis_edist.comap _).le_basis_iff uniformity_basis_edist).trans <| by
      simp only [subset_def, Prod.forall]; rfl

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ≥0∞),
      0 < i' →
        ∃ i,
          0 < i ∧ ∀ (a b : α), (a, b) ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < i} → (a, b) ∈ {p | edist p.1 p.2 < i'}) ↔
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ≥0∞), 0 < i' → ∃ i, 0 < i ∧ Prod.map f f ⁻¹' {p | edist p.1 p.2 < i} ⊆ {p | edist p.1 p.2 < i'}) ↔
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

Tactic:
simp only [subset_def, Prod.forall]

Result:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ≥0∞),
      0 < i' →
        ∃ i,
          0 < i ∧ ∀ (a b : α), (a, b) ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < i} → (a, b) ∈ {p | edist p.1 p.2 < i'}) ↔
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
-- Mathlib/Data/List/Count.lean
lemma count_diff (a : α) (l₁ : List α) :
    ∀ l₂, count a (l₁.diff l₂) = count a l₁ - count a l₂
  | [] => rfl
  | b :: l₂ => by
    simp only [diff_cons, count_diff, count_erase, beq_iff_eq, Nat.sub_right_comm, count_cons,
      Nat.sub_add_eq]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
⊢ count a (l₁.diff (b :: l₂)) = count a l₁ - count a (b :: l₂)

Tactic:
simp only [diff_cons, count_diff, count_erase, beq_iff_eq, Nat.sub_right_comm, count_cons,
  Nat.sub_add_eq]

Result:
no goals
-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem Submartingale.bddAbove_iff_exists_tendsto_aux [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)
    (hf0 : f 0 = 0) (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) :
    ∀ᵐ ω ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)

Tactic:
filter_upwards [hf.exists_tendsto_of_abs_bddAbove_aux hf0 hbdd] with ω hω using
  ⟨hω, fun ⟨c, hc⟩ => hc.bddAbove_range⟩

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem to_real_im (x : ℤ[i]) : ((x.im : ℤ) : ℝ) = (x : ℂ).im

Proof state:
x : ℤ[i]
⊢ ↑x.im = (toComplex x).im

Tactic:
simp [toComplex_def]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem sbtw_iff_right_ne_and_left_mem_image_Ioi {x y z : P} :
    Sbtw R x y z ↔ z ≠ y ∧ x ∈ lineMap z y '' Set.Ioi (1 : R)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
⊢ Sbtw R x y z ↔ z ≠ y ∧ x ∈ ⇑(lineMap z y) '' Set.Ioi 1

Tactic:
rw [sbtw_comm, sbtw_iff_left_ne_and_right_mem_image_Ioi]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_eq_sqrt_one_sub_cos_sq {x : ℝ} (hl : 0 ≤ x) (hu : x ≤ π) :
    sin x = √(1 - cos x ^ 2)

Proof state:
x : ℝ
hl : 0 ≤ x
hu : x ≤ π
⊢ sin x = √(1 - cos x ^ 2)

Tactic:
rw [← abs_sin_eq_sqrt_one_sub_cos_sq, abs_of_nonneg (sin_nonneg_of_nonneg_of_le_pi hl hu)]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem le_of_succ_succ_get?_contsAux_b {b : K}
    (nth_partDen_eq : (of v).partDens.get? n = some b) :
    b * ((of v).contsAux <| n + 1).b ≤ ((of v).contsAux <| n + 2).b

Proof state:
case intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
⊢ gp_n.b * ((of v).contsAux (n + 1)).b ≤ ((of v).contsAux (n + 2)).b

Tactic:
simp [of_partNum_eq_one (partNum_eq_s_a nth_s_eq), zero_le_of_contsAux_b,
  GenContFract.contsAux_recurrence nth_s_eq rfl rfl]

Result:
no goals

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
⊢ b * ((of v).contsAux (n + 1)).b ≤ ((of v).contsAux (n + 2)).b

Tactic:
obtain ⟨gp_n, nth_s_eq, rfl⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b :=
  exists_s_b_of_partDen nth_partDen_eq

Result:
case intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
⊢ gp_n.b * ((of v).contsAux (n + 1)).b ≤ ((of v).contsAux (n + 2)).b
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_le_sInf (h : ∀ μ' ∈ m, μ ≤ μ') : μ ≤ sInf m :=
  have : μ.toOuterMeasure ≤ sInf (toOuterMeasure '' m) :=
    le_sInf <| forall_mem_image.2 fun _ hμ ↦ toOuterMeasure_le.2 <| h _ hμ
  le_iff.2 fun s hs => by rw [sInf_apply hs]; exact this s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : ∀ μ' ∈ m, μ ≤ μ'
this : μ.toOuterMeasure ≤ sInf (toOuterMeasure '' m)
s : Set α
hs : MeasurableSet s
⊢ μ s ≤ (sInf (toOuterMeasure '' m)) s

Tactic:
exact this s

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : ∀ μ' ∈ m, μ ≤ μ'
this : μ.toOuterMeasure ≤ sInf (toOuterMeasure '' m)
s : Set α
hs : MeasurableSet s
⊢ μ s ≤ (sInf m) s

Tactic:
rw [sInf_apply hs]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : ∀ μ' ∈ m, μ ≤ μ'
this : μ.toOuterMeasure ≤ sInf (toOuterMeasure '' m)
s : Set α
hs : MeasurableSet s
⊢ μ s ≤ (sInf (toOuterMeasure '' m)) s
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem mrange_id : mrange (MonoidHom.id M) = ⊤

Proof state:
M : Type u_1
inst✝ : MulOneClass M
⊢ mrange (id M) = ⊤

Tactic:
simp [mrange_eq_map]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma mul_div_cancel_of_imp' (h : b = 0 → a = 0) : b * (a / b) = a

Proof state:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ b * (a / b) = a

Tactic:
rw [mul_comm, div_mul_cancel_of_imp h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem or_mod_two_eq_one : (a ||| b) % 2 = 1 ↔ a % 2 = 1 ∨ b % 2 = 1

Proof state:
a b : Nat
⊢ (a.testBit 0 || b.testBit 0) = true ↔ a.testBit 0 = true ∨ b.testBit 0 = true

Tactic:
simp

Result:
no goals

Proof state:
a b : Nat
⊢ (a ||| b) % 2 = 1 ↔ a % 2 = 1 ∨ b % 2 = 1

Tactic:
simp only [mod_two_eq_one_iff_testBit_zero]

Result:
a b : Nat
⊢ (a ||| b).testBit 0 = true ↔ a.testBit 0 = true ∨ b.testBit 0 = true

Proof state:
a b : Nat
⊢ (a ||| b).testBit 0 = true ↔ a.testBit 0 = true ∨ b.testBit 0 = true

Tactic:
rw [testBit_or]

Result:
a b : Nat
⊢ (a.testBit 0 || b.testBit 0) = true ↔ a.testBit 0 = true ∨ b.testBit 0 = true
-- Mathlib/Data/Int/ModEq.lean
theorem natCast_modEq_iff {a b n : ℕ} : a ≡ b [ZMOD n] ↔ a ≡ b [MOD n]

Proof state:
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ ↑(a % n) = ↑(b % n)

Tactic:
simp [natCast_mod]

Result:
no goals

Proof state:
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ a % n = b % n

Tactic:
rw [← Int.ofNat_inj]

Result:
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ ↑(a % n) = ↑(b % n)

Proof state:
a b n : ℕ
⊢ ↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]

Tactic:
unfold ModEq Nat.ModEq

Result:
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ a % n = b % n
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_eq_false_iff_exists_isSome_getValueCast? [BEq α] [LawfulBEq α]
    {l : List ((a : α) × β a)} : l.isEmpty = false ↔ ∃ a, (getValueCast? a l).isSome

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
⊢ l.isEmpty = false ↔ ∃ a, (getValueCast? a l).isSome = true

Tactic:
simp [isEmpty_eq_false_iff_exists_isSome_getEntry?, isSome_getValueCast?_eq_isSome_getEntry?]

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem neg (hf : UnifIntegrable f p μ) : UnifIntegrable (-f) p μ

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
⊢ ∀ ⦃ε : ℝ⦄,
    0 < ε →
      ∃ δ,
        ∃ (_ : 0 < δ),
          ∀ (i : ι) (s : Set α),
            MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
exact hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
⊢ UnifIntegrable (-f) p μ

Tactic:
simp_rw [UnifIntegrable, Pi.neg_apply, Set.indicator_neg', eLpNorm_neg]

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
⊢ ∀ ⦃ε : ℝ⦄,
    0 < ε →
      ∃ δ,
        ∃ (_ : 0 < δ),
          ∀ (i : ι) (s : Set α),
            MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
-- Mathlib/Order/Minimal.lean
theorem minimal_iff_eq (hy : P y) (hP : ∀ ⦃x⦄, P x → y ≤ x) : Minimal P x ↔ x = y :=
  ⟨fun h ↦ h.eq_of_ge hy (hP h.prop), by rintro rfl; exact ⟨hy, fun z hz _ ↦ hP hz⟩⟩

Proof state:
α : Type u_1
P : α → Prop
x y : α
inst✝ : PartialOrder α
hy : P y
hP : ∀ ⦃x : α⦄, P x → y ≤ x
⊢ x = y → Minimal P x

Tactic:
rintro rfl

Result:
α : Type u_1
P : α → Prop
x : α
inst✝ : PartialOrder α
hy : P x
hP : ∀ ⦃x_1 : α⦄, P x_1 → x ≤ x_1
⊢ Minimal P x

Proof state:
α : Type u_1
P : α → Prop
x : α
inst✝ : PartialOrder α
hy : P x
hP : ∀ ⦃x_1 : α⦄, P x_1 → x ≤ x_1
⊢ Minimal P x

Tactic:
exact ⟨hy, fun z hz _ ↦ hP hz⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Comap.lean
@[simp] lemma comap_zero (f : α → β) : (0 : Measure β).comap f = 0

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) 0)
⊢ comap f 0 = 0

Tactic:
simp [comap, hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
⊢ comap f 0 = 0

Tactic:
by_cases hf : Injective f ∧ ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) (0 : Measure β)

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) 0
⊢ comap f 0 = 0

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) 0)
⊢ comap f 0 = 0

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) 0
⊢ comap f 0 = 0

Tactic:
simp [comap, hf]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem _root_.Real.toNNReal_div' {x y : ℝ} (hy : 0 ≤ y) :
    Real.toNNReal (x / y) = Real.toNNReal x / Real.toNNReal y

Proof state:
x y : ℝ
hy : 0 ≤ y
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal

Tactic:
rw [div_eq_inv_mul, div_eq_inv_mul, Real.toNNReal_mul (inv_nonneg.2 hy), Real.toNNReal_inv]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma isIso_of_coyoneda_map_bijective {X Y : C} (f : X ⟶ Y)
    (hf : ∀ (T : C), Function.Bijective (fun (x : Y ⟶ T) => f ≫ x)) :
    IsIso f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x => f ≫ x
⊢ IsIso f

Tactic:
obtain ⟨g, hg : f ≫ g = 𝟙 X⟩ := (hf X).2 (𝟙 X)

Result:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x => f ≫ x
g : Y ⟶ X
hg : f ≫ g = 𝟙 X
⊢ IsIso f

Proof state:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x => f ≫ x
g : Y ⟶ X
hg : f ≫ g = 𝟙 X
⊢ (fun x => f ≫ x) (g ≫ f) = (fun x => f ≫ x) (𝟙 Y)

Tactic:
simp only [Category.comp_id, ← Category.assoc, hg, Category.id_comp]

Result:
no goals

Proof state:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x => f ≫ x
g : Y ⟶ X
hg : f ≫ g = 𝟙 X
⊢ IsIso f

Tactic:
refine ⟨g, hg, (hf _).1 ?_⟩

Result:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x => f ≫ x
g : Y ⟶ X
hg : f ≫ g = 𝟙 X
⊢ (fun x => f ≫ x) (g ≫ f) = (fun x => f ≫ x) (𝟙 Y)
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem mul_inv_cancel_right (a : α) (b : αˣ) : a * b * ↑b⁻¹ = a

Proof state:
α : Type u
inst✝ : Monoid α
a : α
b : αˣ
⊢ a * ↑b * ↑b⁻¹ = a

Tactic:
rw [mul_assoc, mul_inv, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem msb_sub {x y: BitVec w} :
    (x - y).msb
      = (x.msb ^^ ((~~~y + 1#w).msb ^^ carry (w - 1 - 0) x (~~~y + 1#w) false))

Proof state:
w : Nat
x y : BitVec w
⊢ (x - y).msb = (x.msb ^^ ((~~~y + 1#w).msb ^^ carry (w - 1 - 0) x (~~~y + 1#w) false))

Tactic:
simp [sub_toAdd, BitVec.neg_eq_not_add, msb_add]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem pdiv_zeta [DivisionSemiring R] (f : ArithmeticFunction R) :
    pdiv f zeta = f

Proof state:
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
⊢ f.pdiv ↑ζ = f

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
n : ℕ
⊢ (f.pdiv ↑ζ) n = f n

Proof state:
case h
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
n : ℕ
⊢ (f.pdiv ↑ζ) n = f n

Tactic:
cases n <;> simp [succ_ne_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem pi_zero : pi (fun _ ↦ 0 : (i : ι) → P1 →ᵃ[k] φv i) = 0

Proof state:
case h.h
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : Module k V1
ι : Type u_9
φv : ι → Type u_10
inst✝¹ : (i : ι) → AddCommGroup (φv i)
inst✝ : (i : ι) → Module k (φv i)
p✝ : P1
x✝ : ι
⊢ (pi fun x => 0) p✝ x✝ = 0 p✝ x✝

Tactic:
rfl

Result:
no goals

Proof state:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : Module k V1
ι : Type u_9
φv : ι → Type u_10
inst✝¹ : (i : ι) → AddCommGroup (φv i)
inst✝ : (i : ι) → Module k (φv i)
⊢ (pi fun x => 0) = 0

Tactic:
ext

Result:
case h.h
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : Module k V1
ι : Type u_9
φv : ι → Type u_10
inst✝¹ : (i : ι) → AddCommGroup (φv i)
inst✝ : (i : ι) → Module k (φv i)
p✝ : P1
x✝ : ι
⊢ (pi fun x => 0) p✝ x✝ = 0 p✝ x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_min_add_left (a b c : Nat) : min (a + b) (a + c) = a + min b c

Proof state:
a b c : Nat
⊢ min (b + a) (c + a) = a + min b c

Tactic:
rw [Nat.add_comm a]

Result:
a b c : Nat
⊢ min (b + a) (c + a) = min b c + a

Proof state:
a b c : Nat
⊢ min (a + b) (a + c) = a + min b c

Tactic:
repeat rw [Nat.add_comm a]

Result:
a b c : Nat
⊢ min (b + a) (c + a) = min b c + a

Proof state:
a b c : Nat
⊢ min (b + a) (c + a) = min b c + a

Tactic:
exact Nat.add_min_add_right ..

Result:
no goals
-- Mathlib/Topology/Algebra/ConstMulAction.lean
theorem isClosed_setOf_map_smul {N : Type*} [Monoid N] (α β) [MulAction M α] [MulAction N β]
    [TopologicalSpace β] [T2Space β] [ContinuousConstSMul N β] (σ : M → N) :
    IsClosed { f : α → β | ∀ c x, f (c • x) = σ c • f x }

Proof state:
M : Type u_1
inst✝⁶ : Monoid M
N : Type u_4
inst✝⁵ : Monoid N
α : Type u_5
β : Type u_6
inst✝⁴ : MulAction M α
inst✝³ : MulAction N β
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed (⋂ i, ⋂ i_1, {x | x (i • i_1) = σ i • x i_1})

Tactic:
exact isClosed_iInter fun c => isClosed_iInter fun x =>
  isClosed_eq (continuous_apply _) ((continuous_apply _).const_smul _)

Result:
no goals

Proof state:
M : Type u_1
inst✝⁶ : Monoid M
N : Type u_4
inst✝⁵ : Monoid N
α : Type u_5
β : Type u_6
inst✝⁴ : MulAction M α
inst✝³ : MulAction N β
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed {f | ∀ (c : M) (x : α), f (c • x) = σ c • f x}

Tactic:
simp only [Set.setOf_forall]

Result:
M : Type u_1
inst✝⁶ : Monoid M
N : Type u_4
inst✝⁵ : Monoid N
α : Type u_5
β : Type u_6
inst✝⁴ : MulAction M α
inst✝³ : MulAction N β
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed (⋂ i, ⋂ i_1, {x | x (i • i_1) = σ i • x i_1})
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem leftInvSeq_concat (ω : List B) (i : B) :
    lis (ω.concat i) = (lis ω).concat ((π ω) * (s i) * (π ω)⁻¹)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
i : B
⊢ cs.leftInvSeq (ω.concat i) = (cs.leftInvSeq ω).concat (cs.wordProd ω * cs.simple i * (cs.wordProd ω)⁻¹)

Tactic:
simp [leftInvSeq_eq_reverse_rightInvSeq_reverse, rightInvSeq]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem erase_ne {i i' : ι} {f : Π₀ i, β i} (h : i' ≠ i) : (f.erase i) i' = f i'

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
f : Π₀ (i : ι), β i
h : i' ≠ i
⊢ (erase i f) i' = f i'

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem uniformContinuous_ofUniformFun :
    UniformContinuous fun f : α →ᵤ β ↦ ofFun 𝔖 (UniformFun.toFun f)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ∀ i ∈ 𝔖,
    ∀ i_2 ∈ 𝓤 β,
      ∃ i_4 ∈ 𝓤 β,
        ∀ ⦃x : (α →ᵤ β) × (α →ᵤ β)⦄,
          x ∈ UniformFun.gen α β i_4 →
            ((ofFun 𝔖) (UniformFun.toFun x.1), (ofFun 𝔖) (UniformFun.toFun x.2)) ∈ UniformOnFun.gen 𝔖 i i_2

Tactic:
exact fun _ _ U hU ↦ ⟨U, hU, fun f hf x _ ↦ hf x⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ UniformContinuous fun f => (ofFun 𝔖) (UniformFun.toFun f)

Tactic:
simp only [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf, tendsto_principal,
  (UniformFun.hasBasis_uniformity _ _).eventually_iff]

Result:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ∀ i ∈ 𝔖,
    ∀ i_2 ∈ 𝓤 β,
      ∃ i_4 ∈ 𝓤 β,
        ∀ ⦃x : (α →ᵤ β) × (α →ᵤ β)⦄,
          x ∈ UniformFun.gen α β i_4 →
            ((ofFun 𝔖) (UniformFun.toFun x.1), (ofFun 𝔖) (UniformFun.toFun x.2)) ∈ UniformOnFun.gen 𝔖 i i_2
-- Mathlib/Combinatorics/HalesJewett.lean
protected lemma IsMono.reindex {eη : η ≃ η'} {eα : α ≃ α'} {eι : ι ≃ ι'} {C : (ι → α) → κ}
    (hl : l.IsMono C) : (l.reindex eη eα eι).IsMono fun x ↦ C <| eα.symm ∘ x ∘ eι

Proof state:
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι → α) → κ
hl : IsMono C l
⊢ IsMono (fun x => C (⇑eα.symm ∘ x ∘ ⇑eι)) (l.reindex eη eα eι)

Tactic:
simp [reindex_isMono, Function.comp_assoc]

Result:
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι → α) → κ
hl : IsMono C l
⊢ IsMono (fun x => C (⇑eα.symm ∘ ⇑eα ∘ x)) l

Proof state:
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι → α) → κ
hl : IsMono C l
⊢ IsMono (fun x => C (⇑eα.symm ∘ ⇑eα ∘ x)) l

Tactic:
simpa [← Function.comp_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_congr [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α} (hab : a == b)
    {h} : getValue a l h = getValue b l ((containsKey_congr hab).symm.trans h)

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
a b : α
hab : (a == b) = true
h : containsKey a l = true
⊢ getValue a l h = getValue b l ⋯

Tactic:
rw [← Option.some_inj, ← getValue?_eq_some_getValue, ← getValue?_eq_some_getValue,
  getValue?_congr hab]

Result:
no goals