harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_coe {P : α → Prop} {Pbot : P ⊥} {Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)} (t : Finset β)
    (f : β → { x : α // P x }) :
    (@sup { x // P x } _ (Subtype.semilatticeSup Psup) (Subtype.orderBot Pbot) t f : α) =
      t.sup fun x => ↑(f x)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
⊢ ↑(t.sup f) = t.sup fun x => ↑(f x)

Tactic:
letI := Subtype.orderBot Pbot

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
⊢ ↑(t.sup f) = t.sup fun x => ↑(f x)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
⊢ ↑(t.sup f) = t.sup fun x => ↑(f x)

Tactic:
apply comp_sup_eq_sup_comp Subtype.val <;> intros <;> rfl

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
⊢ ↑(t.sup f) = t.sup fun x => ↑(f x)

Tactic:
letI := Subtype.semilatticeSup Psup

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
⊢ ↑(t.sup f) = t.sup fun x => ↑(f x)
-- Mathlib/Order/Monotone/Basic.lean
theorem Int.rel_of_forall_rel_succ_of_lt (r : β → β → Prop) [IsTrans β r] {f : ℤ → β}
    (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℤ⦄ (hab : a < b) : r (f a) (f b)

Proof state:
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a b : ℤ
hab : a < b
⊢ r (f a) (f b)

Tactic:
rcases lt.dest hab with ⟨n, rfl⟩

Result:
case intro
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
hab : a < a + ↑n.succ
⊢ r (f a) (f (a + ↑n.succ))

Proof state:
case intro.zero
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + ↑(Nat.succ 0)))

Tactic:
rw [Int.ofNat_one]

Result:
case intro.zero
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + 1))

Proof state:
case intro.succ
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑n.succ))
⊢ r (f a) (f (a + ↑(n + 1) + 1))

Tactic:
exact _root_.trans ihn (h _)

Result:
no goals

Proof state:
case intro.zero
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + 1))

Tactic:
apply h

Result:
no goals

Proof state:
case intro
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
hab : a < a + ↑n.succ
⊢ r (f a) (f (a + ↑n.succ))

Tactic:
clear hab

Result:
case intro
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
⊢ r (f a) (f (a + ↑n.succ))

Proof state:
case intro
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
⊢ r (f a) (f (a + ↑n.succ))

Tactic:
induction n with
| zero => rw [Int.ofNat_one]; apply h
| succ n ihn => rw [Int.ofNat_succ, ← Int.add_assoc]; exact _root_.trans ihn (h _)

Result:
no goals

Proof state:
case intro.succ
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑n.succ))
⊢ r (f a) (f (a + ↑(n + 1).succ))

Tactic:
rw [Int.ofNat_succ, ← Int.add_assoc]

Result:
case intro.succ
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑n.succ))
⊢ r (f a) (f (a + ↑(n + 1) + 1))
-- Mathlib/Algebra/Divisibility/Units.lean
theorem isUnit_iff_dvd_one {x : α} : IsUnit x ↔ x ∣ 1 :=
  ⟨IsUnit.dvd, fun ⟨y, h⟩ => ⟨⟨x, y, h.symm, by rw [h, mul_comm]⟩, rfl⟩⟩

Proof state:
α : Type u_1
inst✝ : CommMonoid α
x : α
x✝ : x ∣ 1
y : α
h : 1 = x * y
⊢ y * x = 1

Tactic:
rw [h, mul_comm]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem value_at (a : ℤ) {R : Type*} [CommSemiring R] (χ : R →* ℤ)
    (hp : ∀ (p : ℕ) (pp : p.Prime), p ≠ 2 → @legendreSym p ⟨pp⟩ a = χ p) {b : ℕ} (hb : Odd b) :
    J(a | b) = χ b

Proof state:
case e_a
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯ =
    List.pmap (fun a x => (⇑χ ∘ Nat.cast) a) b.primeFactorsList ⋯

Tactic:
apply List.pmap_congr_left

Result:
case e_a.h
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ ∀ a_1 ∈ b.primeFactorsList, ∀ (h₁ : Nat.Prime a_1), Nat.Prime a_1 → legendreSym a_1 a = (⇑χ ∘ Nat.cast) a_1

Proof state:
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ J(a | b) = (List.map (⇑χ) (List.map Nat.cast b.primeFactorsList)).prod

Tactic:
rw [jacobiSym, List.map_map, ← List.pmap_eq_map Nat.Prime _ _
  fun _ => prime_of_mem_primeFactorsList]

Result:
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ (List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯).prod =
    (List.pmap (fun a x => (⇑χ ∘ Nat.cast) a) b.primeFactorsList ⋯).prod

Proof state:
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ J(a | b) = χ ↑b

Tactic:
conv_rhs => rw [← prod_primeFactorsList hb.pos.ne', cast_list_prod, map_list_prod χ]

Result:
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ J(a | b) = (List.map (⇑χ) (List.map Nat.cast b.primeFactorsList)).prod

Proof state:
case e_a.h
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ ∀ a_1 ∈ b.primeFactorsList, ∀ (h₁ : Nat.Prime a_1), Nat.Prime a_1 → legendreSym a_1 a = (⇑χ ∘ Nat.cast) a_1

Tactic:
exact fun p h pp _ => hp p pp (hb.ne_two_of_dvd_nat <| dvd_of_mem_primeFactorsList h)

Result:
no goals

Proof state:
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ (List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯).prod =
    (List.pmap (fun a x => (⇑χ ∘ Nat.cast) a) b.primeFactorsList ⋯).prod

Tactic:
congr 1

Result:
case e_a
a : ℤ
R : Type u_1
inst✝ : CommSemiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯ =
    List.pmap (fun a x => (⇑χ ∘ Nat.cast) a) b.primeFactorsList ⋯
-- Mathlib/MeasureTheory/Covering/OneDim.lean
theorem tendsto_Icc_vitaliFamily_right (x : ℝ) :
    Tendsto (fun y => Icc x y) (𝓝[>] x) ((vitaliFamily (volume : Measure ℝ) 1).filterAt x)

Proof state:
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ x - ε ≤ x

Tactic:
linarith

Result:
no goals

Proof state:
case h
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ Icc x y ⊆ Metric.closedBall x ε

Tactic:
rw [closedBall_eq_Icc]

Result:
case h
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ Icc x y ⊆ Icc (x - ε) (x + ε)

Proof state:
case refine_1
x : ℝ
⊢ ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ∈ (vitaliFamily volume 1).setsAt x

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy using Icc_mem_vitaliFamily_at_right hy

Result:
no goals

Proof state:
case h
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ Icc x y ⊆ Icc (x - ε) (x + ε)

Tactic:
exact Icc_subset_Icc (by linarith) hy.2

Result:
no goals

Proof state:
case refine_2
x ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ⊆ Metric.closedBall x ε

Tactic:
filter_upwards [Icc_mem_nhdsGT <| show x < x + ε by linarith] with y hy

Result:
case h
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ Icc x y ⊆ Metric.closedBall x ε

Proof state:
case refine_2
x : ℝ
⊢ ∀ ε > 0, ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ⊆ Metric.closedBall x ε

Tactic:
intro ε εpos

Result:
case refine_2
x ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ⊆ Metric.closedBall x ε

Proof state:
x ε : ℝ
εpos : ε > 0
⊢ x < x + ε

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
⊢ Tendsto (fun y => Icc x y) (𝓝[>] x) ((vitaliFamily volume 1).filterAt x)

Tactic:
refine (VitaliFamily.tendsto_filterAt_iff _).2 ⟨?_, ?_⟩

Result:
case refine_1
x : ℝ
⊢ ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ∈ (vitaliFamily volume 1).setsAt x

case refine_2
x : ℝ
⊢ ∀ ε > 0, ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ⊆ Metric.closedBall x ε
-- Mathlib/Topology/Order/Monotone.lean
theorem Antitone.map_ciInf_of_continuousAt {ι : Sort*} [Nonempty ι] {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iInf g)) (Af : Antitone f)
    (bdd : BddBelow (range g)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Af : Antitone f
bdd : autoParam (BddBelow (range g)) _auto✝
⊢ f (⨅ i, g i) = ⨆ i, f (g i)

Tactic:
rw [iInf, Antitone.map_csInf_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iSup,
  comp_def]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem directedOn_iUnion {r} {f : ι → Set α} (hd : Directed (· ⊆ ·) f)
    (h : ∀ x, DirectedOn r (f x)) : DirectedOn r (⋃ x, f x)

Proof state:
α : Type u_1
ι : Sort u_5
r : α → α → Prop
f : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) f
h : ∀ (x : ι), DirectedOn r (f x)
⊢ ∀ (x : α) (x_1 : ι), x ∈ f x_1 → ∀ (y : α) (x_2 : ι), y ∈ f x_2 → ∃ z, (∃ i, z ∈ f i) ∧ r x z ∧ r y z

Tactic:
exact fun a₁ b₁ fb₁ a₂ b₂ fb₂ =>
  let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂
  let ⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂)
  ⟨x, ⟨z, xf⟩, xa₁, xa₂⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_5
r : α → α → Prop
f : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) f
h : ∀ (x : ι), DirectedOn r (f x)
⊢ DirectedOn r (⋃ x, f x)

Tactic:
simp only [DirectedOn, exists_prop, mem_iUnion, exists_imp]

Result:
α : Type u_1
ι : Sort u_5
r : α → α → Prop
f : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) f
h : ∀ (x : ι), DirectedOn r (f x)
⊢ ∀ (x : α) (x_1 : ι), x ∈ f x_1 → ∀ (y : α) (x_2 : ι), y ∈ f x_2 → ∃ z, (∃ i, z ∈ f i) ∧ r x z ∧ r y z
-- Mathlib/Order/CompleteLattice.lean
theorem le_iSup_iff {s : ι → α} : a ≤ iSup s ↔ ∀ b, (∀ i, s i ≤ b) → a ≤ b

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteSemilatticeSup α
a : α
s : ι → α
⊢ a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b

Tactic:
simp [iSup, le_sSup_iff, upperBounds]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_modifyKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) (l : List ((a : α) × β a)) :
    (modifyKey k f l).length = l.length

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : (modifyKey k f tail✝).length = tail✝.length
⊢ (match getValueCast? k (head✝ :: tail✝) with
      | none => head✝ :: tail✝
      | some v => replaceEntry k (f v) (head✝ :: tail✝)).length =
    (head✝ :: tail✝).length

Tactic:
split <;> next h => simp only [length_replaceEntry, List.length_cons]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
⊢ (modifyKey k f l).length = l.length

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
⊢ (modifyKey k f []).length = [].length

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : (modifyKey k f tail✝).length = tail✝.length
⊢ (modifyKey k f (head✝ :: tail✝)).length = (head✝ :: tail✝).length

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
⊢ (modifyKey k f []).length = [].length

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : (modifyKey k f tail✝).length = tail✝.length
x✝ : Option (β k)
v✝ : β k
h : getValueCast? k (head✝ :: tail✝) = some v✝
⊢ (replaceEntry k (f v✝) (head✝ :: tail✝)).length = (head✝ :: tail✝).length

Tactic:
simp only [length_replaceEntry, List.length_cons]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : (modifyKey k f tail✝).length = tail✝.length
⊢ (modifyKey k f (head✝ :: tail✝)).length = (head✝ :: tail✝).length

Tactic:
next ih =>
simp only [modifyKey]
split <;> next h => simp only [length_replaceEntry, List.length_cons]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : (modifyKey k f tail✝).length = tail✝.length
⊢ (modifyKey k f (head✝ :: tail✝)).length = (head✝ :: tail✝).length

Tactic:
simp only [modifyKey]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih : (modifyKey k f tail✝).length = tail✝.length
⊢ (match getValueCast? k (head✝ :: tail✝) with
      | none => head✝ :: tail✝
      | some v => replaceEntry k (f v) (head✝ :: tail✝)).length =
    (head✝ :: tail✝).length
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem _root_.IsUnit.det_zpow {A : M} (h : IsUnit A.det) (n : ℤ) : IsUnit (A ^ n).det

Proof state:
case ofNat
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A ^ ofNat n).det

Tactic:
simpa using h.pow n

Result:
no goals

Proof state:
case negSucc
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A ^ -[n+1]).det

Tactic:
simpa using h.pow n.succ

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℤ
⊢ IsUnit (A ^ n).det

Tactic:
rcases n with n | n

Result:
case ofNat
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A ^ ofNat n).det

case negSucc
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A ^ -[n+1]).det
-- Mathlib/MeasureTheory/Measure/DiracProba.lean
/-- The composition of `diracProbaEquiv.symm` and `diracProba` is the subtype inclusion. -/
lemma diracProba_comp_diracProbaEquiv_symm_eq_val [T0Space X] :
    diracProba ∘ (diracProbaEquiv (X := X)).symm = fun μ ↦ μ.val

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
⊢ diracProba ∘ ⇑diracProbaEquiv.symm = fun μ => ↑μ

Tactic:
funext μ

Result:
case h
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
μ : ↑(range diracProba)
⊢ (diracProba ∘ ⇑diracProbaEquiv.symm) μ = ↑μ

Proof state:
case h
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
μ : ↑(range diracProba)
⊢ (diracProba ∘ ⇑diracProbaEquiv.symm) μ = ↑μ

Tactic:
simp [diracProbaEquiv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem ite_cond_eq_true {α : Sort u} {c : Prop} {_ : Decidable c} (a b : α) (h : c = True) : (if c then a else b) = a

Proof state:
α : Sort u
c : Prop
x✝ : Decidable c
a b : α
h : c = True
⊢ ite c a b = a

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Nat/PSub.lean
theorem psub_eq_some {m : ℕ} : ∀ {n k}, psub m n = some k ↔ k + n = m
  | 0, k => by simp [eq_comm]
  | n + 1, k => by
    apply Option.bind_eq_some.trans
    simp only [psub_eq_some, ppred_eq_some]
    simp [add_comm, add_left_comm]

Proof state:
m n k : ℕ
⊢ (∃ a, m.psub n = some a ∧ a.ppred = some k) ↔ k + (n + 1) = m

Tactic:
simp only [psub_eq_some, ppred_eq_some]

Result:
m n k : ℕ
⊢ (∃ a, a + n = m ∧ k.succ = a) ↔ k + (n + 1) = m

Proof state:
m n k : ℕ
⊢ m.psub (n + 1) = some k ↔ k + (n + 1) = m

Tactic:
apply Option.bind_eq_some.trans

Result:
m n k : ℕ
⊢ (∃ a, m.psub n = some a ∧ a.ppred = some k) ↔ k + (n + 1) = m

Proof state:
m k : ℕ
⊢ m.psub 0 = some k ↔ k + 0 = m

Tactic:
simp [eq_comm]

Result:
no goals

Proof state:
m n k : ℕ
⊢ (∃ a, a + n = m ∧ k.succ = a) ↔ k + (n + 1) = m

Tactic:
simp [add_comm, add_left_comm]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Defs.lean
theorem prod_replicate (n : ℕ) (a : M) : (replicate n a).prod = a ^ n

Proof state:
case succ
M : Type u_4
inst✝ : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
⊢ (replicate (n + 1) a).prod = a ^ (n + 1)

Tactic:
rw [replicate_succ, prod_cons, ih, pow_succ']

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
n : ℕ
a : M
⊢ (replicate n a).prod = a ^ n

Tactic:
induction n with
| zero => rw [pow_zero, replicate_zero, prod_nil]
| succ n ih => rw [replicate_succ, prod_cons, ih, pow_succ']

Result:
no goals

Proof state:
case zero
M : Type u_4
inst✝ : Monoid M
a : M
⊢ (replicate 0 a).prod = a ^ 0

Tactic:
rw [pow_zero, replicate_zero, prod_nil]

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem Submodule.IsPrincipal.map_ringHom (f : F) {I : Ideal R}
    (hI : IsPrincipal I) : IsPrincipal (Ideal.map f I) :=
  ⟨⟨f (IsPrincipal.generator I), by
      rw [Ideal.submodule_span_eq, ← Set.image_singleton, ← Ideal.map_span,
      Ideal.span_singleton_generator]⟩⟩

Proof state:
R : Type u
S : Type u_1
F : Type u_3
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hI : IsPrincipal I
⊢ Ideal.map f I = span S {f (generator I)}

Tactic:
rw [Ideal.submodule_span_eq, ← Set.image_singleton, ← Ideal.map_span,
Ideal.span_singleton_generator]

Result:
no goals
-- Mathlib/Data/List/Lookmap.lean
theorem lookmap_map_eq (g : α → β) (h : ∀ (a), ∀ b ∈ f a, g a = g b) :
    ∀ l : List α, map g (l.lookmap f) = map g l
  | [] => rfl
  | a :: l => by
    rcases h' : f a with - | b
    · simpa [h'] using lookmap_map_eq _ h l
    · simp [lookmap_cons_some _ _ h', h _ _ h']

Proof state:
case some
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
b : α
h' : f a = some b
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

Tactic:
simp [lookmap_cons_some _ _ h', h _ _ h']

Result:
no goals

Proof state:
case none
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
h' : f a = none
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

Tactic:
simpa [h'] using lookmap_map_eq _ h l

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

Tactic:
rcases h' : f a with - | b

Result:
case none
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
h' : f a = none
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

case some
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
b : α
h' : f a = some b
⊢ map g (lookmap f (a :: l)) = map g (a :: l)
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
protected lemma IsCycle.reverse {p : G.Walk u u} (h : p.IsCycle) : p.reverse.IsCycle

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
h' : p.reverse = nil
⊢ p = nil

Tactic:
simp_all [← Walk.length_eq_zero_iff]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.IsCycle
⊢ p.reverse.IsCycle

Tactic:
simp only [Walk.isCycle_def, nodup_tail_support_reverse] at h ⊢

Result:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
⊢ p.reverse.IsTrail ∧ p.reverse ≠ nil ∧ p.support.tail.Nodup

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
⊢ p.reverse.IsTrail ∧ p.reverse ≠ nil ∧ p.support.tail.Nodup

Tactic:
exact ⟨h.1.reverse, fun h' ↦ h.2.1 (by simp_all [← Walk.length_eq_zero_iff]), h.2.2⟩

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_eq_oangle_of_dist_eq {p₁ p₂ p₃ : P} (h : dist p₁ p₂ = dist p₁ p₃) :
    ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁

Tactic:
rw [oangle, oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁,
  o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : dist p₁ p₂ = dist p₁ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁

Tactic:
simp_rw [dist_eq_norm_vsub V] at h

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem bicone_ι_π_self {F : J → C} (B : Bicone F) (j : J) : B.ι j ≫ B.π j = 𝟙 (F j)

Proof state:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
B : Bicone F
j : J
⊢ B.ι j ≫ B.π j = 𝟙 (F j)

Tactic:
simpa using B.ι_π j j

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem primeFactorsList_sublist_of_dvd {n k : ℕ} (h : n ∣ k) (h' : k ≠ 0) :
    n.primeFactorsList <+ k.primeFactorsList

Proof state:
case intro
n a : ℕ
h' : n * a ≠ 0
⊢ n.primeFactorsList <+ (n * a).primeFactorsList

Tactic:
exact primeFactorsList_sublist_right (right_ne_zero_of_mul h')

Result:
no goals

Proof state:
n k : ℕ
h : n ∣ k
h' : k ≠ 0
⊢ n.primeFactorsList <+ k.primeFactorsList

Tactic:
obtain ⟨a, rfl⟩ := h

Result:
case intro
n a : ℕ
h' : n * a ≠ 0
⊢ n.primeFactorsList <+ (n * a).primeFactorsList
-- Mathlib/Logic/Relation.lean
theorem fun_eq_comp (f : γ → α) : (f · = ·) ∘r r = (r <| f ·)

Proof state:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → α
x : γ
y : β
⊢ ((fun x1 x2 => f x1 = x2) ∘r r) x y ↔ r (f x) y

Tactic:
simp [Comp]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → α
⊢ (fun x1 x2 => f x1 = x2) ∘r r = fun x => r (f x)

Tactic:
ext x y

Result:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → α
x : γ
y : β
⊢ ((fun x1 x2 => f x1 = x2) ∘r r) x y ↔ r (f x) y