harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Relation.lean
theorem head_induction_on {P : ∀ a : α, TransGen r a b → Prop} {a : α} (h : TransGen r a b)
    (base : ∀ {a} (h : r a b), P a (single h))
    (ih : ∀ {a c} (h' : r a c) (h : TransGen r c b), P c h → P a (h.head h')) : P a h

Proof state:
case tail.base
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {P : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), P a ⋯) → (∀ {a c : α} (h' : r a c) (h : TransGen r c b), P c h → P a ⋯) → P a a✝
P : (a : α) → TransGen r a c → Prop
base : ∀ {a : α} (h : r a c), P a ⋯
ih : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), P c_1 h → P a ⋯
⊢ ∀ {a : α} (h : r a b), P a ⋯

Tactic:
exact fun h ↦ ih h (single hbc) (base hbc)

Result:
no goals

Proof state:
case single
α : Type u_1
r : α → α → Prop
b a b✝ : α
h : r a b✝
P : (a : α) → TransGen r a b✝ → Prop
base : ∀ {a : α} (h : r a b✝), P a ⋯
ih : ∀ {a c : α} (h' : r a c) (h : TransGen r c b✝), P c h → P a ⋯
⊢ P a ⋯

Tactic:
exact base h

Result:
no goals

Proof state:
case tail.ih
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {P : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), P a ⋯) → (∀ {a c : α} (h' : r a c) (h : TransGen r c b), P c h → P a ⋯) → P a a✝
P : (a : α) → TransGen r a c → Prop
base : ∀ {a : α} (h : r a c), P a ⋯
ih : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), P c_1 h → P a ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 b), P c_1 ⋯ → P a ⋯

Tactic:
exact fun hab hbc ↦ ih hab _

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {P : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), P a ⋯) → (∀ {a c : α} (h' : r a c) (h : TransGen r c b), P c h → P a ⋯) → P a a✝
P : (a : α) → TransGen r a c → Prop
base : ∀ {a : α} (h : r a c), P a ⋯
ih : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), P c_1 h → P a ⋯
⊢ P a ⋯

Tactic:
apply h_ih

Result:
case tail.base
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {P : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), P a ⋯) → (∀ {a c : α} (h' : r a c) (h : TransGen r c b), P c h → P a ⋯) → P a a✝
P : (a : α) → TransGen r a c → Prop
base : ∀ {a : α} (h : r a c), P a ⋯
ih : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), P c_1 h → P a ⋯
⊢ ∀ {a : α} (h : r a b), P a ⋯

case tail.ih
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {P : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), P a ⋯) → (∀ {a c : α} (h' : r a c) (h : TransGen r c b), P c h → P a ⋯) → P a a✝
P : (a : α) → TransGen r a c → Prop
base : ∀ {a : α} (h : r a c), P a ⋯
ih : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), P c_1 h → P a ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 b), P c_1 ⋯ → P a ⋯
-- Mathlib/Algebra/Group/Submonoid/MulOpposite.lean
theorem op_closure (s : Set M) : (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Proof state:
M : Type u_2
inst✝ : MulOneClass M
s : Set M
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Tactic:
congr with a

Result:
case e_a.h
M : Type u_2
inst✝ : MulOneClass M
s : Set M
a : Submonoid Mᵐᵒᵖ
⊢ a ∈ {a | s ⊆ MulOpposite.op ⁻¹' ↑a} ↔ a ∈ {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Proof state:
M : Type u_2
inst✝ : MulOneClass M
s : Set M
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
simp_rw [closure, op_sInf, Set.preimage_setOf_eq, Submonoid.coe_unop]

Result:
M : Type u_2
inst✝ : MulOneClass M
s : Set M
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Proof state:
case e_a.h
M : Type u_2
inst✝ : MulOneClass M
s : Set M
a : Submonoid Mᵐᵒᵖ
⊢ a ∈ {a | s ⊆ MulOpposite.op ⁻¹' ↑a} ↔ a ∈ {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Tactic:
exact MulOpposite.unop_surjective.forall

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem minimal_subtype {x : Subtype Q} :
    Minimal (fun x ↦ P x.1) x ↔ Minimal (P ⊓ Q) x

Proof state:
α : Type u_1
P Q : α → Prop
inst✝ : LE α
x : Subtype Q
⊢ Minimal (fun x => P ↑x) x ↔ Minimal (P ⊓ Q) ↑x

Tactic:
obtain ⟨x, hx⟩ := x

Result:
case mk
α : Type u_1
P Q : α → Prop
inst✝ : LE α
x : α
hx : Q x
⊢ Minimal (fun x => P ↑x) ⟨x, hx⟩ ↔ Minimal (P ⊓ Q) ↑⟨x, hx⟩

Proof state:
case mk
α : Type u_1
P Q : α → Prop
inst✝ : LE α
x : α
hx : Q x
⊢ (P x ∧ ∀ (a : α), Q a → P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y

Tactic:
tauto

Result:
no goals

Proof state:
case mk
α : Type u_1
P Q : α → Prop
inst✝ : LE α
x : α
hx : Q x
⊢ Minimal (fun x => P ↑x) ⟨x, hx⟩ ↔ Minimal (P ⊓ Q) ↑⟨x, hx⟩

Tactic:
simp only [Minimal, Subtype.forall, Subtype.mk_le_mk, Pi.inf_apply, inf_Prop_eq]

Result:
case mk
α : Type u_1
P Q : α → Prop
inst✝ : LE α
x : α
hx : Q x
⊢ (P x ∧ ∀ (a : α), Q a → P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
-- Mathlib/Data/Multiset/UnionInter.lean
lemma union_add_inter (s t : Multiset α) : s ∪ t + s ∩ t = s + t

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ≤ (s ∪ t + s) ∩ (s ∪ t + t)

Tactic:
refine le_inter (Multiset.add_le_add_right le_union_right) ?_

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ≤ s ∪ t + t

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t ≤ s ∪ t + s ∩ t

Tactic:
rw [Multiset.add_comm, add_inter_distrib]

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ≤ (s ∪ t + s) ∩ (s ∪ t + t)

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ∩ t ≤ s + t

Tactic:
rw [Multiset.add_comm]

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t + t ≤ s + t

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∪ t + s ∩ t ≤ s + t

Tactic:
rw [union_add_distrib]

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + s ∩ t ∪ (t + s ∩ t) ≤ s + t

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t + t ≤ s + t

Tactic:
exact Multiset.add_le_add_right inter_le_left

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ≤ s ∪ t + t

Tactic:
rw [Multiset.add_comm]

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t ≤ s ∪ t + t

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + s ∩ t ∪ (t + s ∩ t) ≤ s + t

Tactic:
refine union_le (Multiset.add_le_add_left inter_le_right) ?_

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ∩ t ≤ s + t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∪ t + s ∩ t = s + t

Tactic:
apply _root_.le_antisymm

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∪ t + s ∩ t ≤ s + t

case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t ≤ s ∪ t + s ∩ t

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t ≤ s ∪ t + t

Tactic:
exact Multiset.add_le_add_right le_union_left

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
lemma toSpec_injective {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
    Function.Injective (toSpec 𝒜 f)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x₁ x₂ : ↑↑(Proj.restrict ⋯).toPresheafedSpace
h : (ConcreteCategory.hom (toSpec 𝒜 f)) x₁ = (ConcreteCategory.hom (toSpec 𝒜 f)) x₂
⊢ x₁ = x₂

Tactic:
have := congr_arg (FromSpec.toFun f_deg hm) h

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x₁ x₂ : ↑↑(Proj.restrict ⋯).toPresheafedSpace
h : (ConcreteCategory.hom (toSpec 𝒜 f)) x₁ = (ConcreteCategory.hom (toSpec 𝒜 f)) x₂
this :
  FromSpec.toFun f_deg hm ((ConcreteCategory.hom (toSpec 𝒜 f)) x₁) =
    FromSpec.toFun f_deg hm ((ConcreteCategory.hom (toSpec 𝒜 f)) x₂)
⊢ x₁ = x₂

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ Function.Injective ⇑(ConcreteCategory.hom (toSpec 𝒜 f))

Tactic:
intro x₁ x₂ h

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x₁ x₂ : ↑↑(Proj.restrict ⋯).toPresheafedSpace
h : (ConcreteCategory.hom (toSpec 𝒜 f)) x₁ = (ConcreteCategory.hom (toSpec 𝒜 f)) x₂
⊢ x₁ = x₂

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x₁ x₂ : ↑↑(Proj.restrict ⋯).toPresheafedSpace
h : (ConcreteCategory.hom (toSpec 𝒜 f)) x₁ = (ConcreteCategory.hom (toSpec 𝒜 f)) x₂
this :
  FromSpec.toFun f_deg hm ((ConcreteCategory.hom (toSpec 𝒜 f)) x₁) =
    FromSpec.toFun f_deg hm ((ConcreteCategory.hom (toSpec 𝒜 f)) x₂)
⊢ x₁ = x₂

Tactic:
rwa [fromSpec_toSpec, fromSpec_toSpec] at this

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFree_map_iff {f : α ↪ β} [Nonempty α] :
    (G.map f).CliqueFree n ↔ G.CliqueFree n

Proof state:
case inl.inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
inst✝ : Nonempty α
hle : 1 ≤ 1
⊢ (SimpleGraph.map f G).CliqueFree 1 ↔ G.CliqueFree 1

Tactic:
simp [CliqueFree, show ∃ (_ : β), True from ⟨f (Classical.arbitrary _), trivial⟩]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
f : α ↪ β
inst✝ : Nonempty α
⊢ (SimpleGraph.map f G).CliqueFree n ↔ G.CliqueFree n

Tactic:
obtain (hle | hlt) := le_or_lt n 1

Result:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
f : α ↪ β
inst✝ : Nonempty α
hle : n ≤ 1
⊢ (SimpleGraph.map f G).CliqueFree n ↔ G.CliqueFree n

case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
f : α ↪ β
inst✝ : Nonempty α
hlt : 1 < n
⊢ (SimpleGraph.map f G).CliqueFree n ↔ G.CliqueFree n

Proof state:
case inl.inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
inst✝ : Nonempty α
hle : 0 ≤ 1
⊢ (SimpleGraph.map f G).CliqueFree 0 ↔ G.CliqueFree 0

Tactic:
simp [CliqueFree]

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
f : α ↪ β
inst✝ : Nonempty α
hle : n ≤ 1
⊢ (SimpleGraph.map f G).CliqueFree n ↔ G.CliqueFree n

Tactic:
obtain (rfl | rfl) := Nat.le_one_iff_eq_zero_or_eq_one.1 hle

Result:
case inl.inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
inst✝ : Nonempty α
hle : 0 ≤ 1
⊢ (SimpleGraph.map f G).CliqueFree 0 ↔ G.CliqueFree 0

case inl.inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
inst✝ : Nonempty α
hle : 1 ≤ 1
⊢ (SimpleGraph.map f G).CliqueFree 1 ↔ G.CliqueFree 1

Proof state:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
f : α ↪ β
inst✝ : Nonempty α
hlt : 1 < n
⊢ (SimpleGraph.map f G).CliqueFree n ↔ G.CliqueFree n

Tactic:
simp [CliqueFree, isNClique_map_iff hlt]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
/-- If each component of the counit is an epimorphism, then the right adjoint is faithful. -/
lemma faithful_R_of_epi_counit_app [∀ X, Epi (h.counit.app X)] : R.Faithful where
  map_injective {X Y f g} hfg

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), Epi (h.counit.app X)
X Y : D
f g : X ⟶ Y
hfg : R.map f = R.map g
⊢ f = g

Tactic:
apply Epi.left_cancellation (f := h.counit.app X)

Result:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), Epi (h.counit.app X)
X Y : D
f g : X ⟶ Y
hfg : R.map f = R.map g
⊢ h.counit.app X ≫ f = h.counit.app X ≫ g

Proof state:
case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), Epi (h.counit.app X)
X Y : D
f g : X ⟶ Y
hfg : R.map f = R.map g
⊢ (h.homEquiv (R.obj X) Y) (h.counit.app X ≫ f) = (h.homEquiv (R.obj X) Y) (h.counit.app X ≫ g)

Tactic:
simpa using hfg

Result:
no goals

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), Epi (h.counit.app X)
X Y : D
f g : X ⟶ Y
hfg : R.map f = R.map g
⊢ h.counit.app X ≫ f = h.counit.app X ≫ g

Tactic:
apply (h.homEquiv (R.obj X) Y).injective

Result:
case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), Epi (h.counit.app X)
X Y : D
f g : X ⟶ Y
hfg : R.map f = R.map g
⊢ (h.homEquiv (R.obj X) Y) (h.counit.app X ≫ f) = (h.homEquiv (R.obj X) Y) (h.counit.app X ≫ g)
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem Int.alternating_sum_range_choose {n : ℕ} :
    (∑ m ∈ range (n + 1), ((-1) ^ m * n.choose m : ℤ)) = if n = 0 then 1 else 0

Proof state:
case succ
n : ℕ
⊢ ∑ m ∈ range (n + 1 + 1), (-1) ^ m * ↑((n + 1).choose m) = if n + 1 = 0 then 1 else 0

Tactic:
have h := add_pow (-1 : ℤ) 1 n.succ

Result:
case succ
n : ℕ
h : (-1 + 1) ^ n.succ = ∑ m ∈ range (n.succ + 1), (-1) ^ m * 1 ^ (n.succ - m) * ↑(n.succ.choose m)
⊢ ∑ m ∈ range (n + 1 + 1), (-1) ^ m * ↑((n + 1).choose m) = if n + 1 = 0 then 1 else 0

Proof state:
case succ
n : ℕ
h : 0 ^ n.succ = ∑ x ∈ range (n.succ + 1), (-1) ^ x * ↑(n.succ.choose x)
⊢ ∑ m ∈ range (n + 1 + 1), (-1) ^ m * ↑((n + 1).choose m) = if n + 1 = 0 then 1 else 0

Tactic:
rw [← h, zero_pow n.succ_ne_zero, if_neg n.succ_ne_zero]

Result:
no goals

Proof state:
case zero

⊢ ∑ m ∈ range (0 + 1), (-1) ^ m * ↑(Nat.choose 0 m) = if 0 = 0 then 1 else 0

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ ∑ m ∈ range (n + 1), (-1) ^ m * ↑(n.choose m) = if n = 0 then 1 else 0

Tactic:
cases n with
| zero => simp
| succ n =>
  have h := add_pow (-1 : ℤ) 1 n.succ
  simp only [one_pow, mul_one, neg_add_cancel] at h
  rw [← h, zero_pow n.succ_ne_zero, if_neg n.succ_ne_zero]

Result:
no goals

Proof state:
case succ
n : ℕ
h : (-1 + 1) ^ n.succ = ∑ m ∈ range (n.succ + 1), (-1) ^ m * 1 ^ (n.succ - m) * ↑(n.succ.choose m)
⊢ ∑ m ∈ range (n + 1 + 1), (-1) ^ m * ↑((n + 1).choose m) = if n + 1 = 0 then 1 else 0

Tactic:
simp only [one_pow, mul_one, neg_add_cancel] at h

Result:
case succ
n : ℕ
h : 0 ^ n.succ = ∑ x ∈ range (n.succ + 1), (-1) ^ x * ↑(n.succ.choose x)
⊢ ∑ m ∈ range (n + 1 + 1), (-1) ^ m * ↑((n + 1).choose m) = if n + 1 = 0 then 1 else 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H : buckets.WF)
    (h₁ : ∀ [PartialEquivBEq α] [LawfulHashable α],
      (buckets.1[i].toList.Pairwise fun a b => ¬(a.1 == b.1)) →
      d.toList.Pairwise fun a b => ¬(a.1 == b.1))
    (h₂ : (buckets.1[i].All fun k _ => ((hash k).toUSize % .ofNat buckets.1.size).toNat = i.toNat) →
      d.All fun k _ => ((hash k).toUSize % USize.ofNat buckets.1.size).toNat = i.toNat) :
    (buckets.update i d h).WF

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Buckets α β
i✝ : USize
d : AssocList α β
h : i✝.toNat < buckets.val.size
H : buckets.WF
h₁ :
  ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) buckets.val[i✝].toList →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) d.toList
h₂ :
  AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) buckets.val[i✝] →
    AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) d
i : Nat
hi : i < (buckets.update i✝ d h).val.size
p : α × β
eq : i✝.toNat = i
hp : p ∈ d.toList
⊢ ((hash p.fst).toUSize % USize.ofNat buckets.val.size).toNat = i

Tactic:
exact eq ▸ h₂ (H.2 _ _) _ hp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : Vector α n) (init : γ) :
    (l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
init : γ
l : Array α
⊢ Array.foldr g init (Array.filterMap f { toArray := l, size_toArray := ⋯ }.toArray) =
    foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.foldr_filterMap']

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
init : γ
l : Array α
⊢ Array.foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init l =
    Array.foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init l

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → Option β
g : β → γ → γ
l : Vector α n
init : γ
⊢ Array.foldr g init (Array.filterMap f l.toArray) =
    foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
init : γ
l : Array α
⊢ Array.foldr g init (Array.filterMap f { toArray := l, size_toArray := ⋯ }.toArray) =
    foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
init : γ
l : Array α
⊢ Array.foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init l =
    Array.foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init l

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_insertList_of_mem [BEq α] [EquivBEq α]
    {l toInsert : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k')
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ toInsert.map Sigma.fst)
    {h} :
    getKey k' (insertList l toInsert) h = k

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : k ∈ List.map Sigma.fst toInsert
h : containsKey k' (insertList l toInsert) = true
⊢ getKey k' (insertList l toInsert) h = k

Tactic:
rw [← Option.some_inj, ← getKey?_eq_some_getKey,
  getKey?_insertList_of_mem k_beq distinct_l distinct_toInsert mem]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma rightUnshift_add {n' a : ℤ} (γ₁ γ₂ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n) :
    (γ₁ + γ₂).rightUnshift n hn = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ₁ γ₂ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn

Tactic:
apply _root_.map_add

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ₁ γ₂ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ (γ₁ + γ₂).rightUnshift n hn = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn

Tactic:
change (rightShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = _

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ₁ γ₂ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem mul_eq_bot [NoZeroDivisors R] : I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥ :=
  ⟨fun hij =>
    or_iff_not_imp_left.mpr fun I_ne_bot =>
      J.eq_bot_iff.mpr fun j hj =>
        let ⟨i, hi, ne0⟩ := I.ne_bot_iff.mp I_ne_bot
        Or.resolve_left (mul_eq_zero.mp ((I * J).eq_bot_iff.mp hij _ (mul_mem_mul hi hj))) ne0,
    fun h => by obtain rfl | rfl := h; exacts [bot_mul _, mul_bot _]⟩

Proof state:
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : NoZeroDivisors R
h : I = ⊥ ∨ J = ⊥
⊢ I * J = ⊥

Tactic:
obtain rfl | rfl := h

Result:
case inl
R : Type u
inst✝¹ : Semiring R
J : Ideal R
inst✝ : NoZeroDivisors R
⊢ ⊥ * J = ⊥

case inr
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : NoZeroDivisors R
⊢ I * ⊥ = ⊥

Proof state:
case inl
R : Type u
inst✝¹ : Semiring R
J : Ideal R
inst✝ : NoZeroDivisors R
⊢ ⊥ * J = ⊥

case inr
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : NoZeroDivisors R
⊢ I * ⊥ = ⊥

Tactic:
exacts [bot_mul _, mul_bot _]

Result:
no goals
-- Mathlib/Algebra/Group/Translate.lean
lemma translate_translate (a b : G) (f : G → α) : τ a (τ b f) = τ (a + b) f

Proof state:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
⊢ τ a (τ b f) = τ (a + b) f

Tactic:
ext

Result:
case h
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
x✝ : G
⊢ τ a (τ b f) x✝ = τ (a + b) f x✝

Proof state:
case h
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
x✝ : G
⊢ τ a (τ b f) x✝ = τ (a + b) f x✝

Tactic:
simp [sub_sub]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem smul_mem_of_mem_closure_of_mem {X : Type*} [MulAction G X] {s : Set G} {t : Set X}
    (hs : ∀ g ∈ s, g⁻¹ ∈ s) (hst : ∀ᵉ (g ∈ s) (x ∈ t), g • x ∈ t) {g : G}
    (hg : g ∈ Subgroup.closure s) {x : X} (hx : x ∈ t) : g • x ∈ t

Proof state:
case inv_mem
G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g g' : G
hg' : g' ∈ s
x : X
hx : x ∈ t
⊢ g'⁻¹ • x ∈ t

Tactic:
exact hst g'⁻¹ (hs g' hg') x hx

Result:
no goals

Proof state:
G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g : G
hg : g ∈ closure s
x : X
hx : x ∈ t
⊢ g • x ∈ t

Tactic:
induction hg using Subgroup.closure_induction'' generalizing x with
| one => simpa
| mem g' hg' => exact hst g' hg' x hx
| inv_mem g' hg' => exact hst g'⁻¹ (hs g' hg') x hx
| mul _ _ _ _ h₁ h₂ => rw [mul_smul]; exact h₁ (h₂ hx)

Result:
no goals

Proof state:
case mul
G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g x✝ y✝ : G
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : ∀ {x : X}, x ∈ t → x✝ • x ∈ t
h₂ : ∀ {x : X}, x ∈ t → y✝ • x ∈ t
x : X
hx : x ∈ t
⊢ x✝ • y✝ • x ∈ t

Tactic:
exact h₁ (h₂ hx)

Result:
no goals

Proof state:
case mem
G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g g' : G
hg' : g' ∈ s
x : X
hx : x ∈ t
⊢ g' • x ∈ t

Tactic:
exact hst g' hg' x hx

Result:
no goals

Proof state:
case one
G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g : G
x : X
hx : x ∈ t
⊢ 1 • x ∈ t

Tactic:
simpa

Result:
no goals

Proof state:
case mul
G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g x✝ y✝ : G
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : ∀ {x : X}, x ∈ t → x✝ • x ∈ t
h₂ : ∀ {x : X}, x ∈ t → y✝ • x ∈ t
x : X
hx : x ∈ t
⊢ (x✝ * y✝) • x ∈ t

Tactic:
rw [mul_smul]

Result:
case mul
G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g x✝ y✝ : G
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : ∀ {x : X}, x ∈ t → x✝ • x ∈ t
h₂ : ∀ {x : X}, x ∈ t → y✝ • x ∈ t
x : X
hx : x ∈ t
⊢ x✝ • y✝ • x ∈ t