harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/NAry.lean
theorem card_dvd_card_image₂_right (hf : ∀ a ∈ s, Injective (f a))
    (hs : ((fun a => t.image <| f a) '' s).PairwiseDisjoint id) : #t ∣ #(image₂ f s t)

Proof state:
case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
ih : #t ∣ #(image₂ f s t)
h : ∃ x, ∃ (_ : x ∈ s), ¬Disjoint (image (f a) t) (image (f x) t)
⊢ #t ∣ #(image (fun b => f a b) t ∪ image₂ f s t)

Tactic:
obtain ⟨b, hb, h⟩ := h

Result:
case neg.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
ih : #t ∣ #(image₂ f s t)
b : α
hb : b ∈ s
h : ¬Disjoint (image (f a) t) (image (f b) t)
⊢ #t ∣ #(image (fun b => f a b) t ∪ image₂ f s t)
-- Mathlib/Data/Finset/Grade.lean
protected lemma isAtom_iff : IsAtom s ↔ ∃ a, s = {a}

Proof state:
α : Type u_1
s : Finset α
⊢ IsAtom s ↔ ∃ a, s = {a}

Tactic:
simp [← bot_covBy_iff, covBy_iff_exists_cons, eq_comm]

Result:
no goals
-- Mathlib/Topology/Homotopy/Contractible.lean
theorem id_nullhomotopic (X : Type*) [TopologicalSpace X] [ContractibleSpace X] :
    (ContinuousMap.id X).Nullhomotopic

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ (ContinuousMap.id X).Homotopic (const X (hv.invFun ()))

Tactic:
convert hv.left_inv.symm

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
⊢ (ContinuousMap.id X).Nullhomotopic

Tactic:
obtain ⟨hv⟩ := ContractibleSpace.hequiv_unit X

Result:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ (ContinuousMap.id X).Nullhomotopic

Proof state:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ (ContinuousMap.id X).Nullhomotopic

Tactic:
use hv.invFun ()

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ (ContinuousMap.id X).Homotopic (const X (hv.invFun ()))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem add_one_le_iff {n : Nat} : ∀ {k : Fin (n + 1)}, k + 1 ≤ k ↔ k = last _

Proof state:
n✝ n : Nat
k : Fin (n + 2)
⊢ (if k = last (n + 1) then 0 else ↑k + 1) ≠ ↑k

Tactic:
split <;> simp [*, (Nat.succ_ne_zero _).symm, Nat.ne_of_gt (Nat.lt_succ_self _)]

Result:
no goals

Proof state:
n✝ n : Nat
k : Fin (n + 2)
⊢ ↑(k + 1) ≠ ↑k

Tactic:
rw [val_add_one]

Result:
n✝ n : Nat
k : Fin (n + 2)
⊢ (if k = last (n + 1) then 0 else ↑k + 1) ≠ ↑k

Proof state:
n✝ n : Nat
⊢ ∀ {k : Fin (n + 1 + 1)}, k + 1 ≤ k ↔ k = last (n + 1)

Tactic:
intro (k : Fin (n+2))

Result:
n✝ n : Nat
k : Fin (n + 2)
⊢ k + 1 ≤ k ↔ k = last (n + 1)

Proof state:
n : Nat
⊢ ∀ {k : Fin (0 + 1)}, k + 1 ≤ k ↔ k = last 0

Tactic:
intro (k : Fin 1)

Result:
n : Nat
k : Fin 1
⊢ k + 1 ≤ k ↔ k = last 0

Proof state:
n : Nat
⊢ ∀ {k : Fin (n + 1)}, k + 1 ≤ k ↔ k = last n

Tactic:
match n with
| 0 =>
  intro (k : Fin 1)
  exact iff_of_true (Subsingleton.elim (α := Fin 1) (k+1) _ ▸ Nat.le_refl _) (fin_one_eq_zero ..)
| n + 1 =>
  intro (k : Fin (n+2))
  rw [← add_one_lt_iff, lt_def, le_def, Nat.lt_iff_le_and_ne, and_iff_left]
  rw [val_add_one]
  split <;> simp [*, (Nat.succ_ne_zero _).symm, Nat.ne_of_gt (Nat.lt_succ_self _)]

Result:
no goals

Proof state:
n : Nat
k : Fin 1
⊢ k + 1 ≤ k ↔ k = last 0

Tactic:
exact iff_of_true (Subsingleton.elim (α := Fin 1) (k+1) _ ▸ Nat.le_refl _) (fin_one_eq_zero ..)

Result:
no goals

Proof state:
n✝ n : Nat
k : Fin (n + 2)
⊢ k + 1 ≤ k ↔ k = last (n + 1)

Tactic:
rw [← add_one_lt_iff, lt_def, le_def, Nat.lt_iff_le_and_ne, and_iff_left]

Result:
n✝ n : Nat
k : Fin (n + 2)
⊢ ↑(k + 1) ≠ ↑k
-- Mathlib/Algebra/Lie/TraceForm.lean
@[simp] lemma mem_killingCompl {x : L} :
    x ∈ I.killingCompl ↔ ∀ y ∈ I, killingForm R L y x = 0

Proof state:
R : Type u_1
L : Type u_3
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ x ∈ killingCompl R L I ↔ ∀ y ∈ I, ((killingForm R L) y) x = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma isDiameter_ofDiameter (p₁ p₂ : P) : (Sphere.ofDiameter p₁ p₂).IsDiameter p₁ p₂ :=
  ⟨by simp [Sphere.ofDiameter, mem_sphere, inv_mul_eq_div], rfl⟩

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ p₁ ∈ Sphere.ofDiameter p₁ p₂

Tactic:
simp [Sphere.ofDiameter, mem_sphere, inv_mul_eq_div]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_polynomial : (W'.map f).toProjective.polynomial = MvPolynomial.map f W'.polynomial

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ (map W' f).toProjective.polynomial = (MvPolynomial.map f) W'.polynomial

Tactic:
simp only [polynomial]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ X y ^ 2 * X z + C (map W' f).toProjective.a₁ * X x * X y * X z + C (map W' f).toProjective.a₃ * X y * X z ^ 2 -
      (X x ^ 3 + C (map W' f).toProjective.a₂ * X x ^ 2 * X z + C (map W' f).toProjective.a₄ * X x * X z ^ 2 +
        C (map W' f).toProjective.a₆ * X z ^ 3) =
    (MvPolynomial.map f)
      (X y ^ 2 * X z + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 2 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z + C W'.a₄ * X x * X z ^ 2 + C W'.a₆ * X z ^ 3))

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ X y ^ 2 * X z + C (map W' f).toProjective.a₁ * X x * X y * X z + C (map W' f).toProjective.a₃ * X y * X z ^ 2 -
      (X x ^ 3 + C (map W' f).toProjective.a₂ * X x ^ 2 * X z + C (map W' f).toProjective.a₄ * X x * X z ^ 2 +
        C (map W' f).toProjective.a₆ * X z ^ 3) =
    (MvPolynomial.map f)
      (X y ^ 2 * X z + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 2 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z + C W'.a₄ * X x * X z ^ 2 + C W'.a₆ * X z ^ 3))

Tactic:
map_simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatMap_map (f : α → β) (g : β → Array γ) (l : Array α) :
    (map f l).flatMap g = l.flatMap (fun a => g (f a))

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → Array γ
l : List α
⊢ flatMap g (map f { toList := l }) = flatMap (fun a => g (f a)) { toList := l }

Tactic:
simp [List.flatMap_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → Array γ
l : Array α
⊢ flatMap g (map f l) = flatMap (fun a => g (f a)) l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → Array γ
l : List α
⊢ flatMap g (map f { toList := l }) = flatMap (fun a => g (f a)) { toList := l }
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem coequalizer.isoTargetOfSelf_hom :
    (coequalizer.isoTargetOfSelf f).hom = coequalizer.desc (𝟙 Y) (by simp)

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ π f f ≫ (isoTargetOfSelf f).hom = π f f ≫ desc (𝟙 Y) ⋯

Tactic:
simp [coequalizer.isoTargetOfSelf]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (isoTargetOfSelf f).hom = desc (𝟙 Y) ⋯

Tactic:
ext

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ π f f ≫ (isoTargetOfSelf f).hom = π f f ≫ desc (𝟙 Y) ⋯

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ f ≫ 𝟙 Y = f ≫ 𝟙 Y

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem sublist_reverse_iff : l₁ <+ l₂.reverse ↔ l₁.reverse <+ l₂ :=
  by rw [← reverse_sublist, reverse_reverse]

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁ <+ l₂.reverse ↔ l₁.reverse <+ l₂

Tactic:
rw [← reverse_sublist, reverse_reverse]

Result:
no goals
-- Mathlib/Data/DFinsupp/Ext.lean
theorem add_closure_iUnion_range_single :
    AddSubmonoid.closure (⋃ i : ι, Set.range (single i : β i → Π₀ i, β i)) = ⊤ :=
  top_unique fun x _ => by
    apply DFinsupp.induction x
    · exact AddSubmonoid.zero_mem _
    exact fun a b f _ _ hf =>
      AddSubmonoid.add_mem _
        (AddSubmonoid.subset_closure <| Set.mem_iUnion.2 ⟨a, Set.mem_range_self _⟩) hf

Proof state:
case h0
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ 0 ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))

Tactic:
exact AddSubmonoid.zero_mem _

Result:
no goals

Proof state:
case ha
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i),
    f i = 0 →
      b ≠ 0 →
        f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i)) →
          single i b + f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))

Tactic:
exact fun a b f _ _ hf =>
  AddSubmonoid.add_mem _
    (AddSubmonoid.subset_closure <| Set.mem_iUnion.2 ⟨a, Set.mem_range_self _⟩) hf

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ x ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))

Tactic:
apply DFinsupp.induction x

Result:
case h0
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ 0 ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))

case ha
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i),
    f i = 0 →
      b ≠ 0 →
        f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i)) →
          single i b + f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))
-- Mathlib/Algebra/Group/End.lean
@[to_additive existing (attr := simp) zpow_addRight]
lemma zpow_mulRight : ∀ n : ℤ, Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)
  | Int.ofNat n => by simp
  | Int.negSucc n => by simp

Proof state:
α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulRight a ^ Int.negSucc n = Equiv.mulRight (a ^ Int.negSucc n)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulRight a ^ Int.ofNat n = Equiv.mulRight (a ^ Int.ofNat n)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem eval₂_gcd_eq_zero [CommSemiring k] [DecidableEq R]
    {ϕ : R →+* k} {f g : R[X]} {α : k} (hf : f.eval₂ ϕ α = 0)
    (hg : g.eval₂ ϕ α = 0) : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0

Proof state:
R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0

Tactic:
rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
  Polynomial.eval₂_mul, hf, hg, zero_mul, zero_mul, zero_add]

Result:
no goals
-- Mathlib/NumberTheory/FunctionField.lean
theorem inftyValuation.C {k : Fq} (hk : k ≠ 0) :
    inftyValuationDef Fq (RatFunc.C k) = Multiplicative.ofAdd (0 : ℤ)

Proof state:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
k : Fq
hk : k ≠ 0
hCk : RatFunc.C k ≠ 0
⊢ inftyValuationDef Fq (RatFunc.C k) = ↑(Multiplicative.ofAdd 0)

Tactic:
rw [inftyValuationDef, if_neg hCk, RatFunc.intDegree_C]

Result:
no goals

Proof state:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
k : Fq
hk : k ≠ 0
⊢ inftyValuationDef Fq (RatFunc.C k) = ↑(Multiplicative.ofAdd 0)

Tactic:
have hCk : RatFunc.C k ≠ 0 := (map_ne_zero _).mpr hk

Result:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
k : Fq
hk : k ≠ 0
hCk : RatFunc.C k ≠ 0
⊢ inftyValuationDef Fq (RatFunc.C k) = ↑(Multiplicative.ofAdd 0)
-- Mathlib/Tactic/Linarith/Lemmas.lean
@[nolint unusedArguments]
lemma zero_mul_eq {α} {R : α → α → Prop} [Semiring α] {a b : α} (h : a = 0) (_ : R b 0) :
    a * b = 0

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : Semiring α
a b : α
h : a = 0
x✝ : R b 0
⊢ a * b = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/SetTheory/Lists.lean
theorem equiv_atom {a} {l : Lists α} : atom a ~ l ↔ atom a = l :=
  ⟨fun h => by cases h; rfl, fun h => h ▸ Equiv.refl _⟩

Proof state:
case refl
α : Type u_1
a : α
⊢ atom a = atom a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
a : α
l : Lists α
h : atom a ~ l
⊢ atom a = l

Tactic:
cases h

Result:
case refl
α : Type u_1
a : α
⊢ atom a = atom a
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Finset.Nonempty.csSup_mem {s : Finset α} (h : s.Nonempty) : sSup (s : Set α) ∈ s

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Finset α
h : s.Nonempty
⊢ sSup ↑s ∈ s

Tactic:
rw [h.csSup_eq_max']

Result:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Finset α
h : s.Nonempty
⊢ s.max' h ∈ s

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Finset α
h : s.Nonempty
⊢ s.max' h ∈ s

Tactic:
exact s.max'_mem _

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma ofHom_desc :
    Cochain.ofHom (desc φ α β eq) = descCochain φ α (Cochain.ofHom β) (neg_add_cancel 1)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
⊢ Cochain.ofHom (desc φ α β eq) = descCochain φ α (Cochain.ofHom β) ⋯

Tactic:
simp [desc]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_dvd_prod_of_le (h : s ≤ t) : s.prod ∣ t.prod

Proof state:
case intro
α : Type u_3
inst✝ : CommMonoid α
s z : Multiset α
h : s ≤ s + z
⊢ s.prod ∣ (s + z).prod

Tactic:
simp only [prod_add, dvd_mul_right]

Result:
no goals

Proof state:
α : Type u_3
inst✝ : CommMonoid α
s t : Multiset α
h : s ≤ t
⊢ s.prod ∣ t.prod

Tactic:
obtain ⟨z, rfl⟩ := exists_add_of_le h

Result:
case intro
α : Type u_3
inst✝ : CommMonoid α
s z : Multiset α
h : s ≤ s + z
⊢ s.prod ∣ (s + z).prod
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem prod_le_iff {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
    H.prod K ≤ J ↔ map (MonoidHom.inl G N) H ≤ J ∧ map (MonoidHom.inr G N) K ≤ J

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
K : Subgroup N
J : Subgroup (G × N)
⊢ H.prod K ≤ J ↔ map (MonoidHom.inl G N) H ≤ J ∧ map (MonoidHom.inr G N) K ≤ J

Tactic:
simpa only [← Subgroup.toSubmonoid_le] using Submonoid.prod_le_iff

Result:
no goals
-- Mathlib/Algebra/Group/Int/Even.lean
@[parity_simps] lemma even_add_one : Even (n + 1) ↔ ¬Even n

Proof state:
n : ℤ
⊢ Even (n + 1) ↔ ¬Even n

Tactic:
simp [even_add]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem iInf_coe {ι} (p : ι → Submodule R M) : (↑(⨅ i, p i) : Set M) = ⋂ i, ↑(p i)

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
⊢ ⋂ p_1 ∈ Set.range fun i => p i, ↑p_1 = ⋂ i, ↑(p i)

Tactic:
simp only [Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq']

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
⊢ ↑(⨅ i, p i) = ⋂ i, ↑(p i)

Tactic:
rw [iInf, sInf_coe]

Result:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
⊢ ⋂ p_1 ∈ Set.range fun i => p i, ↑p_1 = ⋂ i, ↑(p i)
-- Mathlib/RingTheory/Multiplicity.lean
theorem multiplicity_le_emultiplicity :
    multiplicity a b ≤ emultiplicity a b

Proof state:
case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ ↑(multiplicity a b) ≤ emultiplicity a b

Tactic:
simp [hf.emultiplicity_eq_multiplicity]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
⊢ ↑(multiplicity a b) ≤ emultiplicity a b

Tactic:
by_cases hf : FiniteMultiplicity a b

Result:
case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ ↑(multiplicity a b) ≤ emultiplicity a b

case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ ↑(multiplicity a b) ≤ emultiplicity a b

Proof state:
case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ ↑(multiplicity a b) ≤ emultiplicity a b

Tactic:
simp [hf, emultiplicity_eq_top.2]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Classes/SatisfiesM.lean
theorem SatisfiesM_StateRefT_eq [Monad m] :
    SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s)

Proof state:
m : Type → Type
ω σ α✝ : Type
p : α✝ → Prop
x : StateRefT' ω σ m α✝
inst✝ : Monad m
⊢ SatisfiesM p x ↔ ∀ (s : ST.Ref ω σ), SatisfiesM p (x s)

Tactic:
simp [SatisfiesM_ReaderT_eq, ReaderT.run]

Result:
no goals
-- Mathlib/Algebra/FreeMonoid/Symbols.lean
theorem symbols_mul {a b : FreeMonoid α} : symbols (a * b) = symbols a ∪ symbols b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : FreeMonoid α
⊢ (a * b).symbols = a.symbols ∪ b.symbols

Tactic:
simp only [symbols, List.mem_toFinset, Finset.mem_union]

Result:
α : Type u_1
inst✝ : DecidableEq α
a b : FreeMonoid α
⊢ List.toFinset (a * b) = List.toFinset a ∪ List.toFinset b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : FreeMonoid α
⊢ List.toFinset (a * b) = List.toFinset a ∪ List.toFinset b

Tactic:
apply List.toFinset_append

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem dist_le_diam_of_mem' (h : EMetric.diam s ≠ ⊤) (hx : x ∈ s) (hy : y ∈ s) :
    dist x y ≤ diam s

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : EMetric.diam s ≠ ⊤
hx : x ∈ s
hy : y ∈ s
⊢ (edist x y).toReal ≤ (EMetric.diam s).toReal

Tactic:
exact ENNReal.toReal_mono h <| EMetric.edist_le_diam_of_mem hx hy

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : EMetric.diam s ≠ ⊤
hx : x ∈ s
hy : y ∈ s
⊢ dist x y ≤ diam s

Tactic:
rw [diam, dist_edist]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : EMetric.diam s ≠ ⊤
hx : x ∈ s
hy : y ∈ s
⊢ (edist x y).toReal ≤ (EMetric.diam s).toReal
-- Mathlib/SetTheory/Nimber/Basic.lean
theorem lt_add_cases {a b c : Nimber} (h : a < b + c) : a + c < b ∨ a + b < c

Proof state:
a b c : Nimber
h : a < b + c
⊢ a + c < b ∨ a + b < c

Tactic:
obtain ha | hb | hc := add_trichotomy <| add_assoc a b c ▸ add_ne_zero_iff.2 h.ne

Result:
case inl
a b c : Nimber
h : a < b + c
ha : b + c < a
⊢ a + c < b ∨ a + b < c

case inr.inl
a b c : Nimber
h : a < b + c
hb : c + a < b
⊢ a + c < b ∨ a + b < c

case inr.inr
a b c : Nimber
h : a < b + c
hc : a + b < c
⊢ a + c < b ∨ a + b < c

Proof state:
case inl
a b c : Nimber
h : a < b + c
ha : b + c < a
⊢ a + c < b ∨ a + b < c

case inr.inl
a b c : Nimber
h : a < b + c
hb : c + a < b
⊢ a + c < b ∨ a + b < c

case inr.inr
a b c : Nimber
h : a < b + c
hc : a + b < c
⊢ a + c < b ∨ a + b < c

Tactic:
exacts [(h.asymm ha).elim, Or.inl <| add_comm c a ▸ hb, Or.inr hc]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem lookupAll_length_le_one (a : α) {l : List (Sigma β)} (h : l.NodupKeys) :
    length (lookupAll a l) ≤ 1

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ (lookupAll a l).length ≤ 1

Tactic:
rwa [← nodup_replicate, ← map_const]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (lookupAll a l).length ≤ 1

Tactic:
have := Nodup.sublist ((lookupAll_sublist a l).map _) h

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map Sigma.fst (map (Sigma.mk a) (lookupAll a l))).Nodup
⊢ (lookupAll a l).length ≤ 1

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map Sigma.fst (map (Sigma.mk a) (lookupAll a l))).Nodup
⊢ (lookupAll a l).length ≤ 1

Tactic:
rw [map_map] at this

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ (lookupAll a l).length ≤ 1
-- Mathlib/Algebra/Homology/Homotopy.lean
lemma prevD_eq_zero (f : ∀ i j, C.X i ⟶ D.X j) (i : ι) (hi : ¬ c.Rel (c.prev i) i) :
    prevD i f = 0

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel (c.prev i) i
⊢ (prevD i) f = 0

Tactic:
dsimp [prevD]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel (c.prev i) i
⊢ f i (c.prev i) ≫ D.d (c.prev i) i = 0

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel (c.prev i) i
⊢ f i (c.prev i) ≫ D.d (c.prev i) i = 0

Tactic:
rw [shape _ _ _ hi, comp_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
lemma cyclesMap_eq [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    cyclesMap φ = h₁.cyclesIso.hom ≫ γ.φK ≫ h₂.cyclesIso.inv

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ cyclesMap φ = h₁.cyclesIso.hom ≫ γ.φK ≫ h₂.cyclesIso.inv

Tactic:
dsimp [LeftHomologyData.cyclesIso, cyclesMapIso']

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ cyclesMap φ = cyclesMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φK ≫ cyclesMap' (𝟙 S₂) h₂ S₂.leftHomologyData

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ cyclesMap φ = cyclesMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φK ≫ cyclesMap' (𝟙 S₂) h₂ S₂.leftHomologyData

Tactic:
rw [← γ.cyclesMap'_eq, ← cyclesMap'_comp, ← cyclesMap'_comp, id_comp, comp_id]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ cyclesMap φ = cyclesMap' φ S₁.leftHomologyData S₂.leftHomologyData

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ cyclesMap φ = cyclesMap' φ S₁.leftHomologyData S₂.leftHomologyData

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Int/NatPrime.lean
theorem Prime.dvd_natAbs_of_coe_dvd_sq {p : ℕ} (hp : p.Prime) (k : ℤ) (h : (p : ℤ) ∣ k ^ 2) :
    p ∣ k.natAbs

Proof state:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ k.natAbs

Tactic:
apply @Nat.Prime.dvd_of_dvd_pow _ _ 2 hp

Result:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ k.natAbs ^ 2

Proof state:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ k.natAbs ^ 2

Tactic:
rwa [sq, ← natAbs_mul, ← natCast_dvd, ← sq]

Result:
no goals