harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/TypeVec.lean
theorem prod_id : ∀ {n} {α β : TypeVec.{u} n}, (id ⊗' id) = (id : α ⊗ β ⟹ _)

Proof state:
case a.h.fz.mk
n✝¹ n✝ : ℕ
α✝ β✝ : TypeVec.{u} (n✝ + 1)
fst✝ : α✝.last
snd✝ : β✝.last
⊢ (id ⊗' id) Fin2.fz (fst✝, snd✝) = id Fin2.fz (fst✝, snd✝)

Tactic:
rfl

Result:
no goals

Proof state:
case a.h.fs
n✝¹ n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec.{u} n✝} (a : (α ⊗ β) a✝), (id ⊗' id) a✝ a = id a✝ a
α✝ β✝ : TypeVec.{u} (n✝ + 1)
a : (α✝ ⊗ β✝) a✝.fs
⊢ (id ⊗' id) a✝.fs a = id a✝.fs a

Tactic:
apply i_ih

Result:
no goals

Proof state:
case a.h
n✝ : ℕ
α✝ β✝ : TypeVec.{u} n✝
i : Fin2 n✝
a : (α✝ ⊗ β✝) i
⊢ (id ⊗' id) i a = id i a

Tactic:
induction i with
| fz => cases a; rfl
| fs _ i_ih => apply i_ih

Result:
no goals

Proof state:
n✝ : ℕ
α✝ β✝ : TypeVec.{u} n✝
⊢ (id ⊗' id) = id

Tactic:
ext i a

Result:
case a.h
n✝ : ℕ
α✝ β✝ : TypeVec.{u} n✝
i : Fin2 n✝
a : (α✝ ⊗ β✝) i
⊢ (id ⊗' id) i a = id i a

Proof state:
case a.h.fz
n✝¹ n✝ : ℕ
α✝ β✝ : TypeVec.{u} (n✝ + 1)
a : (α✝ ⊗ β✝) Fin2.fz
⊢ (id ⊗' id) Fin2.fz a = id Fin2.fz a

Tactic:
cases a

Result:
case a.h.fz.mk
n✝¹ n✝ : ℕ
α✝ β✝ : TypeVec.{u} (n✝ + 1)
fst✝ : α✝.last
snd✝ : β✝.last
⊢ (id ⊗' id) Fin2.fz (fst✝, snd✝) = id Fin2.fz (fst✝, snd✝)

Proof state:
⊢ ∀ {n : ℕ} {α β : TypeVec.{u} n}, (id ⊗' id) = id

Tactic:
intros

Result:
n✝ : ℕ
α✝ β✝ : TypeVec.{u} n✝
⊢ (id ⊗' id) = id
-- Mathlib/Data/Set/Prod.lean
theorem prod_union : s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂

Proof state:
case h.mk
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t₁ ∪ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∪ s ×ˢ t₂

Tactic:
simp [and_or_left]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
⊢ s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t₁ ∪ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∪ s ×ˢ t₂
-- Mathlib/Algebra/Group/AddChar.lean
@[simp] lemma zsmul_apply (n : ℤ) (ψ : AddChar A M) (a : A) : (n • ψ) a = ψ a ^ n

Proof state:
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
n : ℤ
ψ : AddChar A M
a : A
⊢ (n • ψ) a = ψ a ^ n

Tactic:
cases n <;> simp [-neg_apply, neg_apply']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_ne_nil_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : List α}
    (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ [] ↔ xs ≠ []

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ pmap f xs H ≠ [] ↔ xs ≠ []

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombination_indicator_subset (w : ι → k) (p : ι → P) {s₁ s₂ : Finset ι}
    (h : s₁ ⊆ s₂) :
    s₁.affineCombination k p w = s₂.affineCombination k p (Set.indicator (↑s₁) w)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ (affineCombination k s₁ p) w = (affineCombination k s₂ p) ((↑s₁).indicator w)

Tactic:
rw [affineCombination_apply, affineCombination_apply,
  weightedVSubOfPoint_indicator_subset _ _ _ h]

Result:
no goals
-- Mathlib/Topology/SeparatedMap.lean
theorem IsSeparatedMap.comp_right {f : X → Y} (sep : IsSeparatedMap f) {g : A → X}
    (cont : Continuous g) (inj : g.Injective) : IsSeparatedMap (f ∘ g)

Proof state:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed (Function.pullbackDiagonal f)
g : A → X
cont : Continuous g
inj : Function.Injective g
⊢ IsClosed (Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f)

Tactic:
exact sep.preimage (cont.mapPullback cont)

Result:
no goals

Proof state:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsSeparatedMap f
g : A → X
cont : Continuous g
inj : Function.Injective g
⊢ IsSeparatedMap (f ∘ g)

Tactic:
rw [isSeparatedMap_iff_isClosed_diagonal] at sep ⊢

Result:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed (Function.pullbackDiagonal f)
g : A → X
cont : Continuous g
inj : Function.Injective g
⊢ IsClosed (Function.pullbackDiagonal (f ∘ g))

Proof state:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed (Function.pullbackDiagonal f)
g : A → X
cont : Continuous g
inj : Function.Injective g
⊢ IsClosed (Function.pullbackDiagonal (f ∘ g))

Tactic:
rw [← inj.preimage_pullbackDiagonal]

Result:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed (Function.pullbackDiagonal f)
g : A → X
cont : Continuous g
inj : Function.Injective g
⊢ IsClosed (Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f)
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem inv_cpow_eq_ite (x : ℂ) (n : ℂ) :
    x⁻¹ ^ n = if x.arg = π then conj (x ^ conj n)⁻¹ else (x ^ n)⁻¹

Proof state:
x n : ℂ
⊢ x⁻¹ ^ n = if x.arg = π then (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else (x ^ n)⁻¹

Tactic:
simp_rw [Complex.cpow_def, log_inv_eq_ite, inv_eq_zero, map_eq_zero, ite_mul, neg_mul,
  RCLike.conj_inv, apply_ite conj, apply_ite exp, apply_ite Inv.inv, map_zero, map_one, exp_neg,
  inv_one, inv_zero, ← exp_conj, map_mul, conj_conj]

Result:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ else (cexp (log x * n))⁻¹) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else (cexp ((starRingEnd ℂ) (log x) * n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹

Proof state:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ else (cexp (log x * n))⁻¹) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else (cexp ((starRingEnd ℂ) (log x) * n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹

Tactic:
split_ifs with hx hn ha ha <;> rfl

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem orderOf_eq_card_of_forall_mem_zpowers {g : α} (hx : ∀ x, x ∈ zpowers g) :
    orderOf g = Nat.card α

Proof state:
α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = Nat.card α

Tactic:
rw [← Nat.card_zpowers, (zpowers g).eq_top_iff'.mpr hx, card_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem getElem_mapIdx (f : Nat → α → β) (as : Array α) (i : Nat)
    (h : i < (as.mapIdx f).size) :
    (as.mapIdx f)[i] = f i (as[i]'(by simp_all)) :=
  (mapIdx_spec _ _ (fun i b h => b = f i as[i]) fun _ _ => rfl).2 i (by simp_all)

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
as : Array α
i : Nat
h : i < (mapIdx f as).size
⊢ i < as.size

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type ?u.40839
β : Type ?u.40845
f : Nat → α → β
as : Array α
i : Nat
h : i < (mapIdx f as).size
⊢ i < as.size

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `mul_inv_lt_iff₀'` for a version with multiplication on the other side. -/
lemma mul_inv_lt_iff₀ (hc : 0 < c) : b * c⁻¹ < a ↔ b < a * c where
  mp h

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosStrictMono G₀
hc : 0 < c
h : b * c⁻¹ < a
⊢ b < a * c

Tactic:
simpa [hc.ne'] using mul_lt_mul_of_pos_right h hc

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosStrictMono G₀
hc : 0 < c
h : b < a * c
⊢ b * c⁻¹ < a

Tactic:
simpa [hc.ne'] using mul_lt_mul_of_pos_right h (inv_pos.2 hc)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem coordinate_eval_0 : (coordinate 0).eval (.ofList (a0 :: t)) = a0

Proof state:
a0 : Int
t : List Int
⊢ (coordinate 0).eval (Coeffs.ofList (a0 :: t)) = a0

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem chromaticNumber_eq_zero_of_isempty (G : SimpleGraph V) [IsEmpty V] :
    G.chromaticNumber = 0

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ G.chromaticNumber = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← Nat.cast_zero, chromaticNumber_le_iff_colorable]

Result:
V : Type u
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ G.Colorable 0

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ G.Colorable 0

Tactic:
apply colorable_of_isEmpty

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
lemma IsOfFinOrder.of_pow {n : ℕ} (h : IsOfFinOrder (a ^ n)) (hn : n ≠ 0) : IsOfFinOrder a

Proof state:
case intro.intro
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
hn : n ≠ 0
m : ℕ
hm : 0 < m
ha : (a ^ n) ^ m = 1
⊢ ∃ n, 0 < n ∧ a ^ n = 1

Tactic:
exact ⟨n * m, mul_pos hn.bot_lt hm, by rwa [pow_mul]⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
hn : n ≠ 0
m : ℕ
hm : 0 < m
ha : (a ^ n) ^ m = 1
⊢ a ^ (n * m) = 1

Tactic:
rwa [pow_mul]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
h : ∃ n_1, 0 < n_1 ∧ (a ^ n) ^ n_1 = 1
hn : n ≠ 0
⊢ ∃ n, 0 < n ∧ a ^ n = 1

Tactic:
rcases h with ⟨m, hm, ha⟩

Result:
case intro.intro
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
hn : n ≠ 0
m : ℕ
hm : 0 < m
ha : (a ^ n) ^ m = 1
⊢ ∃ n, 0 < n ∧ a ^ n = 1

Proof state:
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
h : IsOfFinOrder (a ^ n)
hn : n ≠ 0
⊢ IsOfFinOrder a

Tactic:
rw [isOfFinOrder_iff_pow_eq_one] at *

Result:
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
h : ∃ n_1, 0 < n_1 ∧ (a ^ n) ^ n_1 = 1
hn : n ≠ 0
⊢ ∃ n, 0 < n ∧ a ^ n = 1
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.ker_mulVecLin_eq_bot_iff {M : Matrix m n R} :
    (LinearMap.ker M.mulVecLin) = ⊥ ↔ ∀ v, M *ᵥ v = 0 → v = 0

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
⊢ ker M.mulVecLin = ⊥ ↔ ∀ (v : n → R), M *ᵥ v = 0 → v = 0

Tactic:
simp only [Submodule.eq_bot_iff, LinearMap.mem_ker, Matrix.mulVecLin_apply]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) :
    σ i.castSucc ≫ σ j = σ j.succ ≫ σ i

Proof state:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ σ i.castSucc ≫ σ j = σ j.succ ≫ σ i

Tactic:
apply CategoryTheory.Quotient.sound

Result:
case h
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ FreeSimplexQuiver.homRel
    (Paths.of.map (FreeSimplexQuiver.Hom.σ i.castSucc) ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ j))
    (Paths.of.map (FreeSimplexQuiver.Hom.σ j.succ) ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ i))

Proof state:
case h
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ FreeSimplexQuiver.homRel
    (Paths.of.map (FreeSimplexQuiver.Hom.σ i.castSucc) ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ j))
    (Paths.of.map (FreeSimplexQuiver.Hom.σ j.succ) ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ i))

Tactic:
exact FreeSimplexQuiver.homRel.σ_comp_σ H

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray

Proof state:
α : Type u_1
l : List α
as : Array α
⊢ foldl push as l = as ++ l.toArray

Tactic:
induction l generalizing as <;> simp [*]

Result:
no goals
-- Mathlib/GroupTheory/Exponent.lean
theorem _root_.MulOpposite.exponent : exponent (MulOpposite G) = exponent G

Proof state:
G : Type u
inst✝ : Monoid G
⊢ (if h : ∃ n, 0 < n ∧ ∀ (g : Gᵐᵒᵖ), g ^ n = 1 then Nat.find h else 0) =
    if h : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1 then Nat.find h else 0

Tactic:
congr!

Result:
case h₂.h.e'_1.h.h.e'_2.a
G : Type u
inst✝ : Monoid G
h_congr_thm✝ :
  ∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c), (∀ (h : c), x_1 ⋯ = u h) → (∀ (h : ¬c), y ⋯ = v h) → dite b x_1 y = dite c u v
h✝ : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1
x✝ : ℕ
⊢ (∀ (g : Gᵐᵒᵖ), g ^ x✝ = 1) ↔ ∀ (g : G), g ^ x✝ = 1

case h₁.h.e'_2.h.h.e'_2.a
G : Type u
inst✝ : Monoid G
x✝ : ℕ
⊢ (∀ (g : Gᵐᵒᵖ), g ^ x✝ = 1) ↔ ∀ (g : G), g ^ x✝ = 1

Proof state:
G : Type u
inst✝ : Monoid G
⊢ Monoid.exponent Gᵐᵒᵖ = Monoid.exponent G

Tactic:
simp only [Monoid.exponent, ExponentExists]

Result:
G : Type u
inst✝ : Monoid G
⊢ (if h : ∃ n, 0 < n ∧ ∀ (g : Gᵐᵒᵖ), g ^ n = 1 then Nat.find h else 0) =
    if h : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1 then Nat.find h else 0
-- Mathlib/CategoryTheory/Limits/EpiMono.lean
lemma epi_iff_inl_eq_inr (hc : IsColimit c) : Epi f ↔ c.inl = c.inr

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
⊢ Epi f

Tactic:
constructor

Result:
case mpr.left_cancellation
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
⊢ ∀ {Z : C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ c.inl = c.inr → Epi f

Tactic:
intro hf

Result:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
⊢ Epi f

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ Epi f → c.inl = c.inr

Tactic:
intro hf

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : Epi f
⊢ c.inl = c.inr

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ Epi f ↔ c.inl = c.inr

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ Epi f → c.inl = c.inr

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
⊢ c.inl = c.inr → Epi f

Proof state:
case mpr.left_cancellation.mk.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
φ : c.pt ⟶ Z
h : f ≫ c.inl ≫ φ = f ≫ c.inr ≫ φ
⊢ c.inl ≫ φ = c.inr ≫ φ

Tactic:
rw [hf]

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : Epi f
⊢ c.inl = c.inr

Tactic:
simpa only [← cancel_epi f] using c.condition

Result:
no goals

Proof state:
case mpr.left_cancellation
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
⊢ ∀ {Z : C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h

Tactic:
intro Z g g' h

Result:
case mpr.left_cancellation
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
g g' : Y ⟶ Z
h : f ≫ g = f ≫ g'
⊢ g = g'

Proof state:
case mpr.left_cancellation
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
g g' : Y ⟶ Z
h : f ≫ g = f ≫ g'
⊢ g = g'

Tactic:
obtain ⟨φ, rfl, rfl⟩ := PushoutCocone.IsColimit.desc' hc g g' h

Result:
case mpr.left_cancellation.mk.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
hf : c.inl = c.inr
Z : C
φ : c.pt ⟶ Z
h : f ≫ c.inl ≫ φ = f ≫ c.inr ≫ φ
⊢ c.inl ≫ φ = c.inr ≫ φ
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem isGood_mono {l : Products I} {o₁ o₂ : Ordinal} (h : o₁ ≤ o₂)
    (hl : l.isGood (π C (ord I · < o₁))) : l.isGood (π C (ord I · < o₂))

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : isGood (π C fun x => ord I x < o₁) l
⊢ isGood (π C fun x => ord I x < o₂) l

Tactic:
intro hl'

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : isGood (π C fun x => ord I x < o₁) l
hl' : eval (π C fun x => ord I x < o₂) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o₂) '' {m | m < l})
⊢ False

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : isGood (π C fun x => ord I x < o₁) l
hl' : eval (π C fun x => ord I x < o₂) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o₂) '' {m | m < l})
⊢ False

Tactic:
apply hl

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : isGood (π C fun x => ord I x < o₁) l
hl' : eval (π C fun x => ord I x < o₂) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o₂) '' {m | m < l})
⊢ eval (π C fun x => ord I x < o₁) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o₁) '' {m | m < l})

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : isGood (π C fun x => ord I x < o₁) l
hl' : eval (π C fun x => ord I x < o₂) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o₂) '' {m | m < l})
⊢ eval (π C fun x => ord I x < o₁) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o₁) '' {m | m < l})

Tactic:
rwa [eval_πs_image' C h (prop_of_isGood  C _ hl), ← eval_πs' C h (prop_of_isGood  C _ hl),
  Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C h)] at hl'

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem next_stop : ∀ {s}, Valid s → s.next ⟨s.bsize⟩ = ⟨s.bsize⟩
  | _, h => let ⟨l, m, r, h⟩ := h.validFor; by simp [h.bsize, h.next_stop]

Proof state:
x✝ : Substring
h✝ : x✝.Valid
l m r : List Char
h : ValidFor l m r x✝
⊢ x✝.next { byteIdx := x✝.bsize } = { byteIdx := x✝.bsize }

Tactic:
simp [h.bsize, h.next_stop]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
lemma algebraMap_apply_eq_form_iff {x y : span S (range P.root)} {s : S} :
    algebraMap S R s = B.form x y ↔ s = B.posForm x y

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
s : S
⊢ (algebraMap S R) s = (B.form ↑x) ↑y ↔ s = (B.posForm x) y

Tactic:
simp [RootPositiveForm.posForm]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem add_nsmul_modEq (n : ℕ) : a + n • p ≡ a [PMOD p] :=
  ⟨-n, by simp⟩

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a : α
n : ℕ
⊢ a - (a + n • p) = -↑n • p

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Flat/EquationalCriterion.lean
theorem exists_factorization_of_apply_eq_zero_of_free [Flat R M] {N : Type*} [AddCommGroup N]
    [Module R N] [Free R N] [Module.Finite R N] {f : N} {x : N →ₗ[R] M} (h : x f = 0) :
    ∃ (k : ℕ) (a : N →ₗ[R] (Fin k →₀ R)) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a f = 0 :=
  have e := ((Module.Free.chooseBasis R N).reindex (Fintype.equivFin _)).repr.symm
  have ⟨k, a, y, hya, haf⟩ := iff_forall_exists_factorization.mp ‹Flat R M›
    (f := e.symm f) (x := x ∘ₗ e) (by simpa using h)
  ⟨k, a ∘ₗ e.symm, y, by rwa [← comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm], haf⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Flat R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : N
x : N →ₗ[R] M
h : x f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ ↑e = y ∘ₗ a
haf : a (e.symm f) = 0
⊢ x = y ∘ₗ a ∘ₗ ↑e.symm

Tactic:
rwa [← comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Flat R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : N
x : N →ₗ[R] M
h : x f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
⊢ (x ∘ₗ ↑e) (e.symm f) = 0

Tactic:
simpa using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_bne [BEq α] {l : List α} : (l.all fun x => a != x) = !l.contains a

Proof state:
α : Type u_1
a : α
inst✝ : BEq α
l : List α
⊢ (l.all fun x => a != x) = !l.contains a

Tactic:
induction l <;> simp_all [bne]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_univ (f : α → ℝ≥0∞) : ∫⁻ x in univ, f x ∂μ = ∫⁻ x, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
rw [Measure.restrict_univ]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem mk'_sub (x₁ x₂ : R) (y₁ y₂ : M) :
    mk' S (x₁ * y₂ - x₂ * y₁) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ mk' S (x₁ * ↑y₂ - x₂ * ↑y₁) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, ← mk'_neg, ← mk'_add, neg_mul]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem aequiv_ofEquiv {U : Type*} [CommRing U] [Algebra R U] (h : IsAdjoinRoot S f)
    (h' : IsAdjoinRoot T f) (e : T ≃ₐ[R] U) : h.aequiv (h'.ofEquiv e) = (h.aequiv h').trans e

Proof state:
case h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
U : Type u_2
inst✝¹ : CommRing U
inst✝ : Algebra R U
h : IsAdjoinRoot S f
h' : IsAdjoinRoot T f
e : T ≃ₐ[R] U
a : S
⊢ (h.aequiv (h'.ofEquiv e)) a = ((h.aequiv h').trans e) a

Tactic:
rw [← h.map_repr a, aequiv_map, AlgEquiv.trans_apply, aequiv_map, ofEquiv_map_apply]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
U : Type u_2
inst✝¹ : CommRing U
inst✝ : Algebra R U
h : IsAdjoinRoot S f
h' : IsAdjoinRoot T f
e : T ≃ₐ[R] U
⊢ h.aequiv (h'.ofEquiv e) = (h.aequiv h').trans e

Tactic:
ext a

Result:
case h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
U : Type u_2
inst✝¹ : CommRing U
inst✝ : Algebra R U
h : IsAdjoinRoot S f
h' : IsAdjoinRoot T f
e : T ≃ₐ[R] U
a : S
⊢ (h.aequiv (h'.ofEquiv e)) a = ((h.aequiv h').trans e) a
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_eq_of_subset {f g : (∀ i, π i) → ℝ≥0∞} (hst : s ⊆ t)
    (hf : Measurable f) (hg : Measurable g) (hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ) :
    ∫⋯∫⁻_t, f ∂μ = ∫⋯∫⁻_t, g ∂μ

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f g : ((i : δ) → π i) → ℝ≥0∞
hst : s ⊆ t
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
⊢ ∫⋯∫⁻_t, f ∂μ = ∫⋯∫⁻_t, g ∂μ

Tactic:
rw [← union_sdiff_of_subset hst, lmarginal_union' μ f hf disjoint_sdiff,
  lmarginal_union' μ g hg disjoint_sdiff, hfg]

Result:
no goals