harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/FixedPoints.lean
theorem lfp_lfp (h : α →o α →o α) : (lfp.comp h).lfp = h.onDiag.lfp

Proof state:
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
⊢ lfp (lfp.comp h) = lfp h.onDiag

Tactic:
let a := (lfp.comp h).lfp

Result:
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
⊢ lfp (lfp.comp h) = lfp h.onDiag

Proof state:
case refine_1
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
⊢ (lfp.comp h) (lfp h.onDiag) ≤ lfp h.onDiag

Tactic:
exact lfp_le _ h.onDiag.map_lfp.le

Result:
no goals

Proof state:
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
⊢ lfp (lfp.comp h) = lfp h.onDiag

Tactic:
refine (lfp_le _ ?_).antisymm (lfp_le _ (Eq.le ?_))

Result:
case refine_1
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
⊢ (lfp.comp h) (lfp h.onDiag) ≤ lfp h.onDiag

case refine_2
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
⊢ h.onDiag (lfp (lfp.comp h)) = lfp (lfp.comp h)

Proof state:
case refine_2
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
ha : (⇑lfp ∘ ⇑h) a = a
⊢ h.onDiag (lfp (lfp.comp h)) = lfp (lfp.comp h)

Tactic:
calc
  h a a = h a (h a).lfp := congr_arg (h a) ha.symm
  _ = (h a).lfp := (h a).map_lfp
  _ = a := ha

Result:
no goals

Proof state:
case refine_2
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
⊢ h.onDiag (lfp (lfp.comp h)) = lfp (lfp.comp h)

Tactic:
have ha : (lfp ∘ h) a = a := (lfp.comp h).map_lfp

Result:
case refine_2
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
ha : (⇑lfp ∘ ⇑h) a = a
⊢ h.onDiag (lfp (lfp.comp h)) = lfp (lfp.comp h)
-- Mathlib/Probability/Kernel/Invariance.lean
theorem bind_smul (κ : Kernel α β) (μ : Measure α) (r : ℝ≥0∞) : (r • μ).bind κ = r • μ.bind κ

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
r : ℝ≥0∞
s : Set β
hs : MeasurableSet s
⊢ ((r • μ).bind ⇑κ) s = (r • μ.bind ⇑κ) s

Tactic:
rw [Measure.bind_apply hs (Kernel.measurable _), lintegral_smul_measure, Measure.coe_smul,
  Pi.smul_apply, Measure.bind_apply hs (Kernel.measurable _), smul_eq_mul]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
r : ℝ≥0∞
⊢ (r • μ).bind ⇑κ = r • μ.bind ⇑κ

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
r : ℝ≥0∞
s : Set β
hs : MeasurableSet s
⊢ ((r • μ).bind ⇑κ) s = (r • μ.bind ⇑κ) s
-- Mathlib/Order/Interval/Set/Basic.lean
@[simp] lemma Ici_False : Ici False = univ

Proof state:
⊢ Ici False = univ

Tactic:
aesop

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem TransGen.lift {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → p (f a) (f b))
    (hab : TransGen r a b) : TransGen p (f a) (f b)

Proof state:
case tail
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
b✝ c✝ : α
a✝ : TransGen r a b✝
hcd : r b✝ c✝
hac : TransGen p (f a) (f b✝)
⊢ TransGen p (f a) (f c✝)

Tactic:
exact TransGen.tail hac (h _ _ hcd)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
hab : TransGen r a b
⊢ TransGen p (f a) (f b)

Tactic:
induction hab with
| single hac => exact TransGen.single (h a _ hac)
| tail _ hcd hac => exact TransGen.tail hac (h _ _ hcd)

Result:
no goals

Proof state:
case single
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
b✝ : α
hac : r a b✝
⊢ TransGen p (f a) (f b✝)

Tactic:
exact TransGen.single (h a _ hac)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem some_eq_getElem?_iff {a : Vector α n} : some b = a[i]? ↔ ∃ h : i < n, a[i] = b

Proof state:
α : Type u_1
n : Nat
b : α
i : Nat
a : Vector α n
⊢ some b = a[i]? ↔ ∃ h, a[i] = b

Tactic:
rw [eq_comm, getElem?_eq_some_iff]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_smul_sub_left (x y : V) (r : ℝ) :
    (o.oangle (r • y - x) y).sign = -(o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
⊢ (o.oangle (r • y - x) y).sign = -(o.oangle x y).sign

Tactic:
rw [← oangle_sign_neg_left, sub_eq_neg_add, oangle_sign_add_smul_left]

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
lemma ringExpChar.eq (q : ℕ) [h : ExpChar R q] : ringExpChar R = q

Proof state:
case prime
R : Type u_1
inst✝ : NonAssocSemiring R
q : ℕ
h : Nat.Prime q
hchar✝ : CharP R q
⊢ q ⊔ 1 = q

Tactic:
exact Nat.max_eq_left h.one_lt.le

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
q : ℕ
h : ExpChar R q
⊢ ringExpChar R = q

Tactic:
rcases h with _ | h

Result:
case zero
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
⊢ ringExpChar R = 1

case prime
R : Type u_1
inst✝ : NonAssocSemiring R
q : ℕ
h : Nat.Prime q
hchar✝ : CharP R q
⊢ ringExpChar R = q

Proof state:
case zero
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
this : CharP R 0
⊢ ringExpChar R = 1

Tactic:
rw [ringExpChar, ringChar.eq R 0]

Result:
case zero
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
this : CharP R 0
⊢ 0 ⊔ 1 = 1

Proof state:
case zero
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
⊢ ringExpChar R = 1

Tactic:
haveI := CharP.ofCharZero R

Result:
case zero
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
this : CharP R 0
⊢ ringExpChar R = 1

Proof state:
case zero
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
this : CharP R 0
⊢ 0 ⊔ 1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
case prime
R : Type u_1
inst✝ : NonAssocSemiring R
q : ℕ
h : Nat.Prime q
hchar✝ : CharP R q
⊢ ringExpChar R = q

Tactic:
rw [ringExpChar, ringChar.eq R q]

Result:
case prime
R : Type u_1
inst✝ : NonAssocSemiring R
q : ℕ
h : Nat.Prime q
hchar✝ : CharP R q
⊢ q ⊔ 1 = q
-- Mathlib/Data/ENNReal/Basic.lean
theorem toNNReal_eq_one_iff (x : ℝ≥0∞) : x.toNNReal = 1 ↔ x = 1 :=
  WithTop.untopD_eq_iff.trans <| by simp

Proof state:
x : ℝ≥0∞
⊢ x = ↑1 ∨ x = ⊤ ∧ 1 = 0 ↔ x = 1

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/ClassEquation.lean
theorem sum_conjClasses_card_eq_card [Fintype <| ConjClasses G] [Fintype G]
    [∀ x : ConjClasses G, Fintype x.carrier] :
    ∑ x : ConjClasses G, x.carrier.toFinset.card = Fintype.card G

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑x.carrier
⊢ (x : ConjClasses G) × ↑x.carrier ≃ G

Tactic:
simpa [carrier_eq_preimage_mk] using Equiv.sigmaFiberEquiv ConjClasses.mk

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑x.carrier
this : (x : ConjClasses G) × ↑x.carrier ≃ G
⊢ ∑ x : ConjClasses G, x.carrier.toFinset.card = Fintype.card G

Tactic:
simpa using (Fintype.card_congr this)

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑x.carrier
⊢ ∑ x : ConjClasses G, x.carrier.toFinset.card = Fintype.card G

Tactic:
suffices (Σ x : ConjClasses G, x.carrier) ≃ G by simpa using (Fintype.card_congr this)

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑x.carrier
⊢ (x : ConjClasses G) × ↑x.carrier ≃ G
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem mem_lieSpan {x : L} : x ∈ lieSpan R L s ↔ ∀ K : LieSubalgebra R L, s ⊆ K → x ∈ K

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x : L
⊢ x ∈ ↑(lieSpan R L s) ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K

Tactic:
rw [lieSpan, sInf_coe]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x : L
⊢ x ∈ ⋂ s_1 ∈ {N | s ⊆ ↑N}, ↑s_1 ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x : L
⊢ x ∈ lieSpan R L s ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K

Tactic:
change x ∈ (lieSpan R L s : Set L) ↔ _

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x : L
⊢ x ∈ ↑(lieSpan R L s) ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x : L
⊢ x ∈ ⋂ s_1 ∈ {N | s ⊆ ↑N}, ↑s_1 ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K

Tactic:
exact Set.mem_iInter₂

Result:
no goals
-- Mathlib/CategoryTheory/EssentialImage.lean
lemma essImage_ext (F : C ⥤ D) {X Y : F.EssImageSubcategory} (f g : X ⟶ Y)
    (h : F.essImageInclusion.map f = F.essImageInclusion.map g) : f = g

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : F.EssImageSubcategory
f g : X ⟶ Y
h : F.essImageInclusion.map f = F.essImageInclusion.map g
⊢ f = g

Tactic:
simpa using h

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToHom_map (F : C ⥤ D) {X Y : C} (p : X = Y) :
    F.map (eqToHom p) = eqToHom (congr_arg F.obj p)

Proof state:
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ F.map (eqToHom ⋯) = eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
p : X = Y
⊢ F.map (eqToHom p) = eqToHom ⋯

Tactic:
cases p

Result:
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ F.map (eqToHom ⋯) = eqToHom ⋯
-- Mathlib/RingTheory/Int/Basic.lean
theorem Int.Prime.dvd_mul' {m n : ℤ} {p : ℕ} (hp : Nat.Prime p) (h : (p : ℤ) ∣ m * n) :
    (p : ℤ) ∣ m ∨ (p : ℤ) ∣ n

Proof state:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ m.natAbs ∨ p ∣ n.natAbs

Tactic:
exact Int.Prime.dvd_mul hp h

Result:
no goals

Proof state:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ ↑p ∣ m ∨ ↑p ∣ n

Tactic:
rw [Int.natCast_dvd, Int.natCast_dvd]

Result:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ m.natAbs ∨ p ∣ n.natAbs
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem ne_add_one (n : Nat) : n ≠ n + 1 := fun h => by cases h

Proof state:
n : Nat
h : n = n + 1
⊢ False

Tactic:
cases h

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem monic_ascPochhammer (n : ℕ) [Nontrivial S] [NoZeroDivisors S] :
    Monic <| ascPochhammer S n

Proof state:
case zero
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
⊢ (ascPochhammer S 0).Monic

Tactic:
simp

Result:
no goals

Proof state:
S : Type u
inst✝² : Semiring S
n : ℕ
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
⊢ (ascPochhammer S n).Monic

Tactic:
induction' n with n hn

Result:
case zero
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
⊢ (ascPochhammer S 0).Monic

case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
n : ℕ
hn : (ascPochhammer S n).Monic
⊢ (ascPochhammer S (n + 1)).Monic

Proof state:
case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
n : ℕ
hn : (ascPochhammer S n).Monic
this : (X + 1).leadingCoeff = 1
⊢ (ascPochhammer S (n + 1)).Monic

Tactic:
rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
  leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
  monic_X, one_mul, one_mul, this, one_pow]

Result:
no goals

Proof state:
case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
n : ℕ
hn : (ascPochhammer S n).Monic
⊢ (ascPochhammer S (n + 1)).Monic

Tactic:
have : leadingCoeff (X + 1 : S[X]) = 1 := leadingCoeff_X_add_C 1

Result:
case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
n : ℕ
hn : (ascPochhammer S n).Monic
this : (X + 1).leadingCoeff = 1
⊢ (ascPochhammer S (n + 1)).Monic
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma cpow_inv_two_im_eq_sqrt {x : ℂ} (hx : 0 ≤ x.im) :
    (x ^ (2⁻¹ : ℂ)).im = sqrt ((‖x‖ - x.re) / 2)

Proof state:
x : ℂ
hx : 0 ≤ x.im
⊢ (x ^ 2⁻¹).im = √((‖x‖ - x.re) / 2)

Tactic:
rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
  ← Real.sqrt_eq_rpow, sin_half_eq_sqrt, ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub,
  mul_one, norm_mul_cos_arg]

Result:
case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.arg

case hr
x : ℂ
hx : 0 ≤ x.im
⊢ x.arg ≤ 2 * π

Proof state:
case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.arg

Tactic:
rwa [arg_nonneg_iff]

Result:
no goals

Proof state:
case hr
x : ℂ
hx : 0 ≤ x.im
⊢ x.arg ≤ 2 * π

Tactic:
linarith [pi_pos, arg_le_pi x]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem degree_eq_one_iff_unique_adj {G' : Subgraph G} {v : V} [Fintype (G'.neighborSet v)] :
    G'.degree v = 1 ↔ ∃! w : V, G'.Adj v w

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
⊢ G'.degree v = 1 ↔ ∃! w, G'.Adj v w

Tactic:
rw [← finset_card_neighborSet_eq_degree, Finset.card_eq_one, Finset.singleton_iff_unique_mem]

Result:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
⊢ (∃! a, a ∈ (G'.neighborSet v).toFinset) ↔ ∃! w, G'.Adj v w

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
⊢ (∃! a, a ∈ (G'.neighborSet v).toFinset) ↔ ∃! w, G'.Adj v w

Tactic:
simp only [Set.mem_toFinset, mem_neighborSet]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x

Proof state:
α : Type u_1
a : Array α
x : α
⊢ (a.push x)[a.size]? = some x

Tactic:
rw [getElem?_pos, getElem_push_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem arithShiftRight_congr (m n : Nat) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m)
    (rhs' : BitVec n) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    BitVec.sshiftRight' lhs rhs = BitVec.sshiftRight' lhs' rhs'

Proof state:
m n : Nat
lhs : BitVec m
rhs : BitVec n
lhs' : BitVec m
rhs' : BitVec n
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs.sshiftRight' rhs = lhs'.sshiftRight' rhs'

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem mul_injective_of_disjoint {H₁ H₂ : Subgroup G} (h : Disjoint H₁ H₂) :
    Function.Injective (fun g => g.1 * g.2 : H₁ × H₂ → G)

Proof state:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (fun g => ↑g.1 * ↑g.2) x = (fun g => ↑g.1 * ↑g.2) y
⊢ x = y

Tactic:
rw [← inv_mul_eq_iff_eq_mul, ← mul_assoc, ← mul_inv_eq_one, mul_assoc] at hxy

Result:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑y.1)⁻¹ * ↑x.1 * (↑x.2 * (↑y.2)⁻¹) = 1
⊢ x = y

Proof state:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : ↑(y.1⁻¹ * x.1) = 1 ∧ ↑(x.2 * y.2⁻¹) = 1
⊢ x = y

Tactic:
rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
  Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
⊢ Injective fun g => ↑g.1 * ↑g.2

Tactic:
intro x y hxy

Result:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (fun g => ↑g.1 * ↑g.2) x = (fun g => ↑g.1 * ↑g.2) y
⊢ x = y

Proof state:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑y.1)⁻¹ * ↑x.1 * (↑x.2 * (↑y.2)⁻¹) = 1
⊢ x = y

Tactic:
replace hxy := disjoint_iff_mul_eq_one.mp h (y.1⁻¹ * x.1).prop (x.2 * y.2⁻¹).prop hxy

Result:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : ↑(y.1⁻¹ * x.1) = 1 ∧ ↑(x.2 * y.2⁻¹) = 1
⊢ x = y
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem ofComapInfPrincipal_mem (h : m '' s ∈ g) : s ∈ ofComapInfPrincipal h

Proof state:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this✝ : f.NeBot
this : s ∈ f
⊢ s ∈ ofComapInfPrincipal h

Tactic:
exact le_def.mp (of_le _) s this

Result:
no goals

Proof state:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : f.NeBot
⊢ s ∈ ofComapInfPrincipal h

Tactic:
have : s ∈ f := mem_inf_of_right (mem_principal_self s)

Result:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this✝ : f.NeBot
this : s ∈ f
⊢ s ∈ ofComapInfPrincipal h

Proof state:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ s ∈ ofComapInfPrincipal h

Tactic:
let f := Filter.comap m g ⊓ 𝓟 s

Result:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ s ∈ ofComapInfPrincipal h

Proof state:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ s ∈ ofComapInfPrincipal h

Tactic:
haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h

Result:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : f.NeBot
⊢ s ∈ ofComapInfPrincipal h
-- Mathlib/Algebra/Homology/ImageToKernel.lean
theorem imageToKernel_comp_mono {D : V} (h : C ⟶ D) [Mono h] (w) :
    imageToKernel f (g ≫ h) w =
      imageToKernel f g ((cancel_mono h).mp (by simpa using w : (f ≫ g) ≫ h = 0 ≫ h)) ≫
        (Subobject.isoOfEq _ _ (kernelSubobject_comp_mono g h)).inv

Proof state:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
D : V
h : C ⟶ D
inst✝ : Mono h
w : f ≫ g ≫ h = 0
⊢ imageToKernel f (g ≫ h) w = imageToKernel f g ⋯ ≫ ((kernelSubobject (g ≫ h)).isoOfEq (kernelSubobject g) ⋯).inv

Tactic:
ext

Result:
case h
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
D : V
h : C ⟶ D
inst✝ : Mono h
w : f ≫ g ≫ h = 0
⊢ imageToKernel f (g ≫ h) w ≫ (kernelSubobject (g ≫ h)).arrow =
    (imageToKernel f g ⋯ ≫ ((kernelSubobject (g ≫ h)).isoOfEq (kernelSubobject g) ⋯).inv) ≫
      (kernelSubobject (g ≫ h)).arrow

Proof state:
case h
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
D : V
h : C ⟶ D
inst✝ : Mono h
w : f ≫ g ≫ h = 0
⊢ imageToKernel f (g ≫ h) w ≫ (kernelSubobject (g ≫ h)).arrow =
    (imageToKernel f g ⋯ ≫ ((kernelSubobject (g ≫ h)).isoOfEq (kernelSubobject g) ⋯).inv) ≫
      (kernelSubobject (g ≫ h)).arrow

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
D : V
h : C ⟶ D
inst✝ : Mono h
w : f ≫ g ≫ h = 0
⊢ (f ≫ g) ≫ h = 0 ≫ h

Tactic:
simpa using w

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_symmDiff_inf : a ∆ b ∆ (a ⊓ b) = a ⊔ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b ∆ (a ⊓ b) = a ⊔ b

Tactic:
rw [← symmDiff_sdiff_inf a, sdiff_symmDiff_eq_sup, symmDiff_sup_inf]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
lemma toColex_ne_toColex {s t : Finset α} : toColex s ≠ toColex t ↔ s ≠ t

Proof state:
α : Type u_1
s t : Finset α
⊢ { ofColex := s } ≠ { ofColex := t } ↔ s ≠ t

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem lift_eq_iff_equiv (c₁ c₂ : Computation α) : LiftRel (· = ·) c₁ c₂ ↔ c₁ ~ c₂ :=
  ⟨fun ⟨h1, h2⟩ a =>
    ⟨fun a1 => by let ⟨b, b2, ab⟩ := h1 a1; rwa [ab],
     fun a2 => by let ⟨b, b1, ab⟩ := h2 a2; rwa [← ab]⟩,
    fun e => ⟨fun {a} a1 => ⟨a, (e _).1 a1, rfl⟩, fun {a} a2 => ⟨a, (e _).2 a2, rfl⟩⟩⟩

Proof state:
α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 => x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 => x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 => x1 = x2) a b
a1 : a ∈ c₁
b : α
b2 : b ∈ c₂
ab : (fun x1 x2 => x1 = x2) a b
⊢ a ∈ c₂

Tactic:
rwa [ab]

Result:
no goals

Proof state:
α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 => x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 => x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 => x1 = x2) a b
a2 : a ∈ c₂
⊢ a ∈ c₁

Tactic:
let ⟨b, b1, ab⟩ := h2 a2

Result:
α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 => x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 => x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 => x1 = x2) a b
a2 : a ∈ c₂
b : α
b1 : b ∈ c₁
ab : (fun x1 x2 => x1 = x2) b a
⊢ a ∈ c₁

Proof state:
α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 => x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 => x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 => x1 = x2) a b
a2 : a ∈ c₂
b : α
b1 : b ∈ c₁
ab : (fun x1 x2 => x1 = x2) b a
⊢ a ∈ c₁

Tactic:
rwa [← ab]

Result:
no goals

Proof state:
α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 => x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 => x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 => x1 = x2) a b
a1 : a ∈ c₁
⊢ a ∈ c₂

Tactic:
let ⟨b, b2, ab⟩ := h1 a1

Result:
α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 => x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 => x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 => x1 = x2) a b
a1 : a ∈ c₁
b : α
b2 : b ∈ c₂
ab : (fun x1 x2 => x1 = x2) a b
⊢ a ∈ c₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem mapM_append [Monad m] [LawfulMonad m] (f : α → m β) {l₁ l₂ : Array α} :
    (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f))

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l₂ : Array α
l₁ : List α
⊢ mapM f ({ toList := l₁ } ++ l₂) = do
    let __do_lift ← mapM f { toList := l₁ }
    let __do_lift_1 ← mapM f l₂
    pure (__do_lift ++ __do_lift_1)

Tactic:
rcases l₂ with ⟨l₂⟩

Result:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l₁ l₂ : List α
⊢ mapM f ({ toList := l₁ } ++ { toList := l₂ }) = do
    let __do_lift ← mapM f { toList := l₁ }
    let __do_lift_1 ← mapM f { toList := l₂ }
    pure (__do_lift ++ __do_lift_1)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l₁ l₂ : Array α
⊢ mapM f (l₁ ++ l₂) = do
    let __do_lift ← mapM f l₁
    let __do_lift_1 ← mapM f l₂
    pure (__do_lift ++ __do_lift_1)

Tactic:
rcases l₁ with ⟨l₁⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l₂ : Array α
l₁ : List α
⊢ mapM f ({ toList := l₁ } ++ l₂) = do
    let __do_lift ← mapM f { toList := l₁ }
    let __do_lift_1 ← mapM f l₂
    pure (__do_lift ++ __do_lift_1)

Proof state:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l₁ l₂ : List α
⊢ mapM f ({ toList := l₁ } ++ { toList := l₂ }) = do
    let __do_lift ← mapM f { toList := l₁ }
    let __do_lift_1 ← mapM f { toList := l₂ }
    pure (__do_lift ++ __do_lift_1)

Tactic:
simp

Result:
no goals