harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
@[reassoc]
lemma Exact.comp_eq_zero (h : S.Exact) {X Y : C} {a : X ⟶ S.X₂} (ha : a ≫ S.g = 0)
    {b : S.X₂ ⟶ Y} (hb : S.f ≫ b = 0) : a ≫ b = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.Exact
⊢ a ≫ b = 0

Tactic:
rw [exact_iff_iCycles_pOpcycles_zero] at eq

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.iCycles ≫ S.pOpcycles = 0
⊢ a ≫ b = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
⊢ a ≫ b = 0

Tactic:
have eq := h

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.Exact
⊢ a ≫ b = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
⊢ a ≫ b = 0

Tactic:
have := h.hasHomology

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
⊢ a ≫ b = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.iCycles ≫ S.pOpcycles = 0
⊢ a ≫ b = 0

Tactic:
rw [← S.liftCycles_i a ha, ← S.p_descOpcycles b hb, assoc, reassoc_of% eq,
  zero_comp, comp_zero]

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem ConvolutionExistsAt.distrib_add {x : G} (hfg : ConvolutionExistsAt f g x L μ)
    (hfg' : ConvolutionExistsAt f g' x L μ) :
    (f ⋆[L, μ] (g + g')) x = (f ⋆[L, μ] g) x + (f ⋆[L, μ] g') x

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g g' : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x : G
hfg : ConvolutionExistsAt f g x L μ
hfg' : ConvolutionExistsAt f g' x L μ
⊢ (f ⋆[L, μ] (g + g')) x = (f ⋆[L, μ] g) x + (f ⋆[L, μ] g') x

Tactic:
simp only [convolution_def, (L _).map_add, Pi.add_apply, integral_add hfg hfg']

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_of_subsingleton' [Subsingleton E] (a : E) : ‖a‖ = 0

Proof state:
E : Type u_5
inst✝¹ : SeminormedGroup E
inst✝ : Subsingleton E
a : E
⊢ ‖a‖ = 0

Tactic:
rw [Subsingleton.elim a 1, norm_one']

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem ofReal_log {x : ℝ} (hx : 0 ≤ x) : (x.log : ℂ) = log x :=
  Complex.ext (by rw [log_re, ofReal_re, Complex.norm_of_nonneg hx])
    (by rw [ofReal_im, log_im, arg_ofReal_of_nonneg hx])

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x)).im = (log ↑x).im

Tactic:
rw [ofReal_im, log_im, arg_ofReal_of_nonneg hx]

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x)).re = (log ↑x).re

Tactic:
rw [log_re, ofReal_re, Complex.norm_of_nonneg hx]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convergence.lean
/-- If `f` is bounded, then the abscissa of absolute convergence of `f` is bounded above by `1`. -/
lemma LSeries.abscissaOfAbsConv_le_of_le_const {f : ℕ → ℂ} (h : ∃ C, ∀ n ≠ 0, ‖f n‖ ≤ C) :
    abscissaOfAbsConv f ≤ 1

Proof state:
f : ℕ → ℂ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C
⊢ ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ 0

Tactic:
simpa using h

Result:
no goals

Proof state:
f : ℕ → ℂ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C
⊢ abscissaOfAbsConv f ≤ 1

Tactic:
simpa using abscissaOfAbsConv_le_of_le_const_mul_rpow (x := 0) (by simpa using h)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem findIdxs_cons :
    (x :: xs : List α).findIdxs p =
      bif p x then 0 :: (xs.findIdxs p).map (· + 1) else (xs.findIdxs p).map (· + 1)

Proof state:
case isFalse
α : Type u_1
x : α
xs : List α
p : α → Bool
h✝ : ¬p x = true
⊢ foldrIdx (fun i a is => if p a = true then (i + 0 + 1) :: is else is) [] xs =
    map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then (i + 0) :: is else is) [] xs)

Tactic:
apply findIdxs_cons_aux

Result:
no goals

Proof state:
α : Type u_1
x : α
xs : List α
p : α → Bool
⊢ findIdxs p (x :: xs) =
    bif p x then 0 :: map (fun x => x + 1) (findIdxs p xs) else map (fun x => x + 1) (findIdxs p xs)

Tactic:
dsimp [findIdxs]

Result:
α : Type u_1
x : α
xs : List α
p : α → Bool
⊢ (if p x = true then 0 :: foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs 1
    else foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs 1) =
    bif p x then 0 :: map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs)
    else map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs)

Proof state:
case isFalse
α : Type u_1
x : α
xs : List α
p : α → Bool
h✝ : ¬p x = true
⊢ foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs 1 =
    map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs)

Tactic:
simp only [Nat.zero_add, foldrIdx_start, Nat.add_zero, cons.injEq, true_and]

Result:
case isFalse
α : Type u_1
x : α
xs : List α
p : α → Bool
h✝ : ¬p x = true
⊢ foldrIdx (fun i a is => if p a = true then (i + 0 + 1) :: is else is) [] xs =
    map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then (i + 0) :: is else is) [] xs)

Proof state:
α : Type u_1
x : α
xs : List α
p : α → Bool
⊢ (if p x = true then 0 :: foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs 1
    else foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs 1) =
    bif p x then 0 :: map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs)
    else map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs)

Tactic:
rw [cond_eq_if]

Result:
α : Type u_1
x : α
xs : List α
p : α → Bool
⊢ (if p x = true then 0 :: foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs 1
    else foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs 1) =
    if p x = true then 0 :: map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs)
    else map (fun x => x + 1) (foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs)
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem image_range_orderOf [DecidableEq G] :
    letI : Fintype (zpowers x) := (Subgroup.zpowers x).instFintypeSubtypeMemOfDecidablePred
    Finset.image (fun i => x ^ i) (Finset.range (orderOf x)) = (zpowers x : Set G).toFinset

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
x : G
inst✝ : DecidableEq G
this : Fintype ↥(zpowers x) := (zpowers x).instFintypeSubtypeMemOfDecidablePred
⊢ Finset.image (fun i => x ^ i) (Finset.range (orderOf x)) = (↑(zpowers x)).toFinset

Tactic:
ext x

Result:
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
x✝ : G
inst✝ : DecidableEq G
this : Fintype ↥(zpowers x✝) := (zpowers x✝).instFintypeSubtypeMemOfDecidablePred
x : G
⊢ x ∈ Finset.image (fun i => x✝ ^ i) (Finset.range (orderOf x✝)) ↔ x ∈ (↑(zpowers x✝)).toFinset

Proof state:
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
x✝ : G
inst✝ : DecidableEq G
this : Fintype ↥(zpowers x✝) := (zpowers x✝).instFintypeSubtypeMemOfDecidablePred
x : G
⊢ x ∈ Finset.image (fun i => x✝ ^ i) (Finset.range (orderOf x✝)) ↔ x ∈ (↑(zpowers x✝)).toFinset

Tactic:
rw [Set.mem_toFinset, SetLike.mem_coe, mem_zpowers_iff_mem_range_orderOf]

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
x : G
inst✝ : DecidableEq G
⊢ Finset.image (fun i => x ^ i) (Finset.range (orderOf x)) = (↑(zpowers x)).toFinset

Tactic:
letI : Fintype (zpowers x) := (Subgroup.zpowers x).instFintypeSubtypeMemOfDecidablePred

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
x : G
inst✝ : DecidableEq G
this : Fintype ↥(zpowers x) := (zpowers x).instFintypeSubtypeMemOfDecidablePred
⊢ Finset.image (fun i => x ^ i) (Finset.range (orderOf x)) = (↑(zpowers x)).toFinset
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem smul_ball'' : a • ball b r = ball (a • b) r

Proof state:
case h
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
x✝ : E
⊢ x✝ ∈ a • ball b r ↔ x✝ ∈ ball (a • b) r

Tactic:
simp [mem_ball, Set.mem_smul_set, dist_eq_norm_div, _root_.div_eq_inv_mul,
  ← eq_inv_mul_iff_mul_eq, mul_assoc]

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a • ball b r = ball (a • b) r

Tactic:
ext

Result:
case h
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
x✝ : E
⊢ x✝ ∈ a • ball b r ↔ x✝ ∈ ball (a • b) r
-- Mathlib/LinearAlgebra/Dimension/Free.lean
theorem finite_iff_of_rank_eq_nsmul {W} [AddCommGroup W] [Module R W] [Module.Free R W] {n : ℕ}
    (hn : n ≠ 0) (hVW : Module.rank R M = n • Module.rank R W) :
    Module.Finite R M ↔ Module.Finite R W

Proof state:
R : Type u
M : Type v
inst✝⁷ : Semiring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
W : Type v
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Free R W
n : ℕ
hn : n ≠ 0
hVW : Module.rank R M = n • Module.rank R W
⊢ Module.Finite R M ↔ Module.Finite R W

Tactic:
simp only [← rank_lt_aleph0_iff, hVW, nsmul_lt_aleph0_iff_of_ne_zero hn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {k a : α} :
    (m.erase k).getKey! a = if k == a then default else m.getKey! a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
k a : α
⊢ (m.erase k).getKey! a = if (k == a) = true then default else m.getKey! a

Tactic:
simp_to_model [erase] using List.getKey!_eraseKey

Result:
no goals
-- Mathlib/RingTheory/FiniteLength.lean
theorem exists_compositionSeries_of_isNoetherian_isArtinian [IsNoetherian R M] [IsArtinian R M] :
    ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤

Proof state:
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
⊢ ∃ s, RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤

Tactic:
obtain ⟨f, f0, n, hn⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (Submodule R M)

Result:
case intro.intro.intro
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
f0 : IsMin (f 0)
n : ℕ
hn : IsMax (f n) ∧ ∀ i < n, f i ⋖ f (i + 1)
⊢ ∃ s, RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤

Proof state:
case intro.intro.intro
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
f0 : IsMin (f 0)
n : ℕ
hn : IsMax (f n) ∧ ∀ i < n, f i ⋖ f (i + 1)
⊢ ∃ s, RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤

Tactic:
exact ⟨⟨n, fun i ↦ f i, fun i ↦ hn.2 i i.2⟩, f0.eq_bot, hn.1.eq_top⟩

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
@[simp] lemma Ioi_True : Ioi True = ∅

Proof state:
⊢ Ioi True = ∅

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem coe_sub {r₁ r₂ : ℝ≥0} (h : r₂ ≤ r₁) : ((r₁ - r₂ : ℝ≥0) : ℝ) = ↑r₁ - ↑r₂ :=
  max_eq_left <| le_sub_comm.2 <| by simp [show (r₂ : ℝ) ≤ r₁ from h]

Proof state:
r₁ r₂ : ℝ≥0
h : r₂ ≤ r₁
⊢ ↑r₂ ≤ ↑r₁ - 0

Tactic:
simp [show (r₂ : ℝ) ≤ r₁ from h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem length_set (as : List α) (i : Nat) (a : α) : (as.set i a).length = as.length

Proof state:
case cons
α : Type u
a x : α
xs : List α
ih : ∀ (i : Nat), (xs.set i a).length = xs.length
i : Nat
⊢ ((x :: xs).set i a).length = (x :: xs).length

Tactic:
cases i with
| zero => rfl
| succ i => simp [set, ih]

Result:
no goals

Proof state:
case cons.succ
α : Type u
a x : α
xs : List α
ih : ∀ (i : Nat), (xs.set i a).length = xs.length
i : Nat
⊢ ((x :: xs).set (i + 1) a).length = (x :: xs).length

Tactic:
simp [set, ih]

Result:
no goals

Proof state:
case cons.zero
α : Type u
a x : α
xs : List α
ih : ∀ (i : Nat), (xs.set i a).length = xs.length
⊢ ((x :: xs).set 0 a).length = (x :: xs).length

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
as : List α
i : Nat
a : α
⊢ (as.set i a).length = as.length

Tactic:
induction as generalizing i with
| nil => rfl
| cons x xs ih =>
  cases i with
  | zero => rfl
  | succ i => simp [set, ih]

Result:
no goals

Proof state:
case nil
α : Type u
a : α
i : Nat
⊢ (nil.set i a).length = nil.length

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem ofFn_congr {m n : ℕ} (h : m = n) (f : Fin m → α) :
    ofFn f = ofFn fun i : Fin n => f (Fin.cast h.symm i)

Proof state:
α : Type u
m : ℕ
f : Fin m → α
⊢ ofFn f = ofFn fun i => f (Fin.cast ⋯ i)

Tactic:
simp_rw [Fin.cast_refl, id]

Result:
no goals

Proof state:
α : Type u
m n : ℕ
h : m = n
f : Fin m → α
⊢ ofFn f = ofFn fun i => f (Fin.cast ⋯ i)

Tactic:
subst h

Result:
α : Type u
m : ℕ
f : Fin m → α
⊢ ofFn f = ofFn fun i => f (Fin.cast ⋯ i)
-- Mathlib/RingTheory/HahnSeries/Basic.lean
@[simp]
protected lemma map_zero [Zero S] (f : ZeroHom R S) :
    (0 : HahnSeries Γ R).map f = 0

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero S
f : ZeroHom R S
x✝ : Γ
⊢ (map 0 f).coeff x✝ = coeff 0 x✝

Tactic:
simp

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero S
f : ZeroHom R S
⊢ map 0 f = 0

Tactic:
ext

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero S
f : ZeroHom R S
x✝ : Γ
⊢ (map 0 f).coeff x✝ = coeff 0 x✝
-- Mathlib/.lake/packages/batteries/Batteries/Data/Int.lean
theorem ofBits_zero (f : Fin 0 → Bool) : ofBits f = 0

Proof state:
f : Fin 0 → Bool
⊢ ofBits f = 0

Tactic:
simp [ofBits]

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem exists_max_image (s : Finset β) (f : β → α) (h : s.Nonempty) :
    ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

Proof state:
α : Type u_2
β : Type u_3
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

Tactic:
obtain ⟨y, hy⟩ := max_of_nonempty (h.image f)

Result:
case intro
α : Type u_2
β : Type u_3
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
y : α
hy : (image f s).max = ↑y
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

Proof state:
case intro
α : Type u_2
β : Type u_3
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
y : α
hy : (image f s).max = ↑y
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

Tactic:
rcases mem_image.mp (mem_of_max hy) with ⟨x, hx, rfl⟩

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
x : β
hx : x ∈ s
hy : (image f s).max = ↑(f x)
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
x : β
hx : x ∈ s
hy : (image f s).max = ↑(f x)
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

Tactic:
exact ⟨x, hx, fun x' hx' => le_max_of_eq (mem_image_of_mem f hx') hy⟩

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem IsCyclic.image_range_orderOf (ha : ∀ x : α, x ∈ zpowers a) :
    Finset.image (fun i => a ^ i) (range (orderOf a)) = univ

Proof state:
α : Type u_1
a : α
inst✝² : Group α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ha : ∀ (x : α), x ∈ ↑(zpowers a)
⊢ image (fun i => a ^ i) (range (orderOf a)) = univ

Tactic:
simp only [_root_.image_range_orderOf, Set.eq_univ_iff_forall.mpr ha, Set.toFinset_univ]

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝² : Group α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ha : ∀ (x : α), x ∈ zpowers a
⊢ image (fun i => a ^ i) (range (orderOf a)) = univ

Tactic:
simp_rw [← SetLike.mem_coe] at ha

Result:
α : Type u_1
a : α
inst✝² : Group α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ha : ∀ (x : α), x ∈ ↑(zpowers a)
⊢ image (fun i => a ^ i) (range (orderOf a)) = univ
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem iSup_lt_lift {ι} {f : ι → Cardinal} {c : Cardinal}
    (hι : Cardinal.lift.{v, u} #ι < c.ord.cof)
    (hf : ∀ i, f i < c) : iSup f < c

Proof state:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
⊢ iSup f < c

Tactic:
rw [← ord_lt_ord, iSup_ord (Cardinal.bddAbove_range _)]

Result:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
⊢ ⨆ i, (f i).ord < c.ord

Proof state:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
⊢ ⨆ i, (f i).ord < c.ord

Tactic:
refine iSup_lt_ord_lift hι fun i => ?_

Result:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
i : ι
⊢ (f i).ord < c.ord

Proof state:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
i : ι
⊢ f i < c

Tactic:
apply hf

Result:
no goals

Proof state:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
i : ι
⊢ (f i).ord < c.ord

Tactic:
rw [ord_lt_ord]

Result:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
i : ι
⊢ f i < c
-- Mathlib/GroupTheory/Sylow.lean
theorem pow_dvd_card_of_pow_dvd_card [Finite G] {p n : ℕ} [hp : Fact p.Prime] (P : Sylow p G)
    (hdvd : p ^ n ∣ Nat.card G) : p ^ n ∣ Nat.card P

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ n ∣ (↑P).index * Nat.card ↥↑P
⊢ p ^ n ∣ Nat.card ↥↑P

Tactic:
exact (hp.1.coprime_pow_of_not_dvd P.not_dvd_index).symm.dvd_of_dvd_mul_left hdvd

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ n ∣ Nat.card G
⊢ p ^ n ∣ Nat.card ↥↑P

Tactic:
rw [← index_mul_card P.1] at hdvd

Result:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ n ∣ (↑P).index * Nat.card ↥↑P
⊢ p ^ n ∣ Nat.card ↥↑P
-- Mathlib/Data/Finset/Sigma.lean
theorem pairwiseDisjoint_map_sigmaMk :
    (s : Set ι).PairwiseDisjoint fun i => (t i).map (Embedding.sigmaMk i)

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ (↑s).PairwiseDisjoint fun i => map (Embedding.sigmaMk i) (t i)

Tactic:
intro i _ j _ hij

Result:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ (Disjoint on fun i => map (Embedding.sigmaMk i) (t i)) i j

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk i) (t i) → a ∉ map (Embedding.sigmaMk j) (t j)

Tactic:
simp_rw [mem_map, Function.Embedding.sigmaMk_apply]

Result:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, (∃ a_1 ∈ t i, ⟨i, a_1⟩ = a) → ¬∃ a_2 ∈ t j, ⟨j, a_2⟩ = a

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, (∃ a_1 ∈ t i, ⟨i, a_1⟩ = a) → ¬∃ a_2 ∈ t j, ⟨j, a_2⟩ = a

Tactic:
rintro _ ⟨y, _, rfl⟩ ⟨z, _, hz'⟩

Result:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
y : α i
left✝¹ : y ∈ t i
z : α j
left✝ : z ∈ t j
hz' : ⟨j, z⟩ = ⟨i, y⟩
⊢ False

Proof state:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
y : α i
left✝¹ : y ∈ t i
z : α j
left✝ : z ∈ t j
hz' : ⟨j, z⟩ = ⟨i, y⟩
⊢ False

Tactic:
exact hij (congr_arg Sigma.fst hz'.symm)

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ (Disjoint on fun i => map (Embedding.sigmaMk i) (t i)) i j

Tactic:
rw [Function.onFun, disjoint_left]

Result:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk i) (t i) → a ∉ map (Embedding.sigmaMk j) (t j)
-- Mathlib/Data/Real/EReal.lean
lemma add_ne_top_iff_ne_top_left {x y : EReal} (hy : y ≠ ⊥) (hy' : y ≠ ⊤) :
    x + y ≠ ⊤ ↔ x ≠ ⊤

Proof state:
x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤

Tactic:
cases x <;> simp [add_ne_top_iff_ne_top₂, hy, hy']

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Basic.lean
lemma RingHom.IsStableUnderBaseChange.localizationPreserves : LocalizationPreserves P

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : P f
⊢ P (IsLocalization.map S' f ⋯)

Tactic:
exact hP.isLocalization_map _ _ hf

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
⊢ LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P

Tactic:
introv R hf

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : P f
⊢ P (IsLocalization.map S' f ⋯)
-- Mathlib/Analysis/Calculus/FDeriv/Comp.lean
theorem HasFDerivAt.iterate {f : E → E} {f' : E →L[𝕜] E} (hf : HasFDerivAt f f' x)
    (hx : f x = x) (n : ℕ) : HasFDerivAt f^[n] (f' ^ n) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ HasFDerivAt f^[n] (f' ^ n) x

Tactic:
refine HasFDerivAtFilter.iterate hf ?_ hx n

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ Tendsto f (𝓝 x) (𝓝 x)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ Tendsto f (𝓝 x) (𝓝 x)

Tactic:
convert hf.continuousAt.tendsto

Result:
case h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ x = f x

Proof state:
case h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ x = f x

Tactic:
exact hx.symm

Result:
no goals