harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Impl.lean
theorem splitRevInTwo'_fst (l : { l : List α // l.length = n }) :
    (splitRevInTwo' l).1 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).2.1, by simp; omega⟩

Proof state:
case e_val.e_a
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ l.val.length - n / 2 = (n + 1) / 2

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ ⟨drop (l.val.length - n / 2) l.val.reverse, ⋯⟩ = ⟨drop ((n + 1) / 2) l.val.reverse, ⋯⟩

Tactic:
congr

Result:
case e_val.e_a
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ l.val.length - n / 2 = (n + 1) / 2

Proof state:
α : Type ?u.38724
n : Nat
l : { l // l.length = n }
⊢ l.val.reverse.length = ?m.38773

Tactic:
simpa using l.2

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ (splitRevInTwo' l).fst = ⟨(splitInTwo ⟨l.val.reverse, ⋯⟩).snd.val, ⋯⟩

Tactic:
simp only [splitRevInTwo', splitRevAt_eq, reverse_take, splitInTwo_snd]

Result:
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ ⟨drop (l.val.length - n / 2) l.val.reverse, ⋯⟩ = ⟨drop ((n + 1) / 2) l.val.reverse, ⋯⟩

Proof state:
α : Type ?u.38724
n : Nat
l : { l // l.length = n }
⊢ (splitInTwo ⟨l.val.reverse, ⋯⟩).snd.val.length = n / 2

Tactic:
simp

Result:
α : Type ?u.38724
n : Nat
l : { l // l.length = n }
⊢ l.val.length - (n + 1) / 2 = n / 2

Proof state:
α : Type ?u.38724
n : Nat
l : { l // l.length = n }
⊢ l.val.length - (n + 1) / 2 = n / 2

Tactic:
omega

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isClique_map_finset_iff :
    (G.map f).IsClique t ↔ #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique s ∧ s.map f = t

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
⊢ (SimpleGraph.map f G).IsClique ↑t ↔ #t ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
obtain (ht | ht) := le_or_lt #t 1

Result:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : #t ≤ 1
⊢ (SimpleGraph.map f G).IsClique ↑t ↔ #t ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ (SimpleGraph.map f G).IsClique ↑t ↔ #t ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

Proof state:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : #t ≤ 1
⊢ (SimpleGraph.map f G).IsClique ↑t

Tactic:
exact IsClique.of_subsingleton <| card_le_one.1 ht

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : #t ≤ 1
⊢ (SimpleGraph.map f G).IsClique ↑t ↔ #t ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
simp only [ht, true_or, iff_true]

Result:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : #t ≤ 1
⊢ (SimpleGraph.map f G).IsClique ↑t

Proof state:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ (SimpleGraph.map f G).IsClique ↑t ↔ #t ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
rw [isClique_map_finset_iff_of_nontrivial, ← not_lt]

Result:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ↔ ¬1 < #t ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ t.Nontrivial

Proof state:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ↔ ¬1 < #t ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
simp [ht, Finset.map_eq_image]

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ t.Nontrivial

Tactic:
exact Finset.one_lt_card_iff_nontrivial.mp ht

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem inv_id : inv (𝟙 X) = 𝟙 X

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ inv (𝟙 X) = 𝟙 X

Tactic:
apply inv_eq_of_hom_inv_id

Result:
case hom_inv_id
C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X

Proof state:
case hom_inv_id
C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_flatMap (xs : Vector α n) (f : α → Vector β m) (p : β → Bool) :
    (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p)

Proof state:
case mk
α : Type u_1
n : Nat
β : Type
m : Nat
f : α → Vector β m
p : β → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ find? p ({ toArray := toArray✝, size_toArray := size_toArray✝ }.flatMap f) =
    findSome? (fun x => find? p (f x)) { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp [Array.find?_flatMap, Array.flatMap_toArray]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type
m : Nat
xs : Vector α n
f : α → Vector β m
p : β → Bool
⊢ find? p (xs.flatMap f) = findSome? (fun x => find? p (f x)) xs

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : Nat
β : Type
m : Nat
f : α → Vector β m
p : β → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ find? p ({ toArray := toArray✝, size_toArray := size_toArray✝ }.flatMap f) =
    findSome? (fun x => find? p (f x)) { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem map_comap_incl {I₁ I₂ : LieIdeal R L} : map I₁.incl (comap I₁.incl I₂) = I₁ ⊓ I₂

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I₁ I₂ : LieIdeal R L
⊢ map I₁.incl (comap I₁.incl I₂) = I₁ ⊓ I₂

Tactic:
conv_rhs => rw [← I₁.incl_idealRange]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I₁ I₂ : LieIdeal R L
⊢ map I₁.incl (comap I₁.incl I₂) = I₁.incl.idealRange ⊓ I₂

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I₁ I₂ : LieIdeal R L
⊢ I₁.incl.IsIdealMorphism

Tactic:
exact I₁.incl_isIdealMorphism

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I₁ I₂ : LieIdeal R L
⊢ map I₁.incl (comap I₁.incl I₂) = I₁.incl.idealRange ⊓ I₂

Tactic:
rw [← map_comap_eq]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I₁ I₂ : LieIdeal R L
⊢ I₁.incl.IsIdealMorphism
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y

Proof state:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
⊢ x.sdiv y = x &&& y

Tactic:
have hy : y = 0#1 ∨ y = 1#1 := by bv_omega

Result:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
hy : y = 0#1 ∨ y = 1#1
⊢ x.sdiv y = x &&& y

Proof state:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
⊢ y = 0#1 ∨ y = 1#1

Tactic:
bv_omega

Result:
no goals

Proof state:
x y : BitVec 1
⊢ x = 0#1 ∨ x = 1#1

Tactic:
bv_omega

Result:
no goals

Proof state:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
hy : y = 0#1 ∨ y = 1#1
⊢ x.sdiv y = x &&& y

Tactic:
rcases hx with rfl | rfl <;>
  rcases hy with rfl | rfl <;>
    rfl

Result:
no goals

Proof state:
x y : BitVec 1
⊢ x.sdiv y = x &&& y

Tactic:
have hx : x = 0#1 ∨ x = 1#1 := by bv_omega

Result:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
⊢ x.sdiv y = x &&& y
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem liftHom_root (h : IsAdjoinRoot S f) : h.liftHom x hx' h.root = x

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
f : R[X]
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
x : T
inst✝ : Algebra R T
hx' : (aeval x) f = 0
h : IsAdjoinRoot S f
⊢ (liftHom x hx' h) h.root = x

Tactic:
rw [← lift_algebraMap_apply, lift_root]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
/-- A constructor for `PosSMulMono` requiring you to prove `b₁ ≤ b₂ → a • b₁ ≤ a • b₂` only when
`0 < a` -/
lemma PosSMulMono.of_pos (h₀ : ∀ a : α, 0 < a → ∀ b₁ b₂ : β, b₁ ≤ b₂ → a • b₁ ≤ a • b₂) :
    PosSMulMono α β where
  elim a ha b₁ b₂ h

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
ha : 0 = a
⊢ a • b₁ ≤ a • b₂

Tactic:
simp [← ha]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
⊢ a • b₁ ≤ a • b₂

Tactic:
obtain ha | ha := ha.eq_or_lt

Result:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
ha : 0 = a
⊢ a • b₁ ≤ a • b₂

case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
ha : 0 < a
⊢ a • b₁ ≤ a • b₂

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
ha : 0 < a
⊢ a • b₁ ≤ a • b₂

Tactic:
exact h₀ _ ha _ _ h

Result:
no goals
-- Mathlib/Data/Int/Interval.lean
theorem card_fintype_Ioc : Fintype.card (Set.Ioc a b) = (b - a).toNat

Proof state:
a b : ℤ
⊢ Fintype.card ↑(Set.Ioc a b) = (b - a).toNat

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_iterate_comp (k : ℕ) :
    (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree

Proof state:
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
k : ℕ
⊢ (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree

Tactic:
induction k with
| zero => simp
| succ k IH => rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ (p.comp^[0] q).natDegree = p.natDegree ^ 0 * q.natDegree

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
k : ℕ
IH : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
⊢ (p.comp^[k + 1] q).natDegree = p.natDegree ^ (k + 1) * q.natDegree

Tactic:
rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem map_add_univ [DecidableEq ι] [Fintype ι] (m m' : ∀ i, M₁ i) :
    f (m + m') = ∑ s : Finset ι, f (s.piecewise m m')

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m m' : (i : ι) → M₁ i
⊢ f (m + m') = ∑ s : Finset ι, f (s.piecewise m m')

Tactic:
simpa using f.map_piecewise_add m m' Finset.univ

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem ne_zero_of_mk'_ne_zero {x : R} {y : M} (hxy : IsLocalization.mk' S x y ≠ 0) : x ≠ 0

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
y : ↥M
hxy : mk' S 0 y ≠ 0
⊢ False

Tactic:
exact hxy (IsLocalization.mk'_zero _)

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
hxy : mk' S x y ≠ 0
⊢ x ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
y : ↥M
hxy : mk' S 0 y ≠ 0
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sin_add_pi_div_two (θ : Angle) : sin (θ + ↑(π / 2)) = cos θ

Proof state:
case h
x✝ : ℝ
⊢ (↑x✝ + ↑(π / 2)).sin = (↑x✝).cos

Tactic:
exact Real.sin_add_pi_div_two _

Result:
no goals

Proof state:
θ : Angle
⊢ (θ + ↑(π / 2)).sin = θ.cos

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (↑x✝ + ↑(π / 2)).sin = (↑x✝).cos
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem le_of_mem_A {r ε : ℝ} {L : F} {x : ℝ} (hx : x ∈ A f L r ε) {y z : ℝ}
    (hy : y ∈ Icc x (x + r / 2)) (hz : z ∈ Icc x (x + r / 2)) :
  ‖f z - f y - (z - y) • L‖ ≤ ε * r

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r ε : ℝ
L : F
x : ℝ
hx : x ∈ A f L r ε
y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r

Tactic:
rcases hx with ⟨r', r'mem, hr'⟩

Result:
case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r ε : ℝ
L : F
x y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r ε : ℝ
L : F
x y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
⊢ x + r / 2 ≤ x + r'

Tactic:
linarith [r'mem.1]

Result:
no goals

Proof state:
case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r ε : ℝ
L : F
x y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r

Tactic:
have A : x + r / 2 ≤ x + r' := by linarith [r'mem.1]

Result:
case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r ε : ℝ
L : F
x y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
A : x + r / 2 ≤ x + r'
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r

Proof state:
case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r ε : ℝ
L : F
x y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
A : x + r / 2 ≤ x + r'
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r

Tactic:
exact hr' _ ((Icc_subset_Icc le_rfl A) hy) _ ((Icc_subset_Icc le_rfl A) hz)

Result:
no goals
-- Mathlib/Algebra/Module/Basic.lean
theorem map_inv_intCast_smul [AddCommGroup M] [AddCommGroup M₂] {F : Type*} [FunLike F M M₂]
    [AddMonoidHomClass F M M₂] (f : F) (R S : Type*) [DivisionRing R] [DivisionRing S] [Module R M]
    [Module S M₂] (z : ℤ) (x : M) : f ((z⁻¹ : R) • x) = (z⁻¹ : S) • f x

Proof state:
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
z : ℤ
x : M
⊢ f ((↑z)⁻¹ • x) = (↑z)⁻¹ • f x

Tactic:
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg

Result:
case intro.inl
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑↑n)⁻¹ • x) = (↑↑n)⁻¹ • f x

case intro.inr
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑(-↑n))⁻¹ • x) = (↑(-↑n))⁻¹ • f x

Proof state:
case intro.inr
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑(-↑n))⁻¹ • x) = (↑(-↑n))⁻¹ • f x

Tactic:
simp_rw [Int.cast_neg, Int.cast_natCast, inv_neg, neg_smul, map_neg,
  map_inv_natCast_smul _ R S]

Result:
no goals

Proof state:
case intro.inl
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑↑n)⁻¹ • x) = (↑↑n)⁻¹ • f x

Tactic:
rw [Int.cast_natCast, Int.cast_natCast, map_inv_natCast_smul _ R S]

Result:
no goals
-- Mathlib/Order/Chain.lean
theorem chainClosure_succ_total_aux (hc₁ : ChainClosure r c₁)
    (h : ∀ ⦃c₃⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂) :
    SuccChain r c₂ ⊆ c₁ ∨ c₁ ⊆ c₂

Proof state:
case succ.inr
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl

Result:
no goals

Proof state:
case union
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
hn : ¬SuccChain r c₂ ⊆ ⋃₀ s✝
a : Set α
ha : a ∈ s✝
⊢ a ⊆ c₂

Tactic:
exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha

Result:
no goals

Proof state:
case union
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
⊢ SuccChain r c₂ ⊆ ⋃₀ s✝ ∨ ⋃₀ s✝ ⊆ c₂

Tactic:
refine or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => ?_

Result:
case union
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
hn : ¬SuccChain r c₂ ⊆ ⋃₀ s✝
a : Set α
ha : a ∈ s✝
⊢ a ⊆ c₂

Proof state:
case succ
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃ ∨ c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
obtain ih | ih := ih

Result:
case succ.inl
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

case succ.inr
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Proof state:
case succ.inl
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
exact Or.inl (ih.trans subset_succChain)

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem corec_eq (f : β → Option (α × β)) (b : β) :
    destruct (corec f b) = omap (corec f) (f b)

Proof state:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
⊢ (corec f b).destruct = omap (corec f) (f b)

Tactic:
dsimp [corec, destruct, get]

Result:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩)) (corec' (Corec.f f) (some b) 0) =
    match f b with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Proof state:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩)) (corec' (Corec.f f) (some b) 0) =
    match f b with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Tactic:
rw [h]

Result:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩)) (Corec.f f (some b)).fst =
    match f b with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Proof state:
case some.mk.a
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ ↑(tail ⟨corec' (Corec.f f) (some b), ⋯⟩) = ↑⟨corec' (Corec.f f) (some b'), ⋯⟩

Tactic:
dsimp [corec, tail]

Result:
case some.mk.a
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ (corec' (Corec.f f) (some b)).tail = corec' (Corec.f f) (some b')
-- Mathlib/CategoryTheory/Opposites.lean
theorem op_inv {X Y : C} (f : X ⟶ Y) [IsIso f] : (inv f).op = inv f.op

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (inv f).op = inv f.op

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Result:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ f.op ≫ (inv f).op = 𝟙 (op Y)

Proof state:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ f.op ≫ (inv f).op = 𝟙 (op Y)

Tactic:
rw [← op_comp, IsIso.inv_hom_id, op_id]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.add_int_mul_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℤ) :
    f (x + n * c) = (n.negOnePow : ℤ) * f x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : Ring α
inst✝ : Ring β
h : Antiperiodic f c
n : ℤ
⊢ f (x + ↑n * c) = ↑↑n.negOnePow * f x

Tactic:
simpa only [zsmul_eq_mul] using h.add_zsmul_eq n

Result:
no goals